Currently, exercise is a composition of acquire' and exercise'.
The first function evaluates predicates within a When or Anytime node and continues unfolding only if predicates are true. It also has the following effects:
replace When pred c with When (TimeGte t) c if pred is non-deterministic and the predicate is True
replace Cond obs x y with the chosen sub-contract
The latter function checks the sub-trees of Or and Anytime nodes against the input election. When there is a match, it replaces the Or / Anytime node with the elected sub-tree and stops the recursion.
As a consequence of this, whenever an election is made, the effects of acquire' are not applied to the elected sub-tree (because the recursion stops). A user might then be forced to invoke lifecycle immediately following a successful election.
There are two alternative approaches:
once an election is made, invoke acquire' on the elected sub-tree. By doing this, the effects of acquire' are applied to the entire tree. There will be no need to call lifecycle immediately after a successful election.
the effectful part of acquire' is ignored in exercise. This would allow for better separation between the effects of lifecycle and exercise. Moreover, it would have the additional property that, in case of an unsuccessful election, the output claim is equal to the input claim.
It is unclear what is most convenient from a usability perspective.
Currently,
exerciseis a composition ofacquire'andexercise'.The first function evaluates predicates within a
WhenorAnytimenode and continues unfolding only if predicates are true. It also has the following effects:When pred cwithWhen (TimeGte t) cifpredis non-deterministic and the predicate isTrueCond obs x ywith the chosen sub-contractThe latter function checks the sub-trees of
OrandAnytimenodes against the input election. When there is a match, it replaces theOr/Anytimenode with the elected sub-tree and stops the recursion.As a consequence of this, whenever an election is made, the effects of
acquire'are not applied to the elected sub-tree (because the recursion stops). A user might then be forced to invokelifecycleimmediately following a successful election.There are two alternative approaches:
once an election is made, invoke
acquire'on the elected sub-tree. By doing this, the effects ofacquire'are applied to the entire tree. There will be no need to calllifecycleimmediately after a successful election.the effectful part of
acquire'is ignored inexercise. This would allow for better separation between the effects oflifecycleandexercise. Moreover, it would have the additional property that, in case of an unsuccessful election, the output claim is equal to the input claim.It is unclear what is most convenient from a usability perspective.