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

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


This little question for help follows a previous message of an abstraction

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,