\documentclass{article}

\usepackage[bmargin=2cm,tmargin=2cm,lmargin=1cm,rmargin=1cm,landscape,a4paper]{geometry}
\usepackage{circus}
\usepackage{stateflow}


\begin{document}
\setlength{\zedindent}{.5cm}
\begin{zsection}\\
\SECTION Air\_impl \parents circus\_toolkit,basic\_toolkit
\end{zsection}\\
\vspace{-1cm}
\begin{zed}
Air\_IN\_NO\_ACTIVE\_CHILD == 0\\
Air\_IN\_Off == 1\\
Air\_IN\_On == 2\\
Air\_IN\_PowerOff == 1\\
Air\_IN\_PowerOn == 2\\
Air\_event\_CLOCK == 1\\
Air\_event\_SWITCH == 0\\
CALL\_EVENT == \negate 1\\
\end{zed}
\vspace{-1cm}
\begin{zed}
BlockIO\_Air == [airflow:\nat]
\end{zed}
%
\begin{schema}{D\_Work\_Air}
is\_active\_c1\_Air:\nat\\
is\_c1\_Air:\nat\\
is\_active\_FAN2:\nat\\
is\_FAN2:\nat\\
is\_active\_SpeedValue:\nat\\
is\_active\_FAN1:\nat\\
is\_FAN1:\nat\\
\end{schema}
%
\begin{zed}
ExternalInputs\_Air == [temp:\real;  inputevents:\seq\boolean]\\
ExternalOutputs\_Air == [airflow:\nat]
\end{zed}
%
\begin{axdef}
is\_active\_c1\_Air: D\_Work\_Air \cross \nat \fun D\_Work\_Air
\where
\forall b: D\_Work\_Air; v:\nat @ is\_active\_c1\_Air(b,v) = \lblot is\_active\_c1\_Air == v, is\_c1\_Air == b.is\_c1\_Air, is\_active\_FAN2 == b.is\_active\_FAN2,\\\t1
is\_FAN2 == b.is\_FAN2, is\_active\_SpeedValue == b.is\_active\_SpeedValue, is\_active\_FAN1 == b.is\_active\_FAN1, is\_FAN1 == b.is\_FAN1 \rblot\\
\end{axdef}
%
\begin{axdef}
is\_c1\_Air: D\_Work\_Air \cross \nat \fun D\_Work\_Air
\where
\forall b: D\_Work\_Air; v:\nat @ is\_c1\_Air(b,v) = \lblot is\_active\_c1\_Air ==  b.is\_active\_c1\_Air, is\_c1\_Air == v, is\_active\_FAN2 == b.is\_active\_FAN2,\\\t1
is\_FAN2 == b.is\_FAN2, is\_active\_SpeedValue == b.is\_active\_SpeedValue, is\_active\_FAN1 == b.is\_active\_FAN1, is\_FAN1 == b.is\_FAN1 \rblot\\
\end{axdef}
%
\begin{axdef}
is\_active\_FAN2: D\_Work\_Air \cross \nat \fun D\_Work\_Air
\where
\forall b: D\_Work\_Air; v:\nat @ is\_active\_FAN2(b,v) = \lblot is\_active\_c1\_Air ==  b.is\_active\_c1\_Air, is\_c1\_Air == b.is\_c1\_Air, is\_active\_FAN2 == v,\\\t1
is\_FAN2 == b.is\_FAN2, is\_active\_SpeedValue == b.is\_active\_SpeedValue, is\_active\_FAN1 == b.is\_active\_FAN1, is\_FAN1 == b.is\_FAN1 \rblot\\
\end{axdef}
%
\begin{axdef}
is\_FAN2: D\_Work\_Air \cross \nat \fun D\_Work\_Air
\where
\forall b: D\_Work\_Air; v:\nat @ is\_FAN2(b,v) = \lblot is\_active\_c1\_Air ==  b.is\_active\_c1\_Air, is\_c1\_Air == b.is\_c1\_Air, is\_active\_FAN2 == b.is\_active\_FAN2,\\\t1
is\_FAN2 == v, is\_active\_SpeedValue == b.is\_active\_SpeedValue, is\_active\_FAN1 == b.is\_active\_FAN1, is\_FAN1 == b.is\_FAN1 \rblot\\
\end{axdef}
%
\begin{axdef}
is\_active\_SpeedValue: D\_Work\_Air \cross \nat \fun D\_Work\_Air
\where
\forall b: D\_Work\_Air; v:\nat @ is\_active\_SpeedValue(b,v) = \lblot is\_active\_c1\_Air ==  b.is\_active\_c1\_Air, is\_c1\_Air == b.is\_c1\_Air,\\\t1
 is\_active\_FAN2 == b.is\_active\_FAN2, is\_FAN2 == b.is\_FAN2, is\_active\_SpeedValue == v, is\_active\_FAN1 == b.is\_active\_FAN1,\\\t1
 is\_FAN1 == b.is\_FAN1 \rblot\\
\end{axdef}
%
\begin{axdef}
is\_active\_FAN1: D\_Work\_Air \cross \nat \fun D\_Work\_Air
\where
\forall b: D\_Work\_Air; v:\nat @ is\_active\_FAN1(b,v) = \lblot is\_active\_c1\_Air ==  b.is\_active\_c1\_Air, is\_c1\_Air == b.is\_c1\_Air,\\\t1
 is\_active\_FAN2 == b.is\_active\_FAN2, is\_FAN2 == b.is\_FAN2, is\_active\_SpeedValue == b.is\_active\_SpeedValue, is\_active\_FAN1 == v,\\\t1
 is\_FAN1 == b.is\_FAN1 \rblot\\
\end{axdef}
%
\begin{axdef}
is\_FAN1: D\_Work\_Air \cross \nat \fun D\_Work\_Air
\where
\forall b: D\_Work\_Air; v:\nat @ is\_FAN1(b,v) = \lblot is\_active\_c1\_Air ==  b.is\_active\_c1\_Air, is\_c1\_Air == b.is\_c1\_Air,\\\t1
is\_active\_FAN2 == b.is\_active\_FAN2, is\_FAN2 == b.is\_FAN2, is\_active\_SpeedValue == b.is\_active\_SpeedValue,\\\t1
 is\_active\_FAN1 == b.is\_active\_FAN1, is\_FAN1 == v \rblot\\
\end{axdef}
%
\begin{axdef}
airflow: BlockIO\_Air \cross \nat \fun BlockIO\_Air
\where
\forall b: BlockIO\_Air; v: \nat @ airflow(b,v) = \lblot airflow == v\rblot
\end{axdef}
%
\begin{axdef}
temp: ExternalInputs\_Air \cross \real \fun ExternalInputs\_Air
\where
\forall b: ExternalInputs\_Air; v: \real @ temp(b,v) = \lblot temp == v, inputevents == b.inputevents \rblot
\end{axdef}
%
\begin{axdef}
inputevents: ExternalInputs\_Air \cross (\seq \boolean) \fun ExternalInputs\_Air
\where
\forall b: ExternalInputs\_Air; v: \seq\boolean @ inputevents(b,v) = \lblot temp == b.temp, inputevents == v \rblot
\end{axdef}

%
\begin{schema}{Air\_state}
	\_sfEvent\_Air\_:\num\\
	Air\_B:BlockIO\_Air\\
	Air\_DWork: D\_Work\_Air\\
	Air\_U: ExternalInputs\_Air\\
	Air\_Y: ExternalOutputs\_Air
\end{schema}
%
\begin{circus}
\circchannel in\_FAN1: Air\_state\\
\circchannel out\_FAN1: \nat\\
\circchannel input\_event: (\seq \boolean)\\
\circchannel i\_temp: \real\\
\circchannel o\_airflow: \nat
\end{circus}
%
\begin{circus}
\circprocess Air \circdef \circbegin
\end{circus}
%
\begin{circusaction}
\circstate Air\_state
\end{circusaction}
%
\begin{circusaction}
Air\_FAN1 \circdef\\
\circblockbegin
	\circvar Air\_B:BlockIO\_Air; Air\_DWork: D\_Work\_Air; Air\_U: ExternalInputs\_Air; Air\_Y: ExternalOutputs\_Air; \_sfEvent\_Air\_:\num \circspot\\
	in\_FAN1?s \then Air\_B,Air\_DWork,Air\_U,Air\_Y,\_sfEvent\_Air\_:=s.Air\_B,s.Air\_DWork,s.Air\_U,s.Air\_Y,s.\_sfEvent\_Air\_\circseq\\
	\circblockbegin
	\circif Air\_DWork.is\_FAN1 = Air\_IN\_Off \circthen\\
		\circblockbegin
		\circif Air\_U.temp \geq 120 \circthen Air\_DWork := is\_FAN1(Air\_DWork,Air\_IN\_On)\\
		\circelse \lnot (Air\_U.temp \geq 120) \circthen \Skip\\
		\circfi
		\circblockend\\
	\circelse Air\_DWork.is\_FAN1 = Air\_IN\_On \circthen\\
		\circblockbegin
		\circif Air\_U.temp < 120 \circthen Air\_DWork := is\_FAN1(Air\_DWork,Air\_IN\_Off)\\
		\circelse \lnot(Air\_U.temp < 120) \circthen \Skip\\
		\circfi
		\circblockend\\
	\circelse \lnot (Air\_DWork.is\_FAN1 = Air\_IN\_Off \lor Air\_DWork.is\_FAN1 = Air\_IN\_On) \circthen\\\t1
		Air\_DWork := is\_FAN1(Air\_DWork,Air\_IN\_Off)\\
	\circfi
	\circblockend\circseq\\
	out\_FAN1!(Air\_DWork.is\_FAN1) \then \Skip
\circblockend
\end{circusaction}
%
\begin{circusaction}
Air\_chartstep\_c1\_Air \circdef\\
\circblockbegin
	\circif Air\_DWork.is\_active\_c1\_Air = 0 \circthen
		\circblockbegin
		Air\_DWork  := is\_active\_c1\_Air(Air\_DWork,1)\circseq\\
		Air\_DWork  := is\_c1\_Air(Air\_DWork,Air\_IN\_PowerOff)\circseq
		Air\_B := airflow(Air\_B,0)
		\circblockend\\
	\circelse \lnot (Air\_DWork.is\_active\_c1\_Air = 0) \circthen\\
		\circblockbegin
		\circif Air\_DWork.is\_c1\_Air = Air\_IN\_PowerOff \circthen
			\circblockbegin
			\circif \_sfEvent\_Air\_ = Air\_event\_SWITCH \circthen\\
				\circblockbegin
				Air\_DWork := is\_c1\_Air(Air\_DWork,Air\_IN\_PowerOn)\circseq\\
				Air\_DWork := is\_active\_FAN1(Air\_DWork,1)\circseq\\
				Air\_DWork := is\_FAN1(Air\_DWork,Air\_IN\_Off)\circseq\\
				Air\_DWork := is\_active\_FAN2(Air\_DWork,1)\circseq\\
				Air\_DWork := is\_FAN2(Air\_DWork,Air\_IN\_Off)\circseq\\
				Air\_DWork := is\_active\_SpeedValue(Air\_DWork,1)
				\circblockend\\
			\circelse \lnot(\_sfEvent\_Air\_ = Air\_event\_SWITCH) \circthen \Skip\\
			\circfi
			\circblockend\\
		\circelse Air\_DWork.is\_c1\_Air = Air\_IN\_PowerOn \circthen\\
			\circblockbegin
			\circif \_sfEvent\_Air\_ = Air\_event\_SWITCH \circthen
				\circblockbegin
				Air\_DWork := is\_active\_SpeedValue(Air\_DWork,0)\circseq\\
				Air\_DWork := is\_FAN2(Air\_DWork,Air\_IN\_NO\_ACTIVE\_CHILD)\circseq\\
				Air\_DWork := is\_active\_FAN2(Air\_DWork,0)\circseq\\
				Air\_DWork := is\_FAN1(Air\_DWork,Air\_IN\_NO\_ACTIVE\_CHILD)\circseq\\
				Air\_DWork := is\_active\_FAN1(Air\_DWork,0)\circseq\\
				Air\_DWork := is\_c1\_Air(Air\_DWork,Air\_IN\_PowerOff)\circseq
				Air\_B := airflow(Air\_B,0)
				\circblockend\\
			\circelse \lnot(\_sfEvent\_Air\_ = Air\_event\_SWITCH) \circthen\\
				\circblockbegin
				in\_FAN1!(\theta Air\_state) \then \Skip\circseq\\
				\circblockbegin
				\circif Air\_DWork.is\_FAN2 = Air\_IN\_Off \circthen
					\circblockbegin
					\circif Air\_U.temp \geq 150 \circthen Air\_DWork := is\_FAN2(Air\_DWork,Air\_IN\_On)\\
					\circelse \lnot(Air\_U.temp \geq 150) \circthen \Skip\\
					\circfi
					\circblockend\\
				\circelse Air\_DWork.is\_FAN2 = Air\_IN\_On \circthen
					\circblockbegin
					\circif Air\_U.temp < 150 \circthen Air\_DWork := is\_FAN2(Air\_DWork,Air\_IN\_Off)\\
					\circelse \lnot (Air\_U.temp < 150) \circthen \Skip\\
					\circfi
					\circblockend\\
				\circelse \lnot (Air\_DWork.is\_FAN2 = Air\_IN\_Off \lor Air\_DWork.is\_FAN2 = Air\_IN\_On) \circthen
			          		Air\_DWork := is\_FAN2(Air\_DWork,Air\_IN\_Off)\\
				\circfi
				\circblockend\circseq\\
				out\_FAN1?f1 \then Air\_DWork  := is\_FAN1(Air\_DWork,f1)\circseq\\
				Air\_B := airflow(Air\_B,(\IF~Air\_DWork.is\_FAN1 = Air\_IN\_On \THEN~1\ELSE~0) +
				          (\IF~Air\_DWork.is\_FAN2 = Air\_IN\_On \THEN~1\ELSE~0))\\
				\circblockend\\
			\circfi
			\circblockend\\
		\circelse \lnot (Air\_DWork.is\_c1\_Air = Air\_IN\_PowerOff \lor Air\_DWork.is\_c1\_Air = Air\_IN\_PowerOn) \circthen\\\t1
			Air\_DWork  := is\_c1\_Air(Air\_DWork,Air\_IN\_PowerOff)\circseq Air\_B := airflow(Air\_B,0)\\
		\circfi\\
		\circblockend\\
	\circfi
\circblockend
\end{circusaction}
%
\begin{circusaction}
Air\_output \circdef\\
\circblockbegin
	\circblockbegin
	\circif Air\_U.inputevents(1) = \true \circthen\\\t1
		\_sfEvent\_Air\_ := Air\_event\_SWITCH\circseq Air\_chartstep\_c1\_Air\\
	\circelse \lnot (Air\_U.inputevents(1) = \true) \circthen \Skip\\
	\circfi
	\circblockend\circseq\\
	\circblockbegin
	\circif Air\_U.inputevents(2) = \true \circthen\\\t1
		\_sfEvent\_Air\_ := Air\_event\_CLOCK\circseq Air\_chartstep\_c1\_Air\\
	\circelse \lnot (Air\_U.inputevents(2) = \true) \circthen \Skip\\
	\circfi
	\circblockend\circseq\\
	Air\_Y := Air\_B
\circblockend
\end{circusaction}
%
\begin{circusaction}
MdlInitialize \circdef\\
\circblockbegin
	\_sfEvent\_Air\_ := CALL\_EVENT\circseq\\
	Air\_DWork := is\_active\_FAN1(Air\_DWork,0)\circseq\\
	Air\_DWork := is\_FAN1(Air\_DWork,0)\circseq\\
	Air\_DWork := is\_active\_FAN2(Air\_DWork,0)\circseq\\
	Air\_DWork := is\_FAN2(Air\_DWork,0)\circseq\\
	Air\_DWork := is\_active\_SpeedValue(Air\_DWork,0)\circseq\\
	Air\_DWork := is\_active\_c1\_Air(Air\_DWork,0)\circseq\\
	Air\_DWork := is\_c1\_Air(Air\_DWork,0)\circseq\\
	Air\_B := airflow(Air\_B,0)
\circblockend
\end{circusaction}
%
\begin{circusaction}
FAN1 \circdef \circmu X \circspot Air\_FAN1
\end{circusaction}
%
\begin{circusaction}
read\_inputs \circdef
\circblockbegin
	input\_event?es \then Air\_U:=inputevents(Air\_U,es)\circseq\\
	i\_temp?v \then Air\_U:=temp(Air\_U,v)
\circblockend
\end{circusaction}
%
\begin{circusaction}
write\_outputs \circdef o\_airflow!(Air\_Y.airflow) \then \Skip
\end{circusaction}
%
\begin{circusaction}
ExecuteChart \circdef MdlInitialize\circseq (\circmu X \circspot read\_inputs\circseq Air\_output\circseq write\_outputs\circseq end\_cycle \then X)
\end{circusaction}
%
\begin{circusaction}
\circspot ExecuteChart \lpar \{\_sfEvent\_Air\_,Air\_U,Air\_B,Air\_DWork,Air\_Y\} | \lchanset in\_FAN1, out\_FAN1 \rchanset | \{\} \rpar FAN1
\end{circusaction}
%
\begin{circus}
\circend
\end{circus}

\end{document} 