Merge pull request #2 from thecml/feature-newtrain

Feature newtrain

ERTMS/Interlocking.vdmpp

@@ -23,87 +23,97 @@ types
 												 rt : Route
 
 instance variables
-	private occupiedTracks : map Track to bool; -- physically occupied track
-	private availableRoutes : set of Route; -- routes not planned to be occupied
+	private trackTable : map Track to bool; -- track table with physical state of track
+	private availableRoutes : set of Route; -- routes from controller to be used
 
 	inv InvNoDuplicateTrack(availableRoutes);
-	inv InvNoTrackAvailableAndOccupied(occupiedTracks, 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 (
-			let rt in set availableRoutes in
-				if(prt subset rt and forall tr in set prt & occupiedTracks(tr) = false)
-					then return mk_ProceedReply(<PROCEED_GRANTED>, availableRoutes)
-			else return mk_ProceedReply(<PROCEED_DENIED>, 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 := {rts | rts in set availableRoutes
+						 & forall ptrs in set {prt} & rts inter ptrs = {}};
+						 return ProceedGranted(respTrs);
+					)
+					else
+						return ProceedDenied(respTrs)
+			else return ProceedDenied(respTrs)
 			) else (
-				return mk_ProceedReply(<PROCEED_DENIED>, availableRoutes);
+				return ProceedDenied(respTrs)
 			)
 	pre card prt > 0;
-
+
+	private ProceedGranted: set of Track ==> ProceedReply
+	ProceedGranted(respTrs) ==
+		return mk_ProceedReply(<PROCEED_GRANTED>, availableRoutes inter {respTrs});
+
+	private ProceedDenied: set of Track ==> ProceedReply
+	ProceedDenied(respTrs) ==
+		return mk_ProceedReply(<PROCEED_DENIED>, availableRoutes inter {respTrs});
+
 	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 (
+							availableRoutes := availableRoutes union {rt};
+							trackTable := trackTable ++ { tr |-> false | tr in set GetTracksInRoutes({rt})};	
+					) 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 = <TRAIN_ENTER>) then (
-		atomic (
-				occupiedTracks := occupiedTracks ++ {tr |-> true};
-				availableRoutes := {rt | rt in set availableRoutes & rt inter {tr} = {}};
-				)
-			)
-		else if (sta = <TRAIN_LEAVE>) then (
-		atomic (
-				occupiedTracks := occupiedTracks ++ {tr|->false};
-				availableRoutes := availableRoutes union {{tr}};
-				)
-			)
-		post tr in set dom occupiedTracks;
+		if(sta = <TRAIN_ENTER>) then
+				trackTable := trackTable ++ {tr |-> true}
+		else if (sta = <TRAIN_LEAVE>) 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)};
-		 )
-
+			trackTable := { tr |-> false | tr in set GetTracksInRoutes(rts)};
+		 );
+
+	pure public GetTracksInRoutes: set of Route ==> set of Track
+	GetTracksInRoutes(rts) ==
+		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 GetTracksInRoute: set of Route -> set of Track
-	GetTracksInRoute(rts) ==
-	(
-		if (card rts > 0) then (let rt in set rts in rt) else {}
-	);
-
 	public InvNoTrackAvailableAndOccupied: map Track to bool * set of Route -> bool
 	InvNoTrackAvailableAndOccupied(trmap, rts) ==
 	-- A track cannot be available and occupied.

ERTMS/RadioBlockCenter.vdmpp

@@ -10,53 +10,48 @@ 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;
 
 	inv Interlocking`InvNoDuplicateTrack(availableRoutes);
 
 operations	
-	public RequestMovementAuthority: Interlocking`Track ==> MovementAuthorityReply
-	RequestMovementAuthority(tr) ==
-	if (card availableRoutes > 0) then
+	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)
-			then (
-					dcl msg : Interlocking`Order;
-					def mk_Interlocking`ProceedReply(message,rtr) = itl.RequestToProceed({tr})
-					in
-						(
-						msg := message; availableRoutes := rtr; );
-						if (msg = <PROCEED_GRANTED>)
-							then ( return <MovementAuthorityGranted>; )
-					 	else (
-					availableRoutes := {{tr} | art in set availableRoutes & art inter {tr} = {}};
-					return <MovementAuthorityDenied>;
+		--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(rt subset respTracks) then (
+				dcl msg : Interlocking`Order;
+				def mk_Interlocking`ProceedReply(message,rtr) = itl.RequestToProceed(rt, respTracks)
+				in (
+					msg := message;
+					availableRoutes := rtr; );
+					if (msg = <PROCEED_GRANTED>)
+						then ( return <MovementAuthorityGranted>; )
+				 	else (
+				--availableRoutes := {{tr} | art in set availableRoutes & art inter {tr} = {}};
+				return <MovementAuthorityDenied>;
 				)
 		) else return <MovementAuthorityDenied>;
-	) else return <MovementAuthorityDenied>;
-
-	private GetAvailableRoutesFromItl: () ==> ()
-	GetAvailableRoutesFromItl() ==
-		availableRoutes := itl.GetAvaliableRoutes(responsibleTracks);
+	);
 
 	public GetAvailableRoutes: () ==> set of Interlocking`Route
 	GetAvailableRoutes() ==
 		return availableRoutes;
 
 	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 := {|->};
 	);

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);
 	);
 

ERTMS/Test/InterlockingTest.vdmpp

@@ -41,15 +41,15 @@ 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 = <PROCEED_GRANTED>);
 	);
 
 	public Test_RouteNotInAvaRoutes_ProceedDenied: () ==> ()
 	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 = <PROCEED_DENIED>);
 	);
 
@@ -66,9 +66,9 @@ operations
 	(
 		dcl track : Interlocking`Track := mk_Interlocking`Track(10,5,15,5,"AB",100);
 		uut.SetTrackState(track, <TRAIN_ENTER>);
-		assertTrue(track in set uut.GetOccupiedTracks());
+		assertTrue(track in set uut.GetTrackTable());
 		uut.SetTrackState(track, <TRAIN_LEAVE>);
-		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, <TRAIN_ENTER>);
 		uut.SetTrackState(tr, <TRAIN_LEAVE>);
-		assertTrue(tr not in set uut.GetOccupiedTracks());
+		assertTrue(tr not in set uut.GetTrackTable());
 	);
 
 	public Test_RouteHasNoDuplicateTrack_InvSucceed: () ==> ()

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 = <MovementAuthorityGranted>);
 	);
 
-	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 = <MovementAuthorityDenied>);
 	);