Pnet for moderated meeting | FSM model | CTL formulae |
getModel.ml |
Check your program against Clarke's original |
Turn in your work via the Web. Make an area that I can read and put all the code and supporting documentation in it Make sure your directory has a "README.txt" file explaining what is there and how to use it.
You may use the assignment data area as an example.
Here is a version of
"getModel.ml" for the later ML version.
Thanks to Chris Vanderknyff for this one.
Pnet for moderated meeting | FSM model | CTL formulae |
I have converted the Petri Net into an annotated FSM for model checking analysis, also available above at the "FSM" link.
Finally, you must run your model checker on the model to check the temporal formulae found at the "CTL" link above.
Note the information below about what input notation
you MUST deal with, and what extensions you may deal with for
extra credit.
Inputs will be:
Example
STATES 8 ARCS 12 ATOMIC welcome, overview, shuttle, engines, allow, inhibit, begin, orbiter, propulsion, begin2, return, remove ; #0 100010100000 1 #1 010010011000 2 6 #2 010101000011 3 4 #3 000110000010 0 #4 110001100001 0 5 #5 010001000001 1 #6 011001000101 7 4 #7 001010000100 0 #END
* ~p * p1 & p2 p1 | p2 abbrev for ~(~p1 & ~p2) p1 -> p2 abbrev for ~p1 | p2 * AXp * EXp * AU(p1,p2) this is notation for A [ p1 U p2 ] * EU(p1,p2) this is notation for E [ p1 U p2 ] AFp abbrev for A [ true U p ] EFp abbrev for E [ true U p ], or EU(true,p) AGp abbrev for ~EF(~p) EGp abbrev for ~AF(~p)
The REQUIRED functionality is to accept and check the reduced notation (the "*" operators above). You may assume that all CTL formulae have been translated into these operators by the user.
You may wish to make your implementation deal with the full CTL notation as input, and do the reduction/translation in the checker... it's your choice.
As examples of rewriting, consider:
EF(p1) -> AG(p2)can be re-written as
~EF(p1) | AG(p2) ~EU(true,p1) | ~EF(~p2) ~EU(true,p1) | ~EU(true,~p2) ~(EU(true,p1) & EU(true,~p2))This uses only the ~, &, EU operators
The algorithm operates in stages:
Other primitives:
proc label_graph (f) is (* handles 7 cases depending on whether f is atomic or has one of these forms: ~f, f1 and f2, AXf, EXf, A[f1 U f2], E[f1 U f2] *) ... (* case where operator is AU *) { for all s in S { marked(s) := false } L: for all s in S { if ~marked(s) au(f,s,b) } } ... endproc proc au (f,s,b) is if marked(s) { b := labeled(s,f); return } marked(s) := true ; if labeled(s,arg2(f)) { add_label(s,f) ; b := true ; return ; } elsif ~labeled(s,arg1(f)) { b := false ; return ; } for all s1 in successors(s) { au(f,s1,b1) ; if ~b1 { b := false; return } } add_label(s,f); b := true; return ; endproc