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

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

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


On Monday, July 26, 2021 at 7:31:57 AM UTC-4 Andrew Helwer wrote:
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:

IsRootOfTree(n) ==
    IF n = Leaf
        /\ "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.


On Sunday, July 25, 2021 at 12:24:40 AM UTC-4 Alex Weisberger wrote:
Consider the following spec of a tree (extremely simplified, with only two possible node values):



Values == {V1, V2}


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/d1317208-b3fe-4255-9b37-86ed3f624d12n%40googlegroups.com.