[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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



By the way if I import TLAPS then write your property as:

THEOREM InitProperty == Init => InductiveInvariant
    BY Zenon DEFS Cardinality, Init, InductiveInvariant

then it checks a lot faster since it doesn't have to wait for the other provers to fail.

Andrew

On Friday, March 31, 2023 at 8:20:58 AM UTC-4 Andrew Helwer wrote:
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.

Andrew

On 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/202210041448

Andrew

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

    









--
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/66cf43af-bf68-483c-b577-ab90fe364efcn%40googlegroups.com.