module CONTROLLER_PAR (DEFINITIONS) is

process MC [REQ, INF: SigBoolChannel, CMD: SigChannel, LAMBDA, NU: none]
           (p0, p1, p2, p3, tr: Bool) is
   -- Master controller - parallel version
   var new_p0, new_p3, new_tr: Bool in
      new_p0 := p0;
      new_p3 := p3;
      new_tr := tr;
      par
         -- this thread possibly modifies new_p0
         if not (p0) then
            NU; -- Markov delay inserted here
            REQ (Add);
            INF (Present);
            new_p0 := true
         end if
      ||
         if p1 then
            CMD (Lock);
            INF (Locked);
            CMD (Drill);
            INF (Drilled);
            CMD (Unlock);
            INF (Unlocked)
         end if
      ||
         -- this thread possibly modifies new_tr
         if p2 then
            CMD (Test);
            INF (Tested, ?new_tr)
         end if
      ||
         -- this thread possibly modifies new_p3
         if p3 then
            REQ (Remove, tr);
            LAMBDA; -- Markov delay inserted here
            INF (Absent);
            new_p3 := false
         end if
      end par;
      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