From 11a82175f3a464f8e07d9404ecdd9689489a8e0b Mon Sep 17 00:00:00 2001 From: Samuel Pastva Date: Wed, 28 Apr 2021 18:09:18 +0200 Subject: [PATCH] Remove unused dependencies and update version. --- Cargo.toml | 4 +- src/scc/algo_effectively_constant.rs | 187 ---------------- src/scc/algo_par_utils.rs | 27 --- src/scc/algo_symbolic_components.rs | 322 --------------------------- src/scc/algo_symbolic_reach.rs | 190 ---------------- 5 files changed, 1 insertion(+), 729 deletions(-) delete mode 100644 src/scc/algo_effectively_constant.rs delete mode 100644 src/scc/algo_par_utils.rs delete mode 100644 src/scc/algo_symbolic_components.rs delete mode 100644 src/scc/algo_symbolic_reach.rs diff --git a/Cargo.toml b/Cargo.toml index 89e867c..f7ea13a 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "biodivine-aeon-server" -version = "0.4.0-beta.1" +version = "0.4.0" authors = ["Samuel Pastva "] edition = "2018" default-run = "biodivine-aeon-server" @@ -19,8 +19,6 @@ lto = true biodivine-lib-bdd = "0.2.1" biodivine-lib-param-bn = "0.1.0" rocket = "0.4.6" -rayon = "1.5.0" -crossbeam = "0.8.0" lazy_static = "1.4.0" json = "0.12.4" regex = "1.4.2" diff --git a/src/scc/algo_effectively_constant.rs b/src/scc/algo_effectively_constant.rs deleted file mode 100644 index ac3e159..0000000 --- a/src/scc/algo_effectively_constant.rs +++ /dev/null @@ -1,187 +0,0 @@ -use biodivine_lib_param_bn::symbolic_async_graph::{GraphColoredVertices, SymbolicAsyncGraph}; -use biodivine_lib_param_bn::VariableId; - -/// This routine removes vertices which can never appear in an attractor by detecting parameter values -/// for which the variable jumps only in one direction. -/// -/// If such one-directional jump is detected, then all states that can reach it are naturally -/// not in any attractor (since in an attractor, that jump would have to be reversed eventually). -/// -/// Note that this does not mean the variable has to strictly always jump - that is why we need the -/// backward reachability to detect states that can actually achieve irreversible jump. -pub fn remove_effectively_constant_states( - graph: &SymbolicAsyncGraph, - set: GraphColoredVertices, -) -> (GraphColoredVertices, Vec) { - println!("Remove effectively constant states."); - let original_size = set.approx_cardinality(); - let mut universe = set; - let mut stop = false; - let mut variables: Vec = graph.network().variables().collect(); - while !stop { - stop = true; - let mut to_remove = graph.empty_vertices().clone(); - for variable in graph.network().variables() { - let active_variables: Vec = variables - .iter() - .cloned() - .filter(|it| *it != variable) - .collect(); - let vertices_where_var_can_jump = graph.var_can_post(variable, &universe); - let vertices_where_var_jumped = graph.var_post(variable, &universe); - let reachable_after_jump = reach_saturated_fwd_excluding( - graph, - &vertices_where_var_jumped, - &universe, - &active_variables, - ); - let can_jump_again = reachable_after_jump.intersect(&vertices_where_var_can_jump); - let will_never_jump_again = vertices_where_var_can_jump.minus(&can_jump_again); - if !will_never_jump_again.is_empty() { - stop = false; - let to_remove_for_var = reach_saturated_bwd_excluding( - graph, - &will_never_jump_again, - &universe, - &active_variables, - ); - to_remove = to_remove.union(&to_remove_for_var); - //universe = universe.minus(&to_remove); THIS IS A BAD IDEA... - println!( - "{:?} will never jump again: {}", - variable, - will_never_jump_again.approx_cardinality() - ); - println!( - "Eliminated {}/{} {:+e}%", - to_remove.approx_cardinality(), - universe.approx_cardinality(), - (to_remove.approx_cardinality() / universe.approx_cardinality()) * 100.0 - ); - } - } - universe = universe.minus(&to_remove); - let original_vars = variables.len(); - variables = variables - .into_iter() - .filter(|v| !graph.var_can_post(*v, &universe).is_empty()) - .collect(); - println!( - "Universe now has {} nodes. Eliminated {} variables.", - universe.clone().into_bdd().size(), - original_vars - variables.len() - ); - } - - println!("Final active variables: {}", variables.len()); - println!( - "Removed {}/{} {:+e}%; {} nodes.", - universe.approx_cardinality(), - original_size, - (universe.approx_cardinality() / original_size) * 100.0, - universe.clone().into_bdd().size() - ); - - for v in &variables { - let vertices_where_var_can_jump = graph.var_can_post(*v, &universe); - let reachable_before_jump = reach_saturated_bwd_excluding( - graph, - &vertices_where_var_can_jump, - &universe, - &variables, - ); - let reachable_after_jump = reach_saturated_fwd_excluding( - graph, - &vertices_where_var_can_jump, - &universe, - &variables, - ); - let components = reachable_before_jump.intersect(&reachable_after_jump); - let below = reachable_after_jump.minus(&components); - let can_reach_below = - reach_saturated_bwd_excluding(graph, &below, &universe, &variables).minus(&below); - println!( - "({:?}) Below: {} Can reach below: {}", - v, - below.approx_cardinality(), - can_reach_below.approx_cardinality() - ); - universe = universe.minus(&can_reach_below); - } - - println!("Final active variables: {}", variables.len()); - println!( - "Removed {}/{} {:+e}%; {} nodes.", - universe.approx_cardinality(), - original_size, - (universe.approx_cardinality() / original_size) * 100.0, - universe.clone().into_bdd().size() - ); - return (universe, variables); -} - -pub fn reach_saturated_fwd_excluding( - graph: &SymbolicAsyncGraph, - initial: &GraphColoredVertices, - guard: &GraphColoredVertices, - variables: &Vec, -) -> GraphColoredVertices { - if variables.is_empty() { - return initial.clone(); - } - let mut result = initial.clone(); - let last_variable = variables.len() - 1; - let mut active_variable = last_variable; - loop { - let variable = variables[active_variable]; - let post = graph - .var_post(variable, &result) - .intersect(guard) - .minus(&result); - result = result.union(&post); - - if !post.is_empty() { - active_variable = last_variable; - } else { - if active_variable == 0 { - break; - } else { - active_variable -= 1; - } - } - } - return result; -} - -pub fn reach_saturated_bwd_excluding( - graph: &SymbolicAsyncGraph, - initial: &GraphColoredVertices, - guard: &GraphColoredVertices, - variables: &Vec, -) -> GraphColoredVertices { - if variables.is_empty() { - return initial.clone(); - } - let mut result = initial.clone(); - let last_variable = variables.len() - 1; - let mut active_variable = last_variable; - loop { - let variable = variables[active_variable]; - let post = graph - .var_pre(variable, &result) - .intersect(guard) - .minus(&result); - result = result.union(&post); - - if !post.is_empty() { - active_variable = last_variable; - } else { - if active_variable == 0 { - break; - } else { - active_variable -= 1; - } - } - } - return result; -} diff --git a/src/scc/algo_par_utils.rs b/src/scc/algo_par_utils.rs deleted file mode 100644 index e6fc819..0000000 --- a/src/scc/algo_par_utils.rs +++ /dev/null @@ -1,27 +0,0 @@ -use rayon::prelude::*; - -// TODO: Something, something, FUTURES! -pub fn par_fold(items: Vec, action: F) -> T -where - F: Fn(&T, &T) -> T + Sync, -{ - if items.is_empty() { - panic!("Empty parallel fold"); - } else if items.len() == 1 { - return items[0].clone(); - } else { - let data: &[T] = &items; - let joined: Vec = data - .par_iter() - .chunks(2) - .map(|chunk| { - if chunk.len() == 2 { - action(&chunk[0], &chunk[1]) - } else { - chunk[0].clone() - } - }) - .collect(); - return par_fold(joined, action); - } -} diff --git a/src/scc/algo_symbolic_components.rs b/src/scc/algo_symbolic_components.rs deleted file mode 100644 index b99cfc2..0000000 --- a/src/scc/algo_symbolic_components.rs +++ /dev/null @@ -1,322 +0,0 @@ -use crate::scc::algo_effectively_constant::{ - reach_saturated_bwd_excluding, reach_saturated_fwd_excluding, - remove_effectively_constant_states, -}; -use crate::scc::ProgressTracker; -use biodivine_lib_param_bn::symbolic_async_graph::{GraphColoredVertices, SymbolicAsyncGraph}; -use biodivine_lib_std::param_graph::Params; -use std::sync::atomic::AtomicBool; - -pub fn components_2(graph: &SymbolicAsyncGraph, on_component: F) -where - F: Fn(GraphColoredVertices) -> () + Send + Sync, -{ - let mut universe = graph.unit_vertices().clone(); - - let (constrained, variables) = remove_effectively_constant_states(graph, universe); - universe = constrained.clone(); - - while !universe.is_empty() { - println!("Pick a new pivot branch..."); - let pivot = universe.pick_vertex(); - - let bwd_pivot = reach_saturated_bwd_excluding(graph, &pivot, &universe, &variables); - let component_with_pivot = - reach_saturated_fwd_excluding(graph, &pivot, &bwd_pivot, &variables); - let after_component = graph - .post(&component_with_pivot) - .minus(&component_with_pivot); - let is_candidate = component_with_pivot - .colors() - .minus(&after_component.colors()); - if !is_candidate.is_empty() { - on_component(component_with_pivot.intersect_colors(&is_candidate)); - } - universe = universe.minus(&bwd_pivot); - } -} - -/* -/// Compute the SCCs that are induced by the vertices in `initial`. -/// -/// Uses lockstep, so in terms of symbolic steps, this should be optimal. -fn components_with(graph: &SymbolicAsyncGraph, initial: &GraphColoredVertices) -> GraphColoredVertices { - println!("Lockstep component search."); - let mut still_running = initial.color_projection(graph); - let mut fwd = initial.clone(); - let mut bwd = initial.clone(); - let mut fwd_frontier = initial.clone(); - let mut bwd_frontier = initial.clone(); - let mut fwd_unfinished = graph.empty_vertices().clone(); - let mut bwd_unfinished = graph.empty_vertices().clone(); - // First, find fwd/bwd templates using lockstep. - while !still_running.is_empty() { - println!("(1) Still running {}; {} {} {} {}", still_running.cardinality(), fwd.as_bdd().size(), bwd.as_bdd().size(), fwd_unfinished.as_bdd().size(), bwd_unfinished.as_bdd().size()); - let post = post(graph, &fwd_frontier).minus(&fwd); - let pre = pre(graph, &bwd_frontier).minus(&bwd); - // Compute colours that FINISHED in this iteration. - let fwd_finished_now = fwd_frontier.color_projection(graph).minus(&post.color_projection(graph)); - let bwd_finished_now = bwd_frontier.color_projection(graph).minus(&pre.color_projection(graph)); - let bwd_finished_now = bwd_finished_now.minus(&fwd_finished_now); // Resolve ties. - // Remove BWD-FINISHED colours from FWD frontier and move all vertices with these colours to unfinished. - fwd_frontier = post.minus_colors(&bwd_finished_now); - fwd_unfinished = fwd_unfinished.union(&fwd.intersect_colors(&bwd_finished_now)); - fwd = fwd.minus_colors(&bwd_finished_now).union(&fwd_frontier); - // Remove FWD-FINISHED colours from BWD frontier and move all vertices with these colours to unfinished. - bwd_frontier = pre.minus_colors(&fwd_finished_now); - bwd_unfinished = bwd_unfinished.union(&bwd.intersect_colors(&fwd_finished_now)); - bwd = bwd.minus_colors(&fwd_finished_now).union(&bwd_frontier); - // Mark finished colours as done. - still_running = still_running.minus(&fwd_finished_now.union(&bwd_finished_now)); - } - // Now fwd and bwd contain VALID forward/backward sets and are colour disjoint. - // We have to continue computing unfinished within these valid bounds. - assert!(fwd.color_projection(graph).intersect(&bwd.color_projection(graph)).is_empty()); - assert!(initial.color_projection(graph).minus(&fwd.color_projection(graph)).minus(&bwd.color_projection(graph)).is_empty()); - - loop { - let post = post(graph, &fwd_unfinished).minus(&fwd_unfinished).intersect(&bwd); - let pre = pre(graph, &bwd_unfinished).minus(&bwd_unfinished).intersect(&fwd); - fwd_unfinished = fwd_unfinished.union(&post); - bwd_unfinished = bwd_unfinished.union(&pre); - println!("(2) Still running {}", post.cardinality() + pre.cardinality()); - if post.is_empty() && pre.is_empty() { - break; - } - } - // At this point, fwd_unfinished and bwd_unfinished are completely done within the bounds of bwd/fwd. - // We can therefore join them back - fwd = fwd.union(&fwd_unfinished); - bwd = bwd.union(&bwd_unfinished); - - // The final result is the intersection of the two. - return fwd.intersect(&bwd); -}*/ - -pub fn components( - graph: &SymbolicAsyncGraph, - _progress: &ProgressTracker, - _cancelled: &AtomicBool, - on_component: F, -) where - F: Fn(GraphColoredVertices) -> () + Send + Sync, -{ - components_2(graph, on_component); - /* - crossbeam::thread::scope(|scope| { - println!("Detect eventually stable..."); - // TODO: This is not correct, because for parametrisations can_move will never be empty... - /*let mut without_fixed = graph.unit_vertices().clone(); - for variable in graph.network().graph().variable_ids() { - let true_states = graph.state_variable_true(variable).intersect(&without_fixed); - let false_states = graph.state_variable_false(variable).intersect(&without_fixed); - let can_move_true = graph.has_any_post(variable, &true_states); - let can_move_false = graph.has_any_post(variable, &false_states); - if can_move_true.is_empty() { - // Every transition for this variable is 0 -> 1, hence states that have this - // transition enabled cannot be in attractor because it would never reverse... - without_fixed = without_fixed.minus(&can_move_false) - - // At this point, we also know that the two sets (true states and false states) - // are independent and can be processed in parallel! We should use that! TODO... - } - if can_move_false.is_empty() { - without_fixed = without_fixed.minus(&can_move_true) - } - } - println!("Fixed {}/{}", without_fixed.cardinality(), graph.unit_vertices().cardinality());*/ - - println!("Start detecting sinks"); - - - let mut can_be_sink = graph.unit_vertices().clone(); // intentionally use all vertices - //panic!(""); - for variable in graph.network().graph().variable_ids() { - print!("{:?}...", variable); - io::stdout().flush().unwrap(); - if cancelled.load(Ordering::SeqCst) { - return (); - } - let has_successor = &graph.has_any_post(variable, graph.unit_vertices()); - can_be_sink = can_be_sink.minus(has_successor); - } - println!(); - - let mut is_sink = can_be_sink.clone(); - /*for sink in is_sink.state_projection(graph).states(graph) { - let mut valuations = Vec::new(); - for (i_v, v) in graph.network().graph().variable_ids().enumerate() { - let name = graph.network().graph().get_variable(v).get_name(); - valuations.push((name.clone(), sink.get(i_v))); - } - let sink_colors = is_sink.intersect(&graph.vertex(sink.clone())).color_projection(); - let sink_remaining = is_sink.minus(&graph.vertex(sink.clone())).intersect_colors(&sink_colors); - let sink_rank = if sink_remaining.is_empty() { 1 } else { 2 }; - - println!("========================= Sink state (Rank {}) {:?} =========================", sink_rank, sink.values()); - println!("{:?}", valuations); - println!("========================= Witness network ========================="); - let witness = graph.make_witness(&sink_colors); - println!("{}", witness.to_string()); - }*/ - let sinks = is_sink.clone(); - // Now we have to report sinks, but we have to satisfy that every reported set has only one component: - while !is_sink.is_empty() { - let to_report = is_sink.pivots(graph); - is_sink = is_sink.minus(&to_report); - on_component(to_report); - } - - println!("Sinks detected: {}", sinks.cardinality()); - - /*let has_successors: Vec = graph.network().graph().variable_ids() - .collect::>() - .into_par_iter() - .map(|variable: VariableId| { - graph.has_any_post(variable, graph.unit_vertices()) - }) - .collect(); - let has_successors = par_fold(has_successors, |a, b| a.union(b));*/ - - let (not_constant, _) = remove_effectively_constant_states(graph, graph.unit_vertices().clone()); - println!("Not constant: {}/{}", not_constant.cardinality(), graph.unit_vertices().cardinality()); - - if cancelled.load(Ordering::SeqCst) { - return (); - } - - let can_reach_sink = - guarded_reach_bwd(&graph, &sinks, ¬_constant, cancelled, progress); - - if cancelled.load(Ordering::SeqCst) { - return (); - } - - let initial = not_constant.minus(&can_reach_sink); - - println!("Initial: {}", initial.cardinality()); - - if initial.is_empty() { - return (); - } - - let mut queue: Vec<(f64, GraphColoredVertices)> = Vec::new(); - queue.push((initial.cardinality(), initial)); - - while let Some((universe_cardinality, universe)) = queue.pop() { - if cancelled.load(Ordering::SeqCst) { - return (); - } - - println!( - "Universe cardinality: {} Remaining work queue: {}", - universe_cardinality, - queue.len() - ); - let remaining: f64 = queue.iter().map(|(a, _)| *a).sum::() + universe_cardinality; - progress.update_remaining(remaining); - println!("Look for pivots..."); - let pivots = universe.pivots(graph); - let backward = guarded_reach_bwd(&graph, &pivots, &universe, cancelled, progress); - let pivots = improve_pivots(graph, pivots.clone(), &(universe.minus(&backward).union(&pivots))); - println!("Pivots cardinality: {}", pivots.cardinality()); - let backward = guarded_reach_bwd(&graph, &backward.union(&pivots), &universe, cancelled, progress); - let component_with_pivots = guarded_reach_fwd(&graph, &pivots, &backward, cancelled, progress); - - let mut is_terminal = component_with_pivots.color_projection(graph); - for v in graph.network().graph().variable_ids() { - let successors = graph.any_post(v, &component_with_pivots).minus(&component_with_pivots).color_projection(graph); - if !successors.is_empty() { - is_terminal = is_terminal.minus(&successors); - } - } - - if !is_terminal.is_empty() { - let terminal = component_with_pivots.intersect_colors(&is_terminal); - scope.spawn(|_| { - on_component(terminal); - }); - } - - let remaining = universe.minus(&backward); - if !remaining.is_empty() { - queue.push((remaining.cardinality(), remaining)); - } - - /* - let forward = guarded_reach_fwd(&graph, &pivots, &universe, cancelled, progress); - - if cancelled.load(Ordering::SeqCst) { - return (); - } - - let component_with_pivots = - guarded_reach_bwd(&graph, &pivots, &forward, cancelled, progress); - - if cancelled.load(Ordering::SeqCst) { - return (); - } - - let reachable_terminals = forward.minus(&component_with_pivots); - - let leaves_current = reachable_terminals.color_projection(); - let is_terminal = graph.unit_colors().minus(&leaves_current); - - if !is_terminal.is_empty() { - let terminal = component_with_pivots.intersect_colors(&is_terminal); - scope.spawn(|_| { - on_component(terminal); - }); - } - - let basins_of_reachable_terminals = - guarded_reach_bwd(&graph, &forward, &universe, cancelled, progress); - - if cancelled.load(Ordering::SeqCst) { - return (); - } - - let unreachable_terminals = universe.minus(&basins_of_reachable_terminals); - - if !leaves_current.is_empty() { - queue.push((reachable_terminals.cardinality(), reachable_terminals)); - } - if !unreachable_terminals.is_empty() { - queue.push((unreachable_terminals.cardinality(), unreachable_terminals)); - }*/ - } - - println!("Main component loop done..."); - }) - .unwrap();*/ -} - -/*fn improve_pivots(graph: &SymbolicAsyncGraph, pivots: GraphColoredVertices, universe: &GraphColoredVertices) -> GraphColoredVertices { - let mut discovered = pivots.clone(); - let mut final_pivots = graph.empty_vertices().clone(); - let mut frontier = pivots.clone(); - println!("Pivot optimisation..."); - while !frontier.is_empty() { - if discovered.as_bdd().size() > 10_000 { - println!("{}/{} ({:+e}%, nodes result({}))", - discovered.cardinality(), - universe.cardinality(), - (discovered.cardinality() / universe.cardinality()) * 100.0, - discovered.as_bdd().size() - ); - } - let mut new_successor = graph.empty_vertices().clone(); - for v in graph.network().graph().variable_ids() { - new_successor = new_successor.union(&graph.any_post(v, &frontier)); - } - new_successor = new_successor.minus(&discovered); - let stopped_in_this_step = frontier.color_projection(graph).minus(&new_successor.color_projection(graph)); - if !stopped_in_this_step.is_empty() { - // For colours that stopped in this iteration - final_pivots = final_pivots.union(&frontier.intersect_colors(&stopped_in_this_step).pivots(graph)) - } - frontier = new_successor; - discovered = discovered.union(&frontier); - } - return final_pivots; -}*/ diff --git a/src/scc/algo_symbolic_reach.rs b/src/scc/algo_symbolic_reach.rs deleted file mode 100644 index 8361497..0000000 --- a/src/scc/algo_symbolic_reach.rs +++ /dev/null @@ -1,190 +0,0 @@ -use crate::scc::ProgressTracker; -use biodivine_lib_param_bn::symbolic_async_graph::{GraphColoredVertices, SymbolicAsyncGraph}; -use std::io; -use std::io::Write; -use std::sync::atomic::{AtomicBool, Ordering}; - -pub fn guarded_reach_fwd( - graph: &SymbolicAsyncGraph, - initial: &GraphColoredVertices, - guard: &GraphColoredVertices, - cancelled: &AtomicBool, - progress: &ProgressTracker, -) -> GraphColoredVertices { - /*let mut result = initial.clone(); - let mut frontier = initial.clone(); - - println!("Reach fwd..."); - while !frontier.is_empty() { - if cancelled.load(Ordering::SeqCst) { - return result; // result is incorrect, but we are cancelled so we don't care... - } - - progress.update_last_wave(frontier.cardinality()); - - println!("{}/{} ({:+e}%, nodes result({}), frontier({}))", - result.cardinality(), - guard.cardinality(), - (result.cardinality()/guard.cardinality()) * 100.0, - result.clone().into_bdd().size(), - frontier.clone().into_bdd().size() - ); - print!("{} || ", frontier.cardinality()); - let mut successors = graph.empty_vertices().clone(); - for variable in graph.network().graph().variable_ids() { - print!("{:?}...", variable); - io::stdout().flush().unwrap(); - if cancelled.load(Ordering::SeqCst) { - return result; // result is incorrect, but we are cancelled so we don't care... - } - successors = successors.union(&graph.post(variable, &frontier, guard)); - } - successors = successors.minus(&result); - result = result.union(&successors); - println!(); - frontier = successors; - } - - progress.update_last_wave(0.0); - return result;*/ - let mut result = initial.clone(); - - println!("Reach fwd..."); - loop { - if cancelled.load(Ordering::SeqCst) { - return result; // result is incorrect, but we are cancelled so we don't care... - } - - progress.update_last_wave(result.cardinality()); - - println!( - "{}/{} ({:+e}%, nodes result({}))", - result.cardinality(), - guard.cardinality(), - (result.cardinality() / guard.cardinality()) * 100.0, - result.clone().into_bdd().size() - ); - let mut successors = graph.empty_vertices().clone(); - for variable in graph.network().graph().variable_ids() { - io::stdout().flush().unwrap(); - if cancelled.load(Ordering::SeqCst) { - return result; // result is incorrect, but we are cancelled so we don't care... - } - let s = graph.post(variable, &result, guard); - successors = successors.union(&s); - /*if !s.is_empty() { - println!("{:?} -> {}", variable, s.into_bdd().size()); - }*/ - } - print!(" || {}", successors.clone().into_bdd().size()); - println!(); - successors = successors.minus(&result); - if successors.is_empty() { - break; - } - result = result.union(&successors); - } - - progress.update_last_wave(0.0); - return result; -} - -pub fn guarded_reach_bwd( - graph: &SymbolicAsyncGraph, - initial: &GraphColoredVertices, - guard: &GraphColoredVertices, - cancelled: &AtomicBool, - progress: &ProgressTracker, -) -> GraphColoredVertices { - /*let mut result = initial.clone(); - let mut frontier = initial.clone(); - - println!("Reach bwd..."); - while !frontier.is_empty() { - if cancelled.load(Ordering::SeqCst) { - return result; // result is incorrect, but we are cancelled so we don't care... - } - - progress.update_last_wave(frontier.cardinality()); - - println!("{}/{} ({:+e}%, nodes result({}), frontier({}))", - result.cardinality(), - guard.cardinality(), - (result.cardinality()/guard.cardinality()) * 100.0, - result.clone().into_bdd().size(), - frontier.clone().into_bdd().size() - ); - print!("{} || ", frontier.cardinality()); - /*let var_predecessors: Vec = graph.network().graph().variable_ids().collect::>() - .into_par_iter() - .map(|variable| { - let mut predecessors = graph.empty_vertices().clone(); - let mut sub_frontier = graph.pre(variable, &frontier, guard); - while !sub_frontier.is_empty() { - sub_frontier = sub_frontier.minus(&predecessors); - predecessors = predecessors.union(&sub_frontier); - sub_frontier = graph.pre(variable, &sub_frontier, guard); - } - predecessors - }) - .collect(); - let predecessors = par_fold(var_predecessors, |a, b| a.union(b)); - frontier = predecessors.minus(&result); - result = result.union(&predecessors);*/ - let mut predecessors = graph.empty_vertices().clone(); - for variable in graph.network().graph().variable_ids() { - print!("{:?}...", variable); - io::stdout().flush().unwrap(); - if cancelled.load(Ordering::SeqCst) { - return result; // result is incorrect, but we are cancelled so we don't care... - } - predecessors = predecessors.union(&graph.pre(variable, &frontier, guard)); - } - predecessors = predecessors.minus(&result); - result = result.union(&predecessors); - println!(); - frontier = predecessors; - } - - progress.update_last_wave(0.0);*/ - let mut result = initial.clone(); - - println!("Reach bwd..."); - loop { - if cancelled.load(Ordering::SeqCst) { - return result; // result is incorrect, but we are cancelled so we don't care... - } - - progress.update_last_wave(result.cardinality()); - - println!( - "{}/{} ({:+e}%, nodes result({}))", - result.cardinality(), - guard.cardinality(), - (result.cardinality() / guard.cardinality()) * 100.0, - result.clone().into_bdd().size() - ); - let mut predecessors = graph.empty_vertices().clone(); - for variable in graph.network().graph().variable_ids() { - io::stdout().flush().unwrap(); - if cancelled.load(Ordering::SeqCst) { - return result; // result is incorrect, but we are cancelled so we don't care... - } - let s = graph.pre(variable, &result, guard); - predecessors = predecessors.union(&s); - /*if !s.is_empty() { - println!("{:?} -> {}", variable, s.into_bdd().size()); - }*/ - } - print!(" || {}", predecessors.clone().into_bdd().size()); - println!(); - predecessors = predecessors.minus(&result); - if predecessors.is_empty() { - break; - } - result = result.union(&predecessors); - } - - progress.update_last_wave(0.0); - return result; -}