Model Checking

You can find the source code and executables for Ed Clarke's original model checker here

~stotts/public_html/COMP723-s13/Mcheck/MCBsrc

Here is the COMP723-readme file:

use

login.cs.unc.edu

to run mcb


./mcb meet.fsm.good


this will run the model checker on a model made from the floor control protocol
shown in

./mcb paper.fsm

this will run the model checker on the two process model from the
clarke paper

syntax:

AG(C1 | T1 | N1).   expect true

AF(C1).   expect false from state 0 (which the model checker 
                                     does by default)

EF(C1 ^ C2).  expect false... both processes cant have the resource
                              at the same time