[BUG] Bogus "Found a cyclic dependency among operators:..." error

[lemmy]

Not sure how to interpret that error, but StarvationFree appears nowhere except in its definition.

markus@avocado:/tmp/3procs$ apalache check MC
# Tool home: /home/markus/src/TLA/_community/apalache
# Package:   /home/markus/src/TLA/_community/apalache/mod-distribution/target/apalache-pkg-0.11.1-SNAPSHOT-full.jar
# JVM args: -Xmx4096m -DTLA-Library=/home/markus/src/TLA/_community/apalache/src/tla
#
# APALACHE version 0.11.1-SNAPSHOT build v0.11.0-17-gf55663c
#
# WARNING: This tool is in the experimental stage.
#          Please report bugs at: [https://github.com/informalsystems/apalache/issues]
# 
# Usage statistics is ON. Thank you!
# If you have changed your mind, disable the statistics with config --enable-stats=false.

Checker options: filename=MC, init=, next=, inv=                  I@14:39:05.431
Tuning:                                                           I@14:39:05.902
PASS #0: SanyParser                                               I@14:39:05.902
Parsing file /tmp/3procs/MC.tla
Parsing file /tmp/3procs/ProtoBakeryPCal.tla
Parsing file /tmp/TLC.tla
Parsing file /tmp/Integers.tla
Parsing file /tmp/FiniteSets.tla
Parsing file /tmp/Naturals.tla
Parsing file /tmp/Sequences.tla
Error by TLA+ parser: Found a cyclic dependency among operators: subProcsOf, ncs, FSpec, GoodNums, setnum, cs, InCS, pid, StarvationFree, Spec, Mutex, Next E@14:39:06.540
It took me 0 days  0 hours  0 min  1 sec                          I@14:39:06.541
Total time: 1.112 sec                                             I@14:39:06.542
EXITCODE: ERROR (99)

markus@avocado:/tmp/3procs$ tlc MC
TLC2 Version 2.15 of Day Month 20?? (rev: be76942)
Warning: Please run the Java VM, which executes TLC with a throughput optimized garbage collector, by passing the "-XX:+UseParallelGC" property.
(Use the -nowarning option to disable this warning.)
Running breadth-first search Model-Checking with fp 92 and seed -7060124807455608380 with 1 worker on 4 cores with 5952MB heap and 64MB offheap memory [pid: 34027] (Linux 5.4.0-66-generic amd64, Ubuntu 11.0.10 x86_64, MSBDiskFPSet, DiskStateQueue).
Parsing file /tmp/3procs/MC.tla
Parsing file /tmp/3procs/ProtoBakeryPCal.tla
Parsing file /tmp/TLC.tla (jar:file:/opt/toolbox/tla2tools.jar!/tla2sany/StandardModules/TLC.tla)
Parsing file /tmp/Integers.tla (jar:file:/opt/toolbox/tla2tools.jar!/tla2sany/StandardModules/Integers.tla)
Parsing file /tmp/FiniteSets.tla (jar:file:/opt/toolbox/tla2tools.jar!/tla2sany/StandardModules/FiniteSets.tla)
Parsing file /tmp/Naturals.tla (jar:file:/opt/toolbox/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)
Parsing file /tmp/Sequences.tla (jar:file:/opt/toolbox/tla2tools.jar!/tla2sany/StandardModules/Sequences.tla)
Semantic processing of module Naturals
Semantic processing of module Integers
Semantic processing of module Sequences
Semantic processing of module FiniteSets
Semantic processing of module ProtoBakeryPCal
Semantic processing of module TLC
Semantic processing of module MC
Starting... (2021-03-11 14:39:15)
Computing initial states...
Finished computing initial states: 1 distinct state generated at 2021-03-11 14:39:15.
Progress(14) at 2021-03-11 14:39:18: 138,262 states generated (138,262 s/min), 49,461 distinct states found (49,461 ds/min), 24,650 states left on queue.
....

-------------------------- MODULE ProtoBakeryPCal --------------------------
EXTENDS Integers, FiniteSets 

q \ll r == \/ q[1] < r[1]
           \/ /\ q[1] = r[1]
              /\ q[2] < r[2]

CONSTANT AnyNum
ASSUME AnyNum \notin Nat

CONSTANT Procs
ASSUME  /\ Procs \subseteq Int
        /\ IsFiniteSet(Procs)

SubProcs == {q \in Procs \X Procs : q[1] # q[2]}
subProcsOf(pid) == {q \in SubProcs : q[1] = pid[1]}
ProcIds == {<<p>> : p \in Procs}
Mirror(q) == <<q[2], q[1]>>
Wr0Procs == {<<q[1], q[2], "wr0">> : q \in SubProcs}
sprocOfW0(w) == <<w[1], w[2]>>

Min(S) == CHOOSE n \in S : \A m \in S \ {n} : m > n

Zeros(S) == [i \in S |-> 0]

GoodNums(pid, fcn) == { m \in Nat \ {0} : \A q \in subProcsOf(pid) :
                                            <<fcn[q], q[2]>> \ll <<m, pid[1]>> } 

Replace(fcn, S, val) ==
  [x \in DOMAIN fcn |-> IF x \in S THEN val ELSE fcn[x]]                                            

\* BEGIN TRANSLATION (chksum(pcal) = "19c645ce" /\ chksum(tla) = "6a96cb81")
VARIABLES num, vnum, temp, pc

vars == << num, vnum, temp, pc >>

ProcSet == (SubProcs) \cup (ProcIds) \cup (Wr0Procs)

Init == (* Global variables *)
        /\ num = Zeros(Procs)
        /\ vnum = Zeros(SubProcs)
        /\ temp = Zeros(SubProcs)
        /\ pc = [self \in ProcSet |-> CASE self \in SubProcs -> "enter"
                                        [] self \in ProcIds -> "ncs"
                                        [] self \in Wr0Procs -> "wr0"]

enter(self) == /\ pc[self] = "enter"
               /\ pc[<<self[1]>>] = "setnum"
               /\ IF vnum[Mirror(self)] = AnyNum
                     THEN /\ \E v \in Nat:
                               temp' = [temp EXCEPT ![self] = v]
                     ELSE /\ temp' = [temp EXCEPT ![self] = vnum[Mirror(self)]]
               /\ pc' = [pc EXCEPT ![self] = "wr1"]
               /\ UNCHANGED << num, vnum >>

wr1(self) == /\ pc[self] = "wr1"
             /\ pc[<<self[1]>>] = "cs"
             /\ vnum' = [vnum EXCEPT ![self] = num[self[1]]]
             /\ pc' = [pc EXCEPT ![self] = "wait1"]
             /\ UNCHANGED << num, temp >>

wait1(self) == /\ pc[self] = "wait1"
               /\ pc[Mirror(self)] /=  "wr1"
               /\ pc' = [pc EXCEPT ![self] = "wait2"]
               /\ UNCHANGED << num, vnum, temp >>

wait2(self) == /\ pc[self] = "wait2"
               /\ IF vnum[Mirror(self)] \notin {AnyNum, 0}
                     THEN /\ <<num[self[1]], self[1]>> \ll <<vnum[Mirror(self)], self[2]>>
                     ELSE /\ TRUE
               /\ pc' = [pc EXCEPT ![self] = "scs"]
               /\ UNCHANGED << num, vnum, temp >>

scs(self) == /\ pc[self] = "scs"
             /\ pc[<<self[1]>>] = "ncs"
             /\ pc' = [pc EXCEPT ![self] = "enter"]
             /\ UNCHANGED << num, vnum, temp >>

subProc(self) == enter(self) \/ wr1(self) \/ wait1(self) \/ wait2(self)
                    \/ scs(self)

ncs(self) == /\ pc[self] = "ncs"
             /\ \A q \in subProcsOf(self) : pc[q] = "enter"
             /\ pc' = [pc EXCEPT ![self] = "setnum"]
             /\ UNCHANGED << num, vnum, temp >>

setnum(self) == /\ pc[self] = "setnum"
                /\ \A q \in subProcsOf(self) : pc[q] = "wr1"
                /\ \E n \in GoodNums(self, temp):
                     num' = [num EXCEPT ![self[1]] = n]
                /\ vnum' = Replace(vnum, subProcsOf(self), AnyNum)
                /\ pc' = [pc EXCEPT ![self] = "cs"]
                /\ temp' = temp

cs(self) == /\ pc[self] = "cs"
            /\ \A q \in subProcsOf(self) : pc[q] = "scs"
            /\ num' = [num EXCEPT ![self[1]] = 0]
            /\ vnum' = Replace(vnum, subProcsOf(self), AnyNum)
            /\ pc' = [pc EXCEPT ![self] = "ncs"]
            /\ temp' = temp

pid(self) == ncs(self) \/ setnum(self) \/ cs(self)

wr0(self) == /\ pc[self] = "wr0"
             /\ LET q == <<self[1], self[2]>> IN
                  /\ (pc[q] = "enter") /\ (vnum[q] = AnyNum)
                  /\ vnum' = [vnum EXCEPT ![q] = 0]
             /\ pc' = [pc EXCEPT ![self] = "wr0"]
             /\ UNCHANGED << num, temp >>

wr(self) == wr0(self)

Next == (\E self \in SubProcs: subProc(self))
           \/ (\E self \in ProcIds: pid(self))
           \/ (\E self \in Wr0Procs: wr(self))

Spec == /\ Init /\ [][Next]_vars
        /\ \A self \in SubProcs : WF_vars((pc[self] # "wait2") /\ subProc(self))
        /\ \A self \in ProcIds : WF_vars((pc[self] # "ncs") /\ pid(self))
        /\ \A self \in Wr0Procs : WF_vars(wr(self))

\* END TRANSLATION 
-----------------------------------------------------------------------------
FSpec == /\ Spec 
         /\ \A q \in SubProcs : WF_vars(wait2(q) /\ (vnum[Mirror(q)] # AnyNum))
TypeOK == /\ num  \in [Procs -> Nat]
          /\ vnum \in [SubProcs -> Nat \cup {AnyNum}]
          /\ temp \in [SubProcs -> Nat]  
          /\ pc \in [ProcSet -> STRING]

InCS(p)  == (pc[p] = "cs") /\ (\A q \in subProcsOf(p) : pc[q] = "scs")

Mutex == \A p \in ProcIds : \A q \in ProcIds \ {p} : ~(InCS(p) /\ InCS(q))

StarvationFree == \A p \in ProcIds : (pc[p] = "setnum") ~> InCS(p) 
-----------------------------------------------------------------------------
TestMaxNum == 2
TestNat == 0..(TestMaxNum + 1)
=============================================================================
\* Modification History
\* Created Thu Mar 11 22:07:26 UTC 2021 by lamport

---- MODULE MC ----
EXTENDS ProtoBakeryPCal, TLC

\* CONSTANT definitions @modelParameterConstants:0Procs
const_16155006965746000 == 
{-3,-2,-1}
----

\* CONSTANT definition @modelParameterDefinitions:0
def_ov_16155006965747000 ==
TestNat
----
\* CONSTRAINT definition @modelParameterContraint:0
constr_16155006965748000 ==
\A q \in SubProcs : temp[q] =< TestMaxNum
----
=============================================================================

---- CONFIG MC ----
\* CONSTANT declarations
CONSTANT AnyNum = AnyNum
\* CONSTANT definitions
CONSTANT
Procs <- const_16155006965746000
\* CONSTANT definition
CONSTANT
Nat <- def_ov_16155006965747000
\* CONSTRAINT definition
CONSTRAINT
constr_16155006965748000
\* SPECIFICATION definition
SPECIFICATION
Spec
\* INVARIANT definition
INVARIANT
Mutex
\* Generated on Thu Mar 11 22:11:36 UTC 2021
====

[konnov]

@Kukovec could you maybe have a look to see, where it is happening?

[konnov]

This is interesting. We are internally sorting operator definitions, as they sometimes come out of order, especially when instances are involved. The problem in this example is that pid is used in two roles: as an operator name and as a parameter name. It works in this example because the operator pid is defined after the operator subProcsOf(pid). I always find those declaration rules counterintuitive. I will see what we can do.

[konnov]

That was not hard. Fixed in #777.