Re: [isabelle] I/O automata syntax in Isabelle 2011
On Tue, 1 Feb 2011, Giuliano Losa wrote:
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?
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.)
This archive was generated by a fusion of
Pipermail (Mailman edition) and