[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

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

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 ||

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