Overture Tool
Formal Modelling in VDM
BuslinesWithDBPP
Author: Claus Ballegaard Nielsen
This example models bus lines in a city, in which passengers are to be transferred from stop to stop. Passengers with specific destinations will arrive at a central station, and the route and flow of the buses need to be planned to service the passenger in the best possible way. The number and routes of buses as wells as the inflow of passengers are variables.
This version connects to a database containing maps and busroutes.
Remote Debugger must be set to remote class: gui.BuslinesRemote
| Properties | Values |
|---|---|
| Language Version: | vdm10 |
| Entry point : | new World().Run() |
Types.vdmpp
class Types
types
public Time = nat;
public Direction = <NORTH> | <SOUTH> | <EAST> | <WEST>;
public Event = BusRoute | Inflow | Simulate | WasteTime;
public BusRoute ::
ID : nat
route : seq of Road`RoadNumber
t : Time;
public Inflow ::
flow : nat
t : Time;
public Simulate ::
t : nat;
public WasteTime ::
t : Time;
functions
public static DirectionToGraphics : Direction -> nat
DirectionToGraphics(d) ==
(
cases d:
<NORTH>-> 1,
<SOUTH>-> 5,
<EAST>-> 3,
<WEST>-> 7
end
);
end Types
ClockTick.vdmpp
class ClockTick
thread
while true do
(
World`timerRef.WaitRelative(1);
World`timerRef.NotifyAll();
World`timerRef.Awake();
)
end ClockTick
WaitNotify.vdmpp
class WaitNotify
instance variables
waitset : set of nat := {}
operations
public Wait : () ==> ()
Wait() ==
( AddToWaitSet (threadid);
Awake()
);
public Notify : () ==> ()
Notify() ==
let p in set waitset in
waitset := waitset \ {p};
public NotifyThread: nat ==> ()
NotifyThread(tId) ==
waitset := waitset \ {tId};
public NotifyAll: () ==> ()
NotifyAll() ==
waitset := {};
private AddToWaitSet : nat ==> ()
AddToWaitSet(n) ==
waitset := waitset union {n};
private Awake : () ==> ()
Awake() == skip
sync
per Awake => threadid not in set waitset;
mutex(AddToWaitSet)
end WaitNotify
World.vdmpp
-----------------------------------------------
-- Class: World
-- Description: World class
-----------------------------------------------
-- Rules of this world
-- In the model the city map is loaded form a database so is the buses and their routes.
-- There are multiple maps which can be loaded and validated in the model.
-- A simulation can be started on specific maps.
-- Buses and routes can also be defined in the inputvalues.txt
--
-- Example of a map
-- _ _ _ _ WP2_ _ _ _ _ C _ _ _ _ _ _ F _ _ _ _ _R8
-- | | R5 | R7 R15| |
-- | | R6|_ D _ _ _ _ _|WP4 |
-- |R4 |R3 | R11 | |
-- | | R14| |R10 |
-- A|_ _ _ _ B|_ _ _ _ _ _ _ WP1_ _R16_WP3_ _ _ _ _| Central
-- | R1 R2 | | R9 |
-- | R13 |_ _ E _ _|R12 |
-- | |
-- | |
-- |_ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ |
-- HW1
--
-- Rules of the model --
-- � Passengers arrive at a certain inflow rate on central station, their destination is randomly picked
-- � Buses always drives at full speed according to the roads speed limit
-- � Passengers will not get on buses that do not pass their stop
-- � Passenger will not change between multiple buses to get to a stop
-- � Buses always drives in cicles. i.e. the start and the stop of a route must be the same
-- � A bus route is defined by roads, and the bus will stop at all stops it passes on these roads
-- � The roads in the bus route must be connected end to end, as the bus can not jump passed pieces of road
-- � Roads are connected by waypoints, some of these waypoints function as bus stops where passengers get off.
class World
instance variables
public static graphics : gui_Graphics:= new gui_Graphics();
public static env : [Environment] := new Environment("inputvalues.txt");
public static timerRef : TimeStamp := new TimeStamp();
operations
public World: () ==> World
World() ==
(
Printer`Out("World created: ");
Printer`Out("------------------------------------------\n");
);
public Run: () ==> ()
Run() ==
(
graphics.init();
);
public StartSimulation: () ==> ()
StartSimulation() ==
(
env.run();
);
public addWaypoint : Waypoint`WaypointsEnum ==> Waypoint
addWaypoint(wp) == env.city.addWaypoint(wp);
public addRoad : Waypoint`WaypointsEnum * Waypoint`WaypointsEnum * Road`RoadNumber * nat * bool==> ()
addRoad(wp1, wp2, roadNmbr, length, highspeed) ==
env.city.addRoad(wp1,wp2,roadNmbr,length, highspeed);
public addBus : nat * seq of Road`RoadNumber ==> Bus
addBus(lineNumber, route) ==
env.city.addBus(lineNumber, route);
end World
Config.vdmpp
-----------------------------------------------
-- Class: Config
-- Description: Config contains configuration values
-----------------------------------------------
--
-- class definition
--
class Config
--
-- Values definition section
--
values
--max passengers on bus
public static BusCapacity : nat = 15;
--speed limit on road, buses will always drive to the limit
public static DefaultRoadSpeedLimit : nat = 10;
--amount of waiting time beofre passengers become annoyed
public static PassengerAnnoyanceLimit : nat = 40;
--max value of passengers inflow
public static MaxInflow : nat = 10;
end Config
Waypoint.vdmpp
class Waypoint
types
public BusStops = <A> | <B> | <C> | <D> | <E> | <F> | <Central>;
public WaypointsEnum = <WP1> | <WP2> | <WP3> | <WP4> | <WP5> | <WP6> | <WP7> | BusStops;
instance variables
protected id : WaypointsEnum;
protected isStop : bool := false;
operations
public Waypoint : Waypoint`WaypointsEnum ==> Waypoint
Waypoint(s) ==
(
id := s;
);
pure public GetId : () ==> WaypointsEnum
GetId()== return id;
pure public IsStop: () ==> bool
IsStop()== return isStop;
functions
public static StringToBusStop : seq of char -> Waypoint`BusStops
StringToBusStop(busstop) ==
(
cases busstop:
"A" -> <A>,
"B" -> <B>,
"C" -> <C>,
"D" -> <D>,
"E" -> <E>,
"F" -> <F>,
"Central" -> <Central>
end
);
public static StringToWaypoint : seq of char -> Waypoint`WaypointsEnum
StringToWaypoint(wp) ==
(
cases wp:
"WP1" -> <WP1>,
"WP2" -> <WP2>,
"WP3" -> <WP3>,
"WP4" -> <WP4>,
"WP5" -> <WP5>,
"WP6" -> <WP6>,
"WP7" -> <WP7>,
others -> StringToBusStop(wp)
end
);
end Waypoint
Road.vdmpp
class Road
types
public RoadNumber = <R1> | <R2> | <R3> | <R4> | <R5> | <R6> | <R7> | <R8>
| <R9> | <R10> | <R11> | <R12> | <R13> |<R14> | <R15> | <R16> | <HW1>;
values
instance variables
roadNmbr : RoadNumber;
roadLength : nat;
speedlimit : nat;
wps : set of Waypoint := {};
timePenalty : nat;
inv card wps > 1;
operations
public Road : RoadNumber * set of Waypoint * nat ==> Road
Road(roadnumber, waypoints, length) ==
(
roadNmbr := roadnumber;
roadLength := length;
speedlimit := Config`DefaultRoadSpeedLimit;
wps := waypoints;
timePenalty := floor(roadLength / speedlimit);
)
pre card waypoints > 1;
public Road : RoadNumber * set of Waypoint * nat * nat ==> Road
Road(roadnumber, waypoints, length, limit) ==
(
roadNmbr := roadnumber;
roadLength := length;
speedlimit := limit;
wps := waypoints;
--time cost of driving on the road
timePenalty := floor(roadLength / speedlimit);
)
pre card waypoints > 1;
pure public Covers : set of Waypoint ==> bool
Covers(waypoints) ==
return {w.GetId() | w in set waypoints} = {w.GetId() | w in set wps}; --does road cover the waypoints in arg
pure public GetWaypoints : () ==> set of Waypoint
GetWaypoints()==
return wps;
pure public OppositeEnd : Waypoint ==> Waypoint
OppositeEnd(wp)==
let opposite in set wps \ {wp} in return opposite
pre wp in set wps; -- if the waypoint is not found on the road
-- it may indicate that the route is not connected
-- by the same waypoint
pure public GetSpeedLimit : () ==> nat
GetSpeedLimit()==
return speedlimit;
public GetLength : () ==> nat
GetLength() ==
return roadLength;
pure public GetRoadNumber : () ==> RoadNumber
GetRoadNumber()==
return roadNmbr;
pure public GetTimePenalty : () ==> nat
GetTimePenalty()==
return timePenalty;
end Road
City.vdmpp
class City
instance variables
wayspoints : inmap Waypoint`WaypointsEnum to Waypoint := {|->};
stops : inmap Waypoint`BusStops to Busstop := {|->};
roads : inmap Road`RoadNumber to Road := {|->};
buses : inmap nat to Bus := {|->};
central : Busstop;
inflow : nat;
operations
public City : () ==> City
City()==
(
central := addBusstop(<Central>);
inflow := 1; --default inflow value
);
public newCity : () ==> ()
newCity() ==
(
stops := {|->};
roads := {|->};
wayspoints := {|->};
buses := {|->};
central := addBusstop(<Central>);
);
--add a new busStop to the city
public addBusstop : Waypoint`BusStops ==> Busstop
addBusstop(stp) ==
(
let bs = new Busstop(stp) in
(
stops := stops munion {stp|->bs};
wayspoints := wayspoints munion {stp |-> bs};
return bs
)
)
pre stp not in set dom stops;
--add waypoint to the city, pasengers cannot get off at a waypoint
public addWaypoint : Waypoint`WaypointsEnum ==> Waypoint
addWaypoint(stp) ==
(
Printer`Out("CITY: Add WP");
let wp = new Waypoint(stp) in
(
wayspoints := wayspoints munion {stp |-> wp};
return wp;
)
)
pre stp not in set dom stops;
--add road to the city, a road are end to end and must have to waypoints and a roadnumber
-- the length of the road has significance to travel time of the bus
public addRoad : Waypoint * Waypoint * Road`RoadNumber * nat ==> ()
addRoad(wp1, wp2, roadNmbr, length) ==
(
let r = new Road(roadNmbr, {wp1, wp2}, length) in
(
roads := roads munion {roadNmbr |-> r};
);
)
pre roadNmbr not in set dom roads --road number not used before
and wp1 <> wp2 --not the same wp, a road to the same wp is not a road
and forall r in set rng roads & not r.Covers({wp1, wp2}); -- waypoint not connected before
public addRoad : Waypoint`WaypointsEnum * Waypoint`WaypointsEnum * Road`RoadNumber * nat * bool ==> ()
addRoad(wp1, wp2, roadNmbr, length, highspeed) ==
if highspeed then
addRoad(wayspoints(wp1), wayspoints(wp2), roadNmbr, length, Config`DefaultRoadSpeedLimit + 10)
else
addRoad(wayspoints(wp1), wayspoints(wp2), roadNmbr, length);
--overloaded addRoad, which allows for the speedlimit of the road to be change from
-- the default value
public addRoad : Waypoint * Waypoint * Road`RoadNumber * nat * nat==> ()
addRoad(wp1, wp2, roadNmbr, length ,speedlimit) ==
(
let r = new Road(roadNmbr, {wp1, wp2}, length, speedlimit) in
(
roads := roads munion {roadNmbr |-> r};
)
)
pre roadNmbr not in set dom roads --road number not used before
and forall r in set rng roads & not r.Covers({wp1, wp2}) -- waypoint not connected before
and wp1 <> wp2; --not the same wp, a road to the same wp is not a road
--add a new bus with a particular road
public addBus : nat * seq of Road`RoadNumber ==> Bus
addBus(lineNumber, route)==
(
--validate that route is possible and finds waypoints along route
dcl busstops : seq of Waypoint := [];
dcl currentWP : Waypoint;
--find roads from ids
let busRoads = findRoadsFromRoadNumber(route) in
(
--always start from central
currentWP := central;
busstops := [currentWP];
--find busstops on the route, starting from central
for all i in set inds busRoads do
(
--stepwise move along route
currentWP := busRoads(i).OppositeEnd(currentWP);
busstops := busstops ^ [currentWP];
);
if (hd busstops <> busstops(len(busstops))) then
exit "End not the same as start "; --change to pre?
--create bus
let bus = new Bus(lineNumber, busRoads, busstops) in
(
--add to mapping
buses := buses munion {lineNumber |-> bus};
--
World`graphics.busAdded(lineNumber);
return bus;
)
);
)
pre len route > 1 --there actually is a route
and lineNumber not in set dom buses; --bus linenumber is not known
pure private findRoadsFromRoadNumber : seq of Road`RoadNumber ==> seq of Road
findRoadsFromRoadNumber(route)==
return [roads(elem) | elem in seq route];
pure public getCentralStation : () ==> Busstop
getCentralStation()==
return central;
--passenger inflow
public setInflow : nat ==> ()
setInflow(flow) ==
(
inflow := flow;
World`graphics.inflowChanged(inflow);
);
pure public getInflow : () ==> nat
getInflow()==
return inflow;
pure public getBuses : () ==> set of Bus
getBuses()==
return rng buses;
--sync functionality for ensuring thread is started,
--due to lack of thread scheduling fairness
public WaitForThreadStart : () ==> ()
WaitForThreadStart() == skip;
private ThreadStarted : () ==> ()
ThreadStarted() == skip;
sync
--mutex(setInflow);
--mutex(setInflow, getInflow);
per WaitForThreadStart => #fin(ThreadStarted) > 0
thread
(
ThreadStarted();
while true do
(
--add passengers to central station
for all - in set {1,...,getInflow()} do
(
--random find stop for passenger to get off
let stopSeq = VDMUtil`set2seq[Waypoint`BusStops](dom stops) in --TODO exclude central
let i = MATH`rand(World`timerRef.GetTime()) mod len stopSeq in
let pass = new Passenger(stops(stopSeq(i+1))) in
(
--let pass = new Passenger(stops(<A>)) in --TODO
central.AddPassenger(pass);
World`graphics.passengerAtCentral(pass.Id(),
VDMUtil`val2seq_of_char[Waypoint`WaypointsEnum]
(pass.GetDestination().GetId()));
)
);
World`env.handleEvent(Printer`natToString(central.GetWaitingCount()) ^ " passengers waiting a central station");
--check annoyance of waiting passengers
for all pass in set central.GetWaiting() do
pass.AnnoyedOfWaiting();
World`timerRef.WaitRelative(5);
World`timerRef.NotifyAll();
World`timerRef.Awake();
)
)
end City
TimeStamp.vdmpp
class TimeStamp
values
public stepLength : nat = 1;
instance variables
currentTime : nat := 0;
wakeUpMap : map nat to nat := {|->};
--syncWithTimeInc : set of nat := {};
--syncWithTimeIncCurrent : set of nat := {};
operations
public WaitRelative : nat ==> ()
WaitRelative(val) ==
AddToWakeUpMap(threadid, currentTime + val);
public WaitAbsolute : nat ==> ()
WaitAbsolute(val) ==
AddToWakeUpMap(threadid, val);
AddToWakeUpMap : nat * nat ==> ()
AddToWakeUpMap(tId, val) ==
wakeUpMap := wakeUpMap ++ { tId |-> val };
public NotifyThread : nat ==> ()
NotifyThread(tId) ==
wakeUpMap := {tId} <-: wakeUpMap;
public NotifyAll : () ==> ()
NotifyAll() ==
let threadSet : set of nat = {th | th in set dom wakeUpMap & wakeUpMap(th) <= currentTime }
in
for all t in set threadSet
do
NotifyThread(t);
public NotifyAndIncTime : () ==> ()
NotifyAndIncTime() ==
(
currentTime := currentTime + stepLength;
NotifyAll();
-- syncWithTimeIncCurrent := syncWithTimeInc;
);
public GetTime : () ==> nat
GetTime() ==
return currentTime;
public Awake: () ==> ()
Awake() == skip;
--public SyncWithTimeIncrement : () ==> ()
--SyncWithTimeIncrement() ==
--(
-- syncWithTimeInc := syncWithTimeInc union {threadid}; --keep track of all
-- syncWithTimeIncCurrent := syncWithTimeIncCurrent union {threadid}; --include in current sync round
-- skip;
--);
--public YieldTimeIncrement: () ==> ()
--YieldTimeIncrement()==
--(
-- syncWithTimeIncCurrent := syncWithTimeIncCurrent \ {threadid};
-- skip
--);
sync
per Awake => threadid not in set dom wakeUpMap;
per NotifyAndIncTime => (card {th | th in set dom wakeUpMap & wakeUpMap(th) = currentTime +1} > 0) ; --The magic one, only allow run
-- per NotifyAndIncTime => ({th | th in set dom wakeUpMap & wakeUpMap(th) <= currentTime} inter syncWithTimeIncCurrent) = {};
mutex(NotifyAll);
mutex(AddToWakeUpMap);
mutex(AddToWakeUpMap, NotifyAll);
-- mutex(SyncWithTimeIncrement);
-- mutex(YieldTimeIncrement);
-- mutex(SyncWithTimeIncrement, YieldTimeIncrement, NotifyAndIncTime);
end TimeStamp
gui_Graphics.vdmpp
class gui_Graphics
operations
public init : () ==> ()
init() == is not yet specified;
public busInRouteTo : nat * seq of char * seq of char * nat ==> ()
busInRouteTo(busid, roadid, waypoint, time) == is not yet specified;
public move : () ==> ()
move() == is not yet specified;
public sleep : () ==> ()
sleep() == is not yet specified;
public passengerAtCentral : nat * seq of char ==> ()
passengerAtCentral(id, waypoint) == is not yet specified;
public passengerAnnoyed : nat==> ()
passengerAnnoyed(id) == is not yet specified;
public passengerGotOnBus : nat ==> ()
passengerGotOnBus(id) == is not yet specified;
public inflowChanged : nat ==> ()
inflowChanged(id) == is not yet specified;
public busAdded : nat ==> ()
busAdded(id) == is not yet specified;
public busStopping : nat ==> ()
busStopping(id) == is not yet specified;
public busPassengerCountChanged : nat * nat ==> ()
busPassengerCountChanged(busid, count) == is not yet specified;
end gui_Graphics
Environment.vdmpp
-----------------------------------------------
-- Class: Environment
-- Description: Environment class in the VeMo project
-----------------------------------------------
--
-- class definition
--
class Environment
instance variables
public city : City;
private io : IO := new IO();
private inlines : seq of inline := [];
private outlines : seq of char := [];
private busy : bool := true;
private simulating : bool := false;
private passengersTransported : nat := 0;
private passengersAnnoyed : nat := 0;
private passengersCount : nat :=0;
private passengersAnnoyedStops : map Waypoint`WaypointsEnum to nat := {|->};
types
inline = Types`Event;
InputTP = seq of inline;
operations
public Environment: seq of char ==> Environment
Environment(filename) ==
(
city := new City();
def mk_(-,input) = io.freadval[InputTP](filename) in
(
inlines := input;
);
--BuildCityMap();
);
private BuildCityMap : () ==> ()
BuildCityMap() ==
(
dcl a : Busstop, b : Busstop, c : Busstop, d : Busstop, e : Busstop, f :Busstop;
dcl wp1 : Waypoint, wp2 : Waypoint, wp3 : Waypoint, wp4 : Waypoint;
a := city.addBusstop(<A>);
b := city.addBusstop(<B>);
c := city.addBusstop(<C>);
d := city.addBusstop(<D>);
e := city.addBusstop(<E>);
f := city.addBusstop(<F>);
wp1 := city.addWaypoint(<WP1>);
wp2 := city.addWaypoint(<WP2>);
wp3 := city.addWaypoint(<WP3>);
wp4 := city.addWaypoint(<WP4>);
city.addRoad(a, b, <R1>, 40);
city.addRoad(b, wp1, <R2>, 80);
city.addRoad(b, wp2, <R3>, 50);
city.addRoad(a, wp2, <R4>, 90);
city.addRoad(wp2, c, <R5>, 60);
city.addRoad(c, d, <R6>, 40);
city.addRoad(c, f, <R7>, 60);
city.addRoad(f, city.getCentralStation(), <R8>, 100);
city.addRoad(city.getCentralStation(), wp3, <R9>, 50);
city.addRoad(wp3, wp4, <R10>, 30);
city.addRoad(d, wp4, <R11>, 40);
city.addRoad(wp3, e, <R12>, 40);
city.addRoad(e, wp1, <R13>, 40);
city.addRoad(wp1, d, <R14>, 30);
city.addRoad(f, wp4, <R15>, 20);
city.addRoad(wp1, wp3, <R16>, 40);
city.addRoad(a, city.getCentralStation(), <HW1>, 310, Config`DefaultRoadSpeedLimit + 10);
);
public Events: () ==> ()
Events() ==
(
if inlines <> []
then
(
dcl done : bool := false,
eventOccurred : bool := false,
curtime : Types`Time := World`timerRef.GetTime();
while not done do
(
def event = hd inlines in
cases event:
mk_Types`BusRoute(-,-,-) ->
(
if event.t <= curtime
then
(
Printer`OutWithTS("Environment: Bus route "
^ Printer`natToString(event.ID));
let b = city.addBus(event.ID, event.route) in
(
Printer`Out("Waypoints:");
let wps = b.GetWaypoints() in
let wpsIds = [wp.GetId() | wp in seq wps] in
IO`print(wpsIds);
Printer`Out("\nStops:");
let wps = b.GetStops() in
let wpsIds = [wp.GetId() | wp in seq wps] in
IO`print(wpsIds);
Printer`Out("\n");
if simulating then
(
start(b);
);
);
eventOccurred := true;
)
),
mk_Types`Inflow(-,-) ->
(
if event.t <= curtime
then
(
SetInflow(event.flow);
eventOccurred := true;
)
),
mk_Types`Simulate(-) ->
(
if event.t <= curtime
then
(
if not simulating then
(
Printer`OutWithTS("Environment: "
^ "Simulation started");
simulating := true;
start(city);
city.WaitForThreadStart();
for all bus in set city.getBuses() do
(
start(bus);
bus.WaitForThreadStart();
);
);
eventOccurred := true;
)
),
mk_Types`WasteTime(-) ->
(
if event.t <= curtime
then
(
Printer`OutWithTS("Environment: Wasting time");
eventOccurred := true;
)
),
others -> Printer`OutWithTS("Environment: No match found")
end;
if eventOccurred then
(
inlines := tl inlines;
done := len inlines = 0;
)
else
done := true;
eventOccurred := false;
);
)
else busy := false;
);
public handleEvent : seq of char ==> ()
handleEvent(s) ==
(
Printer`OutWithTS("#Environment handled System Event: " ^ s);
outlines := outlines ^ Printer`natToString(World`timerRef.GetTime()) ^ ": " ^ s ^ "\n";
);
private SetInflow : nat ==> ()
SetInflow(flow)==
(
Printer`OutWithTS("Environment: "
^ "Inflow changed to " ^ Printer`natToString(flow));
city.setInflow(flow);
);
public IncreaseInflow : () ==> ()
IncreaseInflow() ==
(
Printer`Out("Increase");
let flow = city.getInflow() in
(
if(flow < Config`MaxInflow) then
SetInflow(flow +1);
)
);
public DecreaseInflow : () ==> ()
DecreaseInflow() ==
(
let flow = city.getInflow() in
(
if(flow > 0) then
SetInflow(flow -1);
)
);
public TransportedPassengers : nat ==> ()
TransportedPassengers(number)==
passengersTransported := passengersTransported + number;
public AnnoyedPassenger : nat * Waypoint`WaypointsEnum ==> ()
AnnoyedPassenger(number, goal)==
(
passengersAnnoyed := passengersAnnoyed + number;
if(goal not in set dom passengersAnnoyedStops) then
(
passengersAnnoyedStops := passengersAnnoyedStops ++ {goal |-> number};
)
else
passengersAnnoyedStops := passengersAnnoyedStops ++ {goal |-> passengersAnnoyedStops(goal) + number};
);
public PassengerCount : () ==> ()
PassengerCount()==
passengersCount := passengersCount + 1;
public report : () ==> ()
report() ==
(
Printer`Out("\n\nHowever beautiful the strategy," ^
" you should occasionally look at the results.");
Printer`Out("**************RESULT**************");
Printer`Out("**********************************");
--Printer`Out(outlines);
Printer`Out(" " ^ VDMUtil`val2seq_of_char[nat](passengersCount) ^ "\t passengers in total. (transported and at central)");
Printer`Out(" " ^ VDMUtil`val2seq_of_char[nat](passengersTransported) ^ "\t passengers transported.");
Printer`Out(" " ^ VDMUtil`val2seq_of_char[nat](passengersAnnoyed) ^ "\t passengers got annoyed.");
for all waypoint in set dom passengersAnnoyedStops do
(
Printer`Out("\t" ^ VDMUtil`val2seq_of_char[Waypoint`WaypointsEnum](waypoint) ^ " : " ^ VDMUtil`val2seq_of_char[nat](passengersAnnoyedStops(waypoint)));
);
Printer`Out("\n**********************************");
Printer`Out("**********************************");
);
public isFinished : () ==> ()
isFinished() == skip;
public goEnvironment : () ==> ()
goEnvironment() == skip;
public run : () ==> ()
run() ==
(
start(new ClockTick());
Events();
World`graphics.move();
);
public step : () ==> ()
step() ==
(
Events();
World`timerRef.NotifyAndIncTime();
World`timerRef.Awake();
if(busy) then
(
World`graphics.move();
World`graphics.sleep();
)
else
(
report();
)
);
sync
per isFinished => not busy;
mutex(handleEvent)
end Environment
Bus.vdmpp
class Bus
instance variables
seats : set of Passenger;
inv card seats <= Config`BusCapacity;
--bus line number
line : nat;
-- the route of road the bus is moving along
route : seq of Road;
-- what roads are left in the current pass of the route
curRoute : seq of Road;
-- where are we heading
nextWP : Waypoint;
-- what road are we currently on
currentRoad : Road;
--waypoints passed by the bus
wps : seq of Waypoint;
operations
public Bus : nat * seq of Road * seq of Waypoint ==> Bus
Bus(linenumber, busroute, waypoints)==
(
line := linenumber;
route := busroute;
curRoute := busroute;
nextWP := hd waypoints;
wps := waypoints;
seats := {};
)
pre len waypoints > 1 --ensure bus has somewhere to go
and waypoints <> [];
public GetOn : set of Passenger ==> ()
GetOn(ps) ==
(
seats := seats union ps;
World`graphics.busPassengerCountChanged(line, card seats);
)
pre card seats + card ps <= Config`BusCapacity;
public GotOff : set of Passenger ==> ()
GotOff(p) ==
(
seats := seats \ p;
World`graphics.busPassengerCountChanged(line, card seats);
)
pre p inter seats <> {};
pure public GetWaypoints : () ==> seq of Waypoint
GetWaypoints()==
return wps;
pure public GetStops : () ==> seq of Busstop
GetStops()==
return [wps(i) | i in set inds wps & wps(i).IsStop() ];
private NextWaypoint : () ==> Waypoint
NextWaypoint()==
(
--start route over
if(len curRoute = 0) then
curRoute := route;
--next road
let nextRoad = hd curRoute in
(
--move along route
curRoute := tl curRoute;
--what road are we on
currentRoad := nextRoad;
-- update waypoints
let currentWp = nextWP in
(
nextWP := currentRoad.OppositeEnd(currentWp);
return currentWp;
)
);
);
--functionality to ensure thread start
public WaitForThreadStart : () ==> ()
WaitForThreadStart() == skip;
private ThreadStarted : () ==> ()
ThreadStarted() == skip;
sync
per GetOn => card seats < Config`BusCapacity;
per WaitForThreadStart => #fin(ThreadStarted) > 0
thread
(
dcl passGettingOn : set of Passenger;
ThreadStarted();
let - = NextWaypoint() in skip; --prevent return
--loop which moves bus along route, and lets passengers on and off at stops
while true do
(
Printer`OutWithTS("%Bus " ^ Printer`natToString(line) ^ ": running on " ^
VDMUtil`val2seq_of_char[Road`RoadNumber](currentRoad.GetRoadNumber()) ^
" with length " ^ Printer`natToString(currentRoad.GetLength()) ^ " and speedlimit " ^
Printer`natToString(currentRoad.GetSpeedLimit()) ^
" Next: " ^ VDMUtil`val2seq_of_char[Waypoint`WaypointsEnum](nextWP.GetId()) ^
" Time: " ^ Printer`natToString(currentRoad.GetTimePenalty())
);
World`graphics.busInRouteTo(line,
VDMUtil`val2seq_of_char[Road`RoadNumber](currentRoad.GetRoadNumber()),
VDMUtil`val2seq_of_char[Waypoint`WaypointsEnum](nextWP.GetId()),
currentRoad.GetTimePenalty());
--add to penalty for moving along road
World`timerRef.WaitRelative(currentRoad.GetTimePenalty());
World`timerRef.NotifyAll();
World`timerRef.Awake();
--next on bus route
let next = NextWaypoint() in
(
Printer`OutWithTS("%Bus " ^ Printer`natToString(line) ^
" arrived at " ^
VDMUtil`val2seq_of_char[Waypoint`WaypointsEnum](next.GetId()));
let nextId = next.GetId() in
(
--let passengers in at central station if
--their destination is on the bus' route
if nextId = <Central> then
(
--bus returned with passengers; in the current model this should not be possible
--if(seats <> {}) then exit "Bus returned with passengers";
let central : Busstop = next in
(
--find passengers for bus
let potentialPassengers : set of Passenger = central.GetWaitingOn(wps) in
(
if(card potentialPassengers > 0) then
(
--count available sets in bus
if((Config`BusCapacity - card seats) < card potentialPassengers) then
--not room for all, select some
passGettingOn := SelectSubset(potentialPassengers, Config`BusCapacity - card seats)
else
passGettingOn := potentialPassengers;
-- leave busstop and enter bus seats
central.PassengerLeft(passGettingOn);
GetOn(passGettingOn);
for all p in set passGettingOn do p.GotOnBus();
Printer`OutWithTS("%Bus " ^ Printer`natToString(line) ^ ": " ^
Printer`natToString(card passGettingOn) ^ " got on");
--add to time penalty for stopping
World`graphics.busStopping(line);
World`timerRef.WaitRelative(3);
World`timerRef.NotifyAll();
World`timerRef.Awake();
)
);
);
);
-- let passengers off at their destination
let gettingOff = { p | p in set seats & p.GetDestination() = next} in
(
if(card gettingOff > 0) then
(
GotOff(gettingOff);
Printer`OutWithTS("%Bus " ^ Printer`natToString(line) ^ ": " ^
Printer`natToString(card gettingOff) ^ " got off");
World`env.TransportedPassengers(card gettingOff);
--add to time penalty for stopping
World`graphics.busStopping(line);
World`timerRef.WaitRelative(3);
World`timerRef.NotifyAll();
World`timerRef.Awake();
);
);
);
);
);
);
operations
pure private SelectSubset : set of Passenger * nat ==> set of Passenger
SelectSubset(ps, limit)==
(
--base case
if limit = 0 then
return {};
--smaller than limit, return
if card ps <= limit then
return ps;
--recusive
let sub in set ps in
return {sub} union SelectSubset(ps \ {sub}, limit -1);
)
end Bus
Printer.vdmpp
class Printer
operations
public static Out: seq of char ==> ()
Out (pstr) ==
def - = new IO().echo(pstr ^ "\n") in skip;
public static natToString : nat ==> seq of char
natToString(n) ==
(
return VDMUtil`val2seq_of_char[nat](n);
);
public static OutWithTS: seq of char ==> ()
OutWithTS (pstr) ==
def - = new IO().echo(Printer`natToString(World`timerRef.GetTime()) ^": " ^ pstr ^ "\n") in skip;
public static intToString : int ==> seq of char
intToString(i) ==
(
return VDMUtil`val2seq_of_char[int](i);
);
end Printer
Passenger.vdmpp
class Passenger
instance variables
static nextPassengerId : nat := 1;
passengerId : nat;
goal : Waypoint;
inv goal.IsStop() = true;
annoyanceLimit : nat;
pickedUp : bool;
alreadyAnnoyed : bool;
operations
public Passenger : Busstop==> Passenger
Passenger(destination) ==
(
passengerId := GetNextId();
goal := destination;
annoyanceLimit := World`timerRef.GetTime() + Config`PassengerAnnoyanceLimit;
pickedUp := false;
alreadyAnnoyed := false;
World`env.PassengerCount();
)
pre destination.IsStop() = true;
pure public GetDestination : () ==> Waypoint
GetDestination()==
return goal;
public GotOnBus : () ==> ()
GotOnBus()==
(
World`graphics.passengerGotOnBus(passengerId);
pickedUp := true;
);
public IsAnnoyedOfWaiting : () ==> bool
IsAnnoyedOfWaiting() == return annoyanceLimit < World`timerRef.GetTime()
and not pickedUp;
-- report to environment when passenger becomes annoyed.
public AnnoyedOfWaiting : () ==> ()
AnnoyedOfWaiting() ==
(
if(IsAnnoyedOfWaiting() and not alreadyAnnoyed) then
(
alreadyAnnoyed := true;
World`env.handleEvent("Passenger " ^ Printer`natToString(passengerId) ^ " heading for " ^
VDMUtil`val2seq_of_char[Waypoint`WaypointsEnum](goal.GetId()) ^ " is annoyed of waiting.");
World`env.AnnoyedPassenger(1, goal.GetId());
World`graphics.passengerAnnoyed(passengerId);
)
);
pure public Id : () ==> nat
Id()==
return passengerId;
private GetNextId : () ==> nat
GetNextId() ==
(
let pid = nextPassengerId
in
(
nextPassengerId := nextPassengerId +1;
return pid;
)
);
sync
mutex(GotOnBus, AnnoyedOfWaiting);
end Passenger
Busstop.vdmpp
class Busstop is subclass of Waypoint
instance variables
waiting : set of Passenger := {};
operations
public Busstop : Waypoint`BusStops ==> Busstop
Busstop(s) ==
(
id := s;
isStop := true;
);
--number of passenger waiting
pure public GetWaitingCount : () ==> nat
GetWaitingCount() ==
return card waiting;
--get passengers waiting
pure public GetWaiting : () ==> set of Passenger
GetWaiting() ==
return waiting;
-- get passengers waiting on a bus which passes specific stops
pure public GetWaitingOn : seq of Waypoint==> set of Passenger
GetWaitingOn(stopsAt)==
let stops = elems stopsAt in
return {p | p in set waiting & {p.GetDestination()} inter stops <> {}};
--passenger arrived at the busstop
public AddPassenger : Passenger ==> ()
AddPassenger(p) ==
waiting := waiting union {p};
--passenger got on a bus
public PassengerLeft : set of Passenger ==> ()
PassengerLeft(p) ==
waiting := waiting \ p
pre p inter waiting <> {};
sync
---protect waiting instance variable
mutex(AddPassenger, PassengerLeft)
end Busstop