Open
Description
This issue is related to a pull request.
In the NEWEPOCH
rule, we:
- finalise the rewards calculation by forcing the pulser (calling
completeRupd
), and then - call
updateRewards
with the result. Theassert
inupdateRewards
needs to become an STS assertion.
That PR could not address this issue, due to the fact that an STS assertion does not have access to Globals
which is required for completeRupd
to run the pulsing calculation of rewards. In order to be able to solve this problem either the pulser finalisation function completeRupd
should not have to depend on Globals
, or we need to memoize the reward update result in the state to be able to pass it on to the PostCondition
STS assertion.