storage_system_v0.mclr2

% initializing 0 rack
map emptyRack: RackID -> PacketID;
var er: RackID;
eqn emptyRack(er) = 0;

sort PacketID = Nat; % 0 indicates 0/non-existant packet
     RackID = Pos; % rack levels in rack R
     ElevatorID = struct e_1 | e_2 | e_1_2; % elevator e_1, e_2, or both (e_1_2)
     RackRecord = RackID -> PacketID; % array that maps RackID to PacketID. (each rack(RackID) should contains a PacketID, Nat or 0 if its 0))
     EleState = struct free|storing|delivering; 
     JobType = struct store|deliver;

% CONVEYOR C1 ACTIONS
act  read_Want2Store, ToStore, send_ToStore, TakePacket, send_TakePacket, read_AskPacket: PacketID;
     
% CONVEYOR C2 ACTIONS
act  read_Want2Request, ToRequest, send_ToRequest, DeliverPacket, read_DeliverPacket, send_Want2Deliver:  PacketID; 

% RACK ACTIONS
act  read_ToStore: PacketID; % C1 ask rack to store packet
     read_ToRequest: PacketID; % C2 request a packet to rack
     send_OrderToE1, OrderToE1: PacketID # RackID # JobType;
     send_OrderToE2, OrderToE2: PacketID # RackID # JobType;
     read_E1Accept, E1Accept:Bool;
     read_E2Accept, E2Accept:Bool;
     send_PacketFound: PacketID # Bool; % R tells C2 that packet PacketID is available in the rack R
     send_StorageAvailable: Bool; % R tells C1 that storage is available
     GiveDelivery, send_GiveDelivery: PacketID;
     AcceptToDeliver, read_AcceptToDeliver: PacketID # ElevatorID;
     StorePacket, read_StorePacket: PacketID # RackID;

% ELEVATOR ACTIONS
act 
     %communication between elevators
     sendE1_E2: RackID; %inform E2 of the next position of E1
     readE1_E2: RackID; %E2 receive the next position of E1
     sycE1_E2: RackID;%synchronisation action between sendE1_E2 & readE1_E2
     %inform the other elevator whether a conflict exits
     send_E2OK: Bool;
     read_E2OK: Bool;
     sycE2OK: Bool;%synchronisation action between send_E2OK & read_E2OK
     %receive request from Rack
     read_OrderToE1: PacketID # RackID # JobType;
     read_OrderToE2: PacketID # RackID # JobType;
     %accept request 
     send_E1Accept: Bool;
     send_E2Accept: Bool;
     %elevator movement
     Move2Plat;
     Move2Rack;
     %receive and deliver packet at conveyor
     send_AskPacket, AskPacket: PacketID;
     receive_TakePacket: PacketID;
     send_DeliverPacket: PacketID;
     %store and take packet from Rack
     send_StorePacket: PacketID # RackID;
     receive_GiveDelivery: PacketID;
     %move to default level
     Move2Default;

% EXTERNAL ACTIONS
map maxId : PacketID ;
eqn maxId = 2;

map initPool : PacketID -> Set ( PacketID );
var n: PacketID ;
eqn (n == 0) -> initPool (n) = {0};
    (n > 0) -> initPool ( n) = {n } + initPool ( Int2Nat (n -1));

act  Want2Store, send_Want2Store, Want2Request, send_Want2Request, Want2Deliver, read_Want2Deliver: PacketID;
     PacketFound, read_PacketFound: PacketID # Bool; 
     StorageAvailable, read_StorageAvailable: Bool;
     emptyPoolError ;

proc PackagePool ( available , used : Set ( PacketID )) =
    sum pid: PacketID . ((pid != 0) && ( pid < maxId ) && (pid in available )) -> send_Want2Store (pid ) . PackagePool ( available - {pid} , used + { pid })
  + sum pid: PacketID . ((pid != 0) && ( pid < maxId ) && (pid in used )) -> send_Want2Request (pid ) . sum b: Bool . read_PacketFound(pid, b) . (b == false)-> PackagePool () <> (read_Want2Deliver(pid). PackagePool (available + {pid} , used - { pid }))
  + ( available == {}) -> emptyPoolError . PackagePool ();

% C1 PROCESS
%
proc C1 =
     sum pid: PacketID . ((pid != 0) && ( pid < maxId )) -> read_Want2Store(pid) . StoringPacket(pid); 

proc StoringPacket (pid: PacketID) = 
     send_ToStore(pid) . sum b: Bool . read_StorageAvailable(b) . (b == false)-> StoringPacket(pid) <> 
                                                                    read_AskPacket(pid) . send_TakePacket(pid) . C1;

% C2 PROCESS
%
proc C2 = 
     sum pid:PacketID . ((pid != 0) && ( pid < maxId )) -> read_Want2Request(pid) . send_ToRequest (pid) . sum b: Bool . read_PacketFound(pid, b) . (b == false)-> C2 <>
                                                                                                                   read_DeliverPacket (pid). send_Want2Deliver(pid). C2;

% RACK PROCESS
%
%% First the code will check the packet, it will not process non-existant packet. 
%% After it receives ToStore from C1, it will try to find available rack using FindRack
proc Rack(r: RackRecord) =
     sum pid:PacketID . ((pid != 0) && ( pid < maxId )) -> read_ToStore(pid) . FindRack(r, pid)
   + sum pid:PacketID . ((pid != 0) && ( pid < maxId )) -> read_ToRequest(pid) . FindPacket(r, pid)
   + sum pid:PacketID, eid:RackID . ((pid != 0) && ( pid < maxId ) && (eid < 5) && (eid !=2)) -> read_StorePacket(pid, eid) . Rack(r[eid->pid])
   + sum pid:PacketID, eid:RackID , b:Bool . ((pid != 0) && ( pid < maxId ) && (eid < 5) && (eid !=2)) -> read_E1Accept(b) . (b==true) -> send_GiveDelivery(pid) . Rack(r[eid->0])
   + sum pid:PacketID, eid:RackID , b:Bool . ((pid != 0) && ( pid < maxId ) && (eid < 5) && (eid !=2)) -> read_E2Accept(b) . (b==true) -> send_GiveDelivery(pid) . Rack(r[eid->0]);

%% First the code will check the rack rid1. If its 0 (0), it will send_OrderToStore to e2 (bottom elevator). 
%% If its full, it will move to check next rack.
%% Then the code will check the rack rid2. If its 0 (0), it will send_OrderToStore to e1 (top elevator). 
%% If its full, means all storage is full and it send_StorageNotAvailable 
proc FindRack(r: RackRecord, pid: PacketID) =
     ( r(1) == 0 ) -> ( send_StorageAvailable(true) . send_OrderToE2(pid, 1, store) . Rack(r) ) <>
      (( r(3) == 0 ) -> ( send_StorageAvailable(true) . send_OrderToE1(pid, 3, store) . Rack(r) ) <> 
       (( r(4) == 0 ) ->  ( send_StorageAvailable(true) . send_OrderToE1(pid, 4, store) . Rack(r) ) <> 
        (send_StorageAvailable(false) . Rack(r))));

%% First the code will check the rack rid1. If it contains correct pid, it will send_OrderToDeliver to e2 (bottom elevator). 
%% If its 0/wrong pid, it will move to check next rack.
%% Then the code will check the rack rid2. If it contains correct pid, it will send_OrderToDeliver to e2 (bottom elevator). 
%% If its 0/wrong pid, means all rack has been checked and it send_PacketNotFound 
proc FindPacket(r: RackRecord, pid: PacketID) =
     ( r(1) == pid ) -> ( send_PacketFound(pid, true). send_OrderToE2(pid, 1, deliver) . Rack(r)) <> 
      (( r(3) == pid ) -> ( send_PacketFound(pid, true) . send_OrderToE2(pid, 3, deliver) . Rack(r)) <> 
       (( r(4) == pid ) ->  ( send_PacketFound(pid, true) . send_OrderToE1(pid, 4, deliver) . Rack(r)) <> 
        (send_PacketFound(pid, false) . Rack(r))));


%E1 PROCESS
%% E1 will deliver and store packet to highest level
%% E1 will deliver packet to middle level
proc
E1(E1State:EleState, CurPos: RackID, JobPos: RackID)=
((E1State == free && CurPos == 4) -> sum pid: PacketID, rid:RackID, job:JobType. ((pid != 0) && (pid < maxId) && (rid < 5) && (rid !=2))
-> read_OrderToE1(pid, rid, job) . ((rid == 3 && job == store) -> send_E1Accept(true) . E1(E1State = storing, JobPos = 3) 
+ (rid == 4 && job == store) -> send_E1Accept(true) . E1(E1State = storing, JobPos = 4)
+ (rid == 4 && job == deliver) -> send_E1Accept(true) . E1(E1State = delivering, JobPos = 4)))
+
((E1State == free && CurPos == 4) -> sendE1_E2(4) . E1(E1State = free))
+
((E1State == free && CurPos == 4) -> sendE1_E2(4) . E1(E1State = free))

+
((E1State == free && CurPos == 4) -> sum ConflictState:Bool .read_E2OK(ConflictState) . E1(E1State = free))
+
(E1State == free && CurPos != 4) -> sum eid:RackID . ((eid < 5) && (eid !=2)) -> sendE1_E2(4) . sum ConflictState:Bool . read_E2OK(ConflictState) . 
(ConflictState == true) -> Move2Default . E1(E1State = free, CurPos = 4)
+
(E1State == storing && JobPos == 3 && CurPos == 4) ->  sendE1_E2(2).  sum ConflictState:Bool . read_E2OK(ConflictState) . (ConflictState == true) 
-> Move2Plat.E1(E1State = storing, CurPos = 2) <> (E1(E1State = storing, CurPos = 4))
+
((E1State == storing && JobPos == 3 && CurPos == 2) -> sum pid:PacketID . ((pid != 0) && (pid < maxId)) -> send_AskPacket(pid) . receive_TakePacket(pid) . Move2Rack . send_StorePacket(pid, 3) . E1(E1State = free, CurPos = 3))
+
((E1State == storing && JobPos == 4 && CurPos == 4) ->  sendE1_E2(2). sum ConflictState:Bool . read_E2OK(ConflictState) . (ConflictState == true) -> Move2Plat.E1(E1State = storing, CurPos = 2) <> (E1(E1State = storing, CurPos = 4)))
+
((E1State == storing && JobPos == 4 && CurPos == 2) -> sum pid:PacketID . ((pid != 0) && (pid < maxId)) -> send_AskPacket(pid) . receive_TakePacket(pid) . Move2Rack . send_StorePacket(pid, 4) . E1(E1State = free, CurPos = 4)) 
+
((E1State == delivering && JobPos == 4 && CurPos == 4) -> sum pid:PacketID . ((pid != 0) && (pid < maxId)) -> (receive_GiveDelivery(pid) . sendE1_E2(2) . sum ConflictState:Bool . read_E2OK(ConflictState) . (ConflictState == true) -> Move2Plat.E1(E1State = delivering, CurPos = 2) <> (E1(E1State = delivering, CurPos = 4))))
+
((E1State == delivering && JobPos == 4 && CurPos == 2) -> sum pid:PacketID .  ((pid != 0) && (pid < maxId)) -> send_DeliverPacket(pid) . Move2Default . E1(E1State = free, CurPos = 4)) ;

%E2 PROCESS
E2(E2State:EleState, CurPos: RackID, JobPos: RackID)=
((E2State == free && CurPos == 1) -> sum pid: PacketID, rid:RackID, job:JobType . ((pid != 0)  && (pid < maxId) && (rid < 5) && (rid !=2) ) 
-> read_OrderToE2(pid, rid, job) .
((rid == 3 && job == deliver) -> send_E2Accept(true) . E2(E2State = delivering, JobPos = 3) 
+ (rid == 1 && job == store) -> send_E2Accept(true) . E2(E2State = storing, JobPos = 1)
+ (rid == 1 && job == deliver) -> send_E2Accept(true) . E2(E2State = delivering, JobPos = 1)))
+
((E2State == free && CurPos == 1) -> send_E2OK(true) . E2(E2State = free))
+
((E2State == free && CurPos == 1) -> sum eid:RackID . ((eid < 5)) -> readE1_E2(eid) . E2(E2State = free))
+
((E2State == free && CurPos != 1) -> send_E2OK(true) . Move2Default . E2(E2State = free, CurPos = 1))
+
(E2State == delivering && JobPos == 3 && CurPos == 1) ->  sum eid:RackID . ((eid < 5)) -> readE1_E2(eid) . (eid == 2) -> (send_E2OK(false) .  E2(E2State = delivering, CurPos = 3)) 
                                                                                                    <> (send_E2OK(true) .  E2(E2State = delivering, CurPos = 3))
+
(E2State == delivering && JobPos == 3 && CurPos == 3) ->  sum eid:RackID, pid: PacketID . ((pid != 0) && (pid < maxId) && (eid < 5) ) -> receive_GiveDelivery(pid) . readE1_E2(eid) . (eid == 2) -> (send_E2OK(false) . Move2Plat . send_DeliverPacket(pid) . E2(E2State = free, CurPos = 2)) <> (send_E2OK(true) . Move2Plat . send_DeliverPacket(pid) . E2(E2State = free, CurPos = 2))
+
(E2State == delivering && JobPos == 1 && CurPos == 1) ->  sum eid:RackID, pid: PacketID . ((pid != 0) && (pid < maxId) && (eid < 5) ) -> receive_GiveDelivery(pid) . readE1_E2(eid) . (eid == 2) -> (send_E2OK(false) . Move2Plat . E2(E2State = delivering, CurPos = 2)) <> (send_E2OK(true) . Move2Plat . E2(E2State = delivering, CurPos = 2))
+
((E2State == delivering && JobPos == 1 && CurPos == 2) ->  sum pid: PacketID . ((pid != 0) && (pid < maxId)) -> send_DeliverPacket(pid) . Move2Default . E2(E2State = free, CurPos = 1))
+
(E2State == storing && JobPos == 1 && CurPos == 1) ->  sum eid:RackID . readE1_E2(eid) . (eid == 2) -> (send_E2OK(false) . Move2Plat . E2(E2State = storing, CurPos = 2)) <> (send_E2OK(true) . Move2Plat . E2(E2State = storing, CurPos = 2))
+
((E2State == storing && JobPos == 1 && CurPos == 2) ->  sum pid:PacketID . ((pid != 0) && (pid < maxId)) -> send_AskPacket(pid) . receive_TakePacket(pid) . send_E2OK(true) . Move2Rack . send_StorePacket(pid, 1) . E2(E2State = free, CurPos = 1)) ;

init 
         allow({
	Want2Store, Want2Request, Want2Deliver, PacketFound, StorageAvailable, ToStore, ToRequest, TakePacket, DeliverPacket,
           OrderToE1, OrderToE2, StorePacket, GiveDelivery, E1Accept, E2Accept,
           sycE1_E2, sycE2OK, AskPacket, Move2Plat, Move2Rack, Move2Default
	},
     	comm({
		send_Want2Store | read_Want2Store -> 		Want2Store,
		send_Want2Request | read_Want2Request -> 		Want2Request,
		send_Want2Deliver | read_Want2Deliver -> 		Want2Deliver,
		send_PacketFound | read_PacketFound -> 		PacketFound,
		send_StorageAvailable | read_StorageAvailable -> 	StorageAvailable,
 		send_ToStore | read_ToStore -> 			ToStore,
		send_ToRequest | read_ToRequest -> 		ToRequest,
		send_TakePacket | receive_TakePacket -> 		TakePacket,
		send_DeliverPacket | read_DeliverPacket -> 		DeliverPacket,
		send_OrderToE1 | read_OrderToE1 -> 		OrderToE1,
		send_OrderToE2 | read_OrderToE2 -> 		OrderToE2,
		send_StorePacket | read_StorePacket ->                   StorePacket,
                       send_GiveDelivery | receive_GiveDelivery ->              GiveDelivery,
                       send_E1Accept | read_E1Accept ->                         E1Accept,
                       send_E2Accept | read_E2Accept ->                         E2Accept,
                       sendE1_E2|readE1_E2 ->                                   sycE1_E2,
                       send_E2OK|read_E2OK ->                                   sycE2OK,
                       send_AskPacket|read_AskPacket ->                         AskPacket
          	     },
                PackagePool ( initPool ( maxId ), {}) || C1 || C2 || Rack(emptyRack) || E1(free, 4, 4)|| E2(free, 1, 1)
     	)
         );