Promela code MultiElevators - Misho

/*
	Elevator template model for Assignment 2 of 2IX20 - Software Specification.
	Set up for one elevator and two floors.
*/

// LTL formulas to be verified
//ltl p1 { []<> (floor_request_made[1]==true) } /* this property does not hold, as a request for floor 1 can be indefinitely postponed. */
// ltl p2 { []<> (cabin_door_is_open==true) } /* this property should hold, but does not yet; at any moment during an execution, the opening of the cabin door will happen at some later point. */
// ltl a1 { [] ((floor_request_made[1]==true) -> <>(cabin_door_is_open[1]==true)) }
// ltl a2 { [] ((floor_request_made[2]==true) -> <>(cabin_door_is_open[2]==true)) }
// ltl b1 { []<> (cabin_door_is_open==true) }
// ltl b2 { []<> (cabin_door_is_open==false) }
// ltl c { [] ((cabin_door_is_open==true) -> (cabin_door_is_open[el_dest_floor]==true)) }

// the number of elevators
#define M 2
// the number of floors
#define N 4

// IDs of req_button processes - must be from 0 to N-1 - get the 0 right, in single el. first button process will have _pid=4, so we -4 in reqid definition. Counting the number of processes, with M elevators, the first button process will have _pid=3*M+2, hence subtract 3*M+2 to get the first button with reqid=0
#define reqid _pid-(3*M+1) // TODO modify

// keep track of which elevators are free
bool el_free[M] = true; // all are free, initially

// type for direction of elevator
mtype { down, up, none };

// asynchronous channel to handle passenger requests
chan request = [N] of { byte };
// status of requests per floor
bool floor_request_made[N];

// status of floor doors of the shaft of the multiple elevators
// Each floor[i] has a field - array cabin_door_is_open[M]
typedef door_open {
    bool cabin_door_is_open[M]; // COLUMNS, doors on a floor = M
}
door_open floor[N]; // ROWS - each of N rows has M doors
// floor[i].cabin_door_is_open[j] will open the door on floor i (0 <= i <= N-1), with number j (0 <= j <= M)


// status and synchronous channels for elevator cabin and engine
byte el_dest_floor[M]; // current floor of each of M elevators
bool cabin_door_is_open[M]; // M cabin doors for M elevators
chan update_cabin_door[M] = [0] of { bool };
chan cabin_door_updated[M] = [0] of { bool };
chan move_el[M] = [0] of { bool };
chan floor_reached[M] = [0] of { bool }; // each of M elevators must reach a requested floor

// synchronous channels for communication between request handler and main control
//chan go = [0] of { byte };
chan go_el[M] = [0] of { byte }; // one channel for each of M elevators

#define main_control_id _pid-(2*M)

chan served = [0] of { bool };

#define elevator_engine_id _pid-M
#define cabin_door_id _pid

// cabin door process
active [M] proctype cabin_door() {
	do

	:: update_cabin_door[cabin_door_id]?true ->
    floor[el_dest_floor[cabin_door_id]].cabin_door_is_open[cabin_door_id] = true;
    cabin_door_is_open[cabin_door_id] = true;
    cabin_door_updated[cabin_door_id]!true;

	:: update_cabin_door[cabin_door_id]?false ->
    cabin_door_is_open[cabin_door_id] = false;
    floor[el_dest_floor[cabin_door_id]].cabin_door_is_open[cabin_door_id] = false;
    cabin_door_updated[cabin_door_id]!false;

	od;
}

// process combining the elevator engine and sensors
active [M] proctype elevator_engine() {
	do // 'elevator_engine_id' refers to which elevator will move (dependence active [M])
	:: move_el[elevator_engine_id]?true ->
		do
		:: move_el[elevator_engine_id]?false -> break;
		:: floor_reached[elevator_engine_id]!true;
		od;
	od;
}

// DUMMY main control process. Remodel it to control the doors and the engine!
active [M] proctype main_control() {
	byte dest;
    // 'main_control_id' is reference to the elevator (dependence active [M])
	do
	:: go_el[main_control_id]?dest ->
	   el_dest_floor[main_control_id] = dest;
       el_free[main_control_id] = false;

		// Moving elevator
	   move_el[main_control_id]!true; floor_reached[main_control_id]?true;
	   update_cabin_door[main_control_id]!true; cabin_door_updated[main_control_id]?true;
	   update_cabin_door[main_control_id]!false; cabin_door_updated[main_control_id]?false;

       // After serving a floor
	   floor_request_made[dest] = false;
       el_free[main_control_id] = true;
	od;
}

// request handler process. Remodel this process to serve M elevators!
active proctype req_handler() {
	byte dest;
    short el_num = 0;
	do
	:: request?dest;
        if
        :: (el_free[el_num] == true) -> // Halts until elevator el_num is free, then sends req to this el.
            go_el[el_num]!dest;
            el_num = el_num + 1;
            if
            :: (el_num == M) -> el_num = 0;
            :: else // Avoids blocking
            fi;
        fi;

	od;
}

// request button associated to a floor i to request an elevator
active [N] proctype req_button() {
	do
	:: !floor_request_made[reqid] ->
	   atomic {
		request!reqid;
		floor_request_made[reqid] = true;
	   }
	od;
}