Paramaterized Instantiation and Universal Quantification

[Adam Shimi]

Hi everyone.

For a TLA+ project I'm working on, I wanted to use Parameterized instantiation in order to have a "general" module, that is to say a module where I would only have to change the variables names and a few other lines, and it would work for any number of variables.
In order to do so, I added a constant operator in the form of a set containing every variable, and made my state transitions iterate through this set by universal quantification, calling the instantiation state transition with each variable as a parameter in turn.

But when I did so, TLC never generated a state after the initial one.

What I gathered from playing with PrintT is that, somewhere along the line, TLC defined the next-state value of my variable within the universal quantification. Thus, when I tried to define it in the state transition of the parameterized instantiation, TLC interpreted it as a test for equality and evaluated it at FALSE.

I still do not know where it does so. I guess it must be caused by my definition of a set of variables, that is a constant operator. Yet I did not manage to find a clear cut answer in Specifying Systems.

This is the reason underlying this message : to ask an explanation to someone better at TLA+ and TLC than me. For if I must abandon this idea, I at least want to understand why I have to.

But my specification was way to big to send here, so I wrote a little toy example where the error still emerges.
In it, the specification supermodule has two variables, which are both initialized at 0. The only transition is one where both variables are changed to 1 (through the mix of parameterized instantiation and universal quantification explained above). And the only temporal property to check is that both variables will eventually be equal to 1.

The issue mentionned above still appears in this toy example : TLC only generates the initial state.

Does someone have a precise explanation of this behavior ?

Thanks in advance, and have a good day.

Adam Shimi

[Stephan Merz]

Hi,

the key elements of your toy module are

VARIABLES s0, s1

Mod(s) == INSTANCE mod WITH s <- s

All == {s0, s1}

t == \A s \in All : Mod(s)!Add

where in mod we have

Add == s' = 1

Let's assume that TLC attempts to evaluate action t in state z where both variables s0 and s1 have value 0. Then All = {0} and the definition of t boils down to Mod(0)!Add, which in turn evaluates to 0' = 1, which is FALSE, so there is no successor state of z for action t.

It seems to me that your mental picture is a semantics of "call by name" where set All would contain references to the variables s0 and s1 rather than the values of these variables.

Back to your original intention: the canonical way to obtain a generic specification is to use functions (arrays). More precisely, a single variable evaluates to a function, and each "array cell" corresponds to the individual variables that you have in mind. Concretely,

CONSTANT Dom

VARIABLE s

\** initialize the entire array

Init == s = [d \in Dom |-> 0]

\** update certain elements of the array

trans(D) == s' = [d \in Dom |-> IF d \in D THEN 1 ELSE s[d]]

\** next-state relation: update some array elements

Next == \E D \in SUBSET Dom : trans(D)

In practice, of course, both the update and the conditions on the choice of the subset to update would be more complicated.

Note in particular that the action trans has to define the new value of the overall function and that it is not enough to write, say,

trans(D) == 

  /\ \A d \in D : s'[d] = 1

  /\ \A d \in Dom \ D : UNCHANGED s[d]

because this does not uniquely define the domain of s' (for example, it could be a superset of the original domain). In fact, the above definition does not even specify that s' is a function. In principle, you could write something like

trans(D) == 

  /\ s' \in [Dom -> 0 .. 10]

  /\ \A d \in D : s'[d] = 1

  /\ \A d \in Dom \ D : UNCHANGED s[d]

but TLC is very inefficient in evaluating this definition because it would actually enumerate all possible functions and remove those that do not satisfy the formula in order to compute the only possible successor state.

Hope this helps,

Stephan

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

[Adam Shimi]

Hi Stephan,

First, thanks a lot for your prompt and accurate answer !

You are completely right : my mental model of All was based on a call-by-name semantics instead of the obvious call-by-value.

As for the canonical encoding of general specification, I indeed thought about that (or Sequences, but these are only functions from Nat to my values' type). But the transitions of my actual specification are not atomic with respect to all my s0, s1, etc variables. Thus, I cannot use it for my purpose.

I guess not, but I am curious : is there some call-by-name mecanisms in TLA+ ?

[Stephan Merz]

Hi Adam,

> As for the canonical encoding of general specification, I indeed thought about that (or Sequences, but these are only functions from Nat to my values' type). But the transitions of my actual specification are not atomic with respect to all my s0, s1, etc variables. Thus, I cannot use it for my purpose.

not sure I understand this: the actions of a TLA+ specifications must correspond to atomic transitions. But I leave it to you to figure out if you can adapt the function-based approach or not.

> I guess not, but I am curious : is there some call-by-name mecanisms in TLA+ ?

No, the point of TLA+ is to be declarative (what Leslie calls "simple math"). Programming language semantics are much more complicated than that. Of course, you can model references explicitly – just like you'd model memory cells – but your spec will become much more complicated as well.

Best regards,
Stephan

[Leslie Lamport]

TLC does not handle parametrized instantiation.  See

 

           http://lamport.azurewebsites.net/tla/current-tools.pdf

[Adam Shimi]

Hi again,

Stephan :

In fact, I did not read carefully enough your previous answer : I thought you could only define the next-state value of a function by specifying all the function in one declaration (hence my comment about the atomic part). Since it is apparently possible to define values of the function one by one (as long as TLC knows the domain and all the value of the function in the domain, before the end of the next-state computation), I can probably use it. Thanks again for the tip !

Also, thanks for the answer to my other question.

Leslie :

Hum, but my toy example (with t's definition replaced by the one in the comment) actually use parameterized instantiation, and yet TLC behave exactly as it should (generates the good states and checks the temporal property). Is it because my example is so ridiculously simple ?

Also, is there a conceptual reason why parameterized instantiation are not handled (meaning is it conceptually hard to find an algorithm to do so) or is it simply a feature missing by lack of time and manpower ?

Thanks in advance.

Adam

[Adam Shimi]

Hi again,

Sorry to keep bothering you, but I would really like to know "how much" of parameterized instanciation is not implemented in TLC.

Because TLASany let me write such instantiations, and in all my tests (the toy example above as well as the actual speficification, which now works thanks to Stephan's idea), TLC actually model check my specification correctly.

One possibility I thought about is that TLC would conflate the variables if the same instanciation is used with different ones, and somehow mess with the result. Is it the case ?

Thanks in advance and have a good day.

Adam

[Leslie Lamport]

A little experimentation suggests that TLC cannot perform the substitution required for parametrized instantiation in expressions involving subscripts--that is, expressions of the form [A]_v, <<A>>_v, WF_v(A), and SF_v(A).  Checking and possibly fixing this problem have been added to our (rather long) list of things to do.  Any further information that anyone can provide about when parametrized instantiation does and doesn't work would be helpful.

Leslie