Report Stuttering as Back to state if a moot action is taken

[egolf-cs]

The spec I've attached below reports a stuttering violation. This is confusing to me as there is an always enabled, strongly fair action SendLock. I believe that the action SendLock is taken in the "stuttering step" of the violation, but it isn't being reported since there is no change in state. Is it possible to have TLC report this as Back to state or otherwise report the action that was taken?

EXTENDS TLC

CONSTANT Node

VARIABLE lock_msg
VARIABLE grant_msg
VARIABLE unlock_msg
VARIABLE holds_lock
VARIABLE server_holds_lock

vars == <<lock_msg, grant_msg, unlock_msg, holds_lock, server_holds_lock>>

SendLock(n) == 
    /\ lock_msg' = lock_msg \cup {n}
    /\ UNCHANGED <<unlock_msg, grant_msg, holds_lock, server_holds_lock>>

RecvLock(n) == 
    /\ server_holds_lock
    \* /\ n \in lock_msg
    /\ FALSE
    \* /\ server_holds_lock' = FALSE
    /\ server_holds_lock' = TRUE
    /\ lock_msg' = lock_msg \ {n}
    /\ grant_msg' = grant_msg \cup {n}
    /\ UNCHANGED <<unlock_msg,holds_lock>>

RecvGrant(n) == 
    /\ n \in grant_msg
    /\ grant_msg' = grant_msg \ {n}
    /\ holds_lock' = holds_lock \cup {n}
    /\ UNCHANGED <<lock_msg,unlock_msg,server_holds_lock>>

Unlock(n) == 
    /\ n \in holds_lock
    /\ holds_lock' = holds_lock \ {n}
    /\ unlock_msg' = unlock_msg \cup {n}
    /\ UNCHANGED <<lock_msg, grant_msg, server_holds_lock>>

RecvUnlock(n) == 
    /\ n \in unlock_msg
    /\ unlock_msg' = unlock_msg \ {n}
    /\ server_holds_lock' = TRUE
    /\ UNCHANGED <<lock_msg, grant_msg, holds_lock>>

NextParam(n) == 
    \/ SendLock(n)
    \/ RecvLock(n)
    \/ RecvGrant(n)
    \/ Unlock(n)
    \/ RecvUnlock(n)

Next == \E n \in Node : NextParam(n)

Init == 
    /\ lock_msg = {}
    /\ unlock_msg = {}
    /\ grant_msg = {}
    /\ holds_lock = {}
    /\ server_holds_lock = TRUE

Spec == 
    /\ Init 
    /\ [][Next]_vars
    /\ \A n \in Node : SF_vars(NextParam(n))

\* No two clients think they hold the lock simultaneously.
Mutex == \A x,y \in Node : ((x \in holds_lock) /\ (y \in holds_lock)) => (x = y)

Liveness == 
    /\ \A n \in Node : [] (n \in lock_msg => <> (n \in holds_lock))
    /\ \A n \in Node : []<> (n \in lock_msg)
    /\ \A n \in Node : []<> (n \notin lock_msg)

====

[lemmy]

Please attach the counterexample to the stuttering violation.

[egolf-cs]

Here is the output:

java -cp /home/egolf/.vscode/extensions/alygin.vscode-tlaplus-1.5.4/tools/tla2tools.jar -XX:+UseParallelGC tlc2.TLC lock_serv.tla -tool -modelcheck -coverage 1 -config lock_serv.cfg
TLC2 Version 2.16 of 31 December 2020 (rev: cdddf55)
Running breadth-first search Model-Checking with fp 128 and seed 7433361044253834044 with 1 worker on 8 cores with 3492MB heap and 64MB offheap memory [pid: 974] (Linux 5.3.0-28-generic amd64, Private Build 17.0.7 x86_64, MSBDiskFPSet, DiskStateQueue).
Starting SANY...
Parsing file lock_serv.tla
Parsing file /tmp/TLC.tla
Parsing file /tmp/Naturals.tla
Parsing file /tmp/Sequences.tla
Parsing file /tmp/FiniteSets.tla
Semantic processing of module Naturals
Semantic processing of module Sequences
Semantic processing of module FiniteSets
Semantic processing of module TLC
Semantic processing of module lock_serv
SANY finished.
Starting... (2024-02-05 13:09:59)
Implied-temporal checking--satisfiability problem has 4 branches.
Computing initial states...
Finished computing initial states: 1 distinct state generated at 2024-02-05 13:09:59.
Progress(4) at 2024-02-05 13:09:59: 25 states generated, 8 distinct states found, 0 states left on queue.
Checking 4 branches of temporal properties for the complete state space with 32 total distinct states at (2024-02-05 13:09:59)
Temporal properties were violated.
The following behavior constitutes a counter-example:
1: <Initial predicate>
/\ lock_msg = {}
/\ server_holds_lock = TRUE
/\ holds_lock = {}
/\ grant_msg = {}
/\ unlock_msg = {}
2: <SendLock line 15, col 5 to line 16, col 73 of module lock_serv>
/\ lock_msg = {n1}
/\ server_holds_lock = TRUE
/\ holds_lock = {}
/\ grant_msg = {}
/\ unlock_msg = {}
3: <SendLock line 15, col 5 to line 16, col 73 of module lock_serv>
/\ lock_msg = {n1, n2}
/\ server_holds_lock = TRUE
/\ holds_lock = {}
/\ grant_msg = {}
/\ unlock_msg = {}
4: <SendLock line 15, col 5 to line 16, col 73 of module lock_serv>
/\ lock_msg = {n1, n2, n3}
/\ server_holds_lock = TRUE
/\ holds_lock = {}
/\ grant_msg = {}
/\ unlock_msg = {}
5: Stuttering
Finished checking temporal properties in 00s at 2024-02-05 13:09:59
The coverage statistics at 2024-02-05 13:09:59
<Init line 55, col 1 to line 55, col 4 of module lock_serv>: 2:2
  line 56, col 5 to line 60, col 31 of module lock_serv: 2
<SendLock line 14, col 1 to line 14, col 11 of module lock_serv>: 7:39
  line 15, col 8 to line 15, col 36 of module lock_serv: 39
  line 16, col 8 to line 16, col 73 of module lock_serv: 39
<RecvLock line 18, col 1 to line 18, col 11 of module lock_serv>: 0:0
  line 23, col 8 to line 23, col 32 of module lock_serv: 0
  line 24, col 8 to line 24, col 33 of module lock_serv: 0
  line 25, col 8 to line 25, col 38 of module lock_serv: 0
  line 26, col 8 to line 26, col 42 of module lock_serv: 0
<RecvGrant line 28, col 1 to line 28, col 12 of module lock_serv>: 0:0
  line 29, col 8 to line 29, col 22 of module lock_serv: 36
  line 30, col 8 to line 30, col 35 of module lock_serv: 0
  line 31, col 8 to line 31, col 40 of module lock_serv: 0
  line 32, col 8 to line 32, col 58 of module lock_serv: 0
<Unlock line 34, col 1 to line 34, col 9 of module lock_serv>: 0:0
  line 35, col 8 to line 35, col 23 of module lock_serv: 36
  line 36, col 8 to line 36, col 37 of module lock_serv: 0
  line 37, col 8 to line 37, col 40 of module lock_serv: 0
  line 38, col 8 to line 38, col 59 of module lock_serv: 0
<RecvUnlock line 40, col 1 to line 40, col 13 of module lock_serv>: 0:0
  line 41, col 8 to line 41, col 23 of module lock_serv: 36
  line 42, col 8 to line 42, col 37 of module lock_serv: 0
  line 43, col 8 to line 43, col 32 of module lock_serv: 0
  line 44, col 8 to line 44, col 52 of module lock_serv: 0
<Mutex line 68, col 1 to line 68, col 5 of module lock_serv>
  line 68, col 10 to line 68, col 80 of module lock_serv: 8
  |line 68, col 28 to line 68, col 80 of module lock_serv: 72
  |line 68, col 21 to line 68, col 24 of module lock_serv: 8
End of statistics.
Progress(4) at 2024-02-05 13:09:59: 25 states generated (2,384 s/min), 8 distinct states found (763 ds/min), 0 states left on queue.
25 states generated, 8 distinct states found, 0 states left on queue.
Finished in 636ms at (2024-02-05 13:09:59)

[lemmy]

Sounds reasonable to make this "cosmetic" change. Do you have the bandwidth to provide a patch?