[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[PVS-Help] Error when trying to model-check



Hi,

 

I am trying to model-check ‘reachableA_D’ appearing in the specification below:

 

%---------Begin-----------

 

test  : THEORY

 

  BEGIN

            State: TYPE = {a,b,c,d}

            s,s0,s1: VAR State

 

            Next(s0,s1):bool =

                        (s0=a AND (s1=b OR s1=c))

                        OR (s0=c AND s1=d)

 

            InD(s):bool = s=d

 

            init(s):bool = s=a

 

            reachableA_D: THEOREM init(s) IMPLIES EF(Next,InD)(s)

 

  END test

 

%---------End-----------

 

But I am get the following error:

 

%-----------------

 

reachableA_D : 

 

  |-------

{1}   FORALL (s: State): init(s) IMPLIES EF(Next, InD)(s)

 

Rule? (model-check)

 

Type-error in KERNEL::OBJECT-NOT-TYPE-ERROR-HANDLER:

   "b3" is not of type (UNSIGNED-BYTE 32)

   [Condition of type TYPE-ERROR]

 

Restarts:

  0: [ABORT] Return to Top-Level.

 

Debug  (type H for help)

 

(MU_MK_REL_VAR_DCL #<unavailable-arg>)

0]

 

%-----------------

 

Please advice.

Many thanks in advance.

 

Ankit Goel

Graduate Student

School of Computing

National University of Singapore