Syntax and Static Semantics

• A TrafficLight model consists of a number of states. Each state has a unique name (a string), and exactly one of them is the start state. There is no explicit end state.
• States may be connected by zero or more transitions.
• There are two types of transitions:
  • Timed transitions are labelled with an integer number, which represents the time delay after which the transition will "fire".
  • An interrupt transition is labelled with the name of an interrupt (a string).
  • A maximum of one outgoing timed transition is allowed for each state.
  • Each interrupt name of interrupt transitions going out of a single state need to be distinct.
• Associated with each state is a description of the visualization of the traffic light when it is in that state. The description specifies, for each of the three coloured lights (Red, Green, Yellow) in a traffic light, whether it is on or off. A state named "red" for example may have the visualization {Red=on, Green=off, Yellow=off} associated with it.
• Multiple states may refer to the same visualization.
• The interrupt-producing environment in which the traffic light will operate needs to be modelled too. This is done by means of a time-ordered interrupt list. The interrupt list consists of linearly connected interrupt notices. An interrupt notice has a non-negative integer absolute time (milliseconds) timestamp as well as the name of the interrupt (a string).
• For simulation purposes only, a (singleton) global time entity holding a non-negative integer absolute time (milliseconds) value is needed. This value should be initialized to 0 and will only be updated (increased) by the simulator (operational semantics).
• Also for simulation purposes, a current state will refer to the state the model is in at any given time.

Dynamic Semantics

• First, the global time is initialized to 0. Then, the current state is made to refer to the start state of the model.
• The simulation specified below continues until no more state transitions are possible.
• A state transition T from the current state C to a new state (possibly the same) N occurs if:
  • there is a timed state transition T from the current state C to a new state (possibly the same) N, this transition will be taken if the global time + the time delay of the transition is strictly smaller than the time of the earliest interrupt notice in the external interrupt list. The effects of this state transition are:
    1. The global time is updated to the global time + the time delay of the transition.
    2. During non-visual simulation, the global time, interrupt name, old current state C and new current state N are printed (forming a simulation trace); during visual simulation, the effect will be visible on the model.
    The current state is updated to state N.
  • there is an interrupt transition from the current state C for which the interrupt name is equal to the interrupt name in the earliest interrupt notice in the external interrupt list. The effects of this state transition are:
    1. The global time is updated to the time in the interrupt notice.
    2. During non-visual simulation, the global time, interrupt name, old current state C and new current state N are printed (forming a simulation trace); during visual simulation, the effect will be visible on the model.
    3. The current state is updated to state N.
    4. The interrupt notice is removed from the interrupt list.

TrafficLight.mdepth and TrafficLightSim.eol

Download TrafficLight.zip and unzip into your Formalisms folder.

Download operationalSemantics.zip and unzip into your the TrafficLight/Operational/ folder.