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

77 views
Skip to first unread message

azte...@jammm.com

unread,
Nov 5, 2017, 1:50:38 AM11/5/17
to tlaplus
In the TLA book on page 57, the definition for RdMiss(p) contains the formula:

buf[p].op = "Rd"

However, buf is function with domain Proc and range that includes
requests, values, and NoValue. So, buf[p] might not be a function with a
domain containing "op". It might not be a function at all.

I guess I have two questions:

What does f["op"] mean when "op" is not in the domain of the function, f?
What does f["op"] mean when f is not a function?

I'm looking specifically for what those things mean in TLA+ but a mathematical
context is more than welcome.

TIA, -=greg

Leslie Lamport

unread,
Nov 5, 2017, 1:55:07 AM11/5/17
to tlaplus
The answer to your two questions is that they are "silly expressions".  See Section 6.2 (page 67) of Specifying Systems.


Leslie

Greg Wiley

unread,
Nov 5, 2017, 6:39:12 PM11/5/17
to tla...@googlegroups.com
It appears I am guilty of thinking like a computer programmer.

Thank you for that. Because of other conjuncts, 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

loki der quaeler

unread,
Nov 6, 2017, 12:30:15 AM11/6/17
to tlaplus

Hmm.. the toolbox editor should have denoted a parse error when you declared something in VARIABLES that was an integer - did it not?

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

WRT TLC, the ordering of the terms does matter for conjunctions; since in your modified spec, pc = "grape" never evaluates to true, any following same-depth conjuncts will not be evaluated, i believe.

loki

Justin Sampson

unread,
Nov 6, 2017, 12:31:06 PM11/6/17
to tla...@googlegroups.com

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: <tla...@googlegroups.com> on behalf of Greg Wiley <azte...@jammm.com>
Reply-To: "tla...@googlegroups.com" <tla...@googlegroups.com>
Date: Sunday, November 5, 2017 at 3:39 PM
To: tlaplus <tla...@googlegroups.com>
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.

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

Reply all
Reply to author
Forward
0 new messages