[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 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.Greetings,Michael---- MODULE VerySimpleCounterWrongLargeBranching ----EXTENDS IntegersVARIABLES ctlim == 2^25Invariant1 == ct \in IntInvariant2 == ct < limInit == ct \in (0 .. lim - 1)Inc(i) == ct + i =< lim /\ ct' = ct + iReset == ct = lim /\ ct' = 0Next == \/ \E i \in (1 .. 1000) : Inc(i) \/ Reset==== The config file is:INIT InitNEXT NextINVARIANT Invariant1INVARIANT Invariant2