Invariant checking doesn't work (?)

[thanhnguyen2187]

Hi! Thanks for the awesome project!

I encountered a "strange" error with the example in "Writing an Invariant". After setting is_unique = TRUE, the code looks like this:

---- MODULE scratch ----
EXTENDS Integers, Sequences, TLC

S == 1..10

(* --algorithm scratch
variables
    seq \in S \X S \X S \X S;
    index = 1;
    seen = {};
    is_unique = TRUE;
define
    TypeVariant ==
        /\ is_unique = FALSE
        /\ seen \subseteq S
        /\ index \in 1..Len(seq) + 1
end define;
begin
    Iterate:
        while index <= Len(seq) do
            if seq[index] \notin seen then
                seen := seen \union {seq[index]};
            else
                is_unique := FALSE;
            end if;
            index := index + 1;
        end while;
end algorithm; *)

I'm running tlc from the command line for that file, and it does not raise any error, while I think setting is_unique = TRUE should have raised some kind of problem.

TLC2 Version 2.18 of Day Month 20?? (rev: 03c7bf4)
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 121 and seed -3319692803442497325 with 1 worker on 8 cores with 3988MB heap and 64MB offheap memory [pid: 3513117] (Linux 6.1.74 amd64, N/A 21 x86_64, MSBDiskFPSet, DiskStateQueue).
Parsing file /home/thanh/Sources/thanhnguyen2187/playground/learn-tlaplus/scratch.tla
Parsing file /tmp/tlc-13031397994372591900/Integers.tla (jar:file:/home/thanh/Sources/thanhnguyen2187/playground/learn-tlaplus/tla2tools.jar!/tla2sany/StandardModules/Integers.tla)
Parsing file /tmp/tlc-13031397994372591900/Sequences.tla (jar:file:/home/thanh/Sources/thanhnguyen2187/playground/learn-tlaplus/tla2tools.jar!/tla2sany/StandardModules/Sequences.tla)
Parsing file /tmp/tlc-13031397994372591900/TLC.tla (jar:file:/home/thanh/Sources/thanhnguyen2187/playground/learn-tlaplus/tla2tools.jar!/tla2sany/StandardModules/TLC.tla)
Parsing file /tmp/tlc-13031397994372591900/_TLCTrace.tla (jar:file:/home/thanh/Sources/thanhnguyen2187/playground/learn-tlaplus/tla2tools.jar!/tla2sany/StandardModules/_TLCTrace.tla)
Parsing file /tmp/tlc-13031397994372591900/Naturals.tla (jar:file:/home/thanh/Sources/thanhnguyen2187/playground/learn-tlaplus/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)
Parsing file /tmp/tlc-13031397994372591900/FiniteSets.tla (jar:file:/home/thanh/Sources/thanhnguyen2187/playground/learn-tlaplus/tla2tools.jar!/tla2sany/StandardModules/FiniteSets.tla)
Parsing file /tmp/tlc-13031397994372591900/TLCExt.tla (jar:file:/home/thanh/Sources/thanhnguyen2187/playground/learn-tlaplus/tla2tools.jar!/tla2sany/StandardModules/TLCExt.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 TLC
Semantic processing of module TLCExt
Semantic processing of module _TLCTrace
Semantic processing of module scratch
Starting... (2024-04-26 02:04:23)
Computing initial states...
Computed 2 initial states...
Computed 4 initial states...
Computed 8 initial states...
Computed 16 initial states...
Computed 32 initial states...
Computed 64 initial states...
Computed 128 initial states...
Computed 256 initial states...
Computed 512 initial states...
Computed 1024 initial states...
Computed 2048 initial states...
Computed 4096 initial states...
Computed 8192 initial states...
Finished computing initial states: 10000 distinct states generated at 2024-04-26 02:04:23.
Model checking completed. No error has been found.
  Estimates of the probability that TLC did not check all reachable states
  because two distinct states had the same fingerprint:
  calculated (optimistic):  val = 3.3E-11
70000 states generated, 60000 distinct states found, 0 states left on queue.
The depth of the complete state graph search is 6.
The average outdegree of the complete state graph is 1 (minimum is 0, the maximum 1 and the 95th percentile is 1).
Finished in 00s at (2024-04-26 02:04:23)

For more context, I'm running TLA code from the command line like this:

java -cp tla2tools.jar pcal.trans scratch.tla
java -cp tla2tools.jar tlc2.TLC scratch.tla

What do you think can be the issue?

Thanks!

[hwayne]

Hi,

Sorry I'm getting to this late! Only saw this just now.

When you do java -cp tla2tools.jar pcal.trans, it will clobber your existing scratch.cfg file, meaning the invariant is removed too.