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

*From*: Alex Weisberger <alex.m.weisberger@xxxxxxxxx>*Date*: Sat, 24 Jul 2021 20:24:02 -0700 (PDT)

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."

"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.

- Prev by Date:
**Re: [tlaplus] Difference between action and temporal formula?** - Next by Date:
**[tlaplus] How to prove RealInv' in the example "BubbleSort" ?** - Previous by thread:
**Re: [tlaplus] Difference between action and temporal formula?** - Next by thread:
**[tlaplus] Re: Model checking a mutually recursive definition of a tree** - Index(es):