[tlaplus] Re: Zenon error: uncaught exception File "ext

On Thursday, March 30, 2023 at 7:01:28 PM UTC-4 jayaprabhakar k wrote:

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" *)

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