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

Re: abstract-and-mc command - what am I doing wrong




Sara:
 The command should be 

(abstract-and-mc "state" "abs_state" (("B1" "lambda s:sem(s) <= 0")
                                      ("B2" "lambda s:sem(s) > 0")))

-Shankar

> From:    Sara Van Langenhove <Sara.VanLangenhove@rug.ac.be>
> Subject: abstract-and-mc command - what am I doing wrong
> Date:    Thu, 27 Mar 2003 15:38:34 +0100 (MET)
> To:      support PVS <pvs-help@csl.sri.com>
> 
> Hey,
> 
> This little question for help follows a previous message of an abstraction
> problem...
> 
> Currently I`m trying to understand the theory about abstractions and the
> use of it in PVS and I therefore use a theory about semaphores (defined as
> an int).
> 
> location: type = {idle, wait, critical}
> state: type = [# pc1,pc2: location, sem:int #]
> abs_state: type = [# pc1,pc2:location, B1,B2:boolean #]
> 
> s,s1,s2: var state
> 
> If I try to proof something I use the rule
> 
> (abstract-and-mc "state" "abs_state" ( "(B1, lambda(s:sem(s) <= 0)"
>                                        "(B2, lambda(s:sem(s) > 0)"))
> 
> but I get the following error:
> 
> "Abstraction map entry (B1, lambda s: sem(s) <= 0) is not well-formed[mu-init]
> 
> I`ve already tried several versions of the last parameter but without any
> success. What am I doing wrong? Can anyone help me?
> 
> Thanks a lot,
> 
> Sara