% Tick axiom
local tick: bool 

macro ticking = ~tick /\ []<>tick

% Controller variables
local Tc, Ic, Bc: bool 

% Plant variables
local T, I, B: bool 

%%% Plant description

% Plant variables cannot change spontaneously. They change only when
% the control variables change.
macro p1: bool where p1 =
   Tc /\ (T <--> Tc) /\ ()Tc ==> ()(T <--> Tc)
macro p2: bool where p2 =
   ~Tc /\ (T <--> Tc) /\ ()~Tc ==> ()(T <--> Tc)
macro p3: bool where p3 =
   Ic /\ (I <--> Ic) /\ ()Ic ==> ()(I <--> Ic)
macro p4: bool where p4 =
   ~Ic /\ (I <--> Ic) /\ ()~Ic ==> ()(I <--> Ic)
macro p5: bool where p5 =
   Bc /\ (B <--> Bc) /\ ()Bc ==> ()(B <--> Bc)
macro p6: bool where p6 =
   ~Bc /\ (B <--> Bc) /\ ()~Bc ==> ()(B <--> Bc)

% If the control variables change, then the plant responds before the
% next tick.
macro p7: bool where p7 =
   (~(T <--> Tc)) ==> ( ~tick Until (T <--> Tc))
macro p8: bool where p8 =
   (~(I <--> Ic)) ==> ( ~tick Until (I <--> Ic))
macro p9: bool where p9 =
   (~(B <--> Bc)) ==> ( ~tick Until (B <--> Bc))

%%% Controller description

% Maintain appropriate control variables
macro c1: bool where c1 =
   Bc ==> (~Ic /\ ~Tc) \/ (I /\ T)

% Only turn beam on if appropriate adjustments were made one tick
% earlier

macro cA  = (Bc /\ ~Ic /\ ~Tc)
macro cB1 = (~Ic /\ ~Tc)
macro cB2 = (Ic /\  Tc)

(*
macro c2 = (!cA Awaits tick) /\ (!tick ==> cB1 Awaits !cA)
macro c3 = (!cA Awaits tick) /\ (!tick ==> cB2 Awaits !cA)
*)
macro c2: bool where c2 =
   (Bc /\ ~Ic /\ ~Tc) ==> (~Ic /\ ~Tc) Since tick
macro c3: bool where c3 =
   (Bc /\  Ic /\  Tc) ==> ( Ic /\  Tc) Since tick

%%% Initial condition
macro init: bool where init =
   (~Ic /\ ~Tc) \/ (I /\ T)
%%% Requirements %%%
macro r = B ==> (I <--> T);
      init
   /\ ticking
   /\ p1 /\ p2 /\ p3 /\ p4 /\ p5 /\ p6 /\ p7 /\ p8 /\ p9
   /\ c1 /\ c2 /\ c3
-->   r