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

Re: [tlaplus] TLA+ logic

Hi Ron,

Do you have a TLA+ spec of the flawed sorting algorithm ?

On 6 Dec 2015, at 18:39, Ron Pressler <r...@xxxxxxxxxxxxxxxxxxx> wrote:

 (a very interesting bug -- which only occurs on very large arrays -- was found in Java's sorting algorithm using the KeY project for symbolic execution) 

I am also not sure what kind of symbolic execution you are after.
The answer of Leslie Lamport refers to BDD-based symbolic model checking.
The ProB tool can be used for constraint-based symbolic execution, which in turn can be used for bounded model checking or test-case generation.
Below is an artificial example, where the ProB bounded model checker finds a counter-example (Init with ct=33554431 followed by Inc(1)) immediately by solving the corresponding constraints, but the explicit model checking with TLC reports: "Too many possible next states…"
Is this the kind of symbolic execution you are after ?

Of course, ProB’s support for TLA+ is unfortunately still limited (the TLA+ specs have to go through a typechecker, no support for user-defined recursive operators,… ); but we would be happy to try out more involved examples.


---- MODULE VerySimpleCounterWrongLargeBranching ----
EXTENDS Integers
lim == 2^25
Invariant1 == ct \in Int
Invariant2 == ct < lim
Init == ct \in (0 .. lim - 1)

Inc(i) == ct + i =< lim
/\ ct' = ct + i

Reset == ct = lim
/\ ct' = 0

Next == \/ \E i \in (1 .. 1000) : Inc(i)
\/ Reset

The config file is:
INVARIANT Invariant1
INVARIANT Invariant2