MODULE main

VAR
  Tmr1 : 1..5;
  Tmr2 : 1..4;
  Tmr3 : 1..6;
  Tmr4 : 1..3;

  Sw1  : { On, Off };
  Sw2  : { On, Off };
  Sw3  : { On, Off };
  Sw4  : { On, Off };

ASSIGN
  init(Tmr1) := 2;
  init(Tmr2) := 3;
  init(Tmr3) := 1;
  init(Tmr4) := 2;

  init(Sw1)  := Off;
  init(Sw2)  := Off;
  init(Sw3)  := Off;
  init(Sw4)  := Off;

  next(Tmr1) := case
                    Tmr1 < 5 : Tmr1 + 1;
                    TRUE     : 1;
                esac;

  next(Tmr2) := case
                    Tmr2 < 4 : Tmr2 + 1;
                    TRUE     : 1;
                esac;

  next(Tmr3) := case
                    Tmr3 < 6 : Tmr3 + 1;
                    TRUE     : 1;
                esac;

  next(Tmr4) := case
                    Tmr4 < 3 : Tmr4 + 1;
                    TRUE     : 1;
                esac;

  next(Sw1)  := case
                    Tmr1 = 5 : On;
                    TRUE     : Off;
                esac;

  next(Sw2)  := case
                    Tmr2 = 4 : On;
                    TRUE     : Off;
                esac;

  next(Sw3)  := case
                    Tmr3 = 6 : On;
                    TRUE     : Off;
                esac;

  next(Sw4)  := case
                    Tmr4 = 3 : On;
                    TRUE     : Off;
                esac;


SPEC  AF ( Sw1 = On & Sw2 = On & ( Sw3 = On | Sw4 = On) )
SPEC  AF ( Sw1 = On & Sw2 = On &  Sw3 = On & Sw4 = On )