[tlaplus] Model checking a mutually recursive definition of a tree

[Alex Weisberger <alex.m.weisberger@xxxxxxxxx>]

Consider the following spec of a tree (extremely simplified, with only two possible node values):

CONSTANTS V1, V2, Leaf

VARIABLES tree

Values == {V1, V2}

RECURSIVE Tree

RECURSIVE Nodes

Tree == {Leaf} \union Nodes

Nodes == [value: Values, left: Tree, right: Tree]

TypeOk == tree \in Tree

Init == tree = [

  value |-> V1, 

  left |-> [

    value |-> V2,

    left |-> Leaf,

    right |-> Leaf

  ],

  right |-> Leaf

]  

Next == tree' = Leaf

This is obviously a trivial example (just two predefined states with a single transition), but I'm using it build up to reasoning about trees more. This fails when model checking in TLC with the following error:

"This was a Java StackOverflowError. It was probably the result
of an incorrect recursive function definition that caused TLC to enter
an infinite loop when trying to compute the function or its application
to an element in its putative domain.
While working on the initial state:
tree = [ value |-> V1,
  left |-> [value |-> V2, left |-> Leaf, right |-> Leaf],
  right |-> Leaf ]


The error occurred when TLC was evaluating the nested
expressions at the following positions:
The error call stack is empty."

I didn't know how TLC would handle mutually recursive definitions such as the above Tree definition, but I also don't exactly understand why it doesn't handle it. I could go with defining a Tree as a Graph, and use a similar definition to what is listed in Specifying Systems, but I thought this was an interesting example to ask about.

Does anyone have any insight into how to make a definition like this model-checkable?

-- 
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/2bd71d8b-2efe-4fb8-b568-6eff04756906n%40googlegroups.com.