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

findinitobs(a,b,...,A);

Notes

Exactly like findinit, except that for each state with the given set of next observable actions, we give an observable trace leading to the state. That is, we take the the trace produced by findinit and delete all taus!

See also

  • findinit
  • deadlocks
    Edinburgh Concurrency Workbench (v7.1). Page generated: Sun Jul 18 11:46:51 BST 1999