driver-assist.nv
· 1.2 KiB · Text
Исходник
Playground
|# Model based off of https://beza1e1.tuxen.de/tla-plus.html #|
|# Driving Assist #|
:author: "June Gardner"
|:state: off :seatbelt: unknown| :state: fault
|:state: off :sensors: broken | :state: fault
|:state: off :brakes: broken | :state: fault
|:state: off :seatbelt: off | :state: temporary fault
|:state: off :sensors: blind| :state: temporary fault
|:state: off | :state: active
|:state: active :seatbelt: off | :state: temporary fault
|:state: active :sensors: blind | :state: temporary fault
|:state: active :seatbelt: unknown| :state: fault
|:state: active :seatbelt: broken | :state: fault
|:state: temporary fault :seatbelt: on :sensors: ok :brakes: ok|
:state: active
|:state: temporary fault :seatbelt: unknown| :state: fault
|:state: temporary fault :sensors: broken | :state: fault
|:state: temporary fault :brakes: broken | :state: fault
|:state: fault| :state: off
|:expected state: $x :state: $x?|
:passed:
|:expected state: $x $y :state: $x $y?|
:passed:
|:expected state: $x|
:failed:
:expected: $x
|:: activate driver assist|
:state: active
|:: gather data from sensors|
:sensors: blind
:brakes: broken
||:: activate driver assist
:: gather data from sensors
:expected state: off
| 1 | |# Model based off of https://beza1e1.tuxen.de/tla-plus.html #| |
| 2 | |# Driving Assist #| |
| 3 | :author: "June Gardner" |
| 4 | |
| 5 | |:state: off :seatbelt: unknown| :state: fault |
| 6 | |:state: off :sensors: broken | :state: fault |
| 7 | |:state: off :brakes: broken | :state: fault |
| 8 | |
| 9 | |:state: off :seatbelt: off | :state: temporary fault |
| 10 | |:state: off :sensors: blind| :state: temporary fault |
| 11 | |:state: off | :state: active |
| 12 | |
| 13 | |:state: active :seatbelt: off | :state: temporary fault |
| 14 | |:state: active :sensors: blind | :state: temporary fault |
| 15 | |:state: active :seatbelt: unknown| :state: fault |
| 16 | |:state: active :seatbelt: broken | :state: fault |
| 17 | |
| 18 | |:state: temporary fault :seatbelt: on :sensors: ok :brakes: ok| |
| 19 | :state: active |
| 20 | |:state: temporary fault :seatbelt: unknown| :state: fault |
| 21 | |:state: temporary fault :sensors: broken | :state: fault |
| 22 | |:state: temporary fault :brakes: broken | :state: fault |
| 23 | |
| 24 | |:state: fault| :state: off |
| 25 | |
| 26 | |:expected state: $x :state: $x?| |
| 27 | :passed: |
| 28 | |:expected state: $x $y :state: $x $y?| |
| 29 | :passed: |
| 30 | |:expected state: $x| |
| 31 | :failed: |
| 32 | :expected: $x |
| 33 | |
| 34 | |:: activate driver assist| |
| 35 | :state: active |
| 36 | |
| 37 | |:: gather data from sensors| |
| 38 | :sensors: blind |
| 39 | :brakes: broken |
| 40 | |
| 41 | ||:: activate driver assist |
| 42 | :: gather data from sensors |
| 43 | :expected state: off |
| 44 |