Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Automaton example

view this post on Zulip Email Gateway (Aug 18 2022 at 09:35):

From: Gabriele Pozzani <gabriele.pozzani@gmail.com>
I started to study the representation of input/output automata in Isabelle.
I opened the example Cockpit.thy in the directory HOLCF/IOA/Modelcheck and I
started the analysis. Isabelle loads MuIOAOracle but when reach the keyword
"automaton" it stops with the error message:

*** Outer syntax error: command expected,
*** but identifier "automaton" was found

Why?
I read the article about IOA but I didn't understand where is the problem.
Can anyone help me?

Thanks
Gabriele

view this post on Zulip Email Gateway (Aug 18 2022 at 09:36):

From: Alexander Krauss <krauss@in.tum.de>
Hi Gabriele,

*** Outer syntax error: command expected,
*** but identifier "automaton" was found

You are using the wrong keyword file for ProofGeneral. In order to know
what are keywords, ProofGeneral uses a keyword file which is generated
by Isabelle and is located in "$ISABELLE_HOME/etc/isar-keywords.el". In
fact, the standard keyword file should already know about IOA...

What version are you using?

You can re-generate the keyword file by issuing the command

ML {* ProofGeneral.write_keywords "" *}

after you have loaded all the theories you are using.
Then copy the created file "isar-keywords.el" to the above location.

Hope that helps,
Alex

view this post on Zulip Email Gateway (Aug 18 2022 at 09:38):

From: Makarius <makarius@sketis.net>
You need to use the proper logic image, i.e. IOA (which is derived from
HOLCF). You can produce it like this:

Isabelle2005/build -m IOA HOLCF

Then run Isabelle with -l IOA option, or select the image manually from
the ProofGeneral menu.

Makarius

view this post on Zulip Email Gateway (Aug 18 2022 at 09:39):

From: Gabriele Pozzani <gabriele.pozzani@gmail.com>
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?

Thanks for the collaboration.

Gabriele

view this post on Zulip Email Gateway (Aug 18 2022 at 09:44):

From: Makarius <makarius@sketis.net>
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
Test.thy

Last updated: May 03 2024 at 12:27 UTC