Model checking a mutually recursive definition of a tree

[Alex Weisberger]

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?

[Andrew Helwer]

Tree is a countably infinite set. The problem is your TypeOK definition. I think TLC tries to evaluate it  by enumerating the Tree set and checking each element to see whether it matches your tree variable's value. I tried overriding this behavior by writing:

RECURSIVE IsRootOfTree(_)
IsRootOfTree(n) ==
    IF n = Leaf
    THEN TRUE
    ELSE
        /\ "value" \in DOMAIN n
        /\ n.value \in Values
        /\ "left" \in DOMAIN n
        /\ IsRootOfTree(n.left)
        /\ "right" \in DOMAIN n
        /\ IsRootOfTree(n.right)

TypeOk == IsRootOfTree(tree)

However this then caused TLC to output a novel (to me) error:

TLC threw an unexpected exception.
This was probably caused by an error in the spec or model.
See the User Output or TLC Console for clues to what happened.
The exception was a java.lang.ClassCastException
: class tlc2.tool.coverage.ActionWrapper cannot be cast to class tlc2.tool.coverage.OpApplNodeWrapper (tlc2.tool.coverage.ActionWrapper and tlc2.tool.coverage.OpApplNodeWrapper are in unnamed module of loader 'app')

I think Hillel Wayne wrote a spec of a linked list at one point which might be useful to you, although I can't find it. Other than that the only method I've thought of to specify recursive data structures is to actually model their allocation & layout in memory.

Andrew

[Andrew Helwer]

I wrote up a spec of a memory-layout-based binary tree here, if you're interested (feel free to use): https://github.com/ahelwer/formal-methods-experiments/blob/master/tla/MemoryTree.tla

I don't claim that it's the best implementation of binary tree logic, but it works for the Add(value) case at least, with some pretty good invariant coverage.

I also opened an issue on github about TLC not being able to handle RECURSIVE definitions in invariants: https://github.com/tlaplus/tlaplus/issues/649

Andrew

[Markus Kuppe]

On 7/26/21 4:31 AM, Andrew Helwer wrote:
> However this then caused TLC to output a novel (to me) error:
>
> TLC threw an unexpected exception.
> This was probably caused by an error in the spec or model.
> See the User Output or TLC Console for clues to what happened.
> The exception was a java.lang.ClassCastException
> : class tlc2.tool.coverage.ActionWrapper cannot be cast to class
> tlc2.tool.coverage.OpApplNodeWrapper (tlc2.tool.coverage.ActionWrapper
> and tlc2.tool.coverage.OpApplNodeWrapper are in unnamed module of loader
> 'app')

This issue [1] has been fixed in the most up-to-date nightly [2].

As a workaround for previous versions of TLC, run TLC without the
-coverage parameter. In the Toolbox, turn off profiling on the "TLC
Options" page of the model editor.

Markus

[1] https://github.com/tlaplus/tlaplus/issues/649
[2] https://nightly.tlapl.us