module ControlEquation =

process updateOrder =
   ( ? event clk_updateOrder;
       integer aSpeed;
     !
   )
   spec (| clk_updateOrder ^= aSpeed |)
   (| ControlEquation_orderedSpeed ::= aSpeed
    |);


process calculate =
   ( ? event clk_calculate;
       integer speed;
     ! dreal newTorque;
   )
   spec (| clk_calculate ^= speed ^= newTorque |)
   (| newTorque := atan(ControlEquation_regulatingCoefficient ? * dreal(ControlEquation_orderedSpeed ? - speed)) / 2.0
    |);


end;