You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
and I want to refer to the before value of one of the items of the sequence in a post condition. Here's a simple example:
update:(nat)==>()
update(n) ==
(
counts(n):=counts(n)+1;
...
)
pre n in set inds counts
post counts(n) = counts~(n) + 1
This goes through the syntax/type checker fine, but when the operation is called by the interpreter it has an error message:
"Error 4034: Name 'counts~' not in scope in 'H:\Compass\CML\workspace\T243-timing\T243v2.cml' at line 99:19 at in 'H:\Compass\CML\workspace\T243-timing\T243v2.cml' at line 99:19".
I believe this is the correct syntax and there I have no such issue with doing the same thing with a variable of type nat.
The text was updated successfully, but these errors were encountered:
lausdahl
changed the title
Using ~ to refer to before value of a sequence gives error message
Interpreter: Using ~ to refer to before value of a sequence gives error message
Aug 22, 2014
I have a state variable:
and I want to refer to the before value of one of the items of the sequence in a post condition. Here's a simple example:
This goes through the syntax/type checker fine, but when the operation is called by the interpreter it has an error message:
I believe this is the correct syntax and there I have no such issue with doing the same thing with a variable of type nat.
The text was updated successfully, but these errors were encountered: