COMP 204 Programming Assignment 1 Report

Adrian Ilie

Links

- model checker source code: adyilie.ml

- sample output text file: output.txt

- translated formulas file: mymeet.ctl

To run the model checker in sml, use the following sequence of commands:

use("adyilie.ml");

main("meet.fsm","mymeet.ctl");

The model checker main function takes as inputs the names of two files: the model file and a file containing the formulas to be evaluated, separated by semicolons.

To evaluate single formulas (in the format described below), use the following commands, where <formula> can be any valid string formula:

val model = createModel("meet.fsm");

evaluateStringFormula("<formula>",model);

Program Description

I modified the model reader from "getModel.ml", to make it build a model that better suited my needs.

The model I used was a tuple in the following format:

string list * *(*list of all atomic predicate names*)*

int list * *(*list of all state numbers*)*

(int * int list) list * *(*list of arcs to next states for a state*)*

(int * int list) list * *(*list of true atomic predicates for a state*)*

(int * int list) list *(*list of true subformulas indexes for a state*)*

I preferred having the state number in each list because it made manipulating the model easier. Also, instead of Boolean values for the list of true atomic predicates in each state I used a list of indexes in the atomic predicates list. Also, to each state, a new "atomic predicate" is added to the list, the predicate "true", which is true in all states.

The formula parser builds a tree approximately as the one described in Clarke's paper. A node in the tree has the following structure:

int * *(*subformula index*)*

string * *(*operator name*)*

(int * int) *(* list of indexes of the two operands as subformulas in the same tree*)*

If the operator is unary, then the second operand's index is –1.

If the subformula is an atomic predicate, the operator name is a null string, the first operand's index is the atomic predicate's index in the atomic predicates list and the second operand's index is –1.

For the program to process a formula, it has to be written in terms of the following operators: NOT, AX, EX, OR, AND, AU and EU. This is the complete set of operators according to Clarke's paper, to which I added OR (the easiest to implement).

The process of evaluating a formula consists in the following phases:

- empty the labels list for all states;
- evaluate the subformulas in the tree built by the parser – in reverse order, so atomic predicates get evaluated first – each subformula is evaluated in all states;
- the result is true if the outermost subformula (index=1) is true (its index is a member of the true subformulas list of a state) after the evaluation process.

Results

The results of evaluating the requested formulas were as follows:

1) Can more than one person be speaking at one time? Can a listener ever get the floor when someone is already speaking?

1a. EF (Pspeak & TgetFloor) (expect "FALSE")

Translated for the formula parser, this formula becomes:

(EF(AND Pspeak TgetFloor)) =

= (EU true (AND Pspeak TgetFloor))

The output of the program is:

(EUtrue(ANDPspeakTgetFloor)) : false

1b. AG (Pspeak -> ~TgetFloor) & AG (TgetFloor -> ~Pspeak) (expect "TRUE")

Translated for the formula parser, this formula becomes the negation of the first one:

AND(AG(OR (~Pspeak) (~TgetFloor)) AG(OR (~TgetFloor) (~Pspeak))) =

= AND(AG(OR (~Pspeak) (~TgetFloor)) AG(OR (~Pspeak) (~TgetFloor))) =

= AG(OR (~Pspeak) (~TgetFloor)) =

= (~EF(~(OR (~Pspeak) (~TgetFloor)))) =

= (~(EU true (~(OR (~Pspeak) (~TgetFloor))))) =

= (~(EU true (AND Pspeak TgetFloor))) =

= (~1a)

The output of the program is:

(~(EUtrue(ANDPspeakTgetFloor))) : true

2) The meeting is always moderated, except when someone is on hold.

2. AG (~Pmoderate -> Phold) (expect "TRUE")

Translated for the formula parser, this formula becomes:

AG (~Pmoderate -> Phold) =

= AG(OR Pmoderate Phold) =

= (~(EU true (~(OR Pmoderate Phold))))

The output of the program is:

(~(EUtrue(~(ORPmoderatePhold)))) : true

3) Is it possible for a speaker to get "stuck" on hold?

3. AG (Phold -> AX(AF(~Phold))) (expect "FALSE")

Translated for the formula parser, this formula becomes:

AG (Phold -> AX(AF(~Phold))) =

= AG(OR (~Phold) AX(AU true (~Phold))) =

= (~EF(~(OR (~Phold) AX(AU true (~Phold))))) =

= (~(EU true (~(OR (~Phold) (AX (AU true (~Phold)))))))

The output of the program is:

(~(EUtrue(~(OR(~Phold)(AX(AUtrue(~Phold))))))) : false

The floor control operations are critical, and some of them should be mutually exclusive. The following two formulas test if that requirement is met by our model.

4) Can the floor be grabbed and dropped simultaneously?

4. EF (TgrabFloor & TdropFloor) (expect "FALSE")

Translated for the formula parser, this formula becomes:

EF (AND (TgrabFloor TdropFloor)) =

= (EU true(AND TgrabFloor TdropFloor))

The output of the program is:

(EUtrue(ANDTgrabFloorTdropFloor)) : false

5) Can the floor be gotten and released simultaneously?

5. EF (TgetFloor & TreleaseFloor) (expect "FALSE")

Translated for the formula parser, this formula becomes:

EF (AND (TgetFloor TreleaseFloor)) =

= (EU true(AND TgrabFloor TreleaseFloor))

The output of the program is:

(EUtrue(ANDTreleaseFloorTgetFloor)) : false

In a conference protocol, participants should be able to enter and leave freely. This translates into the following formula:

6) Can participants be added and removed from the pool at any time?

6. EF (Taddp & Tdelp) (expect "TRUE")

Translated for the formula parser, this formula becomes:

EF (AND (Taddp Tdelp)) =

= (EU true(AND Taddp Tdelp))

The output of the program is:

(EUtrue(ANDTaddpTdelp)) : true