CIS 301. Logical Foundations of Programming, Fall 2000

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) := {0, 1};
                init(lamp2) := {0, 1};
                init(lamp3) := {0, 1};

		next(lamp1) :=
                  case
		    ( lamp2 &  lamp3) : 0;
		    (!lamp2 & !lamp3) : 1;
		    1                 : lamp2;
		  esac;

		next(lamp2) :=
                  case
		    ( lamp1 &  lamp3) : 0;
		    (!lamp1 & !lamp3) : 1;
		    1                 : lamp3;
		  esac;

		next(lamp3) :=
                  case
		    ( lamp1 &  lamp2) : 0;
		    (!lamp1 & !lamp2) : 1;
		    1                 : lamp1;
		  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.

SPEC AF (lamp1)
SPEC !EF (lamp1 & lamp2 & lamp3)
SPEC AG( lamp1 -> AF (!lamp1))
SPEC EG( EF (lamp1 & lamp2 & lamp3))

Let's execute that program:

nunk% smv sol10.smv
-- specification AF lamp1 is true
-- specification !EF (lamp1 & lamp2 & lamp3) is false
-- as demonstrated by the following execution sequence
state 1.1:
lamp1 = 0
lamp2 = 0
lamp3 = 0

state 1.2:
lamp1 = 1
lamp2 = 1
lamp3 = 1

-- specification AG (lamp1 -> AF (!lamp1)) is true
-- specification EG EF (lamp1 & lamp2 & lamp3) is false
-- as demonstrated by the following execution sequence
state 2.1:
lamp1 = 0
lamp2 = 0
lamp3 = 1


resources used:
user time: 0.03 s, system time: 0.02 s
BDD nodes allocated: 290
Bytes allocated: 1245184
BDD nodes representing transition relation: 23 + 1

Comments on the generated counter examples:

• The first counter example is not a minimal one, since the system could have began in the state "111".
• The counter example for the last property does not make any sense. This is because meaningful counter examples can only be generated for a certain fragment of CTL (that includes all safety properties) and the last property is not expressible in that fragment. At least, we know that the property doesn't hold, although we may have a hard time understanding why. :-(