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

["Adrian Balij" <adrian.balij@xxxxxxxxx>]

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



essentially what i have is an function that describes whether an event or occured, the function takes a time input and outputs a bool

in my table, I am trying to get whether an event occured in the previous time unit (currentTime-1).

Any ideas? Thanks for your help


-- 
Thanks,

Adrian