Email Gateway (Aug 18 2022 at 17:02): Email Gateway (Aug 18 2022 at 17:02):From: Giuliano Losa <giuliano.losa@epfl.ch>
Hello,
the paper "Integrating Theorem Proving and Model Checking in Isabelle/IOA"
presents a nice syntax for describing I/O automata and I would like to use
it.
I found ioa_syn.ML in the Isabelle 2005 distribution but it is not included
in later versions.
What would it take to make it work in Isabelle 2011?
Giuliano
Email Gateway (Aug 18 2022 at 17:05):From: Makarius <makarius@sketis.net>
Essentially a rewrite from scratch, using contemporary Isabelle concepts,
and avoiding program-generated strings that are reparsed as terms.
(This IOA specification mechanism dates back to 1999/2000 and was using
very old layers of the system, that were gradually phased out after
Isabelle2005. The package was never really maintained after its initial
implementation, and in recent years it was not even used/tested in the
distribution, so it started rotting.)
Makarius
Last updated: Apr 24 2024 at 20:16 UTC