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

*From*: Greg Wiley <azte...@xxxxxxxxx>*Date*: Sun, 5 Nov 2017 16:00:34 -0800 (PST)*References*: <7928ce64-f9ac-4cb3-91bb-925a58a7cb8d@googlegroups.com> <be04f72b-6dfc-4d01-9214-51f50e1409a6@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

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) ofSpecifying Systems.

Leslie

**Follow-Ups**:**Re: [tlaplus] Re: What does f[x] mean when f is not a function?***From:*Justin Sampson

**Re: What does f[x] mean when f is not a function?***From:*loki der quaeler

**References**:**What does f[x] mean when f is not a function?***From:*azte . . .

**Re: What does f[x] mean when f is not a function?***From:*Leslie Lamport

- Prev by Date:
**Re: What does f[x] mean when f is not a function?** - Next by Date:
**Re: Analysis: Runway, a new formal specification system** - Previous by thread:
**Re: What does f[x] mean when f is not a function?** - Next by thread:
**Re: What does f[x] mean when f is not a function?** - Index(es):