findinit: find states with a given set of next observable actions



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