Model Checking 2

Do the following things:

• Model the dining philosophers problem with a classical Pnet (black tokens only, no priorities on the arcs, no inhibitor arcs, no debit arcs, no colors, no extensions). Create a 3 philosopher model, and you may use the one shown in the Pnet powerpoint slides as a guide.


• Convert the Pnet model into an annotated finite state machine so that we can analyze it with the mcb model checker. Use this input format. Use my interpretation of the state space... make atomic facts for each place ("Pname1", "Pname2", etc.) and make atomic facts for each transition ("Tname1", "Tname2", etc.). If a place is marked in some state mark its fact as a 1 in the bitvector for that state; if a transition is enabled, mark its fact a 1 in the bit vector for that state.
  
  For making the state machine from the net, remember that the state of a net is a vector of integers showing how many tokens are in each place. Make that vector for the start state and then note which transitions are enabled to fire... these are arcs to next states. Fire one, note the new net state vector... that is a state in the FSM. Etc.


• Write CTL formulae to express the following properties. Run the model checker on them and show what it says about the truth of the property: the following:

  
  (a) There can never be two philosopher eating at the same time.
  
  (b) It is possible to for only one philosopher to be thinking
  
  (c) It is impossible that any philosopher is starved... i.e.,
      fails to get two forks to eat.
  
  (d) There is no chance that once a philosopher gets the forks
      it eats forever and never gives up the forks
  
  (e) It is impossible for all philosophers to always think 
      and never eat
  
  
  

Links to the mcb executable, what the FSM text file format looks like, etc. are here in A7.