The Symphony IDE

Formal Modelling for Systems of Systems

Go to our GitHub Profile

BorderTrafficImplicitV2

Author:

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

BorderTrafficImplv2_TP.cml

types

  CountryId = token
  ActuatorId = token

  Location = int

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

  --natural number corresponding to sequence position
  Corridor = seq of nat

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) ==
   (
      if targetSpeed <= speedLimit
      then floor ((speedLimit-targetSpeed)/maxInterval) + 1 -- not sure if this is best way, ok for now
      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
   post RESULT > target

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


channels

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

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

  --act mngr channels--
  actStatus : seq of nat 
  determineCorr : int * nat
  newCorr : Corridor
  createCorr : Corridor * nat
  disableCorr : Corridor

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


process CountryTMS =  i:CountryId, n:CountryId, sl:nat,  
                     aCorr : seq of Actuator @
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 : seq of Actuator := aCorr

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

 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 (startLoc: int, distance:nat) resc: Corridor
   pre len acts > 1 -- the TMS must have actuators
   post elems resc subset inds acts and 
        forall a in set elems resc @ 
          (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 (pCorr: Corridor , target: nat) 
   pre elems pCorr subset inds acts and
       (len pCorr > 0 => target < nationalSpeedLimit)
   post 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 (pCorr: Corridor)
   pre elems pCorr subset inds acts
   post 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 (startLoc : int, distance : nat) b: bool
   post b = not (exists act in set elems acts @ act.loc >= (startLoc + distance)) -- Only valid for Country B!


   --Operation to state current speeds shown on actuators
   outputActs() displ: seq of nat
   post displ = [acts(a).disp | a in set inds acts] 

@Skip
end 


values

  maxDiff : nat = 20
  maxChange : nat = 40

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

  limitA : nat = 100

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

  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)

  actCorrA : seq of Actuator = [actA1, actA2, actA3, actA4]

  restrictionSpeed : nat = 20
  blockageSpeed : nat = 5

  maxInterval : nat = 40