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..86db29c 100644 --- a/src/stateright_tests.rs +++ b/src/stateright_tests.rs @@ -18,6 +18,7 @@ type ObjLE = pergola::LatticeElt; type Msg = Message; type Part = Participant; +#[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>> } @@ -122,6 +124,7 @@ impl ConcordeSystem { impl System for ConcordeSystem { type Actor = ConcordeActor; + type History = (); fn actors(&self) -> Vec { self.peer_proposals.clone().into_iter() .map(|(id, proposals_to_make)| ConcordeActor { id, proposals_to_make}) @@ -134,10 +137,11 @@ 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| !state.network.is_empty()), Property::always("trivial", |_, _| true), ] } - fn within_boundary(&self, state: &SystemState) -> bool { + fn within_boundary(&self, state: &SystemState) -> bool { lattice_agreement_boundary(self, state) } @@ -152,7 +156,7 @@ impl System for ConcordeSystem { fn lattice_agreement_validity( _model: &SystemModel, - state: &SystemState, + state: &SystemState, ) -> bool { let mut all_proposed_added_peers = BTreeSet::new(); let mut all_proposed_removed_peers = BTreeSet::new(); @@ -197,7 +201,7 @@ fn lattice_agreement_validity( fn lattice_agreement_consistency( _model: &SystemModel, - state: &SystemState, + state: &SystemState, ) -> bool { for part in state.actor_states.iter() { let h = &part.learned_history; @@ -220,7 +224,7 @@ fn lattice_agreement_consistency( // (Luckily this is how the liveness of lattice agreement is specified) fn lattice_agreement_liveness( model: &SystemModel, - state: &SystemState, + state: &SystemState, ) -> bool { for part in state.actor_states.iter() { for actor in model.actors.iter() { @@ -238,7 +242,7 @@ fn lattice_agreement_liveness( // Returning false here means "past the boundary, stop exploring" fn lattice_agreement_boundary( system: &ConcordeSystem, - state: &SystemState, + state: &SystemState, ) -> bool { for part in state.actor_states.iter() { match system.peer_proposals.get(&part.id) { @@ -287,6 +291,8 @@ fn model_check() { } } } + + checker.assert_example("sends messages"); } //--------------------------------------------------------- @@ -382,7 +388,7 @@ fn msg_to_string(msg: &Msg) -> String { } } -fn print_system_state(state: &SystemState) { +fn print_system_state(state: &SystemState) { // println!(" state at depth {}:", state.depth); for part in state.actor_states.iter() { println!(" participant {}:", usize::from(part.id)); @@ -446,7 +452,7 @@ fn print_system_action_opt(action: &Option>) { fn print_path( path: Path< - SystemState, + SystemState, SystemAction, >, ) {