PlusCal in Alloy

[alcino]

Hi,

@peter.kriens

First question, you think it is a good idea to have Pluscal in Alloy? Assuming yes, is the syntax here proposed to your liking?

In the kind of models I do, I never felt a strong need for such a language, but if others find it useful why not (the actions in many distributed protocols are quite simple to model in normal Electrum). I have not read in detail your proposal for processes (yet), but the syntax you propose for the algorithms looks nice.

@peter.kriens

I also thought, maybe wrongly, that I could place the assert on different places.

I think in PlusCal you can put an assert wherever you want. I don’t see a problem with that.

@peter.kriens

Part of the problem is that I don’t fully ‘feel’ the stuttering steps. Anything I could read to get a better understanding?

Lamport wrote extensively about that. I think that any introductory article about TLA discusses stuttering steps.

@peter.kriens

I am not sure I get this? Isn’t that the consequence that of removing the check for eventually pc=Done ? If the while loop does not terminate, eventually pc=Done can never be true, so the assertion will fail?

I think my explanation was not very good, so I’ll try again In Electrum all behaviours are infinite. Having only stuttering steps when the algorithm terminates might be a bit problematic, because you might exclude from the analysis partial runs that do not reach that point. For example, if for particular values of a and b the algorithm needs 15 steps (loop iterations) to terminate and your scope for the time domain is 10 all runs for those inputs will be excluded from the analysis. Let’s suppose you have an assert inside the while to check for some loop invariant, and lets suppose that for those particular inputs there was a problem and that assert would actually fail after 3 steps. You would not detect this problem because that run would not be considered. If you had stuttering steps, then it would be ok, because Electrum would be able to produce an infinite trace that is a counter-example (it would take the 3 steps and then stutter forever). What I did say wrong is that if the loop does not terminate no infinite runs would exist: in fact if the values of the variables start repeating after some time it could still be possible to have an infinite trace.

@peter.kriens

However, one of the problems I saw is that I cannot handle while (true) {} , and that is a common pattern. So I’ll experiment with this.

This is a good example: you might want to have such kind of algorithms and an assert inside the while.

@peter.kriens

Can you elaborate on why this is impossible in Electrum? I take it as an axiom that TLA can do what Alloy can do? Am I wrong?

I’m not saying its impossible - we have just not figured out a good way to do it. TLA has a different verification technique (explicit state enumeration) that makes it simpler to verify deadlocks. Notice that even the notion of deadlock could a bit strange in Electrum and we would need to come up with a good definition: we don’t have an explicit model of a state machine, namely we don’t have an explicit specification of transitions, so it might be not clear what deadlock means. It just happens that many Electrum specifications look like a specification of a state machine (always (action1 or action2 or ...), where action_1, etc, are specified with formulas involving only relations or primed relations, without other temporal operators). In this case (that btw includes the result of the translation from your PlusCal like language) we could use the same definition of deadlock as in TLA - a deadlock is a state where no actions are enabled, and only stuttering steps can occur. Even in this particular case, due to differences in the underlying verification technique, it is not obvious to me how to check deadlock absence in Electrum. For Electrum specifications that do not fit in this pattern I don’t know if it is clear what deadlock means. If anyone has an idea about how to proceed with this we would be glad to discuss it.

Best,
Alcino