/***********/
Jimmy Dias
UNC COMP 204
10/04/02
/***********/


The model checking code was designed to run using the SML/NJ 110.0.7
interpreter. 

test.ml contains the CTL formula for the handin material. Results for
checking each of the formula against the loaded module are found in meet.ctl.exp.

SAMPLE RUNS

************************************
checking extended set of CTL formula
************************************

sml> use "getModel.ml";
sml> use "chkModelExt.ml";
sml> val m = getModel "meet.fsm";
sml> val f = Ef(And(Pred "Pspeak",Pred "TgetFloor"));
sml> mCheckExt m f 0;


/**************** test.ml *************** /


val f1a = Ef (And(Pred "Pspeak", Pred "TgetFloor"));
val f1b = And(Ag(Imply(Pred "Pspeak", Not(Pred "TgetFloor"))), Ag (Imply(Pred "TgetFloor", Not(Pred "Pspeak"))));
val f2 = Ag(Imply(Not(Pred "Pmoderate"),Pred "Phold"));
val f3 = Ag(Imply(Pred "Phold",Ax(Af(Not(Pred "Phold")))));
val f4 = Ag(Imply(Pred "Pwait", Ax(Af(Not(Pred "Pwait")))));
val f5 = Or(Ag(Pred "Pmoderate"),Au(Not(Pred "Pmoderate"),Pred "Pmoderate"));
val f6 = Ef(And(Not(Pred "Pmoderate"),Pred "TgrabFloor"));


/**************** test.ml *************** /