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

*From*: Ron Pressler <r...@xxxxxxxxxxxxxxxxxxx>*Date*: Tue, 20 Oct 2015 15:30:40 -0700 (PDT)*References*: <4a40f27f-5358-4339-84e1-1ceff5eecefa@googlegroups.com> <81654554-8d29-4b5e-9ad1-c451b6548a41@googlegroups.com> <8f77b9ff-48f6-4ad3-bb4a-3f381334bf6a@googlegroups.com> <0ee7e8a4-07ed-4c07-a61b-5a91064b4042@googlegroups.com>

Sorry again, obviously it's a partial relation induced by the formula on all pairs of states... :)

On Wednesday, October 21, 2015 at 12:40:19 AM UTC+3, Ron Pressler wrote:

On Wednesday, October 21, 2015 at 12:40:19 AM UTC+3, Ron Pressler wrote:

My mistake was not realizing that Next is a full relation on the entire universe of states (I thought that it was a "constructive" partial relation), that for _every_ two states s and t, must determine whether t can be a next state of s or not. Then, on top of that, there's TLC's evaluation rules about the first encounter with a primed variable that must uniquely determine its value, and therefore cannot be a negation of the sort ~(x' = ...).Do I have it right?

**References**:**Unclear TLC evaluation behavior***From:*Ron Pressler

**Re: Unclear TLC evaluation behavior***From:*Leslie Lamport

**Re: Unclear TLC evaluation behavior***From:*Ron Pressler

**Re: Unclear TLC evaluation behavior***From:*Ron Pressler

- Prev by Date:
**Re: Unclear TLC evaluation behavior** - Next by Date:
**Potentially confusing behavior of a PlusCal algorithm** - Previous by thread:
**Re: Unclear TLC evaluation behavior** - Next by thread:
**Re: Unclear TLC evaluation behavior** - Index(es):