module cim is

-- Computer Integrated Manufacturing (CIM) Architecture

------------------------------------------------------------------------------
-- type definitions
------------------------------------------------------------------------------

type Cmd is
   READ, DELIVER
end type

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

type Raw is
   R (N: nat)
   with ==, !=, get
end type

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

function RType (R: Raw): nat is
   return R.N
end function

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

type Prd is
   P (N: nat)
   with ==, !=, get
end type

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

function PType (P: Prd): nat is
   return P.N
end function

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

type RQueue is
   nil, append (RQ: RQueue, R: Raw)
   with ==, get
end type

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

function empty (RQ: RQueue): bool is
   return RQ == nil
end function

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

function head (RQ1: RQueue): Raw is
   case RQ1
      var R: Raw, RQ2: RQueue
   in
         nil -> raise UNEXPECTED
      |  append (nil, R) -> return R
      |  append (RQ2, any Raw) -> return head (RQ2)
   end case
end function

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

function tail (RQ1: RQueue): RQueue is
   case RQ1
      var R: Raw, RQ2: RQueue
   in
         nil -> raise UNEXPECTED
      |  append (nil, any Raw) -> return nil
      |  append (RQ2, R) -> return append (tail (RQ2), R)
   end case
end function

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

type PQueue is
   nil, append (PQ: PQueue, P: Prd)
   with ==, get
end type

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

function empty (PQ: PQueue): bool is
   return PQ == nil
end function

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

function head (PQ1: PQueue): Prd is
   case PQ1
      var P: Prd, PQ2: PQueue
   in
         nil -> raise UNEXPECTED
      |  append (nil, P) -> return P
      |  append (PQ2, any Prd) -> return head (PQ2)
   end case
end function

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

function tail (PQ1: PQueue): PQueue is
   case PQ1
      var P: Prd, PQ2: PQueue
   in
         nil -> raise UNEXPECTED
      |  append (nil, any Prd) -> return nil
      |  append (PQ2, P) -> return append (tail (PQ2), P)
   end case
end function

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

type PrdStock is
   nil, cons (P: Prd, N: Nat, PS: PrdStock)
   with get
end type

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

function GetQty (P: Prd, PS: PrdStock): Nat is
   if P == PS.P then
      return PS.N
   else
      return GetQty (P, PS.PS)
   end if
end function

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

function SetQty (P: Prd, N: Nat, PS: PrdStock): PrdStock is
   if P == PS.P then
      return cons (P, N, PS.PS)
   else
      return cons (PS.P, PS.N, SetQty (P, N, PS.PS))
   end if
end function

------------------------------------------------------------------------------
-- channel definitions
------------------------------------------------------------------------------

channel Nat1Channel is
   (N: Nat)
end channel

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

channel Nat2Channel is
   (N1, N2: Nat)
end channel

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

channel CmdChannel is
   (C: Cmd, PS: PrdStock),
   (C: Cmd, N1, N2: Nat)
end channel

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

channel RawChannel is
   (R: Raw)
end channel

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

channel NatRawChannel is
   (N: Nat, R: Raw)
end channel

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

channel PrdChannel is
   (P: Prd)
end channel

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

channel PrdNatChannel is
   (P: Prd, N: Nat)
end channel

------------------------------------------------------------------------------
-- process definitions
------------------------------------------------------------------------------

process MAIN [REQUEST: Nat2Channel, INPUT: Nat1Channel, OUTPUT: PrdNatChannel,
              CMD_SU: Nat2Channel, CMD_ST: CmdChannel, CMD: Nat2Channel,
              RDY: Nat1Channel, GET: RawChannel, PUT: PrdChannel,
              WIN: NatRawChannel, WOUT: PrdChannel] is
   par CMD, RDY, CMD_SU, CMD_ST in
      Controller [CMD, RDY, CMD_SU, CMD_ST, REQUEST]
   ||
      par WIN, WOUT, GET, PUT in
         par
            RawBelt [WIN, GET] (nil of RQueue)
         ||
            PrdBelt [WOUT, PUT] (nil of PQueue)
         end par
      ||
         par
            Supply [CMD_SU, INPUT, GET]
         ||
            Store [CMD_ST, OUTPUT, PUT] (cons (P (1 of nat), 2 of nat, cons (P (2 of nat), 2 of nat, cons (P (3 of nat), 2 of nat, nil of PrdStock))))
         ||
            Workcell [CMD, RDY, WIN, WOUT] (1 of nat)
         ||
            Workcell [CMD, RDY, WIN, WOUT] (2 of nat)
         ||
            Workcell [CMD, RDY, WIN, WOUT] (3 of nat)
         end par
      end par
   end par
end process

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

process Controller [CMD: Nat2Channel, RDY: Nat1Channel, CMD_SU: Nat2Channel,
                    CMD_ST: CmdChannel, REQUEST: Nat2Channel] is
   var PrType, Qty, Q:Nat, Stock:PrdStock in
      loop
         REQUEST (?PrType, ?Qty) where (PrType >= 1) and (PrType <= 3) and
                                       (Qty >= 1) and (Qty <= 2);
         CMD_ST (READ, ?Stock);
         Q := GetQty (P (PrType), Stock);
         if Q < Qty then
            CMD (PrType, Qty - Q);
            CMD_SU (PrType, Qty - Q);
            RDY (PrType)
         end if;
         CMD_ST (DELIVER, PrType, Qty)
      end loop
   end var
end process

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

process RawBelt [WIN: NatRawChannel, GET: RawChannel] (in var RQ: RQueue) is
   -- Raw material transport belt
   var PrType: Nat, R: Raw in
      loop
         alt
            only if not (empty (RQ)) then
               WIN (?PrType, head(RQ)) where (RType (head (RQ)) == PrType);
               RQ := tail(RQ)
            end if
         []
            GET (?R);
            RQ := append (RQ, R)
         end alt
      end loop
   end var
end process

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

process PrdBelt [WOUT:PrdChannel, PUT:PrdChannel] (in var PQ:PQueue) is
   -- Product transport belt
   var P:Prd in
      loop
         alt
            only if not (empty (PQ)) then
               PUT (head (PQ));
               PQ := tail (PQ)
            end if
         []
            WOUT (?P);
            PQ := append (PQ, P)
         end alt
      end loop
   end var
end process

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

process Supply [CMD_SU:Nat2Channel, INPUT:Nat1Channel, GET:RawChannel] is
   -- Raw material supply
   var State: Bool, PrType, Qty: Nat in
      State := false;
      PrType := 0;  -- to suppress a data-flow error
      Qty := 0;     -- to suppress a data-flow error
      loop
         case State in
            false ->
               CMD_SU (?PrType, ?Qty);
               State := true
         |  true ->
               if Qty > 0 then
                  INPUT (PrType);
                  GET (R (PrType));
                  Qty := Qty - 1
                  -- State := true
               else
                  State := false
               end if
         end case
      end loop
   end var
end process

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

process Store [CMD_ST: CmdChannel, OUTPUT: PrdNatChannel, PUT: PrdChannel]
              (in var Stock: PrdStock) is
   -- Product store
   var P: Prd, PrType, Qty: Nat in
      loop
         alt
            CMD_ST (READ, Stock)
         []
            CMD_ST (DELIVER, ?PrType, ?Qty) where (Qty <= GetQty (P (PrType), Stock));
            OUTPUT (P (PrType), Qty);
            Stock := SetQty (P (PrType), GetQty (P (PrType), Stock) - Qty, Stock)
         []
            PUT (?P);
            Stock := SetQty (P, GetQty (P, Stock) + 1, Stock)
         end alt
      end loop
   end var
end process

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

process Workcell [CMD: Nat2Channel, RDY: Nat1Channel, WIN: NatRawChannel,
                  WOUT:PrdChannel] (PrType:Nat) is
   hide CMD_A: Nat1Channel, RDY_A: none, CMD_B: Nat1Channel, RDY_B: none,
        TR: none, AR: none, GET_A: PrdChannel, PUT_B: PrdChannel in
      par GET_A, PUT_B, TR, AR in
         par CMD_A, RDY_A, CMD_B, RDY_B in
            WCC [CMD, RDY, CMD_A, RDY_A, CMD_B, RDY_B, TR, AR] (PrType)
         ||
            par
               WSA [CMD_A, RDY_A, WIN, GET_A] (PrType)
            ||
               WSB [CMD_B, RDY_B, PUT_B, WOUT]
            end par
         end par
      ||
         WCT [GET_A, PUT_B, TR, AR] (nil of PQueue)
      end par
   end hide
end process

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

process WSA [CMD_A:Nat1Channel, RDY_A:None, WIN:NatRawChannel, GET_A:PrdChannel] (PrType:Nat) is
   -- Workstation A: building products from raw material
   var State: Bool, N: Nat in
      State := false;
      N := 0; -- to suppress a data-flow error
      loop
         case State in
            false ->
               CMD_A (?N);
               State := true
         |  true ->
               if N > 0 then
                  WIN (PrType, ?any Raw);
                  GET_A (P (PrType));
                  N := N - 1
                  -- State := true
               else
                  RDY_A;
                  State := false
               end if
            end case
      end loop
   end var
end process

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

process WSB [CMD_B: Nat1Channel, RDY_B: None, PUT_B: PrdChannel,
             WOUT: PrdChannel] is
   -- Workstation B: processing products to final form
   var State: Bool, N: Nat in
      State := false;
      N := 0; -- to suppress a data-flow error
      loop
         case State in
            false ->
               CMD_B (?N);
               State := true
         |  true ->
               var P:Prd in
                  if N > 0 then
                     PUT_B (?P);
                     WOUT (P);
                     N := N - 1
                     -- State := true
                  else
                     RDY_B;
                     State := false
                  end if
               end var
         end case
      end loop
   end var
end process

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

process WCT [GET_A:PrdChannel, PUT_B:PrdChannel, TR:None, AR:None]
            (in var PQ:PQueue) is
   -- Workcell transport service
   var P:Prd in
      loop
         alt
            par
               TR
            ||
               GET_A (?P)
            end par;
            PQ := append (PQ, P)
         []
            only if not (empty (PQ)) then
               PUT_B (head (PQ));
               AR;
               PQ := tail (PQ)
            end if
         end alt
      end loop
   end var
end process

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

process WCC [CMD: Nat2Channel, RDY: Nat1Channel, CMD_A: Nat1Channel,
             RDY_A: None, CMD_B: Nat1Channel, RDY_B: None, TR: None, AR: None]
             (PrType: Nat) is
   -- Workcell controller
   var State: Bool, N: Nat in
      State := false;
      N := 0; -- to suppress a data-flow error
      loop
         case State in
            false ->
               CMD (PrType, ?N);
               CMD_B (N);
               State := true
         |  true ->
               if N > 0 then
                  CMD_A (1 of Nat);
                  RDY_A;
                  TR;
                  AR;
                  N := N - 1
                  -- State := true
               else
                  RDY_B;
                  RDY (PrType);
                  State := false
               end if
         end case
      end loop
   end var
end process

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

end module