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

*From*: Leslie Lamport <tlapl...@xxxxxxxxx>*Date*: Sat, 27 May 2017 07:19:25 -0700 (PDT)*Cc*: ston...@xxxxxxxxx*References*: <1b8021e4-4bfa-4d26-bddb-64cf28e4f27d@googlegroups.com>

You are asking for an explanation of why your specification causes TLC to produce a particular output without showing us your specification. I presume that's why no one bothered to answer your question. If you double-click on the line in the error trace between the last two states, the Toolbox will show you what part of the next-state relation permitted the step from state 4 to state 5. Understanding why that formula allowed that step should allow you to answer your question yourself.

On Wednesday, May 24, 2017 at 1:27:05 PM UTC-7, stonebits@... wrote:

On Wednesday, May 24, 2017 at 1:27:05 PM UTC-7, stonebits@... wrote:

My "value" error trace when there's a solution (the /= Goal is violated) is the following

State (num = 1)

(small :> 0 @@ big :> 0)

State (num = 2)

(small :> 0 @@ big :> 5)

State (num = 3)

(small :> 3 @@ big :> 2)

State (num = 4)

(small :> 0 @@ big :> 2)

State (num = 5)

(small :> -2 @@ big :> 4)

I'm confused as to why "small" is ever negative as it is in state 5 -- any ideas?

**Follow-Ups**:**Re: Interpreting the DieHarder error trace***From:*ston . . .

**References**:**Interpreting the DieHarder error trace***From:*ston . . .

- Prev by Date:
**Re: Paramaterized Instantiation and Universal Quantification** - Next by Date:
**Modeling memory barriers** - Previous by thread:
**Interpreting the DieHarder error trace** - Next by thread:
**Re: Interpreting the DieHarder error trace** - Index(es):