Skip to content

Commit

Permalink
Make TrapSpaces and FixedPoints algorithms interruptible.
Browse files Browse the repository at this point in the history
  • Loading branch information
@daemontus
daemontus committed Jan 26, 2024
1 parent e93c9ce commit b95165b
Show file tree
Hide file tree
Showing 4 changed files with 292 additions and 132 deletions.
174 changes: 98 additions & 76 deletions src/fixed_points/mod.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -31,7 +31,7 @@ use crate::Space;
/// (The module is hidden, but we re-export iterator in this module)
mod symbolic_iterator;
use crate::symbolic_async_graph::projected_iteration::MixedProjection;
use crate::{BooleanNetwork, VariableId};
use crate::{global_log_level, log_essential, never_stop, should_log, BooleanNetwork, VariableId};
pub use symbolic_iterator::SymbolicIterator;

/// Implements the iterator used by `FixedPoints::solver_iterator`.
Expand Down Expand Up @@ -147,29 +147,24 @@ impl FixedPoints {
stg: &SymbolicAsyncGraph,
restriction: &GraphColoredVertices,
) -> GraphColoredVertices {
if cfg!(feature = "print-progress") {
Self::_symbolic(stg, restriction, global_log_level(), &never_stop).unwrap()
}

pub fn _symbolic<E, F: Fn() -> Result<(), E>>(
stg: &SymbolicAsyncGraph,
restriction: &GraphColoredVertices,
log_level: usize,
interrupt: &F,
) -> Result<GraphColoredVertices, E> {
if should_log(log_level) {
println!(
"Start symbolic fixed-point search with {}[nodes:{}] candidates.",
restriction.approx_cardinality(),
restriction.symbolic_size()
);
}

let mut to_merge: Vec<Bdd> = stg
.variables()
.map(|var| {
let can_step = stg.var_can_post(var, stg.unit_colored_vertices());
let is_stable = stg.unit_colored_vertices().minus(&can_step);
if cfg!(feature = "print-progress") {
println!(
" > Created initial set for {:?} using {} BDD nodes.",
var,
is_stable.symbolic_size()
);
}
is_stable.into_bdd()
})
.collect();
let mut to_merge = Self::prepare_to_merge(stg, log_level, interrupt)?;

/*
Note to self: There is actually a marginally faster version of this algorithm that
Expand All @@ -183,23 +178,27 @@ impl FixedPoints {
to_merge.push(restriction.as_bdd().clone());
}

interrupt()?;

let fixed_points = Self::symbolic_merge(
stg.symbolic_context().bdd_variable_set(),
to_merge,
HashSet::default(),
);

interrupt()?;

let fixed_points = stg.unit_colored_vertices().copy(fixed_points);

if cfg!(feature = "print-progress") {
if should_log(log_level) {
println!(
"Found {}[nodes:{}] fixed-points.",
fixed_points.approx_cardinality(),
fixed_points.symbolic_size(),
);
}

fixed_points
Ok(fixed_points)
}

/// This is a general symbolic projected fixed-point algorithm. It works on the same
Expand Down Expand Up @@ -231,21 +230,7 @@ impl FixedPoints {
);
}

let mut to_merge: Vec<Bdd> = stg
.variables()
.map(|var| {
let can_step = stg.var_can_post(var, stg.unit_colored_vertices());
let is_stable = stg.unit_colored_vertices().minus(&can_step);
if cfg!(feature = "print-progress") {
println!(
" > Created initial set for {:?} using {} BDD nodes.",
var,
is_stable.symbolic_size()
);
}
is_stable.into_bdd()
})
.collect();
let mut to_merge = Self::prepare_to_merge(stg, global_log_level(), &never_stop).unwrap();

// Now compute the BDD variables that should be projected away.
let ctx = stg.symbolic_context();
Expand Down Expand Up @@ -312,8 +297,18 @@ impl FixedPoints {
universe: &BddVariableSet,
to_merge: Vec<Bdd>,
// The set of variables that will be eliminated from the result.
mut project: HashSet<BddVariable>,
project: HashSet<BddVariable>,
) -> Bdd {
Self::_symbolic_merge(universe, to_merge, project, global_log_level(), &never_stop).unwrap()
}

pub fn _symbolic_merge<E, F: Fn() -> Result<(), E>>(
universe: &BddVariableSet,
to_merge: Vec<Bdd>,
mut project: HashSet<BddVariable>,
log_level: usize,
interrupt: &F,
) -> Result<Bdd, E> {
// First, assign each merge item a unique integer identifier.
let mut to_merge: HashMap<usize, Bdd> = to_merge.into_iter().enumerate().collect();

Expand All @@ -339,6 +334,7 @@ impl FixedPoints {

let mut result = universe.mk_true();
let mut merged = HashSet::new();
interrupt()?;

/*
Note to self: It seems that not all projections are always beneficial to the BDD size.
Expand All @@ -356,8 +352,9 @@ impl FixedPoints {
if dependencies.is_subset(&merged) {
result = result.var_exists(p_var);
project.remove(&p_var);
interrupt()?;

if cfg!(feature = "print-progress") {
if log_essential(log_level, result.size()) {
println!(" > Projection. New result has {} BDD nodes. Remaining projections: {}.",
result.size(),
project.len()
Expand All @@ -383,6 +380,8 @@ impl FixedPoints {
&result,
biodivine_lib_bdd::op_function::and,
);
interrupt()?;

if let Some(bdd) = bdd {
// At this point, the size of the BDD should be smaller or equal to the
// best result, so we can just update it.
Expand All @@ -401,10 +400,10 @@ impl FixedPoints {
merged.insert(best_index);

if result.is_false() {
return universe.mk_false();
return Ok(universe.mk_false());
}

if cfg!(feature = "print-progress") {
if log_essential(log_level, result.size()) {
println!(
" > Merge. New result has {} BDD nodes. Remaining constraints: {}.",
result.size(),
Expand All @@ -414,7 +413,9 @@ impl FixedPoints {
}
}

if cfg!(feature = "print-progress") {
interrupt()?;

if should_log(log_level) {
println!("Merge finished with {} BDD nodes.", result.size(),);
}

Expand All @@ -423,7 +424,7 @@ impl FixedPoints {
// And everything was merged.
assert_eq!(merged.len(), support_sets.len());

result
Ok(result)
}

/// The result of the function are all vertices that can appear as fixed-points for **some**
Expand All @@ -444,29 +445,24 @@ impl FixedPoints {
stg: &SymbolicAsyncGraph,
restriction: &GraphColoredVertices,
) -> GraphVertices {
if cfg!(feature = "print-progress") {
Self::_symbolic_vertices(stg, restriction, global_log_level(), &never_stop).unwrap()
}

pub fn _symbolic_vertices<E, F: Fn() -> Result<(), E>>(
stg: &SymbolicAsyncGraph,
restriction: &GraphColoredVertices,
log_level: usize,
interrupt: &F,
) -> Result<GraphVertices, E> {
if should_log(log_level) {
println!(
"Start symbolic fixed-point vertex search with {}[nodes:{}] candidates.",
restriction.approx_cardinality(),
restriction.symbolic_size()
);
}

let mut to_merge: Vec<Bdd> = stg
.variables()
.map(|var| {
let can_step = stg.var_can_post(var, stg.unit_colored_vertices());
let is_stable = stg.unit_colored_vertices().minus(&can_step);
if cfg!(feature = "print-progress") {
println!(
" > Created initial set for {:?} using {} BDD nodes.",
var,
is_stable.symbolic_size()
);
}
is_stable.into_bdd()
})
.collect();
let mut to_merge = Self::prepare_to_merge(stg, log_level, interrupt)?;

// Finally add the global requirement on the whole state space, if it is relevant.
if !stg.unit_colored_vertices().is_subset(restriction) {
Expand All @@ -480,20 +476,24 @@ impl FixedPoints {
.cloned()
.collect();

interrupt()?;

let bdd =
Self::symbolic_merge(stg.symbolic_context().bdd_variable_set(), to_merge, project);

let vertices = stg.empty_colored_vertices().vertices().copy(bdd);

if cfg!(feature = "print-progress") {
interrupt()?;

if should_log(log_level) {
println!(
"Found {}[nodes:{}] fixed-point vertices.",
vertices.approx_cardinality(),
vertices.symbolic_size(),
);
}

vertices
Ok(vertices)
}

/// Similar to `Self::symbolic_vertices`, but only returns colors for which there exists
Expand All @@ -502,29 +502,24 @@ impl FixedPoints {
stg: &SymbolicAsyncGraph,
restriction: &GraphColoredVertices,
) -> GraphColors {
if cfg!(feature = "print-progress") {
Self::_symbolic_colors(stg, restriction, global_log_level(), &never_stop).unwrap()
}

pub fn _symbolic_colors<E, F: Fn() -> Result<(), E>>(
stg: &SymbolicAsyncGraph,
restriction: &GraphColoredVertices,
log_level: usize,
interrupt: &F,
) -> Result<GraphColors, E> {
if should_log(log_level) {
println!(
"Start symbolic fixed-point color search with {}[nodes:{}] candidates.",
restriction.approx_cardinality(),
restriction.symbolic_size()
);
}

let mut to_merge: Vec<Bdd> = stg
.variables()
.map(|var| {
let can_step = stg.var_can_post(var, stg.unit_colored_vertices());
let is_stable = restriction.minus(&can_step);
if cfg!(feature = "print-progress") {
println!(
" > Created initial set for {:?} using {} BDD nodes.",
var,
is_stable.symbolic_size()
);
}
is_stable.into_bdd()
})
.collect();
let mut to_merge = Self::prepare_to_merge(stg, log_level, interrupt)?;

// Finally add the global requirement on the whole state space, if it is relevant.
if !stg.unit_colored_vertices().is_subset(restriction) {
Expand All @@ -538,20 +533,24 @@ impl FixedPoints {
.cloned()
.collect();

interrupt()?;

let bdd =
Self::symbolic_merge(stg.symbolic_context().bdd_variable_set(), to_merge, project);

let colors = stg.empty_colored_vertices().colors().copy(bdd);

if cfg!(feature = "print-progress") {
interrupt()?;

if should_log(log_level) {
println!(
"Found {}[nodes:{}] fixed-point colors.",
colors.approx_cardinality(),
colors.symbolic_size(),
);
}

colors
Ok(colors)
}

/// This function creates an iterator that yields symbolic sets of fixed-point states, such
Expand Down Expand Up @@ -683,6 +682,29 @@ impl FixedPoints {

solver
}

fn prepare_to_merge<E, F: Fn() -> Result<(), E>>(
stg: &SymbolicAsyncGraph,
log_level: usize,
interrupt: &F,
) -> Result<Vec<Bdd>, E> {
let mut to_merge = Vec::new();
for var in stg.variables() {
let can_step = stg.var_can_post(var, stg.unit_colored_vertices());
let is_stable = stg.unit_colored_vertices().minus(&can_step);
interrupt()?;

if log_essential(log_level, is_stable.symbolic_size()) {
println!(
" > Created initial set for {:?} using {} BDD nodes.",
var,
is_stable.symbolic_size()
);
}
to_merge.push(is_stable.into_bdd());
}
Ok(to_merge)
}
}

#[cfg(test)]
Expand Down
26 changes: 26 additions & 0 deletions src/lib.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -74,6 +74,32 @@ lazy_static! {
static ref ID_REGEX: Regex = Regex::new(ID_REGEX_STR).unwrap();
}

/* TODO: These log level utils can probably move to a separate util crate at some point. */
/* TODO: Logging could be more useful, e.g. print line number and similar info. */
const LOG_NOTHING: usize = 0;
const LOG_ESSENTIAL: usize = 1;
const LOG_VERBOSE: usize = 2;

fn global_log_level() -> usize {
if cfg!(feature = "print-progress") {
1
} else {
0
}
}

fn log_essential(log_level: usize, symbolic_size: usize) -> bool {
log_level >= LOG_VERBOSE || (symbolic_size > 100_000 && log_level >= LOG_ESSENTIAL)
}

fn should_log(log_level: usize) -> bool {
log_level > LOG_NOTHING
}

fn never_stop() -> Result<(), ()> {
Ok(())
}

/// A type-safe index of a `Variable` inside a `RegulatoryGraph` (or a `BooleanNetwork`).
///
/// If needed, it can be converted into `usize` for serialisation and safely read
Expand Down
Loading

0 comments on commit b95165b

Please sign in to comment.