From 7e6b81f4519a91753e574962dd94aa83003b434b Mon Sep 17 00:00:00 2001
From: Jonathan Nadal <jon.nadal@gmail.com>
Date: Sat, 11 Jul 2020 08:22:02 -0700
Subject: [PATCH 1/2] upgrade to stateright 0.10.0

The following changes in particular may be helpful:

- Fixes Explorer.
- Introduces `System::History`.
- Introduces `assert_properties` helper.
---
 Cargo.toml              |  4 ++--
 src/stateright_tests.rs | 15 ++++++++-------
 2 files changed, 10 insertions(+), 9 deletions(-)

diff --git a/Cargo.toml b/Cargo.toml
index 80feb54..bc9278a 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -22,5 +22,5 @@ serde = "1.0"
 futures = "0.3.5"
 pretty_env_logger = "0.4"
 bit-set = "0.5.2"
-stateright = "0.9.0"
-num_cpus = "1.13.0"
\ No newline at end of file
+stateright = "0.10.0"
+num_cpus = "1.13.0"
diff --git a/src/stateright_tests.rs b/src/stateright_tests.rs
index 40cc742..5100b08 100644
--- a/src/stateright_tests.rs
+++ b/src/stateright_tests.rs
@@ -122,6 +122,7 @@ impl ConcordeSystem {
 
 impl System for ConcordeSystem {
     type Actor = ConcordeActor;
+    type History = ();
     fn actors(&self) -> Vec<Self::Actor> {
         self.peer_proposals.clone().into_iter()
         .map(|(id, proposals_to_make)| ConcordeActor { id, proposals_to_make})
@@ -137,7 +138,7 @@ impl System for ConcordeSystem {
             Property::always("trivial", |_, _| true),
         ]
     }
-    fn within_boundary(&self, state: &SystemState<Self::Actor>) -> bool {
+    fn within_boundary(&self, state: &SystemState<Self>) -> bool {
         lattice_agreement_boundary(self, state)
     }
 
@@ -152,7 +153,7 @@ impl System for ConcordeSystem {
 
 fn lattice_agreement_validity(
     _model: &SystemModel<ConcordeSystem>,
-    state: &SystemState<ConcordeActor>,
+    state: &SystemState<ConcordeSystem>,
 ) -> bool {
     let mut all_proposed_added_peers = BTreeSet::new();
     let mut all_proposed_removed_peers = BTreeSet::new();
@@ -197,7 +198,7 @@ fn lattice_agreement_validity(
 
 fn lattice_agreement_consistency(
     _model: &SystemModel<ConcordeSystem>,
-    state: &SystemState<ConcordeActor>,
+    state: &SystemState<ConcordeSystem>,
 ) -> bool {
     for part in state.actor_states.iter() {
         let h = &part.learned_history;
@@ -220,7 +221,7 @@ fn lattice_agreement_consistency(
 // (Luckily this is how the liveness of lattice agreement is specified)
 fn lattice_agreement_liveness(
     model: &SystemModel<ConcordeSystem>,
-    state: &SystemState<ConcordeActor>,
+    state: &SystemState<ConcordeSystem>,
 ) -> bool {
     for part in state.actor_states.iter() {
         for actor in model.actors.iter() {
@@ -238,7 +239,7 @@ fn lattice_agreement_liveness(
 // Returning false here means "past the boundary, stop exploring"
 fn lattice_agreement_boundary(
     system: &ConcordeSystem,
-    state: &SystemState<ConcordeActor>,
+    state: &SystemState<ConcordeSystem>,
 ) -> bool {
     for part in state.actor_states.iter() {
         match system.peer_proposals.get(&part.id) {
@@ -382,7 +383,7 @@ fn msg_to_string(msg: &Msg) -> String {
     }
 }
 
-fn print_system_state(state: &SystemState<ConcordeActor>) {
+fn print_system_state(state: &SystemState<ConcordeSystem>) {
     // println!("    state at depth {}:", state.depth);
     for part in state.actor_states.iter() {
         println!("        participant {}:", usize::from(part.id));
@@ -446,7 +447,7 @@ fn print_system_action_opt(action: &Option<SystemAction<Msg>>) {
 
 fn print_path(
     path: Path<
-        SystemState<ConcordeActor>,
+        SystemState<ConcordeSystem>,
         SystemAction<Msg>,
     >,
 ) {

From 817837e3c76b238e7f08cb69e196f71b3fac3b20 Mon Sep 17 00:00:00 2001
From: Jonathan Nadal <jon.nadal@gmail.com>
Date: Sat, 11 Jul 2020 12:29:03 -0700
Subject: [PATCH 2/2] test: sometimes sends messages

I loaded `ConcordeSystem::simple()` into Stateright's Explorer and
noticed that the latest version isn't sending any messages. This commit
simply adds a regression test, which is currently failing.

The commit also adds `#derive(Clone)` to `ConcordeActor` and
`ConcordeSystem` as those are necessary for using the Explorer.
---
 src/stateright_tests.rs | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/src/stateright_tests.rs b/src/stateright_tests.rs
index 5100b08..86db29c 100644
--- a/src/stateright_tests.rs
+++ b/src/stateright_tests.rs
@@ -18,6 +18,7 @@ type ObjLE = pergola::LatticeElt<ObjLD>;
 type Msg = Message<ObjLD, Id>;
 type Part = Participant<ObjLD, Id>;
 
+#[derive(Clone)]
 struct ConcordeActor {
     // This 'id' field seems a little redundant but we need it to fish the id of
     // an actor out of the System<> struct, which doesn't otherwise provide a
@@ -95,6 +96,7 @@ impl Actor for ConcordeActor {
     }
 }
 
+#[derive(Clone)]
 struct ConcordeSystem {
     peer_proposals: BTreeMap<Id, Vec<StateLE<ObjLD, Id>>>
 }
@@ -135,6 +137,7 @@ impl System for ConcordeSystem {
             Property::always("valid", lattice_agreement_validity),
             Property::always("consistent", lattice_agreement_consistency),
             Property::eventually("live", lattice_agreement_liveness),
+            Property::sometimes("sends messages", |_, state: &SystemState<ConcordeSystem>| !state.network.is_empty()),
             Property::always("trivial", |_, _| true),
         ]
     }
@@ -288,6 +291,8 @@ fn model_check() {
             }
         }
     }
+
+    checker.assert_example("sends messages");
 }
 
 //---------------------------------------------------------