Re: [isabelle] Automaton example



On Fri, 1 Sep 2006, Gabriele Pozzani wrote:

> I proved to re-generate the keyword file but nothing change. I opened 
> isar-keywords.el in a text-editor and the keyword automaton is present.
> 
> I re-built the logic image as suggested by Makarius but, again, nothing 
> change.
> 
> Do you have other ideas?

What happens if you load the attached fragment of 
Isabelle2005/src/HOLCF/IOA/Modelcheck/Cockpit.thy like this:

  $ Isabelle2005/bin/isabelle IOA
  ML> use_thy "Test";

Make double sure that this is really the IOA image, not just HOL.


	Makarius
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


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.