Re: [tlaplus] pluscal: with vs local variable - change in distinct states for action

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.

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

--
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/fdfec940-dec1-4b79-a2f2-72350ea38310n%40googlegroups.com.