Re: [isabelle] Error in automaton example



On Mon, 11 Sep 2006, Gabriele Pozzani wrote:

> 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 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





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