[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Next-state involving existential quantifier using PlusCal?


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