-- changed to run on SMV 2.5.3...  PEB 18 Nov 1998.  Stuff like
--	next(Enum1=Activate)
-- changed to
--	next(Enum1)=Activate
MODULE main
VAR
    Ignited   : boolean;
    EngRun   : boolean;
    Toofast   : boolean;
    Brake   : boolean;
    Enum1   : { Activate, Deactivate, Resume };
    CruiseControl   : { Off, Inactive, Cruise, Override, QC-CruiseControl-NULL };
    PBrake   : boolean;
    PToofast   : boolean;
    PEngRun   : boolean;
    PEnum1   : { Activate, Deactivate, Resume };
    PIgnited   : boolean;


INIT
(  ( !(Ignited) )  )
INIT
  Toofast -> (EngRun) 

INIT
  EngRun -> (Ignited) 


ASSIGN
init(CruiseControl) := case
    !(Ignited) : Off;
    1 : QC-CruiseControl-NULL;
esac;

next(CruiseControl) := case
-- line 1
    CruiseControl=Off  & !Ignited & next(Ignited) : Inactive;
-- line 2
    CruiseControl=Inactive  & Ignited & !next(Ignited) : Off;
-- line 3
    CruiseControl=Inactive  & EngRun & !Toofast & !Brake & !(Enum1=Activate) & next(Enum1)=Activate : Cruise;
-- line 4
    CruiseControl=Cruise  & Ignited & !next(Ignited) : Off;
-- line 5
    CruiseControl=Cruise  & Ignited & EngRun & !next(EngRun) : Inactive;
    CruiseControl=Cruise  & Ignited & !Toofast & next(Toofast) : Inactive;
    CruiseControl=Cruise  & Ignited & EngRun & !Toofast & !Brake & next(Brake) : Override;
    CruiseControl=Cruise  & Ignited & EngRun & !Toofast & !(Enum1=Deactivate) & next(Enum1)=Deactivate : Override;
    CruiseControl=Override  & Ignited & !next(Ignited) : Off;
    CruiseControl=Override  & Ignited & EngRun & !next(EngRun) : Inactive;
    CruiseControl=Override  & Ignited & EngRun & !Toofast & !Brake & !(Enum1=Activate) & next(Enum1)=Activate : Cruise;
    CruiseControl=Override  & Ignited & EngRun & !Toofast & !Brake & !(Enum1=Resume) & next(Enum1)=Resume : Cruise;
    1 : CruiseControl;
esac;

init(PBrake) := Brake; next(PBrake) := Brake;
init(PToofast) := Toofast; next(PToofast) := Toofast;
init(PEngRun) := EngRun; next(PEngRun) := EngRun;
init(PEnum1) := Enum1; next(PEnum1) := Enum1;
init(PIgnited) := Ignited; next(PIgnited) := Ignited;


TRANS
  Toofast -> (EngRun) 

TRANS
  ( (!EngRun & next(EngRun) & !Toofast & next(Toofast)) |
    (EngRun & !next(EngRun) & Toofast & !next(Toofast)) |
    (!EngRun & next(EngRun) & !Toofast & !next(Toofast)) |
    (EngRun & !next(EngRun) & !Toofast & !next(Toofast)) |
    (EngRun & next(EngRun) & Toofast & !next(Toofast)) |
    (EngRun & next(EngRun) & !Toofast & next(Toofast)) |
    (Toofast=next(Toofast)) & (EngRun=next(EngRun))
  )

TRANS
  EngRun -> (Ignited) 

TRANS
  ( (!Ignited & next(Ignited) & !EngRun & next(EngRun)) |
    (Ignited & !next(Ignited) & EngRun & !next(EngRun)) |
    (!Ignited & next(Ignited) & !EngRun & !next(EngRun)) |
    (Ignited & !next(Ignited) & !EngRun & !next(EngRun)) |
    (Ignited & next(Ignited) & EngRun & !next(EngRun)) |
    (Ignited & next(Ignited) & !EngRun & next(EngRun)) |
    (EngRun=next(EngRun)) & (Ignited=next(Ignited))
  )

TRANS
  (!(Toofast=next(Toofast)) & !(EngRun=next(EngRun)) & !(Ignited=next(Ignited)) & (Enum1=next(Enum1)) & (Brake=next(Brake))) | 
  (!(Toofast=next(Toofast)) & !(EngRun=next(EngRun)) & (Enum1=next(Enum1)) & (Brake=next(Brake)) & (Ignited=next(Ignited))) | 
  (!(EngRun=next(EngRun)) & !(Ignited=next(Ignited)) & (Enum1=next(Enum1)) & (Brake=next(Brake)) & (Toofast=next(Toofast))) | 
  (!(EngRun=next(EngRun)) & (Enum1=next(Enum1)) & (Brake=next(Brake)) & (Toofast=next(Toofast)) & (Ignited=next(Ignited))) | 
  (!(Ignited=next(Ignited)) & (Enum1=next(Enum1)) & (Brake=next(Brake)) & (Toofast=next(Toofast)) & (EngRun=next(EngRun))) | 
  (!(Toofast=next(Toofast)) & (Enum1=next(Enum1)) & (Brake=next(Brake)) & (EngRun=next(EngRun)) & (Ignited=next(Ignited))) | 
  (!(Enum1=next(Enum1)) & (Brake=next(Brake)) & (Toofast=next(Toofast)) & (EngRun=next(EngRun)) & (Ignited=next(Ignited))) | 
  (!(Brake=next(Brake)) & (Enum1=next(Enum1)) & (Ignited=next(Ignited)) & (EngRun=next(EngRun)) & (Toofast=next(Toofast)))


-- line 1
SPEC AG (CruiseControl = QC-CruiseControl-NULL -> AX (!PIgnited & Ignited -> CruiseControl = Inactive))
SPEC AG (CruiseControl = Override -> AX (!PIgnited & Ignited -> CruiseControl = Inactive))
SPEC AG (CruiseControl = Cruise -> AX (!PIgnited & Ignited -> CruiseControl = Inactive))
SPEC AG (CruiseControl = Inactive -> AX (!PIgnited & Ignited -> CruiseControl = Inactive))
SPEC AG (CruiseControl = Off -> AX (!PIgnited & Ignited -> CruiseControl = QC-CruiseControl-NULL))
SPEC AG (CruiseControl = Off -> AX (!PIgnited & Ignited -> CruiseControl = Override))
SPEC AG (CruiseControl = Off -> AX (!PIgnited & Ignited -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Off -> AX (!PIgnited & Ignited -> CruiseControl = Off))
SPEC AG (CruiseControl = QC-CruiseControl-NULL -> AX (PIgnited & !Ignited -> CruiseControl = Off))
SPEC AG (CruiseControl = Override -> AX (PIgnited & !Ignited -> CruiseControl = Off))
SPEC AG (CruiseControl = Cruise -> AX (PIgnited & !Ignited -> CruiseControl = Off))
SPEC AG (CruiseControl = Off -> AX (PIgnited & !Ignited -> CruiseControl = Off))
SPEC AG (CruiseControl = Inactive -> AX (PIgnited & !Ignited -> CruiseControl = QC-CruiseControl-NULL))
SPEC AG (CruiseControl = Inactive -> AX (PIgnited & !Ignited -> CruiseControl = Override))
SPEC AG (CruiseControl = Inactive -> AX (PIgnited & !Ignited -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Inactive -> AX (PIgnited & !Ignited -> CruiseControl = Inactive))
SPEC AG (CruiseControl = QC-CruiseControl-NULL -> AX (!PEnum1 = Activate & Enum1 = Activate & (PIgnited & PEngRun & !PToofast & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Override -> AX (!PEnum1 = Activate & Enum1 = Activate & (PIgnited & PEngRun & !PToofast & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Cruise -> AX (!PEnum1 = Activate & Enum1 = Activate & (PIgnited & PEngRun & !PToofast & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Off -> AX (!PEnum1 = Activate & Enum1 = Activate & (PIgnited & PEngRun & !PToofast & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Inactive -> AX (!PEnum1 = Resume & Enum1 = Activate & (PIgnited & PEngRun & !PToofast & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Inactive -> AX (!PEnum1 = Deactivate & Enum1 = Activate & (PIgnited & PEngRun & !PToofast & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Inactive -> AX (!PEnum1 = Enum1 & Enum1 = Activate & (PIgnited & PEngRun & !PToofast & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Inactive -> AX (!PEnum1 = Activate & Enum1 = Resume & (PIgnited & PEngRun & !PToofast & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Inactive -> AX (!PEnum1 = Activate & Enum1 = Deactivate & (PIgnited & PEngRun & !PToofast & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Inactive -> AX (!PEnum1 = Activate & Enum1 = PEnum1 & (PIgnited & PEngRun & !PToofast & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Inactive -> AX (!PEnum1 = Activate & Enum1 = Activate & (PIgnited & PEngRun & !PToofast & !PBrake) -> CruiseControl = QC-CruiseControl-NULL))
SPEC AG (CruiseControl = Inactive -> AX (!PEnum1 = Activate & Enum1 = Activate & (PIgnited & PEngRun & !PToofast & !PBrake) -> CruiseControl = Override))
SPEC AG (CruiseControl = Inactive -> AX (!PEnum1 = Activate & Enum1 = Activate & (PIgnited & PEngRun & !PToofast & !PBrake) -> CruiseControl = Inactive))
SPEC AG (CruiseControl = Inactive -> AX (!PEnum1 = Activate & Enum1 = Activate & (PIgnited & PEngRun & !PToofast & !PBrake) -> CruiseControl = Off))
SPEC AG (CruiseControl = QC-CruiseControl-NULL -> AX (PIgnited & !Ignited -> CruiseControl = Off))
SPEC AG (CruiseControl = Override -> AX (PIgnited & !Ignited -> CruiseControl = Off))
SPEC AG (CruiseControl = Inactive -> AX (PIgnited & !Ignited -> CruiseControl = Off))
SPEC AG (CruiseControl = Off -> AX (PIgnited & !Ignited -> CruiseControl = Off))
SPEC AG (CruiseControl = Cruise -> AX (PIgnited & !Ignited -> CruiseControl = QC-CruiseControl-NULL))
SPEC AG (CruiseControl = Cruise -> AX (PIgnited & !Ignited -> CruiseControl = Override))
SPEC AG (CruiseControl = Cruise -> AX (PIgnited & !Ignited -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Cruise -> AX (PIgnited & !Ignited -> CruiseControl = Inactive))
SPEC AG (CruiseControl = QC-CruiseControl-NULL -> AX (!PToofast & Toofast & PIgnited -> CruiseControl = Inactive))
SPEC AG (CruiseControl = Override -> AX (!PToofast & Toofast & PIgnited -> CruiseControl = Inactive))
SPEC AG (CruiseControl = Inactive -> AX (!PToofast & Toofast & PIgnited -> CruiseControl = Inactive))
SPEC AG (CruiseControl = Off -> AX (!PToofast & Toofast & PIgnited -> CruiseControl = Inactive))
SPEC AG (CruiseControl = Cruise -> AX (!PToofast & Toofast & PIgnited -> CruiseControl = QC-CruiseControl-NULL))
SPEC AG (CruiseControl = Cruise -> AX (!PToofast & Toofast & PIgnited -> CruiseControl = Override))
SPEC AG (CruiseControl = Cruise -> AX (!PToofast & Toofast & PIgnited -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Cruise -> AX (!PToofast & Toofast & PIgnited -> CruiseControl = Off))
SPEC AG (CruiseControl = QC-CruiseControl-NULL -> AX (!PBrake & Brake & (PIgnited & PEngRun & !PToofast) -> CruiseControl = Override))
SPEC AG (CruiseControl = Override -> AX (!PBrake & Brake & (PIgnited & PEngRun & !PToofast) -> CruiseControl = Override))
SPEC AG (CruiseControl = Inactive -> AX (!PBrake & Brake & (PIgnited & PEngRun & !PToofast) -> CruiseControl = Override))
SPEC AG (CruiseControl = Off -> AX (!PBrake & Brake & (PIgnited & PEngRun & !PToofast) -> CruiseControl = Override))
SPEC AG (CruiseControl = Cruise -> AX (!PBrake & Brake & (PIgnited & PEngRun & !PToofast) -> CruiseControl = QC-CruiseControl-NULL))
SPEC AG (CruiseControl = Cruise -> AX (!PBrake & Brake & (PIgnited & PEngRun & !PToofast) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Cruise -> AX (!PBrake & Brake & (PIgnited & PEngRun & !PToofast) -> CruiseControl = Inactive))
SPEC AG (CruiseControl = Cruise -> AX (!PBrake & Brake & (PIgnited & PEngRun & !PToofast) -> CruiseControl = Off))
SPEC AG (CruiseControl = QC-CruiseControl-NULL -> AX (!PEnum1 = Deactivate & Enum1 = Deactivate & (PIgnited & PEngRun & !PToofast) -> CruiseControl = Override))
SPEC AG (CruiseControl = Override -> AX (!PEnum1 = Deactivate & Enum1 = Deactivate & (PIgnited & PEngRun & !PToofast) -> CruiseControl = Override))
SPEC AG (CruiseControl = Inactive -> AX (!PEnum1 = Deactivate & Enum1 = Deactivate & (PIgnited & PEngRun & !PToofast) -> CruiseControl = Override))
SPEC AG (CruiseControl = Off -> AX (!PEnum1 = Deactivate & Enum1 = Deactivate & (PIgnited & PEngRun & !PToofast) -> CruiseControl = Override))
SPEC AG (CruiseControl = Cruise -> AX (!PEnum1 = Resume & Enum1 = Deactivate & (PIgnited & PEngRun & !PToofast) -> CruiseControl = Override))
SPEC AG (CruiseControl = Cruise -> AX (!PEnum1 = Activate & Enum1 = Deactivate & (PIgnited & PEngRun & !PToofast) -> CruiseControl = Override))
SPEC AG (CruiseControl = Cruise -> AX (!PEnum1 = Enum1 & Enum1 = Deactivate & (PIgnited & PEngRun & !PToofast) -> CruiseControl = Override))
SPEC AG (CruiseControl = Cruise -> AX (!PEnum1 = Deactivate & Enum1 = Resume & (PIgnited & PEngRun & !PToofast) -> CruiseControl = Override))
SPEC AG (CruiseControl = Cruise -> AX (!PEnum1 = Deactivate & Enum1 = Activate & (PIgnited & PEngRun & !PToofast) -> CruiseControl = Override))
SPEC AG (CruiseControl = Cruise -> AX (!PEnum1 = Deactivate & Enum1 = PEnum1 & (PIgnited & PEngRun & !PToofast) -> CruiseControl = Override))
SPEC AG (CruiseControl = Cruise -> AX (!PEnum1 = Deactivate & Enum1 = Deactivate & (PIgnited & PEngRun & !PToofast) -> CruiseControl = QC-CruiseControl-NULL))
SPEC AG (CruiseControl = Cruise -> AX (!PEnum1 = Deactivate & Enum1 = Deactivate & (PIgnited & PEngRun & !PToofast) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Cruise -> AX (!PEnum1 = Deactivate & Enum1 = Deactivate & (PIgnited & PEngRun & !PToofast) -> CruiseControl = Inactive))
SPEC AG (CruiseControl = Cruise -> AX (!PEnum1 = Deactivate & Enum1 = Deactivate & (PIgnited & PEngRun & !PToofast) -> CruiseControl = Off))
SPEC AG (CruiseControl = QC-CruiseControl-NULL -> AX (PIgnited & !Ignited -> CruiseControl = Off))
SPEC AG (CruiseControl = Cruise -> AX (PIgnited & !Ignited -> CruiseControl = Off))
SPEC AG (CruiseControl = Inactive -> AX (PIgnited & !Ignited -> CruiseControl = Off))
SPEC AG (CruiseControl = Off -> AX (PIgnited & !Ignited -> CruiseControl = Off))
SPEC AG (CruiseControl = Override -> AX (PIgnited & !Ignited -> CruiseControl = QC-CruiseControl-NULL))
SPEC AG (CruiseControl = Override -> AX (PIgnited & !Ignited -> CruiseControl = Override))
SPEC AG (CruiseControl = Override -> AX (PIgnited & !Ignited -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Override -> AX (PIgnited & !Ignited -> CruiseControl = Inactive))
SPEC AG (CruiseControl = QC-CruiseControl-NULL -> AX (!PEnum1 = Activate & Enum1 = Activate & (PIgnited & PEngRun & !PToofast & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Cruise -> AX (!PEnum1 = Activate & Enum1 = Activate & (PIgnited & PEngRun & !PToofast & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Inactive -> AX (!PEnum1 = Activate & Enum1 = Activate & (PIgnited & PEngRun & !PToofast & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Off -> AX (!PEnum1 = Activate & Enum1 = Activate & (PIgnited & PEngRun & !PToofast & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Override -> AX (!PEnum1 = Resume & Enum1 = Activate & (PIgnited & PEngRun & !PToofast & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Override -> AX (!PEnum1 = Deactivate & Enum1 = Activate & (PIgnited & PEngRun & !PToofast & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Override -> AX (!PEnum1 = Enum1 & Enum1 = Activate & (PIgnited & PEngRun & !PToofast & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Override -> AX (!PEnum1 = Activate & Enum1 = Resume & (PIgnited & PEngRun & !PToofast & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Override -> AX (!PEnum1 = Activate & Enum1 = Deactivate & (PIgnited & PEngRun & !PToofast & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Override -> AX (!PEnum1 = Activate & Enum1 = PEnum1 & (PIgnited & PEngRun & !PToofast & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Override -> AX (!PEnum1 = Activate & Enum1 = Activate & (PIgnited & PEngRun & !PToofast & !PBrake) -> CruiseControl = QC-CruiseControl-NULL))
SPEC AG (CruiseControl = Override -> AX (!PEnum1 = Activate & Enum1 = Activate & (PIgnited & PEngRun & !PToofast & !PBrake) -> CruiseControl = Override))
SPEC AG (CruiseControl = Override -> AX (!PEnum1 = Activate & Enum1 = Activate & (PIgnited & PEngRun & !PToofast & !PBrake) -> CruiseControl = Inactive))
SPEC AG (CruiseControl = Override -> AX (!PEnum1 = Activate & Enum1 = Activate & (PIgnited & PEngRun & !PToofast & !PBrake) -> CruiseControl = Off))
SPEC AG (CruiseControl = QC-CruiseControl-NULL -> AX (!PEnum1 = Resume & Enum1 = Resume & (PIgnited & PEngRun & !PToofast & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Cruise -> AX (!PEnum1 = Resume & Enum1 = Resume & (PIgnited & PEngRun & !PToofast & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Inactive -> AX (!PEnum1 = Resume & Enum1 = Resume & (PIgnited & PEngRun & !PToofast & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Off -> AX (!PEnum1 = Resume & Enum1 = Resume & (PIgnited & PEngRun & !PToofast & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Override -> AX (!PEnum1 = Deactivate & Enum1 = Resume & (PIgnited & PEngRun & !PToofast & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Override -> AX (!PEnum1 = Activate & Enum1 = Resume & (PIgnited & PEngRun & !PToofast & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Override -> AX (!PEnum1 = Enum1 & Enum1 = Resume & (PIgnited & PEngRun & !PToofast & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Override -> AX (!PEnum1 = Resume & Enum1 = Deactivate & (PIgnited & PEngRun & !PToofast & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Override -> AX (!PEnum1 = Resume & Enum1 = Activate & (PIgnited & PEngRun & !PToofast & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Override -> AX (!PEnum1 = Resume & Enum1 = PEnum1 & (PIgnited & PEngRun & !PToofast & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Override -> AX (!PEnum1 = Resume & Enum1 = Resume & (PIgnited & PEngRun & !PToofast & !PBrake) -> CruiseControl = QC-CruiseControl-NULL))
SPEC AG (CruiseControl = Override -> AX (!PEnum1 = Resume & Enum1 = Resume & (PIgnited & PEngRun & !PToofast & !PBrake) -> CruiseControl = Override))
SPEC AG (CruiseControl = Override -> AX (!PEnum1 = Resume & Enum1 = Resume & (PIgnited & PEngRun & !PToofast & !PBrake) -> CruiseControl = Inactive))
SPEC AG (CruiseControl = Override -> AX (!PEnum1 = Resume & Enum1 = Resume & (PIgnited & PEngRun & !PToofast & !PBrake) -> CruiseControl = Off))
SPEC AG (CruiseControl = QC-CruiseControl-NULL -> !Ignited)
SPEC AG (CruiseControl = Override -> !Ignited)
SPEC AG (CruiseControl = Cruise -> !Ignited)
SPEC AG (CruiseControl = Inactive -> !Ignited)
SPEC AG (CruiseControl = QC-CruiseControl-NULL -> Ignited)
SPEC AG (CruiseControl = Override -> Ignited)
SPEC AG (CruiseControl = Cruise -> Ignited)
SPEC AG (CruiseControl = Off -> Ignited)
SPEC AG (CruiseControl = QC-CruiseControl-NULL -> Ignited & EngRun & !Toofast & !Brake & !Enum1 = Deactivate)
SPEC AG (CruiseControl = Override -> Ignited & EngRun & !Toofast & !Brake & !Enum1 = Deactivate)
SPEC AG (CruiseControl = Inactive -> Ignited & EngRun & !Toofast & !Brake & !Enum1 = Deactivate)
SPEC AG (CruiseControl = Off -> Ignited & EngRun & !Toofast & !Brake & !Enum1 = Deactivate)
SPEC AG (CruiseControl = Cruise -> Ignited & EngRun & !Toofast & !Brake & !Enum1 = Resume)
SPEC AG (CruiseControl = Cruise -> Ignited & EngRun & !Toofast & !Brake & !Enum1 = Activate)
SPEC AG (CruiseControl = Cruise -> Ignited & EngRun & !Toofast & !Brake & !Enum1 = PEnum1)
SPEC AG (CruiseControl = QC-CruiseControl-NULL -> Ignited & EngRun)
SPEC AG (CruiseControl = Cruise -> Ignited & EngRun)
SPEC AG (CruiseControl = Inactive -> Ignited & EngRun)
SPEC AG (CruiseControl = Off -> Ignited & EngRun)
SPEC AG (CruiseControl = Off -> AX (!PIgnited | Ignited -> CruiseControl = Inactive))
SPEC AG (CruiseControl = Inactive -> AX (PIgnited | !Ignited -> CruiseControl = Off))
SPEC AG (CruiseControl = Inactive -> AX (!PEnum1 = Activate & Enum1 = Activate | PIgnited & PEngRun & !PToofast & !PBrake -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Inactive -> AX ((!PEnum1 = Activate | Enum1 = Activate) & (PIgnited & PEngRun & !PToofast & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Inactive -> AX (!PEnum1 = Activate & Enum1 = Activate & (PIgnited & PEngRun & !PToofast | !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Inactive -> AX (!PEnum1 = Activate & Enum1 = Activate & ((PIgnited & PEngRun | !PToofast) & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Inactive -> AX (!PEnum1 = Activate & Enum1 = Activate & ((PIgnited | PEngRun) & !PToofast & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Cruise -> AX (PIgnited | !Ignited -> CruiseControl = Off))
SPEC AG (CruiseControl = Cruise -> AX (!PToofast & Toofast | PIgnited -> CruiseControl = Inactive))
SPEC AG (CruiseControl = Cruise -> AX ((!PToofast | Toofast) & PIgnited -> CruiseControl = Inactive))
SPEC AG (CruiseControl = Cruise -> AX (!PBrake & Brake | PIgnited & PEngRun & !PToofast -> CruiseControl = Override))
SPEC AG (CruiseControl = Cruise -> AX ((!PBrake | Brake) & (PIgnited & PEngRun & !PToofast) -> CruiseControl = Override))
SPEC AG (CruiseControl = Cruise -> AX (!PBrake & Brake & (PIgnited & PEngRun | !PToofast) -> CruiseControl = Override))
SPEC AG (CruiseControl = Cruise -> AX (!PBrake & Brake & ((PIgnited | PEngRun) & !PToofast) -> CruiseControl = Override))
SPEC AG (CruiseControl = Cruise -> AX (!PEnum1 = Deactivate & Enum1 = Deactivate | PIgnited & PEngRun & !PToofast -> CruiseControl = Override))
SPEC AG (CruiseControl = Cruise -> AX ((!PEnum1 = Deactivate | Enum1 = Deactivate) & (PIgnited & PEngRun & !PToofast) -> CruiseControl = Override))
SPEC AG (CruiseControl = Cruise -> AX (!PEnum1 = Deactivate & Enum1 = Deactivate & (PIgnited & PEngRun | !PToofast) -> CruiseControl = Override))
SPEC AG (CruiseControl = Cruise -> AX (!PEnum1 = Deactivate & Enum1 = Deactivate & ((PIgnited | PEngRun) & !PToofast) -> CruiseControl = Override))
SPEC AG (CruiseControl = Override -> AX (PIgnited | !Ignited -> CruiseControl = Off))
SPEC AG (CruiseControl = Override -> AX (!PEnum1 = Activate & Enum1 = Activate | PIgnited & PEngRun & !PToofast & !PBrake -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Override -> AX ((!PEnum1 = Activate | Enum1 = Activate) & (PIgnited & PEngRun & !PToofast & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Override -> AX (!PEnum1 = Activate & Enum1 = Activate & (PIgnited & PEngRun & !PToofast | !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Override -> AX (!PEnum1 = Activate & Enum1 = Activate & ((PIgnited & PEngRun | !PToofast) & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Override -> AX (!PEnum1 = Activate & Enum1 = Activate & ((PIgnited | PEngRun) & !PToofast & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Override -> AX (!PEnum1 = Resume & Enum1 = Resume | PIgnited & PEngRun & !PToofast & !PBrake -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Override -> AX ((!PEnum1 = Resume | Enum1 = Resume) & (PIgnited & PEngRun & !PToofast & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Override -> AX (!PEnum1 = Resume & Enum1 = Resume & (PIgnited & PEngRun & !PToofast | !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Override -> AX (!PEnum1 = Resume & Enum1 = Resume & ((PIgnited & PEngRun | !PToofast) & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Override -> AX (!PEnum1 = Resume & Enum1 = Resume & ((PIgnited | PEngRun) & !PToofast & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Cruise -> Ignited & EngRun & !Toofast & !Brake | !Enum1 = Deactivate)
SPEC AG (CruiseControl = Cruise -> (Ignited & EngRun & !Toofast | !Brake) & !Enum1 = Deactivate)
SPEC AG (CruiseControl = Cruise -> (Ignited & EngRun | !Toofast) & !Brake & !Enum1 = Deactivate)
SPEC AG (CruiseControl = Cruise -> (Ignited | EngRun) & !Toofast & !Brake & !Enum1 = Deactivate)
SPEC AG (CruiseControl = Override -> Ignited | EngRun)
SPEC AG (CruiseControl = Off -> AX (!Brake & Ignited -> CruiseControl = Inactive))
SPEC AG (CruiseControl = Off -> AX (!PBrake & Ignited -> CruiseControl = Inactive))
SPEC AG (CruiseControl = Off -> AX (!EngRun & Ignited -> CruiseControl = Inactive))
SPEC AG (CruiseControl = Off -> AX (!PEngRun & Ignited -> CruiseControl = Inactive))
SPEC AG (CruiseControl = Off -> AX (!Toofast & Ignited -> CruiseControl = Inactive))
SPEC AG (CruiseControl = Off -> AX (!PToofast & Ignited -> CruiseControl = Inactive))
SPEC AG (CruiseControl = Off -> AX (!Ignited & Ignited -> CruiseControl = Inactive))
SPEC AG (CruiseControl = Off -> AX (!PIgnited & PIgnited -> CruiseControl = Inactive))
SPEC AG (CruiseControl = Off -> AX (!PIgnited & Brake -> CruiseControl = Inactive))
SPEC AG (CruiseControl = Off -> AX (!PIgnited & PBrake -> CruiseControl = Inactive))
SPEC AG (CruiseControl = Off -> AX (!PIgnited & EngRun -> CruiseControl = Inactive))
SPEC AG (CruiseControl = Off -> AX (!PIgnited & PEngRun -> CruiseControl = Inactive))
SPEC AG (CruiseControl = Off -> AX (!PIgnited & Toofast -> CruiseControl = Inactive))
SPEC AG (CruiseControl = Off -> AX (!PIgnited & PToofast -> CruiseControl = Inactive))
SPEC AG (CruiseControl = Inactive -> AX (Brake & !Ignited -> CruiseControl = Off))
SPEC AG (CruiseControl = Inactive -> AX (PBrake & !Ignited -> CruiseControl = Off))
SPEC AG (CruiseControl = Inactive -> AX (EngRun & !Ignited -> CruiseControl = Off))
SPEC AG (CruiseControl = Inactive -> AX (PEngRun & !Ignited -> CruiseControl = Off))
SPEC AG (CruiseControl = Inactive -> AX (Toofast & !Ignited -> CruiseControl = Off))
SPEC AG (CruiseControl = Inactive -> AX (PToofast & !Ignited -> CruiseControl = Off))
SPEC AG (CruiseControl = Inactive -> AX (Ignited & !Ignited -> CruiseControl = Off))
SPEC AG (CruiseControl = Inactive -> AX (PIgnited & !PIgnited -> CruiseControl = Off))
SPEC AG (CruiseControl = Inactive -> AX (PIgnited & !Brake -> CruiseControl = Off))
SPEC AG (CruiseControl = Inactive -> AX (PIgnited & !PBrake -> CruiseControl = Off))
SPEC AG (CruiseControl = Inactive -> AX (PIgnited & !EngRun -> CruiseControl = Off))
SPEC AG (CruiseControl = Inactive -> AX (PIgnited & !PEngRun -> CruiseControl = Off))
SPEC AG (CruiseControl = Inactive -> AX (PIgnited & !Toofast -> CruiseControl = Off))
SPEC AG (CruiseControl = Inactive -> AX (PIgnited & !PToofast -> CruiseControl = Off))
SPEC AG (CruiseControl = Inactive -> AX (!Enum1 = Activate & Enum1 = Activate & (PIgnited & PEngRun & !PToofast & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Inactive -> AX (!PEnum1 = Activate & PEnum1 = Activate & (PIgnited & PEngRun & !PToofast & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Inactive -> AX (!PEnum1 = Activate & Enum1 = Activate & (Brake & PEngRun & !PToofast & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Inactive -> AX (!PEnum1 = Activate & Enum1 = Activate & (PBrake & PEngRun & !PToofast & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Inactive -> AX (!PEnum1 = Activate & Enum1 = Activate & (EngRun & PEngRun & !PToofast & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Inactive -> AX (!PEnum1 = Activate & Enum1 = Activate & (PEngRun & PEngRun & !PToofast & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Inactive -> AX (!PEnum1 = Activate & Enum1 = Activate & (Toofast & PEngRun & !PToofast & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Inactive -> AX (!PEnum1 = Activate & Enum1 = Activate & (PToofast & PEngRun & !PToofast & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Inactive -> AX (!PEnum1 = Activate & Enum1 = Activate & (Ignited & PEngRun & !PToofast & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Inactive -> AX (!PEnum1 = Activate & Enum1 = Activate & (PIgnited & Toofast & !PToofast & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Inactive -> AX (!PEnum1 = Activate & Enum1 = Activate & (PIgnited & PToofast & !PToofast & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Inactive -> AX (!PEnum1 = Activate & Enum1 = Activate & (PIgnited & Ignited & !PToofast & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Inactive -> AX (!PEnum1 = Activate & Enum1 = Activate & (PIgnited & PIgnited & !PToofast & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Inactive -> AX (!PEnum1 = Activate & Enum1 = Activate & (PIgnited & Brake & !PToofast & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Inactive -> AX (!PEnum1 = Activate & Enum1 = Activate & (PIgnited & PBrake & !PToofast & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Inactive -> AX (!PEnum1 = Activate & Enum1 = Activate & (PIgnited & EngRun & !PToofast & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Inactive -> AX (!PEnum1 = Activate & Enum1 = Activate & (PIgnited & PEngRun & !Ignited & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Inactive -> AX (!PEnum1 = Activate & Enum1 = Activate & (PIgnited & PEngRun & !PIgnited & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Inactive -> AX (!PEnum1 = Activate & Enum1 = Activate & (PIgnited & PEngRun & !Brake & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Inactive -> AX (!PEnum1 = Activate & Enum1 = Activate & (PIgnited & PEngRun & !PBrake & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Inactive -> AX (!PEnum1 = Activate & Enum1 = Activate & (PIgnited & PEngRun & !EngRun & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Inactive -> AX (!PEnum1 = Activate & Enum1 = Activate & (PIgnited & PEngRun & !PEngRun & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Inactive -> AX (!PEnum1 = Activate & Enum1 = Activate & (PIgnited & PEngRun & !Toofast & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Inactive -> AX (!PEnum1 = Activate & Enum1 = Activate & (PIgnited & PEngRun & !PToofast & !EngRun) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Inactive -> AX (!PEnum1 = Activate & Enum1 = Activate & (PIgnited & PEngRun & !PToofast & !PEngRun) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Inactive -> AX (!PEnum1 = Activate & Enum1 = Activate & (PIgnited & PEngRun & !PToofast & !Toofast) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Inactive -> AX (!PEnum1 = Activate & Enum1 = Activate & (PIgnited & PEngRun & !PToofast & !PToofast) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Inactive -> AX (!PEnum1 = Activate & Enum1 = Activate & (PIgnited & PEngRun & !PToofast & !Ignited) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Inactive -> AX (!PEnum1 = Activate & Enum1 = Activate & (PIgnited & PEngRun & !PToofast & !PIgnited) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Inactive -> AX (!PEnum1 = Activate & Enum1 = Activate & (PIgnited & PEngRun & !PToofast & !Brake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Cruise -> AX (Brake & !Ignited -> CruiseControl = Off))
SPEC AG (CruiseControl = Cruise -> AX (PBrake & !Ignited -> CruiseControl = Off))
SPEC AG (CruiseControl = Cruise -> AX (EngRun & !Ignited -> CruiseControl = Off))
SPEC AG (CruiseControl = Cruise -> AX (PEngRun & !Ignited -> CruiseControl = Off))
SPEC AG (CruiseControl = Cruise -> AX (Toofast & !Ignited -> CruiseControl = Off))
SPEC AG (CruiseControl = Cruise -> AX (PToofast & !Ignited -> CruiseControl = Off))
SPEC AG (CruiseControl = Cruise -> AX (Ignited & !Ignited -> CruiseControl = Off))
SPEC AG (CruiseControl = Cruise -> AX (PIgnited & !PIgnited -> CruiseControl = Off))
SPEC AG (CruiseControl = Cruise -> AX (PIgnited & !Brake -> CruiseControl = Off))
SPEC AG (CruiseControl = Cruise -> AX (PIgnited & !PBrake -> CruiseControl = Off))
SPEC AG (CruiseControl = Cruise -> AX (PIgnited & !EngRun -> CruiseControl = Off))
SPEC AG (CruiseControl = Cruise -> AX (PIgnited & !PEngRun -> CruiseControl = Off))
SPEC AG (CruiseControl = Cruise -> AX (PIgnited & !Toofast -> CruiseControl = Off))
SPEC AG (CruiseControl = Cruise -> AX (PIgnited & !PToofast -> CruiseControl = Off))
SPEC AG (CruiseControl = Cruise -> AX (!Ignited & Toofast & PIgnited -> CruiseControl = Inactive))
SPEC AG (CruiseControl = Cruise -> AX (!PIgnited & Toofast & PIgnited -> CruiseControl = Inactive))
SPEC AG (CruiseControl = Cruise -> AX (!Brake & Toofast & PIgnited -> CruiseControl = Inactive))
SPEC AG (CruiseControl = Cruise -> AX (!PBrake & Toofast & PIgnited -> CruiseControl = Inactive))
SPEC AG (CruiseControl = Cruise -> AX (!EngRun & Toofast & PIgnited -> CruiseControl = Inactive))
SPEC AG (CruiseControl = Cruise -> AX (!PEngRun & Toofast & PIgnited -> CruiseControl = Inactive))
SPEC AG (CruiseControl = Cruise -> AX (!Toofast & Toofast & PIgnited -> CruiseControl = Inactive))
SPEC AG (CruiseControl = Cruise -> AX (!PToofast & PToofast & PIgnited -> CruiseControl = Inactive))
SPEC AG (CruiseControl = Cruise -> AX (!PToofast & Ignited & PIgnited -> CruiseControl = Inactive))
SPEC AG (CruiseControl = Cruise -> AX (!PToofast & PIgnited & PIgnited -> CruiseControl = Inactive))
SPEC AG (CruiseControl = Cruise -> AX (!PToofast & Brake & PIgnited -> CruiseControl = Inactive))
SPEC AG (CruiseControl = Cruise -> AX (!PToofast & PBrake & PIgnited -> CruiseControl = Inactive))
SPEC AG (CruiseControl = Cruise -> AX (!PToofast & EngRun & PIgnited -> CruiseControl = Inactive))
SPEC AG (CruiseControl = Cruise -> AX (!PToofast & PEngRun & PIgnited -> CruiseControl = Inactive))
SPEC AG (CruiseControl = Cruise -> AX (!PToofast & Toofast & Brake -> CruiseControl = Inactive))
SPEC AG (CruiseControl = Cruise -> AX (!PToofast & Toofast & PBrake -> CruiseControl = Inactive))
SPEC AG (CruiseControl = Cruise -> AX (!PToofast & Toofast & EngRun -> CruiseControl = Inactive))
SPEC AG (CruiseControl = Cruise -> AX (!PToofast & Toofast & PEngRun -> CruiseControl = Inactive))
SPEC AG (CruiseControl = Cruise -> AX (!PToofast & Toofast & Toofast -> CruiseControl = Inactive))
SPEC AG (CruiseControl = Cruise -> AX (!PToofast & Toofast & PToofast -> CruiseControl = Inactive))
SPEC AG (CruiseControl = Cruise -> AX (!PToofast & Toofast & Ignited -> CruiseControl = Inactive))
SPEC AG (CruiseControl = Cruise -> AX (!EngRun & Brake & (PIgnited & PEngRun & !PToofast) -> CruiseControl = Override))
SPEC AG (CruiseControl = Cruise -> AX (!PEngRun & Brake & (PIgnited & PEngRun & !PToofast) -> CruiseControl = Override))
SPEC AG (CruiseControl = Cruise -> AX (!Toofast & Brake & (PIgnited & PEngRun & !PToofast) -> CruiseControl = Override))
SPEC AG (CruiseControl = Cruise -> AX (!PToofast & Brake & (PIgnited & PEngRun & !PToofast) -> CruiseControl = Override))
SPEC AG (CruiseControl = Cruise -> AX (!Ignited & Brake & (PIgnited & PEngRun & !PToofast) -> CruiseControl = Override))
SPEC AG (CruiseControl = Cruise -> AX (!PIgnited & Brake & (PIgnited & PEngRun & !PToofast) -> CruiseControl = Override))
SPEC AG (CruiseControl = Cruise -> AX (!Brake & Brake & (PIgnited & PEngRun & !PToofast) -> CruiseControl = Override))
SPEC AG (CruiseControl = Cruise -> AX (!PBrake & PBrake & (PIgnited & PEngRun & !PToofast) -> CruiseControl = Override))
SPEC AG (CruiseControl = Cruise -> AX (!PBrake & EngRun & (PIgnited & PEngRun & !PToofast) -> CruiseControl = Override))
SPEC AG (CruiseControl = Cruise -> AX (!PBrake & PEngRun & (PIgnited & PEngRun & !PToofast) -> CruiseControl = Override))
SPEC AG (CruiseControl = Cruise -> AX (!PBrake & Toofast & (PIgnited & PEngRun & !PToofast) -> CruiseControl = Override))
SPEC AG (CruiseControl = Cruise -> AX (!PBrake & PToofast & (PIgnited & PEngRun & !PToofast) -> CruiseControl = Override))
SPEC AG (CruiseControl = Cruise -> AX (!PBrake & Ignited & (PIgnited & PEngRun & !PToofast) -> CruiseControl = Override))
SPEC AG (CruiseControl = Cruise -> AX (!PBrake & PIgnited & (PIgnited & PEngRun & !PToofast) -> CruiseControl = Override))
SPEC AG (CruiseControl = Cruise -> AX (!PBrake & Brake & (Brake & PEngRun & !PToofast) -> CruiseControl = Override))
SPEC AG (CruiseControl = Cruise -> AX (!PBrake & Brake & (PBrake & PEngRun & !PToofast) -> CruiseControl = Override))
SPEC AG (CruiseControl = Cruise -> AX (!PBrake & Brake & (EngRun & PEngRun & !PToofast) -> CruiseControl = Override))
SPEC AG (CruiseControl = Cruise -> AX (!PBrake & Brake & (PEngRun & PEngRun & !PToofast) -> CruiseControl = Override))
SPEC AG (CruiseControl = Cruise -> AX (!PBrake & Brake & (Toofast & PEngRun & !PToofast) -> CruiseControl = Override))
SPEC AG (CruiseControl = Cruise -> AX (!PBrake & Brake & (PToofast & PEngRun & !PToofast) -> CruiseControl = Override))
SPEC AG (CruiseControl = Cruise -> AX (!PBrake & Brake & (Ignited & PEngRun & !PToofast) -> CruiseControl = Override))
SPEC AG (CruiseControl = Cruise -> AX (!PBrake & Brake & (PIgnited & Toofast & !PToofast) -> CruiseControl = Override))
SPEC AG (CruiseControl = Cruise -> AX (!PBrake & Brake & (PIgnited & PToofast & !PToofast) -> CruiseControl = Override))
SPEC AG (CruiseControl = Cruise -> AX (!PBrake & Brake & (PIgnited & Ignited & !PToofast) -> CruiseControl = Override))
SPEC AG (CruiseControl = Cruise -> AX (!PBrake & Brake & (PIgnited & PIgnited & !PToofast) -> CruiseControl = Override))
SPEC AG (CruiseControl = Cruise -> AX (!PBrake & Brake & (PIgnited & Brake & !PToofast) -> CruiseControl = Override))
SPEC AG (CruiseControl = Cruise -> AX (!PBrake & Brake & (PIgnited & PBrake & !PToofast) -> CruiseControl = Override))
SPEC AG (CruiseControl = Cruise -> AX (!PBrake & Brake & (PIgnited & EngRun & !PToofast) -> CruiseControl = Override))
SPEC AG (CruiseControl = Cruise -> AX (!PBrake & Brake & (PIgnited & PEngRun & !Ignited) -> CruiseControl = Override))
SPEC AG (CruiseControl = Cruise -> AX (!PBrake & Brake & (PIgnited & PEngRun & !PIgnited) -> CruiseControl = Override))
SPEC AG (CruiseControl = Cruise -> AX (!PBrake & Brake & (PIgnited & PEngRun & !Brake) -> CruiseControl = Override))
SPEC AG (CruiseControl = Cruise -> AX (!PBrake & Brake & (PIgnited & PEngRun & !PBrake) -> CruiseControl = Override))
SPEC AG (CruiseControl = Cruise -> AX (!PBrake & Brake & (PIgnited & PEngRun & !EngRun) -> CruiseControl = Override))
SPEC AG (CruiseControl = Cruise -> AX (!PBrake & Brake & (PIgnited & PEngRun & !PEngRun) -> CruiseControl = Override))
SPEC AG (CruiseControl = Cruise -> AX (!PBrake & Brake & (PIgnited & PEngRun & !Toofast) -> CruiseControl = Override))
SPEC AG (CruiseControl = Cruise -> AX (!Enum1 = Deactivate & Enum1 = Deactivate & (PIgnited & PEngRun & !PToofast) -> CruiseControl = Override))
SPEC AG (CruiseControl = Cruise -> AX (!PEnum1 = Deactivate & PEnum1 = Deactivate & (PIgnited & PEngRun & !PToofast) -> CruiseControl = Override))
SPEC AG (CruiseControl = Cruise -> AX (!PEnum1 = Deactivate & Enum1 = Deactivate & (Brake & PEngRun & !PToofast) -> CruiseControl = Override))
SPEC AG (CruiseControl = Cruise -> AX (!PEnum1 = Deactivate & Enum1 = Deactivate & (PBrake & PEngRun & !PToofast) -> CruiseControl = Override))
SPEC AG (CruiseControl = Cruise -> AX (!PEnum1 = Deactivate & Enum1 = Deactivate & (EngRun & PEngRun & !PToofast) -> CruiseControl = Override))
SPEC AG (CruiseControl = Cruise -> AX (!PEnum1 = Deactivate & Enum1 = Deactivate & (PEngRun & PEngRun & !PToofast) -> CruiseControl = Override))
SPEC AG (CruiseControl = Cruise -> AX (!PEnum1 = Deactivate & Enum1 = Deactivate & (Toofast & PEngRun & !PToofast) -> CruiseControl = Override))
SPEC AG (CruiseControl = Cruise -> AX (!PEnum1 = Deactivate & Enum1 = Deactivate & (PToofast & PEngRun & !PToofast) -> CruiseControl = Override))
SPEC AG (CruiseControl = Cruise -> AX (!PEnum1 = Deactivate & Enum1 = Deactivate & (Ignited & PEngRun & !PToofast) -> CruiseControl = Override))
SPEC AG (CruiseControl = Cruise -> AX (!PEnum1 = Deactivate & Enum1 = Deactivate & (PIgnited & Toofast & !PToofast) -> CruiseControl = Override))
SPEC AG (CruiseControl = Cruise -> AX (!PEnum1 = Deactivate & Enum1 = Deactivate & (PIgnited & PToofast & !PToofast) -> CruiseControl = Override))
SPEC AG (CruiseControl = Cruise -> AX (!PEnum1 = Deactivate & Enum1 = Deactivate & (PIgnited & Ignited & !PToofast) -> CruiseControl = Override))
SPEC AG (CruiseControl = Cruise -> AX (!PEnum1 = Deactivate & Enum1 = Deactivate & (PIgnited & PIgnited & !PToofast) -> CruiseControl = Override))
SPEC AG (CruiseControl = Cruise -> AX (!PEnum1 = Deactivate & Enum1 = Deactivate & (PIgnited & Brake & !PToofast) -> CruiseControl = Override))
SPEC AG (CruiseControl = Cruise -> AX (!PEnum1 = Deactivate & Enum1 = Deactivate & (PIgnited & PBrake & !PToofast) -> CruiseControl = Override))
SPEC AG (CruiseControl = Cruise -> AX (!PEnum1 = Deactivate & Enum1 = Deactivate & (PIgnited & EngRun & !PToofast) -> CruiseControl = Override))
SPEC AG (CruiseControl = Cruise -> AX (!PEnum1 = Deactivate & Enum1 = Deactivate & (PIgnited & PEngRun & !Ignited) -> CruiseControl = Override))
SPEC AG (CruiseControl = Cruise -> AX (!PEnum1 = Deactivate & Enum1 = Deactivate & (PIgnited & PEngRun & !PIgnited) -> CruiseControl = Override))
SPEC AG (CruiseControl = Cruise -> AX (!PEnum1 = Deactivate & Enum1 = Deactivate & (PIgnited & PEngRun & !Brake) -> CruiseControl = Override))
SPEC AG (CruiseControl = Cruise -> AX (!PEnum1 = Deactivate & Enum1 = Deactivate & (PIgnited & PEngRun & !PBrake) -> CruiseControl = Override))
SPEC AG (CruiseControl = Cruise -> AX (!PEnum1 = Deactivate & Enum1 = Deactivate & (PIgnited & PEngRun & !EngRun) -> CruiseControl = Override))
SPEC AG (CruiseControl = Cruise -> AX (!PEnum1 = Deactivate & Enum1 = Deactivate & (PIgnited & PEngRun & !PEngRun) -> CruiseControl = Override))
SPEC AG (CruiseControl = Cruise -> AX (!PEnum1 = Deactivate & Enum1 = Deactivate & (PIgnited & PEngRun & !Toofast) -> CruiseControl = Override))
SPEC AG (CruiseControl = Override -> AX (Brake & !Ignited -> CruiseControl = Off))
SPEC AG (CruiseControl = Override -> AX (PBrake & !Ignited -> CruiseControl = Off))
SPEC AG (CruiseControl = Override -> AX (EngRun & !Ignited -> CruiseControl = Off))
SPEC AG (CruiseControl = Override -> AX (PEngRun & !Ignited -> CruiseControl = Off))
SPEC AG (CruiseControl = Override -> AX (Toofast & !Ignited -> CruiseControl = Off))
SPEC AG (CruiseControl = Override -> AX (PToofast & !Ignited -> CruiseControl = Off))
SPEC AG (CruiseControl = Override -> AX (Ignited & !Ignited -> CruiseControl = Off))
SPEC AG (CruiseControl = Override -> AX (PIgnited & !PIgnited -> CruiseControl = Off))
SPEC AG (CruiseControl = Override -> AX (PIgnited & !Brake -> CruiseControl = Off))
SPEC AG (CruiseControl = Override -> AX (PIgnited & !PBrake -> CruiseControl = Off))
SPEC AG (CruiseControl = Override -> AX (PIgnited & !EngRun -> CruiseControl = Off))
SPEC AG (CruiseControl = Override -> AX (PIgnited & !PEngRun -> CruiseControl = Off))
SPEC AG (CruiseControl = Override -> AX (PIgnited & !Toofast -> CruiseControl = Off))
SPEC AG (CruiseControl = Override -> AX (PIgnited & !PToofast -> CruiseControl = Off))
SPEC AG (CruiseControl = Override -> AX (!Enum1 = Activate & Enum1 = Activate & (PIgnited & PEngRun & !PToofast & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Override -> AX (!PEnum1 = Activate & PEnum1 = Activate & (PIgnited & PEngRun & !PToofast & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Override -> AX (!PEnum1 = Activate & Enum1 = Activate & (Brake & PEngRun & !PToofast & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Override -> AX (!PEnum1 = Activate & Enum1 = Activate & (PBrake & PEngRun & !PToofast & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Override -> AX (!PEnum1 = Activate & Enum1 = Activate & (EngRun & PEngRun & !PToofast & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Override -> AX (!PEnum1 = Activate & Enum1 = Activate & (PEngRun & PEngRun & !PToofast & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Override -> AX (!PEnum1 = Activate & Enum1 = Activate & (Toofast & PEngRun & !PToofast & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Override -> AX (!PEnum1 = Activate & Enum1 = Activate & (PToofast & PEngRun & !PToofast & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Override -> AX (!PEnum1 = Activate & Enum1 = Activate & (Ignited & PEngRun & !PToofast & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Override -> AX (!PEnum1 = Activate & Enum1 = Activate & (PIgnited & Toofast & !PToofast & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Override -> AX (!PEnum1 = Activate & Enum1 = Activate & (PIgnited & PToofast & !PToofast & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Override -> AX (!PEnum1 = Activate & Enum1 = Activate & (PIgnited & Ignited & !PToofast & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Override -> AX (!PEnum1 = Activate & Enum1 = Activate & (PIgnited & PIgnited & !PToofast & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Override -> AX (!PEnum1 = Activate & Enum1 = Activate & (PIgnited & Brake & !PToofast & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Override -> AX (!PEnum1 = Activate & Enum1 = Activate & (PIgnited & PBrake & !PToofast & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Override -> AX (!PEnum1 = Activate & Enum1 = Activate & (PIgnited & EngRun & !PToofast & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Override -> AX (!PEnum1 = Activate & Enum1 = Activate & (PIgnited & PEngRun & !Ignited & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Override -> AX (!PEnum1 = Activate & Enum1 = Activate & (PIgnited & PEngRun & !PIgnited & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Override -> AX (!PEnum1 = Activate & Enum1 = Activate & (PIgnited & PEngRun & !Brake & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Override -> AX (!PEnum1 = Activate & Enum1 = Activate & (PIgnited & PEngRun & !PBrake & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Override -> AX (!PEnum1 = Activate & Enum1 = Activate & (PIgnited & PEngRun & !EngRun & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Override -> AX (!PEnum1 = Activate & Enum1 = Activate & (PIgnited & PEngRun & !PEngRun & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Override -> AX (!PEnum1 = Activate & Enum1 = Activate & (PIgnited & PEngRun & !Toofast & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Override -> AX (!PEnum1 = Activate & Enum1 = Activate & (PIgnited & PEngRun & !PToofast & !EngRun) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Override -> AX (!PEnum1 = Activate & Enum1 = Activate & (PIgnited & PEngRun & !PToofast & !PEngRun) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Override -> AX (!PEnum1 = Activate & Enum1 = Activate & (PIgnited & PEngRun & !PToofast & !Toofast) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Override -> AX (!PEnum1 = Activate & Enum1 = Activate & (PIgnited & PEngRun & !PToofast & !PToofast) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Override -> AX (!PEnum1 = Activate & Enum1 = Activate & (PIgnited & PEngRun & !PToofast & !Ignited) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Override -> AX (!PEnum1 = Activate & Enum1 = Activate & (PIgnited & PEngRun & !PToofast & !PIgnited) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Override -> AX (!PEnum1 = Activate & Enum1 = Activate & (PIgnited & PEngRun & !PToofast & !Brake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Override -> AX (!Enum1 = Resume & Enum1 = Resume & (PIgnited & PEngRun & !PToofast & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Override -> AX (!PEnum1 = Resume & PEnum1 = Resume & (PIgnited & PEngRun & !PToofast & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Override -> AX (!PEnum1 = Resume & Enum1 = Resume & (Brake & PEngRun & !PToofast & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Override -> AX (!PEnum1 = Resume & Enum1 = Resume & (PBrake & PEngRun & !PToofast & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Override -> AX (!PEnum1 = Resume & Enum1 = Resume & (EngRun & PEngRun & !PToofast & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Override -> AX (!PEnum1 = Resume & Enum1 = Resume & (PEngRun & PEngRun & !PToofast & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Override -> AX (!PEnum1 = Resume & Enum1 = Resume & (Toofast & PEngRun & !PToofast & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Override -> AX (!PEnum1 = Resume & Enum1 = Resume & (PToofast & PEngRun & !PToofast & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Override -> AX (!PEnum1 = Resume & Enum1 = Resume & (Ignited & PEngRun & !PToofast & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Override -> AX (!PEnum1 = Resume & Enum1 = Resume & (PIgnited & Toofast & !PToofast & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Override -> AX (!PEnum1 = Resume & Enum1 = Resume & (PIgnited & PToofast & !PToofast & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Override -> AX (!PEnum1 = Resume & Enum1 = Resume & (PIgnited & Ignited & !PToofast & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Override -> AX (!PEnum1 = Resume & Enum1 = Resume & (PIgnited & PIgnited & !PToofast & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Override -> AX (!PEnum1 = Resume & Enum1 = Resume & (PIgnited & Brake & !PToofast & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Override -> AX (!PEnum1 = Resume & Enum1 = Resume & (PIgnited & PBrake & !PToofast & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Override -> AX (!PEnum1 = Resume & Enum1 = Resume & (PIgnited & EngRun & !PToofast & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Override -> AX (!PEnum1 = Resume & Enum1 = Resume & (PIgnited & PEngRun & !Ignited & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Override -> AX (!PEnum1 = Resume & Enum1 = Resume & (PIgnited & PEngRun & !PIgnited & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Override -> AX (!PEnum1 = Resume & Enum1 = Resume & (PIgnited & PEngRun & !Brake & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Override -> AX (!PEnum1 = Resume & Enum1 = Resume & (PIgnited & PEngRun & !PBrake & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Override -> AX (!PEnum1 = Resume & Enum1 = Resume & (PIgnited & PEngRun & !EngRun & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Override -> AX (!PEnum1 = Resume & Enum1 = Resume & (PIgnited & PEngRun & !PEngRun & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Override -> AX (!PEnum1 = Resume & Enum1 = Resume & (PIgnited & PEngRun & !Toofast & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Override -> AX (!PEnum1 = Resume & Enum1 = Resume & (PIgnited & PEngRun & !PToofast & !EngRun) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Override -> AX (!PEnum1 = Resume & Enum1 = Resume & (PIgnited & PEngRun & !PToofast & !PEngRun) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Override -> AX (!PEnum1 = Resume & Enum1 = Resume & (PIgnited & PEngRun & !PToofast & !Toofast) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Override -> AX (!PEnum1 = Resume & Enum1 = Resume & (PIgnited & PEngRun & !PToofast & !PToofast) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Override -> AX (!PEnum1 = Resume & Enum1 = Resume & (PIgnited & PEngRun & !PToofast & !Ignited) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Override -> AX (!PEnum1 = Resume & Enum1 = Resume & (PIgnited & PEngRun & !PToofast & !PIgnited) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Override -> AX (!PEnum1 = Resume & Enum1 = Resume & (PIgnited & PEngRun & !PToofast & !Brake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Off -> !PIgnited)
SPEC AG (CruiseControl = Off -> !Brake)
SPEC AG (CruiseControl = Off -> !PBrake)
SPEC AG (CruiseControl = Off -> !EngRun)
SPEC AG (CruiseControl = Off -> !PEngRun)
SPEC AG (CruiseControl = Off -> !Toofast)
SPEC AG (CruiseControl = Off -> !PToofast)
SPEC AG (CruiseControl = Inactive -> PIgnited)
SPEC AG (CruiseControl = Inactive -> Brake)
SPEC AG (CruiseControl = Inactive -> PBrake)
SPEC AG (CruiseControl = Inactive -> EngRun)
SPEC AG (CruiseControl = Inactive -> PEngRun)
SPEC AG (CruiseControl = Inactive -> Toofast)
SPEC AG (CruiseControl = Inactive -> PToofast)
SPEC AG (CruiseControl = Cruise -> PIgnited & EngRun & !Toofast & !Brake & !Enum1 = Deactivate)
SPEC AG (CruiseControl = Cruise -> Brake & EngRun & !Toofast & !Brake & !Enum1 = Deactivate)
SPEC AG (CruiseControl = Cruise -> PBrake & EngRun & !Toofast & !Brake & !Enum1 = Deactivate)
SPEC AG (CruiseControl = Cruise -> EngRun & EngRun & !Toofast & !Brake & !Enum1 = Deactivate)
SPEC AG (CruiseControl = Cruise -> PEngRun & EngRun & !Toofast & !Brake & !Enum1 = Deactivate)
SPEC AG (CruiseControl = Cruise -> Toofast & EngRun & !Toofast & !Brake & !Enum1 = Deactivate)
SPEC AG (CruiseControl = Cruise -> PToofast & EngRun & !Toofast & !Brake & !Enum1 = Deactivate)
SPEC AG (CruiseControl = Cruise -> Ignited & PEngRun & !Toofast & !Brake & !Enum1 = Deactivate)
SPEC AG (CruiseControl = Cruise -> Ignited & Toofast & !Toofast & !Brake & !Enum1 = Deactivate)
SPEC AG (CruiseControl = Cruise -> Ignited & PToofast & !Toofast & !Brake & !Enum1 = Deactivate)
SPEC AG (CruiseControl = Cruise -> Ignited & Ignited & !Toofast & !Brake & !Enum1 = Deactivate)
SPEC AG (CruiseControl = Cruise -> Ignited & PIgnited & !Toofast & !Brake & !Enum1 = Deactivate)
SPEC AG (CruiseControl = Cruise -> Ignited & Brake & !Toofast & !Brake & !Enum1 = Deactivate)
SPEC AG (CruiseControl = Cruise -> Ignited & PBrake & !Toofast & !Brake & !Enum1 = Deactivate)
SPEC AG (CruiseControl = Cruise -> Ignited & EngRun & !PToofast & !Brake & !Enum1 = Deactivate)
SPEC AG (CruiseControl = Cruise -> Ignited & EngRun & !Ignited & !Brake & !Enum1 = Deactivate)
SPEC AG (CruiseControl = Cruise -> Ignited & EngRun & !PIgnited & !Brake & !Enum1 = Deactivate)
SPEC AG (CruiseControl = Cruise -> Ignited & EngRun & !Brake & !Brake & !Enum1 = Deactivate)
SPEC AG (CruiseControl = Cruise -> Ignited & EngRun & !PBrake & !Brake & !Enum1 = Deactivate)
SPEC AG (CruiseControl = Cruise -> Ignited & EngRun & !EngRun & !Brake & !Enum1 = Deactivate)
SPEC AG (CruiseControl = Cruise -> Ignited & EngRun & !PEngRun & !Brake & !Enum1 = Deactivate)
SPEC AG (CruiseControl = Cruise -> Ignited & EngRun & !Toofast & !PBrake & !Enum1 = Deactivate)
SPEC AG (CruiseControl = Cruise -> Ignited & EngRun & !Toofast & !EngRun & !Enum1 = Deactivate)
SPEC AG (CruiseControl = Cruise -> Ignited & EngRun & !Toofast & !PEngRun & !Enum1 = Deactivate)
SPEC AG (CruiseControl = Cruise -> Ignited & EngRun & !Toofast & !Toofast & !Enum1 = Deactivate)
SPEC AG (CruiseControl = Cruise -> Ignited & EngRun & !Toofast & !PToofast & !Enum1 = Deactivate)
SPEC AG (CruiseControl = Cruise -> Ignited & EngRun & !Toofast & !Ignited & !Enum1 = Deactivate)
SPEC AG (CruiseControl = Cruise -> Ignited & EngRun & !Toofast & !PIgnited & !Enum1 = Deactivate)
SPEC AG (CruiseControl = Cruise -> Ignited & EngRun & !Toofast & !Brake & !PEnum1 = Deactivate)
SPEC AG (CruiseControl = Override -> PIgnited & EngRun)
SPEC AG (CruiseControl = Override -> Brake & EngRun)
SPEC AG (CruiseControl = Override -> PBrake & EngRun)
SPEC AG (CruiseControl = Override -> EngRun & EngRun)
SPEC AG (CruiseControl = Override -> PEngRun & EngRun)
SPEC AG (CruiseControl = Override -> Toofast & EngRun)
SPEC AG (CruiseControl = Override -> PToofast & EngRun)
SPEC AG (CruiseControl = Override -> Ignited & PEngRun)
SPEC AG (CruiseControl = Override -> Ignited & Toofast)
SPEC AG (CruiseControl = Override -> Ignited & PToofast)
SPEC AG (CruiseControl = Override -> Ignited & Ignited)
SPEC AG (CruiseControl = Override -> Ignited & PIgnited)
SPEC AG (CruiseControl = Override -> Ignited & Brake)
SPEC AG (CruiseControl = Override -> Ignited & PBrake)
SPEC AG AX (!PIgnited & Ignited -> CruiseControl = Inactive)
SPEC AG (CruiseControl = Off -> AX (!PIgnited & Ignited))
SPEC AG (CruiseControl = Off -> AX (!PIgnited -> CruiseControl = Inactive))
SPEC AG (CruiseControl = Off -> AX (Ignited -> CruiseControl = Inactive))
SPEC AG AX (PIgnited & !Ignited -> CruiseControl = Off)
SPEC AG (CruiseControl = Inactive -> AX (PIgnited & !Ignited))
SPEC AG (CruiseControl = Inactive -> AX (PIgnited -> CruiseControl = Off))
SPEC AG (CruiseControl = Inactive -> AX (!Ignited -> CruiseControl = Off))
SPEC AG AX (!PEnum1 = Activate & Enum1 = Activate & (PIgnited & PEngRun & !PToofast & !PBrake) -> CruiseControl = Cruise)
SPEC AG (CruiseControl = Inactive -> AX (!PEnum1 = Activate & Enum1 = Activate & (PIgnited & PEngRun & !PToofast & !PBrake)))
SPEC AG (CruiseControl = Inactive -> AX (!PEnum1 = Activate & (PIgnited & PEngRun & !PToofast & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Inactive -> AX (Enum1 = Activate & (PIgnited & PEngRun & !PToofast & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Inactive -> AX (!PEnum1 = Activate & Enum1 = Activate & (PIgnited & PEngRun & !PToofast) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Inactive -> AX (!PEnum1 = Activate & Enum1 = Activate & (PIgnited & PEngRun & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Inactive -> AX (!PEnum1 = Activate & Enum1 = Activate & (PIgnited & !PToofast & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Inactive -> AX (!PEnum1 = Activate & Enum1 = Activate & (PEngRun & !PToofast & !PBrake) -> CruiseControl = Cruise))
SPEC AG AX (PIgnited & !Ignited -> CruiseControl = Off)
SPEC AG (CruiseControl = Cruise -> AX (PIgnited & !Ignited))
SPEC AG (CruiseControl = Cruise -> AX (PIgnited -> CruiseControl = Off))
SPEC AG (CruiseControl = Cruise -> AX (!Ignited -> CruiseControl = Off))
SPEC AG AX (!PToofast & Toofast & PIgnited -> CruiseControl = Inactive)
SPEC AG (CruiseControl = Cruise -> AX (!PToofast & Toofast & PIgnited))
SPEC AG (CruiseControl = Cruise -> AX (!PToofast & Toofast -> CruiseControl = Inactive))
SPEC AG (CruiseControl = Cruise -> AX (!PToofast & PIgnited -> CruiseControl = Inactive))
SPEC AG (CruiseControl = Cruise -> AX (Toofast & PIgnited -> CruiseControl = Inactive))
SPEC AG AX (!PBrake & Brake & (PIgnited & PEngRun & !PToofast) -> CruiseControl = Override)
SPEC AG (CruiseControl = Cruise -> AX (!PBrake & Brake & (PIgnited & PEngRun & !PToofast)))
SPEC AG (CruiseControl = Cruise -> AX (!PBrake & (PIgnited & PEngRun & !PToofast) -> CruiseControl = Override))
SPEC AG (CruiseControl = Cruise -> AX (Brake & (PIgnited & PEngRun & !PToofast) -> CruiseControl = Override))
SPEC AG (CruiseControl = Cruise -> AX (!PBrake & Brake & (PIgnited & PEngRun) -> CruiseControl = Override))
SPEC AG (CruiseControl = Cruise -> AX (!PBrake & Brake & (PIgnited & !PToofast) -> CruiseControl = Override))
SPEC AG (CruiseControl = Cruise -> AX (!PBrake & Brake & (PEngRun & !PToofast) -> CruiseControl = Override))
SPEC AG AX (!PEnum1 = Deactivate & Enum1 = Deactivate & (PIgnited & PEngRun & !PToofast) -> CruiseControl = Override)
SPEC AG (CruiseControl = Cruise -> AX (!PEnum1 = Deactivate & Enum1 = Deactivate & (PIgnited & PEngRun & !PToofast)))
SPEC AG (CruiseControl = Cruise -> AX (!PEnum1 = Deactivate & (PIgnited & PEngRun & !PToofast) -> CruiseControl = Override))
SPEC AG (CruiseControl = Cruise -> AX (Enum1 = Deactivate & (PIgnited & PEngRun & !PToofast) -> CruiseControl = Override))
SPEC AG (CruiseControl = Cruise -> AX (!PEnum1 = Deactivate & Enum1 = Deactivate & (PIgnited & PEngRun) -> CruiseControl = Override))
SPEC AG (CruiseControl = Cruise -> AX (!PEnum1 = Deactivate & Enum1 = Deactivate & (PIgnited & !PToofast) -> CruiseControl = Override))
SPEC AG (CruiseControl = Cruise -> AX (!PEnum1 = Deactivate & Enum1 = Deactivate & (PEngRun & !PToofast) -> CruiseControl = Override))
SPEC AG AX (PIgnited & !Ignited -> CruiseControl = Off)
SPEC AG (CruiseControl = Override -> AX (PIgnited & !Ignited))
SPEC AG (CruiseControl = Override -> AX (PIgnited -> CruiseControl = Off))
SPEC AG (CruiseControl = Override -> AX (!Ignited -> CruiseControl = Off))
SPEC AG AX (!PEnum1 = Activate & Enum1 = Activate & (PIgnited & PEngRun & !PToofast & !PBrake) -> CruiseControl = Cruise)
SPEC AG (CruiseControl = Override -> AX (!PEnum1 = Activate & Enum1 = Activate & (PIgnited & PEngRun & !PToofast & !PBrake)))
SPEC AG (CruiseControl = Override -> AX (!PEnum1 = Activate & (PIgnited & PEngRun & !PToofast & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Override -> AX (Enum1 = Activate & (PIgnited & PEngRun & !PToofast & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Override -> AX (!PEnum1 = Activate & Enum1 = Activate & (PIgnited & PEngRun & !PToofast) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Override -> AX (!PEnum1 = Activate & Enum1 = Activate & (PIgnited & PEngRun & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Override -> AX (!PEnum1 = Activate & Enum1 = Activate & (PIgnited & !PToofast & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Override -> AX (!PEnum1 = Activate & Enum1 = Activate & (PEngRun & !PToofast & !PBrake) -> CruiseControl = Cruise))
SPEC AG AX (!PEnum1 = Resume & Enum1 = Resume & (PIgnited & PEngRun & !PToofast & !PBrake) -> CruiseControl = Cruise)
SPEC AG (CruiseControl = Override -> AX (!PEnum1 = Resume & Enum1 = Resume & (PIgnited & PEngRun & !PToofast & !PBrake)))
SPEC AG (CruiseControl = Override -> AX (!PEnum1 = Resume & (PIgnited & PEngRun & !PToofast & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Override -> AX (Enum1 = Resume & (PIgnited & PEngRun & !PToofast & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Override -> AX (!PEnum1 = Resume & Enum1 = Resume & (PIgnited & PEngRun & !PToofast) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Override -> AX (!PEnum1 = Resume & Enum1 = Resume & (PIgnited & PEngRun & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Override -> AX (!PEnum1 = Resume & Enum1 = Resume & (PIgnited & !PToofast & !PBrake) -> CruiseControl = Cruise))
SPEC AG (CruiseControl = Override -> AX (!PEnum1 = Resume & Enum1 = Resume & (PEngRun & !PToofast & !PBrake) -> CruiseControl = Cruise))
SPEC AG CruiseControl = Off
SPEC AG (!Ignited)
SPEC AG CruiseControl = Inactive
SPEC AG Ignited
SPEC AG (Ignited & EngRun & !Toofast & !Brake & !Enum1 = Deactivate)
SPEC AG (CruiseControl = Cruise -> Ignited & EngRun & !Toofast & !Brake)
SPEC AG (CruiseControl = Cruise -> Ignited & EngRun & !Toofast & !Enum1 = Deactivate)
SPEC AG (CruiseControl = Cruise -> Ignited & EngRun & !Brake & !Enum1 = Deactivate)
SPEC AG (CruiseControl = Cruise -> Ignited & !Toofast & !Brake & !Enum1 = Deactivate)
SPEC AG (CruiseControl = Cruise -> EngRun & !Toofast & !Brake & !Enum1 = Deactivate)
SPEC AG (Ignited & EngRun)
SPEC AG (CruiseControl = Override -> Ignited)
SPEC AG (CruiseControl = Override -> EngRun)
SPEC AG (!Ignited -> CruiseControl = Off)
SPEC AG (Ignited -> CruiseControl = Inactive)