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

Stephan

On 14 Dec 2022, at 13:11, 'Vivek Pandey' via tlaplus <tlaplus@xxxxxxxxxxxxxxxx> wrote:

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

CONSTANT N, NIL

\* 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.