src/HOLCF/IOA/Modelcheck/Cockpit.thy

added translation from IOA to mucalculus and corresponding modelchecker examples;

Cockpit = MuIOAOracle + 

datatype ('a)action = Alarm 'a | Info 'a | Ack 'a
datatype event = None | PonR | Eng | Fue

(* this cockpit automaton is a deeply simplified version of
the control component of a helicopter alarm system
considered in a study of ESG.
Some properties will be proved by using model checker mucke *)
automaton cockpit =
signature
actions (event)action
inputs "Alarm a"
outputs "Ack a","Info a"
states
	APonR_incl :: bool
	info :: event
initially "info=None & ~APonR_incl"
transitions
"Alarm a"
	post info:="if (a=None) then info else a",
 	     APonR_incl:="if (a=PonR) then True else APonR_incl"
"Info a"
	pre "(a=info)"
"Ack a"
	pre "(a=PonR --> APonR_incl) & (a=None --> ~APonR_incl)"
	post info:="None",APonR_incl:="if (a=PonR) then False else APonR_incl"

automaton cockpit_hide = hide "Info a" in cockpit

(* following automatons express the properties to be proved, see Cockpit.ML *)
automaton Al_before_Ack =
signature
actions (event)action
inputs "Alarm a"
outputs "Ack a"
states
	APonR_incl :: bool
initially "~APonR_incl"
transitions
"Alarm a"
	post APonR_incl:="if (a=PonR) then True else APonR_incl"
"Ack a"
	pre "(a=PonR --> APonR_incl)"
	post APonR_incl:="if (a=PonR) then False else APonR_incl"

automaton Info_while_Al =
signature
actions (event)action
inputs "Alarm a"
outputs "Ack a","Info i"
states
	info_at_Pon :: bool
initially "~info_at_Pon"
transitions
"Alarm a"
post
info_at_Pon:="if (a=PonR) then True else (if (a=None) then info_at_Pon else False)"
"Info a"
	pre "(a=PonR) --> info_at_Pon"
"Ack a"
	post info_at_Pon:="False"

automaton Info_before_Al =
signature
actions (event)action
inputs "Alarm a"
outputs "Ack a","Info i"
states
	info_at_None :: bool
initially "info_at_None"
transitions
"Alarm a"
	post info_at_None:="if (a=None) then info_at_None else False"
"Info a"
	pre "(a=None) --> info_at_None"
"Ack a"
	post info_at_None:="True"

end