Hello,
I'm trying to specify a cache consistency protocol in PlusCal, and I'm having trouble with the step "the writer writes an arbitrary value to the database".
In TLA+, I would simply include the following conjunct:
- \E value \in Values \cup {Deleted} : db_value' = value
Is there a way to generate the same result in PlusCal? I already tried the following:
- \E value \in Values \cup {Deleted} : db_value := value;
- This seems to generate \E' = [\E EXCEPT !value \in Values \cup {Deleted} : db_value = value]
- db_value := CHOOSE value \in Values \cup {Deleted} : TRUE;
- The semantics of using CHOOSE seems to be different than the semantics of using an existential quantifier
Thanks!
-Elliott