## mustpre: are two agents related by the must preorder?

`mustpre(A,B);`

### Notes

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.

### See also

musteq
maypre
testpre

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