\documentclass{article}

\usepackage[margin=20mm,bmargin=30mm,a4paper]{geometry}
\usepackage{circus}
\usepackage{stateflow}
%\newenvironment{circusaction*}{\begin{circusaction}}{\end{circusaction}}

%\AddToShipoutPicture{\AtTextLowerLeft{\framebox(\LenToUnit{\textwidth},\LenToUnit{\textheight}){}}}

\begin{document}

\begin{zsection}
  \SECTION stateflow\_toolkit \parents circus\_toolkit, basic\_toolkit
\end{zsection}

%%Zinword \aand aand
%%Zinword \aor aor
%%Zpreword \anot anot

%%Zinword \band band
%%Zinword \bor bor
%%Zinword \bxor bxor
%%Zpreword \bnot bnot

%%Zinword \lshift lshift
%%Zinword \rshift rshift

%%Zinword \alt alt
%%Zinword \agt agt
%%Zinword \aleq aleq
%%Zinword \ageq ageq
%%Zinword \aeq aeq
%%Zinword \aneq aneq

\begin{zed}
\function 40 \leftassoc (\varg \aand \varg)\\
\function 40 \leftassoc (\varg \aor \varg)\\
\function (\anot \varg)\\
\function 40 \leftassoc (\varg \band \varg)\\
\function 40 \leftassoc (\varg \bor \varg)\\
\function 40 \leftassoc (\varg \bxor \varg)\\
\function (\bnot \varg)\\
\function 40 \leftassoc (\varg \lshift \varg)\\
\function 40 \leftassoc (\varg \rshift \varg)\\
\function 40 \leftassoc (\varg \alt \varg)\\
\function 40 \leftassoc (\varg \agt \varg)\\
\function 40 \leftassoc (\varg \aleq \varg)\\
\function 40 \leftassoc (\varg \ageq \varg)\\
\function 40 \leftassoc (\varg \aeq \varg)\\
\function 40 \leftassoc (\varg \aneq \varg)\\
\end{zed}

\begin{axdef}
\varg \aand \varg: \arithmos \cross \arithmos \fun \arithmos\\
\varg \aor \varg: \arithmos \cross \arithmos \fun \arithmos\\
\anot \varg: \arithmos \fun \arithmos\\
\varg \band \varg: \arithmos \cross \arithmos \fun \arithmos\\
\varg \bor \varg: \arithmos \cross \arithmos \fun \arithmos\\
\varg \bxor \varg: \arithmos \cross \arithmos \fun \arithmos\\
\bnot \varg:\arithmos \fun \arithmos\\
\varg \lshift \varg: \arithmos \cross \arithmos \fun \arithmos\\
\varg \rshift \varg: \arithmos \cross \arithmos \fun \arithmos\\
\varg \alt \varg: \arithmos \cross \arithmos \fun \arithmos\\
\varg \agt \varg: \arithmos \cross \arithmos \fun \arithmos\\
\varg \aleq \varg: \arithmos \cross \arithmos \fun \arithmos\\
\varg \ageq \varg: \arithmos \cross \arithmos \fun \arithmos\\
\varg \aeq \varg: \arithmos \cross \arithmos \fun \arithmos\\
\varg \aneq \varg: \arithmos \cross \arithmos \fun \arithmos\\
\where
\forall x,y: \arithmos @ x \aand y = \anot (\anot x \aor \anot y)\\
\forall x,y: \arithmos @ x \band y = \bnot (\bnot x \bor \bnot y)\\
\forall x,y: \arithmos @ x \bxor y = (x \band \bnot y) \bor (\bnot x \band y)
\end{axdef}

\begin{zed}
DECOMPOSITION ::= SET | CLUSTER \\
TYPE ::= AND | OR | CHART\\
DESTINATION ::= STATE | JUNCTION\\
[SID, TID, JID,EVENT]\\
NID ::= snode\ldata SID\rdata | jnode\ldata JID\rdata\\
%False == [ | false]\\
%True == [ | true]\\
%Boolean == \{False, True\}
SFBOOL == \num
\end{zed}


%STATE=(identifier,default,inner,outer,parent,left,right,substates,decomposition,type,history)
\begin{schema}{State}
identifier: SID\\
default, inner, outer: TID\\
parent, left, right: SID\\
substates: \seq SID\\
decomposition: DECOMPOSITION\\
type: TYPE\\
history: \boolean
\end{schema}

%JUNCTION=(identifier,transition,history,parent)
\begin{schema}{Junction}
identifier: JID\\
transition: TID\\
parent: SID\\
history: \boolean
\end{schema}

%TRANSITION=(identifier,source,stype,destination,dtype,next,parent)
\begin{schema}{Transition}
identifier: TID\\
source, destination: NID\\
next: TID\\
parent: SID
\end{schema}

\begin{axdef}
nullstate: State\\
nulljunction: Junction\\
nulltransition: Transition
\where
nullstate.history = \false\\
nulljunction.history = \false
\end{axdef}

\begin{schema}{StateflowChart}
identifier: SID\\
states: SID \ffun State\\
transitions: TID \ffun Transition\\
junctions: JID \ffun Junction
\where
nullstate \notin \ran states\\
nulltransition \notin \ran transitions\\
nulljunction \notin \ran junctions\\
\#\{s: \ran states | s.type = CHART\} = 1\\
(states(identifier)).type = CHART\\
\forall n: SID | n \in \dom states @ (states(n)).identifier = n\\
\forall n: JID | n \in \dom junctions @ (junctions(n)).identifier = n\\
\forall n: TID | n \in \dom transitions @ (transitions(n)).identifier = n
\end{schema}

\begin{axdef}
has\_active\_substate: \power ((SID \pfun \boolean) \cross State)
\where
\forall state\_status: SID \pfun \boolean; s: State @\\
(state\_status,s) \in has\_active\_substate \iff (\exists ss: \ran(s.substates) @ state\_status(ss) = \true)
\end{axdef}

\begin{axdef}
parent: State \rel State
\where
\forall s_1, s_2: State @ parent(s_1) = s_2 \iff s_1.parent = s_2.identifier
\end{axdef}

\begin{axdef}
ancestors: State \fun \power State
\where
\forall s: State @ ancestors(s) = (parent\plus)\limg\{s\}\rimg \setminus \{nullstate\}
\end{axdef}

\begin{axdef}
la: (State \cross State) \fun State
\where
\forall s_1, s_2: State @ la(s_1,s_2) = \mu x: (ancestors(s_1) \cap ancestors(s_2)) |\\
\t1 (\forall y: (ancestors(s_1) \cap ancestors(s_2)) @ x = y \lor y \in ancestors(x)) @ x
\end{axdef}

%\begin{zed}
%rw ::= read | write
%\end{zed}

\begin{circus}
\circchannel read\_inputs, write\_outputs\\
\circchannel input\_event: \seq \boolean\\
\circchannel events: \seq EVENT\\
\circchannel local\_event: EVENT \cross State\\

%Note the second parameters of these channels is used to communicate the origin of a transition path, in order
%to check the conditions of early return logic. Therefore, it is only relevant for executeconditionaction, and
%executetransitionaction. However, we can use it to communicate the source of the transition path that led
%to a state being exited, and use this information to interrupt the appropriate part of the chart. The modifications
%necessary would be to pass as a parameters the source of the transition path to the ExitState action (as well
%as to ExitStates, and use this parameter as the second value communicated through executeexitactions.
%Then, if the early return logic conditions for exit actions occur, we interrupt the executeTransition through
%a communication over i\_ExecuteTransition.source.

\circchannel executeentryaction,executeexitaction: SID\\
\circchannel executeduringaction: SID \cross EVENT\\
\circchannel executeconditionaction,executetransitionaction: TID\\
% I need to check if a condition can have a temporal expression. Chances are it can.

\circchannel evaluatecondition: TID\cross \boolean\\
\circchannel checktrigger: TID\cross EVENT\\
\circchannel result: TID \cross EVENT \cross \boolean\\

\circchannel activate, deactivate: SID\\

\circchannel junction: JID \cross Junction\\
\circchannel transition: TID \cross Transition\\
\circchannel state: SID \cross State\\
\circchannel chart: State\\
\circchannel status: SID\cross\boolean\\
\circchannel history: SID\cross SID\\
%\circchannel event: EVENT\\

\circchannel end\_local\_execution, end\_action\\
\circchannel interrupt: \boolean\\

\circchannel end\_cycle\\

%\circchannel error\\ % Now, instead of flagging error, the process deadlocks.

\circchannelset interface == \lchanset executeentryaction,executeduringaction,executeexitaction,\\
\t1 executeconditionaction,executetransitionaction,evaluatecondition, checktrigger, result,\\
\t1 junction, transition,state,chart,status,history,activate,deactivate, read\_inputs, write\_outputs,\\
\t1 end\_local\_execution, end\_action, local\_event, interrupt, events \rchanset\\

\end{circus}

\begin{circus}
\circchannel stsuccess, stfail\\
\circchannelset statetransition == \lchanset  stsuccess, stfail \rchanset
\end{circus}

\begin{axdef}
and,or: \boolean \cross \boolean \fun \boolean\\
not:\boolean \fun \boolean
\where
or(\false,\false) = and(\false,\false) = and(\true,\false) = and(\false,\true) = \false\\
and(\true,\true) = or(\true,\true) = or(\true,\false) = or(\false,\true) = \true\\
not(\true) = \false\\
not(\false) = \true
\end{axdef}

\begin{circus}
\circprocess Simulator \circdef \circbegin
\end{circus}

\begin{circusaction}
entryActionCheck \circdef \circval sid: SID; \circvres b: \boolean \circspot status!sid?active \then b:= not(active)\\
duringActionCheck \circdef \circval sid: SID; \circvres b: \boolean \circspot entryActionCheck(sid,b)\\
exitActionCheck \circdef \circval sid: SID; \circvres b: \boolean \circspot entryActionCheck(sid,b)\\
conditionActionCheck \circdef \circval sid: SID; \circvres b: \boolean \circspot entryActionCheck(sid,b)\\

transitionActionCheck \circdef \circval sid: SID; \circvres b: \boolean \circspot entryActionCheck(sid,b)\circseq
\circvar ss: \seq SID \circspot\\\t1
\circblockbegin
state!sid?s \then ss:=s.substates \circseq\\
\circmu X \circspot \circblockbegin
\circif ss = \langle\rangle \circthen \Skip\\
\circelse~~ss \neq \langle\rangle \circthen status!(head~ss)?active \then (b:=or(b,active) \circseq ss:=tail~ss \circseq X)\\
\circfi
\circblockend
\circblockend\\

exitStatesCheck \circdef \circval sid: SID; \circvres b: \boolean \circspot transitionActionCheck(sid,b)\\

enterState1Check \circdef \circval sid: SID; \circvres b: \boolean \circspot state!sid?s \then entryActionCheck(s.parent,b)\\
enterState2Check \circdef \circval sid: SID; \circvres b: \boolean \circspot state!sid?s \then\\\t1
\circblockbegin
\circif s.left = nullstate.identifier \circthen b:=\false\\
\circelse~~s.left \neq nullstate.identifier \circthen entryActionCheck(s.left,b)\\
\circfi
\circblockend
\end{circusaction}

\begin{circusaction}
%enterState14Check \circdef \circval sid: SID; \circvres b: \boolean \circspot state!sid?s \then status!(s.parent)?a1 \then status!sid?a3 \then\\\t1
%\circblockbegin
%\circif s.left = nullstate.identifier \circthen b:=not(and(a1,a3))\\
%\circelse~~s.left \neq nullstate.identifier \circthen status!(s.left)?a2 \then b:=not(and(and(a1,a2),a3))\\
%\circfi
%\circblockend\\

enterState15Check \circdef \circval sid: SID; \circvres b: \boolean \circspot entryActionCheck(sid,b)\\

%enterStateCheck \circdef \circval sid: SID; \circvres b: \boolean \circspot entryActionCheck(sid,b)\\
\end{circusaction}

%begin executetransition
\begin{circusaction}
ExecuteTransition \circdef \circval tid: TID; \circval path: \seq TID; \circval source: State; \circval ce: EVENT; \circvres success: \boolean \circspot\\
\circblockbegin
\circif tid = nulltransition.identifier \circthen\\
\circblockbegin
\circif path = \emptyset \circthen success:=\false\\
\circelse~~path \neq \emptyset \circthen
\circblockbegin
transition!(last~path)?lt \then \\
ExecuteTransition(lt.next,(front~path),source,ce,success)
\circblockend\\
\circfi
\circblockend\\
\circelse~~tid \neq nulltransition.identifier \circthen\\
CheckValidity(tid,path,source,ce,success)\\
\circfi
\circblockend
\end{circusaction}
%end executetransition

%begin checkvalidity
\begin{circusaction}
CheckValidity \circdef \circval tid: TID; \circval path: \seq TID; \circval source: State; \circval ce: EVENT; \circvres success: \boolean \circspot\\\t1
checktrigger!tid!ce\then result!tid!ce?e \then evaluatecondition!tid?c \then\\
\t1 \circblockbegin
\circif e = \true \land c = \true \circthen\\ \circblockbegin executeconditionaction!tid \then LocalEventCondition(source.identifier) \circseq\\
\circvar b: \boolean \circspot \circblockbegin conditionActionCheck(source.identifier,b)\circseq\\
\circblockbegin
\circif b = \true \circthen success:=\true\\
\circelse~~b = \false \circthen Proceed(tid,path\cat\langle tid\rangle,source,ce,success)\\
\circfi
\circblockend
\circblockend
\circblockend\\
\circelse~~\lnot( e = \true \land c = \true) \circthen \circblockbegin transition!tid?t \then\\
ExecuteTransition(t.next,path,source,ce,success)\circblockend\\
\circfi
\circblockend
\end{circusaction}
%end checkvalidity

%begin proceed
\begin{circusaction}
Proceed \circdef \circval tid: TID; \circval path: \seq TID; \circval source: State; \circval ce: EVENT; \circvres success: \boolean \circspot\\
transition!tid?t \then \\
\circblockbegin \circif t.destination \in \ran snode \circthen \circblockbegin
state!((snode\inv)~t.destination)?dest \then\\ proceedToState(source,dest,path,ce,success)\circblockend\\
\circelse~~t.destination \in \ran jnode \circthen proceedToJunction(tid,path,source,ce,success)\\
\circfi
\circblockend
\end{circusaction}
%end proceed

%begin proceedtostate
\begin{circusaction}
proceedToState \circdef \circval src, dest: State; \circval path: \seq TID; \circval ce: EVENT; \circvres success:\boolean \circspot\\
\circblockbegin
ExitStates((la(src,dest)).substates,ce)\circseq\\
\circvar b: \boolean \circspot \circblockbegin
exitStatesCheck((la(src,dest)).identifier,b)\circseq\\
\circblockbegin \circif b=\true \circthen \Skip\\
\circelse~~b=\false \circthen \circblockbegin
executePath(path,src,dest,ce)\circseq\\
transitionActionCheck((la(src,dest)).identifier,b)\circseq\\
\circblockbegin
\circif b=\true \circthen \Skip\\
\circelse~~b=\false \circthen EnterState(dest,la(src,dest),ce)\\
\circfi
\circblockend
\circblockend\\
\circfi
\circblockend
\circblockend\circseq\\
success:=\true
\circblockend
\end{circusaction}
%end proceedtostate

%begin executepath
\begin{circusaction}
executePath \circdef path: \seq TID; src,dest: State; ce: EVENT \circspot\\
\circblockbegin
\circif \# path = 0 \circthen \Skip\\
\circelse~~\# path > 0 \circthen \circblockbegin executetransitionaction!(head~path) \then\\
 LocalEventTransition((la(src,dest)).identifier) \circseq\\
\circvar b: \boolean \circspot \circblockbegin
transitionActionCheck((la(src,dest)).identifier,b) \circseq\\
\circblockbegin
\circif b=\true \circthen \Skip\\
\circelse~~b=\false \circthen executePath(tail~path,src,dest,ce)\\
\circfi
\circblockend
\circblockend
\circblockend\\
\circfi
\circblockend
\end{circusaction}
%end executepath

%begin proceedtojunction
\begin{circusaction}
proceedToJunction \circdef \circval tid: TID; \circval path: \seq TID; \circval source: State; \circval ce: EVENT; \circvres success: \boolean \circspot\\\t1
\circblockbegin
transition!tid?t \then junction!((jnode\inv)~t.destination)?dj \then\\\t1
\circblockbegin
\circif dj.history = \false \circthen executeJunction(dj,path,source,ce,success)\\
\circelse~~dj.history = \true \circthen history!(dj.parent)?lsid \then\\\t1
 \circblockbegin
\circif lsid = nullstate.identifier \circthen\\\t1 \circblockbegin state!(dj.parent)?s \then\\  ExecuteDefaultTransition(s,s,ce)\circseq success:=\true\circblockend\\
\circelse~~lsid \neq nullstate.identifier \circthen\\\t1 \circblockbegin state!lsid?ls \then\\ proceedToState(source,ls,path,ce,success)\circblockend\\
\circfi
\circblockend\\
\circfi
\circblockend
\circblockend
\end{circusaction}
%end proceedtojunction

%begin executejunction
\begin{circusaction}
executeJunction \circdef \circval j: Junction; \circval path: \seq TID; \circval source: State; \circval ce: EVENT; \circvres success:\boolean \circspot\\
\t1 \circblockbegin \circif j.transition = nulltransition.identifier \circthen\\
\t1 success:=\false\\
\circelse~~j.transition \neq nulltransition.identifier \circthen\\
\t1 ExecuteTransition(j.transition, path, source,ce,success)\\
\circfi\circblockend
\end{circusaction}
%end executejunction

If the default transitions fail, the model deadlocks.

%begin executedefaulttransition
\begin{circusaction}
ExecuteDefaultTransition ~~\circdef~~ s, tpp:State; ce: EVENT \circspot\\\t1
\circblockbegin
\circif s.default \neq nulltransition.identifier \circthen\\
\t1 \circblockbegin
\circvar success:\boolean \circspot ExecuteTransition(s.default,\langle \rangle, s,ce,success)\circseq\\
(\circif success = \true \circthen \Skip \circelse~~success = \false \circthen \Stop \circfi)
\circblockend\\
\circelse~~s.default = nulltransition.identifier \circthen \\\t1
\circblockbegin
\circif \# s.substates = 0 \circthen \Skip\\
\circelse~~\# s.substates = 1 \circthen \circblockbegin state!(head~s.substates)?saux \then\\
EnterState(saux,tpp,ce)\circblockend\\
\circelse~~\# s.substates > 1 \circthen \Stop\\
\circfi
\circblockend\\
\circfi
\circblockend
\end{circusaction}
%end defaulttransition


%begin enterstate
\begin{circusaction}
EnterState \circdef s, tpp: State; ce: EVENT \circspot EnterState16(s,tpp,ce)
\end{circusaction}
%end enterstate

\begin{circusaction}
EnterState24 \circdef s,tpp:State; ce: EVENT \circspot EnterState2(s,tpp,ce) \circseq\\
\circvar b:\boolean \circspot enterState2Check(s.identifier,b)\circseq\\
\circblockbegin
\circif b=\true \circthen \Skip\\
\circelse~~b=\false \circthen EnterState34(s,tpp,ce)\\
\circfi
\circblockend
\end{circusaction}

\begin{circusaction}
EnterState14 ~~\circdef~~ s,tpp: State; ce: EVENT \circspot EnterState1(s,tpp,ce)\circseq\\
\circvar b:\boolean \circspot enterState1Check(s.identifier,b)\circseq\\
\circblockbegin
\circif b=\true \circthen \Skip\\
\circelse~~b=\false \circthen EnterState24(s,tpp,ce)\\
\circfi
\circblockend
\end{circusaction}

\begin{circusaction}
EnterState35 \circdef s,tpp:State; ce: EVENT \circspot EnterState34(s,tpp,ce) \circseq\\
status!(s.identifier)?active \then
\circblockbegin
\circif active=\true \circthen EnterState5(s,tpp,ce)\\
\circelse~~active=\false \circthen \Skip\\
\circfi
\circblockend
\end{circusaction}

\begin{circusaction}
EnterState25 \circdef s,tpp:State; ce: EVENT \circspot EnterState2(s,tpp,ce) \circseq\\
\circvar b:\boolean \circspot enterState2Check(s.identifier,b)\circseq\\
\circblockbegin
\circif b=\true \circthen \Skip\\
\circelse~~b=\false \circthen EnterState35(s,tpp,ce)\\
\circfi
\circblockend
\end{circusaction}

\begin{circusaction}
EnterState15 ~~\circdef~~ s,tpp: State; ce: EVENT \circspot EnterState1(s,tpp,ce)\circseq\\
\circvar b:\boolean \circspot enterState1Check(s.identifier,b)\circseq\\
\circblockbegin
\circif b=\true \circthen \Skip\\
\circelse~~b=\false \circthen EnterState25(s,tpp,ce)\\
\circfi
\circblockend
\end{circusaction}

\begin{circusaction}
EnterState56 \circdef s,tpp:State; ce: EVENT \circspot EnterState5(s,tpp,ce) \circseq\\
status!(s.identifier)?active \then
\circblockbegin
\circif active=\true \circthen EnterState6(s,tpp,ce)\\
\circelse~~active=\false \circthen \Skip\\
\circfi
\circblockend
\end{circusaction}

\begin{circusaction}
EnterState36 \circdef s,tpp:State; ce: EVENT \circspot EnterState34(s,tpp,ce) \circseq\\
status!(s.identifier)?active \then
\circblockbegin
\circif active=\true \circthen EnterState56(s,tpp,ce)\\
\circelse~~active=\false \circthen \Skip\\
\circfi
\circblockend
\end{circusaction}

\begin{circusaction}
EnterState26 \circdef s,tpp:State; ce: EVENT \circspot EnterState2(s,tpp,ce) \circseq\\
\circvar b:\boolean \circspot enterState2Check(s.identifier,b)\circseq\\
\circblockbegin
\circif b=\true \circthen \Skip\\
\circelse~~b=\false \circthen EnterState36(s,tpp,ce)\\
\circfi
\circblockend
\end{circusaction}

\begin{circusaction}
EnterState16 ~~\circdef~~ s,tpp: State; ce: EVENT \circspot EnterState1(s,tpp,ce)\circseq\\
\circvar b:\boolean \circspot enterState1Check(s.identifier,b)\circseq\\
\circblockbegin
\circif b=\true \circthen \Skip\\
\circelse~~b=\false \circthen EnterState26(s,tpp,ce)\\
\circfi
\circblockend
\end{circusaction}

%begin enterstate1
\begin{circusaction}
EnterState1 ~~\circdef~~ s,tpp:State; ce: EVENT \circspot
status!(s.parent)?active \then\\\t1 \circblockbegin
\circif active = \false \circthen\\\t1
state!(s.parent)?p \then EnterState14(p,tpp,ce)\\
\circelse~~active = \true \circthen \Skip\\
\circfi
\circblockend
\end{circusaction}
%end enterstate1

After $EnterState1$, the parent must be active. If it is not, early return logic occurs.

%begin enterstate2
\begin{circusaction}
 EnterState2 ~~\circdef~~ s,tpp:State; ce: EVENT \circspot\\
 \circblockbegin
 \circif s.type = AND \circthen\\ \circblockbegin
 \circif s.left \neq nullstate.identifier \circthen status!(s.left)?active \then\\
\circblockbegin
\circif active = \true \circthen \Skip\\
\circelse~~active \neq \true \circthen  state!(s.left)?ls \then EnterState15(ls,tpp,ce)\\
\circfi
\circblockend\\
 \circelse~~s.left = nullstate.identifier\circthen \Skip\\
 \circfi
 \circblockend\\
 \circelse~~s.type \neq AND \circthen \Skip\\
 \circfi
 \circblockend
\end{circusaction}
%end enterstate2

After $EnterState2$, the left sibling must be active. If it is not, early return logic occurs.

%begin enterstate3
\begin{circusaction}
 EnterState3 ~~\circdef~~ s,tpp:State; ce: EVENT \circspot activate!(s.identifier) \then \Skip
\end{circusaction}
%end enterstate3

%begin enterstate4
\begin{circusaction}
 EnterState4 ~~\circdef~~ s,tpp:State; ce: EVENT \circspot\\\t1
 executeentryaction!(s.identifier) \then LocalEventEntry(s.identifier)
\end{circusaction}
%end enterstate4

\begin{circusaction}
EnterState34 \circdef s, tpp: State; ce: EVENT \circspot\\ status.(s.identifier)?active \then \circblockbegin
\circif active = \true \circthen \Skip\\
\circelse~~active = \false \circthen EnterState3(s,tpp,ce)\circseq EnterState4(s,tpp,ce)\\
\circfi
\circblockend
\end{circusaction}

After $EnterState34$, the state must be active. If it is not, early return logic occurs.


%begin enterstate5
\begin{circusaction}
 EnterState5 ~~\circdef~~ s,tpp:State; ce: EVENT \circspot\\\t1
 EnterState5a(s,tpp,ce) \circseq EnterState5b(s,tpp,ce)
\end{circusaction}
%end enterstate5

$EnterState5a$ might execute parallel substates if their parent has a default transition. If it does, $EnterState5b$ will try to enter in the same states, but since they are already
active, they will not be re-entered. I believe that this steps could be refined to avoid this redundant attempt to enter the substates, but this is the form the manual describes the entering of substates.

%begin enterstate5a
\begin{circusaction}
EnterState5a ~~\circdef~~ s,tpp:State; ce: EVENT \circspot\\
\circblockbegin
\circif s.history = \true \circthen history!(s.identifier)?lsid \then\\\t1
\circblockbegin
\circif lsid \neq nullstate.identifier \circthen  state!lsid?ls \then EnterState15(ls,tpp,ce)\\
\circelse~~lsid = nullstate.identifier \circthen ExecuteDefaultTransition(s,tpp,ce)\\
\circfi
\circblockend\\
\circelse~~s.history = \false \circthen
\circblockbegin
\circif s.default \neq nulltransition.identifier \circthen ExecuteDefaultTransition(s,tpp,ce)\\
\circelse s.default = nulltransition.identifier \circthen \Skip\\
\circfi
\circblockend\\
\circfi
\circblockend
\end{circusaction}
%end enterstate5a

%begin enterstate5b
\begin{circusaction}
EnterState5b ~~\circdef~~ s,tpp:State; ce: EVENT \circspot\\
\circblockbegin
\circif s.decomposition = SET \land s.default = nulltransition.identifier\circthen  EnterStates15(s.substates,tpp,ce)\\
\circelse~~s.decomposition \neq SET \lor s.default \neq nulltransition.identifier \circthen \Skip\\
\circfi
\circblockend
\end{circusaction}
%end enterstate5b

After $EnterState5$, the state must still be active. If it is not, early return logic occurs.

%begin enterstates15
\begin{circusaction}
EnterStates15 ~~\circdef~~ ss:\seq SID; tpp: State; ce: EVENT \circspot\\
\circblockbegin
\circif \# ss = 0 \circthen \Skip\\
\circelse~~\# ss > 0 \circthen status!(head~ss)?active \then\\
\circblockbegin
\circif active = \false \circthen state!(head~ss)?first \then EnterState15(first,tpp,ce)\\
\circelse~~active = \true \circthen \Skip\\
\circfi
\circblockend
\circseq\\
\circvar b:\boolean \circspot \circblockbegin
enterState15Check(head~ss,b) \circseq\\
\circblockbegin
\circif b=\true \circthen \Skip\\
\circelse~~b=\false \circthen EnterStates15(tail~ss,tpp,ce)\\
\circfi
\circblockend
\circblockend\\
\circfi
\circblockend
\end{circusaction}
%end enterstates15

%begin enterstate6
\begin{circusaction}
 EnterState6 ~~\circdef~~ s,tpp:State; ce: EVENT \circspot\\\t1
\circblockbegin
\circif s.type = AND \land s.right \neq nullstate.identifier \circthen state!(s.right)?rs \then EnterState(rs,tpp,ce)\\
\circelse~~s.type \neq AND \lor s.right = nullstate.identifier \circthen EnterState7(s,tpp,ce)\\
\circfi
\circblockend
\end{circusaction}
%end enterstate6

%begin enterstate7
\begin{circusaction}
 EnterState7 ~~\circdef~~ s,tpp:State; ce: EVENT \circspot\\
\circblockbegin
	\circif s.type \neq CHART \circthen state!(s.parent)?p \then\\\t1
	\circblockbegin
		\circif tpp \neq p \circthen EnterState6(p,tpp,ce)\\
		\circelse~~tpp = p \circthen \Skip\\
		\circfi
	\circblockend\\
	\circelse~~s.type = CHART \circthen \Skip\\
	\circfi
\circblockend
\end{circusaction}
%end enterstate7

%begin executestate
\begin{circusaction}
ExecuteState ~~\circdef~~ s: State; ce: EVENT \circspot\\
\circblockbegin%
\circvar success:\boolean \circspot\\
ExecuteTransition(s.outer,\langle\rangle,s,ce,success)\circseq\\
\circblockbegin
\circif success = \true \circthen \Skip\\
\circelse~~success = \false \circthen \circblockbegin executeduringaction!(s.identifier)!ce \then\\
LocalEventDuring(s.identifier) \circseq\\
\circvar b:\boolean \circspot \circblockbegin
duringActionCheck(s.identifier,b) \circseq\\
\circblockbegin
\circif b=\true \circthen \Skip\\
\circelse~~b=\false \circthen AlternativeExecution(s,ce)\\
\circfi
\circblockend
\circblockend
\circblockend\\
\circfi
\circblockend
\circblockend
\end{circusaction}
%end executestate

%begin alternativeexecution
\begin{circusaction}
AlternativeExecution ~~\circdef~~ s: State; ce: EVENT \circspot\\
\circblockbegin%
\circvar success:\boolean \circspot\\
ExecuteTransition(s.inner,\langle\rangle,s,ce,success)\circseq
\circblockbegin
\circif success = \true \circthen \Skip\\
\circelse success = \false \circthen ExecuteSubstates(s,ce)\\
\circfi
\circblockend
\circblockend
\end{circusaction}
%end alternativeexecution

\begin{circusaction}
ExecuteSubstates ~~\circdef~~ s: State; ce: EVENT \circspot\\\t1
\circblockbegin
\circif s.decomposition = SET \circthen ExecuteParallelStates(s.substates,ce)\\
\circelse~~s.decomposition = CLUSTER \circthen ExecuteSequentialStates(s.substates,ce)\\
\circfi
\circblockend
\end{circusaction}

I don't think I need to check if the early return logic condition is true when executing a sequence of states, because the execution of the states is already guarded by a check on the status of the state (which is the early return logic condition for during actions).

\begin{circusaction}
 ExecuteParallelStates ~~\circdef~~ ss:\seq SID; ce: EVENT \circspot\\\t1
 \circblockbegin
\circif \# ss = 0 \circthen \Skip\\
\circelse~~\# ss > 0 \circthen status!(head~ss)?active \then\\
\circblockbegin
\circif active = \true \circthen state!(head~ss)?first \then ExecuteState(first,ce)\\
\circelse~~active = \false \circthen \Skip\\
\circfi
\circblockend
\circseq\\\t1 ExecuteParallelStates(tail~ss,ce)\\
\circfi
\circblockend
\end{circusaction}

\begin{circusaction}
 ExecuteSequentialStates ~~\circdef~~ ss:\seq SID; ce: EVENT \circspot\\\t1
 \circblockbegin
\circif \# ss = 0 \circthen \Skip\\
\circelse~~\# ss > 0 \circthen status!(head~ss)?active \then\\
\circblockbegin
\circif active = \true \circthen state!(head~ss)?first \then ExecuteState(first,ce)\\
\circelse~~active = \false \circthen ExecuteSequentialStates(tail~ss,ce)\\
\circfi
\circblockend\\
\circfi
\circblockend
\end{circusaction}

%begin exitstate
\begin{circusaction}
 ExitState ~~\circdef~~ s:State; ce: EVENT \circspot\\\t1
\circblockbegin
\circblockbegin
\circif s.right \neq nullstate.identifier \circthen status!(s.right)?active \then\\
\circblockbegin
\circif active = \true \circthen state!(s.right)?rs \then ExitState(rs,ce)\\
\circelse~~active = \false \circthen \Skip\\
\circfi
\circblockend\\
\circelse~~s.right = nullstate.identifier \circthen \Skip\\
\circfi
\circblockend
\circseq\\
ExitStates(s.substates,ce)\circseq\\
executeexitaction!(s.identifier) \then LocalEventExit(s.identifier) \circseq\\
\circvar b: \boolean \circspot \circblockbegin
exitActionCheck(s.identifier,b) \circseq\\
\circblockbegin
\circif b=\true \circthen \Skip\\
\circelse~~b=\false \circthen deactivate!(s.identifier) \then \Skip\\
\circfi
\circblockend
\circblockend

\circblockend
\end{circusaction}
%end exitstate

%begin exitstates
\begin{circusaction}
 ExitStates ~~\circdef~~ ss:\seq SID; ce: EVENT \circspot\\\t1
 \circblockbegin
\circif \# ss = 0 \circthen \Skip\\
\circelse~~\# ss > 0 \circthen status!(last~ss)?active \then\\\t1
\circblockbegin
\circif active = \true \circthen state!(last~ss)?l \then ExitState(l,ce)\\
\circelse~~active = \false \circthen \Skip\\
\circfi
\circblockend
\circseq\\\t1 ExitStates(front~ss,ce)\\
\circfi
\circblockend
\end{circusaction}
%end exitstates

%begin executechart
\begin{circusaction}
ExecuteChart ~~\circdef~~ ce: EVENT \circspot\\
chart?c \then status!(c.identifier)?active \then\\\t1
\circblockbegin
\circif active = \true \circthen ExecuteActiveChart(c,ce)\\
\circelse~~active = \false \circthen ExecuteInactiveChart(c,ce)\\
\circfi
\circblockend
\end{circusaction}
%end executechart

If the chart has a default transition, or if it has a sequential decomposition, we execute its default transitions. This action account for the cases where the chart has no default transition, but exactly one
substate, and for the case that it has a default transition and a parallel decomposition. If it has no default transition and it has a parallel decomposition, the the first parallel state is entered (this triggers the entering of all other parallel states in order).

\begin{circusaction}
ExecuteInactiveChart \circdef c: State; ce: EVENT \circspot \\ activate!(c.identifier) \then
\circblockbegin
\circif c.default \neq nulltransition.identifier \lor c.decomposition = CLUSTER \circthen ExecuteDefaultTransition(c,c,ce)\\
\circelse~~c.default = nulltransition.identifier \land c.decomposition = SET \circthen\\
\circblockbegin
\circif c.substates = \langle\rangle \circthen \Skip\\
\circelse~~c.substates \neq \langle\rangle \circthen state!(head(c.substates))?first \then EnterState(first,c,ce)\\
\circfi
\circblockend\\
\circfi
\circblockend
\end{circusaction}

%begin executeactivechart
\begin{circusaction}
 ExecuteActiveChart ~~\circdef~~ c: State; ce: EVENT \circspot \\
\t1
\circblockbegin
\circif c.substates = \emptyset \circthen ExecuteInactiveChart(c,ce)\\
\circelse~~c.substates \neq \emptyset \circthen ExecuteSubstates(c,ce)\\
\circfi
\circblockend
\end{circusaction}
%end executeactivechart

\begin{circusaction}
LocalEventEntry \circdef sid: SID \circspot \circmu X \circspot \\
\circblockbegin
local\_event?e?s \then \circblockbegin
TreatLocalEvent(e,s) \circseq\\
\circvar b: \boolean \circspot \circblockbegin
entryActionCheck(sid,b) \circseq\\
\circblockbegin
\circif b=\true \circthen interrupt.\true \then end\_action \then \Skip\\
\circelse~~b=\false \circthen interrupt.\false \then X\\
\circfi
\circblockend
\circblockend
\circblockend\\
\extchoice\\
end\_action \then \Skip
\circblockend
\end{circusaction}

\begin{circusaction}
LocalEventDuring \circdef sid: SID \circspot \circmu X \circspot \\
\circblockbegin
local\_event?e?s \then \circblockbegin
TreatLocalEvent(e,s) \circseq\\
\circvar b: \boolean \circspot \circblockbegin
duringActionCheck(sid,b) \circseq\\
\circblockbegin
\circif b=\true \circthen interrupt.\true \then end\_action \then \Skip\\
\circelse~~b=\false \circthen interrupt.\false \then X\\
\circfi
\circblockend
\circblockend
\circblockend\\
\extchoice\\
end\_action \then \Skip
\circblockend
\end{circusaction}

\begin{circusaction}
LocalEventExit \circdef sid: SID \circspot \circmu X \circspot \\
\circblockbegin
local\_event?e?s \then \circblockbegin
TreatLocalEvent(e,s) \circseq\\
\circvar b: \boolean \circspot \circblockbegin
exitActionCheck(sid,b) \circseq\\
\circblockbegin
\circif b=\true \circthen interrupt.\true \then end\_action \then \Skip\\
\circelse~~b=\false \circthen interrupt.\false \then X\\
\circfi
\circblockend
\circblockend
\circblockend\\
\extchoice\\
end\_action \then \Skip
\circblockend
\end{circusaction}

\begin{circusaction}
LocalEventCondition \circdef sid: SID \circspot \circmu X \circspot \\
\circblockbegin
local\_event?e?s \then \circblockbegin
TreatLocalEvent(e,s) \circseq\\
\circvar b: \boolean \circspot \circblockbegin
conditionActionCheck(sid,b) \circseq\\
\circblockbegin
\circif b=\true \circthen interrupt.\true \then end\_action \then \Skip\\
\circelse~~b=\false \circthen interrupt.\false \then X\\
\circfi
\circblockend
\circblockend
\circblockend\\
\extchoice\\
end\_action \then \Skip
\circblockend
\end{circusaction}

\begin{circusaction}
LocalEventTransition \circdef sid: SID \circspot \circmu X \circspot \\
\circblockbegin
local\_event?e?s \then \circblockbegin
TreatLocalEvent(e,s) \circseq\\
\circvar b: \boolean \circspot \circblockbegin
transitionActionCheck(sid,b) \circseq\\
\circblockbegin
\circif b=\true \circthen interrupt.\true \then end\_action \then \Skip\\
\circelse~~b=\false \circthen interrupt.\false \then X\\
\circfi
\circblockend
\circblockend
\circblockend\\
\extchoice\\
end\_action \then \Skip
\circblockend
\end{circusaction}

%begin treatlocalevent
\begin{circusaction}
TreatLocalEvent \circdef e: EVENT; s: State \circspot\\
\circblockbegin
\circif s.type = CHART \circthen ExecuteChart(e)\\
\circelse~~s.type \neq CHART \circthen ExecuteState(s,e)\\
\circfi
\circblockend \circseq end\_local\_execution \then \Skip
\end{circusaction}
%end treatlocalevent

\begin{circusaction}
ExecuteEvent \circdef e: EVENT; v: \boolean \circspot \circblockbegin
\circif v = \true \circthen ExecuteChart(e)\\
\circelse~~~v = \false \circthen \Skip\\
\circfi
\circblockend
\end{circusaction}

\begin{displaymath}
ExecuteEvents \circdef es: \seq EVENT; vs: \seq \boolean \circspot
(\Semi i:id(1\upto \#es)\circspot ExecuteEvent(es(i),vs(i)))
\end{displaymath}

\begin{circusaction}
ExecuteEvents \circdef es: \seq EVENT; vs: \seq \boolean \circspot\\
\circvar i: \nat \circspot i:=1\circseq\\
\circmu X \circspot \circblockbegin
\circif i > \#es \circthen \Skip\\
\circelse~~i \leq \#es \circthen ExecuteEvent(es(i),vs(i))\circseq i:=i+1\circseq X\\
\circfi\\
\circblockend
\end{circusaction}



\begin{circusaction}
Step \circdef \circblockbegin
events?es \then  input\_event?vs\prefixcolon(\#vs = \#es) \then read\_inputs\then ExecuteEvents(es,vs) \circseq\\
write\_outputs \then \Skip\circblockend
\end{circusaction}

%Alternative, $input\_events$ is read in $Inputs$ on the chart side.
%
%\begin{circus}
%\circchannel events: \seq (EVENT\cross\boolean)
%\end{circus}
%
%\begin{circusaction}
%Step \circdef \circblockbegin
%read\_inputs\then events?es \then (\Semi i: \dom es \circspot ExecuteEvent(es(i).1,es(i).2)) \circseq\\
%write\_outputs \then end\_cycle \then \Skip\circblockend
%\end{circusaction}


\begin{circusaction}
\circspot (\circmu X \circspot Step \circseq end\_cycle \then X)
\end{circusaction}

\begin{circus}
\circend
\end{circus}

\end{document} 