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

[Anthony Lee <anthonynlee@xxxxxxxxx>]

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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/570a80f0-0929-4f17-90ec-d23400aac344n%40googlegroups.com.
 SPECIFICATION Spec
\* Uncomment the previous line and provide the specification name if it's declared
\* in the specification file. Comment INIT / NEXT parameters if you use SPECIFICATION.

CONSTANTS
    TOTAL = 4
  
\* INIT Init
\* NEXT Next

PROPERTY
    Liveness
\* Uncomment the previous line and add property names

INVARIANT
    TypeOK
    NotSolved
\* Uncomment the previous line and add invariant names

Attachment: 8Queens.tla
Description: Binary data