findinit: find states with a given set of next observable actions
findinit(a,b,...,A);
Notes
So, for example, findinit (a,b,A) is equivalent to findinit (b,a,A), and
will give states reachable from A from which a and b are the only possible
next observable actions. That is, a state D reachable from A should appear
if D =a=> and D =b=> and for no other observable c does D =c=>. Note the
weak transitions here! It's not true that init(D) will be { a,b }.
Of course only observable actions are legal arguments.
For each such state, we give a trace leading to it.
See also
findinitobs
deadlocks
Edinburgh Concurrency Workbench (v7.1).
Page generated: Thu Jan 30 18:23:29 GMT 2003