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

Re: RECURSIVE as a forward declaration

From: Ron Pressler <r...@xxxxxxxxxxxxxxxxxxx>
Date: Fri, 16 Oct 2015 04:43:08 -0700 (PDT)
References: <0785c320-863c-432f-a081-63cd40645612@googlegroups.com> <85f36d7f-64c3-47e2-9750-1f77800c1c11@googlegroups.com>

Right. Thanks!

On Thursday, October 15, 2015 at 12:08:27 PM UTC+3, Leslie Lamport wrote:

Here's something else you can do.

MessageAction(OpAction(_), u , v) == ...

   ...

OpAction(a) == ...

   ...

Next == \/ \E a \in ... : MessageAction(OpAction(a), ...)
          \/ ...

Leslie

References:
- RECURSIVE as a forward declaration
  - From: Ron Pressler
- Re: RECURSIVE as a forward declaration
  - From: Leslie Lamport

Prev by Date: TLAPS-proved invariant violated in TLC?
Next by Date: Re: [tlaplus] TLAPS-proved invariant violated in TLC?
Previous by thread: Re: RECURSIVE as a forward declaration
Next by thread: TLAPS-proved invariant violated in TLC?
Index(es):
- Date
- Thread