I want to instantiate a module multiple times in a TLA specification, e.g., in a communication network consisting of multiple but identical nodes, executing the same protocol.
My problem is that I haven't found a way to do this without having to adapt the composition model (the network in the example above) for each change in the number of nodes.
The following example shows the problem from above on a more abstract level:
This model encapsulates a single variable v which is initialized to 1 and allows to change that variable from 0 to 1.
---- MODULE single ----
VARIABLE v
Init == v = 0
Next == v = 0 /\ v' = 1
Spec == Init /\ [][Next]_v
====
The following model instantiates this module two times:
---- MODULE concurrent_a ----
VARIABLES
a, b
A == INSTANCE single WITH v <- a
B == INSTANCE single WITH v <- b
Init == A!Init /\ B!Init
Next == [A!Next]_a /\ [B!Next]_b
Spec == Init /\ [][Next]_<<a, b>>
====
This is working as expected, both a and b can now be changed from 0 to 1 independently.
However, I want to generalize this to be able to instantiate multiple times without having to adapt the actions every time I change something. I tried the following:
---- MODULE concurrent ----
VARIABLES
a, b, c, d
vars == <<a, b, c, d>> \* For usage in the next-state relation
N(v) == INSTANCE single
Init ==
/\ N(a)!Init
/\ N(b)!Init
/\ N(c)!Init
/\ N(d)!Init
Next ==
/\ [N(a)!Next]_a
/\ [N(b)!Next]_b
/\ [N(c)!Next]_c
/\ [N(d)!Next]_d
Spec == Init /\ [][Next]_vars
====
This is still working, but shows my problem. With each new instance, I have to change the overall specification, i.e., the Init and Next actions.
I want to express this in a way similar to this module:
---- MODULE concurrent_err ----
VARIABLES
a, b, c, d
vars == <<a, b, c, d>> \* For usage in the next-state relation
Vars == {a, b, c, d} \* For quantification
N(v) == INSTANCE single
Init == \A v \in Vars: N(v)!Init
Next == \A v \in Vars: [N(v)!Next]_v
Spec == Init /\ [][Next]_Vars
====
TLC throws an error trying to compute the initial states:
[...]
Computing initial states...
Error: In evaluation, the identifier a is either undefined or not an operator.
line 6, col 10 to line 6, col 10 of module concurrent
Error: The error occurred when TLC was evaluating the nested
expressions at the following positions:
0. Line 10, column 9 to line 10, column 32 in concurrent
1. Line 10, column 18 to line 10, column 21 in concurrent
2. Line 6, column 9 to line 6, column 20 in concurrent
3. Line 6, column 10 to line 6, column 10 in concurrent
0 states generated, 0 distinct states found, 0 states left on queue.
This relates to the evaluation of v \in Vars in the Init (and corresponding Next) Action. However, a similar evaluation(?) takes place in the definition of [Next]_vars. I suppose this corresponds to a syntactical replacement rather than an actual evaluation, and I expected the same to be true for the first case, but this doesn't seem to be true.
Is there a way to express the semantics of module concurrent in a form similar to concurrent_err?
