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

variables

bcNode \in CN \union FN,

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

Stephan