Re: [tlaplus] Why this TLA spec runs into stuttering state?

[Hillel Wayne]

If you remove the liveness property, does TypeOk still pass? Does NotSolved?

On 11/28/2024 5:40 PM, Anthony Lee wrote:

Hi all,

I have created a TLA spec to try 8 Queens problem.

It runs into stuttering state after several steps even when the Spec action has Strong Fairness setting.

Could anyone take a look and give me some hint?

Thanks.

Anthony

--
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 view this discussion visit https://groups.google.com/d/msgid/tlaplus/570a80f0-0929-4f17-90ec-d23400aac344n%40googlegroups.com.

[Stephan Merz]

The liveness property asserts that every run of the algorithm eventually leads to a solution. Instead, you certainly want to check that a solution exists, in other words that there exists a run that leads to a solution. However, I notice that on my side, the invariant NotSolved holds (for TOTAL = 4)?

Stephan

On 29 Nov 2024, at 00:40, Anthony Lee <antho...@gmail.com> wrote:

Hi all,

I have created a TLA spec to try 8 Queens problem.

It runs into stuttering state after several steps even when the Spec action has Strong Fairness setting.

Could anyone take a look and give me some hint?

Thanks.

Anthony

--
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 view this discussion visit https://groups.google.com/d/msgid/tlaplus/570a80f0-0929-4f17-90ec-d23400aac344n%40googlegroups.com.

<8Queens.cfg><8Queens.tla>

[Anthony Lee]

@Stephan

   Yes, you're right. A bug in my code which checks if a position is valid caused this stuttering -- actually in this case it is a real deadlock but I has been reading too much things about fairness and stuttering so that I didn't verify my code enough.

@Hillel,

   Yes, I did that and both passed, but it is false positive.

Now I wonder if there is a way to get all counter-examples.

[Abhishek Singh]

Please check the definition of SameDiagonal. Diagonals lie on x+y = constant and x-y = constant.

-Abhishek

[Anthony Lee]

Hi Abhishek,

Yes, that's the bug in the spec that made TLC runs into stuttering state.

Thanks.

Anthony