| Hi Will,
you may want to look at Chapter 10.2 of Specifying Systems that discusses a similar issue. In particular, the formula
/\ \E n \in Node : x_arr[n]' = x_arr[n] + 1
/\ UNCHANGED mx
is indeed a legal TLA+ formula, but it is too weak for use in the next-state relation because it does not express any condition about values of x_arr[m]’ for m # n. In fact, it does not even assert that x_arr’ is a function, or what the domain of that function would be.
You can remedy those problems by conjoining a type-correctness invariant plus requiring that the other components are unchanged and write something like
/\ x_arr' \in [Node -> Nat] /\ \E n \in Node : /\ x_arr[n]' = x_arr[n] + 1 /\ \A m \in Node \ {n} : x_arr[m]' = x_arr[m] /\ UNCHANGED mx
but TLC will complain that it cannot enumerate the set, and if you override Nat to a suitably small set, it will still be inefficient. As suggested in the chapter mentioned above, defining the updates using EXCEPT expressions is certainly your best option.
Stephan On 26 Jul 2024, at 21:21, 'William Schultz' via tlaplus <tlaplus@xxxxxxxxxxxxxxxx> wrote:
I am running into an issue related to how to specify the composition between a main, root module with several "child" modules that are used via parameterized instantiations.
My overall goal is to have each instantiated child module be composed asynchronously with (i.e. can interleave with) the root module. I am facing an issue with writing and checking such a specification in practice, though, which can be illustrated with a small example as follows.
Assume we have a root module M, and a helper/child module C, where M and C look something like the following:
---- MODULE M ----
CONSTANT Node
VARIABLE mx
VARIABLE x_arr
Child(s) == INSTANCE C WITH x <- x_arr[s]
M1 == mx' = mx + 2
Init ==
/\ mx = 0
/\ x_arr = [n \in Node |-> 0]
Next ==
\* Root module transition.
\/ /\ M1
/\ UNCHANGED x_arr
\* Child transition.
\/ /\ \E n \in Node : Child(n)!C1
/\ UNCHANGED mx
====
---- MODULE C ----
VARIABLE x
C1 == x' = x + 1
Init == x = 0
Next == C1
====
That is, inside M, we instantiate a set of C modules parameterized over 'CONSTANT Node' e.g. a set of process/node ids. And we define a variable x_arr \in [Node -> Nat] to store the internal variables for each of these instantiated child modules.
The problem, though, is that the transition relation of M as written above doesn't work in practice, since if we apply the substitution as defined for each module C, the underlying _expression_ in the second disjunct of Next looks like
/\ \E n \in Node : x_arr[n]' = x_arr[n] + 1
/\ UNCHANGED mx
which, as far as I understand, is valid TLA+, but isn't something that is handled correctly by TLC when evaluating a transition relation to generate next states, since it won't know how to assign the full value of x_arr.
Currently, I've sort of worked around this by defining a few "wrapper" actions inside M that explicitly wrap the actions of C with updates like
x_arr' = [x_arr EXCEPT ![n] = Child(n)!C1_update]
but I find this isn't ideal, since it requires extra maintenance of these wrapper definitions, and kind of breaks the clean separation between M and C, which is what I was hoping to achieve (i.e. that M only knows about the "interface" of C, which consists of its variables/actions).
I suppose it may also be possible to, for any Child(n) action, define a more general wrapper that explicitly sets all indices x_arr[m], where m # n, as UNCHANGED, and leaves x_arr[n] as unspecified i.e. able to take on any type-correct value. Then, conjoining such a wrapper condition with a Child(n) action would seem to be handled by TLC, since x_arr has been assigned a concrete value. But, this seems potentially inefficient if all type-correct values for x[n] must be generated before being constrained by the Child(n) action that modifies only x[n].
Curious to hear any thoughts on this kind of paradigm and whether there may be better ways to address this.
--
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/7e9b3fb8-cc30-48ff-822b-ba4f53f919ben%40googlegroups.com.
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/566F3286-F87E-4E07-863F-9A2CA78C21B6%40gmail.com.
|