[WIP] State machine support #84

AltSysrq · 2018-08-22T04:11:45Z

Something I've been working on here and there for a while, originally suggested in #28.

As noted in the first commit, this absolutely needs more tests and is probably still a bit deficient on documentation. I wanted to get this up now though to solicit opinions on the model/ergonomics now that the implementation is basically functional.

I'd recommend starting by reading the (still incomplete) tutorial and then the syntax docs above it.

@Centril I'd appreciate your thoughts when you have time.

Still needs more documentation and definitely more tests.

Centril

Nice work :) Here are some initial thoughts.

Centril · 2018-08-22T10:49:56Z

src/test_runner/errors.rs

@@ -92,7 +92,7 @@ impl<T : fmt::Debug> fmt::Display for TestError<T> {
            TestError::Abort(ref why) =>
                write!(f, "Test aborted: {}", why),
            TestError::Fail(ref why, ref what) =>
-                write!(f, "Test failed: {}; minimal failing input: {:?}",
+                write!(f, "Test failed: {}; minimal failing input: {:#?}",


Hmm; this is a non-trivial change in proptest wrt. UX;
While it will it will help for complex structures (because they would have overflowed the screen horizontally and so the terminal would have line-split...) I think it will also be less great for simple structs and tuples.

Centril · 2018-08-22T10:56:25Z

examples/state_machine_v1.rs

+#[macro_use]
+extern crate proptest;
+
+use std::cmp;


Any specific reason to do cmp::Ord? The trait should be well know so Ord seems simpler.

Centril · 2018-08-22T10:59:47Z

examples/state_machine_v1.rs

+    // We define a strategy for our starting state. Here, we always start with
+    // an empty heap.
+    fn initial_heap_strategy<T : cmp::Ord + fmt::Debug + Clone>
+        () -> impl Strategy<Value = MyHeapState<T>>


Should probably stick to a consistent style wrt. where or direct bounds?
Also, running rustfmt after merging the PR would be good (on the whole of proptest).

Centril · 2018-08-22T11:04:19Z

examples/state_machine_v1.rs

+        fn push(&mut state, value: T) {
+            // Add it to the heap...
+            state.heap.push(value.clone());
+            // ... and also the Vec where we track what the heap contains.


s/track what/track of what/

Centril · 2018-08-22T11:08:34Z

examples/state_machine_v1.rs

+        fn pop(&mut state) {
+            let was_empty = state.heap.is_empty();
+
+            match state.heap.pop() {


perhaps use if let here to reduce rightward drift?

Centril · 2018-08-22T12:40:16Z

src/state_machine.rs

+    /// the value.
+    pub fn new(mutation_strategy: impl Strategy<Value = Box<dyn Mutator<S>>> + 'static,
+               invariants: Arc<dyn Fn (&mut S) -> TestCaseResult>) -> Self {
+        StateMachine {


Self { .. }

Centril · 2018-08-22T12:50:16Z

src/state_machine.rs

+    pub fn run(mut self) -> Result<S, TestCaseError> {
+        if self.trace {
+            println!("initial state: {:?}", self.state);
+            println!("check initial invariants");


A thought for later: It might be nice to change from using println to use some more principled logging facility that users can control. I think the quickcheck crate does this. But this is out of scope for this PR.

Centril · 2018-08-22T12:51:40Z

src/state_machine.rs

+    /// Mutate `state`.
+    ///
+    /// This effectively consumes `self`, but it is passed as a mutable
+    /// reference so that this trait is object-safe and so that the mutator can


Add a test that asserts object safety.

Centril · 2018-08-22T12:55:26Z

src/state_machine.rs

+    function: Option<F>,
+    arguments: Option<A>,
+    formatted_arguments: Option<Cow<'static, str>>,
+    name: &'static str,


These fields are in common from the previous struct... Reuse?

Centril · 2018-08-22T12:56:33Z

src/state_machine.rs

+        let args = self.arguments.take().expect("Mutator applied more than once");
+        if self.formatted_arguments.is_none() {
+            self.formatted_arguments = Some(Cow::Owned(format!("{:?}", args)));
+        }


This bit is identical from DirectMutator; refactor?

Centril · 2018-08-22T13:51:24Z

Additional thoughts:

The base of this is quite nice.
I wonder if sugar should be added for preconditions of mutators (they can easily be added as ifs in each mutator but sugar could be nice...). This would model the fact that in state machines, after visiting some state nodes, a state machine may enter a phase which causes it to never enter those previous state nodes.
Sugar for post conditions could also be nice. You could add optional require and ensure clauses to each mutator to do this and the previous point.
Is "mutation" the right word? Other words to consider "command", "action". Tho perhaps "mutation" is the rustic word :)
The major question for me is whether and how this can be used for tests involving concurrent situations such as async or involving mutexes and so on... In particular, can we do the things in http://scalacheck.org/files/scaladays2014/#27 and the following slides?

In particular, there's the question of symbolic vs. dynamic execution (see https://medium.com/@jlouis666/breaking-erlang-maps-2-362730a91400 for a discussion). In the blog post, they note that they generate the command sequence (and I assume that would include delegated bits too) before invoking any of the commands.

From reading the code in this PR I'm not 100% sure what is done wrt. symbolic / dynamic execution, but I think that the command structure, including delegates are generated before any mutations actually occur (which is good). Could you say a few words about this? I think it would be good to include in the documentation or at least the code a bit about the high level logic of how the execution model works possibly including some diagrams / pictures or ascii art as in the medium blog post.

I think it would be good to have some test cases for concurrent situations.

Eh2406 · 2019-06-14T21:26:24Z

I was working on a data structure in Cargos internals and remembered this work. How is it going? What are the next steps?

AltSysrq · 2019-06-23T16:27:41Z

To be honest, I haven't really done anything here since I made the PR. IIRC I ran into some fundamental flaw in the way this is designed and put it on the backburner, but I've forgotten what that was now.

zmitchell · 2019-10-22T17:56:52Z

I'd be interested in continuing work on this if someone is able to mentor me

Initial implementation of state machine support.

9b54207

Still needs more documentation and definitely more tests.

Centril reviewed Aug 22, 2018

View reviewed changes

Eh2406 mentioned this pull request Aug 22, 2018

Thoughts on README in no particular order blt/bughunt-rust#2

Open

Eh2406 mentioned this pull request Sep 16, 2018

use proptest to fuzz the resolver rust-lang/cargo#5921

Merged

14 tasks

tzemanovic mentioned this pull request Jan 3, 2022

[WIP] alternative state machine support #257

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[WIP] State machine support #84

[WIP] State machine support #84

AltSysrq commented Aug 22, 2018

Centril left a comment

Centril Aug 22, 2018 •

edited

Centril Aug 22, 2018

Centril Aug 22, 2018

Centril Aug 22, 2018

Centril Aug 22, 2018

Centril Aug 22, 2018

Centril Aug 22, 2018

Centril Aug 22, 2018

Centril Aug 22, 2018

Centril Aug 22, 2018

Centril commented Aug 22, 2018

Eh2406 commented Jun 14, 2019

AltSysrq commented Jun 23, 2019

zmitchell commented Oct 22, 2019

[WIP] State machine support #84

Are you sure you want to change the base?

[WIP] State machine support #84

Conversation

AltSysrq commented Aug 22, 2018

Centril left a comment

Choose a reason for hiding this comment

Centril Aug 22, 2018 • edited

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Centril commented Aug 22, 2018

Eh2406 commented Jun 14, 2019

AltSysrq commented Jun 23, 2019

zmitchell commented Oct 22, 2019

Centril Aug 22, 2018 •

edited