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.fsmThe 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 "."