spec2rec: CONTEXT = BEGIN spec: TYPE = {a, b, c, d, e}; specvote: TYPE = [#x1: spec, x2: spec#]; activity: TYPE = [# xspec: specvote, xrel: bool, xrec: bool #]; action: TYPE = DATATYPE tick, mu1, omega291, alpha1, omega191, rho11, rho21, mu2, omega292, alpha2, omega192, 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, 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 = omega291 THEN t1!twenty_nine ELSIF ac = alpha1 THEN t1!one ELSIF ac = omega191 THEN t1!nineteen ELSIF ac = rho11 THEN t1!one ELSIF ac = rho21 THEN t1!one ELSIF ac = mu2 THEN t1!one ELSIF ac = omega292 THEN t1!twenty_nine ELSIF ac = alpha2 THEN t1!one ELSIF ac = omega192 THEN t1!nineteen 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 = mu1 THEN t1!one ELSIF ac = omega291 THEN t1!twenty_nine ELSIF ac = alpha1 THEN t1!one ELSIF ac = omega191 THEN t1!nineteen ELSIF ac = rho11 THEN t1!one ELSIF ac = rho21 THEN t1!one ELSIF ac = mu2 THEN t1!one ELSIF ac = omega292 THEN t1!twenty_nine ELSIF ac = alpha2 THEN t1!one ELSIF ac = omega192 THEN t1!nineteen 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 = mu1 THEN si.is.Pressure AND si.is.Power ELSIF si.nta = omega291 THEN TRUE ELSIF si.nta = alpha1 THEN si.is.Power ELSIF si.nta = omega191 THEN TRUE ELSIF si.nta = rho11 THEN NOT si.is.Power ELSIF si.nta = rho21 THEN NOT si.is.Power ELSIF si.nta = mu2 THEN si.is.Pressure AND si.is.Power ELSIF si.nta = omega292 THEN TRUE ELSIF si.nta = alpha2 THEN si.is.Power ELSIF si.nta = omega192 THEN TRUE ELSIF si.nta = rho12 THEN NOT si.is.Power ELSIF si.nta = rho22 THEN NOT si.is.Power 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 = mu1 THEN si.a.xspec.x1 = a ELSIF si.nta = omega291 THEN si.a.xspec.x1 = b ELSIF si.nta = alpha1 THEN si.a.xspec.x1 = c ELSIF si.nta = omega191 THEN si.a.xspec.x1 = d ELSIF si.nta = rho11 THEN si.a.xspec.x1 = c ELSIF si.nta = rho21 THEN si.a.xspec.x1 = e ELSIF si.nta = mu2 THEN si.a.xspec.x2 = a ELSIF si.nta = omega292 THEN si.a.xspec.x2 = b ELSIF si.nta = alpha2 THEN si.a.xspec.x2 = c ELSIF si.nta = omega192 THEN si.a.xspec.x2 = d ELSIF si.nta = rho12 THEN si.a.xspec.x2 = c ELSIF si.nta = rho22 THEN si.a.xspec.x2 = e 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; spec1: MODULE = BEGIN GLOBAL s: cs!states INITIALIZATION s = (# activ := (# xspec := (#x1:= a, x2:= a#), xrel := FALSE, xrec := FALSE #), basic:= (# Relay := (#r1:= FALSE, r2:= FALSE#), Power := FALSE, Pressure := FALSE , 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(mu1, s) --> s' = ((s WITH .activ.xspec.x1:=b) WITH .action_time:= t!reset_clocks(mu1, (s WITH .activ.xspec.x1:=b))) [] enabled (omega291, s) --> s' = ((s WITH .activ.xspec.x1 := c) WITH . action_time:= t!reset_clocks(omega291, s WITH .activ.xspec.x1 := c)) [] enabled (alpha1, s) --> s' = (((s WITH .activ.xspec.x1 :=d) WITH .basic.Relay.r1 := TRUE) WITH .action_time:= t!reset_clocks(alpha1, (s WITH .activ.xspec.x1 := d) WITH .basic.Relay.r1:=TRUE)) [] enabled(omega191, s) --> s' = (s WITH .activ.xspec.x1 := e) WITH . action_time:= t!reset_clocks(omega191, s WITH .activ.xspec.x1 := e ) [] enabled(rho11, s) --> s' = (s WITH .activ.xspec.x1 := a) WITH .action_time := t!reset_clocks(rho11, s WITH .activ.xspec.x1 := a) [] enabled(rho21, s) --> s' = ((s WITH .activ.xspec.x1 := a) WITH .basic.Relay.r1 := FALSE) WITH .action_time:= t!reset_clocks(rho21, (s WITH .activ.xspec.x1 := a) WITH .basic.Relay.r1 := FALSE) [] enabled(mu2, s) --> s' = ((s WITH .activ.xspec.x2:=b) WITH .action_time:= t!reset_clocks(mu2, (s WITH .activ.xspec.x2:=b))) [] enabled (omega292, s) --> s' = ((s WITH .activ.xspec.x2 := c) WITH . action_time:= t!reset_clocks(omega292, s WITH .activ.xspec.x2 := c)) [] enabled (alpha2, s) --> s' = (((s WITH .activ.xspec.x2 :=d) WITH .basic.Relay.r2 := TRUE) WITH .action_time:= t!reset_clocks(alpha2, (s WITH .activ.xspec.x2 := d) WITH .basic.Relay.r2:=TRUE)) [] enabled(omega192, s) --> s' = (s WITH .activ.xspec.x2 := e) WITH . action_time:= t!reset_clocks(omega192, s WITH .activ.xspec.x2 := e ) [] enabled(rho12, s) --> s' = (s WITH .activ.xspec.x2 := a) WITH .action_time := t!reset_clocks(rho12, s WITH .activ.xspec.x2 := a) [] enabled(rho22, s) --> s' = ((s WITH .activ.xspec.x2 := a) WITH .basic.Relay.r2 := FALSE) WITH .action_time:= t!reset_clocks(rho22, (s WITH .activ.xspec.x2 := a) 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 := 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.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 spec1 |- G(NOT (s.basic.Tw = 0 AND s.activ.xrec)); END