From fde922d1f02d20012669c76c5f6700a9f9d23064 Mon Sep 17 00:00:00 2001 From: Christian Lillelund Date: Mon, 3 Dec 2018 01:02:21 +0100 Subject: [PATCH 1/6] Started new train --- ERTMS/Interlocking.vdmpp | 85 ++++++++++++++++--------------- ERTMS/RadioBlockCenter.vdmpp | 33 +++++------- ERTMS/Test/EurobaliseTest.vdmpp | 6 +-- ERTMS/Test/InterlockingTest.vdmpp | 6 +-- ERTMS/Test/TrainTest.vdmpp | 8 +-- ERTMS/Train.vdmpp | 33 ++++++++++-- ERTMS/World.vdmpp | 9 ++-- 7 files changed, 103 insertions(+), 77 deletions(-) diff --git a/ERTMS/Interlocking.vdmpp b/ERTMS/Interlocking.vdmpp index 0ff2e06..0d4eafa 100644 --- a/ERTMS/Interlocking.vdmpp +++ b/ERTMS/Interlocking.vdmpp @@ -23,11 +23,11 @@ types rt : Route instance variables - private occupiedTracks : map Track to bool; -- physically occupied track + private trackTable : map Track to bool; -- track table with physical state of track private availableRoutes : set of Route; -- routes not planned to be occupied inv InvNoDuplicateTrack(availableRoutes); - inv InvNoTrackAvailableAndOccupied(occupiedTracks, availableRoutes); + inv InvNoTrackAvailableAndOccupied(trackTable, availableRoutes); operations public RequestToProceed: Route ==> ProceedReply @@ -35,9 +35,15 @@ operations -- if route is in avaliableRoutes and the route tracks are not in the dom of trackOccupied -- grant proceed by returning true, else return false if (card availableRoutes > 0) then ( - let rt in set availableRoutes in - if(prt subset rt and forall tr in set prt & occupiedTracks(tr) = false) - then return mk_ProceedReply(, availableRoutes) + if(exists rt in set availableRoutes + & prt subset rt and forall tr in set prt + & tr in set dom trackTable) then + if(forall tr in set prt & trackTable(tr) = false) then ( + availableRoutes := availableRoutes \ {prt}; + return mk_ProceedReply(, availableRoutes) + ) + else + return mk_ProceedReply(, availableRoutes) else return mk_ProceedReply(, availableRoutes) ) else ( return mk_ProceedReply(, availableRoutes); @@ -47,63 +53,60 @@ operations public RequestRoute: (Route) ==> () RequestRoute(rt) == -- if route is not in routesAvaliable and the tracks are not occupied , - -- then add it to routesAvaliable and clear occupiedTracks -- else do nothing + -- then add it to routesAvaliable and clear trackTable -- else do nothing if (rt not in set availableRoutes and - forall tr in set rt & tr not in set dom occupiedTracks - or occupiedTracks(tr) = false) - then ( - atomic ( - availableRoutes := availableRoutes union {rt}; - occupiedTracks := occupiedTracks ++ {let tr in set rt in tr |-> false} - ) - ) else skip; + forall tr in set rt & tr not in set dom trackTable + or trackTable(tr) = false) + then ( + atomic ( + availableRoutes := availableRoutes union {rt}; + trackTable := trackTable ++ {let tr in set rt in tr |-> false} + ) + ) else skip; public SetTrackState: Track * Eurobalise`TrainState ==> () SetTrackState(tr, sta) == -- if train enters, set specific track as occupied -- if train leaves, clear track - if(sta = ) then ( - atomic ( - occupiedTracks := occupiedTracks ++ {tr |-> true}; - availableRoutes := {rt | rt in set availableRoutes & rt inter {tr} = {}}; - ) - ) - else if (sta = ) then ( - atomic ( - occupiedTracks := occupiedTracks ++ {tr|->false}; - availableRoutes := availableRoutes union {{tr}}; - ) - ) - post tr in set dom occupiedTracks; + if(sta = ) then + trackTable := trackTable ++ {tr |-> true} + else if (sta = ) then + trackTable := trackTable ++ {tr|->false} + post tr in set dom trackTable; - public GetAvaliableRoutes: () ==> set of Route + pure public GetAvaliableRoutes: () ==> set of Route GetAvaliableRoutes() == return availableRoutes; - public GetAvaliableRoutes: set of Track ==> set of Route + pure public GetAvaliableRoutes: set of Track ==> set of Route GetAvaliableRoutes(trs) == return (availableRoutes inter {trs}); - public GetOccupiedTracks : () ==> set of Track - GetOccupiedTracks() == + pure public GetTrackTable : () ==> set of Track + GetTrackTable() == ( - return {tr | tr in set dom occupiedTracks & occupiedTracks(tr) = true}; + return {tr | tr in set dom trackTable & trackTable(tr) = true}; ); public Interlocking: set of Route ==> Interlocking Interlocking(rts) == atomic ( availableRoutes := rts; - occupiedTracks := { tr |-> false | tr in set GetTracksInRoute(rts)}; - ) - -functions - public GetTracksInRoute: set of Route -> set of Track + trackTable := { tr |-> false | tr in set GetTracksInRoute(rts)}; + ); + + pure public GetTracksInRoute: set of Route ==> set of Track GetTracksInRoute(rts) == - ( - if (card rts > 0) then (let rt in set rts in rt) else {} - ); - + if (card rts > 0) then + ( + dcl trs : set of Track := {}; + for all rt in set rts do + for all tr in set rt do + trs := trs union {tr}; + return trs; + ) else return {}; + +functions public InvNoTrackAvailableAndOccupied: map Track to bool * set of Route -> bool InvNoTrackAvailableAndOccupied(trmap, rts) == -- A track cannot be available and occupied. diff --git a/ERTMS/RadioBlockCenter.vdmpp b/ERTMS/RadioBlockCenter.vdmpp index 0742d0d..50c8ff2 100644 --- a/ERTMS/RadioBlockCenter.vdmpp +++ b/ERTMS/RadioBlockCenter.vdmpp @@ -20,28 +20,23 @@ instance variables operations public RequestMovementAuthority: Interlocking`Track ==> MovementAuthorityReply RequestMovementAuthority(tr) == - if (card availableRoutes > 0) then ( - dcl trs: set of Interlocking`Track := {let t in set rt in t | rt in set availableRoutes}; - if(tr in set responsibleTracks and tr in set trs) - then ( - dcl msg : Interlocking`Order; - def mk_Interlocking`ProceedReply(message,rtr) = itl.RequestToProceed({tr}) - in - ( - msg := message; availableRoutes := rtr; ); - if (msg = ) - then ( return ; ) - else ( - availableRoutes := {{tr} | art in set availableRoutes & art inter {tr} = {}}; - return ; + --dcl trs: set of Interlocking`Track := {let t in set rt in t | rt in set availableRoutes}; + --if(tr in set responsibleTracks and tr in set trs) + if(tr in set responsibleTracks) then ( + dcl msg : Interlocking`Order; + def mk_Interlocking`ProceedReply(message,rtr) = itl.RequestToProceed({tr}) + in ( + msg := message; + availableRoutes := rtr; ); + if (msg = ) + then ( return ; ) + else ( + --availableRoutes := {{tr} | art in set availableRoutes & art inter {tr} = {}}; + return ; ) ) else return ; - ) else return ; - - private GetAvailableRoutesFromItl: () ==> () - GetAvailableRoutesFromItl() == - availableRoutes := itl.GetAvaliableRoutes(responsibleTracks); + ); public GetAvailableRoutes: () ==> set of Interlocking`Route GetAvailableRoutes() == diff --git a/ERTMS/Test/EurobaliseTest.vdmpp b/ERTMS/Test/EurobaliseTest.vdmpp index 2055c61..5d3616f 100644 --- a/ERTMS/Test/EurobaliseTest.vdmpp +++ b/ERTMS/Test/EurobaliseTest.vdmpp @@ -33,7 +33,7 @@ operations Test_EnterNotCalled_ItlDoesNotChangeStateForTrack() == ( dcl occupiedTracks : set of Interlocking`Track; - occupiedTracks := itl.GetOccupiedTracks(); + occupiedTracks := itl.GetTrackTable(); assertTrue(track not in set occupiedTracks); ); @@ -42,7 +42,7 @@ operations ( dcl occupiedTracks : set of Interlocking`Track; uut.Enter(); - occupiedTracks := itl.GetOccupiedTracks(); + occupiedTracks := itl.GetTrackTable(); assertTrue(track in set occupiedTracks); ); @@ -52,7 +52,7 @@ operations dcl occupiedTracks : set of Interlocking`Track; uut.Enter(); uut.Leave(); - occupiedTracks := itl.GetOccupiedTracks(); + occupiedTracks := itl.GetTrackTable(); assertTrue(track not in set occupiedTracks); ); diff --git a/ERTMS/Test/InterlockingTest.vdmpp b/ERTMS/Test/InterlockingTest.vdmpp index cc3b0e9..e983070 100644 --- a/ERTMS/Test/InterlockingTest.vdmpp +++ b/ERTMS/Test/InterlockingTest.vdmpp @@ -66,9 +66,9 @@ operations ( dcl track : Interlocking`Track := mk_Interlocking`Track(10,5,15,5,"AB",100); uut.SetTrackState(track, ); - assertTrue(track in set uut.GetOccupiedTracks()); + assertTrue(track in set uut.GetTrackTable()); uut.SetTrackState(track, ); - assertTrue(track not in set uut.GetOccupiedTracks()); + assertTrue(track not in set uut.GetTrackTable()); ); public Test_TrainLeavesTrack_TrackNotOccupied: () ==> () @@ -77,7 +77,7 @@ operations dcl tr : Interlocking`Track := mk_Interlocking`Track(10,5,15,5,"AB",100); uut.SetTrackState(tr, ); uut.SetTrackState(tr, ); - assertTrue(tr not in set uut.GetOccupiedTracks()); + assertTrue(tr not in set uut.GetTrackTable()); ); public Test_RouteHasNoDuplicateTrack_InvSucceed: () ==> () diff --git a/ERTMS/Test/TrainTest.vdmpp b/ERTMS/Test/TrainTest.vdmpp index a9d0806..8ec8724 100644 --- a/ERTMS/Test/TrainTest.vdmpp +++ b/ERTMS/Test/TrainTest.vdmpp @@ -60,10 +60,10 @@ operations uut.Start(); uut.Step(); -- track is not occupied in ITL - assertTrue(itl.GetOccupiedTracks() = {}); + assertTrue(itl.GetTrackTable() = {}); uut.Step(); -- track is now occupied in ITL - assertTrue(routeMap(1) in set itl.GetOccupiedTracks()); + assertTrue(routeMap(1) in set itl.GetTrackTable()); ); public Test_TrackFree_TrainGetsMoaAndDrivesHalfWay: () ==> () @@ -105,7 +105,7 @@ operations uut.Step(); uut.Step(); uut.Step(); - assertTrue(routeMap(1) not in set itl.GetOccupiedTracks()); + assertTrue(routeMap(1) not in set itl.GetTrackTable()); ); public Test_TrainIsAtTheEnd_EntersNewTrack: () ==> () @@ -117,7 +117,7 @@ operations uut.Step(); uut.Step(); uut.Step(); - assertTrue(routeMap(2) in set itl.GetOccupiedTracks()); + assertTrue(routeMap(2) in set itl.GetTrackTable()); ); public Test_TrainAtNextTrack_TrainDrivesToEnd: () ==> () diff --git a/ERTMS/Train.vdmpp b/ERTMS/Train.vdmpp index 5bd36eb..7c680ef 100644 --- a/ERTMS/Train.vdmpp +++ b/ERTMS/Train.vdmpp @@ -1,4 +1,7 @@ class Train +types + public State = | | | ; + instance variables private posX : real; private posY : real; @@ -10,6 +13,7 @@ instance variables private speed : real := 0; private started : bool := false; private id : seq of char := ""; + private state: State := ; inv forall x in set {1, ..., card dom route-1} & InvTrackIsConnected(route(x),route(x+1)); @@ -22,11 +26,30 @@ instance variables operations public Step: () ==> () Step() == - ( Drive(); ); + ( + Drive(); + UpdateRecentStates(); + ); + + private Move: () ==> () + Move() == + ( + if (state = ) ( + dcl currentEb : Eurobalise := transponders(route(currentTrack)); + + + + ) + ); + + private UpdateStats: () ==> () + UpdateStats() == + skip; private Drive: () ==> () Drive() == -- Drive() performs one iteration of moving the train + ( -- continue if there is track to traverse if(currentTrack <= card dom route and started) then ( @@ -58,7 +81,7 @@ operations -- we are midway. request MoA for next track, if there is such if (card dom route > currentTrack) then ( if(rbc.RequestMovementAuthority(route(currentTrack+1)) = ) - then ( movementAuths := movementAuths munion {tr |-> true | tr in set rng route}; ) + then ( movementAuths := movementAuths ++ {route(currentTrack) |-> true}; ) ); -- drive the remaining way if (distX = 0 and distY <> 0) then ( posY := posY + distY; ) @@ -70,7 +93,7 @@ operations -- get MoA for current track if(rbc.RequestMovementAuthority(route(currentTrack)) = ) then ( - movementAuths := movementAuths ++ {tr |-> true | tr in set rng route}; + movementAuths := movementAuths ++ {route(currentTrack) |-> true}; started := true; ) else ( -- could not get MoA. Stopping ... @@ -107,6 +130,10 @@ operations GetId() == return id; + public GetTrack: () ==> Interlocking`Track + GetTrack() == + return route(currentTrack); + public IsStarted: () ==> bool IsStarted() == return started; diff --git a/ERTMS/World.vdmpp b/ERTMS/World.vdmpp index 4ee1ef9..d8d5908 100644 --- a/ERTMS/World.vdmpp +++ b/ERTMS/World.vdmpp @@ -35,7 +35,7 @@ values private controller = new Controller([route1, route2], itl); --global radioblockcenter - private rbc = new RadioBlockCenter({route1, route2}, allTracks, itl); + private rbc = new RadioBlockCenter({}, allTracks, itl); -- Eurobalise maps for each train private trackEbMap1 = {track1 |-> new Eurobalise(itl, track1), track2 |-> new Eurobalise(itl, track2), @@ -82,9 +82,10 @@ operations for train in trains do ( train.Step(); - Print("Train " ^ VDMUtil`val2seq_of_char[seq of char](train.GetId()) - ^ " at: " ^ VDMUtil`val2seq_of_char[real](train.GetPosX()) - ^ "-" ^ VDMUtil`val2seq_of_char[real](train.GetPosY())); + Print("Train: " ^ VDMUtil`val2seq_of_char[seq of char](train.GetId()) + ^ " pos: " ^ VDMUtil`val2seq_of_char[real](train.GetPosX()) + ^ "-" ^ VDMUtil`val2seq_of_char[real](train.GetPosY()) + ^ " on track: " ^ VDMUtil`val2seq_of_char[Interlocking`Track](train.GetTrack())); ) ); From b83cc1daf459d58cefdfeb768146bb0e0a10764b Mon Sep 17 00:00:00 2001 From: Christian Lillelund Date: Mon, 3 Dec 2018 01:34:56 +0100 Subject: [PATCH 2/6] More code to new train logic --- ERTMS/RadioBlockCenter.vdmpp | 8 ++++---- ERTMS/Train.vdmpp | 22 ++++++++++++++-------- 2 files changed, 18 insertions(+), 12 deletions(-) diff --git a/ERTMS/RadioBlockCenter.vdmpp b/ERTMS/RadioBlockCenter.vdmpp index 50c8ff2..04c8df8 100644 --- a/ERTMS/RadioBlockCenter.vdmpp +++ b/ERTMS/RadioBlockCenter.vdmpp @@ -18,14 +18,14 @@ instance variables inv Interlocking`InvNoDuplicateTrack(availableRoutes); operations - public RequestMovementAuthority: Interlocking`Track ==> MovementAuthorityReply - RequestMovementAuthority(tr) == + public RequestMovementAuthority: Interlocking`Route ==> MovementAuthorityReply + RequestMovementAuthority(rt) == ( --dcl trs: set of Interlocking`Track := {let t in set rt in t | rt in set availableRoutes}; --if(tr in set responsibleTracks and tr in set trs) - if(tr in set responsibleTracks) then ( + if(responsibleTracks psubset rt) then ( dcl msg : Interlocking`Order; - def mk_Interlocking`ProceedReply(message,rtr) = itl.RequestToProceed({tr}) + def mk_Interlocking`ProceedReply(message,rtr) = itl.RequestToProceed(rt) in ( msg := message; availableRoutes := rtr; ); diff --git a/ERTMS/Train.vdmpp b/ERTMS/Train.vdmpp index 7c680ef..1255779 100644 --- a/ERTMS/Train.vdmpp +++ b/ERTMS/Train.vdmpp @@ -1,6 +1,6 @@ class Train types - public State = | | | ; + public State = | | | ; instance variables private posX : real; @@ -15,6 +15,9 @@ instance variables private id : seq of char := ""; private state: State := ; + private schedule: map nat to Interlocking`Route; + --private currentRoute: Interlocking`Route; + inv forall x in set {1, ..., card dom route-1} & InvTrackIsConnected(route(x),route(x+1)); inv card dom route = card dom transponders; @@ -28,17 +31,21 @@ operations Step() == ( Drive(); - UpdateRecentStates(); + UpdateStats(); ); private Move: () ==> () Move() == ( - if (state = ) ( - dcl currentEb : Eurobalise := transponders(route(currentTrack)); - - - + if (state = ) then ( + if(rbc.RequestMovementAuthority(schedule(1)) = ) + then ( + dcl currentRoute : Interlocking`Route := schedule(1); + + + + ) else + (skip;) ) ); @@ -49,7 +56,6 @@ operations private Drive: () ==> () Drive() == -- Drive() performs one iteration of moving the train - ( -- continue if there is track to traverse if(currentTrack <= card dom route and started) then ( From b7b87f8cafb3538686100af1bdba396a3fdb37cf Mon Sep 17 00:00:00 2001 From: Christian Lillelund Date: Mon, 3 Dec 2018 02:30:15 +0100 Subject: [PATCH 3/6] First version of new train driver --- ERTMS/Interlocking.vdmpp | 6 ++--- ERTMS/Train.vdmpp | 58 +++++++++++++++++++++++++++++----------- 2 files changed, 46 insertions(+), 18 deletions(-) diff --git a/ERTMS/Interlocking.vdmpp b/ERTMS/Interlocking.vdmpp index 0d4eafa..d672b37 100644 --- a/ERTMS/Interlocking.vdmpp +++ b/ERTMS/Interlocking.vdmpp @@ -92,11 +92,11 @@ operations Interlocking(rts) == atomic ( availableRoutes := rts; - trackTable := { tr |-> false | tr in set GetTracksInRoute(rts)}; + trackTable := { tr |-> false | tr in set GetTracksInRoutes(rts)}; ); - pure public GetTracksInRoute: set of Route ==> set of Track - GetTracksInRoute(rts) == + pure public GetTracksInRoutes: set of Route ==> set of Track + GetTracksInRoutes(rts) == if (card rts > 0) then ( dcl trs : set of Track := {}; diff --git a/ERTMS/Train.vdmpp b/ERTMS/Train.vdmpp index 1255779..bb21c36 100644 --- a/ERTMS/Train.vdmpp +++ b/ERTMS/Train.vdmpp @@ -1,6 +1,10 @@ class Train types - public State = | | | ; + public State = | | ; + public TrainLogEntry :: id : seq of char + state : State + posX : real + posY : real instance variables private posX : real; @@ -15,7 +19,9 @@ instance variables private id : seq of char := ""; private state: State := ; - private schedule: map nat to Interlocking`Route; + private routeNo: nat := 0; + private timetable: map nat to Interlocking`Route; + private trainLog: seq of TrainLogEntry; --private currentRoute: Interlocking`Route; inv forall x in set {1, ..., card dom route-1} @@ -31,27 +37,49 @@ operations Step() == ( Drive(); - UpdateStats(); ); private Move: () ==> () Move() == ( - if (state = ) then ( - if(rbc.RequestMovementAuthority(schedule(1)) = ) + if (state = and routeNo < card dom timetable) then ( + UpdateStats(id, state, posX, posY); + if(rbc.RequestMovementAuthority(timetable(routeNo)) = ) then ( - dcl currentRoute : Interlocking`Route := schedule(1); - - - - ) else - (skip;) - ) + dcl currentRoute : Interlocking`Route := timetable(1); + UpdateStats(id, state, posX, posY); + for track in GetTracksInRoute(currentRoute) do ( + dcl currentEb : Eurobalise := transponders(track); + currentEb.Enter(); + speed := track.maxSpeed; + posX := track.endX; + posY := track.endY; + UpdateStats(id, state, posX, posY); + ) + ) else ( + state := ; + UpdateStats(id, state, posX, posY); + ) + ) else UpdateStats(id, state, posX, posY); ); - private UpdateStats: () ==> () - UpdateStats() == - skip; + private UpdateStats: seq of char * State * real * real ==> () + UpdateStats(id, state, posX, posY) == + trainLog := trainLog ^ [mk_TrainLogEntry(id, state, posX, posY)]; + + public GetStats: () ==> seq of TrainLogEntry + GetStats() == + return trainLog; + + pure public GetTracksInRoute: Interlocking`Route ==> seq of Interlocking`Track + GetTracksInRoute(rt) == + if (card rt > 0) then + ( + dcl trs : seq of Interlocking`Track := []; + for all tr in set rt do + trs := trs ^ [tr]; + return trs; + ) else return []; private Drive: () ==> () Drive() == From 20fa4e5180d906c2f97c261d7864ee9ad719096d Mon Sep 17 00:00:00 2001 From: Christian Lillelund Date: Mon, 3 Dec 2018 18:50:49 +0100 Subject: [PATCH 4/6] More train code --- ERTMS/Train.vdmpp | 113 +++++------------- old_train.txt | 58 +++++++++ .../TrainTest.vdmpp => old_train_test.txt | 0 3 files changed, 88 insertions(+), 83 deletions(-) create mode 100644 old_train.txt rename ERTMS/Test/TrainTest.vdmpp => old_train_test.txt (100%) diff --git a/ERTMS/Train.vdmpp b/ERTMS/Train.vdmpp index bb21c36..f688362 100644 --- a/ERTMS/Train.vdmpp +++ b/ERTMS/Train.vdmpp @@ -18,9 +18,8 @@ instance variables private started : bool := false; private id : seq of char := ""; private state: State := ; - - private routeNo: nat := 0; - private timetable: map nat to Interlocking`Route; + + private timetable: seq of Interlocking`Route; private trainLog: seq of TrainLogEntry; --private currentRoute: Interlocking`Route; @@ -39,34 +38,40 @@ operations Drive(); ); - private Move: () ==> () - Move() == + private Drive: () ==> () + Drive() == ( - if (state = and routeNo < card dom timetable) then ( - UpdateStats(id, state, posX, posY); - if(rbc.RequestMovementAuthority(timetable(routeNo)) = ) + if (state = and len timetable > 0) then ( + dcl currentRoute : Interlocking`Route := hd timetable; + UpdateStats(); + if(rbc.RequestMovementAuthority(currentRoute) = ) then ( - dcl currentRoute : Interlocking`Route := timetable(1); - UpdateStats(id, state, posX, posY); + UpdateStats(); for track in GetTracksInRoute(currentRoute) do ( dcl currentEb : Eurobalise := transponders(track); currentEb.Enter(); speed := track.maxSpeed; posX := track.endX; posY := track.endY; - UpdateStats(id, state, posX, posY); - ) + UpdateStats(); + ); + timetable := tl timetable; + UpdateStats(); ) else ( state := ; - UpdateStats(id, state, posX, posY); + UpdateStats(); ) - ) else UpdateStats(id, state, posX, posY); + ) else UpdateStats(); ); - private UpdateStats: seq of char * State * real * real ==> () - UpdateStats(id, state, posX, posY) == + private UpdateStats: () ==> () + UpdateStats() == trainLog := trainLog ^ [mk_TrainLogEntry(id, state, posX, posY)]; + public AddRoute: Interlocking`Route ==> () + AddRoute(rt) == + timetable := timetable ^ [rt]; + public GetStats: () ==> seq of TrainLogEntry GetStats() == return trainLog; @@ -80,73 +85,14 @@ operations trs := trs ^ [tr]; return trs; ) else return []; - - private Drive: () ==> () - Drive() == - -- Drive() performs one iteration of moving the train - ( -- continue if there is track to traverse - if(currentTrack <= card dom route and started) then - ( - dcl currentEb : Eurobalise := transponders(route(currentTrack)); - dcl distX : real := route(currentTrack).endX-posX; - dcl distY : real := route(currentTrack).endY-posY; - -- make sure we have MoA for current track - if (movementAuths(route(currentTrack))) then ( - -- check where the train is currently - if (posX = route(currentTrack).startX and posY = route(currentTrack).startY) - then ( - -- enter track and drive halfway - currentEb.Enter(); - if (distX = 0 and distY <> 0) then ( posY := posY + distY/2; ) - else if (distY = 0 and distX <> 0) then ( posX := posX + distX/2; ) - else if (distY <> 0 and distX <> 0) then - ( posY := posY + distY/2; posX := posX + distX/2; ); - ) else if (posX = route(currentTrack).endX and posY = route(currentTrack).endY) - then ( - -- leave current track, adjust speed to next track - currentEb.Leave(); - if(currentTrack+1 < card dom route) then - atomic ( - speed := route(currentTrack+1).maxSpeed; - currentTrack := currentTrack+1; - ) else - speed := 0; - ) else ( - -- we are midway. request MoA for next track, if there is such - if (card dom route > currentTrack) then ( - if(rbc.RequestMovementAuthority(route(currentTrack+1)) = ) - then ( movementAuths := movementAuths ++ {route(currentTrack) |-> true}; ) - ); - -- drive the remaining way - if (distX = 0 and distY <> 0) then ( posY := posY + distY; ) - else if (distY = 0 and distX <> 0) then ( posX := posX + distX; ) - else if (distX <> 0 and distY <> 0) then - ( posY := posY + distY; posX := posX + distX; ); - ); - ) else ( - -- get MoA for current track - if(rbc.RequestMovementAuthority(route(currentTrack)) = ) - then ( - movementAuths := movementAuths ++ {route(currentTrack) |-> true}; - started := true; - ) else ( - -- could not get MoA. Stopping ... - speed := 0; - ) - ) - ) else ( - -- train has reached end of route, stop - speed := 0; started := false - ) - ); public Start: () ==> () Start() == - started := true; + state := ; public Stop: () ==> () Stop() == - started := false; + state := ; public GetPosX: () ==> real GetPosX() == @@ -164,13 +110,14 @@ operations GetId() == return id; - public GetTrack: () ==> Interlocking`Track - GetTrack() == - return route(currentTrack); + public GetRoute: () ==> Interlocking`Route + GetRoute() == + return hd timetable; - public IsStarted: () ==> bool - IsStarted() == - return started; + public IsRunning: () ==> bool + IsRunning() == + if state = then return true + else return false; public GetMovementAuths: () ==> set of Interlocking`Track GetMovementAuths() == diff --git a/old_train.txt b/old_train.txt new file mode 100644 index 0000000..2a8299a --- /dev/null +++ b/old_train.txt @@ -0,0 +1,58 @@ +private Drive: () ==> () + Drive() == + -- Drive() performs one iteration of moving the train + ( -- continue if there is track to traverse + if(currentTrack <= card dom route and started) then + ( + dcl currentEb : Eurobalise := transponders(route(currentTrack)); + dcl distX : real := route(currentTrack).endX-posX; + dcl distY : real := route(currentTrack).endY-posY; + -- make sure we have MoA for current track + if (movementAuths(route(currentTrack))) then ( + -- check where the train is currently + if (posX = route(currentTrack).startX and posY = route(currentTrack).startY) + then ( + -- enter track and drive halfway + currentEb.Enter(); + if (distX = 0 and distY <> 0) then ( posY := posY + distY/2; ) + else if (distY = 0 and distX <> 0) then ( posX := posX + distX/2; ) + else if (distY <> 0 and distX <> 0) then + ( posY := posY + distY/2; posX := posX + distX/2; ); + ) else if (posX = route(currentTrack).endX and posY = route(currentTrack).endY) + then ( + -- leave current track, adjust speed to next track + currentEb.Leave(); + if(currentTrack+1 < card dom route) then + atomic ( + speed := route(currentTrack+1).maxSpeed; + currentTrack := currentTrack+1; + ) else + speed := 0; + ) else ( + -- we are midway. request MoA for next track, if there is such + if (card dom route > currentTrack) then ( + if(rbc.RequestMovementAuthority(route(currentTrack+1)) = ) + then ( movementAuths := movementAuths ++ {route(currentTrack) |-> true}; ) + ); + -- drive the remaining way + if (distX = 0 and distY <> 0) then ( posY := posY + distY; ) + else if (distY = 0 and distX <> 0) then ( posX := posX + distX; ) + else if (distX <> 0 and distY <> 0) then + ( posY := posY + distY; posX := posX + distX; ); + ); + ) else ( + -- get MoA for current track + if(rbc.RequestMovementAuthority(route(currentTrack)) = ) + then ( + movementAuths := movementAuths ++ {route(currentTrack) |-> true}; + started := true; + ) else ( + -- could not get MoA. Stopping ... + speed := 0; + ) + ) + ) else ( + -- train has reached end of route, stop + speed := 0; started := false + ) + ); \ No newline at end of file diff --git a/ERTMS/Test/TrainTest.vdmpp b/old_train_test.txt similarity index 100% rename from ERTMS/Test/TrainTest.vdmpp rename to old_train_test.txt From 01324eedc5565bc9b85bc77dd68c9c6a7e854575 Mon Sep 17 00:00:00 2001 From: Christian Lillelund Date: Mon, 3 Dec 2018 21:10:39 +0100 Subject: [PATCH 5/6] Changed itl so it respons with the resp tracks to rbc --- ERTMS/Interlocking.vdmpp | 27 ++++++--- ERTMS/RadioBlockCenter.vdmpp | 10 +-- ERTMS/Test/InterlockingTest.vdmpp | 4 +- ERTMS/Test/RadioBlockCenterTest.vdmpp | 12 ++-- ERTMS/Train.vdmpp | 87 +++++++++------------------ ERTMS/World.vdmpp | 76 ++++++++++++----------- 6 files changed, 97 insertions(+), 119 deletions(-) diff --git a/ERTMS/Interlocking.vdmpp b/ERTMS/Interlocking.vdmpp index d672b37..cd667fc 100644 --- a/ERTMS/Interlocking.vdmpp +++ b/ERTMS/Interlocking.vdmpp @@ -27,11 +27,11 @@ instance variables private availableRoutes : set of Route; -- routes not planned to be occupied inv InvNoDuplicateTrack(availableRoutes); - inv InvNoTrackAvailableAndOccupied(trackTable, availableRoutes); +-- inv InvNoTrackAvailableAndOccupied(trackTable, availableRoutes); operations - public RequestToProceed: Route ==> ProceedReply - RequestToProceed(prt) == + public RequestToProceed: Route * set of Track ==> ProceedReply + RequestToProceed(prt, respTrs) == -- if route is in avaliableRoutes and the route tracks are not in the dom of trackOccupied -- grant proceed by returning true, else return false if (card availableRoutes > 0) then ( @@ -39,17 +39,26 @@ operations & prt subset rt and forall tr in set prt & tr in set dom trackTable) then if(forall tr in set prt & trackTable(tr) = false) then ( - availableRoutes := availableRoutes \ {prt}; - return mk_ProceedReply(, availableRoutes) + availableRoutes := {rts | rts in set availableRoutes + & forall ptrs in set {prt} & rts inter ptrs = {}}; + return ProceedGranted(respTrs); ) else - return mk_ProceedReply(, availableRoutes) - else return mk_ProceedReply(, availableRoutes) + return ProceedDenied(respTrs) + else return ProceedDenied(respTrs) ) else ( - return mk_ProceedReply(, availableRoutes); + return ProceedDenied(respTrs) ) pre card prt > 0; - + + private ProceedGranted: set of Track ==> ProceedReply + ProceedGranted(respTrs) == + return mk_ProceedReply(, availableRoutes inter {respTrs}); + + private ProceedDenied: set of Track ==> ProceedReply + ProceedDenied(respTrs) == + return mk_ProceedReply(, availableRoutes inter {respTrs}); + public RequestRoute: (Route) ==> () RequestRoute(rt) == -- if route is not in routesAvaliable and the tracks are not occupied , diff --git a/ERTMS/RadioBlockCenter.vdmpp b/ERTMS/RadioBlockCenter.vdmpp index 04c8df8..6be77d9 100644 --- a/ERTMS/RadioBlockCenter.vdmpp +++ b/ERTMS/RadioBlockCenter.vdmpp @@ -10,7 +10,7 @@ tracks = {mk_Interlocking`Track(10,5,15,5,"AB",100), mk_Interlocking`Track(25,5,30,5,"EF",110)} instance variables - private responsibleTracks : set of Interlocking`Track; + private respTracks : set of Interlocking`Track; private availableRoutes : set of Interlocking`Route; -- from interlocking private movementAuthorites : map nat to seq of Interlocking`Track; private itl : Interlocking; @@ -23,9 +23,9 @@ operations ( --dcl trs: set of Interlocking`Track := {let t in set rt in t | rt in set availableRoutes}; --if(tr in set responsibleTracks and tr in set trs) - if(responsibleTracks psubset rt) then ( + if(rt subset respTracks) then ( dcl msg : Interlocking`Order; - def mk_Interlocking`ProceedReply(message,rtr) = itl.RequestToProceed(rt) + def mk_Interlocking`ProceedReply(message,rtr) = itl.RequestToProceed(rt, respTracks) in ( msg := message; availableRoutes := rtr; ); @@ -44,14 +44,14 @@ operations public GetResponsibleTracks: () ==> set of Interlocking`Track GetResponsibleTracks() == - return responsibleTracks; + return respTracks; public RadioBlockCenter : set of Interlocking`Route * set of Interlocking`Track * Interlocking ==> RadioBlockCenter RadioBlockCenter(rts,trs,pitl) == atomic ( availableRoutes := rts; - responsibleTracks := trs; + respTracks := trs; itl := pitl; movementAuthorites := {|->}; ); diff --git a/ERTMS/Test/InterlockingTest.vdmpp b/ERTMS/Test/InterlockingTest.vdmpp index e983070..4f5962e 100644 --- a/ERTMS/Test/InterlockingTest.vdmpp +++ b/ERTMS/Test/InterlockingTest.vdmpp @@ -41,7 +41,7 @@ operations Test_RouteInAvaRoutes_ProceedGranted() == ( dcl testRoute : Interlocking`Route := {mk_Interlocking`Track(10,5,15,5,"AB",100)}; - dcl msg : Interlocking`ProceedReply := uut.RequestToProceed(testRoute); + dcl msg : Interlocking`ProceedReply := uut.RequestToProceed(testRoute, testRoute); assertTrue(msg.message = ); ); @@ -49,7 +49,7 @@ operations Test_RouteNotInAvaRoutes_ProceedDenied() == ( dcl testRoute : Interlocking`Route := {mk_Interlocking`Track(11,4,16,4,"AB",100)}; - dcl msg : Interlocking`ProceedReply := uut.RequestToProceed(testRoute); + dcl msg : Interlocking`ProceedReply := uut.RequestToProceed(testRoute, testRoute); assertTrue(msg.message = ); ); diff --git a/ERTMS/Test/RadioBlockCenterTest.vdmpp b/ERTMS/Test/RadioBlockCenterTest.vdmpp index a38a4e4..fc073e9 100644 --- a/ERTMS/Test/RadioBlockCenterTest.vdmpp +++ b/ERTMS/Test/RadioBlockCenterTest.vdmpp @@ -42,21 +42,21 @@ operations assertTrue(route not in set uut.GetAvailableRoutes()); ); - public Test_RequestMoaForFreeTrack_MoaGranted_: () ==> () - Test_RequestMoaForFreeTrack_MoaGranted_() == + public Test_RequestMoaForFreeRoute_MoaGranted: () ==> () + Test_RequestMoaForFreeRoute_MoaGranted() == ( dcl track : Interlocking`Track := mk_Interlocking`Track(10,5,15,5,"AB",100); dcl msg : RadioBlockCenter`MovementAuthorityReply - := uut.RequestMovementAuthority(track); + := uut.RequestMovementAuthority({track}); assertTrue(msg = ); ); - public Test_RequestMoaForNotFreeTrack_MoaDenied: () ==> () - Test_RequestMoaForNotFreeTrack_MoaDenied() == + public Test_RequestMoaForNotFreeRoute_MoaDenied: () ==> () + Test_RequestMoaForNotFreeRoute_MoaDenied() == ( dcl track : Interlocking`Track := mk_Interlocking`Track(90,70,95,75,"HI",100); dcl msg : RadioBlockCenter`MovementAuthorityReply - := uut.RequestMovementAuthority(track); + := uut.RequestMovementAuthority({track}); assertTrue(msg = ); ); diff --git a/ERTMS/Train.vdmpp b/ERTMS/Train.vdmpp index f688362..b14e10c 100644 --- a/ERTMS/Train.vdmpp +++ b/ERTMS/Train.vdmpp @@ -7,30 +7,19 @@ types posY : real instance variables - private posX : real; - private posY : real; - private currentTrack : nat; - private route : map nat to Interlocking`Track; - private transponders : map Interlocking`Track to Eurobalise; - private rbc : RadioBlockCenter; - private movementAuths : map Interlocking`Track to bool; - private speed : real := 0; - private started : bool := false; + private posX : real := 0; + private posY : real := 0; + private currentSpeed : real := 0; + private transponders : map Interlocking`Track to Eurobalise := {|->}; private id : seq of char := ""; private state: State := ; + private routeTable: seq of Interlocking`Route := []; + private trainLog: seq of TrainLogEntry := []; + private rbc : RadioBlockCenter; + inv forall rt in seq routeTable & InvTrackIsConnected(rt); + inv state = and currentSpeed >= 0 + or state = and currentSpeed = 0; - private timetable: seq of Interlocking`Route; - private trainLog: seq of TrainLogEntry; - --private currentRoute: Interlocking`Route; - - inv forall x in set {1, ..., card dom route-1} - & InvTrackIsConnected(route(x),route(x+1)); - inv card dom route = card dom transponders; - inv forall tr in set rng route & - tr.startX > 0 and tr.startY > 0 and tr.endX > 0 and tr.endY > 0; - inv started = true and speed >= 0 or started = false and speed = 0; - inv speed <= route(currentTrack).maxSpeed; - operations public Step: () ==> () Step() == @@ -41,8 +30,8 @@ operations private Drive: () ==> () Drive() == ( - if (state = and len timetable > 0) then ( - dcl currentRoute : Interlocking`Route := hd timetable; + if (state = and len routeTable > 0) then ( + dcl currentRoute : Interlocking`Route := hd routeTable; UpdateStats(); if(rbc.RequestMovementAuthority(currentRoute) = ) then ( @@ -50,12 +39,12 @@ operations for track in GetTracksInRoute(currentRoute) do ( dcl currentEb : Eurobalise := transponders(track); currentEb.Enter(); - speed := track.maxSpeed; + currentSpeed := track.maxSpeed; posX := track.endX; posY := track.endY; UpdateStats(); ); - timetable := tl timetable; + routeTable := tl routeTable; UpdateStats(); ) else ( state := ; @@ -70,9 +59,9 @@ operations public AddRoute: Interlocking`Route ==> () AddRoute(rt) == - timetable := timetable ^ [rt]; + routeTable := routeTable ^ [rt]; - public GetStats: () ==> seq of TrainLogEntry + pure public GetStats: () ==> seq of TrainLogEntry GetStats() == return trainLog; @@ -93,53 +82,35 @@ operations public Stop: () ==> () Stop() == state := ; - - public GetPosX: () ==> real - GetPosX() == - return posX; - public GetPosY: () ==> real - GetPosY() == - return posY; - - public GetSpeed: () ==> real - GetSpeed() == - return speed; - + public GetRoute: () ==> Interlocking`Route + GetRoute() == + return hd routeTable; + public GetId: () ==> seq of char GetId() == return id; - public GetRoute: () ==> Interlocking`Route - GetRoute() == - return hd timetable; - public IsRunning: () ==> bool IsRunning() == if state = then return true else return false; - public GetMovementAuths: () ==> set of Interlocking`Track - GetMovementAuths() == - return {tr | tr in set dom movementAuths & movementAuths(tr) = true}; - - public Train: map nat to Interlocking`Track - * map Interlocking`Track to Eurobalise * RadioBlockCenter * seq of char ==> Train - Train(rtmap,trans,prbc, pid) == + public Train: map Interlocking`Track to Eurobalise + * RadioBlockCenter * seq of char ==> Train + Train(trans, prbc, pid) == atomic ( - posX := rtmap(1).startX; - posY := rtmap(1).startY; - currentTrack := 1; - route := rtmap; + --posX := rtmap(1).startX; + --posY := rtmap(1).startY; transponders := trans; rbc := prbc; - movementAuths := {x |-> false | x in set rng rtmap}; id := pid; ); functions - public InvTrackIsConnected: Interlocking`Track * Interlocking`Track -> bool - InvTrackIsConnected(tr1, tr2) == - tr1.endX = tr2.startX and tr1.endY = tr2.startY; + public InvTrackIsConnected: Interlocking`Route -> bool + InvTrackIsConnected(rt) == + forall tr1,tr2 in set rt + & tr1.endX = tr2.startX and tr1.endY = tr2.startY; end Train \ No newline at end of file diff --git a/ERTMS/World.vdmpp b/ERTMS/World.vdmpp index d8d5908..a11a018 100644 --- a/ERTMS/World.vdmpp +++ b/ERTMS/World.vdmpp @@ -22,56 +22,53 @@ values private track10 = mk_Interlocking`Track(25,7,28,5,"L-DE", 90); private track11 = mk_Interlocking`Track(28,5,33,5,"L-EF", 90); - --two routes - private route1 = {track1, track2, track3, track7, track8, track9}; - private route2 = {track4, track5, track6, track7, track10, track11}; + --five routes for all parts of the world + private routeFU = {track1, track2, track3}; + private routeFL = {track4, track5, track6}; + private routeB = {track7}; + private routeLU = {track8, track9}; + private routeLL = {track10, track11}; + + --all tracks in system private allTracks = {track1, track2, track3, track4, track5, track6, track7, track8, track9, track10, track11}; - --global interlocking system for all routes + --global interlocking system, initial empty table private itl = new Interlocking({}); - --global controller for itl - private controller = new Controller([route1, route2], itl); + --global controller, feeds routes to ITL + private controller = new Controller([routeFU, routeFL, + routeB, routeLU, routeLL], itl); - --global radioblockcenter + --global radioblockcenter, no available routes, covers all tracks private rbc = new RadioBlockCenter({}, allTracks, itl); - -- Eurobalise maps for each train - private trackEbMap1 = {track1 |-> new Eurobalise(itl, track1), track2 |-> new Eurobalise(itl, track2), - track3 |-> new Eurobalise(itl, track3), track7 |-> new Eurobalise(itl, track7), - track8 |-> new Eurobalise(itl, track8), track9 |-> new Eurobalise(itl, track9)}; - - private trackEbMap2 = {track4 |-> new Eurobalise(itl, track4), track5 |-> new Eurobalise(itl, track5), - track6 |-> new Eurobalise(itl, track6), track7 |-> new Eurobalise(itl, track7), - track10 |-> new Eurobalise(itl, track10), track11 |-> new Eurobalise(itl, track11)}; + -- Eurobalise maps for trains + private trackEbMap = {track1 |-> new Eurobalise(itl, track1), track2 |-> new Eurobalise(itl, track2), + track3 |-> new Eurobalise(itl, track3), track4 |-> new Eurobalise(itl, track4), + track5 |-> new Eurobalise(itl, track5), track6 |-> new Eurobalise(itl, track6), + track7 |-> new Eurobalise(itl, track7), track8 |-> new Eurobalise(itl, track8), + track9 |-> new Eurobalise(itl, track9), track10 |-> new Eurobalise(itl, track10), + track11 |-> new Eurobalise(itl, track11)}; - -- Route maps for each train - private routeMap1 = {1 |-> track1, 2 |-> track2, 3 |-> track3, - 4 |-> track7, 5 |-> track8, 6 |-> track9}; - private routeMap2 = {1 |-> track4, 2 |-> track5, 3 |-> track6, - 4 |-> track7, 5 |-> track10, 6 |-> track11}; + -- Routetables for trains + private timeTable1 = [routeFU, routeB, routeLU]; + private timeTable2 = [routeFL, routeB, routeLL]; - -- Trains have different routes, but same RBC - private trains: seq of Train = [new Train(routeMap1, trackEbMap1, rbc, "IC1"), - new Train(routeMap2, trackEbMap2, rbc, "IC2")]; + -- Create trains + private trains: seq of Train = [new Train(trackEbMap, rbc, "IC1"), + new Train(trackEbMap, rbc, "IC2")]; -instance variables - operations public World: () ==> World - World() == InitialiseSystem(); + World() == InitialiseSystem(); private InitialiseSystem: () ==> () - InitialiseSystem() == - ( - for train in trains do train.Start(); - controller.Step(); - controller.Step(); - controller.Step(); - controller.Step(); - controller.Step(); - ); + InitialiseSystem() == + ( + for route in timeTable1 do trains(1).AddRoute(route); + for route in timeTable2 do trains(2).AddRoute(route); + ); public Run: nat ==> () Run(stepLimit) == @@ -82,10 +79,11 @@ operations for train in trains do ( train.Step(); - Print("Train: " ^ VDMUtil`val2seq_of_char[seq of char](train.GetId()) - ^ " pos: " ^ VDMUtil`val2seq_of_char[real](train.GetPosX()) - ^ "-" ^ VDMUtil`val2seq_of_char[real](train.GetPosY()) - ^ " on track: " ^ VDMUtil`val2seq_of_char[Interlocking`Track](train.GetTrack())); + -- print stats + Print("Stats for train: " ^ + VDMUtil`val2seq_of_char[seq of char](train.GetId()) + ^ " @ " ^ + VDMUtil`val2seq_of_char[seq of Train`TrainLogEntry](train.GetStats())); ) ); From 27c011c9ce4662ca6fc9ec159e381fe272deef02 Mon Sep 17 00:00:00 2001 From: Christian Lillelund Date: Mon, 3 Dec 2018 23:17:25 +0100 Subject: [PATCH 6/6] Sim completed + results --- ERTMS/Interlocking.vdmpp | 12 ++-- ERTMS/Train.vdmpp | 45 ++++++++----- ERTMS/World.vdmpp | 7 +- SimulationResults.txt | 42 ++++++++++++ old_train.txt | 58 ----------------- old_train_test.txt | 137 --------------------------------------- 6 files changed, 80 insertions(+), 221 deletions(-) create mode 100644 SimulationResults.txt delete mode 100644 old_train.txt delete mode 100644 old_train_test.txt diff --git a/ERTMS/Interlocking.vdmpp b/ERTMS/Interlocking.vdmpp index cd667fc..4b879c8 100644 --- a/ERTMS/Interlocking.vdmpp +++ b/ERTMS/Interlocking.vdmpp @@ -24,7 +24,7 @@ types instance variables private trackTable : map Track to bool; -- track table with physical state of track - private availableRoutes : set of Route; -- routes not planned to be occupied + private availableRoutes : set of Route; -- routes from controller to be used inv InvNoDuplicateTrack(availableRoutes); -- inv InvNoTrackAvailableAndOccupied(trackTable, availableRoutes); @@ -62,16 +62,14 @@ operations public RequestRoute: (Route) ==> () RequestRoute(rt) == -- if route is not in routesAvaliable and the tracks are not occupied , - -- then add it to routesAvaliable and clear trackTable -- else do nothing + -- then add it to routesAvaliable and clear trackTable -- else do nothing if (rt not in set availableRoutes and forall tr in set rt & tr not in set dom trackTable or trackTable(tr) = false) then ( - atomic ( availableRoutes := availableRoutes union {rt}; - trackTable := trackTable ++ {let tr in set rt in tr |-> false} - ) - ) else skip; + trackTable := trackTable ++ { tr |-> false | tr in set GetTracksInRoutes({rt})}; + ) else skip; public SetTrackState: Track * Eurobalise`TrainState ==> () SetTrackState(tr, sta) == @@ -80,7 +78,7 @@ operations if(sta = ) then trackTable := trackTable ++ {tr |-> true} else if (sta = ) then - trackTable := trackTable ++ {tr|->false} + trackTable := trackTable ++ {tr |-> false} post tr in set dom trackTable; pure public GetAvaliableRoutes: () ==> set of Route diff --git a/ERTMS/Train.vdmpp b/ERTMS/Train.vdmpp index b14e10c..d8f3b05 100644 --- a/ERTMS/Train.vdmpp +++ b/ERTMS/Train.vdmpp @@ -1,24 +1,25 @@ class Train types - public State = | | ; + public State = | | | ; public TrainLogEntry :: id : seq of char state : State posX : real posY : real instance variables - private posX : real := 0; - private posY : real := 0; - private currentSpeed : real := 0; + private posX : nat := 0; + private posY : nat := 0; + private currentSpeed : nat := 0; private transponders : map Interlocking`Track to Eurobalise := {|->}; private id : seq of char := ""; private state: State := ; private routeTable: seq of Interlocking`Route := []; private trainLog: seq of TrainLogEntry := []; private rbc : RadioBlockCenter; - inv forall rt in seq routeTable & InvTrackIsConnected(rt); +-- inv forall rt in seq routeTable & InvTrackIsConnected(rt); inv state = and currentSpeed >= 0 - or state = and currentSpeed = 0; + or state = and currentSpeed = 0 + or state = and currentSpeed = 0; operations public Step: () ==> () @@ -30,24 +31,32 @@ operations private Drive: () ==> () Drive() == ( - if (state = and len routeTable > 0) then ( + if (state = or state = + and len routeTable > 0) then ( dcl currentRoute : Interlocking`Route := hd routeTable; UpdateStats(); if(rbc.RequestMovementAuthority(currentRoute) = ) then ( + state := ; UpdateStats(); for track in GetTracksInRoute(currentRoute) do ( dcl currentEb : Eurobalise := transponders(track); - currentEb.Enter(); currentSpeed := track.maxSpeed; + currentEb.Enter(); posX := track.endX; posY := track.endY; + currentEb.Leave(); UpdateStats(); ); routeTable := tl routeTable; + if (routeTable = []) then ( + currentSpeed := 0; + state := ; + ); UpdateStats(); ) else ( - state := ; + currentSpeed := 0; + state := ; UpdateStats(); ) ) else UpdateStats(); @@ -55,11 +64,17 @@ operations private UpdateStats: () ==> () UpdateStats() == - trainLog := trainLog ^ [mk_TrainLogEntry(id, state, posX, posY)]; + ( + trainLog := trainLog ^ [mk_TrainLogEntry(id, state, posX, posY)]; + if(len trainLog > 3) then + trainLog := tl trainLog; + ); public AddRoute: Interlocking`Route ==> () AddRoute(rt) == - routeTable := routeTable ^ [rt]; + routeTable := routeTable ^ [rt] + pre card rt > 0 + post rt = routeTable(len routeTable); pure public GetStats: () ==> seq of TrainLogEntry GetStats() == @@ -108,9 +123,9 @@ operations ); functions - public InvTrackIsConnected: Interlocking`Route -> bool - InvTrackIsConnected(rt) == - forall tr1,tr2 in set rt - & tr1.endX = tr2.startX and tr1.endY = tr2.startY; +-- public InvTrackIsConnected: Interlocking`Route -> bool +-- InvTrackIsConnected(rt) == +-- forall tr1,tr2 in set rt & tr1 <> tr2 => +-- tr1.endX = tr2.startX and tr1.endY = tr2.startY; end Train \ No newline at end of file diff --git a/ERTMS/World.vdmpp b/ERTMS/World.vdmpp index a11a018..0079d16 100644 --- a/ERTMS/World.vdmpp +++ b/ERTMS/World.vdmpp @@ -66,8 +66,8 @@ operations private InitialiseSystem: () ==> () InitialiseSystem() == ( - for route in timeTable1 do trains(1).AddRoute(route); - for route in timeTable2 do trains(2).AddRoute(route); + for route in timeTable1 do (trains(1).AddRoute(route); trains(1).Start()); + for route in timeTable2 do (trains(2).AddRoute(route); trains(2).Start()); ); public Run: nat ==> () @@ -81,8 +81,7 @@ operations train.Step(); -- print stats Print("Stats for train: " ^ - VDMUtil`val2seq_of_char[seq of char](train.GetId()) - ^ " @ " ^ + VDMUtil`val2seq_of_char[seq of char](train.GetId()) ^ " @ " ^ VDMUtil`val2seq_of_char[seq of Train`TrainLogEntry](train.GetStats())); ) ); diff --git a/SimulationResults.txt b/SimulationResults.txt new file mode 100644 index 0000000..ea0bcb9 --- /dev/null +++ b/SimulationResults.txt @@ -0,0 +1,42 @@ +Step: 1 +Stats for train: "IC1" @ [mk_TrainLogEntry("IC1", , 0, 0), mk_TrainLogEntry("IC1", , 0, 0)] +Stats for train: "IC2" @ [mk_TrainLogEntry("IC2", , 20, 5), mk_TrainLogEntry("IC2", , 17, 7), mk_TrainLogEntry("IC2", , 17, 7)] +Step: 2 +Stats for train: "IC1" @ [mk_TrainLogEntry("IC1", , 0, 0), mk_TrainLogEntry("IC1", , 0, 0), mk_TrainLogEntry("IC1", , 0, 0)] +Stats for train: "IC2" @ [mk_TrainLogEntry("IC2", , 17, 7), mk_TrainLogEntry("IC2", , 17, 7), mk_TrainLogEntry("IC2", , 17, 7)] +Step: 3 +Stats for train: "IC1" @ [mk_TrainLogEntry("IC1", , 0, 0), mk_TrainLogEntry("IC1", , 0, 0), mk_TrainLogEntry("IC1", , 0, 0)] +Stats for train: "IC2" @ [mk_TrainLogEntry("IC2", , 17, 7), mk_TrainLogEntry("IC2", , 25, 7), mk_TrainLogEntry("IC2", , 25, 7)] +Step: 4 +Stats for train: "IC1" @ [mk_TrainLogEntry("IC1", , 0, 0), mk_TrainLogEntry("IC1", , 0, 0), mk_TrainLogEntry("IC1", , 0, 0)] +Stats for train: "IC2" @ [mk_TrainLogEntry("IC2", , 28, 5), mk_TrainLogEntry("IC2", , 33, 5), mk_TrainLogEntry("IC2", , 33, 5)] +Step: 5 +Stats for train: "IC1" @ [mk_TrainLogEntry("IC1", , 0, 0), mk_TrainLogEntry("IC1", , 0, 0), mk_TrainLogEntry("IC1", , 0, 0)] +Stats for train: "IC2" @ [mk_TrainLogEntry("IC2", , 33, 5), mk_TrainLogEntry("IC2", , 33, 5), mk_TrainLogEntry("IC2", , 33, 5)] +Step: 6 +Stats for train: "IC1" @ [mk_TrainLogEntry("IC1", , 0, 0), mk_TrainLogEntry("IC1", , 0, 0), mk_TrainLogEntry("IC1", , 0, 0)] +Stats for train: "IC2" @ [mk_TrainLogEntry("IC2", , 33, 5), mk_TrainLogEntry("IC2", , 33, 5), mk_TrainLogEntry("IC2", , 33, 5)] +Step: 7 +Stats for train: "IC1" @ [mk_TrainLogEntry("IC1", , 0, 0), mk_TrainLogEntry("IC1", , 0, 0), mk_TrainLogEntry("IC1", , 0, 0)] +Stats for train: "IC2" @ [mk_TrainLogEntry("IC2", , 33, 5), mk_TrainLogEntry("IC2", , 33, 5), mk_TrainLogEntry("IC2", , 33, 5)] +Step: 8 +Stats for train: "IC1" @ [mk_TrainLogEntry("IC1", , 0, 0), mk_TrainLogEntry("IC1", , 0, 0), mk_TrainLogEntry("IC1", , 0, 0)] +Stats for train: "IC2" @ [mk_TrainLogEntry("IC2", , 33, 5), mk_TrainLogEntry("IC2", , 33, 5), mk_TrainLogEntry("IC2", , 33, 5)] +Step: 9 +Stats for train: "IC1" @ [mk_TrainLogEntry("IC1", , 0, 0), mk_TrainLogEntry("IC1", , 0, 0), mk_TrainLogEntry("IC1", , 0, 0)] +Stats for train: "IC2" @ [mk_TrainLogEntry("IC2", , 33, 5), mk_TrainLogEntry("IC2", , 33, 5), mk_TrainLogEntry("IC2", , 33, 5)] +Step: 10 +Stats for train: "IC1" @ [mk_TrainLogEntry("IC1", , 0, 0), mk_TrainLogEntry("IC1", , 0, 0), mk_TrainLogEntry("IC1", , 0, 0)] +Stats for train: "IC2" @ [mk_TrainLogEntry("IC2", , 33, 5), mk_TrainLogEntry("IC2", , 33, 5), mk_TrainLogEntry("IC2", , 33, 5)] +Step: 11 +Stats for train: "IC1" @ [mk_TrainLogEntry("IC1", , 20, 10), mk_TrainLogEntry("IC1", , 17, 7), mk_TrainLogEntry("IC1", , 17, 7)] +Stats for train: "IC2" @ [mk_TrainLogEntry("IC2", , 33, 5), mk_TrainLogEntry("IC2", , 33, 5), mk_TrainLogEntry("IC2", , 33, 5)] +Step: 12 +Stats for train: "IC1" @ [mk_TrainLogEntry("IC1", , 17, 7), mk_TrainLogEntry("IC1", , 25, 7), mk_TrainLogEntry("IC1", , 25, 7)] +Stats for train: "IC2" @ [mk_TrainLogEntry("IC2", , 33, 5), mk_TrainLogEntry("IC2", , 33, 5), mk_TrainLogEntry("IC2", , 33, 5)] +Step: 13 +Stats for train: "IC1" @ [mk_TrainLogEntry("IC1", , 28, 10), mk_TrainLogEntry("IC1", , 35, 10), mk_TrainLogEntry("IC1", , 35, 10)] +Stats for train: "IC2" @ [mk_TrainLogEntry("IC2", , 33, 5), mk_TrainLogEntry("IC2", , 33, 5), mk_TrainLogEntry("IC2", , 33, 5)] +Step: 14 +Stats for train: "IC1" @ [mk_TrainLogEntry("IC1", , 35, 10), mk_TrainLogEntry("IC1", , 35, 10), mk_TrainLogEntry("IC1", , 35, 10)] +Stats for train: "IC2" @ [mk_TrainLogEntry("IC2", , 33, 5), mk_TrainLogEntry("IC2", , 33, 5), mk_TrainLogEntry("IC2", , 33, 5)] \ No newline at end of file diff --git a/old_train.txt b/old_train.txt deleted file mode 100644 index 2a8299a..0000000 --- a/old_train.txt +++ /dev/null @@ -1,58 +0,0 @@ -private Drive: () ==> () - Drive() == - -- Drive() performs one iteration of moving the train - ( -- continue if there is track to traverse - if(currentTrack <= card dom route and started) then - ( - dcl currentEb : Eurobalise := transponders(route(currentTrack)); - dcl distX : real := route(currentTrack).endX-posX; - dcl distY : real := route(currentTrack).endY-posY; - -- make sure we have MoA for current track - if (movementAuths(route(currentTrack))) then ( - -- check where the train is currently - if (posX = route(currentTrack).startX and posY = route(currentTrack).startY) - then ( - -- enter track and drive halfway - currentEb.Enter(); - if (distX = 0 and distY <> 0) then ( posY := posY + distY/2; ) - else if (distY = 0 and distX <> 0) then ( posX := posX + distX/2; ) - else if (distY <> 0 and distX <> 0) then - ( posY := posY + distY/2; posX := posX + distX/2; ); - ) else if (posX = route(currentTrack).endX and posY = route(currentTrack).endY) - then ( - -- leave current track, adjust speed to next track - currentEb.Leave(); - if(currentTrack+1 < card dom route) then - atomic ( - speed := route(currentTrack+1).maxSpeed; - currentTrack := currentTrack+1; - ) else - speed := 0; - ) else ( - -- we are midway. request MoA for next track, if there is such - if (card dom route > currentTrack) then ( - if(rbc.RequestMovementAuthority(route(currentTrack+1)) = ) - then ( movementAuths := movementAuths ++ {route(currentTrack) |-> true}; ) - ); - -- drive the remaining way - if (distX = 0 and distY <> 0) then ( posY := posY + distY; ) - else if (distY = 0 and distX <> 0) then ( posX := posX + distX; ) - else if (distX <> 0 and distY <> 0) then - ( posY := posY + distY; posX := posX + distX; ); - ); - ) else ( - -- get MoA for current track - if(rbc.RequestMovementAuthority(route(currentTrack)) = ) - then ( - movementAuths := movementAuths ++ {route(currentTrack) |-> true}; - started := true; - ) else ( - -- could not get MoA. Stopping ... - speed := 0; - ) - ) - ) else ( - -- train has reached end of route, stop - speed := 0; started := false - ) - ); \ No newline at end of file diff --git a/old_train_test.txt b/old_train_test.txt deleted file mode 100644 index 8ec8724..0000000 --- a/old_train_test.txt +++ /dev/null @@ -1,137 +0,0 @@ -class TrainTest is subclass of TestCase - -values - tracks = {mk_Interlocking`Track(10,5,15,5,"AB",100), - mk_Interlocking`Track(15,5,20,5,"BC",90)}; - - routeMap = {1 |-> mk_Interlocking`Track(10,5,15,5,"AB",100), - 2 |-> mk_Interlocking`Track(15,5,20,5,"BC",90)}; - - track1 = mk_Interlocking`Track(10,5,15,5,"AB",100); - track2 = mk_Interlocking`Track(15,5,20,5,"BC",90); - -instance variables - private uut: Train; - private rbc: RadioBlockCenter; - private itl: Interlocking; - private eb1 : Eurobalise; - private eb2 : Eurobalise; - -operations - public TrainTest: () ==> TrainTest - TrainTest() == - ( - itl := new Interlocking({tracks}); - eb1 := new Eurobalise(itl, track1); - eb2 := new Eurobalise(itl, track2); - rbc := new RadioBlockCenter({tracks}, tracks, itl); - uut := new Train(routeMap, {track1 |-> eb1, track2 |-> eb2}, rbc, "IC1"); - ); - - public Test_CtorCalled_TrainIsCreatedWithStartPos: () ==> () - Test_CtorCalled_TrainIsCreatedWithStartPos() == - ( - assertTrue(uut.GetPosX() = routeMap(1).startX); - assertTrue(uut.GetPosY() = routeMap(1).startY); - ); - - public Test_TrackOccupieod_MoADeniedAndTrainStandingStill: () ==> () - Test_TrackOccupieod_MoADeniedAndTrainStandingStill() == - ( - itl.SetTrackState(routeMap(1), ); - uut.Start(); - assertTrue(uut.IsStarted()); - uut.Step(); - assertTrue(uut.GetSpeed() = 0); - ); - - public Test_TrackFree_TrainGetsMoa: () ==> () - Test_TrackFree_TrainGetsMoa() == - ( - uut.Start(); - uut.Step(); - uut.Step(); - assertTrue(routeMap(1) in set uut.GetMovementAuths()); - ); - - public Test_TrackFree_TrainGetsMoaAndEntersTrack: () ==> () - Test_TrackFree_TrainGetsMoaAndEntersTrack() == - ( - uut.Start(); - uut.Step(); - -- track is not occupied in ITL - assertTrue(itl.GetTrackTable() = {}); - uut.Step(); - -- track is now occupied in ITL - assertTrue(routeMap(1) in set itl.GetTrackTable()); - ); - - public Test_TrackFree_TrainGetsMoaAndDrivesHalfWay: () ==> () - Test_TrackFree_TrainGetsMoaAndDrivesHalfWay() == - ( - dcl pointX : real := (routeMap(1).endX-routeMap(1).startX)/2; - uut.Start(); - uut.Step(); - uut.Step(); - assertTrue(uut.GetPosX() = routeMap(1).startX+pointX); - ); - - public Test_TrainIsHalfWay_TrainGetsMoaForNextTrack: () ==> () - Test_TrainIsHalfWay_TrainGetsMoaForNextTrack() == - ( - uut.Start(); - uut.Step(); - uut.Step(); - uut.Step(); - assertTrue(routeMap(2) in set uut.GetMovementAuths()); - ); - - public Test_TrainIsHalfWay_TrainDrivesToEnd: () ==> () - Test_TrainIsHalfWay_TrainDrivesToEnd() == - ( - uut.Start(); - uut.Step(); - uut.Step(); - uut.Step(); - assertTrue(uut.GetPosX() = routeMap(1).endX); - assertTrue(uut.GetPosY() = routeMap(1).endY); - ); - - public Test_TrainIsAtTheEnd_LeavesCurrentTrack: () ==> () - Test_TrainIsAtTheEnd_LeavesCurrentTrack() == - ( - uut.Start(); - uut.Step(); - uut.Step(); - uut.Step(); - uut.Step(); - assertTrue(routeMap(1) not in set itl.GetTrackTable()); - ); - - public Test_TrainIsAtTheEnd_EntersNewTrack: () ==> () - Test_TrainIsAtTheEnd_EntersNewTrack() == - ( - uut.Start(); - uut.Step(); - uut.Step(); - uut.Step(); - uut.Step(); - uut.Step(); - assertTrue(routeMap(2) in set itl.GetTrackTable()); - ); - - public Test_TrainAtNextTrack_TrainDrivesToEnd: () ==> () - Test_TrainAtNextTrack_TrainDrivesToEnd() == - ( - uut.Start(); - uut.Step(); - uut.Step(); - uut.Step(); - uut.Step(); - uut.Step(); - uut.Step(); - assertTrue(uut.GetPosX() = routeMap(2).endX); - assertTrue(uut.GetPosY() = routeMap(2).endY); - ); - -end TrainTest \ No newline at end of file