Abstract generation of behavioural seman- seman-tics

In the previous sections we have discussed different approaches for how to make a transition system that models the behaviour of aStaticInterlockingSystem. It

6.6 Abstract generation of behavioural semantics 97

has been decided to make a transition system consisting of one Boolean vari-able for each relay and one Boolean varivari-able for each button. In this context, true is equivalent to drawn or pushed while false is equivalent to dropped or released. Furthermore, it has been decided to make one transition rule per relay for drawing it and one transition rule per relay for dropping it. How to obtain these rules is specified in section 6.3.

In addition to that, section 6.5 introduced the concept of idle. The system should be set to idleif and only if no internal event is possible.

The purpose of this section is to specify a function that, given a StaticInterlock-ingSystem, can generate a transition system that models the dynamic behaviour of the given interlocking system. The transition system will be represented using abstract syntax.

The following sections will only present parts of RSL schemes. The schemes can be viewed in their full length in appendix A that contains the abstractRSL model.

6.6.1 RSL abstract syntax for RSL-SAL transition sys-tems

As previously mentioned in chapter 3, RSL-SALcontains the possibility of in-troducing several data types like maps and sets. As previously decided, the only data type we are going to need is Boolean. In the same way, it is only necessary to assign the values true or false to variables. The assigned values do not need to be evaluations of Boolean expressions.

In order to introduce abstract syntax for the RSL type Bool in a transition system, the following variant type has been added to the Types scheme (see appendix A.1, page 209):

type

Boolean == True|False

We will now introduce the TransitionSystem scheme of the abstract model in appendix A.6, page 222. To introduce the abstract syntax for a variable decla-ration in the initial state of a transition system, the following short record type has been introduced:

6.6 Abstract generation of behavioural semantics 98

type Var ::

id : T.Id val : T.Boolean

idis the variable name which is of the same type as the identifiers for components inside a StaticInterlockingSystem. It will therefore be possible to use the Ids from aStaticInterlockingSystem as variable names in the transition system. val is the value of the givenVar in the initial state.

The variables will be used in the state of the transition system. In order to define transition rules, it is necessary to define assignments. The short record type definition of an assignment is:

type

Assignment ::

id : T.Id

assign : T.Boolean

id is supposed to be equal to the id of aVar inside the state of the transition system such that assign is assigned to that variable in the next state of the transition system.

RSL-SAL allows multiple assignments as part of a transition rule. In order to introduce multiple assignments, the following data type is introduced:

type

MultipleAssignment = Assignment^∗

One could have chosen a set of assignments, but a list better reflects the fact that assignments in RSL-SAL are specified in an ordered, comma separated sequence.

Section 6.3 introduced how to compute rules for dropping and drawing relays.

Such rules are formulated in terms of the data type BooleanExp that includes literals withIds. Therefore,BooleanExp can be used directly as guard inside a transition rule. A type for transition rules that includes a guard and a Multi-pleAssignment is:

type

6.6 Abstract generation of behavioural semantics 99

TransitionRule ::

guard : T.BooleanExp

assignments : MultipleAssignment

After having introducedVar andTransitionRule, it is possible to make a type for a transition system:

type

TransitionSystem ::

state : Var^∗

transitionRules : TransitionRule^∗

One could have chosen sets instead of lists, but we prefer having the transition system as close as possible to how a realRSL-SALtransition system is specified.

6.6.1.1 Well-formed transition systems

A data type for transition systems has now been introduced. However, it has not been specified what a well-formed transition system is. In our context, a well-formedTransitionSystem is a system that corresponds to a realRSL-SAL transition system that can be type-checked.

The following well-formed function has been introduced for testing whether a TransitionSystem is well-formed:

value

isWfTransitionSystem : TransitionSystem→Bool isWfTransitionSystem(ts)≡

isWfState(state(ts))∧

areWfTransitionRules(state(ts), transitionRules(ts))

isWfState checks that the variable declarations in the state use different Ids.

areWfTransitionRules checks that:

• The identifiers used inside the guards are defined in variables of the state.

• Each multiple assignment contains minimum one assignment.

6.6 Abstract generation of behavioural semantics 100

• If identifiers are referred to by assignments, the identifiers are defined in the state.

• A multiple assignment cannot contain more than one assignment for a given identifier.

6.6.2 Transformation to a transition system

A TransitionSystem has now been defined. Therefore, it is possible to define a transformation from a StaticInterlockingSystem to aTransitionSystem. To do that, schemeStaticInterlockingSystemToTransitionSystem has been introduced in the abstractRSLmodel in appendix A.7, page 224. The scheme defines the following function to make the behavioural semantics of a StaticInterlockingSys-tem:

value

makeBehaviouralSemantics :

SIS.StaticInterlockingSystem→^∼ TS.TransitionSystem makeBehaviouralSemantics(sis)astspost

TS.isWfTransitionSystem(ts)∧stateRel(sis, ts)∧ transitionRel(sis, ts)

preSIS.isWfStaticInterlockingSystem(sis)

The function takes a well-formed StaticInterlockingSystem as argument and gives back a well-formedTransitionSystem.

The function stateRel checks that the following properties hold:

• For each relay, the initial state ofsiswill contain a variable with the same Id as the relay and an initial value that corresponds to the state of the relay in theStaticInterlockingSystem. truecorresponds to drawn andfalse corresponds to dropped.

• For each button, the initial state of sis will contain a variable with the sameId as the button andfalse as initial value.

• A variableidle is defined in the state and is initialised to false.

• No other variables are defined in the state.

The function transitionRel checks that the following properties hold: