module COMPONENTS (DEFINITIONS) is

-- Physical components and their controllers

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

process TT [TT1, TT2, TT3, TurnOn, ADD, REM: none, MU: SigChannel] (p0, p1, p2, p3: Bool) is
   -- Turntable
   alt
      TurnOn;
      MU (Turned); -- Markov delay inserted here
      TT2;
      TT [TT1, TT2, TT3, TurnOn, ADD, REM, MU] (p3, p0, p1, p2)
   []
      only if not (p0) then
         ADD;
         TT1;
         TT [TT1, TT2, TT3, TurnOn, ADD, REM, MU] (true, p1, p2, p3)
      end if
   []
      only if p3 then
         REM;
         TT3;
         TT [TT1, TT2, TT3, TurnOn, ADD, REM, MU] (p0, p1, p2, false)
      end if
   end alt
end process

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

process TTC [TT1, TT2, TT3, TurnOn: none, INF: SigBoolChannel, CMD: SigChannel] is
   -- Controller
   loop
      alt
         TT1;
         INF (Present)
      []
         CMD (Turn);
         TurnOn;
         TT2;
         INF (Turned)
      []
         TT3;
         INF (Absent)
      end alt
   end loop
end process

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

process D [D1, D2, DUpDown, DOnOff: none, MU: SigChannel] (mode, pos: Bool) is
   -- Drill
   alt
      DOnOff;
      D [D1, D2, DUpDown, DOnOff, MU] (not (mode), pos)
   []
      only if mode then
         DUpDown;
         if pos then
            D2;
            D [D1, D2, DUpDown, DOnOff, MU] (mode, not (pos))
         else
            MU (Drilled); -- Markov delay inserted here
            D1;
            D [D1, D2, DUpDown, DOnOff, MU] (mode, not (pos))
         end if
      end if
   end alt
end process

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

process DC [D1, D2, DUpDown, DOnOff: none, INF: SigBoolChannel, CMD: SigChannel] is
   -- Controller
   loop
      CMD (Drill);
      DOnOff;
      DUpDown;
      D2;
      DUpDown;
      D1;
      DOnOff;
      INF (Drilled)
   end loop
end process

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

process C [C1, C2, COnOff: none] (locked: Bool) is
   -- Clamp
   COnOff;
   if locked then
      C1
   else
      C2
   end if;
   C [C1, C2, COnOff] (not (locked))
end process

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

process CC [C1, C2, COnOff: none, INF: SigBoolChannel, CMD: SigChannel] is
   -- Controller
   loop
      CMD (Lock);
      COnOff;
      C2;
      INF (Locked);
      CMD (Unlock);
      COnOff;
      C1;
      INF (Unlocked)
   end loop
end process

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

process T [T1, T2, TUpDown: none, MU: SigChannel] (up: Bool) is
   -- Tester
   TUpDown;
   if up then
      alt
         -- Good product
         T2
      []
         -- Bad product
         null
      end alt
   else
      MU (Tested); -- Markov delay inserted here
      T1
   end if;
   T [T1, T2, TUpDown, MU] (not (up))
end process

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

process TC [T1, T2, TUpDown: none, INF: SigBoolChannel, CMD: SigChannel] is
   -- Controller
   loop
      CMD (Test);
      TUpDown;
      alt
         -- Good product
         T2;
         TUpDown;
         T1;
         INF (Tested, true)
      []
         -- Bad product
         TUpDown;
         T1;
         INF (Tested, false)
      end alt
   end loop
end process

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

process Env [REQ: SigBoolChannel, ADD, REM, ERR: none] is
   -- Environment
   loop
      alt
         REQ (Add of Sig);
         ADD
      []
         var r: Bool in
            REQ (Remove, ?r);
            if not (r) then
               ERR
            end if;
            REM
         end var
      end alt
   end loop
end process

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

end module