Retrascope

The heuristic approach of detection the EFSM initial state and the 'reset' signal should be implemented.

If there is a guarded action G -> A, and:

1) x is clock-like variable, which:

a) x belongs to Events(G);
  b) if x belongs to Use(G) then {x} = Use(G) or Use(G) = null.
2) A consists of assignments of y := c, where c is constant.

Then guarded action leads to initial state, and x is reset.