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

Re: [PVS-Help] Expecting an expression. No resolution for vpEeventswith arguments of possible type



Hi Adrian,

The problem is that your second 'vpEevents' has an extra
'e' - I expect you meant to use 'vpEvents'.

Cheers,
Sam

Adrian Balij <adrian.balij@gmail.com> wrote:

> Date: Sat, 3 Nov 2007 20:42:32 -0400
> From: "Adrian Balij" <adrian.balij@gmail.com>
> To: pvs-help@csl.sri.com
> X-SRI-Archive: pvs-help
> Subject: [PVS-Help] Expecting an expression. No resolution for vpEevents
> 	with arguments of possible type
> Sender: pvs-help-bounces+owre=csl.sri.com@csl.sri.com
> 
> 
> Hey everyone
> 
> I am trying to get a hang of PVS and I ran into this problem. I saw another
> user with a similar problem but it did not help me in my situation.
> 
> Here is the error:
> 
> Expecting an expression
> No resolution for vpEevents with arguments of possible types:
>   currentTime - 1 : number_fields.numfield
> 
> Here is my snippet
> 
> 
> pacemakerVVI: Theory
> Begin
> 
> time: Type = nat
> 
> historyOfEvents: Type = [time -> bool]
> 
> VentricularSensed( currentTime: time, vpEvents: historyOfEvents ): bool = Table
> | Not vpEvents(currentTime-1) And vpEvents(currentTime) | True ||
> | vpEevents(currentTime-1) Or Not vpEvents(currentTime) | False ||
> EndTable
> 
> End pacemakerVVI