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:
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?