[tlaplus] Zenon error: uncaught exception File "ext_tla.ml" in TLAPS

[jayaprabhakar k <jayaprabhakar@xxxxxxxxx>]

Hi, 
I am getting started on writing TLAPS proof. From my understanding, TLAPS doesn't support temporal operators, so I can prove eventual consistency etc. But for now I am starting on simple consistent counter that keeps track of count of elements in a set.

But when running the prover, it fails with

Zenon error: uncaught exception File "ext_tla.ml", line 1551, characters 15-21: Assertion failed

for a very simple init condition. Please let me know how to resolve this. Even though the prover says proved, additional theorems also fails with the same error

InductiveInvariant == count = Cardinality(elements) 

THEOREM InitProperty == Init => InductiveInvariant

    BY DEF Init, InductiveInvariant, Cardinality

The full TLA file and the full logs are below

------------------------- MODULE ConsistentCounter -------------------------

EXTENDS Naturals,FiniteSets

CONSTANT MAX_ELEMENTS, BUFFER_SIZE

VARIABLES elements, count, seq

vars == <<elements, count, seq>>

Init == /\ elements = {}
        /\ count = 0
        /\ seq = 0

Add == /\ \E e \in 1..MAX_ELEMENTS:
              /\ e \notin elements
              /\ seq < BUFFER_SIZE
              /\ elements' = elements \union {e}
              /\ seq' =  seq + 1
              /\ count' = Cardinality(elements) + 1

Remove == /\ \E e \in elements:
                 /\ seq < BUFFER_SIZE
                 /\ seq > 0
                 /\ elements' = elements \ {e}
                 /\ seq' =  seq + 1
                 /\ count' = Cardinality(elements) - 1

ConsistencyInvariant == \/ seq > 0
                        \/ (count = Cardinality(elements))

IsCountCorrect == (count = Cardinality(elements))

Next == \/ Add
        \/ Remove
        \/ UNCHANGED vars

Spec == Init /\ [][Next]_vars 

InductiveInvariant == count = Cardinality(elements) 

THEOREM InitProperty == Init => InductiveInvariant
    BY DEF Init, InductiveInvariant, Cardinality

\*THEOREM NextProperty == InductiveInvariant /\ Next => InductiveInvariant'

Full logs.

---------------- New Prover Launch --------------

\* TLAPM version 1.4.5 (commit 33809)
\* launched at 2023-03-30 15:51:15 with command line:
\* /usr/local/bin/tlapm --toolbox 0 0 --cleanfp -I /usr/local/lib/tlaps/ /Users/jp/.tlaplus/VideoCourse/ConsistentCounter.tla

(* fingerprints file "ConsistentCounter.tlaps/fingerprints" removed *)
@!!BEGIN
@!!type:obligation
@!!id:1
@!!loc:45:5:45:7
@!!status:to be proved
@!!END

@!!BEGIN
@!!type:obligationsnumber
@!!count:1
@!!END

** Unexpanded symbols: ---

@!!BEGIN
@!!type:obligation
@!!id:1
@!!loc:45:5:45:7
@!!status:being proved
@!!prover:smt
@!!meth:time-limit: 5
@!!obl:
ASSUME NEW CONSTANT MAX_ELEMENTS,
       NEW CONSTANT BUFFER_SIZE,
       NEW VARIABLE elements,
       NEW VARIABLE count,
       NEW VARIABLE seq
PROVE  (/\ elements = {}
        /\ count = 0
        /\ seq = 0)
       => count
          = (CHOOSE CS :
               CS
               = [T \in SUBSET elements |->
                    IF T = {} THEN 0 ELSE 1 + CS[T \ {CHOOSE x : x \in T}]])[elements]

@!!END

@!!BEGIN
@!!type:obligation
@!!id:1
@!!loc:45:5:45:7
@!!status:failed
@!!prover:smt
@!!meth:time-limit: 5; time-used: 5.0 (100%)
@!!reason:timeout
@!!already:false
@!!obl:
ASSUME NEW CONSTANT MAX_ELEMENTS,
       NEW CONSTANT BUFFER_SIZE,
       NEW VARIABLE elements,
       NEW VARIABLE count,
       NEW VARIABLE seq
PROVE  (/\ elements = {}
        /\ count = 0
        /\ seq = 0)
       => count
          = (CHOOSE CS :
               CS
               = [T \in SUBSET elements |->
                    IF T = {} THEN 0 ELSE 1 + CS[T \ {CHOOSE x : x \in T}]])[elements]

@!!END

Zenon error: uncaught exception File "ext_tla.ml", line 1551, characters 15-21: Assertion failed
@!!BEGIN
@!!type:obligation
@!!id:1
@!!loc:45:5:45:7
@!!status:proved
@!!prover:zenon
@!!meth:time-limit: 10; time-used: 0.0 (0%)
@!!already:false
@!!END

(* created new "ConsistentCounter.tlaps/ConsistentCounter.thy" *)
(* fingerprints written in "ConsistentCounter.tlaps/fingerprints" *)

    

-- 
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/170a3ae6-338d-40c4-8bf9-591fd8777ec1n%40googlegroups.com.