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

*From*: Srikumar Subramanian <srikumar.subramanian@xxxxxxxxxxxx>*Date*: Mon, 7 Dec 2020 21:19:28 -0800 (PST)*References*: <cac57bb6-3d36-433e-a1f9-b3747211fe56n@googlegroups.com> <DCC08488-5FEC-4E15-A19C-C1749E2B3F53@gmail.com>

I guess you meant this? -

edges_stack \in Seq(**UNION** {[X -> Nodes] : X \in **SUBSET **Labels})

or perhaps -

edges_stack \in Seq(**UNION** {[X -> Nodes] : X \in {1..n : n \in Labels}})

On Tuesday, December 8, 2020 at 12:01:26 AM UTC+5:30 Stephan Merz wrote:

Your type invariant states that edges_stack is a sequence of functions that associate nodes to subsets of labels. So, given any subset of labels ({}, {1}, ...), the function should return a node. This is not what << <<"A">> >> does: the domain of <<"A">> is just {1}, as you say.Perhaps you meannode_stack \in Seq(UNION {X -> Nodes : X \in SUBSET Labels})which would allow each function to have a subset of Labels as domain.StephanOn 7 Dec 2020, at 19:14, Tim Leonard <t...@xxxxxxxxxxxxxx> wrote:I'm starting to use the TLA+ toolkit after a decades-long hiatus in my use of TLA+ and TLC, and am struggling with the basics. My spec's type invariant is failing on the initial state, and I don't see why. Here are the spec, the model configuration, and the error:--------------------------------------------------------------------------------(* The relevant part of the spec. *)--------------------------------------------------------------------------------CONSTANT Nodes,Labels,StartNodesVARIABLE node_stack,edges_stackInit == /\ node_stack = EMPTY/\ edges_stack = Push( EMPTY, StartNodes )TypeOK == /\ node_stack \in Seq(Nodes)/\ edges_stack \in Seq([SUBSET(Labels) -> Nodes])--------------------------------------------------------------------------------(* The relevant part of the model configuration. *)--------------------------------------------------------------------------------Nodes <- { "A", "B", "C", "D", "E", "F" }Labels <- 1..Cardinality(Nodes)StartNodes <- << "A" >>--------------------------------------------------------------------------------(* The error. *)--------------------------------------------------------------------------------Invariant TypeOK is violated by the initial state:/\ edges_stack = <<<<"A">>>>/\ node_stack = <<>>I assume that node_stack is satisfying the type invariant, so the problem iswith edges_stack. As I read it, its initial value is a sequence of length one,with the only element being a function with a domain of { 1 } that maps 1 to "A".I thought that would also satisfy the type invariant. What am I misunderstanding?--

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/cac57bb6-3d36-433e-a1f9-b3747211fe56n%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/55e16139-6401-44d1-9b21-e4c1e3d694e2n%40googlegroups.com.

**Follow-Ups**:**Re: [tlaplus] Initial state doesn't satisfy type invariant***From:*Tim Leonard

**References**:**[tlaplus] Initial state doesn't satisfy type invariant***From:*Tim Leonard

**Re: [tlaplus] Initial state doesn't satisfy type invariant***From:*Stephan Merz

- Prev by Date:
**Re: [tlaplus] Initial state doesn't satisfy type invariant** - Next by Date:
**Re: [tlaplus] Initial state doesn't satisfy type invariant** - Previous by thread:
**Re: [tlaplus] Initial state doesn't satisfy type invariant** - Next by thread:
**Re: [tlaplus] Initial state doesn't satisfy type invariant** - Index(es):