# <pre>
# SCR style Cruise Control specification
# March 6, 1998

# I added explanatory comments.  They go from '#' to the end of line.
#	Paul Black 6 April 1998

MONITORED-COND			# "input" variables
  Ignited EngRun Toofast Brake Activate Deactivate Resume 
MODECLASS CruiseControl		# transition table
  INITIAL Off (!Ignited)
  MODE Off
    Inactive @T(Ignited)	# New state is Inactive if there is
				# a transition to Ignited True
  MODE Inactive
    Off @F(Ignited) 
    Cruise @T(Activate) WHEN [EngRun & ~Toofast & ~Brake]  
  MODE Cruise
    Off @F(Ignited) 
    Inactive @F(EngRun) WHEN [Ignited]  
    Inactive @T(Toofast) WHEN [Ignited]  
    Override @T(Brake) WHEN [Ignited & EngRun & ~Toofast]  
    Override @T(Deactivate) WHEN [Ignited & EngRun & ~Toofast]  
  MODE Override
    Off @F(Ignited) 
    Inactive @F(EngRun) WHEN [Ignited]  
    Cruise @T(Activate) WHEN [Ignited & EngRun & ~Toofast & ~Brake]  
    Cruise @T(Resume) WHEN [Ignited & EngRun & ~Toofast & ~Brake]  

ASSUMPTIONS			# the input should never violate these
  EngRun -> Ignited
  Toofast -> EngRun
  Activate / Deactivate / Resume

PROPERTIES			# these are the specs.  E is there 'Exists.'
				# A is 'for All.'  X is 'neXt state.'
  # these are safety invariants
  AG(Off -> ~Ignited) 
  AG(Inactive -> Ignited) 
  AG(Cruise -> (Ignited & EngRun & ~Toofast & ~Brake & ~Deactivate))
  AG(Override -> (Ignited & EngRun))
  # should always be able to reach every state
  EF(Off)
  EF(Inactive)
  EF(Cruise)
  EF(Override)
  # the following are a restatement of the transition table above.
  #	They come in pairs.  The first one (EF) states that the event
  #	can happen.  The second one (AG) repeats the transition.
  EF(Off & EX(@T(Ignited)))
  AG(Off -> AX(@T(Ignited) -> Inactive))
  EF(Inactive & EX(@F(Ignited)))
  AG(Inactive -> AX(@F(Ignited) -> Off))
  EF(Inactive & EX(@T(Activate) & WHEN [Ignited & EngRun & ~Toofast & ~Brake]))
  AG(Inactive -> AX((@T(Activate) & WHEN [Ignited & EngRun & ~Toofast & ~Brake]) -> Cruise))
  EF(Cruise & EX(@F(Ignited)))
  AG(Cruise -> AX(@F(Ignited) -> Off))
  EF(Cruise & EX(@F(EngRun) & WHEN [Ignited]))
  AG(Cruise -> AX((@F(EngRun) & WHEN [Ignited]) -> Inactive))
  EF(Cruise & EX(@T(Toofast) & WHEN [Ignited]))
  AG(Cruise -> AX((@T(Toofast) & WHEN [Ignited]) -> Inactive))
  EF(Cruise & EX(@T(Brake) & WHEN [Ignited & EngRun & ~Toofast]))
  AG(Cruise -> AX((@T(Brake) & WHEN [Ignited & EngRun & ~Toofast]) -> Override))
  EF(Cruise & EX(@T(Deactivate) & WHEN [Ignited & EngRun & ~Toofast]))
  AG(Cruise -> AX((@T(Deactivate) & WHEN [Ignited & EngRun & ~Toofast]) -> Override))
  EF(Override & EX(@F(Ignited)))
  AG(Override -> AX(@F(Ignited) -> Off))
  EF(Override & EX(@F(EngRun) & WHEN [Ignited]))
  AG(Override -> AX((@F(EngRun) & WHEN [Ignited]) -> Inactive))
  EF(Override & EX(@T(Activate) & WHEN [Ignited & EngRun & ~Toofast & ~Brake])) 
  AG(Override -> AX((@T(Activate) & WHEN [Ignited & EngRun & ~Toofast & ~Brake]) -> Cruise))
  EF(Override & EX(@T(Resume) & WHEN [Ignited & EngRun & ~Toofast & ~Brake]))
  AG(Override -> AX((@T(Resume) & WHEN [Ignited & EngRun & ~Toofast & ~Brake]) -> Cruise))

# end
# </pre>