driver-assist.nv
| @@ -30,14 +30,19 @@ | |||
| 30 | 30 | :sensors: blind | |
| 31 | 31 | :brakes: broken | |
| 32 | 32 | ||
| 33 | - | |:expected state: $x :state: $x?| | |
| 33 | + | |:: the system should be in the $x state :state: $x| | |
| 34 | 34 | :passed: | |
| 35 | - | |:expected state: $x $y :state: $x $y?| | |
| 35 | + | |:: the system should be in the $x $y state :state: $x $y| | |
| 36 | 36 | :passed: | |
| 37 | - | |:expected state: $x| | |
| 37 | + | |:: the system should be in the $x state| | |
| 38 | 38 | :failed: | |
| 39 | 39 | :expected: $x | |
| 40 | + | |:: the system should be in the $x $y state| | |
| 41 | + | :failed: | |
| 42 | + | :expected: $x $y | |
| 43 | + | |:: the system should be $x| | |
| 44 | + | :: the system should be in the $x state | |
| 40 | 45 | ||
| 41 | 46 | ||:: activate driver assist | |
| 42 | 47 | :: gather data from sensors | |
| 43 | - | :expected state: off | |
| 48 | + | :: the system should be off | |
driver-assist.nv
| @@ -23,6 +23,13 @@ | |||
| 23 | 23 | ||
| 24 | 24 | |:state: fault| :state: off | |
| 25 | 25 | ||
| 26 | + | |:: activate driver assist| | |
| 27 | + | :state: active | |
| 28 | + | ||
| 29 | + | |:: gather data from sensors| | |
| 30 | + | :sensors: blind | |
| 31 | + | :brakes: broken | |
| 32 | + | ||
| 26 | 33 | |:expected state: $x :state: $x?| | |
| 27 | 34 | :passed: | |
| 28 | 35 | |:expected state: $x $y :state: $x $y?| | |
| @@ -31,13 +38,6 @@ | |||
| 31 | 38 | :failed: | |
| 32 | 39 | :expected: $x | |
| 33 | 40 | ||
| 34 | - | |:: activate driver assist| | |
| 35 | - | :state: active | |
| 36 | - | ||
| 37 | - | |:: gather data from sensors| | |
| 38 | - | :sensors: blind | |
| 39 | - | :brakes: broken | |
| 40 | - | ||
| 41 | 41 | ||:: activate driver assist | |
| 42 | 42 | :: gather data from sensors | |
| 43 | 43 | :expected state: off | |
driver-assist.nv
| @@ -40,4 +40,4 @@ | |||
| 40 | 40 | ||
| 41 | 41 | ||:: activate driver assist | |
| 42 | 42 | :: gather data from sensors | |
| 43 | - | :expected state: fault | |
| 43 | + | :expected state: off | |
driver-assist.nv(файл создан)
| @@ -0,0 +1,43 @@ | |||
| 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: fault | |
Новее
Позже