Add in and out degree for states

src/checker.rs

@@ -11,7 +11,7 @@ mod rewrite_plan;
 mod visitor;
 
 use crate::report::{ReportData, ReportDiscovery, Reporter};
-use crate::{Expectation, Model, Fingerprint};
+use crate::{Expectation, Fingerprint, Model};
 use std::collections::HashMap;
 use std::fmt::{Debug, Display};
 use std::hash::Hash;
@@ -274,6 +274,14 @@ pub trait Checker<M: Model> {
     /// Indicates the maximum depth that has been explored.
     fn max_depth(&self) -> usize;
 
+    /// List of out degree of each state.
+    /// The out degree is the number of actions generated by the state.
+    fn out_degrees(&self) -> Vec<usize>;
+
+    /// List of in degree of each state.
+    /// The in degree is the number of actions that lead into the state.
+    fn in_degrees(&self) -> Vec<usize>;
+
     /// Returns a map from property name to corresponding "discovery" (indicated
     /// by a [`Path`]).
     fn discoveries(&self) -> HashMap<&'static str, Path<M::State, M::Action>>;
@@ -308,6 +316,8 @@ pub trait Checker<M: Model> {
                 total_states: self.state_count(),
                 unique_states: self.unique_state_count(),
                 max_depth: self.max_depth(),
+                out_degrees: self.out_degrees(),
+                in_degrees: self.in_degrees(),
                 duration: method_start.elapsed(),
                 done: false,
             });
@@ -317,6 +327,8 @@ pub trait Checker<M: Model> {
             total_states: self.state_count(),
             unique_states: self.unique_state_count(),
             max_depth: self.max_depth(),
+            out_degrees: self.out_degrees(),
+            in_degrees: self.in_degrees(),
             duration: method_start.elapsed(),
             done: true,
         });
@@ -609,8 +621,8 @@ mod test_report {
         assert!(
             output.starts_with(
                 "\
-                Checking. states=1, unique=1, depth=0\n\
-                Done. states=15, unique=12, depth=4, sec="
+                Checking. states=1, unique=1, depth=0, avg out degree=0, avg in degree=0\n\
+                Done. states=15, unique=12, depth=4, avg out degree=1.1666666666666667, avg in degree=1.1666666666666667, sec="
             ),
             "Output did not start as expected (see test). output={:?}`",
             output
@@ -637,8 +649,8 @@ mod test_report {
         assert!(
             output.starts_with(
                 "\
-                Checking. states=1, unique=1, depth=0\n\
-                Done. states=55, unique=55, depth=28, sec="
+                Checking. states=1, unique=1, depth=0, avg out degree=0, avg in degree=0\n\
+                Done. states=55, unique=55, depth=28, avg out degree=0.9818181818181818, avg in degree=0.9818181818181818, sec="
             ),
             "Output did not start as expected (see test). output={:?}`",
             output

src/checker/bfs.rs

@@ -15,6 +15,13 @@ use std::sync::atomic::{AtomicUsize, Ordering};
 // While this file is currently quite similar to dfs.rs, a refactoring to lift shared
 // behavior is being postponed until DPOR is implemented.
 
+#[derive(Default)]
+struct NodeData {
+    in_degree: usize,
+    out_degree: usize,
+    parent_fingerprint: Option<Fingerprint>,
+}
+
 pub(crate) struct BfsChecker<M: Model> {
     // Immutable state.
     model: Arc<M>,
@@ -25,7 +32,7 @@ pub(crate) struct BfsChecker<M: Model> {
     job_market: Arc<Mutex<JobMarket<M::State>>>,
     state_count: Arc<AtomicUsize>,
     max_depth: Arc<AtomicUsize>,
-    generated: Arc<DashMap<Fingerprint, Option<Fingerprint>, BuildHasherDefault<NoHashHasher<u64>>>>,
+    generated: Arc<DashMap<Fingerprint, NodeData, BuildHasherDefault<NoHashHasher<u64>>>>,
     discoveries: Arc<DashMap<&'static str, Fingerprint>>,
 }
 struct JobMarket<State> { wait_count: usize, jobs: Vec<Job<State>> }
@@ -50,7 +57,7 @@ where M: Model + Send + Sync + 'static,
         let max_depth = Arc::new(AtomicUsize::new(0));
         let generated = Arc::new({
             let generated = DashMap::default();
-            for s in &init_states { generated.insert(fingerprint(s), None); }
+            for s in &init_states { generated.insert(fingerprint(s), NodeData::default()); }
             generated
         });
         let ebits = {
@@ -176,7 +183,7 @@ where M: Model + Send + Sync + 'static,
     fn check_block(
         model: &M,
         state_count: &AtomicUsize,
-        generated: &DashMap<Fingerprint, Option<Fingerprint>, BuildHasherDefault<NoHashHasher<u64>>>,
+        generated: &DashMap<Fingerprint, NodeData, BuildHasherDefault<NoHashHasher<u64>>>,
         pending: &mut Job<M::State>,
         discoveries: &DashMap<&'static str, Fingerprint>,
         visitor: &Option<Box<dyn CheckerVisitor<M> + Send + Sync>>,
@@ -255,6 +262,11 @@ where M: Model + Send + Sync + 'static,
             // Otherwise enqueue newly generated states (with related metadata).
             let mut is_terminal = true;
             model.actions(&state, &mut actions);
+            let generated_fingerprint = fingerprint(&state);
+            generated
+                .entry(generated_fingerprint)
+                .and_modify(|nd| nd.out_degree = actions.len());
+
             let next_states = actions.drain(..).flat_map(|a| model.next_state(&state, a));
             for next_state in next_states {
                 // Skip if outside boundary.
@@ -270,19 +282,29 @@ where M: Model + Send + Sync + 'static,
                 // that it holds in the path leading to the second visit -- another
                 // possible false-negative.
                 let next_fingerprint = fingerprint(&next_state);
-                if let Entry::Vacant(next_entry) = generated.entry(next_fingerprint) {
-                    next_entry.insert(Some(state_fp));
-                } else {
-                    // FIXME: arriving at an already-known state may be a loop (in which case it
-                    // could, in a fancier implementation, be considered a terminal state for
-                    // purposes of eventually-property checking) but it might also be a join in
-                    // a DAG, which makes it non-terminal. These cases can be disambiguated (at
-                    // some cost), but for now we just _don't_ treat them as terminal, and tell
-                    // users they need to explicitly ensure model path-acyclicality when they're
-                    // using eventually properties (using a boundary or empty actions or
-                    // whatever).
-                    is_terminal = false;
-                    continue
+                match generated.entry(next_fingerprint) {
+                    Entry::Occupied(mut o) => {
+                        let nd = o.get_mut();
+                        nd.in_degree += 1;
+                        // FIXME: arriving at an already-known state may be a loop (in which case it
+                        // could, in a fancier implementation, be considered a terminal state for
+                        // purposes of eventually-property checking) but it might also be a join in
+                        // a DAG, which makes it non-terminal. These cases can be disambiguated (at
+                        // some cost), but for now we just _don't_ treat them as terminal, and tell
+                        // users they need to explicitly ensure model path-acyclicality when they're
+                        // using eventually properties (using a boundary or empty actions or
+                        // whatever).
+                        is_terminal = false;
+                        continue
+                    },
+                    Entry::Vacant(v) => {
+                        let nd = NodeData {
+                            in_degree: 1,
+                            out_degree: 0,
+                            parent_fingerprint: Some(state_fp),
+                        };
+                        v.insert(nd);
+                    },
                 }
 
                 // Otherwise further checking is applicable.
@@ -322,6 +344,20 @@ where M: Model,
         self.max_depth.load(Ordering::Relaxed)
     }
 
+    fn out_degrees(&self) -> Vec<usize>{
+        self.generated
+            .iter()
+            .map(|kv| kv.value().out_degree)
+            .collect()
+    }
+
+    fn in_degrees(&self) -> Vec<usize>{
+        self.generated
+            .iter()
+            .map(|kv| kv.value().in_degree)
+            .collect()
+    }
+
     fn discoveries(&self) -> HashMap<&'static str, Path<M::State, M::Action>> {
         self.discoveries.iter()
             .map(|mapref| {
@@ -349,7 +385,7 @@ where M: Model,
 
 fn reconstruct_path<M>(
     model: &M,
-    generated: &DashMap<Fingerprint, Option<Fingerprint>, BuildHasherDefault<NoHashHasher<u64>>>,
+    generated: &DashMap<Fingerprint, NodeData, BuildHasherDefault<NoHashHasher<u64>>>,
     fp: Fingerprint)
     -> Path<M::State, M::Action>
     where M: Model,
@@ -363,7 +399,7 @@ fn reconstruct_path<M>(
     let mut fingerprints = VecDeque::new();
     let mut next_fp = fp;
     while let Some(source) = generated.get(&next_fp) {
-        match *source {
+        match source.parent_fingerprint {
             Some(prev_fingerprint) => {
                 fingerprints.push_front(next_fp);
                 next_fp = prev_fingerprint;