Parallelize refinement check using threads and message passing

Cargo.toml

@@ -43,6 +43,8 @@ edbm = {git = "https://github.com/Ecdar/EDBM"}
 log = "0.4.17"
 env_logger = {version = "0.9.0", optional = true }
 chrono = {version = "0.4.22", optional = true }
+crossbeam-channel = "0.5.6"
+num_cpus = "1.13.1"
 
 # Enable optimizations for EDBM in debug mode, but not for our code:
 [profile.dev.package.edbm]

src/DataTypes/mod.rs

@@ -1,3 +1,3 @@
 pub mod statepair_list;
 
-pub use statepair_list::{PassedStateList, PassedStateListExt, WaitingStateList};
+pub use statepair_list::{PassedStateList, PassedStateListExt};

src/DataTypes/statepair_list.rs

@@ -1,4 +1,4 @@
-use std::collections::{HashMap, VecDeque};
+use std::collections::HashMap;
 
 use edbm::zones::OwnedFederation;
 
@@ -8,12 +8,6 @@ pub type PassedStateList = PassedStateListFed;
 type PassedStateListFed = HashMap<(LocationID, LocationID), OwnedFederation>;
 type PassedStateListVec = HashMap<(LocationID, LocationID), Vec<OwnedFederation>>;
 
-pub type WaitingStateList = DepthFirstWaitingStateList;
-pub struct DepthFirstWaitingStateList {
-    queue: VecDeque<StatePair>,
-    map: HashMap<(LocationID, LocationID), VecDeque<OwnedFederation>>,
-}
-
 pub trait PassedStateListExt {
     fn put(&mut self, pair: StatePair);
     fn has(&self, pair: &StatePair) -> bool;
@@ -53,61 +47,6 @@ impl PassedStateListExt for PassedStateListVec {
     }
 }
 
-impl PassedStateListExt for DepthFirstWaitingStateList {
-    fn put(&mut self, mut pair: StatePair) {
-        self.queue.push_front(pair.clone());
-        let fed = pair.take_zone();
-        let (loc1, loc2) = (pair.locations1.id, pair.locations2.id);
-        let key = (loc1, loc2);
-        if let Some(vec) = self.map.get_mut(&key) {
-            vec.push_front(fed);
-        } else {
-            self.map.insert(key, vec![fed].into());
-        };
-    }
-    fn has(&self, pair: &StatePair) -> bool {
-        let (loc1, loc2, fed) = (
-            pair.locations1.id.clone(),
-            pair.locations2.id.clone(),
-            pair.ref_zone(),
-        );
-        let key = (loc1, loc2);
-        match self.map.get(&key) {
-            Some(vec) => vec.iter().any(|f| fed.subset_eq(f)),
-            None => false,
-        }
-    }
-    fn zones(&self, key: &(LocationID, LocationID)) -> Vec<&OwnedFederation> {
-        match self.map.get(key) {
-            Some(vec) => vec.iter().collect(),
-            None => panic!("No zones for key: {:?}", key),
-        }
-    }
-}
-
-impl DepthFirstWaitingStateList {
-    pub fn new() -> Self {
-        DepthFirstWaitingStateList {
-            queue: VecDeque::new(),
-            map: HashMap::new(),
-        }
-    }
-
-    pub fn pop(&mut self) -> Option<StatePair> {
-        let pair = self.queue.pop_front()?;
-        let key = (pair.locations1.id.clone(), pair.locations2.id.clone());
-
-        if let Some(vec) = self.map.get_mut(&key) {
-            vec.pop_front().unwrap();
-        };
-
-        Some(pair)
-    }
-
-    pub fn is_empty(&self) -> bool {
-        self.queue.is_empty()
-    }
-}
 impl PassedStateListExt for PassedStateListFed {
     fn put(&mut self, mut pair: StatePair) {
         let mut fed = pair.take_zone();