Example: Synthesis Decision Model Example

The Example presented below illustrates a portion of a Decision Model for the TLC domain, which presents decision groups (e.g., Street, Lane-Group) and their corresponding decisions, along with appropriate constraints.

Traffic_Light_Controller: composed of example of Decision Specification

Schedule: one of (Fixed_Schedule, Programmable) {designates the type of traffic light sequence scheduling the TLC system must accommodate}

Geometry: one of {intersection geometry}

X: List length 4 of Street

Y: list length 3 of Street

Fixed_Schedule: composed of example of Decision Specification

Start_Time: (0:00 .. 23:59) { start time for this traffic light sequence schedule}

Stop_Time: (0:00 .. 23:59) { stop time for this traffic light sequence schedule}

…

Street: composed of example of Decision group

Name:identifier {street name}

Right_Turn_Lanes: Lane_Group {characteristics for the right-hand turn lanes}

Left_Turn_Lanes: Lane_Group {characteristics for the left-hand turn lanes}

Through_Lanes: Lane_Group {characteristics for the through lanes}

Pedestrian_Crosswall: one of (Xwalk,No_Xwalk) {designates the presence of pedestrian crosswalk

for this Lane_Group}

Cross_Button: one of (CB,No_CB) {designates the presence of pedestrian crosswalk

pushbutton for this Lane_Group}

….

Lane_Group: compose of example of Decision group

Number_of_Lanes: numeric(1..2) {number of traffic lanes in this Lane_Group}

Sensor: one of (Sensor, No_Sensor) {indicates whether there is a traffic monitoring

device for each lane in this Lane_group}

Constraints example of Decision constraint

- The number of through lanes for Street(1) must be the same as for Street(3)

- There can be at most 4 different schedules in the Fixed_Schedule

- A Through_Lanes group must be specified for each Street