Clark's early model checker

To try these, download the mcb binary to somplace where you can access it when logged into uncle-leo.cs.unc.edu

Then download the models and run

   mcb paper.fsm

   mcb mcb.meet.fsm
The checker will read in the model and ask for fairness constraints. At that point just give it "." and hit return. Then it will be ready to give assertions to check.

For assertions, use the synta shown in Clark's TOPLAS paper online (last few pages). For the names of the atomic predicates, see the models. If the model shows (for example) a predicate named Pspeak.H then you will use Pspeak in an assertion. All assertions are terminated with "."