##### Differences

This shows you the differences between two versions of the page.

 — cs-486:homework-3-2016 [2017/01/11 11:45] (current)egm created 2017/01/11 11:45 egm created 2017/01/11 11:45 egm created Line 1: Line 1: + Objectives: + * Master on-the-fly LTL model checking + == Reading == + Chapter 9 of the course text. + + == Paper Pencil Problems == + Consider the below solution to the dining philosopher for just two participants. Each active thread describes the state of the philosopher. Both start in the the first location, ''​loc0''​. For example, in the first location of ''​Philosopher1'',​ when ''​fork1''​ is available, then ''​Philosopher1''​ sets ''​fork1''​ to ''​true''​ and jumps to ''​loc1''​ (''​goto loc1''​). ​ The description details a transition system from which it is possible to derive a Kripke structure. + + + system TwoDiningPhilosophers { + boolean fork1 = false; + boolean fork2 = false; + + active thread Philosopher1() { + loc loc0:  // take first fork + when !fork1 do  { + fork1 := true; + } + goto loc1; + + loc loc1:  // take second fork + when !fork2 do { + fork2 := true; + } + goto loc2; + ​ + when fork2 do { + fork1 := false;  ​ + } + goto loc0; + + loc loc2:  // drop second fork + when true do { + fork2 := false; ​ + } + goto loc3; + + loc loc3:  // drop first fork + when true do { + fork1 := false; ​ + } + goto loc0; + } + + active thread Philosopher2() { + loc loc0:  // take second fork + when !fork2 do { + fork2 := true; + } + goto loc1; + + loc loc1:  // take first fork + when !fork1 do { + fork1 := true; } + goto loc2; + ​ + when fork1 do { + fork2 := false; ​ + } + goto loc0; + + loc loc2: // drop first fork + when true do { + fork1 := false; ​ + } + goto loc3; + + loc loc3:  // drop put second fork + when true do { + fork2 := false; ​ + } + goto loc0; + } + + ​ + + Consider the following property description for the dining philosophers. + + + // Liveness Property: + // + // ​ If a philosopher picks up a fork, he will eventually release it + // ​ (this can be done for fork 1 or 2) + // + // LTL: + // ​ + // ​   f = [] (fork1/2 --> <> !fork1/2) + ​ + + # '''​(3 points)'''​ Write the complement of the property so it is expressed as a '''​never'''​-claim. + # '''​(5 points)'''​ Create the Buechi Automaton for the never-claim in the previous problem. Express the automaton in either a dotty format or the text format used to describe the dinning philosopher protocol above (i.e., locations with guarded or unguarded commands). Please label accept locations as ''​loc'''​X''':​accept''​ where '''​X'''​ is a number. For example, ''​loc1:​accept''​. + # '''​(15 points)'''​ Perform on-the-fly model checking to see if our system satisfies the property (i.e., check the intersection of the model and the never claim). Please show the entire search graph as we did in class.When doing to the intersection,​ treat each location as as single atomic step.