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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Mon, 7 Dec 2020 19:31:20 +0100*References*: <cac57bb6-3d36-433e-a1f9-b3747211fe56n@googlegroups.com>

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 mean node_stack \in Seq(UNION {X -> Nodes : X \in SUBSET Labels}) which would allow each function to have a subset of Labels as domain.
-- 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+unsubscribe@xxxxxxxxxxxxxxxx. To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/DCC08488-5FEC-4E15-A19C-C1749E2B3F53%40gmail.com. |

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

**Re: [tlaplus] Initial state doesn't satisfy type invariant***From:*Srikumar Subramanian

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

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