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

*From*: Ron Pressler <r...@xxxxxxxxxxxxxxxxxxx>*Date*: Thu, 22 Oct 2015 02:20:07 -0700 (PDT)*References*: <4a40f27f-5358-4339-84e1-1ceff5eecefa@googlegroups.com> <df88c0e2-0f85-46b2-a5ee-a020cb6207ac@googlegroups.com>

Just to make sure I really understand, is the following next-state formula not OK or is it just rejected by TLC for implementation reasons? (assuming x and a are the only variables)

Next ==

IF x' = 3 THEN

a' = "SUCCESS"

ELSE

/\ x' = 5

/\ a' = "FAIL"

(Or even: Next == ~(x' = 3) => x' = 5)

Because it seems to me that for any two states, s and t, the formula [Next]_<<x, a>> always determines whether t can be a next state of s.

If it is just a TLC issue, then it's come up in practice a few times while I writing my first spec. Not in that precise form but more like:

Next ==

IF TrySomething THEN

success' = TRUE

ELSE

/\ UNCHANGED data

/\ success' = FALSE

Or

Next == ~TrySomething => TrySomethingElse

Where TrySomething has some intricate conditions, depending on which it "sets" data' to one of several possible values, or if none of the conditions is met it doesn't touch data'. I'm interested to know whether TrySomething has succeeded or failed. Obviously, this can be refactored by taking the conditions out of TrySomething, but that would make the formula encapsulation and organization less optimal. So, assuming the formula is valid TLA+, it seems quite sensible yet TLC can't handle it...

It is also very likely that I still haven't internalized the TLA+ "style" yet, but at least from a beginner's perspective, the above formulas seem natural.

Ron

**Follow-Ups**:**Re: [tlaplus] Unclear TLC evaluation behavior***From:*Stephan Merz

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

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

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