Runner for event streams #44

andrey-kuprianov · 2021-04-26T12:33:36Z

This PR replaces the previous Runner which was based on Steps, with a new Runner that is based on Event streams.

The intention is to create a unified interface (event streams) that can be used both for unit-testing the implementation, as well as for model-based testing.

…he counterexample length

andrey-kuprianov · 2021-04-26T12:39:17Z

@vitorenesduarte , @romac , would be grateful to hear your comments on this.

@vitorenesduarte , this PR removes the previous TestRunner completely and I am not sure about that. What do you think, does it still make sense to keep it?

romac · 2021-04-26T13:25:28Z

Very nice, I like the little EventStream DSL!

There's one thing, where I am not quite sure about using Default to initialize the system. What if you want to initialize the same System multiple times with different parameters? With Default you have to introduce a new type for each system and implement Default for it, whereas if one could just supply a system you could handle any variations of initial system (maybe even dynamically) without introducing new types.

andrey-kuprianov · 2021-04-26T14:39:07Z

Glad you like the DSL, Romain!

In fact, originally it was that the system has to be supplied as one of the parameters; I've changed it to Default in f00acfe, because this made the usage of Runner shorter/simpler. I could revert this back; or, alternatively, provide an additional method, e.g. run_on_system.

romac · 2021-04-27T10:51:57Z

modelator/src/event.rs

@@ -288,12 +288,14 @@ impl<'a, System> Runner<'a, System> {
        &mut self,
        system: &mut System,
        stream: &mut dyn Iterator<Item = Event>,


This should also work without the need for a trait object (dyn Trait):

Suggested change

stream: &mut dyn Iterator<Item = Event>,

stream: impl Iterator<Item = Event>,

romac · 2021-04-27T10:54:09Z

I could revert this back; or, alternatively, provide an additional method, e.g. run_on_system.

The way you addressed this in 66211b3 looks good to me :)

romac · 2021-04-27T10:55:07Z

If you think it's useful, you can always add a run_with_default method which requires the Default bound and uses the default value of the system.

vitorenesduarte · 2021-04-28T13:14:24Z

modelator/src/error.rs

+    },
+
+    /// A error that occurs when a test fails.
+    #[error("Test failed: {message}\n   {location}")]


Similarly, should we use testand system in this error message?

vitorenesduarte · 2021-04-28T13:14:54Z

modelator/src/error.rs

    /// A `modelator` [enum@Error].
    #[error("Error while running modelator: {0}")]
    Modelator(Error),

    /// A error that occurs when a test fails.
-    #[error("Test failed on step {step_index}/{step_count}:\nsteps: {steps:#?}")]
+    #[error("Unhandled test: {test}")]


Should we use the test field in this error message?

vitorenesduarte · 2021-04-28T13:50:53Z

modelator/src/event.rs

@@ -45,11 +45,11 @@ pub enum Event {
    /// Process the abstract action, modifying the system state.
    Action(Box<dyn Any>),
    /// Expect the provided outcome of the last action.
-    Outcome(String),
+    Expect(String),


I wonder if these should be called TestSteps instead of Events. It wasn't immediately obvious to me what an Event was.

vitorenesduarte · 2021-04-28T14:01:28Z

modelator/src/event.rs

    /// Check the assertion about the abstract system state.
    Check(Box<dyn Any>),
    /// Expect exactly the provided abstract system state.
-    Expect(Box<dyn Any>),
+    Equal(Box<dyn Any>),


IIUC, this Event::Equal is the reason why we need StateHandler::read right?

I'm thinking that implementing StateHandler::read can be a lot of effort (and some users may not even need it). Not only users have to provide a way to go from an abstract state to a concrete one (the bare minimum), now they also need to provide the opposite transformation. Moreover, now users have to implement two traits, StateHandler and ActionHandler.

Overall, I would be in favor of simplifying things (probably because I don't understand why we had to complicate them in the first place): I would have a single trait that only has two methods, init and handle. This would already provide basic functionality. Then, we should also support more complicated setups for which this is not enough, but not at the cost of complicating the rest.

I just realized that what advocating for is very similar to the initial approach we had in the TestRunner:

modelator/modelator/src/runner.rs

Lines 8 to 14 in e3e859d

pub trait TestRunner<S> {

/// Executes the first step against the runner.

fn initial_step(&mut self, step: S) -> bool;

/// Executes each next step against the runner.

fn next_step(&mut self, step: S) -> bool;

}

andrey-kuprianov · 2021-04-28T16:44:58Z

Ha-ha, I am actually already in the process of bringing back the TestRunner :)

I also came to the conclusion that it's better to keep them both -- the runner for events, and the more simple variant as you've had it originally.

Now, why we need a more complex one, not all but a couple of reasons:

in the simple TestRunner the users have to process the states and actions themselves. In particular the actions is a headache.
on the contrary, in the more complex variant, the users need to implement state and action handlers, which they can easily reuse for unit testing. So we provide a nice way to construct unit tests, and the users get MBT for free on top. The alternative is that they need to write a fairly complicated logic themselves each time specifically for MBT.

Just to make it a bit more example-based: compare the hand-written state-checking logic here, which is also incomplete, with the transparent transformations from concrete to abstract states for ICS02 and ICS03.

I hope the difference speaks for itself.

andrey-kuprianov · 2021-04-29T07:12:50Z

Another reason, which I forgot to mention, and which is purely software engineering one: the TestRunner core functionality is too "thin": it does too little to justify it's existence. And exactly because it doesn't do enough of the useful things, this means it pushes them to the users.

andrey-kuprianov · 2021-04-29T15:30:04Z

This is really annoying: the errors when running cargo test for this PR stem not from the errors in the code, but from the interactions between different tests, and also between Apalache and TLC via mc.log. We can't progress without fixing #43 and #46

rnbguy

The commits look good. I added some small comments. But IMHO some internal codes need some refactoring maybe. Not just because of Rust idioms, but to simplify the API. But that should be a future milestone. I really like the Runner API.

rnbguy · 2021-07-26T23:16:58Z

modelator/src/event.rs

    outcome: String,
 }

-impl<'a, System> Default for Runner<'a, System> {
+impl<System: Debug> Default for EventRunner<System> {


Can we remove these redundant Default impls and ::new() fns. Instead derive Default maybe?

rnbguy · 2021-07-26T23:29:09Z

modelator/src/lib.rs

+///     assert!(run_tla_steps(tla_tests_file, tla_config_file, &options, &mut system).is_ok());
+/// }
+/// ```
+pub fn run_tla_steps<P, System, Step>(


Can we make run_tla_steps and run_tla_events convenient struct methods. The function bodies are very small and very direct anyway. Maybe something like this,

Setup::default() .set_options(&Options) .config_file(P) .tests_file(P) .run_tla_steps_on(&mut System)

and something similar for run_tla_events.

rnbguy · 2021-07-26T23:32:54Z

modelator/src/lib.rs

-///         Self::is_even(step.b)
+/// // We define StateHandlers that are able to initialize your SUT from
+/// // these abstract states, as well as to read them at any point in time.
+/// impl StateHandler<A> for NumberSystem {


Should we use the power of AsRef or Deref instead?

rnbguy · 2021-07-26T23:38:01Z

modelator/tests/integration/main.rs

+    }
+}
+
+impl ActionHandler<Action> for NumberSystem {


Why Action is generic type and Outcome is associated type? Action does not have trait bounds. We can make Action as an associated type too, no?

rnbguy · 2021-07-26T23:38:48Z

modelator/tests/integration/main.rs

+
+#[test]
+fn event_runner() {
+    let events = EventStream::new()


haha this is the best example !! so simple and short 👍

rnbguy · 2021-07-26T23:44:30Z

By the way, from what I understood, run_tla_steps and run_tla_events seem to have the same power. Is there anything fundamentally different about them?

rnbguy · 2021-07-27T00:06:30Z

Also, I saw some 'static and DeserializeOwned bounds here and there. Are these lifetimes sanitized? If it is not done yet, I can take a look later. It would remove unnecessary lifetime bounds.

andrey-kuprianov · 2021-07-27T06:29:16Z

By the way, from what I understood, run_tla_steps and run_tla_events seem to have the same power. Is there anything fundamentally different about them?

Well, fundamentally everything is the same;) It's the question of convenience. The first one is about StepRunner (I now think that StateRunner is a better name), and such API is probably better for small specs, where you only want an access to the state of a TLA+ model "as is". The second one is about EventRunner, where some parts of TLA+ state have predefined meaning, like action or actionOutcome (and this should be documented for sure!)

andrey-kuprianov · 2021-07-27T06:33:37Z

As all suggestions seem to be about refactoring and API improvements, I have pulled them in a separate issue #50; to be addressed in the next weeks.

@rnbguy thanks for the review!

andrey-kuprianov added 8 commits April 9, 2021 19:14

add action to integration tests

4b093dd

add integration test for event::Runner

7a00949

replace TestRunner with event::Runner

f00acfe

remove debug print

a163f59

disable caching temporarily to figure out the test failures

d11ac99

trying to figure out test failure reasons

058ee96

reduce MaxNumber to 6 for integration tests to avoid exceeding Apalac…

6f0038c

…he counterexample length

fix doctest

499c692

andrey-kuprianov requested review from romac and vitorenesduarte April 26, 2021 12:33

andrey-kuprianov self-assigned this Apr 26, 2021

use external system for event::Runner

66211b3

romac reviewed Apr 27, 2021

View reviewed changes

remove Default dep for systems

a5e8cb0

vitorenesduarte reviewed Apr 28, 2021

View reviewed changes

andrey-kuprianov added 4 commits April 29, 2021 13:08

improve the example SUT

2c834d6

clippy + fmt

6cbe9d6

bring back StepRunner

75e796b

cleanup

0334944

This was referenced May 7, 2021

Refactor MBT for ICS02 & ICS03 using new modelator Rust API informalsystems/hermes#812

Closed

Execute model checkers in a temporary directory #33

Closed

Merge branch 'main' into andrey/new-runner

7c3a7c4

andrey-kuprianov added 5 commits July 26, 2021 10:04

removed the tlc workaround that became useless with tempdirs

2f22feb

clippy

6958aa5

clippy

1a08d10

make Apalache default; disable TLC integration tests

78e3e29

fmt

1fdc8df

andrey-kuprianov mentioned this pull request Jul 26, 2021

Non-deterministic test failures & behaviour #43

Closed

andrey-kuprianov requested a review from rnbguy July 26, 2021 11:33

rnbguy reviewed Jul 26, 2021

View reviewed changes

andrey-kuprianov mentioned this pull request Jul 27, 2021

Possible refactoring and API improvements #50

Closed

andrey-kuprianov merged commit 748ea8e into main Jul 27, 2021

danwt deleted the andrey/new-runner branch January 18, 2022 14:14

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Runner for event streams #44

Runner for event streams #44

andrey-kuprianov commented Apr 26, 2021

andrey-kuprianov commented Apr 26, 2021

romac commented Apr 26, 2021

andrey-kuprianov commented Apr 26, 2021

romac Apr 27, 2021

romac commented Apr 27, 2021

romac commented Apr 27, 2021

vitorenesduarte Apr 28, 2021

vitorenesduarte Apr 28, 2021

vitorenesduarte Apr 28, 2021

vitorenesduarte Apr 28, 2021

vitorenesduarte Apr 28, 2021

andrey-kuprianov commented Apr 28, 2021 •

edited

Loading

andrey-kuprianov commented Apr 29, 2021

andrey-kuprianov commented Apr 29, 2021

rnbguy left a comment

rnbguy Jul 26, 2021

rnbguy Jul 26, 2021

rnbguy Jul 26, 2021

rnbguy Jul 26, 2021

rnbguy Jul 26, 2021

rnbguy commented Jul 26, 2021

rnbguy commented Jul 27, 2021

andrey-kuprianov commented Jul 27, 2021

andrey-kuprianov commented Jul 27, 2021

	stream: &mut dyn Iterator<Item = Event>,
	stream: impl Iterator<Item = Event>,

	pub trait TestRunner<S> {
	/// Executes the first step against the runner.
	fn initial_step(&mut self, step: S) -> bool;

	/// Executes each next step against the runner.
	fn next_step(&mut self, step: S) -> bool;
	}

Runner for event streams #44

Runner for event streams #44

Conversation

andrey-kuprianov commented Apr 26, 2021

andrey-kuprianov commented Apr 26, 2021

romac commented Apr 26, 2021

andrey-kuprianov commented Apr 26, 2021

Choose a reason for hiding this comment

romac commented Apr 27, 2021

romac commented Apr 27, 2021

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

andrey-kuprianov commented Apr 28, 2021 • edited Loading

andrey-kuprianov commented Apr 29, 2021

andrey-kuprianov commented Apr 29, 2021

rnbguy left a 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

rnbguy commented Jul 26, 2021

rnbguy commented Jul 27, 2021

andrey-kuprianov commented Jul 27, 2021

andrey-kuprianov commented Jul 27, 2021

andrey-kuprianov commented Apr 28, 2021 •

edited

Loading