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

[tlaplus] [External] Need help to understand why model checker is ending up in stuttering step

Hi Folks,

I am new to TLA+ and trying to write a spec for checking cycle in a singly linked list.
The model checker is ending up in stuttering. Can anybody please help me understand & fix it? Thanks!

Here is the spec: -

--------------------------- MODULE CycleDetection ---------------------------

EXTENDS TLC, Naturals, FiniteSets, Sequences


\* Put the constraint on N

ASSUME NIsPositive == N \in (Nat \ {0})

\* Put the constraint on NIL

ASSUME NilIsNotInN == NIL \notin 1..N

\* Represents the set of nodes

Nodes == 1..N

\*Init position of hare and tortoise

InitPos == 1

VARIABLES linkedList, tortoise, hare, cycleDetected, pc

vars == << linkedList, tortoise, hare, cycleDetected, pc >>

\* Check if the linkedList is a valid singly linked linkedList (may have cycle)

IsValidLinkedList(l) == \A n \in Nodes : 

                                            \/  /\ n = N

                                                /\ l[n] \in ((Nodes \union {NIL}) \ {n})

                                            \/ l[n] = n + 1

ValidlinkedListsSet ==  {l \in [Nodes -> Nodes \union {NIL}] : IsValidLinkedList(l) } 

Init == /\ linkedList \in ValidlinkedListsSet        

        /\ tortoise = InitPos

        /\ hare = InitPos

        /\ cycleDetected = FALSE

        /\ pc = "MoveTortoise"

MoveTortoise ==  

        /\ pc = "MoveTortoise"

        /\ tortoise' = IF tortoise # NIL THEN linkedList[tortoise] ELSE NIL                

        /\ pc' = "MoveHare"

        /\ UNCHANGED << linkedList, hare, cycleDetected >>        

MoveHare ==  

        /\ pc = "MoveHare"

        /\ hare' = IF (hare = NIL \/ linkedList[hare] = NIL) THEN NIL ELSE linkedList[linkedList[hare]]        

        /\ pc' = "Check"

        /\ UNCHANGED << linkedList, tortoise, cycleDetected >>        

Check ==        

        /\ pc = "Check"                

        /\ cycleDetected' = (tortoise = hare)               

        /\ pc' = IF (tortoise = NIL \/ hare = NIL \/ (tortoise = hare)) THEN "Done" ELSE "MoveTortoise"

        /\ UNCHANGED << linkedList, tortoise, hare >>

Next == MoveTortoise \/ MoveHare \/ Check \/ (pc = "Done" /\ UNCHANGED vars)

Spec == Init /\ [][Next]_vars

TypeInvariant == 

                    /\ pc \in {"MoveTortoise", "MoveHare", "Done", "Check"}

                    /\ cycleDetected \in BOOLEAN 

                    /\ tortoise \in (Nodes \union {NIL})

                    /\ hare \in (Nodes \union {NIL})                    

Termination == <> (pc = "Done")


By communicating with Grab Holdings Limited and/or its subsidiaries, associate companies and jointly controlled entities (collectively, “Grab”), you are deemed to have consented to the processing of your personal data as set out in the Privacy Notice which can be viewed at https://grab.com/privacy/ 

 This email contains confidential information that may be privileged and is only for the intended recipient(s). If you are not the intended recipient(s), please do not disseminate, distribute or copy this email. Please notify Grab immediately if you have received this by mistake and delete this email from your system. Email transmission may not be secure or error-free as any information could be intercepted, corrupted, lost, destroyed, delayed or incomplete, or contain viruses. Grab does not accept liability for any errors or omissions in this email that arise as a result of email transmission. All intellectual property rights in this email and any attachments shall remain vested in Grab, unless otherwise provided by law

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 on the web visit https://groups.google.com/d/msgid/tlaplus/5aea3c2d-7fec-4ff2-8733-001c558916d2n%40googlegroups.com.