|# 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

|:: activate driver assist|
    :state: active

|:: gather data from sensors|
    :sensors: blind
    :brakes: broken

|:expected state: $x :state: $x?|
    :passed:
|:expected state: $x $y :state: $x $y?|
    :passed:
|:expected state: $x|
    :failed:
    :expected: $x

||:: activate driver assist
  :: gather data from sensors
  :expected state: off