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

*From*: Michael Leuschel <leus...@xxxxxxxxxxxxxxxxxxxxx>*Date*: Sun, 06 Dec 2015 22:42:55 +0100*References*: <dbc52c84-b6ce-4326-aeec-a7c17dd257c0@googlegroups.com> <33ED3621-4D95-4167-9232-9404968DD8E7@gmail.com> <02b4212f-9e09-4759-96a6-d73e7ae0881f@googlegroups.com> <708CF982-1782-422F-8445-6C87C4E7D8D6@gmail.com> <57658c49-b05f-47df-9a41-df4992c873bc@googlegroups.com> <5f44d273-19c0-4086-973c-bbb620e7777b@googlegroups.com> <4ff7ce2d-b955-4953-b58b-8221b6594313@googlegroups.com>

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 |

**Follow-Ups**:**Re: [tlaplus] TLA+ logic***From:*Ron Pressler

**References**:**TLA+ logic***From:*Ron Pressler

**Re: [tlaplus] TLA+ logic***From:*Stephan Merz

**Re: [tlaplus] TLA+ logic***From:*Ron Pressler

**Re: [tlaplus] TLA+ logic***From:*Stephan Merz

**Re: [tlaplus] TLA+ logic***From:*Leslie Lamport

**Re: [tlaplus] TLA+ logic***From:*Chris Newcombe

**Re: [tlaplus] TLA+ logic***From:*Ron Pressler

- Prev by Date:
**Re: [tlaplus] Recursive definitions of higher-order operators** - Next by Date:
**Re: Recursive definitions of higher-order operators** - Previous by thread:
**Re: [tlaplus] TLA+ logic** - Next by thread:
**Re: [tlaplus] TLA+ logic** - Index(es):