[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: "'William Schultz' via tlaplus" <tlaplus@xxxxxxxxxxxxxxxx>*Date*: Tue, 20 Aug 2024 12:02:51 -0700 (PDT)*References*: <7e9b3fb8-cc30-48ff-822b-ba4f53f919ben@googlegroups.com> <CAJ-b8swT_Bsu4BEqtyL4cLa0ybBVG1=SD4-egodPC=NfMdLndg@mail.gmail.com> <2d346901-bc67-4ee9-9848-93adbe81d308n@googlegroups.com> <49675E9F-8D7C-46CB-9164-2846C86FA85A@gmail.com>

Stephan,

Yes, based on the thread here (https://github.com/tlaplus/tlaplus/issues/998) it is now clearer to me why DOMAIN x_arr' = Node is not sufficient to constrain x_arr' to be a function even according to pure TLA+ semantics.

I think my point on modularity effectively still stands though. My issue is that I want to use a defined action inside a child module as is, without the need to explicitly extract its postcondition/update _expression_. I feel like the paradigm of writing something like

/\ x_arr' = [x_arr EXCEPT ![n] = @ + 1]

/\ UNCHANGED mx

still doesn't solve this. That is, if one of the child modules defines an action like

C1 == x' = x + 1

there is no way to extract the relevant update _expression_ (x + 1) you need without some kind of other workaround or some manually added definitions. This is what was motivating my desire to write this as something like:

/\ x_arr' \in [Node -> Int]

/\ \E n \in Node :

/\ Child(n)!C1

/\ \A m \in Node \ {n} : x_arr[m]' = x_arr[m]

/\ UNCHANGED mx

On Monday, August 19, 2024 at 4:25:04 AM UTC-4 Stephan Merz wrote:

DOMAIN x_arr' = Node is not enough, even for the TLA+ semantics, not just for TLC. For example, we have no way of knowing what DOMAIN 42 is. You would have to write/\ x_arr' \in [Node -> Int]/\ \E n \in Node :/\ x_arr[n]' = x_arr[n] + 1/\ \A m \in Node \ {n} : x_arr[m]' = x_arr[m]/\ UNCHANGED mxand making TLC support such a formula requires a major change so that it doesn’t try to enumerate all functions first. (Apalache should handle this better.)Moreover, it is not clear to me why you’d consider the above definition more modular than writing/\ x_arr' = [x_arr EXCEPT ![n] = @ + 1]/\ UNCHANGED mxsince you still have to refer to the domain elements other than n.StephanOn 14 Aug 2024, at 19:17, 'William Schultz' via tlaplus <tla...@xxxxxxxxxxxxxxxx> wrote:Thanks for the suggestions. My ultimate goal is to be able to define C's actions independently, such that M can use them without knowing the internals of each action in C. This seems hard to do, though, with the current tooling.I am curious, though, if TLC could be modified to better support this kind of scenario. For example, as stated above, if you give a transition relation like/\ \E n \in Node :/\ x_arr[n]' = x_arr[n] + 1/\ \A m \in Node \ {n} : x_arr[m]' = x_arr[m]/\ UNCHANGED mxto TLC, it currently will not be able to handle it, since it doesn't know x_arr is a function or what its domain is.But, if you instead wrote something like:/\ DOMAIN x_arr' = Node/\ \E n \in Node :/\ x_arr[n]' = x_arr[n] + 1/\ \A m \in Node \ {n} : x_arr[m]' = x_arr[m]/\ UNCHANGED mxit seems like this might be a well-defined _expression_ that TLC could evaluate.There would presumably be some conditions on when such a formula would be handled by TLC, like(1) the domain of the variable is assigned explicitly and(2) every element in the domain is assigned a value (which holds in the above example).and (1) occurs before (2) during evaluation. Otherwise, the function's assigned value would be under-constrained and an error would have to be thrown. Just a thought on how TLC could possibly be made more flexible to handle this type of scenario.On Tuesday, July 30, 2024 at 9:13:13 AM UTC-4 Hillel Wayne wrote:Could you do `\E n \in Node: x_arr' = (n :> x_arr[n+1]) @@ x_arr`?(Man that was hard to type in a phone)On Fri, Jul 26, 2024, 3:29 PM 'William Schultz' via tlaplus <tla...@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 likex_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+u...@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+u...@xxxxxxxxxxxxxxxx.To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/2d346901-bc67-4ee9-9848-93adbe81d308n%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/4e354157-0c97-4893-85cb-8a46652ca1fcn%40googlegroups.com.

**References**:**[tlaplus] Asynchronous Composition with Parameterized Submodules***From:*'William Schultz' via tlaplus

**Re: [tlaplus] Asynchronous Composition with Parameterized Submodules***From:*Hillel Wayne

**Re: [tlaplus] Asynchronous Composition with Parameterized Submodules***From:*'William Schultz' via tlaplus

**Re: [tlaplus] Asynchronous Composition with Parameterized Submodules***From:*Stephan Merz

- Prev by Date:
**Re: [tlaplus] Looking for Module SequencesExt for RFC9293 Example by Markus Kuppe** - Next by Date:
**[tlaplus] Question about temporal formulas definition in book Specify System(version 21-07-04)** - Previous by thread:
**Re: [tlaplus] Asynchronous Composition with Parameterized Submodules** - Next by thread:
**[tlaplus] Looking for Module SequencesExt for RFC9293 Example by Markus Kuppe** - Index(es):