| Hi Ron, Do you have a TLA+ spec of the flawed sorting algorithm ?
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 Integers VARIABLES ct 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: INIT Init NEXT Next INVARIANT Invariant1 INVARIANT Invariant2 |