% Specification for the rope bridge problem
% (based on Bas Ploeger, 2008)

% Adventurers are identified by their "speeds", i.e. the number of
% minutes they need for crossing the bridge. For this we use the basic
% integer data type of mCRL2 called 'Int'.

% Data type for the position of adventurers and the flashlight.
% Initially, they are all on the 'start' side of the bridge. In the end,
% they should all have reached the 'finish' side.
sort Position = struct start | finish;


act
    % Action declarations:
    % - 'forward'  means:  from start to finish
    % - 'back'     means:  from finish to start

    % The flashlight moves forward together with two adventurers,
    % identified by the action's parameters.
    forward_flashlight: Int # Int;

    % The flashlight moves back together with one adventurer, identified
    % by the action's parameter.
    back_flashlight: Int;


%%% TODO (Exercise 1): 
%%% Add action declarations for Adventurer process here

%%% TODO (Exercise 2):
%%% Add action declarations for synchronised events.

%%% TODO (Exercise 5):
%%% Add action declarations for Referee process.


% The Flashlight process models the flashlight:
% 1. If it is at the 'start' side, it can move forward together with any
%    pair of adventurers.
% 2. If it is at the 'finish' side, it can move back together with any
%    adventurer.
proc Flashlight(pos:Position) =
       (pos == start) ->
         % Case 1.
         sum s,s':Int . forward_flashlight(s,s') . Flashlight(finish)
       <> 
         % Case 2.
         sum s:Int . back_flashlight(s) . Flashlight(start);


%%% TODO (Exercise 1):
%%% Add Adventurer process definition here

%%% TODO (Exercise 5):
%%% Add Referee process definition here



% Initial process definition: the system currently only consists of a
% flashlight at the 'start' side.
init  Flashlight(start) ;

%%% TODO (Exercise 2):
%%% Add the four Adventurer processes to this definition

%%% TODO (Exercise 5):
%%% Add the Referee process to this definition