Initial state doesn't satisfy type invariant

[Tim Leonard]

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,

          StartNodes

VARIABLE  node_stack,

          edges_stack

Init ==   /\ 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 is

with 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?

[Stephan Merz]

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+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/cac57bb6-3d36-433e-a1f9-b3747211fe56n%40googlegroups.com.

[Srikumar Subramanian]

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}})

?

[Tim Leonard]

Thanks, Stephan; that was a help. The expression you suggested didn’t quite work because it needed square brackets around “X -> Nodes”, and TLC couldn’t enumerate the values, but once you showed me what the problem was, I was able to define and use this constant:

SetsOfLabeledEdges ==

          UNION { [ 1..n -> Nodes ] : n \in 0..Cardinality(Nodes) }

[Tim Leonard]

Yes. The second is what I’m now using.

Thank you for the help.

[Srikumar Subramanian]

It took me some time to see that [(SUBSET A) -> B] is not the same as UNION {[X -> B] : X \in SUBSET A}, so I thought I'd write them out here for clarity in case someone else stumbles on it. Apologies for the verbosity -- though it seems obvious now, I didn't start out that way and had to work through it.

Consider A = 1..2 and B = {"a", "b"} 

Then [(SUBSET A) -> B] is the set of all mappings that assign an element of B to each element of SUBSET(A). For the given A, there are 4 subsets - {}, {1}, {2}, {1,2}. So the cardinality of this set is Cardinality(B) ^ Cardinality(SUBSET A) = 2^4 = 16 .. where each of these subsets of A can be assigned either "a" or "b". Now for the obvious thing - all the functions in this set have the same domain.

{[X -> B] : X \in SUBSET A} is the set of sets of functions whose domain is from SUBSET(A) and whose range is B. So this is -

{ [{} -> B], [{1} -> B], [{2} -> B], [{1,2} -> B] }

The first is {<< >>} (the singleton set with the empty tuple)

The second is {<<"a">>,<<"b">>}

The third is {(2 :> "a"), (2 :> "b")}

The fourth is {<<"a","a">>,<<"a","b">>,<<"b","a">>,<<"b","b">>}

The main thing to notice here is that the domains of the functions are all not the same.

Let S1 = [SUBSET(A) -> B] and S2 = UNION {[X -> B] : X \in SUBSET A},

So the cardinality of S2 is 9 .. whereas for S1 is 16.

{DOMAIN X : X \in S1} = {{{}, {1}, {2}, {1, 2}}} (cardinality 1, since all the functions in S1 have the same domain of cardinality 2^Cardinality(A) = 4)

{DOMAIN X : X \in S2} = {{}, {1}, {2}, {1, 2}} (cardinality 4, since the functions can have one of 4 possible domains, each of which is a subset of A)

Hope this helps somebody like me.

[Stephan Merz]

Perhaps it would make sense to add an operator such as

PartialFunctions(A,B) == UNION {[X ->B] : X \in SUBSET A}

to the CommunityModules, representing functions from some subset of A to B?

Stephan

P.S.: Apologies for the typo (missing function brackets) in my reply to the original question. -s

This mail contains confidential information intended only for the individual(s) named. If you’re not the named addressee, don’t disseminate, distribute or copy this e-mail. Please notify the sender immediately and delete it from your system.If you wish not to receive such e-mails you may reply with text “Unsubscribe”.

--
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...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/cd36eaeb-0e53-40cf-a5c5-0fd5895d3793n%40googlegroups.com.

[Srikumar Subramanian]

I have a feeling (albeit uninformed) that such pure partial functions are likely to be too relaxed for many purposes. Even in this example, we're looking for 1..n where n \in A and not any subset of A. Maybe making it slightly more general would be useful since subset enumeration blows up quickly -

PartialFunctions(Domains, Codomain) == UNION {[X -> Codomain] : X \in Domains}

which would be used as PartialFunctions(SUBSET A, B) for the full set of partial functions .. or in this case PartialFunctions({1..n : n \in Labels}, Nodes) where the domains are way more limited. .. but then now PartialFunctions does more than just make sets of partial functions :)

.. and the expression itself reads fairly clear to me now!

-Srikumar

[Tim Leonard]

An update resulting from experience: I was able to define a set of partial functions as I hoped, but found that in non-trivial models, the cardinality of sets of partial functions quickly exceeded the size that TLC was willing to enumerate. Instead, I wound up using this as a type constraint to achieve the same goal while keeping TLC happy:

CONSTANT
  Nodes,                                \* The set of nodes in the graph.
  Labels,                               \* The set of edge labels.
  EdgesOf,                              \* The labeled out edges of each node.
  StartEdges,                           \* The labeled starting points.
  IsGoal                                \* Whether a node is a goal node.

ConstantTypeOK ==
  /\ Nodes # {}
  /\ DOMAIN(EdgesOf) = Nodes
  /\ \A node \in Nodes :
        \A label \in DOMAIN(EdgesOf[node]) :
           /\ label \in Labels
           /\ EdgesOf[node][label] \in Nodes
  /\ \A label \in DOMAIN(StartEdges) :
        /\ label \in Labels
        /\ StartEdges[label] \in Nodes
  /\ DOMAIN(StartEdges) # {}
  /\ IsGoal \in [Nodes -> BOOLEAN]