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

Re: [tlaplus] Potentially confusing behavior of a PlusCal algorithm

Hi Giuliano,

if you look at the TLA+ produced by the PlusCal translator, you'll see that 

B1 == b1

l1 ==
  /\ b1' = TRUE
  /\ B1
  /\ ...

l2 ==
  /\ b2' = TRUE
  /\ b2'
  /\ ...

The translator notices that the await statement in l2 refers to the variable b2 that has been assigned to before, and that the _expression_ b2 should therefore be translated as b2' rather than b2. However, it doesn't notice that B1 involves b1; this would require a finer syntactic analysis than what the translator appears to do.

I had a quick look at the PlusCal manual and did not see a clear description of how exactly expressions are translated. (There is a sentence that says that the expressions in TLA+ are mostly like the ones in the PlusCal algorithm except for some changes, including adding primes.) I do not think that anybody ever attempted to write up a more abstract operational semantics of PlusCal than what is implemented in the PlusCal translator.


On 21 Oct 2015, at 02:21, Giuliano <giulia...@xxxxxxxxx> wrote:

Hello, consider the following algorithm:

--algorithm Algo1 {
    variables b1 = FALSE, b2 = FALSE
    define {
        B1 == b1
    fair process (stuck \in {"stuck"}) {
        l1: b1 := TRUE;
            await B1;
    fair process (notstuck \in {"notstuck"}) {
        l2: b2 := TRUE;
            await b2;

The process "stuck" will never reach the label "Done", while the process "notstuck" will reach it.
This kind of behavior may cause confusion in a more complex algorithm and I could not find any warning about it in the PlusCal user's manual.


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+u...@xxxxxxxxxxxxxxxx.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at http://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.