Stateright

Stateright is a library for specifying actor systems and validating invariants. It features an embedded model checker that can verify both abstract models and real systems.

Examples

As a simple example of an abstract model, we can indicate how to play a sliding puzzle game. Running the model checker against a false invariant indicating that the game is unsolvable results in the discovery of a counterexample: a sequence of steps that does solve the game.

```rust use stateright::*;

[derive(Clone, Debug, Eq, PartialEq)]

enum Slide { Down, Up, Right, Left }

let puzzle = QuickMachine { initstates: || vec![vec![1, 4, 2, 3, 5, 8, 6, 7, 0]], actions: |, actions| { actions.append(&mut vec![ Slide::Down, Slide::Up, Slide::Right, Slide::Left ]); }, nextstate: |laststate, action| { let empty = laststate.iter().position(|x| *x == 0).unwrap(); let emptyy = empty / 3; let emptyx = empty % 3; let maybefrom = match action { Slide::Down if emptyy > 0 => Some(empty - 3), // above Slide::Up if emptyy < 2 => Some(empty + 3), // below Slide::Right if emptyx > 0 => Some(empty - 1), // left Slide::Left if emptyx < 2 => Some(empty + 1), // right _ => None }; maybefrom.map(|from| { let mut nextstate = laststate.clone(); nextstate[empty] = laststate[from]; nextstate[from] = 0; nextstate }) } }; let solved = vec![0, 1, 2, 3, 4, 5, 6, 7, 8]; let mut checker = puzzle.checker(|, state| { state != &solved }); asserteq!(checker.check(100), CheckResult::Fail { state: solved.clone() }); asserteq!(checker.path_to(&solved), vec![ (vec![1, 4, 2, 3, 5, 8, 6, 7, 0], Slide::Down), (vec![1, 4, 2, 3, 5, 0, 6, 7, 8], Slide::Right), (vec![1, 4, 2, 3, 0, 5, 6, 7, 8], Slide::Down), (vec![1, 0, 2, 3, 4, 5, 6, 7, 8], Slide::Right)]); ```

See the examples directory for additional state machines, such as an actor based Single Decree Paxos cluster and an abstract two phase commit state machine.

To model check, run:

sh cargo run --release --example 2pc 3 # 2 phase commit, 3 resource managers cargo run --release --example paxos check 2 # paxos, 2 clients cargo run --release --example wor check 3 # write-once register, 3 clients

Stateright also includes a simple runtime for executing an actor state machine mapping messages to JSON over UDP:

sh cargo run --example paxos spawn

Performance

To benchmark model checking speed, run with larger state spaces:

sh cargo run --release --example 2pc 8 cargo run --release --example paxos check 4 cargo run --release --example wor check 6

Contributing

1. Clone the repository: sh git clone https://github.com/stateright/stateright.git cd stateright
2. Install the latest version of rust: sh rustup update || (curl https://sh.rustup.rs -sSf | sh)
3. Run the tests: sh cargo test && cargo test --examples
4. Review the docs: sh cargo doc --open
5. Explore the code: sh $EDITOR src/ # src/lib.rs is a good place to start
6. If you would like to share improvements, please fork the library, push changes to your fork, and send a pull request.

License

Copyright 2018 Jonathan Nadal and made available under the MIT License.