-- statechartcompiler.csp InputIds = {i | (i,_,_) <- Inputs} xvars = SigChans changes = union(InputIds,xvars) transparent chase, chase_nocache id(x) = x chaseop = chase System(Hierarchy) = chaseop( (VARSandTIMERS [|{|tock,calculate,step,ich,xch,iwrite,read,readch,timer_read,timer_on,timer_cancel|}|] Sys(Hierarchy,true,false))\{|ich,iwrite,read,readch,timer_read,timer_on,timer_cancel|}) [|{|action,tock,step,turn_me_on,outp,xch|}|] (NOACT[|{|tock,step|}|]TOX) NOACT = action?_ -> ACTS [] turn_me_on -> ACTS [] STEPTOCK STEPTOCK = tock -> NOACT ACTS = action?_ -> ACTS [] turn_me_on -> ACTS [] step -> NOACT TOX = tock -> OUTP OUTP = outp?_ -> OUTP [] XCH XCH = xch?_ -> XCH [] step -> STEPTOX [] tock -> OUTP STEPTOX = step -> STEPTOX [] outp?_ -> STEPTOX [] TOX -- The following are the ordinary system with and without the ability to be -- turned on and off at the highest level. SYSTEM'(Hierarchy) = System(Hierarchy) ncSYSTEM(Hierarchy) = SYSTEM'(Hierarchy) [|{|turn_me_on,turn_me_off|}|] STOP --^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -- We now define a basic check which combines a test for all the error -- events with the check that there can never be an infinity of -- step events without an infinity of tocks. delayable = {|xch,turn_me_on,turn_me_off,isat,outp|} error_events = {|action.error, -- indicates nondeterminism caused by -- ambiguous branching varerror, -- multiple writes on a small step outofrange, -- on an assignment (will include ERRVAL) timer_overflow,-- attempt to read a timer that has reached the -- bound Timer_Limit type_error -- boolean expression produces result not 0,1 |} Time_Error_Spec = tock -> Time_Error_Spec [] (STOP |~| ([] x:delayable @ x -> Time_Error_Spec)) Time_Error_Imp(Hierarchy) = SYSTEM(Hierarchy)\diff(Events,Union({{tock},delayable,error_events})) -- You should run the following check for every chart you are -- investigating: -- Time_Error_Spec [FD= Time_Error_Imp(Hierarchy) --^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -- Below is an attempt to make the running phase more efficient through the -- use of chase: it conceals all "internal activity" meaning little steps, the -- synchronisations other than tock, actions labelled progress. (Interactions -- about values of variables have already received this treatment.) We need to -- distinguish the calculate events that occur after a phase of internal input -- (which we do not want to chase) from those that occur after internal -- action/assignment steps. -- We would expect this to give a real advantage (as opposed to merely reducing -- the number of externally visible states while still going through as many -- inside the chase operator) when one has multiple threads active at once -- for a significant proportion of the time. SYSTEM(Hierarchy) = chaseop((ncSYSTEM(Hierarchy)[[calculate <- calculate, calculate <-inputs_over]] [|{calculate, tock, step, inputs_over}|] chREG) \diff(Events,{|step,tock,inputs_over,outp,xch,isat, action.l, tau_nc | l <- ActLabel, l!=progress|}))\{|step|} channel inputs_over chREG = tock -> inputs_over -> chREG [] step -> calculate -> chREG -- Using this on a system that diverges on the timing consistency check (which cannot -- be done on this, though it would be OK if step were not hidden here) can cause -- the chase operator to fail. Using it on a system not proved free of error flag -- events without chasing action.progress can cause the above to be a proper refinement -- of what is intended. -- {- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Creating the hierarchy The definition of the main type of chart structures follows: -} Statelabel = {0..20} -- labels for individual states within -- a sequential graph. Integers at present. datatype Statechart = SCTree.SGlabel.Set(ActLabel).Set((Statelabel,Statechart)) {- The type SGlabel is user-defined like Identifiers and consists of the names of the various sequential graphs which make up a system description. This recursive definition says that a chart is root behaviour identified by one of these labels, RL say, a set of actions labels that are not to be promoted beyond this point, and a set of pairs, each a state label of RL together with a chart (a member of the type we are defining) which sits within it. A chart with no lower level charts has this set of pairs empty, of course. This is reflected in the next definition. -} Sys(SCTree.label.acts.{},initon,par_prom) = (Machine(sm(label),initstate(label),initon,par_prom,SCTree.label.acts.{}) [|{|proceed|}|]STOP) [[action'.a.v <- action.a | a <- all_actions(label), v <- StateLabel']] [[action.a <- action.progress | a <- acts]] -- not controlled outside is renamed to progress {- The function Machine, defined later, creates a process from a description of a sequential chart. Each sequential machine has an event proceed which is used to enable sub-charts to do things (implementing the priority rule). For the above case with no sub-machines this action is not required, hence the synchronisation with STOP that bans it. The renamings are to discard information unnecessary outside this level and to square the outer alphabet of the process with what will be required outside. For a chart with subcharts this becomes a little more complex, since we now need to use the same function on the subcharts, synchronise them appropriately, and turning them on and off correctly. -} Sys(SCTree.label.acts.STs,initon,par_prom) = let TopMach = Machine(sm(label),initstate(label),initon,par_prom,sc0) sc0 = SCTree.label.acts.STs syncacts = sec_acts(label) -- the actions that the top -- node promotes from underneath SLabs = {n | (n,_) <- STs} within (TopMach[[action'.a.l <- action.a | a <- syncacts, l <- StateLabel']] [|union({|tock,step,calculate,turn_me_on,turn_me_off,action',xch,iwrite,proceed,peer_turn_off|}, {|action.a | a <- syncacts|})|] ([|{|tock,step,calculate,turn_me_on,turn_me_off, peer_turn_off,iwrite,xch,action'|}|] v:{v' | (v',_) <- STs} @ (let SCsInV = {sc | (v',sc) <- STs, v'==v} par_prom' = card(SCsInV)>1 and inter(syncacts,Union({Galpha(sc) | sc <-SCsInV}))!={} par_of_subs_of_V = ([|{|tock,step,calculate,turn_me_on,turn_me_off,iwrite,xch,action',peer_turn_off,local_over|}|] sc:SCsInV @ ((Sys(sc,v==startstate(label) and initon,par_prom')[[action.progress <- proceed.v]] -- progress by inner machines controlled by these events [[turn_me_off <- action'.a.v', turn_me_off <- turn_me_off, (if v==startstate(label) then turn_me_on else turn_me_off) <- turn_me_on, turn_me_on <- action'.a.v, turn_me_off <- dummy | a <- diff(all_actions(label),syncacts),v' <- diff(StateLabel',{v})]] -- action by high-level process to the right state re-starts this one ) )) within (if par_prom' then (par_of_subs_of_V [|{one_prom,two_prom,peer_turn_off,step,tock,calculate,local_over}|] Prom_Mon)\{one_prom,two_prom,peer_turn_off,local_over} else par_of_subs_of_V )[[dummy <- peer_turn_off]] -- has the effect of a high-level peer_turn_off turning -- off these sub-machines ) -- ending construction for particular node's subgraphs ) -- ending parallel of all subgraphs ) -- ending complete parallel of Topmach and slaves [[action'.a.v <- action.a | a <- all_actions(label), v <- StateLabel']] [[proceed.v <- action.progress | v <- SLabs]] -- finally all progress within this sys and [[action.a <- action.progress | a <- acts]] -- not controlled outside is renamed to progress {- The following are the definitions of some channels and functions for extracting some of the sets of actions used by the above. -} channel turn_me_on, turn_me_off channel proceed:Statelabel channel dummy sec_acts(label) = let (G,_,_) = sm(label) within Union({set() | (_,_,sa) <- G}) prim_actions(label) = let (G,_,_) = sm(label) within union({progress}, Union({set() | (_,pa,_) <- G})) all_actions(label) = union(prim_actions(label),sec_acts(label)) new_acts(label) = let (G,_,_) = sm(label) within {a | (_,pa,_) <- G, (_,a,_,_) <- set(pa), a != progress} Galpha(SCTree.label.As._) = diff(union(sec_acts(label),prim_actions(label)), union(As,{progress})) {- Labels are associated with the actual state machine descriptions initial state and the variables relevant to that machine in the set AllCharts, defined by the user, with information extracted below. -} sm(label) = let {m} = {(G,l,v) | (G,l,v,vs) <- AllCharts, l==label} within m startstate(label) = let {v} = {v | (G,l,v,vs) <- AllCharts, l==label} within v initstate(label) = let {vs} = {vs' | (_,l,_,vs') <- AllCharts, l==label} within sstate(vs) sls(label) = let {vs} = {ss | (ss,l,_,_) <- AllCharts, l==label} within {n | (n,_,_) <- vs} -- The initial variable state of a given sequential chart. sstate(vs) = ({(i,v) | (i,v,_) <- union(Inputs,Variables), member(i,vs)},{},{}) {- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Expressions for use in assignments The model used for assignable expressions is that each is a function which can be applied to a state which contains the values of all variables it uses and delivers the result. In this version it delivers a pair, the result paired with a list of the variables which are not in state and need to be got from state. Obviously if the second is nonempty the first is nonsense! First two definitions built upon the user-supplied set of constants with values... -} Consts = {c | (c,_) <- Constants} CV(c) = pick({v | (c',v) <- Constants, c'==c}) pick({x}) = x -- The value of a variable or constant i is represented -- by the expression Ival(i)... Ival(i)(S) = let (S',_,_) = S vornot = {x | (j,x) <- S', i==j} within if member(i,Consts) then (CV(i),<>) else if vornot == {} then (0,) else (pick(vornot),<>) -- ch(i) is true (of an input variable) if the value has just -- changed by external input. Can only be true the first -- step after a tock. The state S has a special component to -- record for which variables this is true, and in this version -- we also record which of these values are needed. ch(i)(S) = let (_,CH,_)=S within (bmap(member(i,CH)),<(Nd_C.i)>) -- handling the ch(x) function -- timer(n,e) produces a boolean value: true if timer n exceeds -- expression e. If it is a deterministic timer then it is an -- error for e to be bigger than tlimit, if nondeterministic (and -- therefore representing an arbitrary limit above some the tlimit -- threshold), it is cut bacl to tlimit as explained elsewhere. timer(n,e)(S) = let (_,_,TS) = S t = if member(n,{m | (m,_) <- TS}) then pick({k | (m,k) <- TS,m==n}) else 0 (v',ns) = e(S) v = (if nondetT(n) then min(v',tlimit(n)) else v') invalid = (v > tlimit(n)) or v==ERRVAL within (if invalid then ERRVAL else if t >= v then 1 else 0,^ns) -- always need to update the timer. min(x,y) = if x < y then x else y datatype needs = Nd_V.Identifiers | Nd_C.Identifiers | Nd_T.Timer_Names varneeded(Nd_V._) = true varneeded(_) = false ndv(Nd_V.i) = i chneeded(Nd_C._) = true chneeded(_) = false tneeded(Nd_T._) = true tneeded(_) = false ndc(Nd_C.i) = i ndt(Nd_T.n) = n K(x)(S) = (x,<>) -- combinator for constants TRUE = K(1) -- booleans are modelled as integers FALSE = K(0) ZERO = K(0) ONE = K(1) notf(e)(S) = let (v,m) = e(S) within (if v==ERRVAL then ERRVAL else (1-v), m) andf(e1,e2)(S) = let (v1,m1) = e1(S) (v2,m2) = e2(S) within (if member(ERRVAL,{v1,v2}) then ERRVAL else (v1 * v2), m1^m2) orf(e1,e2)(S) = let (v1,m1) = e1(S) (v2,m2) = e2(S) within (if member(ERRVAL,{v1,v2}) then ERRVAL else (bmap((v1+v2)>0)), m1^m2) -- list-based and and or andl(<>) = TRUE andl(^es) = andf(e,andl(es)) orl(<>) = FALSE orl(^es) = orf(e,orl(es)) succ(e)(S) = let (v,m) = e(S) within (if v==ERRVAL then ERRVAL else v+1, m) decr(e)(S) = let (v,m) = e(S) within (if v==ERRVAL or v<=0 then ERRVAL else v-1, m) add(e1,e2)(S) = let (v1,m1) = e1(S) (v2,m2) = e2(S) within (if member(ERRVAL,{v1,v2}) then ERRVAL else (v1+v2),m1^m2) times(e1,e2)(S) = let (v1,m1) = e1(S) (v2,m2) = e2(S) within (if member(ERRVAL,{v1,v2}) then ERRVAL else (v1*v2),m1^m2) div(e1,e2)(S) = let (v1,m1) = e1(S) (v2,m2) = e2(S) within (if member(ERRVAL,{v1,v2}) or v2==0 then ERRVAL else (v1/v2),m1^m2) minus(e1,e2)(S) = let (v1,m1) = e1(S) (v2,m2) = e2(S) within (if member(ERRVAL,{v1,v2}) then ERRVAL else (v1-v2),m1^m2) addl(<>) = ZERO addl(^es) = add(e,addl(es)) eqf(e1,e2)(S) = let (v1,m1) = e1(S) (v2,m2) = e2(S) within (if member(ERRVAL,{v1,v2}) then ERRVAL else bmap(v1==v2),m1^m2) gef(e1,e2)(S) = let (v1,m1) = e1(S) (v2,m2) = e2(S) within (if member(ERRVAL,{v1,v2}) then ERRVAL else bmap(v1>=v2),m1^m2) gt(e1,e2)(S) = let (v1,m1) = e1(S) (v2,m2) = e2(S) within (if member(ERRVAL,{v1,v2}) then ERRVAL else bmap(v1>v2),m1^m2) cond(b,e1,e2)(S) = let (v0,m0) = b(S) (v1,m1) = e1(S) (v2,m2) = e2(S) within (if v0==ERRVAL then ERRVAL else if v0==1 then v1 else v2,m0^m1^m2) bmap(true) = 1 bmap(false) = 0 -- case takes a selector expression n, a list of pairs of expressions, -- the first matching the selector, and an expression e for when there -- is no match case(n,ps,e)(S) = let (vn,mn) = n(S) (vps,mps) = lev(ps)(S) (ve,me) = e(S) within (if member(ERRVAL,{vn,ve}) then ERRVAL else head(^), mn^mps^me) concat(<>) = <> concat(^xss) = xs^concat(xss) lev(ps)(S) = let es = <(c(S),v(S)) | (c,v) <- ps> within (<(c1,v1) | ((c1,_),(v1,_)) <- es>, concat()) -- so for example we could translate the expression (i+j)>= (k/3) -- by gef(add(Ival(i),Ival(j)),div(Ival(k),K(3))) -- The important thing is that the state parameter is not used -- explicitly: we are combining curried functions. -- Of course the user can define more of these functional -- operations like add and andf in the same style. -- For initialising and defining boolean variables we provide -- the following nbool = {ntrue,nfalse} ntrue = 1 nfalse = 0 ERRVAL = 1000000 {- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Building sequential charts A sequential chart is defined as a state machine: a set of state labels coupled with a set of appropriately annotated actions. As discussed above we need both primary actions, that a machine instigates itself, and secondary ones that promote lower-level ones. The format of a primary action is (guard, -- function state -> "bool" (= {0,1}) label, -- integer updates, -- list of pairs (identifier, state -> value) for assignments following the action next state) A secondary action (where the guards and updates are owned by the substate action which this promotes, but this is listed here because it takes this process to a new state) only has (label, next state) The function Machine takes one of these machines and an initial state and delivers the appropriate behaviour. -} OMEGA = 999 -- the target state of any action which leads outside the present machine; -- namely one that is promoted to a higher level. StateLabel'=union(Statelabel,{OMEGA}) channel action:ActLabel channel action':ActLabel.StateLabel' -- the state label (of target) is added for -- allowing inner machines to know when to start. channel isat:(SGlabel,Statelabel) -- for diagnostics Machine(T,SS,initon,par_prom,sc0) = -- this is a complex definition using many -- subsidiary clauses. let (G,id,start) = T M1(v,S,ison) = xch?(i,z) -> M1(v,upd(S,i,z),ison) [] calculate -> M2(v,S,ison) [] (member((id,v),indstates) and ison) & isat.(id,v) -> M1(v,S,ison) -- M1 is phase of external inputs after a tock M1'(v,S,ison) = iwrite?(i,z) -> M1'(v,upd(S,i,z),ison) [] calculate -> M2(v,S,ison) [] (member((id,v),indstates) and ison) & isat.(id,v) -> M1'(v,S,ison) -- M1' is phase of inputting new variable values after step after a tock M2(v,S,ison) = -- phase of performing actions let {(pa,sa)} = {(pa,sa) | (v',pa,sa) <- G, v==v'} -- this node's actions Analyse(<>,ens) = (if ens == <> then -- no transitions enabled (step -> M1'(v,noch(S),true) [] tock -> M1(v,noch(S),true) [] ([] (l,n):set(sa) @ (if n !=OMEGA then (if not par_prom then action.l -> Timer_Man(sc0,v,n); Assign(<>,n,S) else action.l -> local_over -> Timer_Man(sc0,v,n); Assign(<>,n,S)) else if not par_prom then (action.l -> Timer_Man(sc0,v,n); (let P = (step -> M1'(start,noch(S),false) [] turn_me_off -> step -> M1'(start,noch(S),false) [] ([] (l,n):set(sa) @ action.l -> action.error -> STOP)) within P)) else (two_prom -> STOP [] local_over -> Prom_Act_pa(a,sc0,v,upds,S))) ) [] proceed.v -> M2(v,S,ison) [] par_prom & peer_turn_off -> step -> M1'(start,noch(S),false) [] par_prom & local_over -> Analyse(<>,ens)) else let <(a,upds,nextst)> = ens within -- one enabled (if not par_prom then action'.a.nextst -> Timer_Man(sc0,v,nextst); Assign(upds,nextst,S) else if (nextst != OMEGA) then action'.a.nextst -> local_over -> Timer_Man(sc0,v,nextst); Assign(upds,nextst,S) else (two_prom -> STOP [] par_prom & local_over -> Prom_Act(a,sc0,v,upds,S) [] not(par_prom) & Prom_Act(a,sc0,v,upds,S) )) ) [] turn_me_off -> (step -> M1'(start,noch(S),false) [] tock -> M1(v,noch(S),false)) [] turn_me_on -> step -> M1'(start,noch(S),true) Analyse(<(g,a,us,ns)>^ts,ens) = let needed = missing_vars(g,S) within Collect(<(g,a,us,ns)>^ts,S,ens,needed) Prom_Act(a,sc0,v,upds,S) = action'.a.OMEGA -> Timer_Man(sc0,v,OMEGA); one_prom -> peer_turn_off -> Assign(upds,OMEGA,S) [] turn_me_off -> (step -> M1'(start,noch(S),false) [] tock -> M1(v,noch(S),false)) [] turn_me_on -> step -> M1'(start,noch(S),true) Prom_Act_pa(a,sc0,v,upds,S) = action.a -> Timer_Man(sc0,v,OMEGA); one_prom -> peer_turn_off -> Assign(upds,OMEGA,S) [] turn_me_off -> (step -> M1'(start,noch(S),false) [] tock -> M1(v,noch(S),false)) [] turn_me_on -> step -> M1'(start,noch(S),true) -- Note that this definition would easily permit priority rules to be applied, -- which would simplify many of the examples of guards we have seen in statecharts. Collect(<(g,a,us,ns)>^ts,S',ens,needed) = (if needed == <> then (if eval(g,S')==1 then (if ens==<> then Analyse(ts,<(a,us,ns)>) else action.error -> STOP) else if eval(g,S')==0 then Analyse(ts,ens) else type_error -> STOP) else let ^nds = needed within if varneeded(nd) then read?(_,x):wrange(ndv(nd)) -> Collect(<(g,a,us,ns)>^ts,addval(S',(ndv(nd),x)),ens,nds) else if chneeded(nd) then readch?(_,x):chrange(ndc(nd)) -> Collect(<(g,a,us,ns)>^ts,addch(S',(ndc(nd),x)),ens,nds) else timer_read.ndt(nd)?x:{0..tlimit(ndt(nd))} -> if nondetT(ndt(nd)) and x == tlimit(ndt(nd)) then nondet_nc(Collect(<(g,a,us,ns)>^ts,addtr(S',ndt(nd),x),ens,nds), Collect(<(g,a,us,ns)>^ts,addtr(S',ndt(nd),x+1),ens,nds)) else Collect(<(g,a,us,ns)>^ts,addtr(S',ndt(nd),x),ens,nds)) within -- Body of M2(v,S,ison) if ison then Analyse(pa,<>) else -- when it is off (step -> M1'(v,noch(S),ison) [] tock -> M1(v,noch(S),ison) [] turn_me_on -> step -> M1'(start,noch(S),true) [] turn_me_off -> (step -> M1'(start,noch(S),false) [] tock -> M1(v,noch(S),false)) [] par_prom & peer_turn_off -> step -> M1'(start,noch(S),false) [] par_prom & local_over -> M2(v,S,ison)) -- Assign carries out the assignments consequent on an action, -- primes any timers (other than those tied to states) -- and then moves to the next state. Assign(<>,nxt,S) = step -> (if nxt==OMEGA then M1'(start,noch(S),false) else M1'(nxt,noch(S),true)) [] par_prom & peer_turn_off -> step -> M1'(start,noch(S),false) [] turn_me_off -> step -> M1'(start,noch(S),false) Assign(<(id,e)>^us,nxt,S) = let ms = missing_vars(e,S) Collect(needed,S') = -- similar but not exactly the same as Collect -- for Analyse if needed == <> then (let val=eval(e,S') within if member(id,{n | n <- Named_Timers}) then (if member(val,{1..Timer_Limit}) then timer_on.Tr.id.val -> Assign(us,nxt,S) else outofrange.id -> STOP) else if member((id,val),wrange(id)) then ich.(id,val) -> Assign(us,nxt,S) else outofrange.id -> STOP) else let ^nds = needed within if varneeded(nd) then read?(_,x):wrange(ndv(nd)) -> Collect(nds,addval(S',(ndv(nd),x))) else if chneeded(nd) then readch?(_,x):chrange(ndc(nd)) -> Collect(nds,addch(S',(ndc(nd),x))) else timer_read.ndt(nd)?x:{0..tlimit(ndt(nd))} -> Collect(nds,addtr(S',ndt(nd),x)) within Collect(ms,S) noch((S,C,T)) = (S,{},{}) upd(S,i,z) = let (S',C,T) = S within ({(i',if i'==i then z else z') | (i',z') <- S'},C,T) addval(S,(v,x)) = let (S1,S2,S3) = S S1' = union(S1,{(v,x)}) within (S1',S2,S3) addch(S,(v,x)) = let (S1,S2,S3) = S S2' = if x then union(S2,{v}) else diff(S2,{v}) within (S1,S2',S3) addtr(S,l,x) = let (S1,S2,S3) = S S3' = union({(l,x)},{(l',x') | (l',x') <- S3, l !=l'}) within (S1,S2,S3') -- and finally the definition of Machine: within tock -> (if initon then Timer_Man(sc0,OMEGA,start) else SKIP); M1(start,SS,initon) --^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -- Nondeterministic choice which is protected from chase..... to be used -- for all intended nondeterministic behaviour. channel tau_nc nondet_nc(P,Q) = tau_nc -> P [] tau_nc -> Q --^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -- Process which exists to monitor and propagate effects of -- promoted actions between charts that run in parallel with -- a higher level state. channel one_prom, two_prom, peer_turn_off, local_over Prom_Mon = tock -> calculate -> Prom_Mon' Prom_Mon' = let P =one_prom -> Prom_Mon'' [] step -> calculate -> Prom_Mon' [] tock -> calculate -> Prom_Mon' within P [] local_over -> P Prom_Mon'' = one_prom -> action.error -> STOP [] two_prom -> action.error -> STOP [] peer_turn_off -> step -> calculate -> Prom_Mon' --^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -- The following are standard functions used in expression manipulation. -- Note the set-based definition of remdups. fst((x,y)) = x snd((x,y)) = y remdups(xs) = remdups'({},xs) remdups'(seen,<>) = <> remdups'(seen,^xs) = if member(x,seen) then remdups'(seen,xs) else ^remdups'(union(seen,{x}),xs) missing_vars(e,S) = remdups(snd(e(S))) eval(e,S) = fst(e(S)) head(^_) = x {- Sequence of actions in system: * ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Defining variable processes xch is the channel for external changes (i.e., when this is an input), only possible on tock iwrite is channel for internal writes, two of which on one step are an error ich is channel used to inform processes of real internal change of value after the calculate action -} inpvals = {(v,x) | (v,_,r) <- Inputs, x <- r} varvals = Union({inpvals, {(v,x) | (v,_,r) <- Variables, x <- r} , {(id,x) | id <- SigChans, x <- nbool}}) outpvals = {(v,x) | (v,x) <- varvals, member(v,Outputs)} xvals = {(id,x) | id <- xvars, x <- nbool} wrange(id) = {(i,v) | (i,v) <- varvals, i==id} irange(id) = {(i,v) | (i,v) <- inpvals, i==id} chrange(id) = {(i,b) | i <- changes, i==id, b <- {true,false}} xrange(id) = {(i,v) | (i,v) <- union(xvals,inpvals), i==id} channel xch:varvals channel ich,ich',iwrite:varvals channel outp:outpvals channel step,calculate,tock, varerror, type_error channel read:varvals channel readch:(changes,{true,false}) channel outofrange:Identifiers channel timer_overflow:All_Timers varnames = {x | (x,_,_) <- union(Inputs,Variables)} -- The following definition of a variable process takes account of -- several important features: -- external inputs (xch) only occur immediately after tock. -- external outputs (outp) only occur immediately after tock (and are -- assumed to be latched elsewhere). -- values internally written in one small step do not take effect until the next. VAR(id,range,v,ch)= let VARXI(v,v0) = member(id,InputIds) & xch?(_,v'):wrange(id) -> VARXI(v',v0) [] calculate -> VARNC(v,member(id,changes) and (v!=v0)) [] member(id,Outputs) & outp.(id,v) -> VARXI(v,v0) -- ready for external input VARIW(v) = iwrite.(id,v) -> VARII(v) VARNC(v,ch) = step -> VARII(v) [] tock -> VARXI(v,if member(id,changes) then v else 0) [] ich?(_,v'):wrange(id) -> VARIC(v',ch) [] member(id,xvars) & xch?(_,v'):wrange(id) -> VARXC(v',ch) [] member(id,changes) & readch.(id,ch) -> VARNC(v,ch) VARXC(v,ch) = ich?(_,v'):wrange(id) -> VARIC(v',ch) [] xch?(_,v'):wrange(id) -> VARXC(v',ch) [] step -> VARIW(v) VARII(v) = calculate -> VARNC(v,false) VARIC(v,ch) = step -> VARIW(v) [] ich?(_,_):wrange(id) -> varerror -> STOP -- varerror on 2 writes within small step [] member(id,xvars) & xch?(_,v'):wrange(id) -> VARIC(v',ch) [] member(id,changes) & readch.(id,ch) -> VARIC(v,ch) -- one internal change made so a second one would be an error RdVAR(v) = read.(id,v) -> RdVAR(v) [] xch?(_,v'):xrange(id) -> RdVAR(v') [] iwrite?(_,v'):wrange(id) -> RdVAR(v') within (tock -> VARXI(v,if member(id,changes) then v else 0)) [|union({|iwrite.p | p <- wrange(id)|},{|xch.p | p <- irange(id)|})|] RdVAR(v) -- purpose of the parallel composition is to allow a process to read the -- value of this variable from the previous step even after it has -- been changed via ich on this one. -- There is no such problem with reading the ch(v) objects, so these -- are handled in the main variable process. -- Defining signal processes CSV(id)= let ERCXI(v) = calculate -> ERCNC(0) ERCNC(v) = step -> iwrite.(id,v) -> ERCII(0) [] tock -> ERCXI(0) [] ich?(_,v'):boolch(id) -> if v'==1 then ERCNC(v') else ERROR ERROR = varerror -> STOP -- allow multiple assertions of this event signal because always to TRUE ERCII(v) = calculate -> ERCNC(v) -- ready for internal changes RdERC(v) = read.(id,v) -> RdERC(v) [] iwrite?(_,v'):boolch(id) -> RdERC(v') [] tock -> RdERC(0) within (tock -> ERCXI(0)) [|{|iwrite.(id,p),tock | p <- nbool|}|] RdERC(0) boolch(id) = {(id,x) | x <- nbool} --^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ VARS = ([|{step,calculate,tock}|] (id,v,r):union(Inputs,Variables) @ VAR(id,r,v,false)) Signal_Procs = ([|{step,calculate,tock}|] id:SigChans @ CSV(id)) VARSandSIGNALS = if SigChans == {} then VARS else VARS [|{step,calculate,tock}|] Signal_Procs --^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -- We allow timers which are set up on the entry to a state, or which are -- addressed by their own identifier names. A timer is initialised to -- 0, and is then incremented by one each tock until a limit is reached, -- customised to the largest value that the value of the timer will ever -- be compared with in the timer(n,e) statement. (To use an e which gives -- a larger value will generate a run-time error.) Timer(l) = timer_on.l -> Timer_Running(l,0) [] timer_read.l.0 -> Timer(l) [] timer_cancel.l -> Timer(l) [] tock -> Timer(l) [] step -> Timer(l) Timer_Running(l,n) = tock -> (if n==tlimit(l) then Timer_Running(l,n) else Timer_Running(l,n+1)) [] step -> Timer_Running(l,n) [] timer_read.l.n -> Timer_Running(l,n) [] timer_cancel.l -> Timer(l) [] timer_on.l -> Timer_Running(l,0) -- The following routine is used when a chart leaves one state and -- enters another: this might result in several state-based timers -- being stopped and several others being started. Timer_Man(sc,v,n) = let Starting(X) = if X != {} then timer_on?x:X -> Starting(diff(X,{x})) else SKIP Stopping(X) = if X!= {} then timer_cancel?x:X -> Stopping(diff(X,{x})) else SKIP within Stopping(Timers_off_by(sc,v));Starting(Timers_on_by(sc,n)) datatype Timer_Names' = dummy_timer | En.Timed_Nodes | Tr.Named_Timers -- The user file should contain definitions of the two sets on the right: -- respectively sets of timers attached to nodes and ones addressed by their -- own names. Each timer should be paired by a limit: defined to be the -- greatest number its value should ever be compared with. Timed_Nodes = {x | (x,_) <- Timed_Nodes_Lim} Named_Timers = {x | (x,_) <- Named_Timers_Lim} All_Timers_Lim = union({(En.x,l) | (x,l) <- Timed_Nodes_Lim}, {(Tr.id,l) | (id,l) <- Named_Timers_Lim}) All_Timers = {x | (x,_) <- All_Timers_Lim} tlimit(t) = pick({l | (x,l) <- All_Timers_Lim, x==t}) Timer_Names = if All_Timers=={} then {dummy_timer} else All_Timers Timer_Procs = [|{|step,tock|}|] t <- All_Timers @ Timer(t) Timer_Limit = if All_Timers_Lim=={} then 0 else pick({l | (_,l) <- All_Timers_Lim, {l' | (_,l') <- All_Timers_Lim, l' > l}=={}}) channel timer_on:Timer_Names channel timer_cancel:Timer_Names channel timer_read:Timer_Names.{0..Timer_Limit} nonempty(X) = if X=={} then {{}} else {{x} | x <- X} VARSandTIMERS = if All_Timers == {} then VARSandSIGNALS else VARS[|{|step,tock|}|]Timer_Procs --************************************************************************************** -- The following are the states that are turned on in a given chart when a specified one -- at the top level becomes active: Dir_on(SCTree.lab._.scps,n) = union({(lab,n)}, Union({Dir_on(sc,stst(sc)) | (n',sc) <- scps, n'==n})) stst(SCTree.l._._) = let (_,_,s) = sm(l) within s -- Which allows us to determine which timers are to be turned on when a state is entered Timers_on_by(sc,n) = {En.x | x <- inter(Timed_Nodes,Dir_on(sc,n))} -- Likewise for turning off Dir_off(SCTree.lab._.scps,n) = union({(lab,n)}, Union({Dir_off(SCTree.l'.a.ss,m) | (n', SCTree.l'.a.ss) <- scps, n==n',m<-sls(l')})) Timers_off_by(sc,n) = {En.x | x <- inter(Timed_Nodes,Dir_off(sc,n))} --************************************************************************************ -- Useful extra definitions lift(label) = SCTree.label.{}.{} -- lifts a graph to a single-leaf tree Box_g(name) = let ns = {(0,<>,<>)} within (ns,name,0,{}) -- Gives a null graph into which several can be put for pure parallel -- (within state 0) --*********************************************************************************** {- Abstracting timers Often, in examples like the burglar alarm, we might want very large values of one or more timers, which would create a problem with state spaces. On the other hand, most aspects of correctness are unlikely to depend on the precise limits of these (and perhaps other) timers, and we might feel limited by a proof of a property which only holds for one specific value of a timer limit. Perhaps the most obvious way of attacking this problem is to abstract the constants which are used as the usual tiemr limits into nondeterministic values. While abstracting constants seems like a valuable technique, we cannot use this as the only methods of abstracting timer limits so as to include arbitrarily large limits since we would still be running a timer, now with an unbounded state space. The technique we therefore propose is to propose a limit on timers such that the timer stops counting at that point (as implemented in the previous version) but where, once it has reached that value, it now represents any value at least as great. Therefore an attempt to compare a larger integer against this timer will not produce an error (as before) but rather a nondeterministic result. We can specify this in a script by defining subsets of the two classes of timers that are to be treated nondeterministically: ND_TN and ND_NT -} ND_TS = union({En.x | x <- ND_TN},{ Tr.x | x <- ND_NT}) nondetT(t) = member(t,ND_TS) {- There is no need to change the timer processes themselves. We need, however, to modify the expression evaluation mechanisms in the Machine function to allow for nondeterministic results of boolean tests. We can see two ways of doing this: to introduce branching (which must be protected against the effects of chase) at the point where nondeterminism is introduced or introducing extra values into types to represent a nondeterministic outcome. The latter is unattractive, particularly in the context where nondeterminism has spread to the integer type (through conditionals etc) because of the increased alphabet size and process state space size. Therefore we will go for the latter. A timer result which is nondeterministic will therefore generate a branch in the program, in one branch the timer() being true and in the other it being false. In implementing this we are considerably helped by the fact that Machine is programmed to communicate with the Timer processes before evaluation, rather than having the evaluation being a pure expression evaluation. It is easy to introduce a branch at this point in the program, and protecting it by using the event nc_tau (no chase tau) to give the branching effect. The best way to do it in the particular circumstance of the timer is to say that in the case of a nd timer, if the timer's maximum value is returned when it is interrogated, then the value stored is either that value or plus one (branching) and the expression for comparison with the timer is capped at the maximum. Thus a value less than this limit will never be reckoned greater than the timer, but a comparison at or above the maximum will produce different answers in the two branches. -} --********************************************************************* -- Support for liveness checks {- We might want to prove that (for example) it is impossible to have an infinite sequence of states in which a particular output variable takes value 1, irrespective of what inputs occur. The obvious thing to do here is to hide everything apart from the event outp.(x,1) and prove there is no divergence. But to do this (noting that outputs do not change state and are always optional) and having an infinity of inputs within a single tock. What we therefore do is have a version of SYSTEM in which no more than card({Inputs}) inputs can occur on any tock and in which all outputs other than ones from a specific collection of (variable, value) pairs are forbidden: -} LiveCheckSYS(Hierarchy,SeenInps,SeenOutps) = let pendingtock(X) = if X=={} then tock -> pendingtock(SeenOutps) else outp?(x,_):Union({wrange(x) | x <- X}) -> pendingtock(diff(X,{x})) within ((SYSTEM(Hierarchy)[|{|xch,tock|}|]LimitInputs(card(Inputs))) [|{|tock,outp|}|] pendingtock({})) \diff(Events,union( {|outp.y | x <- SeenOutps,y <- wrange(x)|}, {|xch.y | x <- SeenInps,y <- wrange(x)|} )) LimitInputs(n) = let LI(k) = tock -> LI(n) [] k>0 & xch?_ -> LI(k-1) within LI(n) setchannel(id) = (id,TRUE)