prog2rec: CONTEXT = BEGIN prog: TYPE = {a, b, c}; prog2: TYPE = [#x1: prog, x2: prog#]; activity: TYPE = [# xprog: prog, xrel: bool, xrec: bool #]; ctype: TYPE = [0..30]; action: TYPE = DATATYPE tick, mu11, alpha1, mu21, rho11, rho21, mu12, alpha2, mu22, rho12, rho22, wr, ws, pr, ps, rhoo, rhoc, phistart, phistop END; tr: TYPE = [0..20]; tw: TYPE = [0..2]; internal_state: TYPE = [# Relay: [#r1: bool, r2: bool#], Power:bool, Pressure:bool, c1: [#cs1:ctype, cs2: ctype#], c2: [#cs1:ctype, cs2: 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 = mu11 THEN t1!one ELSIF ac = alpha1 THEN t1!one ELSIF ac = mu21 THEN t1!one ELSIF ac = rho11 THEN t1!one ELSIF ac = rho21 THEN t1!one ELSIF ac = mu12 THEN t1!one ELSIF ac = alpha2 THEN t1!one ELSIF ac = mu22 THEN t1!one ELSIF ac = rho12 THEN t1!one ELSIF ac = rho22 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 = phistop THEN t1!zero ELSE t1!one ENDIF; upper_bound (ac:nt_action): t1!time = IF ac = mu11 THEN t1!one ELSIF ac = alpha1 THEN t1!one ELSIF ac = mu21 THEN t1!one ELSIF ac = rho11 THEN t1!one ELSIF ac = rho21 THEN t1!one ELSIF ac = mu12 THEN t1!one ELSIF ac = alpha2 THEN t1!one ELSIF ac = mu22 THEN t1!one ELSIF ac = rho12 THEN t1!one ELSIF ac = rho22 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 = phistop THEN t1!zero ELSE t1!one ENDIF; % preconditions enabled_state (si:cs!states1): bool = IF si.nta = mu11 THEN (si.is.Pressure AND si.is.Power AND si.is.c1.cs1 = 0 AND si.is.c2.cs1 = 0) OR (si.is.c1.cs1 >= 1 AND si.is.c1.cs1 <= 29) ELSIF si.nta = alpha1 THEN si.is.Power AND si.is.c1.cs1 >= 30 ELSIF si.nta = mu21 THEN (si.is.c1.cs1 = 0 AND si.is.c2.cs1 >= 1 AND si.is.c2.cs1 <= 19) ELSIF si.nta = rho11 THEN NOT si.is.Power AND si.is.c1.cs1 >= 30 ELSIF si.nta = rho21 THEN NOT si.is.Power AND si.is.c1.cs1 = 0 AND si.is.c2.cs1 >= 20 ELSIF si.nta = mu12 THEN (si.is.Pressure AND si.is.Power AND si.is.c1.cs2 = 0 AND si.is.c2.cs2 = 0) OR (si.is.c1.cs2 >= 1 AND si.is.c1.cs2 <= 29) ELSIF si.nta = alpha2 THEN si.is.Power AND si.is.c1.cs2 >= 30 ELSIF si.nta = mu22 THEN (si.is.c1.cs2 = 0 AND si.is.c2.cs2 >= 1 AND si.is.c2.cs2 <= 19) ELSIF si.nta = rho12 THEN NOT si.is.Power AND si.is.c1.cs2 >= 30 ELSIF si.nta = rho22 THEN NOT si.is.Power AND si.is.c1.cs2 = 0 AND si.is.c2.cs2 >= 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.r1 AND si.is.Relay.r2) ELSIF si.nta = rhoc THEN (NOT si.is.Relay.r1 AND NOT si.is.Relay.r2) ELSIF si.nta = phistart THEN si.a.xrel AND si.is.Tr = 0 AND NOT si.is.Power ELSIF si.nta = phistop THEN NOT si.a.xrel OR si.is.Power ELSE FALSE ENDIF; graph(si:cs!states2):bool = IF si.nta = mu11 THEN si.a.xprog = a ELSIF si.nta = alpha1 THEN si.a.xprog = a ELSIF si.nta = mu21 THEN si.a.xprog = a ELSIF si.nta = rho11 THEN si.a.xprog = a ELSIF si.nta = rho21 THEN si.a.xprog = a ELSIF si.nta = mu12 THEN si.a.xprog = a ELSIF si.nta = alpha2 THEN si.a.xprog = a ELSIF si.nta = mu22 THEN si.a.xprog = a ELSIF si.nta = rho12 THEN si.a.xprog = a ELSIF si.nta = rho22 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 NOT si.a.xrec ELSIF si.nta = phistop THEN si.a.xrec 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, xrec := FALSE #), basic:= (# Relay := (#r1:= FALSE, r2:= FALSE#), Power := FALSE, Pressure := FALSE , c1:=(#cs1 := 0, cs2:= 0#), c2:= (#cs1 := 0, cs2:= 0#), Tr := 0, Tw := 0 #), action_time:=(LAMBDA (a:nt_action): t1!zero)#) TRANSITION [ enabled(tick, s) --> s' = (IF ( s.activ.xrec 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.xrec 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(mu11, s) --> s' = ((s WITH .basic.c1.cs1:= s.basic.c1.cs1 + 1) WITH .action_time:= t!reset_clocks(mu11, (s WITH .basic.c1.cs1 :=s.basic.c1.cs1 + 1))) [] enabled (alpha1, s) --> s' = (((s WITH .basic.c1.cs1 :=0) WITH .basic.c2.cs1 := s.basic.c2.cs1 + 1) WITH .basic.Relay.r1 := TRUE) WITH .action_time:= t!reset_clocks(alpha1, ((s WITH .basic.c1.cs1 := 0) WITH .basic.c2.cs1 := s.basic.c2.cs1 + 1) WITH .basic.Relay.r1:=TRUE) [] enabled(mu21, s) --> s' = ((s WITH .basic.c2.cs1 := s.basic.c2.cs1 + 1) WITH .basic.Relay.r1 := TRUE) WITH .action_time:= t!reset_clocks(mu21, (s WITH .basic.c2.cs1 := s.basic.c2.cs1 + 1) WITH .basic.Relay.r1 := TRUE ) [] enabled(rho11, s) --> s' = (s WITH .basic.c1.cs1 := 0) WITH .action_time := t!reset_clocks(rho11, s WITH .basic.c1.cs1 := 0) [] enabled(rho21, s) --> s' = ((s WITH .basic.c2.cs1 := 0) WITH .basic.Relay.r1 := FALSE) WITH .action_time:= t!reset_clocks(rho21, (s WITH .basic.c2.cs1 := 0) WITH .basic.Relay.r1 := FALSE) [] enabled(mu12, s) --> s' = ((s WITH .basic.c1.cs2:= s.basic.c1.cs2 + 1) WITH .action_time:= t!reset_clocks(mu12, (s WITH .basic.c1.cs2 :=s.basic.c1.cs2 + 1))) [] enabled (alpha2, s) --> s' = (((s WITH .basic.c1.cs2 :=0) WITH .basic.c2.cs1 := s.basic.c2.cs1 + 1) WITH .basic.Relay.r2 := TRUE) WITH .action_time:= t!reset_clocks(alpha2, ((s WITH .basic.c1.cs2 := 0) WITH .basic.c2.cs2 := s.basic.c2.cs2 + 1) WITH .basic.Relay.r2:=TRUE) [] enabled(mu22, s) --> s' = ((s WITH .basic.c2.cs2 := s.basic.c2.cs2 + 1) WITH .basic.Relay.r2 := TRUE) WITH .action_time:= t!reset_clocks(mu22, (s WITH .basic.c2.cs2 := s.basic.c2.cs2 + 1) WITH .basic.Relay.r2 := TRUE ) [] enabled(rho12, s) --> s' = (s WITH .basic.c1.cs2 := 0) WITH .action_time := t!reset_clocks(rho12, s WITH .basic.c1.cs2 := 0) [] enabled(rho22, s) --> s' = ((s WITH .basic.c2.cs2 := 0) WITH .basic.Relay.r2 := FALSE) WITH .action_time:= t!reset_clocks(rho22, (s WITH .basic.c2.cs2 := 0) WITH .basic.Relay.r2 := 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 := 19) WITH .action_time:= t!reset_clocks(rhoo,(s WITH .activ.xrel := TRUE) WITH .basic.Tr := 19)) [] 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.xrec := TRUE) WITH .basic.Tw := 2) WITH .action_time:= t!reset_clocks(phistart,(s WITH .activ.xrec := TRUE) WITH .basic.Tw := 2)) [] enabled(phistop, s) --> s' = (((s WITH .activ.xrec := FALSE) WITH .basic.Tw := 0) WITH .action_time:= t!reset_clocks(phistop, (s WITH .activ.xrec := FALSE) WITH .basic.Tw := 0)) ] END; th1: THEOREM spp |- G(NOT (s.basic.Tw = 0 AND s.activ.xrec)); END