Kind2/Lustre examples for the Week 6 quiz on the course Formal Software Verification.

Beams.lus

-- I am building a cancer treatment machine. The machine can emit two types of
-- beams; for simplicity let’s just call them A and B. There are two different
-- plates that can be placed in front of the beam; let’s call them 1 and 2. When
-- you turn the machine on it always starts ups with beam set to A and plate set
-- to 1. That is the initial state.

-- For safety reasons we never want the machine to be at beam B and plate 2.
-- If this every happens a deadline dose of radiation will be emitted and it
-- will kill the patient.
-- But all of the other combinations of beams and plates are valid.
--
-- Method setBeam(str beamType)
-- If beamType = B and plate = 1
-- Set beam = B
-- Else Set beam = A
--
-- Method setPlate(int plateType)
-- If plateType = 2 and beam = A
-- Set plate = 2
-- Else Set plate = 1

type plate_t = subrange [1, 2] of int;
type beam_t = enum { A, B };

node setBeam(beam: beam_t; p: plate_t; set_beam: bool) returns (b: beam_t);
let
  b = A ->
    if set_beam then
      if beam = B and pre p = 1 then B else A
    else
      pre b;
tel

node setPlate(plate: plate_t; b: beam_t; set_plate: bool) returns (p: plate_t);
let
  p = 1 ->
    if set_plate then
      if plate = 2 and pre b = A then 2 else 1
    else
      pre p;
tel

node top (plate: plate_t; beam: beam_t; set_beam: bool)
  returns (p: plate_t; b: beam_t);
let
  b = setBeam(beam, p, set_beam);
  p = setPlate(plate, b, not set_beam);

  --%MAIN;

  --%PROPERTY not (b = B and p = 2);
tel

Microwave.lus

-- 4.  In the material used for this topic, there is an example of a Microwave.
-- Below is the code. To refresh your memory, we never want to get to a state
-- where the door is open and the heat is on. The developer claims to have fixed
-- the defect discovered by the model checking. His fix is reflected in the code
-- below. Perform modeling checking on the code again.

type action_t = enum { OpenDoor, CloseDoor, TurnHeatOn, TurnHeatOff };
type door_t = enum { Opened, Closed };
type heat_t = enum { On, Off };

node makeAction(cur_door: door_t; cur_heat: heat_t; action: action_t)
  returns (new_door: door_t; new_heat: heat_t);
let
  (new_door, new_heat) =
    if action = OpenDoor then
      if not (cur_door = Opened) then
        -- to fix the model:
        -- - comment out "(Opened, cur_heat)"
        -- - uncomment the following if..else:
        (Opened, cur_heat)

        -- the fix:
        -- if cur_heat = On then
        --  (Opened, Off)
        -- else
        -- (Opened, cur_heat)

      else
        (cur_door, cur_heat)

    else if action = CloseDoor then
      if cur_door = Opened then
        (Closed, cur_heat)
      else
        (cur_door, cur_heat)

    else if action = TurnHeatOn then
      if (not (cur_heat = On)) and (not (cur_door = Opened)) then
        (cur_door, On)
      else
        (cur_door, cur_heat)

    else if action = TurnHeatOff then
      if cur_heat = On then
        (cur_door, Off)
      else
        (cur_door, cur_heat)

    else
      (cur_door, cur_heat);
tel

node top (action: action_t) returns ()
var cur_door: door_t;
var cur_heat: heat_t;
var pre_door: door_t;
var pre_heat: heat_t;
let
  (pre_door, pre_heat) = (Closed, Off) -> (pre cur_door, pre cur_heat);
  (cur_door, cur_heat) = makeAction(pre_door, pre_heat, action);

  --%MAIN;
  --%PROPERTY not (cur_door = Opened and cur_heat = On);
tel