[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.



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.





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.









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.