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