Oh I lied, I'm just bad at reading. Yes I see that error. Weirdly the proof then succeeds. Don't know whether it actually succeeded or falsely succeeded.AndrewOn Friday, March 31, 2023 at 8:15:24 AM UTC-4 Andrew Helwer wrote:I tested it with the 1.5.0 prerelease on Linux and did not see that error: https://github.com/tlaplus/tlapm/releases/tag/202210041448AndrewOn 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 = 0Add == /\ \E e \in 1..MAX_ELEMENTS:
/\ e \notin elements
/\ seq < BUFFER_SIZE
/\ elements' = elements \union {e}
/\ seq' = seq + 1
/\ count' = Cardinality(elements) + 1Remove == /\ \E e \in elements:
/\ seq < BUFFER_SIZE
/\ seq > 0
/\ elements' = elements \ {e}
/\ seq' = seq + 1
/\ count' = Cardinality(elements) - 1ConsistencyInvariant == \/ seq > 0
\/ (count = Cardinality(elements))IsCountCorrect == (count = Cardinality(elements))
Next == \/ Add
\/ Remove
\/ UNCHANGED varsSpec == 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" *)