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

Re: [tlaplus] Converting TLA+ spec to PlusCal


TLA+ is more general than PlusCal, and a systematic conversion to PlusCal is unlikely to yield idiomatic results, if it is possible at all: you will probably end up with a single while loop containing all possible actions. It is a bit like the normal form theorem in computability theory.

On 18 Dec 2022, at 13:24, Deividas Bražėnas <deividas.brazenas@xxxxxxxxx> wrote:

Hello all,
I have a TLA+ spec that I'd like to convert to PlusCal, but I'm facing some issues as I don't know how to convert a few parts of the specification.

1. I want to have this predicate as a process, but I'm not sure how to convert this part "\E n \in CN, p \in BOOLEAN :"

UpdatePredicate ==
\E n \in CN, p \in BOOLEAN :
/\ predicate[n] => p \* Only monotonic updates are make the algorithm to terminate.
/\ predicate' = [predicate EXCEPT ![n] = p]
/\ UNCHANGED <<bcNode, bcValue, output, msgs>>

In PlusCal you could represent this as

with (n \in CN, p \in BOOLEAN) {
  await (predicate[n] => p);
  predicate[n] := p

2. I want to specify global variable bcValue in Init based on the set of bcNode

/\ \/ bcNode \in CN /\ bcValue \in Value
    \/ bcNode \in FN /\ bcValue = NotValue

You could perhaps write

  bcNode \in CN \union FN,
  bcValue \in (CASE bcNode \in CN -> Value [] bcNode \in FN -> {NotValue});


You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/EF2E36DD-EB82-4CF4-9383-34E258045780%40gmail.com.