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

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.