mustpre: are two agents related by the must preorder?
Returns true iff for every s in the language of B (including
the empty s) if A converges at s (i.e. you can't get to a divergent
state by following observable path s) then B converges at s and every
acceptance set of B after s contains some acceptance set of A after s.
(Here "divergence" includes performing an infinite sequence of tau moves, as
well as @.)
See Hennessy: Algebraic Theory of Processes, MIT Press.
Edinburgh Concurrency Workbench (v7.1).
Page generated: Sun Jul 18 11:46:51 BST 1999