progrinit: CONTEXT = 
BEGIN
   prog: TYPE = {a, b, c};
   activity: TYPE = [# xprog: prog, xrel: bool, xres: prog #];
   ctype: TYPE = [0..30];
   action: TYPE = DATATYPE
         tick,
         mu1,
         alpha,
         mu2,
         rho1,
         rho2,
         wr,
         ws,
         pr,
         ps,
	 rhoo,
	 rhoc,
 	 phistart,
	 phistop1,
	 phistop2,
	 phicont           
        END;
      tw: TYPE = [0..32];
      tr: TYPE = [0..20];

      internal_state: TYPE = [# Relay: bool, Power:bool, Pressure:bool, 
                             c1: ctype, c2: ctype, Tr: tr, Tw: tw  #];
      nt_action: TYPE = {ac: action | ac /= tick};
      t1: CONTEXT = timedef;
      cs: CONTEXT = states{activity, nt_action, internal_state, timedef!time;};   
%% state variables
% Auxiliary functions

        lower_bound (ac:nt_action): t1!time =
               IF ac = mu1 THEN  t1!one
               ELSIF ac = alpha THEN  t1!one
               ELSIF ac = mu2 THEN t1!one
               ELSIF ac = rho1 THEN t1!one
               ELSIF ac = rho2 THEN t1!one
               ELSIF ac = wr THEN t1!one
               ELSIF ac = ws THEN t1!one
               ELSIF  ac = pr THEN t1!one
               ELSIF ac = ps THEN  t1!one
	       ELSIF ac = rhoo THEN t1!zero
	       ELSIF ac = rhoc THEN t1!zero
	       ELSIF ac = phistart THEN t1!zero
               ELSIF ac = phistop1 THEN t1!zero
               ELSIF ac = phistop2 THEN t1!zero
               ELSIF ac = phicont THEN t1!zero
               ELSE t1!one
	       ENDIF;
        
        upper_bound (ac:nt_action): t1!time =
	IF ac = mu1 THEN  t1!one
               ELSIF ac = alpha THEN  t1!one
               ELSIF ac = mu2 THEN t1!one
               ELSIF ac = rho1 THEN t1!one
               ELSIF ac = rho2 THEN t1!one
               ELSIF ac = wr THEN t1!infinity
               ELSIF ac = ws THEN t1!infinity
               ELSIF  ac = pr THEN t1!infinity
               ELSIF ac = ps THEN  t1!infinity
	       ELSIF ac = rhoo THEN t1!zero
	       ELSIF ac = rhoc THEN t1!zero
	       ELSIF ac = phistart THEN t1!zero
               ELSIF ac = phistop1 THEN t1!zero
               ELSIF ac = phistop2 THEN t1!zero
               ELSIF ac = phicont THEN t1!zero
               ELSE t1!one
	       ENDIF;
		

% preconditions

    enabled_state (si:cs!states1): bool =
	       IF si.nta = mu1 THEN  (si.is.Pressure AND si.is.Power AND
		   si.is.c1 = 0 AND si.is.c2 = 0) OR
		  (si.is.c1 >= 1 AND si.is.c1 <= 29)
               ELSIF si.nta = alpha THEN si.is.Power AND si.is.c1 >= 30
               ELSIF si.nta = mu2 THEN (si.is.c1 = 0 AND si.is.c2 >= 1
					AND si.is.c2 <= 19)
               ELSIF si.nta = rho1 THEN NOT si.is.Power AND si.is.c1 >= 30
               ELSIF si.nta = rho2 THEN NOT si.is.Power AND si.is.c1 = 0
					AND si.is.c2 >= 20
               ELSIF si.nta = wr THEN si.is.Power
               ELSIF si.nta = ws THEN NOT si.is.Power
               ELSIF  si.nta = pr THEN si.is.Pressure
               ELSIF si.nta = ps THEN NOT si.is.Pressure
	       ELSIF si.nta = rhoo THEN si.is.Relay
               ELSIF si.nta = rhoc THEN NOT  si.is.Relay
               ELSIF si.nta = phistart THEN si.a.xprog = a AND NOT si.is.Relay
                    AND  si.is.c1 = 0 AND si.is.c2 = 0 AND 
                    si.is.Power AND si.is.Pressure
               ELSIF si.nta = phistop1 THEN NOT si.is.Power 
					OR NOT si.is.Pressure
               ELSIF  si.nta = phistop2 THEN NOT si.is.Power
				        AND si.is.Tw <= 2 AND si.is.Tw >= 0
               ELSIF si.nta = phicont THEN si.is.Tw = 30
               ELSE FALSE
	       ENDIF;

    graph(si:cs!states2):bool =                
	       IF si.nta = mu1 THEN  si.a.xprog = a
               ELSIF si.nta = alpha THEN  si.a.xprog = a
               ELSIF si.nta = mu2 THEN si.a.xprog =  a
               ELSIF si.nta = rho1 THEN si.a.xprog = a
               ELSIF si.nta = rho2 THEN si.a.xprog = a
               ELSIF si.nta = wr THEN TRUE
               ELSIF si.nta = ws THEN TRUE
               ELSIF  si.nta = pr THEN TRUE
               ELSIF si.nta = ps THEN TRUE
	       ELSIF si.nta = rhoo THEN NOT si.a.xrel
               ELSIF si.nta = rhoc THEN si.a.xrel
               ELSIF si.nta = phistart THEN si.a.xres = a
               ELSIF si.nta = phistop1 THEN si.a.xres = b
               ELSIF  si.nta = phistop2 THEN si.a.xres = c
               ELSIF si.nta = phicont THEN si.a.xres = b
               ELSE FALSE
	       ENDIF;
		

    t: CONTEXT = ttm{activity, internal_state, nt_action; lower_bound,
		upper_bound, enabled_state, graph};
    enabled(ac:action,s:cs!states): bool =
                IF(not (tick?(ac))) THEN t!enabled_general(ac,s) AND t!enabled_time(ac,s)
                ELSE t!enabled_tick(s)
                ENDIF;
spp: MODULE =
BEGIN
  GLOBAL s: cs!states
INITIALIZATION 
  s = (# activ := (# xprog := a, xrel := FALSE, xres := a  #),
                   basic:= (#  Relay := FALSE, Power := FALSE,
                   Pressure := FALSE , c1:= 0, c2:= 0, Tr := 0, Tw := 0 #),
                   action_time:=(LAMBDA (a:nt_action): t1!zero)#)


TRANSITION
[
      enabled(tick, s) -->  s' =  
	(IF (s.activ.xres = b OR s.activ.xres = c) AND s.basic.Tw > 0 AND 
                   s.activ.xrel AND s.basic.Tr > 0 THEN 
        (((s WITH .basic.Tr := s.basic.Tr - 1) 
        	WITH .basic.Tw := s.basic.Tw - 1)
        	WITH .action_time := t!update_clocks(s))
        ELSIF ((s.activ.xres = b OR s.activ.xres = c) AND s.basic.Tw > 0) THEN 
               ((s WITH .basic.Tw := s.basic.Tw - 1) 
		WITH .action_time := t!update_clocks(s))
	ELSIF (s.activ.xrel AND s.basic.Tr > 0) THEN
	       ((s WITH .basic.Tr := s.basic.Tr - 1) 
		WITH .action_time := t!update_clocks(s))
        ELSE (s WITH .action_time := t!update_clocks(s))
	ENDIF) 
      []
      enabled(mu1, s) --> s' =   ((s WITH .basic.c1:= s.basic.c1 + 1) 
          WITH .action_time:= t!reset_clocks(mu1,
         (s WITH .basic.c1 :=s.basic.c1 + 1))) 
      []
      enabled (alpha, s) --> s' = (((s WITH .basic.c1 :=0)
	  WITH .basic.c2 := s.basic.c2 + 1)
          WITH .basic.Relay := TRUE)  WITH  .action_time:=
          t!reset_clocks(alpha, ((s WITH .basic.c1 := 0) WITH 
          .basic.c2 := s.basic.c2 + 1)
           WITH .basic.Relay:=TRUE)
      []
      enabled(mu2, s) --> s' =  ((s WITH .basic.c2 := s.basic.c2 + 1)
          WITH .basic.Relay := TRUE) WITH 
          .action_time:= t!reset_clocks(mu2,
          (s WITH  .basic.c2 := s.basic.c2 + 1) WITH .basic.Relay := TRUE ) 
      []
      enabled(rho1, s) --> s' = (s WITH .basic.c1 := 0)
        WITH  .action_time := t!reset_clocks(rho1, s WITH .basic.c1 := 0)
      []
      enabled(rho2, s) -->  s' = ((s WITH .basic.c2 := 0)  WITH
       .basic.Relay := FALSE) WITH .action_time:= t!reset_clocks(rho2,
       (s WITH .basic.c2 := 0)  WITH .basic.Relay := FALSE)
      []
      enabled(wr, s) --> s' =  (s WITH .basic.Power:=FALSE) WITH .action_time:= t!reset_clocks(wr,s  WITH .basic.Power:= FALSE)
      []
      enabled(ws, s) --> s' =  (s WITH .basic.Power := TRUE) WITH .action_time:= t!reset_clocks(ws,s  WITH .basic.Power := TRUE)
      []
      enabled(pr, s) --> s' =  (s  WITH .basic.Pressure := FALSE) WITH .action_time:= t!reset_clocks(pr,s WITH .basic.Pressure:=FALSE)
      []
      enabled(ps, s) --> s' =  (s WITH .basic.Pressure := TRUE) WITH .action_time:= t!reset_clocks(ps,s WITH .basic.Pressure := TRUE)
      []
      enabled(rhoo, s) --> s' = (((s WITH .activ.xrel := TRUE) 
        WITH .basic.Tr := 20)
	WITH .action_time:= t!reset_clocks(rhoo,(s WITH .activ.xrel := TRUE)
        WITH .basic.Tr := 20))
      []
      enabled(rhoc, s)  --> s' = (((s WITH .activ.xrel := FALSE) 
        WITH .basic.Tr := 0)
	WITH .action_time:= t!reset_clocks(rhoc,(s WITH .activ.xrel := FALSE)
        WITH .basic.Tr := 0))
      []
       enabled(phistart, s)  --> s' = (((s WITH .activ.xres := b) 
        WITH .basic.Tw := 32)
	WITH .action_time:= t!reset_clocks(phistart,(s WITH .activ.xres := b)
        WITH .basic.Tw := 32))
      []
       enabled(phistop1, s)  --> s' = (((s WITH .activ.xres := a) 
        WITH .basic.Tw := 0)
	WITH .action_time:= t!reset_clocks(phistop1,(s WITH .activ.xres := a)
        WITH .basic.Tw := 0))
      []
       enabled(phistop2, s)  --> s' = (((s WITH .activ.xres := a) 
        WITH .basic.Tw := 0)
	WITH .action_time:= t!reset_clocks(phistop2,(s WITH .activ.xres := a)
        WITH .basic.Tw := 0))
      []
        enabled(phicont, s)  --> s' = ((s WITH .activ.xres := c) 
	WITH .action_time:= t!reset_clocks(phicont,s WITH .activ.xres := c))
]
               
END;
th1: THEOREM spp |- G((s.basic.Tw = 0 AND s.activ.xres = c) =>
                       F(s.activ.xrel AND s.basic.Tr = 0)); 
END