## dfweak: find a weak HML formula distinguishing two agents

`dfweak(A,B);`

### Notes

Produces a weak HML formula which distinguishes between the two
agents if they are not weakly bisimilar. The formula is true of the
first agent and false of the second.

### See also

dfstrong
dftrace

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