\begin{zsection}\\
\SECTION air\_Controller \parents stateflow\_toolkit\\
\end{zsection}\\
\begin{axdef}
s\_Off3, s\_On4, s\_FAN2, s\_SpeedValue, s\_Off7, s\_On8, s\_FAN1, s\_PowerOn, s\_PowerOff, c\_Controller: SID
\end{axdef}

\begin{axdef}
t\_On8\_Off7, t\_Off7\_On8, t\_PowerOff\_PowerOn, t\_default\_PowerOff, t\_PowerOn\_PowerOff, t\_On4\_Off3, t\_Off3\_On4, t\_default\_Off3, t\_default\_Off7: TID
\end{axdef}

\begin{axdef}
C\_Controller: State
 \where 
C\_Controller = \circblockbegin\lblot identifier == c\_Controller,
\\ default == t\_default\_PowerOff,
\\ inner == nulltransition.identifier,
\\ outer == nulltransition.identifier,
\\ parent == nullstate.identifier,
\\ left == nullstate.identifier,
\\ right == nullstate.identifier,
\\ substates == \langle s\_PowerOn, s\_PowerOff \rangle,
\\ decomposition == CLUSTER,
\\ type == CHART,
\\ history == \false \rblot\circblockend
\end{axdef}

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

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

\begin{axdef}
S\_FAN2: State
 \where 
S\_FAN2 = \circblockbegin\lblot identifier == s\_FAN2,
\\ default == t\_default\_Off3,
\\ inner == nulltransition.identifier,
\\ outer == nulltransition.identifier,
\\ parent == s\_PowerOn,
\\ left == s\_FAN1,
\\ right == s\_SpeedValue,
\\ substates == \langle s\_Off3, s\_On4 \rangle,
\\ decomposition == CLUSTER,
\\ type == AND,
\\ history == \false \rblot\circblockend
\end{axdef}

\begin{axdef}
S\_SpeedValue: State
 \where 
S\_SpeedValue = \circblockbegin\lblot identifier == s\_SpeedValue,
\\ default == nulltransition.identifier,
\\ inner == nulltransition.identifier,
\\ outer == nulltransition.identifier,
\\ parent == s\_PowerOn,
\\ left == s\_FAN2,
\\ right == nullstate.identifier,
\\ substates == \langle  \rangle,
\\ decomposition == CLUSTER,
\\ type == AND,
\\ history == \false \rblot\circblockend
\end{axdef}

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

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

\begin{axdef}
S\_FAN1: State
 \where 
S\_FAN1 = \circblockbegin\lblot identifier == s\_FAN1,
\\ default == t\_default\_Off7,
\\ inner == nulltransition.identifier,
\\ outer == nulltransition.identifier,
\\ parent == s\_PowerOn,
\\ left == nullstate.identifier,
\\ right == s\_FAN2,
\\ substates == \langle s\_Off7, s\_On8 \rangle,
\\ decomposition == CLUSTER,
\\ type == AND,
\\ history == \false \rblot\circblockend
\end{axdef}

\begin{axdef}
S\_PowerOn: State
 \where 
S\_PowerOn = \circblockbegin\lblot identifier == s\_PowerOn,
\\ default == nulltransition.identifier,
\\ inner == nulltransition.identifier,
\\ outer == t\_PowerOn\_PowerOff,
\\ parent == c\_Controller,
\\ left == nullstate.identifier,
\\ right == nullstate.identifier,
\\ substates == \langle s\_FAN1, s\_FAN2, s\_SpeedValue \rangle,
\\ decomposition == SET,
\\ type == OR,
\\ history == \false \rblot\circblockend
\end{axdef}

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

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

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

\begin{axdef}
T\_PowerOff\_PowerOn: Transition
 \where 
T\_PowerOff\_PowerOn = \circblockbegin\lblot identifier == t\_PowerOff\_PowerOn,
\\ source == snode(s\_PowerOff),
\\ destination == snode(s\_PowerOn),
\\ next == nulltransition.identifier,
\\ parent == c\_Controller \rblot\circblockend
\end{axdef}

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

\begin{axdef}
T\_PowerOn\_PowerOff: Transition
 \where 
T\_PowerOn\_PowerOff = \circblockbegin\lblot identifier == t\_PowerOn\_PowerOff,
\\ source == snode(s\_PowerOn),
\\ destination == snode(s\_PowerOff),
\\ next == nulltransition.identifier,
\\ parent == c\_Controller \rblot\circblockend
\end{axdef}

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

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

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

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

\begin{axdef}
e\_SWITCH, e\_CLOCK: EVENT
\end{axdef}

\begin{circus}
\circchannel o\_airflow: \nat; i\_temp: \real
\end{circus}

\begin{circus}
\circprocess P\_Controller \circdef \circbegin\\
\end{circus}

\begin{axdef}
StateflowChart
 \where 
identifier = c\_Controller\\
states = \{(c\_Controller, C\_Controller), (s\_Off3, S\_Off3), (s\_On4, S\_On4), (s\_FAN2, S\_FAN2), (s\_SpeedValue, S\_SpeedValue), (s\_Off7, S\_Off7), (s\_On8, S\_On8), (s\_FAN1, S\_FAN1), (s\_PowerOn, S\_PowerOn), (s\_PowerOff, S\_PowerOff)\}\\
transitions = \{(t\_On8\_Off7, T\_On8\_Off7), (t\_Off7\_On8, T\_Off7\_On8), (t\_PowerOff\_PowerOn, T\_PowerOff\_PowerOn), (t\_default\_PowerOff, T\_default\_PowerOff), (t\_PowerOn\_PowerOff, T\_PowerOn\_PowerOff), (t\_On4\_Off3, T\_On4\_Off3), (t\_Off3\_On4, T\_Off3\_On4), (t\_default\_Off3, T\_default\_Off3), (t\_default\_Off7, T\_default\_Off7)\}\\
junctions = \{\}
\end{axdef}

\begin{schema}{SimulationInstance~}
v\_airflow: \nat\\
 v\_temp: \real
\end{schema}

\begin{schema}{InitSimulationInstance}
SimulationInstance~'
 \where 
v\_airflow' = 0\\
v\_temp' = 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 Controller\_state == (SimulationInstance~) \land (SimulationData~)
\end{circusaction}

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

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

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

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

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

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

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

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

\begin{circusaction}
entryaction\_PowerOff \circdef (executeentryaction.(s\_PowerOff) \then v\_airflow := 0)
\end{circusaction}

\begin{circusaction}
entryactions \circdef ( entryaction\_Off3\\
\extchoice\\
entryaction\_On4\\
\extchoice\\
entryaction\_FAN2\\
\extchoice\\
entryaction\_SpeedValue\\
\extchoice\\
entryaction\_Off7\\
\extchoice\\
entryaction\_On8\\
\extchoice\\
entryaction\_FAN1\\
\extchoice\\
entryaction\_PowerOn\\
\extchoice\\
entryaction\_PowerOff ) 
\end{circusaction}

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

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

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

\begin{circusaction}
duringaction\_SpeedValue \circdef (executeduringaction.(s\_SpeedValue)?ce \then v\_airflow := (b2r(state\_status(s\_On8)) + b2r(state\_status(s\_On4))))
\end{circusaction}

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

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

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

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

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

\begin{circusaction}
duringactions \circdef ( duringaction\_Off3\\
\extchoice\\
duringaction\_On4\\
\extchoice\\
duringaction\_FAN2\\
\extchoice\\
duringaction\_SpeedValue\\
\extchoice\\
duringaction\_Off7\\
\extchoice\\
duringaction\_On8\\
\extchoice\\
duringaction\_FAN1\\
\extchoice\\
duringaction\_PowerOn\\
\extchoice\\
duringaction\_PowerOff ) 
\end{circusaction}

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

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

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

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

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

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

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

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

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

\begin{circusaction}
exitactions \circdef ( exitaction\_Off3\\
\extchoice\\
exitaction\_On4\\
\extchoice\\
exitaction\_FAN2\\
\extchoice\\
exitaction\_SpeedValue\\
\extchoice\\
exitaction\_Off7\\
\extchoice\\
exitaction\_On8\\
\extchoice\\
exitaction\_FAN1\\
\extchoice\\
exitaction\_PowerOn\\
\extchoice\\
exitaction\_PowerOff ) 
\end{circusaction}

\begin{circusaction}
conditionaction\_On8\_Off7 \circdef (executeconditionaction.(t\_On8\_Off7) \then \Skip)
\end{circusaction}

\begin{circusaction}
conditionaction\_Off7\_On8 \circdef (executeconditionaction.(t\_Off7\_On8) \then \Skip)
\end{circusaction}

\begin{circusaction}
conditionaction\_PowerOff\_PowerOn \circdef (executeconditionaction.(t\_PowerOff\_PowerOn) \then \Skip)
\end{circusaction}

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

\begin{circusaction}
conditionaction\_PowerOn\_PowerOff \circdef (executeconditionaction.(t\_PowerOn\_PowerOff) \then \Skip)
\end{circusaction}

\begin{circusaction}
conditionaction\_On4\_Off3 \circdef (executeconditionaction.(t\_On4\_Off3) \then \Skip)
\end{circusaction}

\begin{circusaction}
conditionaction\_Off3\_On4 \circdef (executeconditionaction.(t\_Off3\_On4) \then \Skip)
\end{circusaction}

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

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

\begin{circusaction}
conditionactions \circdef ( conditionaction\_On8\_Off7\\
\extchoice\\
conditionaction\_Off7\_On8\\
\extchoice\\
conditionaction\_PowerOff\_PowerOn\\
\extchoice\\
conditionaction\_default\_PowerOff\\
\extchoice\\
conditionaction\_PowerOn\_PowerOff\\
\extchoice\\
conditionaction\_On4\_Off3\\
\extchoice\\
conditionaction\_Off3\_On4\\
\extchoice\\
conditionaction\_default\_Off3\\
\extchoice\\
conditionaction\_default\_Off7 ) 
\end{circusaction}

\begin{circusaction}
transitionaction\_On8\_Off7 \circdef (executetransitionaction.(t\_On8\_Off7) \then \Skip)
\end{circusaction}

\begin{circusaction}
transitionaction\_Off7\_On8 \circdef (executetransitionaction.(t\_Off7\_On8) \then \Skip)
\end{circusaction}

\begin{circusaction}
transitionaction\_PowerOff\_PowerOn \circdef (executetransitionaction.(t\_PowerOff\_PowerOn) \then \Skip)
\end{circusaction}

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

\begin{circusaction}
transitionaction\_PowerOn\_PowerOff \circdef (executetransitionaction.(t\_PowerOn\_PowerOff) \then \Skip)
\end{circusaction}

\begin{circusaction}
transitionaction\_On4\_Off3 \circdef (executetransitionaction.(t\_On4\_Off3) \then \Skip)
\end{circusaction}

\begin{circusaction}
transitionaction\_Off3\_On4 \circdef (executetransitionaction.(t\_Off3\_On4) \then \Skip)
\end{circusaction}

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

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

\begin{circusaction}
transitionactions \circdef ( transitionaction\_On8\_Off7\\
\extchoice\\
transitionaction\_Off7\_On8\\
\extchoice\\
transitionaction\_PowerOff\_PowerOn\\
\extchoice\\
transitionaction\_default\_PowerOff\\
\extchoice\\
transitionaction\_PowerOn\_PowerOff\\
\extchoice\\
transitionaction\_On4\_Off3\\
\extchoice\\
transitionaction\_Off3\_On4\\
\extchoice\\
transitionaction\_default\_Off3\\
\extchoice\\
transitionaction\_default\_Off7 ) 
\end{circusaction}

\begin{circusaction}
condition\_On8\_Off7 \circdef ( \circif ((v\_temp \alt 120) \neq 0) \circthen (evaluatecondition.(t\_On8\_Off7)!(\true) \then \Skip)
\\\circelse \lnot (((v\_temp \alt 120) \neq 0)) \circthen ((evaluatecondition.(t\_On8\_Off7)!(\false) \then \Skip))\\

\circfi ) 
\end{circusaction}

\begin{circusaction}
condition\_Off7\_On8 \circdef ( \circif ((v\_temp \ageq 120) \neq 0) \circthen (evaluatecondition.(t\_Off7\_On8)!(\true) \then \Skip)
\\\circelse \lnot (((v\_temp \ageq 120) \neq 0)) \circthen ((evaluatecondition.(t\_Off7\_On8)!(\false) \then \Skip))\\

\circfi ) 
\end{circusaction}

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

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

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

\begin{circusaction}
condition\_On4\_Off3 \circdef ( \circif ((v\_temp \alt 150) \neq 0) \circthen (evaluatecondition.(t\_On4\_Off3)!(\true) \then \Skip)
\\\circelse \lnot (((v\_temp \alt 150) \neq 0)) \circthen ((evaluatecondition.(t\_On4\_Off3)!(\false) \then \Skip))\\

\circfi ) 
\end{circusaction}

\begin{circusaction}
condition\_Off3\_On4 \circdef ( \circif ((v\_temp \ageq 150) \neq 0) \circthen (evaluatecondition.(t\_Off3\_On4)!(\true) \then \Skip)
\\\circelse \lnot (((v\_temp \ageq 150) \neq 0)) \circthen ((evaluatecondition.(t\_Off3\_On4)!(\false) \then \Skip))\\

\circfi ) 
\end{circusaction}

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

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

\begin{circusaction}
conditions \circdef ( condition\_On8\_Off7\\
\extchoice\\
condition\_Off7\_On8\\
\extchoice\\
condition\_PowerOff\_PowerOn\\
\extchoice\\
condition\_default\_PowerOff\\
\extchoice\\
condition\_PowerOn\_PowerOff\\
\extchoice\\
condition\_On4\_Off3\\
\extchoice\\
condition\_Off3\_On4\\
\extchoice\\
condition\_default\_Off3\\
\extchoice\\
condition\_default\_Off7 ) 
\end{circusaction}

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

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

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

\circfi ) )
\end{circusaction}

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

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

\circfi ) )
\end{circusaction}

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

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

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

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

\begin{circusaction}
triggers \circdef ( trigger\_On8\_Off7\\
\extchoice\\
trigger\_Off7\_On8\\
\extchoice\\
trigger\_PowerOff\_PowerOn\\
\extchoice\\
trigger\_default\_PowerOff\\
\extchoice\\
trigger\_PowerOn\_PowerOff\\
\extchoice\\
trigger\_On4\_Off3\\
\extchoice\\
trigger\_Off3\_On4\\
\extchoice\\
trigger\_default\_Off3\\
\extchoice\\
trigger\_default\_Off7 ) 
\end{circusaction}

\begin{circusaction}
getevents \circdef (events!(\langle e\_SWITCH, e\_CLOCK \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\_temp?x \then v\_temp := x))
\end{circusaction}

\begin{circusaction}
Outputs \circdef (write\_outputs \then (o\_airflow!(v\_airflow) \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 Controller \circdef (P\_Controller \lpar  interface \cup \lchanset end\_cycle \rchanset  \rpar Simulator)\circhide  interface
\end{circus}


