\begin{circus}
  \circchannel\ [X] E : \universe[X]
\end{circus}
\vspace{-1ex}

\begin{circus}
  \circchannel\ end\_cycle
\end{circus}
\vspace{-1ex}

\begin{circus}
  \circchannel\ [X] In1 : \universe[X]
\end{circus}
\vspace{-1ex}

\begin{circus}
  \circchannel\ [X] Out1 : \universe[X]
\end{circus}
\vspace{-1ex}


\begin{circus}
  \circchannel\ [X] Diff\_Out : \universe[X]
\end{circus}
\vspace{-1ex}

\begin{circus}
  \circprocess\ [X] Diff \circdef \circbegin
\end{circus}
\vspace{-1ex}

\begin{circusaction}
   \circstate\ Diff\_State == [pid\_Diff\_UnitDelay\_St : \universe[X]]
\end{circusaction}
\vspace{-1ex}



\begin{schema}{pid\_Diff}
    In1?:\universe[X] ; Out1!:\universe[X] \\
    Sum:pid\_Diff\_Sum \\
    UnitDelay:pid\_Diff\_UnitDelay
\where
    (Sum.In1? = In1? 
    UnitDelay.In1? = Sum.In1? 
    Sum.In2? = UnitDelay.Out1! 
    Out1! = Sum.Out1!)
\end{schema}
\vspace{-1ex}

\begin{circusaction}
  pid\_Diff\_Sum \circdef
    \t1 Sum\_Pm
\end{circusaction}
\vspace{-1ex}

\begin{schema}{Init}
  Diff\_State~'
\where
  (\exists b :pid\_Diff\_UnitDelay @
    \t1 pid\_Diff\_UnitDelay\_St' = b.initial\_state)
\end{schema}
\vspace{-1ex}

\begin{schema}{Calc\_Diff}
    \Delta Diff\_State \\
    In1?, Out1!:\universe
\where
    \exists b:pid\_Diff @ \\
        \t1 b.In1?=In1? 
        \t1 \land b.Out1!=Out1! \\
        \t1 \land b.UnitDelay.state = pid\_Diff\_UnitDelay\_St \\
        \t1 \land b.UnitDelay.state'=pid\_Diff\_UnitDelay\_St' \\
\end{schema}
\vspace{-1ex}

\begin{circusaction}
  Calc\_Diff\_Out \circdef
    \t1 Calc\_Diff \circhide (pid\_Diff\_UnitDelay\_St') \land \Xi Diff\_State
\end{circusaction}
\vspace{-1ex}

\begin{circusaction}	
		Exec\_Diff\_out \circdef\\ 
		\t1 \circvar\ In1 : \universe \circspot\\
        \t2 E?x \then In1 := x \circseq\\
		\t2 \circvar\ Out1: \universe \circspot\\ 
		\t3 Calc\_Diff\_out \circseq
		\t3 Diff\_out!Out1 \then Skip
\end{circusaction}
\vspace{-1ex}

\begin{circusaction}
  Flows \circdef
    \t1 Exec\_Diff\_out
\end{circusaction}
\vspace{-1ex}

\begin{circusaction}
  Calc\_Diff\_St \circdef
    \t1 Calc\_Diff \circhide (Out1!)
\end{circusaction}
\vspace{-1ex}


\begin{circusaction}
  Diff\_StUpdt \circdef
    \t1 \circvar\ In1 : \universe \circspot\\
      \t2 E?x \then In1 := x \circseq\\
      \t2 Calc\_Diff\_St
\end{circusaction}
\vspace{-1ex}

\begin{circusaction}
  \circspot Init \circseq\\
    \t1 \circmu X \circspot (Flows \lpar \emptyset | \lchanset E \rchanset | 
	\t3 {pid\_Diff\_UnitDelay\_St} \rpar Diff\_StUpdt) \circseq\\
      \t2 end\_cycle \then X
\end{circusaction}
\vspace{-1ex}

\begin{circus}
  \circend
\end{circus}
\vspace{-1ex}


\begin{circus}
  \circprocess\ Sd \circdef \circbegin
\end{circus}
\vspace{-1ex}

\begin{circusaction}
  Calculate\_pid\_Sd\_out \circdef\\
    \t1 pid\_Sd\\
\end{circusaction}
\vspace{-1ex}

\begin{circusaction}
  Execute\_Sd\_out \circdef\\
    \t1 \circvar\ In1,In2 :\universe \circspot\\
      \t2 (Kd~?x \then In1 := x \linter In1 | In2 \rinter
      \t2 Diff\_out~?x \then In2 := x) 
	  \circseq\\
      \t2 (\circvar\ Out1 : \universe \circspot\\
        \t3 (Calculate\_pid\_Sd\_out \circseq\\
        \t3 pid\_Sd~!Out1 \then Skip))
\end{circusaction}
\vspace{-1ex}

\begin{circusaction}
  Flows \circdef\\
    \t1 Execute\_Sd\_out
\end{circusaction}
\vspace{-1ex}

\begin{circusaction}
  \circspot \circmu X \circspot (Flows) \circseq end\_cycle \then X
\end{circusaction}
\vspace{-1ex}

\begin{circus}
  \circend
\end{circus}
\vspace{-1ex}


\begin{circus}
  \circprocess\ [X] Int \circdef \circbegin
\end{circus}
\vspace{-1ex}

\begin{circusaction}
   \circstate\ Int\_State == [pid\_Int\_UnitDelay\_St : \universe[X]]
\end{circusaction}
\vspace{-1ex}


\begin{schema}{pid\_Int}
    In1?:\universe[X] ; Out1!:\universe[X] \\
    Sum:pid\_Int\_Sum \\
    UnitDelay:pid\_Int\_UnitDelay
\where
    (Sum.In1? = In1? \\
    UnitDelay.In1? = Sum.In1? \\
    Sum.In2? = UnitDelay.Out1! \\
    Out1! = Sum.Out1!)
\end{schema}
\vspace{-1ex}

\begin{circusaction}
  pid\_Int\_Sum \circdef\\
    \t1 Sum\_Pm
\end{circusaction}
\vspace{-1ex}

\begin{schema}{Init}
  Int\_State~'
\where
  (\exists b :pid\_Int\_UnitDelay @\\
    \t1 pid\_Int\_UnitDelay\_St' = b.initial\_state)
\end{schema}
\vspace{-1ex}

\begin{schema}{Calc\_Int}
    \Delta Int\_State \\
    In1?, Out1!:\universe\\
\where
    \exists b:pid\_Int @ \\
        \t1 b.In1?=In1? \\
        \t1 \land b.Out1!=Out1! \\
        \t1 \land b.UnitDelay.state = pid\_Int\_UnitDelay\_St \\
        \t1 \land b.UnitDelay.state'=pid\_Int\_UnitDelay\_St' \\
\end{schema}
\vspace{-1ex}

\begin{zed}
    Calc\_Int\_Out ==\\
	\t1 Calc\_Int \hide (pid\_Int\_UnitDelay\_St') \land \Xi Int\_State
\end{zed}
\vspace{-1ex}

\begin{circusaction}	
		Exec\_Int\_out \circdef\\ 
		\t1 (\circvar\ In1 : \universe \circspot\\
        \t2 E?x \then In1 := x \circseq\\
		\t2 \circvar\ Out1: \universe \circspot\\ 
		\t3 Calc\_Int\_out \circseq\\
		\t3 Int\_out!Out1 \then Skip)
\end{circusaction}
\vspace{-1ex}

\begin{circusaction}
  Flows \circdef\\
    \t1 Exec\_Int\_out
\end{circusaction}
\vspace{-1ex}

\begin{circusaction}
  Calc\_Int\_St \circdef\\
    \t1 Calc\_Int \circhide Out1!
\end{circusaction}
\vspace{-1ex}


\begin{circusaction}
  Int\_StUpdt \circdef\\
    \t1 (\circvar\ In1 : \universe \circspot\\
      \t2 E?x \then In1 := x \circseq\\
      \t2 Calc\_Int\_St)
\end{circusaction}
\vspace{-1ex}

\begin{circusaction}
  \circspot Init \circseq\\
    \t1 \circmu X \circspot (Flows \lpar \{ \} |  \lchanset E \rchanset  | 
	\t3 \{pid\_Int\_UnitDelay\_St\} \rpar Int\_StUpdt) \circseq\\
      \t2 end\_cycle \then X
\end{circusaction}
\vspace{-1ex}


\begin{circus}
  \circend
\end{circus}
\vspace{-1ex}

\begin{circus}
  \circprocess\ Si \circdef \circbegin
\end{circus}
\vspace{-1ex}

\begin{circusaction}
  Calculate\_pid\_Si\_out \circdef\\
    \t1 pid\_Si\\
\end{circusaction}
\vspace{-1ex}

\begin{circusaction}
  Execute\_Si\_out \circdef\\
    \t1 \circvar\ In1,In2 :\universe \circspot\\
      \t2 (E~?x \then In1 := x \linter In1 | In2 \rinter
      \t2 Ki~?x \then In2 := x) \circseq\\
      \t2 (\circvar\ Out1 : \universe \circspot\\
        \t3 Calculate\_pid\_Si\_out \circseq\\
        \t3 Si\_out~!Out1 \then Skip)
\end{circusaction}
\vspace{-1ex}

\begin{circusaction}
  Flows \circdef\\
    \t1 Execute\_Si\_out
\end{circusaction}
\vspace{-1ex}

\begin{circusaction}
  \circspot \circmu X \circspot (Flows) \circseq end\_cycle \then X
\end{circusaction}
\vspace{-1ex}

\begin{circus}
  \circend
\end{circus}
\vspace{-1ex}

\begin{circus}
  \circprocess\ Sp \circdef \circbegin
\end{circus}
\vspace{-1ex}

\begin{circusaction}
  Calculate\_pid\_Sp\_out \circdef\\
    \t1 pid\_Sp\\
\end{circusaction}
\vspace{-1ex}

\begin{circusaction}
  Execute\_Sp\_out \circdef\\
    \t1 \circvar\ In1,In2 :\universe \circspot\\
      \t2 (E~?x \then In1 := x \linter In1 | In2 \rinter
      \t2 Kp~?x \then In2 := x) \circseq\\
      \t2 (\circvar\ Out1 : \universe \circspot\\
        \t3 Calculate\_pid\_Sp\_out \circseq\\
        \t3 Sp\_out~!Out1 \then Skip)
\end{circusaction}
\vspace{-1ex}

\begin{circusaction}
  Flows \circdef\\
    \t1 Execute\_Sp\_out
\end{circusaction}
\vspace{-1ex}

\begin{circusaction}
  \circspot \circmu X \circspot (Flows) \circseq end\_cycle \then X
\end{circusaction}
\vspace{-1ex}

\begin{circus}
  \circend
\end{circus}
\vspace{-1ex}

\begin{circus}
  \circprocess\ Sum \circdef \circbegin
\end{circus}
\vspace{-1ex}

\begin{circusaction}
  Calculate\_pid\_Sum\_out \circdef\\
    \t1 pid\_Sum\\
\end{circusaction}
\vspace{-1ex}

\begin{circusaction}
  Execute\_Y \circdef\\
    \t1 \circvar\ In1,In2,In3 :\universe \circspot\\
      \t2 (Sd\_out~?x \then In1 := x \linter In1 | In2 \rinter
      \t2 (Sp\_out~?x \then In2 := x
      \t2  \linter In2 | In3  \rinter	  
	  \t2 Int\_out~?x \then In3 := x)) \circseq\\
      \t2 (\circvar\ Out1 : \universe \circspot\\
        \t3 Calculate\_pid\_Sum\_out \circseq\\
        \t3 Y~!Out1 \then Skip)
\end{circusaction}
\vspace{-1ex}

\begin{circusaction}
  Flows \circdef\\
    \t1 Execute\_Y
\end{circusaction}
\vspace{-1ex}

\begin{circusaction}
  \circspot \circmu X \circspot (Flows) \circseq end\_cycle \then X
\end{circusaction}
\vspace{-1ex}

\begin{circus}
  \circend
\end{circus}
\vspace{-1ex}

\begin{circus}
  \circprocess\ PID \circdef\ \\
 %%%%%% \t1 (Si \lpar E, Ki, Si\_out, end\_cycle \lchanset E,end_cycle \rchanset E, Diff\_out, end\_cycle \rpar Diff)
 \t1 (Diff\_Sd \lpar  \lchanset E, Ki, Kd, Si\_out, end\_cycle,Diff\_out,Int\_out \rchanset \rpar (Int\_Si
      \lpar  \lchanset E, Kp, Sd\_out, Int\_out, Sp\_out, Y, end\_cycle, Si\_out \rchanset \rpar Sp\_Sum))
	 \circhide \lchanset Si\_out, Diff\_out, Sd\_out, Sp\_out \rchanset

\end{circus}






