Add option to fail fast by waiting for a subset of discoveries (#71)

src/checker.rs

@@ -11,6 +11,7 @@ mod rewrite_plan;
 mod simulation;
 mod visitor;
 
+use crate::has_discoveries::HasDiscoveries;
 use crate::report::{ReportData, ReportDiscovery, Reporter};
 use crate::{Expectation, Fingerprint, Model};
 use std::collections::{BTreeMap, HashMap};
@@ -69,6 +70,7 @@ pub struct CheckerBuilder<M: Model> {
     target_max_depth: Option<NonZeroUsize>,
     thread_count: usize,
     visitor: Option<Box<dyn CheckerVisitor<M> + Send + Sync>>,
+    finish_when: HasDiscoveries,
     timeout: Option<Duration>,
 }
 impl<M: Model> CheckerBuilder<M> {
@@ -80,6 +82,7 @@ impl<M: Model> CheckerBuilder<M> {
             symmetry: None,
             thread_count: 1,
             visitor: None,
+            finish_when: HasDiscoveries::All,
             timeout: None,
         }
     }
@@ -233,6 +236,14 @@ impl<M: Model> CheckerBuilder<M> {
         }
     }
 
+    /// When to finish the checker run.
+    pub fn finish_when(self, has_discoveries: HasDiscoveries) -> Self {
+        Self {
+            finish_when: has_discoveries,
+            ..self
+        }
+    }
+
     /// Sets the number of states that the checker should aim to generate. For performance reasons
     /// the checker may exceed this number, but it will never generate fewer states if more exist.
     pub fn target_state_count(self, count: usize) -> Self {

src/checker/bfs.rs

@@ -43,7 +43,8 @@ where
         let target_max_depth = options.target_max_depth;
         let thread_count = options.thread_count;
         let visitor = Arc::new(options.visitor);
-        let property_count = model.properties().len();
+        let finish_when = Arc::new(options.finish_when);
+        let properties = Arc::new(model.properties());
 
         let init_states: Vec<_> = model
             .init_states()
@@ -89,6 +90,8 @@ where
         for t in 0..thread_count {
             let model = Arc::clone(&model);
             let visitor = Arc::clone(&visitor);
+            let finish_when = Arc::clone(&finish_when);
+            let properties = Arc::clone(&properties);
             let mut job_broker = job_broker.clone();
             let state_count = Arc::clone(&state_count);
             let max_depth = Arc::clone(&max_depth);
@@ -128,7 +131,10 @@ where
                                 target_max_depth,
                                 &max_depth,
                             );
-                            if discoveries.len() == property_count {
+                            if finish_when.matches(
+                                &discoveries.iter().map(|r| *r.key()).collect(),
+                                &properties,
+                            ) {
                                 log::debug!(
                                     "{}: Discovery complete. Shutting down... gen={}",
                                     t,

src/checker/dfs.rs

@@ -42,7 +42,8 @@ where
         let target_max_depth = options.target_max_depth;
         let thread_count = options.thread_count;
         let visitor = Arc::new(options.visitor);
-        let property_count = model.properties().len();
+        let finish_when = Arc::new(options.finish_when);
+        let properties = Arc::new(model.properties());
 
         let init_states: Vec<_> = model
             .init_states()
@@ -64,7 +65,7 @@ where
         });
         let ebits = {
             let mut ebits = EventuallyBits::new();
-            for (i, p) in model.properties().iter().enumerate() {
+            for (i, p) in properties.iter().enumerate() {
                 if let Property {
                     expectation: Expectation::Eventually,
                     ..
@@ -92,6 +93,8 @@ where
         for t in 0..thread_count {
             let model = Arc::clone(&model);
             let visitor = Arc::clone(&visitor);
+            let finish_when = Arc::clone(&finish_when);
+            let properties = Arc::clone(&properties);
             let mut job_broker = job_broker.clone();
             let state_count = Arc::clone(&state_count);
             let max_depth = Arc::clone(&max_depth);
@@ -132,7 +135,10 @@ where
                                 &max_depth,
                                 symmetry,
                             );
-                            if discoveries.len() == property_count {
+                            if finish_when.matches(
+                                &discoveries.iter().map(|r| *r.key()).collect(),
+                                &properties,
+                            ) {
                                 log::debug!(
                                     "{}: Discovery complete. Shutting down... gen={}",
                                     t,

src/checker/simulation.rs

@@ -106,6 +106,8 @@ where
         let target_max_depth = options.target_max_depth;
         let visitor = Arc::new(options.visitor);
         let property_count = model.properties().len();
+        let finish_when = Arc::new(options.finish_when);
+        let properties = Arc::new(model.properties());
 
         let state_count = Arc::new(AtomicUsize::new(0));
         let max_depth = Arc::new(AtomicUsize::new(0));
@@ -137,6 +139,8 @@ where
         for t in 0..options.thread_count {
             let model = Arc::clone(&model);
             let visitor = Arc::clone(&visitor);
+            let finish_when = Arc::clone(&finish_when);
+            let properties = Arc::clone(&properties);
             let state_count = Arc::clone(&state_count);
             let max_depth = Arc::clone(&max_depth);
             let discoveries = Arc::clone(&discoveries);
@@ -171,7 +175,10 @@ where
                             // Check whether we have found everything.
                             // All threads should reach this check and have the same result,
                             // leading them all to shut down together.
-                            if discoveries.len() == property_count {
+                            if finish_when.matches(
+                                &discoveries.iter().map(|r| *r.key()).collect(),
+                                &properties,
+                            ) {
                                 log::debug!("{}: Discovery complete. Shutting down...", t,);
                                 return;
                             }

src/has_discoveries.rs

@@ -0,0 +1,42 @@
+use std::collections::BTreeSet;
+
+use crate::{Model, Property};
+
+#[derive(Debug, Clone)]
+pub enum HasDiscoveries {
+    /// Wait for all discoveries to be made.
+    All,
+    /// Any, whatever is first.
+    Any,
+    /// Any, that counts as a failure.
+    AnyFailures,
+    /// Wait for all failures.
+    AllFailures,
+    /// All of a given set.
+    AllOf(BTreeSet<&'static str>),
+    /// Any of a given set.
+    AnyOf(BTreeSet<&'static str>),
+}
+
+impl HasDiscoveries {
+    pub fn matches<M: Model>(
+        &self,
+        discoveries: &BTreeSet<&'static str>,
+        properties: &[Property<M>],
+    ) -> bool {
+        match self {
+            HasDiscoveries::All => discoveries.len() == properties.len(),
+            HasDiscoveries::Any => !discoveries.is_empty(),
+            HasDiscoveries::AnyFailures => properties
+                .iter()
+                .filter(|prop| prop.expectation.discovery_is_failure())
+                .any(|prop| discoveries.contains(prop.name)),
+            HasDiscoveries::AllFailures => properties
+                .iter()
+                .filter(|prop| prop.expectation.discovery_is_failure())
+                .all(|prop| discoveries.contains(prop.name)),
+            HasDiscoveries::AllOf(props) => props.iter().all(|prop| discoveries.contains(prop)),
+            HasDiscoveries::AnyOf(props) => props.iter().any(|prop| discoveries.contains(prop)),
+        }
+    }
+}

src/lib.rs

@@ -134,16 +134,19 @@
 #[warn(anonymous_parameters)]
 #[warn(missing_docs)]
 mod checker;
+mod has_discoveries;
 mod job_market;
 pub mod report;
 use std::fmt::Debug;
 use std::hash::{Hash, Hasher};
+use std::ops::Add;
 
 #[cfg(test)]
 mod test_util;
 
 pub mod actor;
 pub use checker::*;
+pub use has_discoveries::HasDiscoveries;
 pub mod semantics;
 pub mod util;
 
@@ -325,6 +328,16 @@ pub enum Expectation {
     Sometimes,
 }
 
+impl Expectation {
+    pub const fn discovery_is_failure(&self) -> bool {
+        match self {
+            Expectation::Always => true,
+            Expectation::Eventually => true,
+            Expectation::Sometimes => false,
+        }
+    }
+}
+
 /// A state identifier. See [`fingerprint`].
 type Fingerprint = std::num::NonZeroU64;