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

|:: the system should be in the $x state :state: $x|
    :passed:
|:: the system should be in the $x $y state :state: $x $y|
    :passed:
|:: the system should be in the $x state|
    :failed:
    :expected: $x
|:: the system should be in the $x $y state|
    :failed:
    :expected: $x $y
|:: the system should be $x|
    :: the system should be in the $x state

||:: activate driver assist
  :: gather data from sensors
  :: the system should be off