Skip to content

Commit

Permalink
Merge branch 'master' into 0.4.0
Browse files Browse the repository at this point in the history
  • Loading branch information
daemontus committed Jun 5, 2023
2 parents f1c59e5 + 9964e74 commit 2aa0a77
Show file tree
Hide file tree
Showing 11 changed files with 80 additions and 64 deletions.
67 changes: 34 additions & 33 deletions .github/workflows/build.yml
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@ env:
# A fixed version used for testing, so that the builds don't
# spontaneously break after a few years.
# Make sure to update this from time to time.
RUST_VERSION: "1.65.0"
RUST_VERSION: "1.69.0"
jobs:
# Check formatting
fmt:
Expand All @@ -23,12 +23,12 @@ jobs:
env:
RUSTFLAGS: "-D warnings"
steps:
- name: Checkout.
uses: actions/checkout@v3
- name: Install Rust toolchain.
run: curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh -s -- -y --default-toolchain ${{ env.RUST_VERSION }}
- name: Rust format check.
run: cargo fmt --all -- --check
- uses: actions/checkout@v3
- uses: dtolnay/rust-toolchain@stable
with:
toolchain: ${{ env.RUST_VERSION }}
components: rustfmt
- run: cargo fmt --all -- --check

# Run basic code validity check.
check:
Expand All @@ -38,12 +38,11 @@ jobs:
env:
RUSTFLAGS: "-D warnings"
steps:
- name: Checkout.
uses: actions/checkout@v3
- name: Install Rust toolchain.
run: curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh -s -- -y --default-toolchain ${{ env.RUST_VERSION }}
- name: Rust code validity check.
run: cargo check
- uses: actions/checkout@v3
- uses: dtolnay/rust-toolchain@stable
with:
toolchain: ${{ env.RUST_VERSION }}
- run: cargo check --all-features

# Run all tests
test:
Expand All @@ -62,12 +61,12 @@ jobs:
version: 4.11.2
env:
GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
- name: Checkout.
uses: actions/checkout@v3
- name: Install Rust toolchain.
run: curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh -s -- -y --default-toolchain ${{ env.RUST_VERSION }}
- name: Run tests.
run: cargo test --all-features
- uses: actions/checkout@v3
- uses: dtolnay/rust-toolchain@stable
with:
toolchain: ${{ env.RUST_VERSION }}
components: rustfmt
- run: cargo test --all-features

# Check code style
clippy:
Expand All @@ -77,12 +76,12 @@ jobs:
env:
RUSTFLAGS: "-D warnings"
steps:
- name: Checkout.
uses: actions/checkout@v3
- name: Install Rust toolchain.
run: curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh -s -- -y --default-toolchain ${{ env.RUST_VERSION }}
- name: Run clippy.
run: cargo clippy
- uses: actions/checkout@v3
- uses: dtolnay/rust-toolchain@stable
with:
toolchain: ${{ env.RUST_VERSION }}
components: clippy
- run: cargo clippy --all-features

# Compute code coverage
codecov:
Expand All @@ -92,25 +91,27 @@ jobs:
steps:
- name: Checkout.
uses: actions/checkout@v3
- name: Install Rust toolchain.
run: curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh -s -- -y --default-toolchain ${{ env.RUST_VERSION }}
- name: Setup Z3.
id: z3
uses: cda-tum/setup-z3@v1
with:
version: 4.11.2
env:
GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
- name: Setup cargo-tarpaulin.
run: cargo install cargo-tarpaulin
- name: Run tarpaulin to compute coverage.
run: cargo tarpaulin --verbose --lib --examples --all-features --out Xml
- uses: dtolnay/rust-toolchain@stable
with:
toolchain: ${{ env.RUST_VERSION }}
# Install action using cargo-binstall, which is faster because we don't have to compile tarpaulin every time.
- uses: taiki-e/install-action@v2
with:
tool: cargo-tarpaulin
- run: cargo tarpaulin --verbose --lib --examples --all-features --out Xml
- name: Upload to codecov.io
uses: codecov/codecov-action@v1.0.2
uses: codecov/codecov-action@v3
with:
token: ${{ secrets.CODECOV_TOKEN }}
- name: Archive code coverage results
uses: actions/upload-artifact@v1
with:
name: code-coverage-report
path: cobertura.xml
path: cobertura.xml
3 changes: 2 additions & 1 deletion Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -33,6 +33,7 @@ required-features = ["solver-z3"]
# Enable rich docs for some online docs autogen services.
[package.metadata.docs.rs]
rustdoc-args = ["--html-in-header", "docs-head.html"]
features = [ "solver-z3" ]

[features]
print-progress = []
Expand All @@ -41,7 +42,7 @@ solver-z3 = ["dep:z3"]
[dependencies]
regex = "1.3.3" # Regexes used for parsing of basic .aeon constructs.
lazy_static = "1.4.0" # Used for initialization of commonly used regexes.
biodivine-lib-bdd = ">=0.4.2, <1.0.0"
biodivine-lib-bdd = ">=0.5.1, <1.0.0"
num-bigint = "0.4.3" # Used as infinite-precision representation in BDDs.
num-traits = "0.2.15" # `BigInt::to_f64`
# The latest versions of roxmltree did some
Expand Down
19 changes: 9 additions & 10 deletions src/_impl_boolean_network.rs
Original file line number Diff line number Diff line change
Expand Up @@ -309,29 +309,28 @@ impl BooleanNetwork {
let regulator_is_false = ctx.bdd_variable_set().mk_not_var(regulator);

let observability = {
let fn_x1_to_1 =
bdd!(fn_is_true & regulator_is_true).var_project(regulator);
let fn_x1_to_1 = bdd!(fn_is_true & regulator_is_true).var_exists(regulator);
let fn_x0_to_1 =
bdd!(fn_is_true & regulator_is_false).var_project(regulator);
bdd!(fn_x1_to_1 ^ fn_x0_to_1).project(ctx.state_variables())
bdd!(fn_is_true & regulator_is_false).var_exists(regulator);
bdd!(fn_x1_to_1 ^ fn_x0_to_1).exists(ctx.state_variables())
};

if !observability.is_false() {
let activation = {
let fn_x1_to_0 =
bdd!(fn_is_false & regulator_is_true).var_project(regulator);
bdd!(fn_is_false & regulator_is_true).var_exists(regulator);
let fn_x0_to_1 =
bdd!(fn_is_true & regulator_is_false).var_project(regulator);
bdd!(fn_x0_to_1 & fn_x1_to_0).project(ctx.state_variables())
bdd!(fn_is_true & regulator_is_false).var_exists(regulator);
bdd!(fn_x0_to_1 & fn_x1_to_0).exists(ctx.state_variables())
}
.not();

let inhibition = {
let fn_x0_to_0 =
bdd!(fn_is_false & regulator_is_false).var_project(regulator);
bdd!(fn_is_false & regulator_is_false).var_exists(regulator);
let fn_x1_to_1 =
bdd!(fn_is_true & regulator_is_true).var_project(regulator);
bdd!(fn_x0_to_0 & fn_x1_to_1).project(ctx.state_variables())
bdd!(fn_is_true & regulator_is_true).var_exists(regulator);
bdd!(fn_x0_to_0 & fn_x1_to_1).exists(ctx.state_variables())
}
.not();

Expand Down
16 changes: 16 additions & 0 deletions src/_impl_fn_update.rs
Original file line number Diff line number Diff line change
@@ -1,5 +1,6 @@
use crate::symbolic_async_graph::SymbolicContext;
use crate::FnUpdate::*;
use crate::_aeon_parser::FnUpdateTemp;
use crate::{BinaryOp, BooleanNetwork, ExtendedBoolean, FnUpdate, ParameterId, Space, VariableId};
use biodivine_lib_bdd::{Bdd, BddPartialValuation, BddVariable};
use std::collections::{HashMap, HashSet};
Expand Down Expand Up @@ -111,6 +112,14 @@ impl FnUpdate {

/// Other utility methods.
impl FnUpdate {
/// Try to parse an update function from a string expression using the provided `network`
/// as context.
pub fn try_from_str(expression: &str, network: &BooleanNetwork) -> Result<FnUpdate, String> {
let tmp = FnUpdateTemp::try_from(expression)?;
let update = tmp.into_fn_update(network)?;
Ok(*update)
}

/// Build an update function from an instantiated `Bdd`.
///
/// The support set of the `Bdd` must be a subset of the state variables, i.e. the `Bdd`
Expand Down Expand Up @@ -655,6 +664,13 @@ mod tests {
let fun = bn.get_update_function(c).as_ref().unwrap();
let fun_string = fun.to_string(&bn);

let fun_parse = FnUpdate::try_from_str(
"a & (a | (a ^ (a => (a <=> !(f(a, b) | (true | false))))))",
&bn,
)
.unwrap();
assert_eq!(fun, &fun_parse);

assert_eq!(vec![a, b], fun.collect_arguments());
assert_eq!(
vec![bn.find_parameter("f").unwrap()],
Expand Down
2 changes: 1 addition & 1 deletion src/fixed_points/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -352,7 +352,7 @@ impl FixedPoints {
for p_var in project.clone() {
let dependencies = dependency_map.get(&p_var).unwrap();
if dependencies.is_subset(&merged) {
result = result.var_project(p_var);
result = result.var_exists(p_var);
project.remove(&p_var);

if cfg!(feature = "print-progress") {
Expand Down
1 change: 0 additions & 1 deletion src/sbml/import/_read_transitions.rs
Original file line number Diff line number Diff line change
Expand Up @@ -53,7 +53,6 @@ pub fn read_transitions(model: Node) -> Result<Vec<SbmlTransition>, String> {
}

pub fn read_transition(transition: Node) -> Result<SbmlTransition, String> {
println!("Node: {:?}", transition);
let id = transition
.attribute((SBML_QUAL, "id"))
.map(|it| it.to_string());
Expand Down
4 changes: 2 additions & 2 deletions src/symbolic_async_graph/_impl_graph_colored_vertices.rs
Original file line number Diff line number Diff line change
Expand Up @@ -187,15 +187,15 @@ impl GraphColoredVertices {
/// Set of all colors which are in this set for at least one vertex.
pub fn colors(&self) -> GraphColors {
GraphColors {
bdd: self.bdd.project(&self.state_variables),
bdd: self.bdd.exists(&self.state_variables),
parameter_variables: self.parameter_variables.clone(),
}
}

/// Set of all vertices which are in this set for at least one colour.
pub fn vertices(&self) -> GraphVertices {
GraphVertices {
bdd: self.bdd.project(&self.parameter_variables),
bdd: self.bdd.exists(&self.parameter_variables),
state_variables: self.state_variables.clone(),
}
}
Expand Down
2 changes: 1 addition & 1 deletion src/symbolic_async_graph/_impl_graph_vertices.rs
Original file line number Diff line number Diff line change
Expand Up @@ -76,7 +76,7 @@ impl GraphVertices {
pub fn materialize(&self) -> IterableVertices {
// This is a colossal hack, but it is easier than trying to drag parameter variables into this.
let all_false: Bdd = BddValuation::all_false(self.bdd.num_vars()).into();
let parameters_false = all_false.project(&self.state_variables);
let parameters_false = all_false.exists(&self.state_variables);
IterableVertices {
materialized_bdd: self.bdd.and(&parameters_false),
state_variables: self.state_variables.clone(),
Expand Down
18 changes: 9 additions & 9 deletions src/symbolic_async_graph/_impl_regulation_constraint.rs
Original file line number Diff line number Diff line change
Expand Up @@ -46,12 +46,12 @@ pub(crate) fn apply_regulation_constraints(
*/
let observability = if regulation.observable {
// \exists x_r : F(x_1, ..., x_r, ..., x_n) & x_r | Context where F is one for x_r, but with x_r erased.
let fn_x1_to_1 = bdd!(fn_is_true & regulator_is_true).var_project(regulator);
let fn_x1_to_1 = bdd!(fn_is_true & regulator_is_true).var_exists(regulator);
// \exists x_r : F(x_1, ..., x_r, ..., x_m) & !x_r | Context where F is one for !x_r, but with x_r erased.
let fn_x0_to_1 = bdd!(fn_is_true & regulator_is_false).var_project(regulator);
let fn_x0_to_1 = bdd!(fn_is_true & regulator_is_false).var_exists(regulator);
// Context where F for x_r is not equal F for !x_r (i.e. all witnesses of observability)
// and then with all states erased.
bdd!(fn_x1_to_1 ^ fn_x0_to_1).project(&context.state_variables)
bdd!(fn_x1_to_1 ^ fn_x0_to_1).exists(&context.state_variables)
} else {
context.mk_constant(true)
};
Expand All @@ -76,14 +76,14 @@ pub(crate) fn apply_regulation_constraints(
*/
let non_monotonous = match regulation.monotonicity {
Some(Monotonicity::Activation) => {
let fn_x1_to_0 = bdd!(fn_is_false & regulator_is_true).var_project(regulator);
let fn_x0_to_1 = bdd!(fn_is_true & regulator_is_false).var_project(regulator);
bdd!(fn_x0_to_1 & fn_x1_to_0).project(&context.state_variables)
let fn_x1_to_0 = bdd!(fn_is_false & regulator_is_true).var_exists(regulator);
let fn_x0_to_1 = bdd!(fn_is_true & regulator_is_false).var_exists(regulator);
bdd!(fn_x0_to_1 & fn_x1_to_0).exists(&context.state_variables)
}
Some(Monotonicity::Inhibition) => {
let fn_x0_to_0 = bdd!(fn_is_false & regulator_is_false).var_project(regulator);
let fn_x1_to_1 = bdd!(fn_is_true & regulator_is_true).var_project(regulator);
bdd!(fn_x0_to_0 & fn_x1_to_1).project(&context.state_variables)
let fn_x0_to_0 = bdd!(fn_is_false & regulator_is_false).var_exists(regulator);
let fn_x1_to_1 = bdd!(fn_is_true & regulator_is_true).var_exists(regulator);
bdd!(fn_x0_to_0 & fn_x1_to_1).exists(&context.state_variables)
}
None => context.mk_constant(false),
};
Expand Down
6 changes: 3 additions & 3 deletions src/symbolic_async_graph/_impl_symbolic_async_graph.rs
Original file line number Diff line number Diff line change
Expand Up @@ -132,7 +132,7 @@ impl SymbolicAsyncGraph {
GraphVertices::new(
self.unit_bdd
.var_select(bdd_variable, value)
.project(&self.symbolic_context.parameter_variables),
.exists(&self.symbolic_context.parameter_variables),
&self.symbolic_context,
)
}
Expand Down Expand Up @@ -335,7 +335,7 @@ impl SymbolicAsyncGraph {
cube: &GraphColoredVertices,
) -> GraphColoredVertices {
let bdd_var = stg.symbolic_context().get_state_variable(var);
let relaxed_bdd = cube.as_bdd().var_project(bdd_var);
let relaxed_bdd = cube.as_bdd().var_exists(bdd_var);
stg.empty_vertices().copy(relaxed_bdd)
}

Expand Down Expand Up @@ -399,7 +399,7 @@ impl SymbolicAsyncGraph {
pub fn existential_extra_variable_projection<T: BddSet>(&self, set: &T) -> T {
set.copy(
set.as_bdd()
.project(&self.symbolic_context.all_extra_state_variables),
.exists(&self.symbolic_context.all_extra_state_variables),
)
}

Expand Down
6 changes: 3 additions & 3 deletions src/symbolic_async_graph/projected_iteration.rs
Original file line number Diff line number Diff line change
Expand Up @@ -63,10 +63,10 @@ impl RawProjection {
.into_iter()
.filter(|it| !retained.contains(it))
.collect();
let projection = bdd.project(&to_eliminate);
let projection = bdd.exists(&to_eliminate);
// Then fix everything that is not retained to `False` to ensure succinct enumeration.
let all_false = BddValuation::all_false(projection.num_vars());
let parameters_false = Bdd::from(all_false).project(&retained);
let parameters_false = Bdd::from(all_false).exists(&retained);
RawProjection {
retained_variables: retained,
bdd: projection.and(&parameters_false),
Expand Down Expand Up @@ -210,7 +210,7 @@ impl<'a, 'b> Iterator for FnUpdateProjectionIterator<'a, 'b> {
/// the network variables and some of the update functions.
///
/// This type of projection can be used to relate a specific state to a specific update function.
/// For example, how does a phenotype variable changes with a particular update function?
/// For example, how does a phenotype variable change with a particular update function?
///
/// Note that the same considerations regarding `FnUpdate` uniqueness as for `FnUpdateProjection`
/// apply here as well.
Expand Down

0 comments on commit 2aa0a77

Please sign in to comment.