Model Checking

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

use machine login.cs.unc.edu to access and run mcb

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

First look at how to run the model checker "mcb" and how it operates using the two-process model show as an example in Clarke's paper:

./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

Now let's use a larger model, a version of this floor control protocol. This Pnet is a colored net, shown as an example of an expressive modeling notation. For our purposes we will simplify the net we analyze by reverting to a form of vanilla, traditional Pnet with only black tokens.

./mcb meet.fsm.good

   then when it asks for fairness constraints give "."  and return
   After that type in temporal logic assertions about the model.
   End the line/assertion with a "." to complete the syntax.

   This will run the model checker on a model made from the moderated 
   meeting floor control protocol shown in  this Pnet.  

   This is the model generated from the Pnet.

   Try these CTL formulae

Using this fill in 4,5,6, and 7 at the bottom with CTL formulae, and their English explanations, for three properties of this net that you would like to check. Make them interesting... non-trivial. For each formula you create, show the output from the model checker.