# The Symphony IDE

Formal Modelling for Systems of Systems

Go to our GitHub Profile

## BorderTrafficExplv2

Author:

This example models the traffic flow of a border crossing between two countries in explicit style.

The Border Traffic model aims to describe a contract to which a country’s Traffic Management System (TMS) must conform. The model takes a simplified view of a 1-way road which connects two countries A and B, with a border cutting the road in two.

### BorderTrafficv2.cml

``````types

CountryId = token
ActuatorId = token

Location = int

Actuator :: aId : ActuatorId
loc : Location
disp : nat

ActuatorList = seq of Actuator

--natural number corresponding to sequence position
Corridor = seq of nat
inv Corr == len Corr = card elems Corr

functions

-- Function to calculate the distance required for the corridor based upon the
-- target speed and the current national speed limit of the country.
calcDistance : nat * nat-> nat
calcDistance(targetSpeed, speedLimit) ==
(
-- not sure if this is best way, ok for now
if targetSpeed <= speedLimit
then floor ((speedLimit-targetSpeed)/maxInterval) + 1
else 0
)
pre maxInterval > 0

-- Function to calculate the speed target the neighbouring TMS must acheive.
-- This is based upon the starting location of the corridor, the required
-- distance of the corridor, and the ultimate target speed
calcNeighbourTarget : int * nat * nat * nat -> nat
calcNeighbourTarget(startLoc, target, distance, speedLimit)  ==
(
let interval : nat = calcInterval(target, distance, speedLimit) in
(
target + (interval * abs(startLoc))
)
)
pre speedLimit > target and distance > 0

-- Function to determine the interval between actuators
calcInterval: nat * nat * nat -> nat
calcInterval(target, distance, speedLimit) ==
abs(floor((speedLimit-target)/distance))
pre speedLimit > target and distance > 0

--Function to get the first actuator from the speed corridor
getFirstAct: Corridor -> nat
getFirstAct(Corr) ==
hd Corr
pre Corr <> []

--Function to get the set of all actuators across the boundary
--need to flatten the two sequences - must be distinct
actsToSet : ActuatorList * ActuatorList -> set of Actuator
actsToSet(a1, a2) ==
getSingleActuatorSet({elems a1, elems a2})
pre elems a1 inter elems a2 = {}

getSingleActuatorSet : set of set of Actuator -> set of Actuator
getSingleActuatorSet (allacts) == dinter allacts
pre allacts <> {}

channels

--environment channels--
inIncident : CountryId * int * nat
incidentClear: CountryId * int

--interface channels--
neighbourRequest : CountryId * CountryId * nat
neighbourOk : CountryId * CountryId

--act mngr channel--
actStatus : CountryId * seq of nat

--internal corridor channels--
determineCorr : int * nat
newCorr : Corridor
createCorr : Corridor * nat
disableCorr : Corridor

chansets
-- the main interface between countryTMSs
interface = {neighbourRequest, neighbourOk}

-- interface of SoS and incident creator
incident = {inIncident,incidentClear}

--internal channels--
internal = {determineCorr, newCorr, createCorr, disableCorr}

process CountryTMS = i:CountryId, n:CountryId, sl:nat,
aCorr : ActuatorList @
begin

state
-- identifiers for the TMS and its neighbour
myId : CountryId := i
nId : CountryId := n
nationalSpeedLimit : nat := sl
-- an ordering of the actuators in the country - ordered by location
acts : ActuatorList := aCorr

-- all invariants for TMS process:
-- i) ensures the neighbour id is not its own.
-- ii) establishes a maximum difference between contiguous actuators
-- iii) no actuator is displaying a speed too high
inv myId <> nId and
forall a1, a2 in set inds acts @
(a1 + 1 = a2 => acts(a1).disp - acts(a2).disp < maxDiff) and
forall a in set elems acts @ a.disp <= nationalSpeedLimit

operations

-- Operation to determine which actuators should be present in the speed
-- corridor. Takes the stating location (i.e. where the target speed must be
-- reached) and the required distance of the corridor and returns a 'corridor'
-- of actuators which will have their displays changed.
determineSpeedCorridor : int * nat ==> Corridor
determineSpeedCorridor (startLoc, distance) ==
(
--The, intially empty, corridor
dcl corr : Corridor := [] @
(
-- for each element in the sequence of actuators
for index = 1 to len acts by 1 do
(
-- if  actuator is within the starting and end point of the required distance
if (acts(index).loc >= startLoc and acts(index).loc <= startLoc+distance)
-- add it to the corridor
then corr := corr ^ [index]
);
return corr
)
)
pre len acts > 1 -- the TMS must have actuators
post elems RESULT subset inds acts and
forall a in set elems RESULT @
(acts(a).loc >= startLoc and acts(a).loc <= distance+startLoc)

-- Given the collection of actuators provided, enact the speed corridor up to
-- a target speed as given in the operation parameters.
createSpeedCorridor : Corridor * nat ==> ()
createSpeedCorridor (pCorr, target) ==
(
if target < nationalSpeedLimit then
(
dcl newDisp : nat := target, interval : nat, corrDistance : nat @
(
-- determine the speed difference between actuators
-- needs to be +1 to enable smoother transition
corrDistance := abs(acts(pCorr(1)).loc - acts(pCorr(len pCorr)).loc) + 1;
interval := floor((nationalSpeedLimit - target)/corrDistance);

-- for each actuator in the sequence, change the display value
for index = (len pCorr) to 1  by -1 do
(
acts(pCorr(index)) := mk_Actuator(acts(pCorr(index)).aId, acts(pCorr(index)).loc, newDisp);
newDisp := newDisp + interval
)
)
)
)
pre elems pCorr subset inds acts and
(len pCorr > 0 => target < nationalSpeedLimit)
post elems pCorr subset inds acts and
forall a1, a2 in set elems pCorr @ (a1 <> a2 =>
(acts(a1).loc > acts(a2).loc => acts(a1).disp >= acts(a2).disp))

-- Given the speed corridor provided, remove the speed limits and re-enact the
-- country's national speed limit on all actuator displays.
disableSpeedCorridor : Corridor ==> ()
disableSpeedCorridor(pCorr) ==
(
-- for each actuator in the sequence, change the display value
for index = 1 to (len pCorr) by 1 do
(
acts(pCorr(index)) := mk_Actuator(acts(pCorr(index)).aId, acts(pCorr(index)).loc, nationalSpeedLimit)
)
)
pre elems pCorr subset inds acts
post elems pCorr subset inds acts and
forall a in set elems pCorr @ acts(a).disp = nationalSpeedLimit
--a should not be in any other corridors!

-- Determines if Neighbour is needed based upon the starting location and
-- distance of the speed corridor. **IMPORTANT** current model of location
-- means this is only valid for Country B!
isNeighbourNeeded : int * nat ==> bool
isNeighbourNeeded(startLoc, distance) ==
(
return  not (exists ha in set elems acts @ ha.loc > (startLoc + distance))
)
-- post RESULT = not (exists act in set elems acts @ act.loc >= (startLoc + distance))

--Operation to output the current speeds as shown on actuators.
outputActs: () ==> seq of nat
outputActs() ==
(
--The, intially empty, set of values
dcl v : seq of nat := [] @
(
-- for each element in the sequence of actuators
for index = 1 to len acts by 1 do
(
v := v ^ [acts(index).disp]
);
return v
)
)
post RESULT = [acts(a).disp | a in set inds acts]

actions

BEHAVIOUR = NEW_INCIDENT [] NEIGHBOUR_REQ

NEW_INCIDENT = inIncident.myId?l?t ->
(dcl d : nat := calcDistance(t, nationalSpeedLimit) @
NEW_CORRIDOR(l, t, d))

NEW_CORRIDOR = l : int, t: nat, d:nat @ ACT_STATUS;
(dcl c: Corridor := determineSpeedCorridor(l, d) @
(newCorr.c -> createSpeedCorridor(c, t); ACT_STATUS;
(dcl neighbourNeeded : bool := isNeighbourNeeded(l, d) @
([neighbourNeeded]     & (dcl ntarg:nat := calcNeighbourTarget(l, t, d, nationalSpeedLimit) @
neighbourRequest!myId!nId!ntarg -> CLEAR_INCIDENT(l, c,true))
[]
[not neighbourNeeded] & CLEAR_INCIDENT(l, c, false)))))

CLEAR_INCIDENT = l:int, c:Corridor, neigh:bool @
(incidentClear.myId.l ->  CLEAR_CORRIDOR(c, neigh))

CLEAR_CORRIDOR = c:Corridor,neigh:bool @
[neigh]& disableCorr.c -> disableSpeedCorridor(c); neighbourOk!myId!nId -> ACT_STATUS; NEW_INCIDENT
[]
[not neigh] & disableCorr.c -> disableSpeedCorridor(c); ACT_STATUS;  BEHAVIOUR

NEIGHBOUR_REQ = neighbourRequest.nId.myId?t ->
(dcl d : nat := calcDistance(t, nationalSpeedLimit) @
(dcl c: Corridor := determineSpeedCorridor(0, d) @
ACT_STATUS; newCorr.c -> createSpeedCorridor(c, t); ACT_STATUS;  NEIGHBOUR_CLEAR(c)))

NEIGHBOUR_CLEAR = c:Corridor @
(neighbourOk.nId.myId -> ACT_STATUS; disableCorr.c -> disableSpeedCorridor(c); ACT_STATUS; BEHAVIOUR)

ACT_STATUS = (dcl s : seq of nat := outputActs() @  actStatus.myId!s -> Skip)

@ BEHAVIOUR
end

process CountryA = CountryTMS(theAId, theBId, limitA, actCorrA)
process CountryB = CountryTMS(theBId, theAId, limitB, actCorrB)

process BorderTrafficSoS = CountryA [|interface|] CountryB --\\ internal

process Scenario =
begin
@ inIncident!theBId!(-4)!20 -> incidentClear.theBId.(-4)-> inIncident.theBId.(-1).20 -> incidentClear.theBId.(-1) -> Skip
end

process Test = Scenario [|incident|] BorderTrafficSoS

-- Values are used in the scenarios
values

maxDiff : nat = 20
maxChange : nat = 40

theAId : CountryId = mk_token("Country A")
theBId :CountryId = mk_token("Country B")

limitA : nat = 100
limitB : nat = 90

aIdA1 : ActuatorId = mk_token("aIdA1")
aIdA2 : ActuatorId = mk_token("aIdA2")
aIdA3 : ActuatorId = mk_token("aIdA3")
aIdA4 : ActuatorId = mk_token("aIdA4")

aIdB1 : ActuatorId = mk_token("aIdB1")
aIdB2 : ActuatorId = mk_token("aIdB2")
aIdB3 : ActuatorId = mk_token("aIdB3")
aIdB4 : ActuatorId = mk_token("aIdB4")

actA1 : Actuator = mk_Actuator(aIdA1, 4, limitA)
actA2 : Actuator = mk_Actuator(aIdA2, 3, limitA)
actA3 : Actuator = mk_Actuator(aIdA3, 2, limitA)
actA4 : Actuator = mk_Actuator(aIdA4, 1, limitA)

actB1 : Actuator = mk_Actuator(aIdB1, -1, limitB)
actB2 : Actuator = mk_Actuator(aIdB2, -2, limitB)
actB3 : Actuator = mk_Actuator(aIdB3, -3, limitB)
actB4 : Actuator = mk_Actuator(aIdB4, -4, limitB)

actCorrA : ActuatorList = [actA1, actA2, actA3, actA4]
actCorrB : ActuatorList = [actB1, actB2, actB3, actB4]

restrictionSpeed : nat = 20
blockageSpeed : nat = 5

maxInterval : nat = 40
``````