Next-state involving existential quantifier using PlusCal?

[Elliott Jin]

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

[Leslie Lamport]

with (value \in Values \cup {Deleted})

  { db_value := value }

[Elliott Jin]

Thanks, this worked perfectly!