theory Test
imports IOA
begin

datatype 'a action = Alarm 'a | Info 'a | Ack 'a
datatype event = NONE | PonR | Eng | Fue

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_action "Info a" in cockpit

end