Files:

• ctl.ml : the ML code for the CTL model checker
• fsm.input : the current finite-state machine (FSM) input file (file must be named this to load)
• meet.fsm and test.fsm : two test FSM files

To begin, run

sml

and type

use "ctl.ml"

The current FSM in the file fsm.input will be loaded into the model checker. The main formula checking routine is called

ModelChecker(<formula string>)

The formula string is in postfix format with the following valid operations:

• p not
• p1 p2 and
• p1 p2 or
• p1 p2 ->
• p ax
• p ex
• p1 p2 au
• p1 p2 eu

Also, added the following extra operations, but they seem to cause problems on the required three test cases:

• p af
• p ef
• p ag
• p eg

Where p, p1, p2 are also valid postfix formulas ultimately consisting of atomic predicates at the leaves. For example, if we wish to evaluate

(A and B) or (C and !D)

we would write this in postfix as

A B and C D not and or

so our ModelChecker call would look like

ModelChecker("A B and C D not and or");

at the SML command line. The result will be true or false depending on if the formula is valid at the starting state of the FSM.

In addition, we can also get the current set of valid subformulas at each state printed as a list of list of strings in ML by simply called EvaluateFormula (instead of ModelChecker) with the same formula string.

There are two test FSM files (test.fsm and meet.fsm), just type

cp test.fsm fsm.input
or
cp meet.fsm fsm.input

to try the different FSM files.

Here are a few examples formula strings along with the output for the test.fsm file:

- EvaluateFormula("welcome not");
val it =
  [["welcome","allow","begin"],
   ["welcome not","overview","allow","orbiter","propulsion"],
   ["welcome not","overview","engines","inhibit","return","remove"],
   ["welcome not","engines","allow","return"],
   ["welcome","overview","inhibit","begin","remove"],
   ["welcome not","overview","inhibit","remove"],
   ["welcome not","overview","shuttle","inhibit","begin2","remove"],
   ["welcome not","shuttle","allow","begin2"]] : string list list

as you can see here the "welcome not" subformula was added to the valid subformula lists on all but two of the states; notice that those two states have the valid atomic preposition "welcome" so should not be valid for "welcome not".

- ModelChecker("welcome not");
val it = false : bool

so obviously, if we run the model checker on the same formula string, we get false since the formula "welcome not" is not valid at the first state (first list of strings in the output).

- EvaluateFormula("welcome not allow or inhibit and");
val it =
  [["welcome not allow or","welcome","allow","begin"],
   ["welcome not allow or","welcome not","overview","allow","orbiter",
    "propulsion"],
   ["welcome not allow or inhibit and","welcome not allow or","welcome not",
    "overview","engines","inhibit","return","remove"],
   ["welcome not allow or","welcome not","engines","allow","return"],
   ["welcome","overview","inhibit","begin","remove"],
   ["welcome not allow or inhibit and","welcome not allow or","welcome not",
    "overview","inhibit","remove"],
   ["welcome not allow or inhibit and","welcome not allow or","welcome not",
    "overview","shuttle","inhibit","begin2","remove"],
   ["welcome not allow or","welcome not","shuttle","allow","begin2"]]
  : string list list

This more sophisticated example evaluates a formula of the form "(!A or B) and C". We can see the valid subformulas for each state in the output lists.

- ModelChecker("welcome not allow or inhibit and");
val it = false : bool

Again, running the model checker verifies that this is also not a valid formula in the first state.

Let's evaluate (Pspeak and TgetFloor) or !Phold:

- EvaluateFormula("Pspeak TgetFloor and Phold not or");
val it =
  [["Pspeak TgetFloor and Phold not or","Phold not","Pmutex","Plisten",
    "Pmoderate","Ppool","Taddp","Tdelp","Tsusp","TgetFloor","TswapMod"],
   ["Pspeak TgetFloor and Phold not or","Phold not","Pspeak","Plisten",
    "Pmoderate","Ppool","TgrabFloor","Taddp","Tdelp","Tsusp","TreleaseFloor",
    "TswapMod"],
   ["Pspeak TgetFloor and Phold not or","Phold not","Pspeak","Pwait",
    "Pmoderate","Ppool","TgrabFloor","Taddp","Tresp","TreleaseFloor"],
   ["Pspeak TgetFloor and Phold not or","Phold not","Pmutex","Plisten","Pwait",
    "Pmoderate","Ppool","Taddp","Tdelp","Tsusp","Tresp","TgetFloor",...],
   ["Pspeak TgetFloor and Phold not or","Phold not","Pmutex","Pwait",
    "Pmoderate","Ppool","Taddp","Tresp"],
   ["Pspeak TgetFloor and Phold not or","Phold not","Pmutex","Plisten","Pwait",
    "Pmoderate","Ppool","Taddp","Tdelp","Tsusp","Tresp","TgetFloor",...],
   ["Pspeak TgetFloor and Phold not or","Phold not","Pspeak","Pwait",
    "Pmoderate","Ppool","TgrabFloor","Taddp","Tresp","TreleaseFloor"],
   ["Pspeak TgetFloor and Phold not or","Phold not","Pspeak","Plisten","Pwait",
    "Pmoderate","Ppool","TgrabFloor","Taddp","Tdelp","Tsusp","Tresp",...],
   ["Pspeak TgetFloor and Phold not or","Phold not","Pmutex","Plisten","Pwait",
    "Pmoderate","Ppool","Taddp","Tdelp","Tsusp","Tresp","TgetFloor",...],
   ["Pspeak TgetFloor and Phold not or","Phold not","Pmutex","Plisten",
    "Pmoderate","Ppool","Taddp","Tdelp","Tsusp","TgetFloor","TswapMod"],
   ["Pspeak TgetFloor and Phold not or","Phold not","Pspeak","Plisten",
    "Pmoderate","Ppool","TgrabFloor","Taddp","Tdelp","Tsusp","TreleaseFloor",
    "TswapMod"],
   ["Pspeak TgetFloor and Phold not or","Phold not","Pspeak","Plisten",
    "Pmoderate","Ppool","TgrabFloor","Taddp","Tdelp","Tsusp","TreleaseFloor",
    "TswapMod"],...] : string list list

- ModelChecker("Pspeak TgetFloor and Phold not or");
val it = true : bool

This formula holds on the first state so it is valid. Here is another example:
EU(Pspeak,Pwait) and Phold

- EvaluateFormula("Pspeak Pwait eu Phold and");
val it =
  [["Pmutex","Plisten","Pmoderate","Ppool","Taddp","Tdelp","Tsusp","TgetFloor",
    "TswapMod"],
   ["Pspeak","Plisten","Pmoderate","Ppool","TgrabFloor","Taddp","Tdelp",
    "Tsusp","TreleaseFloor","TswapMod"],
   ["Pspeak","Pwait","Pmoderate","Ppool","TgrabFloor","Taddp","Tresp",
    "TreleaseFloor"],
   ["Pmutex","Plisten","Pwait","Pmoderate","Ppool","Taddp","Tdelp","Tsusp",
    "Tresp","TgetFloor","TswapMod"],
   ["Pmutex","Pwait","Pmoderate","Ppool","Taddp","Tresp"],
   ["Pmutex","Plisten","Pwait","Pmoderate","Ppool","Taddp","Tdelp","Tsusp",
    "Tresp","TgetFloor","TswapMod"],
   ["Pspeak","Pwait","Pmoderate","Ppool","TgrabFloor","Taddp","Tresp",
    "TreleaseFloor"],
   ["Pspeak","Plisten","Pwait","Pmoderate","Ppool","TgrabFloor","Taddp",
    "Tdelp","Tsusp","Tresp","TreleaseFloor","TswapMod"],
   ["Pmutex","Plisten","Pwait","Pmoderate","Ppool","Taddp","Tdelp","Tsusp",
    "Tresp","TgetFloor","TswapMod"],
   ["Pmutex","Plisten","Pmoderate","Ppool","Taddp","Tdelp","Tsusp","TgetFloor",
    "TswapMod"],
   ["Pspeak","Plisten","Pmoderate","Ppool","TgrabFloor","Taddp","Tdelp",
    "Tsusp","TreleaseFloor","TswapMod"],
   ["Pspeak","Plisten","Pmoderate","Ppool","TgrabFloor","Taddp","Tdelp",
    "Tsusp","TreleaseFloor","TswapMod"],...] : string list list

- ModelChecker("Pspeak Pwait eu Phold and");
val it = false : bool

And finally, a much more complicated example:
AU((!Pmoderate or Ppool), Taddp) -> (Pspeak or TgetFloor)

- EvaluateFormula("Pmoderate not Ppool or Taddp au Pspeak TgetFloor or ->");
val it =
  [["Pmoderate not Ppool or Taddp au Pspeak TgetFloor or ->",
    "Pspeak TgetFloor or","Pmoderate not Ppool or Taddp au",
    "Pmoderate not Ppool or","Pmutex","Plisten","Pmoderate","Ppool","Taddp",
    "Tdelp","Tsusp","TgetFloor",...],
   ["Pmoderate not Ppool or Taddp au Pspeak TgetFloor or ->",
    "Pspeak TgetFloor or","Pmoderate not Ppool or","Pspeak","Plisten",
    "Pmoderate","Ppool","TgrabFloor","Taddp","Tdelp","Tsusp","TreleaseFloor",
    ...],
   ["Pmoderate not Ppool or Taddp au Pspeak TgetFloor or ->",
    "Pspeak TgetFloor or","Pmoderate not Ppool or","Pspeak","Pwait",
    "Pmoderate","Ppool","TgrabFloor","Taddp","Tresp","TreleaseFloor"],
   ["Pmoderate not Ppool or Taddp au Pspeak TgetFloor or ->",
    "Pspeak TgetFloor or","Pmoderate not Ppool or","Pmutex","Plisten","Pwait",
    "Pmoderate","Ppool","Taddp","Tdelp","Tsusp","Tresp",...],
   ["Pmoderate not Ppool or Taddp au Pspeak TgetFloor or ->",
    "Pmoderate not Ppool or","Pmutex","Pwait","Pmoderate","Ppool","Taddp",
    "Tresp"],
   ["Pmoderate not Ppool or Taddp au Pspeak TgetFloor or ->",
    "Pspeak TgetFloor or","Pmoderate not Ppool or","Pmutex","Plisten","Pwait",
    "Pmoderate","Ppool","Taddp","Tdelp","Tsusp","Tresp",...],
   ["Pmoderate not Ppool or Taddp au Pspeak TgetFloor or ->",
    "Pspeak TgetFloor or","Pmoderate not Ppool or","Pspeak","Pwait",
    "Pmoderate","Ppool","TgrabFloor","Taddp","Tresp","TreleaseFloor"],
   ["Pmoderate not Ppool or Taddp au Pspeak TgetFloor or ->",
    "Pspeak TgetFloor or","Pmoderate not Ppool or","Pspeak","Plisten","Pwait",
    "Pmoderate","Ppool","TgrabFloor","Taddp","Tdelp","Tsusp",...],
   ["Pmoderate not Ppool or Taddp au Pspeak TgetFloor or ->",
    "Pspeak TgetFloor or","Pmoderate not Ppool or","Pmutex","Plisten","Pwait",
    "Pmoderate","Ppool","Taddp","Tdelp","Tsusp","Tresp",...],
   ["Pmoderate not Ppool or Taddp au Pspeak TgetFloor or ->",
    "Pspeak TgetFloor or","Pmoderate not Ppool or","Pmutex","Plisten",
    "Pmoderate","Ppool","Taddp","Tdelp","Tsusp","TgetFloor","TswapMod"],
   ["Pmoderate not Ppool or Taddp au Pspeak TgetFloor or ->",
    "Pspeak TgetFloor or","Pmoderate not Ppool or","Pspeak","Plisten",
    "Pmoderate","Ppool","TgrabFloor","Taddp","Tdelp","Tsusp","TreleaseFloor",
    ...],
   ["Pmoderate not Ppool or Taddp au Pspeak TgetFloor or ->",
    "Pspeak TgetFloor or","Pmoderate not Ppool or","Pspeak","Plisten",
    "Pmoderate","Ppool","TgrabFloor","Taddp","Tdelp","Tsusp","TreleaseFloor",
    ...],...] : string list list

- ModelChecker("Pmoderate not Ppool or Taddp au Pspeak TgetFloor or ->");
val it = true : bool

The three required test cases are as follows (in the required postfix format):
• "Pspeak TgetFloor and ef" ==> FALSE
• "Pspeak TgetFloor not -> ag TgetFloor Pspeak not -> ag and" ==> TRUE
• "Pmoderate not Phold -> ag" ==> TRUE
• "Phold Phold not af ax -> ag" ==> FALSE

The checker has problems with some (or parts) of these:

- EvaluateFormula("Pspeak TgetFloor and");
val it =
  [["Pmutex","Plisten","Pmoderate","Ppool","Taddp","Tdelp","Tsusp","TgetFloor",
    "TswapMod"],
   ["Pspeak","Plisten","Pmoderate","Ppool","TgrabFloor","Taddp","Tdelp",
    "Tsusp","TreleaseFloor","TswapMod"],
   ["Pspeak","Pwait","Pmoderate","Ppool","TgrabFloor","Taddp","Tresp",
    "TreleaseFloor"],
   ["Pmutex","Plisten","Pwait","Pmoderate","Ppool","Taddp","Tdelp","Tsusp",
    "Tresp","TgetFloor","TswapMod"],
   ["Pmutex","Pwait","Pmoderate","Ppool","Taddp","Tresp"],
   ["Pmutex","Plisten","Pwait","Pmoderate","Ppool","Taddp","Tdelp","Tsusp",
    "Tresp","TgetFloor","TswapMod"],
   ["Pspeak","Pwait","Pmoderate","Ppool","TgrabFloor","Taddp","Tresp",
    "TreleaseFloor"],
   ["Pspeak","Plisten","Pwait","Pmoderate","Ppool","TgrabFloor","Taddp",
    "Tdelp","Tsusp","Tresp","TreleaseFloor","TswapMod"],
   ["Pmutex","Plisten","Pwait","Pmoderate","Ppool","Taddp","Tdelp","Tsusp",
    "Tresp","TgetFloor","TswapMod"],
   ["Pmutex","Plisten","Pmoderate","Ppool","Taddp","Tdelp","Tsusp","TgetFloor",
    "TswapMod"],
   ["Pspeak","Plisten","Pmoderate","Ppool","TgrabFloor","Taddp","Tdelp",
    "Tsusp","TreleaseFloor","TswapMod"],
   ["Pspeak","Plisten","Pmoderate","Ppool","TgrabFloor","Taddp","Tdelp",
    "Tsusp","TreleaseFloor","TswapMod"],...] : string list list

The full formula "freezes" for some reason (with the ef), but I can do the following properly:

- EvaluateFormula("Pspeak ef");
val it =
  [["Pspeak ef","Pmutex","Plisten","Pmoderate","Ppool","Taddp","Tdelp","Tsusp",
    "TgetFloor","TswapMod"],
   ["Pspeak","Plisten","Pmoderate","Ppool","TgrabFloor","Taddp","Tdelp",
    "Tsusp","TreleaseFloor","TswapMod"],
   ["Pspeak","Pwait","Pmoderate","Ppool","TgrabFloor","Taddp","Tresp",
    "TreleaseFloor"],
   ["Pmutex","Plisten","Pwait","Pmoderate","Ppool","Taddp","Tdelp","Tsusp",
    "Tresp","TgetFloor","TswapMod"],
   ["Pmutex","Pwait","Pmoderate","Ppool","Taddp","Tresp"],
   ["Pmutex","Plisten","Pwait","Pmoderate","Ppool","Taddp","Tdelp","Tsusp",
    "Tresp","TgetFloor","TswapMod"],
   ["Pspeak","Pwait","Pmoderate","Ppool","TgrabFloor","Taddp","Tresp",
    "TreleaseFloor"],
   ["Pspeak","Plisten","Pwait","Pmoderate","Ppool","TgrabFloor","Taddp",
    "Tdelp","Tsusp","Tresp","TreleaseFloor","TswapMod"],
   ["Pmutex","Plisten","Pwait","Pmoderate","Ppool","Taddp","Tdelp","Tsusp",
    "Tresp","TgetFloor","TswapMod"],
   ["Pmutex","Plisten","Pmoderate","Ppool","Taddp","Tdelp","Tsusp","TgetFloor",
    "TswapMod"],
   ["Pspeak","Plisten","Pmoderate","Ppool","TgrabFloor","Taddp","Tdelp",
    "Tsusp","TreleaseFloor","TswapMod"],
   ["Pspeak","Plisten","Pmoderate","Ppool","TgrabFloor","Taddp","Tdelp",
    "Tsusp","TreleaseFloor","TswapMod"],...] : string list list

This doesn't cause any problems, but the addition of ag does:

- EvaluateFormula("Pmoderate not Phold ->");
val it =
  [["Pmoderate not Phold ->","Pmutex","Plisten","Pmoderate","Ppool","Taddp",
    "Tdelp","Tsusp","TgetFloor","TswapMod"],
   ["Pmoderate not Phold ->","Pspeak","Plisten","Pmoderate","Ppool",
    "TgrabFloor","Taddp","Tdelp","Tsusp","TreleaseFloor","TswapMod"],
   ["Pmoderate not Phold ->","Pspeak","Pwait","Pmoderate","Ppool","TgrabFloor",
    "Taddp","Tresp","TreleaseFloor"],
   ["Pmoderate not Phold ->","Pmutex","Plisten","Pwait","Pmoderate","Ppool",
    "Taddp","Tdelp","Tsusp","Tresp","TgetFloor","TswapMod"],
   ["Pmoderate not Phold ->","Pmutex","Pwait","Pmoderate","Ppool","Taddp",
    "Tresp"],
   ["Pmoderate not Phold ->","Pmutex","Plisten","Pwait","Pmoderate","Ppool",
    "Taddp","Tdelp","Tsusp","Tresp","TgetFloor","TswapMod"],
   ["Pmoderate not Phold ->","Pspeak","Pwait","Pmoderate","Ppool","TgrabFloor",
    "Taddp","Tresp","TreleaseFloor"],
   ["Pmoderate not Phold ->","Pspeak","Plisten","Pwait","Pmoderate","Ppool",
    "TgrabFloor","Taddp","Tdelp","Tsusp","Tresp","TreleaseFloor",...],
   ["Pmoderate not Phold ->","Pmutex","Plisten","Pwait","Pmoderate","Ppool",
    "Taddp","Tdelp","Tsusp","Tresp","TgetFloor","TswapMod"],
   ["Pmoderate not Phold ->","Pmutex","Plisten","Pmoderate","Ppool","Taddp",
    "Tdelp","Tsusp","TgetFloor","TswapMod"],
   ["Pmoderate not Phold ->","Pspeak","Plisten","Pmoderate","Ppool",
    "TgrabFloor","Taddp","Tdelp","Tsusp","TreleaseFloor","TswapMod"],
   ["Pmoderate not Phold ->","Pspeak","Plisten","Pmoderate","Ppool",
    "TgrabFloor","Taddp","Tdelp","Tsusp","TreleaseFloor","TswapMod"],...]
  : string list list

I had problems with ag and ef in the test cases, even though both operations work with atomic predicates as parameters.