pluscal: with vs local variable - change in distinct states for action

[thisismy...@gmail.com]

Hello Folks

I am using pluscal for writing a spec. If i create a local variable X and then update a global variable Y based on it, i see 1000 distinct states for that action. However, if i use `with` in action for X, then i see 0 distinct states.

I added a assert in `with` case to be sure that Y is changing in some cases as expected.

Is this a cause for concern ?

If not, does this mean that for this action, in 0 distinct case, those states were already seen by TLC ?

E.g.

> 0 Distinct states for DeleteX:

process X = "X"
begin DeleteX:
    while TRUE do
        with X = SelectSeq(gX, isY);
            beforeLen = Len(gY)
            do
            Y := SelectSeq(Y, LAMBDA p: ~YE(p, someCheck));
            assert beforeLen = Len(Y)
        end with;
    end while;
end process;

VS
> Over 1k distinct states for DeleteX:
process X = "X"
variable localX = <<>>
begin DeleteX:
    while TRUE do
    localX := SelectSeq(gX, isY);
        Y := SelectSeq(Y, LAMBDA p: ~YE(p, someCheck));
        end with;
    end while;
end process;

Thanks

Ashish

[Hillel Wayne]

Hi Ashish,

Could you please provide a complete spec? It's hard to know what the issue is without being able to run it for myself locally.

H

--
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...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/fdfec940-dec1-4b79-a2f2-72350ea38310n%40googlegroups.com.