[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[PVS-Help] Expecting an expression. No resolution for vpEeventswith arguments of possible type
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
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 ||
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