\begin{zsection}\\
\SECTION sf\_car\_shift\_logic \parents stateflow\_toolkit, calc\_th\\
\end{zsection}\\
\begin{axdef}
s\_downshifting, s\_gear\_state, s\_fourth, s\_second, s\_third, s\_first, s\_selection\_state, s\_upshifting, s\_steady\_state, c\_shift\_logic: SID
\end{axdef}

\begin{axdef}
t\_third\_fourth, t\_second\_third, t\_first\_second, t\_fourth\_third, t\_default\_first, t\_second\_first, t\_third\_second, t\_steady\_state\_upshifting, t\_default\_steady\_state, t\_upshifting\_steady\_state23, t\_steady\_state\_downshifting, t\_downshifting\_steady\_state25, t\_downshifting\_steady\_state24, t\_upshifting\_steady\_state26: TID
\end{axdef}

\begin{axdef}
C\_shift\_logic: State
 \where 
C\_shift\_logic = \circblockbegin\lblot identifier == c\_shift\_logic,
\\ default == nulltransition.identifier,
\\ inner == nulltransition.identifier,
\\ outer == nulltransition.identifier,
\\ parent == nullstate.identifier,
\\ left == nullstate.identifier,
\\ right == nullstate.identifier,
\\ substates == \langle s\_gear\_state, s\_selection\_state \rangle,
\\ decomposition == SET,
\\ type == CHART,
\\ history == \false \rblot\circblockend
\end{axdef}

\begin{axdef}
S\_downshifting: State
 \where 
S\_downshifting = \circblockbegin\lblot identifier == s\_downshifting,
\\ default == nulltransition.identifier,
\\ inner == nulltransition.identifier,
\\ outer == t\_downshifting\_steady\_state24,
\\ parent == s\_selection\_state,
\\ left == nullstate.identifier,
\\ right == nullstate.identifier,
\\ substates == \langle  \rangle,
\\ decomposition == CLUSTER,
\\ type == OR,
\\ history == \false \rblot\circblockend
\end{axdef}

\begin{axdef}
S\_gear\_state: State
 \where 
S\_gear\_state = \circblockbegin\lblot identifier == s\_gear\_state,
\\ default == t\_default\_first,
\\ inner == nulltransition.identifier,
\\ outer == nulltransition.identifier,
\\ parent == c\_shift\_logic,
\\ left == nullstate.identifier,
\\ right == s\_selection\_state,
\\ substates == \langle s\_first, s\_fourth, s\_third, s\_second \rangle,
\\ decomposition == CLUSTER,
\\ type == AND,
\\ history == \false \rblot\circblockend
\end{axdef}

\begin{axdef}
S\_fourth: State
 \where 
S\_fourth = \circblockbegin\lblot identifier == s\_fourth,
\\ default == nulltransition.identifier,
\\ inner == nulltransition.identifier,
\\ outer == t\_fourth\_third,
\\ parent == s\_gear\_state,
\\ left == nullstate.identifier,
\\ right == nullstate.identifier,
\\ substates == \langle  \rangle,
\\ decomposition == CLUSTER,
\\ type == OR,
\\ history == \false \rblot\circblockend
\end{axdef}

\begin{axdef}
S\_second: State
 \where 
S\_second = \circblockbegin\lblot identifier == s\_second,
\\ default == nulltransition.identifier,
\\ inner == nulltransition.identifier,
\\ outer == t\_second\_third,
\\ parent == s\_gear\_state,
\\ left == nullstate.identifier,
\\ right == nullstate.identifier,
\\ substates == \langle  \rangle,
\\ decomposition == CLUSTER,
\\ type == OR,
\\ history == \false \rblot\circblockend
\end{axdef}

\begin{axdef}
S\_third: State
 \where 
S\_third = \circblockbegin\lblot identifier == s\_third,
\\ default == nulltransition.identifier,
\\ inner == nulltransition.identifier,
\\ outer == t\_third\_fourth,
\\ parent == s\_gear\_state,
\\ left == nullstate.identifier,
\\ right == nullstate.identifier,
\\ substates == \langle  \rangle,
\\ decomposition == CLUSTER,
\\ type == OR,
\\ history == \false \rblot\circblockend
\end{axdef}

\begin{axdef}
S\_first: State
 \where 
S\_first = \circblockbegin\lblot identifier == s\_first,
\\ default == nulltransition.identifier,
\\ inner == nulltransition.identifier,
\\ outer == t\_first\_second,
\\ parent == s\_gear\_state,
\\ left == nullstate.identifier,
\\ right == nullstate.identifier,
\\ substates == \langle  \rangle,
\\ decomposition == CLUSTER,
\\ type == OR,
\\ history == \false \rblot\circblockend
\end{axdef}

\begin{axdef}
S\_selection\_state: State
 \where 
S\_selection\_state = \circblockbegin\lblot identifier == s\_selection\_state,
\\ default == t\_default\_steady\_state,
\\ inner == nulltransition.identifier,
\\ outer == nulltransition.identifier,
\\ parent == c\_shift\_logic,
\\ left == s\_gear\_state,
\\ right == nullstate.identifier,
\\ substates == \langle s\_downshifting, s\_upshifting, s\_steady\_state \rangle,
\\ decomposition == CLUSTER,
\\ type == AND,
\\ history == \false \rblot\circblockend
\end{axdef}

\begin{axdef}
S\_upshifting: State
 \where 
S\_upshifting = \circblockbegin\lblot identifier == s\_upshifting,
\\ default == nulltransition.identifier,
\\ inner == nulltransition.identifier,
\\ outer == t\_upshifting\_steady\_state26,
\\ parent == s\_selection\_state,
\\ left == nullstate.identifier,
\\ right == nullstate.identifier,
\\ substates == \langle  \rangle,
\\ decomposition == CLUSTER,
\\ type == OR,
\\ history == \false \rblot\circblockend
\end{axdef}

\begin{axdef}
S\_steady\_state: State
 \where 
S\_steady\_state = \circblockbegin\lblot identifier == s\_steady\_state,
\\ default == nulltransition.identifier,
\\ inner == nulltransition.identifier,
\\ outer == t\_steady\_state\_upshifting,
\\ parent == s\_selection\_state,
\\ left == nullstate.identifier,
\\ right == nullstate.identifier,
\\ substates == \langle  \rangle,
\\ decomposition == CLUSTER,
\\ type == OR,
\\ history == \false \rblot\circblockend
\end{axdef}

\begin{axdef}
T\_third\_fourth: Transition
 \where 
T\_third\_fourth = \circblockbegin\lblot identifier == t\_third\_fourth,
\\ source == snode(s\_third),
\\ destination == snode(s\_fourth),
\\ next == t\_third\_second,
\\ parent == s\_gear\_state \rblot\circblockend
\end{axdef}

\begin{axdef}
T\_second\_third: Transition
 \where 
T\_second\_third = \circblockbegin\lblot identifier == t\_second\_third,
\\ source == snode(s\_second),
\\ destination == snode(s\_third),
\\ next == t\_second\_first,
\\ parent == s\_gear\_state \rblot\circblockend
\end{axdef}

\begin{axdef}
T\_first\_second: Transition
 \where 
T\_first\_second = \circblockbegin\lblot identifier == t\_first\_second,
\\ source == snode(s\_first),
\\ destination == snode(s\_second),
\\ next == nulltransition.identifier,
\\ parent == s\_gear\_state \rblot\circblockend
\end{axdef}

\begin{axdef}
T\_fourth\_third: Transition
 \where 
T\_fourth\_third = \circblockbegin\lblot identifier == t\_fourth\_third,
\\ source == snode(s\_fourth),
\\ destination == snode(s\_third),
\\ next == nulltransition.identifier,
\\ parent == s\_gear\_state \rblot\circblockend
\end{axdef}

\begin{axdef}
T\_default\_first: Transition
 \where 
T\_default\_first = \circblockbegin\lblot identifier == t\_default\_first,
\\ source == snode(nullstate.identifier),
\\ destination == snode(s\_first),
\\ next == nulltransition.identifier,
\\ parent == s\_gear\_state \rblot\circblockend
\end{axdef}

\begin{axdef}
T\_second\_first: Transition
 \where 
T\_second\_first = \circblockbegin\lblot identifier == t\_second\_first,
\\ source == snode(s\_second),
\\ destination == snode(s\_first),
\\ next == nulltransition.identifier,
\\ parent == s\_gear\_state \rblot\circblockend
\end{axdef}

\begin{axdef}
T\_third\_second: Transition
 \where 
T\_third\_second = \circblockbegin\lblot identifier == t\_third\_second,
\\ source == snode(s\_third),
\\ destination == snode(s\_second),
\\ next == nulltransition.identifier,
\\ parent == s\_gear\_state \rblot\circblockend
\end{axdef}

\begin{axdef}
T\_steady\_state\_upshifting: Transition
 \where 
T\_steady\_state\_upshifting = \circblockbegin\lblot identifier == t\_steady\_state\_upshifting,
\\ source == snode(s\_steady\_state),
\\ destination == snode(s\_upshifting),
\\ next == t\_steady\_state\_downshifting,
\\ parent == s\_selection\_state \rblot\circblockend
\end{axdef}

\begin{axdef}
T\_default\_steady\_state: Transition
 \where 
T\_default\_steady\_state = \circblockbegin\lblot identifier == t\_default\_steady\_state,
\\ source == snode(nullstate.identifier),
\\ destination == snode(s\_steady\_state),
\\ next == nulltransition.identifier,
\\ parent == s\_selection\_state \rblot\circblockend
\end{axdef}

\begin{axdef}
T\_upshifting\_steady\_state23: Transition
 \where 
T\_upshifting\_steady\_state23 = \circblockbegin\lblot identifier == t\_upshifting\_steady\_state23,
\\ source == snode(s\_upshifting),
\\ destination == snode(s\_steady\_state),
\\ next == nulltransition.identifier,
\\ parent == s\_selection\_state \rblot\circblockend
\end{axdef}

\begin{axdef}
T\_steady\_state\_downshifting: Transition
 \where 
T\_steady\_state\_downshifting = \circblockbegin\lblot identifier == t\_steady\_state\_downshifting,
\\ source == snode(s\_steady\_state),
\\ destination == snode(s\_downshifting),
\\ next == nulltransition.identifier,
\\ parent == s\_selection\_state \rblot\circblockend
\end{axdef}

\begin{axdef}
T\_downshifting\_steady\_state25: Transition
 \where 
T\_downshifting\_steady\_state25 = \circblockbegin\lblot identifier == t\_downshifting\_steady\_state25,
\\ source == snode(s\_downshifting),
\\ destination == snode(s\_steady\_state),
\\ next == nulltransition.identifier,
\\ parent == s\_selection\_state \rblot\circblockend
\end{axdef}

\begin{axdef}
T\_downshifting\_steady\_state24: Transition
 \where 
T\_downshifting\_steady\_state24 = \circblockbegin\lblot identifier == t\_downshifting\_steady\_state24,
\\ source == snode(s\_downshifting),
\\ destination == snode(s\_steady\_state),
\\ next == t\_downshifting\_steady\_state25,
\\ parent == s\_selection\_state \rblot\circblockend
\end{axdef}

\begin{axdef}
T\_upshifting\_steady\_state26: Transition
 \where 
T\_upshifting\_steady\_state26 = \circblockbegin\lblot identifier == t\_upshifting\_steady\_state26,
\\ source == snode(s\_upshifting),
\\ destination == snode(s\_steady\_state),
\\ next == t\_upshifting\_steady\_state23,
\\ parent == s\_selection\_state \rblot\circblockend
\end{axdef}

\begin{axdef}
e\_UP, e\_DOWN, ENULL: EVENT
\end{axdef}

\begin{circus}
\circchannel o\_gear: \real; i\_speed: \real; i\_throttle: \real
\end{circus}

\begin{circus}
\circprocess P\_shift\_logic \circdef \circbegin\\
\end{circus}

\begin{axdef}
StateflowChart
 \where 
identifier = c\_shift\_logic\\
states = \{(c\_shift\_logic, C\_shift\_logic), (s\_downshifting, S\_downshifting), (s\_gear\_state, S\_gear\_state), (s\_fourth, S\_fourth), (s\_second, S\_second), (s\_third, S\_third), (s\_first, S\_first), (s\_selection\_state, S\_selection\_state), (s\_upshifting, S\_upshifting), (s\_steady\_state, S\_steady\_state)\}\\
transitions = \{(t\_third\_fourth, T\_third\_fourth), (t\_second\_third, T\_second\_third), (t\_first\_second, T\_first\_second), (t\_fourth\_third, T\_fourth\_third), (t\_default\_first, T\_default\_first), (t\_second\_first, T\_second\_first), (t\_third\_second, T\_third\_second), (t\_steady\_state\_upshifting, T\_steady\_state\_upshifting), (t\_default\_steady\_state, T\_default\_steady\_state), (t\_upshifting\_steady\_state23, T\_upshifting\_steady\_state23), (t\_steady\_state\_downshifting, T\_steady\_state\_downshifting), (t\_downshifting\_steady\_state25, T\_downshifting\_steady\_state25), (t\_downshifting\_steady\_state24, T\_downshifting\_steady\_state24), (t\_upshifting\_steady\_state26, T\_upshifting\_steady\_state26)\}\\
junctions = \{\}
\end{axdef}

\begin{schema}{SimulationInstance~}
v\_gear: \real\\
 v\_up\_th: \real\\
 v\_speed: \real\\
 v\_down\_th: \real\\
 v\_throttle: \real
\end{schema}

\begin{schema}{InitSimulationInstance}
SimulationInstance~'
 \where 
v\_gear' = 0\\
v\_up\_th' = 0\\
v\_speed' = 0\\
v\_down\_th' = 0\\
v\_throttle' = 0
\end{schema}

\begin{schema}{SimulationData}
state\_status: SID \pfun \boolean\\
state\_history: SID \pfun SID
\where
\dom state\_status = \dom states\\
\dom state\_history = \{j: \ran junctions | j.history = \true @ j.parent \}\\
\forall s: \ran states | s.decomposition = CLUSTER @ \#\{ss: \ran s.substates | state\_status(ss) = \true\} \leq 1
\end{schema}

\begin{schema}{InitSimulationData}
SimulationData~'
\where
state\_status' = \{n: \dom states @ n \mapsto \false\}\\
state\_history' = \{n: \dom state\_history' @ n \mapsto nullstate.identifier\}
\end{schema}

\begin{schema}{ActivateNoHistory}
\Delta SimulationData\\
x?: SID
\where
x? \in \dom state\_status\\
(parent~(states~x?)).history = \false\\
state\_history' = state\_history\\
state\_status' = state\_status \oplus \{x?\mapsto \true\}
\end{schema}

\begin{schema}{ActivateWithHistory}
\Delta SimulationData\\
x?: SID
\where
x? \in \dom state\_status\\
(parent~(states~x?)).history = \true\\
state\_history' = state\_history \oplus \{((states~x?).parent) \mapsto x?\}\\
state\_status' = state\_status \oplus \{x?\mapsto \true\}
\end{schema}

\begin{zed}
Activate == (ActivateWithHistory\lor ActivateNoHistory) \land \Xi SimulationInstance
\end{zed}

\begin{schema}{Deactivate}
\Delta SimulationData\\
\Xi SimulationInstance\\
x?: SID
\where
x? \in \dom state\_status\\
state\_history' = state\_history\\
state\_status' = state\_status \oplus \{x?\mapsto \false\}
\end{schema}

\begin{zed}
InitState == (InitSimulationInstance) \land (InitSimulationData)
\end{zed}


\begin{circusaction}
\circstate shift\_logic\_state == (SimulationInstance~) \land (SimulationData~)
\end{circusaction}

\begin{circusaction}
entryaction\_downshifting \circdef (executeentryaction.(s\_downshifting) \then \Skip)
\end{circusaction}

\begin{circusaction}
entryaction\_gear\_state \circdef (executeentryaction.(s\_gear\_state) \then \Skip)
\end{circusaction}

\begin{circusaction}
entryaction\_fourth \circdef (executeentryaction.(s\_fourth) \then v\_gear := 4)
\end{circusaction}

\begin{circusaction}
entryaction\_second \circdef (executeentryaction.(s\_second) \then v\_gear := 2)
\end{circusaction}

\begin{circusaction}
entryaction\_third \circdef (executeentryaction.(s\_third) \then v\_gear := 3)
\end{circusaction}

\begin{circusaction}
entryaction\_first \circdef (executeentryaction.(s\_first) \then v\_gear := 1)
\end{circusaction}

\begin{circusaction}
entryaction\_selection\_state \circdef (executeentryaction.(s\_selection\_state) \then \Skip)
\end{circusaction}

\begin{circusaction}
entryaction\_upshifting \circdef (executeentryaction.(s\_upshifting) \then \Skip)
\end{circusaction}

\begin{circusaction}
entryaction\_steady\_state \circdef (executeentryaction.(s\_steady\_state) \then \Skip)
\end{circusaction}

\begin{circusaction}
entryactions \circdef ( entryaction\_downshifting\\
\extchoice\\
entryaction\_gear\_state\\
\extchoice\\
entryaction\_fourth\\
\extchoice\\
entryaction\_second\\
\extchoice\\
entryaction\_third\\
\extchoice\\
entryaction\_first\\
\extchoice\\
entryaction\_selection\_state\\
\extchoice\\
entryaction\_upshifting\\
\extchoice\\
entryaction\_steady\_state ) 
\end{circusaction}

\begin{circusaction}
duringaction\_downshifting \circdef (executeduringaction.(s\_downshifting)?ce \then \Skip)
\end{circusaction}

\begin{circusaction}
duringaction\_gear\_state \circdef (executeduringaction.(s\_gear\_state)?ce \then \Skip)
\end{circusaction}

\begin{circusaction}
duringaction\_fourth \circdef (executeduringaction.(s\_fourth)?ce \then \Skip)
\end{circusaction}

\begin{circusaction}
duringaction\_second \circdef (executeduringaction.(s\_second)?ce \then \Skip)
\end{circusaction}

\begin{circusaction}
duringaction\_third \circdef (executeduringaction.(s\_third)?ce \then \Skip)
\end{circusaction}

\begin{circusaction}
duringaction\_first \circdef (executeduringaction.(s\_first)?ce \then \Skip)
\end{circusaction}

\begin{circusaction}
duringaction\_selection\_state \circdef (executeduringaction.(s\_selection\_state)?ce \then (\circvar \_aux: \real \cross \real \circspot ( \_aux := calc\_th(v\_gear, v\_throttle)\circseq\\
v\_down\_th := \_aux.1\circseq\\
v\_up\_th := \_aux.2 ) ))
\end{circusaction}

\begin{circusaction}
duringaction\_upshifting \circdef (executeduringaction.(s\_upshifting)?ce \then \Skip)
\end{circusaction}

\begin{circusaction}
duringaction\_steady\_state \circdef (executeduringaction.(s\_steady\_state)?ce \then \Skip)
\end{circusaction}

\begin{circusaction}
duringactions \circdef ( duringaction\_downshifting\\
\extchoice\\
duringaction\_gear\_state\\
\extchoice\\
duringaction\_fourth\\
\extchoice\\
duringaction\_second\\
\extchoice\\
duringaction\_third\\
\extchoice\\
duringaction\_first\\
\extchoice\\
duringaction\_selection\_state\\
\extchoice\\
duringaction\_upshifting\\
\extchoice\\
duringaction\_steady\_state ) 
\end{circusaction}

\begin{circusaction}
exitaction\_downshifting \circdef (executeexitaction.(s\_downshifting) \then \Skip)
\end{circusaction}

\begin{circusaction}
exitaction\_gear\_state \circdef (executeexitaction.(s\_gear\_state) \then \Skip)
\end{circusaction}

\begin{circusaction}
exitaction\_fourth \circdef (executeexitaction.(s\_fourth) \then \Skip)
\end{circusaction}

\begin{circusaction}
exitaction\_second \circdef (executeexitaction.(s\_second) \then \Skip)
\end{circusaction}

\begin{circusaction}
exitaction\_third \circdef (executeexitaction.(s\_third) \then \Skip)
\end{circusaction}

\begin{circusaction}
exitaction\_first \circdef (executeexitaction.(s\_first) \then \Skip)
\end{circusaction}

\begin{circusaction}
exitaction\_selection\_state \circdef (executeexitaction.(s\_selection\_state) \then \Skip)
\end{circusaction}

\begin{circusaction}
exitaction\_upshifting \circdef (executeexitaction.(s\_upshifting) \then \Skip)
\end{circusaction}

\begin{circusaction}
exitaction\_steady\_state \circdef (executeexitaction.(s\_steady\_state) \then \Skip)
\end{circusaction}

\begin{circusaction}
exitactions \circdef ( exitaction\_downshifting\\
\extchoice\\
exitaction\_gear\_state\\
\extchoice\\
exitaction\_fourth\\
\extchoice\\
exitaction\_second\\
\extchoice\\
exitaction\_third\\
\extchoice\\
exitaction\_first\\
\extchoice\\
exitaction\_selection\_state\\
\extchoice\\
exitaction\_upshifting\\
\extchoice\\
exitaction\_steady\_state ) 
\end{circusaction}

\begin{circusaction}
conditionaction\_third\_fourth \circdef (executeconditionaction.(t\_third\_fourth) \then \Skip)
\end{circusaction}

\begin{circusaction}
conditionaction\_second\_third \circdef (executeconditionaction.(t\_second\_third) \then \Skip)
\end{circusaction}

\begin{circusaction}
conditionaction\_first\_second \circdef (executeconditionaction.(t\_first\_second) \then \Skip)
\end{circusaction}

\begin{circusaction}
conditionaction\_fourth\_third \circdef (executeconditionaction.(t\_fourth\_third) \then \Skip)
\end{circusaction}

\begin{circusaction}
conditionaction\_default\_first \circdef (executeconditionaction.(t\_default\_first) \then \Skip)
\end{circusaction}

\begin{circusaction}
conditionaction\_second\_first \circdef (executeconditionaction.(t\_second\_first) \then \Skip)
\end{circusaction}

\begin{circusaction}
conditionaction\_third\_second \circdef (executeconditionaction.(t\_third\_second) \then \Skip)
\end{circusaction}

\begin{circusaction}
conditionaction\_steady\_state\_upshifting \circdef (executeconditionaction.(t\_steady\_state\_upshifting) \then \Skip)
\end{circusaction}

\begin{circusaction}
conditionaction\_default\_steady\_state \circdef (executeconditionaction.(t\_default\_steady\_state) \then \Skip)
\end{circusaction}

\begin{circusaction}
conditionaction\_upshifting\_steady\_state23 \circdef (executeconditionaction.(t\_upshifting\_steady\_state23) \then \Skip)
\end{circusaction}

\begin{circusaction}
conditionaction\_steady\_state\_downshifting \circdef (executeconditionaction.(t\_steady\_state\_downshifting) \then \Skip)
\end{circusaction}

\begin{circusaction}
conditionaction\_downshifting\_steady\_state25 \circdef (executeconditionaction.(t\_downshifting\_steady\_state25) \then (\circvar \_b: \boolean \circspot ((broadcast(e\_DOWN, s\_gear\_state) \circseq check(\_b)) \circseq ( \circif \_b = \true \circthen \Skip
\\\circelse \lnot (\_b = \true) \circthen (\Skip)\\

\circfi ) )))
\end{circusaction}

\begin{circusaction}
conditionaction\_downshifting\_steady\_state24 \circdef (executeconditionaction.(t\_downshifting\_steady\_state24) \then \Skip)
\end{circusaction}

\begin{circusaction}
conditionaction\_upshifting\_steady\_state26 \circdef (executeconditionaction.(t\_upshifting\_steady\_state26) \then (\circvar \_b: \boolean \circspot ((broadcast(e\_UP, s\_gear\_state) \circseq check(\_b)) \circseq ( \circif \_b = \true \circthen \Skip
\\\circelse \lnot (\_b = \true) \circthen (\Skip)\\

\circfi ) )))
\end{circusaction}

\begin{circusaction}
conditionactions \circdef ( conditionaction\_third\_fourth\\
\extchoice\\
conditionaction\_second\_third\\
\extchoice\\
conditionaction\_first\_second\\
\extchoice\\
conditionaction\_fourth\_third\\
\extchoice\\
conditionaction\_default\_first\\
\extchoice\\
conditionaction\_second\_first\\
\extchoice\\
conditionaction\_third\_second\\
\extchoice\\
conditionaction\_steady\_state\_upshifting\\
\extchoice\\
conditionaction\_default\_steady\_state\\
\extchoice\\
conditionaction\_upshifting\_steady\_state23\\
\extchoice\\
conditionaction\_steady\_state\_downshifting\\
\extchoice\\
conditionaction\_downshifting\_steady\_state25\\
\extchoice\\
conditionaction\_downshifting\_steady\_state24\\
\extchoice\\
conditionaction\_upshifting\_steady\_state26 ) 
\end{circusaction}

\begin{circusaction}
transitionaction\_third\_fourth \circdef (executetransitionaction.(t\_third\_fourth) \then \Skip)
\end{circusaction}

\begin{circusaction}
transitionaction\_second\_third \circdef (executetransitionaction.(t\_second\_third) \then \Skip)
\end{circusaction}

\begin{circusaction}
transitionaction\_first\_second \circdef (executetransitionaction.(t\_first\_second) \then \Skip)
\end{circusaction}

\begin{circusaction}
transitionaction\_fourth\_third \circdef (executetransitionaction.(t\_fourth\_third) \then \Skip)
\end{circusaction}

\begin{circusaction}
transitionaction\_default\_first \circdef (executetransitionaction.(t\_default\_first) \then \Skip)
\end{circusaction}

\begin{circusaction}
transitionaction\_second\_first \circdef (executetransitionaction.(t\_second\_first) \then \Skip)
\end{circusaction}

\begin{circusaction}
transitionaction\_third\_second \circdef (executetransitionaction.(t\_third\_second) \then \Skip)
\end{circusaction}

\begin{circusaction}
transitionaction\_steady\_state\_upshifting \circdef (executetransitionaction.(t\_steady\_state\_upshifting) \then \Skip)
\end{circusaction}

\begin{circusaction}
transitionaction\_default\_steady\_state \circdef (executetransitionaction.(t\_default\_steady\_state) \then \Skip)
\end{circusaction}

\begin{circusaction}
transitionaction\_upshifting\_steady\_state23 \circdef (executetransitionaction.(t\_upshifting\_steady\_state23) \then \Skip)
\end{circusaction}

\begin{circusaction}
transitionaction\_steady\_state\_downshifting \circdef (executetransitionaction.(t\_steady\_state\_downshifting) \then \Skip)
\end{circusaction}

\begin{circusaction}
transitionaction\_downshifting\_steady\_state25 \circdef (executetransitionaction.(t\_downshifting\_steady\_state25) \then \Skip)
\end{circusaction}

\begin{circusaction}
transitionaction\_downshifting\_steady\_state24 \circdef (executetransitionaction.(t\_downshifting\_steady\_state24) \then \Skip)
\end{circusaction}

\begin{circusaction}
transitionaction\_upshifting\_steady\_state26 \circdef (executetransitionaction.(t\_upshifting\_steady\_state26) \then \Skip)
\end{circusaction}

\begin{circusaction}
transitionactions \circdef ( transitionaction\_third\_fourth\\
\extchoice\\
transitionaction\_second\_third\\
\extchoice\\
transitionaction\_first\_second\\
\extchoice\\
transitionaction\_fourth\_third\\
\extchoice\\
transitionaction\_default\_first\\
\extchoice\\
transitionaction\_second\_first\\
\extchoice\\
transitionaction\_third\_second\\
\extchoice\\
transitionaction\_steady\_state\_upshifting\\
\extchoice\\
transitionaction\_default\_steady\_state\\
\extchoice\\
transitionaction\_upshifting\_steady\_state23\\
\extchoice\\
transitionaction\_steady\_state\_downshifting\\
\extchoice\\
transitionaction\_downshifting\_steady\_state25\\
\extchoice\\
transitionaction\_downshifting\_steady\_state24\\
\extchoice\\
transitionaction\_upshifting\_steady\_state26 ) 
\end{circusaction}

\begin{circusaction}
condition\_third\_fourth \circdef (evaluatecondition.(t\_third\_fourth)!(\true) \then \Skip)
\end{circusaction}

\begin{circusaction}
condition\_second\_third \circdef (evaluatecondition.(t\_second\_third)!(\true) \then \Skip)
\end{circusaction}

\begin{circusaction}
condition\_first\_second \circdef (evaluatecondition.(t\_first\_second)!(\true) \then \Skip)
\end{circusaction}

\begin{circusaction}
condition\_fourth\_third \circdef (evaluatecondition.(t\_fourth\_third)!(\true) \then \Skip)
\end{circusaction}

\begin{circusaction}
condition\_default\_first \circdef (evaluatecondition.(t\_default\_first)!(\true) \then \Skip)
\end{circusaction}

\begin{circusaction}
condition\_second\_first \circdef (evaluatecondition.(t\_second\_first)!(\true) \then \Skip)
\end{circusaction}

\begin{circusaction}
condition\_third\_second \circdef (evaluatecondition.(t\_third\_second)!(\true) \then \Skip)
\end{circusaction}

\begin{circusaction}
condition\_steady\_state\_upshifting \circdef ( \circif ((v\_speed \agt v\_up\_th) \neq 0) \circthen (evaluatecondition.(t\_steady\_state\_upshifting)!(\true) \then \Skip)
\\\circelse \lnot (((v\_speed \agt v\_up\_th) \neq 0)) \circthen ((evaluatecondition.(t\_steady\_state\_upshifting)!(\false) \then \Skip))\\

\circfi ) 
\end{circusaction}

\begin{circusaction}
condition\_default\_steady\_state \circdef (evaluatecondition.(t\_default\_steady\_state)!(\true) \then \Skip)
\end{circusaction}

\begin{circusaction}
condition\_upshifting\_steady\_state23 \circdef ( \circif ((v\_speed \alt v\_up\_th) \neq 0) \circthen (evaluatecondition.(t\_upshifting\_steady\_state23)!(\true) \then \Skip)
\\\circelse \lnot (((v\_speed \alt v\_up\_th) \neq 0)) \circthen ((evaluatecondition.(t\_upshifting\_steady\_state23)!(\false) \then \Skip))\\

\circfi ) 
\end{circusaction}

\begin{circusaction}
condition\_steady\_state\_downshifting \circdef ( \circif ((v\_speed \alt v\_down\_th) \neq 0) \circthen (evaluatecondition.(t\_steady\_state\_downshifting)!(\true) \then \Skip)
\\\circelse \lnot (((v\_speed \alt v\_down\_th) \neq 0)) \circthen ((evaluatecondition.(t\_steady\_state\_downshifting)!(\false) \then \Skip))\\

\circfi ) 
\end{circusaction}

\begin{circusaction}
condition\_downshifting\_steady\_state25 \circdef ( \circif ((v\_speed \aleq v\_down\_th) \neq 0) \circthen (evaluatecondition.(t\_downshifting\_steady\_state25)!(\true) \then \Skip)
\\\circelse \lnot (((v\_speed \aleq v\_down\_th) \neq 0)) \circthen ((evaluatecondition.(t\_downshifting\_steady\_state25)!(\false) \then \Skip))\\

\circfi ) 
\end{circusaction}

\begin{circusaction}
condition\_downshifting\_steady\_state24 \circdef ( \circif ((v\_speed \agt v\_down\_th) \neq 0) \circthen (evaluatecondition.(t\_downshifting\_steady\_state24)!(\true) \then \Skip)
\\\circelse \lnot (((v\_speed \agt v\_down\_th) \neq 0)) \circthen ((evaluatecondition.(t\_downshifting\_steady\_state24)!(\false) \then \Skip))\\

\circfi ) 
\end{circusaction}

\begin{circusaction}
condition\_upshifting\_steady\_state26 \circdef ( \circif ((v\_speed \ageq v\_up\_th) \neq 0) \circthen (evaluatecondition.(t\_upshifting\_steady\_state26)!(\true) \then \Skip)
\\\circelse \lnot (((v\_speed \ageq v\_up\_th) \neq 0)) \circthen ((evaluatecondition.(t\_upshifting\_steady\_state26)!(\false) \then \Skip))\\

\circfi ) 
\end{circusaction}

\begin{circusaction}
conditions \circdef ( condition\_third\_fourth\\
\extchoice\\
condition\_second\_third\\
\extchoice\\
condition\_first\_second\\
\extchoice\\
condition\_fourth\_third\\
\extchoice\\
condition\_default\_first\\
\extchoice\\
condition\_second\_first\\
\extchoice\\
condition\_third\_second\\
\extchoice\\
condition\_steady\_state\_upshifting\\
\extchoice\\
condition\_default\_steady\_state\\
\extchoice\\
condition\_upshifting\_steady\_state23\\
\extchoice\\
condition\_steady\_state\_downshifting\\
\extchoice\\
condition\_downshifting\_steady\_state25\\
\extchoice\\
condition\_downshifting\_steady\_state24\\
\extchoice\\
condition\_upshifting\_steady\_state26 ) 
\end{circusaction}

\begin{circusaction}
trigger\_third\_fourth \circdef (checktrigger.(t\_third\_fourth)?e \then ( \circif e = e\_UP \circthen (result.(t\_third\_fourth).(e)!(\true) \then \Skip)
\\\circelse \lnot (e = e\_UP) \circthen ((result.(t\_third\_fourth).(e)!(\false) \then \Skip))\\

\circfi ) )
\end{circusaction}

\begin{circusaction}
trigger\_second\_third \circdef (checktrigger.(t\_second\_third)?e \then ( \circif e = e\_UP \circthen (result.(t\_second\_third).(e)!(\true) \then \Skip)
\\\circelse \lnot (e = e\_UP) \circthen ((result.(t\_second\_third).(e)!(\false) \then \Skip))\\

\circfi ) )
\end{circusaction}

\begin{circusaction}
trigger\_first\_second \circdef (checktrigger.(t\_first\_second)?e \then ( \circif e = e\_UP \circthen (result.(t\_first\_second).(e)!(\true) \then \Skip)
\\\circelse \lnot (e = e\_UP) \circthen ((result.(t\_first\_second).(e)!(\false) \then \Skip))\\

\circfi ) )
\end{circusaction}

\begin{circusaction}
trigger\_fourth\_third \circdef (checktrigger.(t\_fourth\_third)?e \then ( \circif e = e\_DOWN \circthen (result.(t\_fourth\_third).(e)!(\true) \then \Skip)
\\\circelse \lnot (e = e\_DOWN) \circthen ((result.(t\_fourth\_third).(e)!(\false) \then \Skip))\\

\circfi ) )
\end{circusaction}

\begin{circusaction}
trigger\_default\_first \circdef (checktrigger.(t\_default\_first)?e \then (result.(t\_default\_first).(e)!(\true) \then \Skip))
\end{circusaction}

\begin{circusaction}
trigger\_second\_first \circdef (checktrigger.(t\_second\_first)?e \then ( \circif e = e\_DOWN \circthen (result.(t\_second\_first).(e)!(\true) \then \Skip)
\\\circelse \lnot (e = e\_DOWN) \circthen ((result.(t\_second\_first).(e)!(\false) \then \Skip))\\

\circfi ) )
\end{circusaction}

\begin{circusaction}
trigger\_third\_second \circdef (checktrigger.(t\_third\_second)?e \then ( \circif e = e\_DOWN \circthen (result.(t\_third\_second).(e)!(\true) \then \Skip)
\\\circelse \lnot (e = e\_DOWN) \circthen ((result.(t\_third\_second).(e)!(\false) \then \Skip))\\

\circfi ) )
\end{circusaction}

\begin{circusaction}
trigger\_steady\_state\_upshifting \circdef (checktrigger.(t\_steady\_state\_upshifting)?e \then (result.(t\_steady\_state\_upshifting).(e)!(\true) \then \Skip))
\end{circusaction}

\begin{circusaction}
trigger\_default\_steady\_state \circdef (checktrigger.(t\_default\_steady\_state)?e \then (result.(t\_default\_steady\_state).(e)!(\true) \then \Skip))
\end{circusaction}

\begin{circusaction}
trigger\_upshifting\_steady\_state23 \circdef (checktrigger.(t\_upshifting\_steady\_state23)?e \then (result.(t\_upshifting\_steady\_state23).(e)!(\true) \then \Skip))
\end{circusaction}

\begin{circusaction}
trigger\_steady\_state\_downshifting \circdef (checktrigger.(t\_steady\_state\_downshifting)?e \then (result.(t\_steady\_state\_downshifting).(e)!(\true) \then \Skip))
\end{circusaction}

\begin{circusaction}
trigger\_downshifting\_steady\_state25 \circdef (checktrigger.(t\_downshifting\_steady\_state25)?e \then (result.(t\_downshifting\_steady\_state25).(e)!(\true) \then \Skip))
\end{circusaction}

\begin{circusaction}
trigger\_downshifting\_steady\_state24 \circdef (checktrigger.(t\_downshifting\_steady\_state24)?e \then (result.(t\_downshifting\_steady\_state24).(e)!(\true) \then \Skip))
\end{circusaction}

\begin{circusaction}
trigger\_upshifting\_steady\_state26 \circdef (checktrigger.(t\_upshifting\_steady\_state26)?e \then (result.(t\_upshifting\_steady\_state26).(e)!(\true) \then \Skip))
\end{circusaction}

\begin{circusaction}
triggers \circdef ( trigger\_third\_fourth\\
\extchoice\\
trigger\_second\_third\\
\extchoice\\
trigger\_first\_second\\
\extchoice\\
trigger\_fourth\_third\\
\extchoice\\
trigger\_default\_first\\
\extchoice\\
trigger\_second\_first\\
\extchoice\\
trigger\_third\_second\\
\extchoice\\
trigger\_steady\_state\_upshifting\\
\extchoice\\
trigger\_default\_steady\_state\\
\extchoice\\
trigger\_upshifting\_steady\_state23\\
\extchoice\\
trigger\_steady\_state\_downshifting\\
\extchoice\\
trigger\_downshifting\_steady\_state25\\
\extchoice\\
trigger\_downshifting\_steady\_state24\\
\extchoice\\
trigger\_upshifting\_steady\_state26 ) 
\end{circusaction}

\begin{circusaction}
getevents \circdef (events!(\langle ENULL \rangle) \then \Skip)
\end{circusaction}

\begin{circusaction}
getstate \circdef (state?x\prefixcolon(x \in \dom(states))!(states(x)) \then \Skip)
\end{circusaction}

\begin{circusaction}
getjunction \circdef (junction?x\prefixcolon(x \in \dom(junctions))!(junctions(x)) \then \Skip)
\end{circusaction}

\begin{circusaction}
gettransition \circdef (transition?x\prefixcolon(x \in \dom(transitions))!(transitions(x)) \then \Skip)
\end{circusaction}

\begin{circusaction}
getchart \circdef (chart!(states(identifier)) \then \Skip)
\end{circusaction}

\begin{circusaction}
broadcast \circdef e: EVENT; dest: SID \circspot
local\_event!(e, states(dest)) \then \circmu X \circspot
\circblockbegin (AllActions \circseq X)\\
\extchoice\\
(end\_local\_execution \then \Skip)\circblockend
\end{circusaction}

\begin{circusaction}
check \circdef \circres erl:\boolean \circspot \circmu X \circspot
(InterfaceActions\circseq X \extchoice interrupt?x \then erl:=x)
\end{circusaction}


\begin{circusaction}
status \circdef (status?x\prefixcolon(x \in \dom(state\_status))!(state\_status(x)) \then \Skip)
\end{circusaction}

\begin{circusaction}
history \circdef (history?x\prefixcolon(x \in \dom(state\_history))!(state\_history(x)) \then \Skip)
\end{circusaction}

\begin{circusaction}
activation \circdef (activate?x \then \lschexpract Activate \rschexpract)
\end{circusaction}

\begin{circusaction}
deactivation \circdef (deactivate?x \then \lschexpract Deactivate \rschexpract)
\end{circusaction}

\begin{circusaction}
ChartActions \circdef (( entryactions\\
\extchoice\\
duringactions\\
\extchoice\\
exitactions\\
\extchoice\\
conditionactions\\
\extchoice\\
transitionactions )  \circseq (end\_action \then \Skip))
\end{circusaction}

\begin{circusaction}
InterfaceActions \circdef ( getevents\\
\extchoice\\
getchart\\
\extchoice\\
getstate\\
\extchoice\\
getjunction\\
\extchoice\\
gettransition\\
\extchoice\\
status\\
\extchoice\\
history\\
\extchoice\\
activation\\
\extchoice\\
deactivation ) 
\end{circusaction}

\begin{circusaction}
Inputs \circdef (read\_inputs \then ((i\_speed?x \then v\_speed := x) \linter \{ v\_speed \} | \{ v\_throttle \} \rinter (i\_throttle?x \then v\_throttle := x)))
\end{circusaction}

\begin{circusaction}
Outputs \circdef (write\_outputs \then (o\_gear!(v\_gear) \then \Skip))
\end{circusaction}

\begin{circusaction}
AllActions \circdef ( conditionactions\\
\extchoice\\
triggers\\
\extchoice\\
Inputs\\
\extchoice\\
Outputs\\
\extchoice\\
ChartActions\\
\extchoice\\
InterfaceActions ) 
\end{circusaction}

\begin{circusaction}
\circspot \lschexpract InitState \rschexpract \circseq 
\circmu X \circspot
\circblockbegin
\circblockbegin
\circmu Y \circspot
\circblockbegin
(AllActions\circseq Y)\\
\extchoice\\
end\_cycle \then \Skip
\circblockend
\circblockend
\circseq X
\circblockend
\\
\end{circusaction}

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

\begin{circus}
\circprocess shift\_logic \circdef (P\_shift\_logic \lpar  interface \cup \lchanset end\_cycle \rchanset  \rpar Simulator)\circhide  interface
\end{circus}


