progres: CONTEXT = BEGIN prog: TYPE = {a, b, c}; activity: TYPE = [# xprog: prog, xrel: bool, xres: prog #]; c1type: TYPE = [0..30]; action: TYPE = DATATYPE tick, mu1, alpha, mu2, rho1, rho2, gamma, 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: c1type, c2: tr, 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 = gamma 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 = gamma 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 = gamma THEN 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.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 = gamma 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(gamma, s) --> s' = (s WITH .basic.c2 := 0) WITH .action_time:= t!reset_clocks(gamma, s WITH .basic.c2 := 0) [] 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