Possible TLC regression on specifications/ewd998/EWD998ChanID.cfg about examples

[lemmy]

I've made several changes to that spec last week. Might this be it?

[ahelwer]

No it was running on the same spec/model. Is there a history repository of nightly builds anywhere I can test it against?

[lemmy]

In these cases I use git bisect.

[ahelwer]

As good an excuse for me to finally learn git bisect as any! I think the last time I would have updated tla2tools.jar was when working on this PR, so June 6th of this year.

[ahelwer]

Okay, found it! Not a problem with TLC, but with the community modules. I had also changed the community modules jar locally (never change two things at once, gah). When using the https://github.com/tlaplus/CommunityModules/releases/tag/202304140044 release instead of the latest https://github.com/tlaplus/CommunityModules/releases/tag/202307191312 release, specifications/ewd998/EWD998ChanID.cfg fails with this error (exit code 13, a liveness failure):

Implied-temporal checking--satisfiability problem has 2 branches.
Computing initial states...
Finished computing initial states: 1 distinct state generated at 2023-08-07 17:26:27.
Error: Action property line 138, col 17 to line 138, col 29 of module EWD998Chan is violated.
Error: The behavior up to this point is:
State 1: <Initial predicate>
/\ color = ( n1 :> "black" @@
  n2 :> "black" @@
  n3 :> "black" @@
  n4 :> "black" @@
  n5 :> "black" )
/\ inbox = ( n1 :> <<>> @@
  n2 :> <<>> @@
  n3 :> <<>> @@
  n4 :>
      << [ color |-> "black",
           type |-> "tok",
           q |-> 0,
           vc |-> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0 @@ n5 :> 0) ] >> @@
  n5 :> <<>> )
/\ active = (n1 :> FALSE @@ n2 :> FALSE @@ n3 :> FALSE @@ n4 :> FALSE @@ n5 :> FALSE)
/\ passes = 0
/\ counter = (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0 @@ n5 :> 0)
/\ clock = ( n1 :> (n1 :> 1 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0 @@ n5 :> 0) @@
  n2 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0 @@ n5 :> 0) @@
  n3 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0 @@ n5 :> 0) @@
  n4 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0 @@ n5 :> 0) @@
  n5 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0 @@ n5 :> 0) )

State 2: <PassToken(n4) line 129, col 3 to line 148, col 57 of module EWD998ChanID>
/\ color = ( n1 :> "black" @@
  n2 :> "black" @@
  n3 :> "black" @@
  n4 :> "white" @@
  n5 :> "black" )
/\ inbox = ( n1 :> <<>> @@
  n2 :> <<>> @@
  n3 :> <<>> @@
  n4 :> <<>> @@
  n5 :>
      << [ color |-> "black",
           type |-> "tok",
           q |-> 0,
           vc |-> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 1 @@ n5 :> 0) ] >> )
/\ active = (n1 :> FALSE @@ n2 :> FALSE @@ n3 :> FALSE @@ n4 :> FALSE @@ n5 :> FALSE)
/\ passes = 1
/\ counter = (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0 @@ n5 :> 0)
/\ clock = ( n1 :> (n1 :> 1 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0 @@ n5 :> 0) @@
  n2 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0 @@ n5 :> 0) @@
  n3 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0 @@ n5 :> 0) @@
  n4 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 1 @@ n5 :> 0) @@
  n5 :> (n1 :> 0 @@ n2 :> 0 @@ n3 :> 0 @@ n4 :> 0 @@ n5 :> 0) )

2 states generated, 2 distinct states found, 0 states left on queue.
The depth of the complete state graph search is 2.
Finished in 01s at (2023-08-07 17:26:27)
Trace exploration spec path: ewd998/EWD998ChanID_TTrace_1691443586.tla

If this isn't a bug then feel free to close.

[lemmy]

You closed it => not a bug?

[ahelwer]

I probably would not have reported this as a bug if I knew the cause originally. At most it is an example of how declaring dependency version of the community modules might be important.