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

*From*: "'Leander Jehl' via tlaplus" <tlaplus@xxxxxxxxxxxxxxxx>*Date*: Thu, 12 Nov 2020 00:05:34 -0800 (PST)

I have a specification with constant Blocks and a function prev \in [Blocks -> Blocks] that defines a tree.

I would like to define an ancestor relation on that tree and prove statements like reflexivity and transitivity.

If I try to prove NatInductiveDefConclusion, it triggers a bug in TLAPS.

I would be grateful for any tips on how to define the ancestor relation, or how to avoid the bug.

Here is my current definition of the ancestor relation:

Extend(A) == A \cup { <<b,c>> \in Blocks \X Blocks: <<b,prev[c]>> \in A }

A0 == { <<b,c>> \in Blocks \X Blocks: b=c }

ancestors[i \in Nat] == IF i=0 THEN A0

ELSE Extend(ancestors[i-1])

Ancestor(b,c) == /\ height[b] <= height[c]

/\ height[c] - height[b] \in Nat

/\ <<b,c>> \in ancestors[height[c] - height[b]]

My complete tree specification can be found here:

https://github.com/leandernikolaus/hotstuff-ivy/blob/master/Tree.tla

Thanks,

Leander

-- A0 == { <<b,c>> \in Blocks \X Blocks: b=c }

ancestors[i \in Nat] == IF i=0 THEN A0

ELSE Extend(ancestors[i-1])

Ancestor(b,c) == /\ height[b] <= height[c]

/\ height[c] - height[b] \in Nat

/\ <<b,c>> \in ancestors[height[c] - height[b]]

My complete tree specification can be found here:

https://github.com/leandernikolaus/hotstuff-ivy/blob/master/Tree.tla

Thanks,

Leander

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/8bbc83f3-9900-4230-baa5-c3f5af7d0514n%40googlegroups.com.

**Follow-Ups**:**Re: [tlaplus] Proving inductive predicates in TLAPS***From:*Stephan Merz

- Prev by Date:
**Re: [tlaplus] How to generate a sequence from another sequence ?** - Next by Date:
**Re: [tlaplus] Proving inductive predicates in TLAPS** - Previous by thread:
**[tlaplus] Re: tla+ source code for the example in "How to Write a 21st Century Proof"** - Next by thread:
**Re: [tlaplus] Proving inductive predicates in TLAPS** - Index(es):