Email Gateway (Aug 18 2022 at 09:38): Email Gateway (Aug 18 2022 at 09:38):From: Gabriele Pozzani <gabriele.pozzani@gmail.com>
Dear all,
I have opened and analyzed the Cockpit example about IOA but when Isabelle
reaches automaton Al_before_Ack it stops with the follow error
*** Type unification failed
*** Type error in application: Incompatible operand type
*** Operator:
*** (action_case
*** (l(a::event).
*** (True OR
*** ((APonR_incl'::bool) =
*** (if (a = PonR) then True else (APonR_incl::bool)))))) ::
*** (event => bool) => (event => bool) => event action => bool
*** Operand: (l(a::?'a). False) :: ?'a => bool
*** The error(s) above occurred in axiom "Al_before_Ack_trans_def"
*** At command "automaton".
I don't understand where is the problem.
The type unification is internal to this automaton or with the previous
automata?
Similar errors occur with other examples and with a my theory.
Can anyone help me?
Thanks in advance for the help.
Gabriele
Email Gateway (Aug 18 2022 at 09:38):From: Makarius <makarius@sketis.net>
I cannot reproduce this problem. It works for me as follows:
* Start Isabelle2005 with the IOA image
* Issue the following ML code from src/HOLCF/IOA/Modelcheck/ROOT.ML:
ML {*
use "../../../HOL/Modelcheck/mucke_oracle.ML";
with_path "../../../HOL/Modelcheck" time_use_thy "MuIOAOracle";
*}
* Visit src/HOLCF/IOA/Modelcheck/Cockpit.thy and assert the whole
buffer.
Makarius
Last updated: May 03 2024 at 08:18 UTC