module CONTROLLER_SEQ (DEFINITIONS) is

------------------------------------------------------------------------------

-- Master controller - sequential version

process MC [REQ, INF: SigBoolChannel, CMD: SigChannel, LAMBDA, NU: none] (p0, p1, p2, p3, tr: Bool) is
   var new_p0, new_p3, new_tr: Bool in
      if p0 then
         new_p0 := p0
      else
         NU; -- Markov delay inserted here
         REQ (Add);
         INF (Present);
         new_p0 := true
      end if;
      i; -- former LOTOS operator ">>"
      if p1 then
         CMD (Lock);
         INF (Locked);
         CMD (Drill);
         INF (Drilled);
         CMD (Unlock);
         INF (Unlocked)
      end if;
      i; -- former LOTOS operator ">>"
      if p2 then
         CMD (Test);
         var r: Bool in
            INF (Tested, ?r);
         new_tr := r
         end var
      else
         new_tr := tr
      end if;
      i; -- former LOTOS operator ">>"
      if p3 then
         REQ (Remove, tr);
         LAMBDA;  -- Markov delay inserted here
         INF (Absent);
         new_p3 := false
      else
         new_p3 := p3
      end if;
      i; -- former LOTOS operator ">>"
      CMD (Turn);
      INF (Turned);
      MC [REQ, INF, CMD, LAMBDA, NU] (new_p3, new_p0, p1, p2, new_tr)
   end var
end process

------------------------------------------------------------------------------
end module