specrres: CONTEXT = BEGIN spec: TYPE = {a, b, c, d, e}; activity: TYPE = [# xspec: spec, xrel: bool, xres: spec #]; action: TYPE = DATATYPE tick, mu, omega29, alpha, omega19, 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, 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 = mu THEN t1!one ELSIF ac = omega29 THEN t1!twenty_nine ELSIF ac = alpha THEN t1!one ELSIF ac = omega19 THEN t1!nineteen 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 = mu THEN t1!one ELSIF ac = omega29 THEN t1!twenty_nine ELSIF ac = alpha THEN t1!one ELSIF ac = omega19 THEN t1!nineteen 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 = mu THEN si.is.Pressure AND si.is.Power ELSIF si.nta = omega29 THEN TRUE ELSIF si.nta = alpha THEN si.is.Power ELSIF si.nta = omega19 THEN TRUE ELSIF si.nta = rho1 THEN NOT si.is.Power ELSIF si.nta = rho2 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 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 = mu THEN si.a.xspec = a ELSIF si.nta = omega29 THEN si.a.xspec = b ELSIF si.nta = alpha THEN si.a.xspec = c ELSIF si.nta = omega19 THEN si.a.xspec = d ELSIF si.nta = rho1 THEN si.a.xspec = c ELSIF si.nta = rho2 THEN si.a.xspec = 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 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 := (# xspec := a, xrel := FALSE, xres := a #), basic:= (# Relay := 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.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(mu, s) --> s' = ((s WITH .activ.xspec:=b) WITH .action_time:= t!reset_clocks(mu, (s WITH .activ.xspec:=b))) [] enabled (omega29, s) --> s' = ((s WITH .activ.xspec := c) WITH . action_time:= t!reset_clocks(omega29, s WITH .activ.xspec := c)) [] enabled (alpha, s) --> s' = (((s WITH .activ.xspec :=d) WITH .basic.Relay := TRUE) WITH .action_time:= t!reset_clocks(alpha, (s WITH .activ.xspec := d) WITH .basic.Relay:=TRUE)) [] enabled(omega19, s) --> s' = (s WITH .activ.xspec := e) WITH . action_time:= t!reset_clocks(omega19, s WITH .activ.xspec := e ) [] enabled(rho1, s) --> s' = (s WITH .activ.xspec := a) WITH .action_time := t!reset_clocks(rho1, s WITH .activ.xspec := a) [] enabled(rho2, s) --> s' = ((s WITH .activ.xspec := a) WITH .basic.Relay := FALSE) WITH .action_time:= t!reset_clocks(rho2, (s WITH .activ.xspec := a) 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)); th1: THEOREM spp |- G((s.basic.Tw = 0 AND s.activ.xres = c) => F(s.activ.xrel AND s.basic.Tr = 0)); END