abstract
State
abstract
StateMachine
abstract
TrafficLight_1
final
xor
TLStates_1
:
StateMachine
initial
xor
on
:
State
-->>
off
initial
xor
normal
:
State
-->>
flashing
initial
green
:
State
-->
yellow
yellow
:
State
-->
red
red
:
State
-->
green
xor
flashing
:
State
-->>
normal
initial
yellow_on
:
State
-->
yellow_off
yellow_off
:
State
-->
yellow_on
off
:
State
-->>
on
t1
:
TrafficLight_1
assert [
always
t1
.
TLStates_1
.
on
-->>
t1
.
TLStates_1
.
on
.
flashing
]
//assert [ always t1.TLStates_1.on -->> t1.TLStates_1.flashing -->> t1.TLStates_1.yellow_on -->> t1.TLStates_1.yellow_off -->> t1.TLStates_1.yellow_on]
assert [
always
t1
.
TLStates_1
.
on
.
flashing
-->>
t1
.
TLStates_1
.
on
.
flashing
.
yellow_on
]
assert [
always
t1
.
TLStates_1
.
on
.
flashing
.
yellow_on
-->>
t1
.
TLStates_1
.
on
.
flashing
.
yellow_off
]
assert [
always
t1
.
TLStates_1
.
on
.
flashing
.
yellow_off
-->>
t1
.
TLStates_1
.
on
.
flashing
.
yellow_on
]
t2
:
TrafficLight_1
[
on
-->
flashing
-->
yellow_on
-->
yellow_off
-->
yellow_on
]
t3
:
TrafficLight_1
assert [
always
t3
.
TLStates_1
.
on
-->>
t3
.
TLStates_1
.
on
.
flashing
.
yellow_off
]
assert [
always
t3
.
TLStates_1
.
on
.
flashing
.
yellow_off
-->>
t3
.
TLStates_1
.
on
.
flashing
.
yellow_on
]
assert [
always
t3
.
TLStates_1
.
on
.
flashing
.
yellow_on
-->>
t3
.
TLStates_1
.
on
.
flashing
.
yellow_off
]