getRouteLockingRelaysCoveringP A wrapper function that finds all the routes from the train route table and calls getRLRsCoveringP. Then getRLRsCov-eringP recursively runs through the routes and calls getRLRCovgetRLRsCov-eringP. Finally, if the given points section is covered by the given route, then the related route locking relay is returned by getRLRCoveringP.
genPointsOpUpdate Returns a set of assignments by updating the idle and updating the points relay to either being locked into a position or intermediate depending on which case.
convRelayIdsToLiterals Converts a set of relay ids into literals to be used in a boolean expression.
11.4 Assertion Generator
This section introduces the assertion generator and describes important parts in the specification. The patterns introduced in chapter 9about inter-model consistency, and chapter 10about safety properties described the assertions in general form. This section will use these patterns and apply them as guidelines to implement the assertion generator.
The assertion generator handles the generation of the safety properties and inter-model consistency conditions. The safety properties consists of no collision and no derailing assertions and other requirements derived from the train route table.
The inter-model consistency consists of conditions that ensure the interaction between the train movement model and the internal relay system model behaves as expected.
Thus, the assertion generator is split into three parts, one for inter-model con-sistency, one for safety conditions assertions and one for the assertions derived from the train route table.
Inter-model consistency consist of the following conditions each with reference back to the patterns mentioned earlier.
• Track Occupation (Section9.2).
168 Generator
• Track Free (Section9.3).
• Train Direction (Section9.4).
• Points Configuration (Section9.5).
• Train Connection (Section 9.6).
The basic safety properties consists of the following conditions each with a reference back to the patterns mentioned earlier.
• No collision (Section 10.2).
• No derailing (Section 10.3).
And lastly, the safety properties derived from the train route table consists of the following conditions each with a reference back to the patterns mentioned earlier.
• Points Position (Section10.4).
• Signal (Section10.5).
• Signal Release (Section 10.6).
• Conflicting Routes (Section10.7).
• Train Route Release (Section10.8).
The following sections will present a description of how a single assertion is generated by introducing some general rules and then an overview of how the assertions are generated. Finally an example from our specification showing how the signal release assertion is generated.
11.4.1 Generating a Single Assertion
RSL-SAL assertions have the following general form:
[ assertionName ] TransitionSystem `TemporalLogic
11.4 Assertion Generator 169
where assertionName is a unique identifier for the assertion. The Transistion-System is the name of the transition system and TemporalLogic is the LTL expression checking the validity of the model/transition system.
The abstract syntax of this is given by the RSL Assertion type. This type was described in section 4.4.4.
In the example below the generateSomeAssertion function accepts two para-meters. This is simply to show the structure, where the number of parameters typically range from two to five.
Generating an assertion has the following general form:
generateSomeAssertion : ...×...→T.Assertion generateSomeAssertion(...,...)≡
(00some_assertion_name00 btoString(...), TransitionSystem,
genSomeFormula(...,...) ),
The name is made unique by concatenating an indicative identifier to the name, where we usually use a track section id, route id or signal id. TheTransitionSystem is simply a variable, that contains the name of the current transition system used in all the generated assertions, namelyInterlockingSystem.
Finally, thegenSomeFormula function is invoked to generate the LTL expressions.
In the simplest form all the assertions consist of a boolean expression implying another boolean expression. The inter-model consistency conditions and the safety properties described in chapter 9 and chapter 10 all requires that the expressions must hold true in all states. Thus, applyingglobally on the general form.
By invoking the functiongenSomeFormula it returns a LTLformula defined in section4.4.4.
Hence, the generated LTLformula has the following general form:
genSomeFormula : ...×... →LTLformula genSomeFormula(...,...)≡
g(impl(...,...))
This would generate the following LTL formula:
170 Generator
G(...⇒...)
11.4.2 Specifying the Assertion Generator
AssertionGenerator.rsl supply the function generateAssertions, which makes calls to each of the subgenerators.
value
generateAssertions :
ObjectRelayAssociations×InterlockingPlan× TrainMovementAssociations→Assertion-set generateAssertions(ora, ip, tma)≡
genConsistencyAssertions(ora, ip, tma)∪ genSafetyAssertions(ora, ip, tma)∪ genTrtAssertions(ora, ip, tma) preisWfInterlockingPlan(ip)∧
isWfTrainMovementAssociations(sld(ip), tma)∧ isWfObjectRelayAssociations(ora, ip)
11.4.2.1 Consistency Assertion Generator
The inter-model consistency assertions are generated by the consistency assertion generator. The more general assertion generator call the genConsistencyAsser-tions method of the consistency assertion generator.
value
genConsistencyAssertions :
ObjectRelayAssociations×InterlockingPlan× TrainMovementAssociations→Assertion-set genConsistencyAssertions(ora, ip, tma) ≡
- - 9.2 Track Occupation
generateOccupationAssertions(ora, ip, tma)∪ - - 9.3 Track Free
generateFreeAssertions(ora, ip, tma)∪ - - 9.4 Train Direction
generateDirectionAssertions(ip, tma)∪ - - 9.5 Points Configuration
11.4 Assertion Generator 171
generatePointsConfigurationAssertions(ora, ip)∪ - - 9.6 Train Connection
generateConnectionAssertions(ip, tma) preisWfInterlockingPlan(ip)∧
isWfTrainMovementAssociations(sld(ip), tma)∧ isWfObjectRelayAssociations(ora, ip)
Consider the track occupation consistency requirement presented in section9.2.
In the following, the specification of the generator for the related assertions will be explained.
value- - 9.2 Track Occupation
generateOccupationAssertions : ObjectRelayAssociations×
InterlockingPlan×TrainMovementAssociations→Assertion-set generateOccupationAssertions(ora, ip, tma)≡
letd = sld(ip),
sections = allLinears(d)∪allPoints(d) - - NB: No line pieces!
in generateOccupationAssertions(sections, ora, tma) end
Track Occupation requires that there must be consistency, for each track section, between the track relay variables and the track counters. Therefore the set of all track sections is given to generateOccupationAssertions.
value
generateOccupationAssertions :
TrackId-set×ObjectRelayAssociations×
TrainMovementAssociations→Assertion-set generateOccupationAssertions(sections, ora, tma)≡
ifsections ={}then{}else lets = hdsections,
sections0 = sections\ {s}
in{generateOccupationAssertion1(s, ora, tma), generateOccupationAssertion2(s, ora, tma)} ∪
generateOccupationAssertions(sections0, ora, tma) - - Recursive end
end
The function generateOccupationAssertions runs through all the track sections recursively and calls the two functions which are respondsible for generating the actual assertion for a given track section.
172 Generator
value
generateOccupationAssertion1 :
TrackId×ObjectRelayAssociations× TrainMovementAssociations→Assertion generateOccupationAssertion1(s, ora, tma)≡
(00occ_00b s,
genOccuFormula1(s, ora, tma)), genOccuFormula1 :
TrackId×ObjectRelayAssociations× TrainMovementAssociations→LTLformula genOccuFormula1(s, ora, tma) ≡
g(impl(b(greaterthan(
literal(getCounterVar(s, tma)), literal(00000))),
neg(ltrl(trackRelayAssoc(ora)(s))))),
generateOccupationAssertion2 is very similar to generateOccupationAssertion1.
However, it generates the other direction of the bi-implication.
value
generateOccupationAssertion2 :
TrackId×ObjectRelayAssociations×
TrainMovementAssociations→Assertion generateOccupationAssertion2(s, ora, tma)≡
(00occ_00b sb
00_00,
genOccuFormula2(s, ora, tma) ), genOccuFormula2 :
TrackId×ObjectRelayAssociations×
TrainMovementAssociations→LTLformula genOccuFormula2(s, ora, tma) ≡
g(
impl(neg(ltrl(trackRelayAssoc(ora)(s))),
b(greaterthan(literal(getCounterVar(s, tma)), literal(00000)))))
The functions for the other consistancy requirements are similar.
11.4 Assertion Generator 173
11.4.2.2 Safety Generator
This subgenerator is respondsable for generating the assertions for the basic safety requirements, i.e. no collision and no derailing.
value
genSafetyAssertions :
ObjectRelayAssociations×InterlockingPlan× TrainMovementAssociations→Assertion-set genSafetyAssertions(ora, ip, tma)≡
- - 10.2 No Collision
The no collistion assertions are generated by the function genNoCollisionAsser-tions, by recursively running through each track section on the station.
value- - 10.2 No Collision
genNoCollisionAssertions : InterlockingPlan× TrainMovementAssociations→Assertion-set genNoCollisionAssertions(ip, tma)≡
letd = sld(ip),
sections = allLinears(d)∪allPoints(d) - - NB: No line pieces!
in generateNoCollisionAssertions(sections, tma) end,
generateNoCollisionAssertions : TrackId-set× TrainMovementAssociations→Assertion-set generateNoCollisionAssertions(sections, tma)≡
ifsections ={}then{}else lets = hdsections,
sections0 = sections\ {s}
in{generateNoCollisionAssertion(s, tma)} ∪
generateNoCollisionAssertions(sections0, tma) - - Recursive call end
end
174 Generator
The pattern described in sections10.2 and10.3is applied to each track section on the station.
value
generateNoCollisionAssertion : TrackId× TrainMovementAssociations→Assertion generateNoCollisionAssertion(s, tma)≡
(00no_collision_00 bs, genNoColFormula(s, tma) ), genNoColFormula : TrackId×
TrainMovementAssociations→LTLformula genNoColFormula(s, tma)≡
g(b(lessthan(literal(getCounterVar(s, tma)), literal(00200))))
11.4.2.3 TRT Generator
The trt generator creates the assertions of the requirements derived from the train route table. Each requirement, as described in section10.4through10.8.
value
genTrtAssertions :
ObjectRelayAssociations×InterlockingPlan× TrainMovementAssociations→Assertion-set genTrtAssertions(ora, ip, tma)≡
- - 10.4 Points Position
genPointsPositionAssertions(ora, trt(ip))∪ - - 10.5 Signal
genSignalAssertions(ora, ip)∪ - - 10.6 Signal Release
genSignalReleaseAssertions(ora, ip)∪ - - 10.7 Conflicting Routes
genConflictingRoutesAssertions(ora, ip)∪ - - 10.8 Train Route Release
genTrainRouteReleaseAssertions(ora, ip) preisWfInterlockingPlan(ip)∧
isWfTrainMovementAssociations(sld(ip), tma)∧ isWfObjectRelayAssociations(ora, ip)