% Specification for the rope bridge problem % Written by Bas Ploeger, June 2008. % Sort for the position of adventurers and 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 forward_adventurer, % an adventurer moves forward forward_flashlight, % the flashlight moves forward forward_referee, % the referee processes a forward movement forward: Int # Int; % two adventurers and a flashlight move forward % and the referee processes this back_adventurer, % an adventurer moves back back_flashlight, % the flashlight moves back back_referee, % the referee processes a back movement back: Int; % one adventurer and a flashlight move back and the % referee processes this report: Int; % the referee reports that all adventurers have % crossed the bridge along with the time that it took % Models the flashlight which can move to the other side of the bridge proc Flashlight(pos:Position) = (pos == start) -> sum s,s':Int . forward_flashlight(s,s') . Flashlight(finish) <> % position == finish sum s:Int . back_flashlight(s) . Flashlight(start); % Models an adventurer who can move to the other side of the bridge with % its designated speed proc Adventurer(speed:Int, pos:Position) = (pos == start) -> ( sum s:Int . % keep the parameters of forward actions sorted; otherwise % we get two transitions for every forward movement of % adventurers with speeds X and Y -- forward(X,Y) and % forward(Y,X) -- both leading to the same state and % modelling the same event. (s > speed) -> forward_adventurer(speed,s) . Adventurer(speed,finish) <> forward_adventurer(s,speed) . Adventurer(speed,finish) ) <> % position == finish back_adventurer(speed) . Adventurer(speed,start); init allow({forward, back, report}, comm({forward_adventurer | forward_adventurer | forward_flashlight -> forward, back_adventurer | back_flashlight -> back}, Adventurer(1,start) || Adventurer(2,start) || Adventurer(5,start) || Adventurer(10,start) || Flashlight(start) ));