CIS 301. Logical Foundations of Programming, Spring 2001

Below you find an incomplete SMV program. The incomplete parts are indicated by a "???".

• You are asked to complete this program (worth six points without the SPEC part) based on a description of the system it means to model:

  We have three lamps, lamp₁, lamp₂, and lamp₃, which we model as boolean variables. Any lamp has value "0" if it is "off"; it has value "1" if it is "on". The system may start off at any initial state. At any state, the next state is determined as follows: for any of the three lamps, lamp_k (where k=1,2,3):

  • if the two other lamps are on, then lamp_k gets turned off in the next state;
  • if the two other lamps are off, then lamp_k gets turned on in the next state;
  • otherwise, lamp_k takes on the current value of some other lamp as specified below:
    • the next state of lamp₁ is the current state of lamp₂;
    • the next state of lamp₂ is the current state of lamp₃;
    • the next state of lamp₃ is the current state of lamp₁.

  MODULE main
          VAR
                  lamp1 : boolean;
  		lamp2 : boolean;
  		lamp3 : boolean;
  
          ASSIGN
                  init(lamp1) := ???;
                  init(lamp2) := ???;
                  init(lamp3) := ???;
  
  		next(lamp1) :=
                    case
  		    ( ??? )           : ???;
  		    ( ??? )           : ???;
  		    1                 : ???;
  		  esac;
  
  		next(lamp2) :=
                    case
  		    ( ??? )           : ???;
  		    ( ??? )           : ???;
  		    1                 : ???;
  		  esac;
  
  		next(lamp3) :=
                    case
  		    ( ??? )           : ???;
  		    ( ??? )           : ???;
  		    1                 : ???;
  		  esac;
  
  SPEC ???
  SPEC ???
  SPEC ???
  SPEC ???
  

• Substitute CTL formulas for the "???" in the SPEC part of your program, where the four properties (worth one point each) are
  • For all paths, lamp₁ is eventually on.
  • It is not the case that there is a path on which, eventually, there is a state where all lamps are on.
  • At any state, if lamp₁ is on, then it will, eventually, be off again.
  • There is a path such that all of its states have a path that eventually reaches a state, where all lamps are on.

Thus, you can earn a total of ten points for completing this homework.