Re: [tlaplus] Re: What does f[x] mean when f is not a function?

Regarding the order of terms, I remember reading that's one of those things where TLC is enforcing a convenient subset of TLA+, whereas TLAPS behaves differently. Mathematically the order doesn't matter, and a formal proof may take advantage of that fact, but the model checker takes the easier route of short-circuit evaluation.

Cheers,

Justin (barely starting to play with TLA+ myself)

From: <tl...@xxxxxxxxxxxxxxxx> on behalf of Greg Wiley <azt...@xxxxxxxxx>
Reply-To: "t...@xxxxxxxxxxxxxxxx" <tl...@xxxxxxxxxxxxxxxx>
Date: Sunday, November 5, 2017 at 3:39 PM
To: tlaplus <tl...@xxxxxxxxxxxxxxxx>
Subject: [tlaplus] Re: What does f[x] mean when f is not a function?

It appears I am guilty of thinking like a computer programmer.

Thank you for that. Because of other conjucands, RdMiss would never be a step from a state where buf[p] is not a request.

I experimented with SimpleProgram, adding this definition:

Silly == /\ pc = "grape"

/\ 1[2] = "orange"

And changing the definition of Next:

Next == Pick \/ Add1 \/ Silly

TLC claimed my model is fine. That is what I expected from reading the silly expressions text.

Then, I changed the definition of Silly:

Silly == /\ pc = "middle"

/\ 1[2] = "orange"

TLC then said I was being ridiculous, using an integer as a function.

I think I get it.

One last thing I wondered, does the order of terms matter?

Silly == /\ 1[2] = "orange"

/\ pc = "grape"

It does. TLC tells me that this _expression_ is ridiculous even though it

is logically equivalent to the first. To use a potentially silly _expression_,

I must ensure that the predicates guarding it are evaluated first due

to what appears to be a short-circuit evaluation. I think the text might

be telling me that but I will study it more to be sure.

Thank you again.

-=greg

On Saturday, November 4, 2017 at 10:55:07 PM UTC-7, Leslie Lamport wrote:

The answer to your two questions is that they are "silly expressions". See Section 6.2 (page 67) of Specifying Systems.

Leslie

--
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+unsu...@xxxxxxxxxxxxxxxx.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.