diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index 94d1774..775e60a 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -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: @@ -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: @@ -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: @@ -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: @@ -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: @@ -92,8 +91,6 @@ 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 @@ -101,16 +98,20 @@ jobs: 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 \ No newline at end of file + path: cobertura.xml diff --git a/Cargo.toml b/Cargo.toml index dd626de..859b5d1 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -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 = [] @@ -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 diff --git a/src/_impl_boolean_network.rs b/src/_impl_boolean_network.rs index 322fea5..d85da27 100644 --- a/src/_impl_boolean_network.rs +++ b/src/_impl_boolean_network.rs @@ -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(); diff --git a/src/_impl_fn_update.rs b/src/_impl_fn_update.rs index e75c23d..f9ea9f8 100644 --- a/src/_impl_fn_update.rs +++ b/src/_impl_fn_update.rs @@ -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}; @@ -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 { + 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` @@ -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()], diff --git a/src/fixed_points/mod.rs b/src/fixed_points/mod.rs index bd0f494..0e518de 100644 --- a/src/fixed_points/mod.rs +++ b/src/fixed_points/mod.rs @@ -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") { diff --git a/src/sbml/import/_read_transitions.rs b/src/sbml/import/_read_transitions.rs index b410e12..5fbc605 100644 --- a/src/sbml/import/_read_transitions.rs +++ b/src/sbml/import/_read_transitions.rs @@ -53,7 +53,6 @@ pub fn read_transitions(model: Node) -> Result, String> { } pub fn read_transition(transition: Node) -> Result { - println!("Node: {:?}", transition); let id = transition .attribute((SBML_QUAL, "id")) .map(|it| it.to_string()); diff --git a/src/symbolic_async_graph/_impl_graph_colored_vertices.rs b/src/symbolic_async_graph/_impl_graph_colored_vertices.rs index a93b33e..a6498d5 100644 --- a/src/symbolic_async_graph/_impl_graph_colored_vertices.rs +++ b/src/symbolic_async_graph/_impl_graph_colored_vertices.rs @@ -187,7 +187,7 @@ 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(), } } @@ -195,7 +195,7 @@ impl GraphColoredVertices { /// 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(), } } diff --git a/src/symbolic_async_graph/_impl_graph_vertices.rs b/src/symbolic_async_graph/_impl_graph_vertices.rs index 424d831..f6f5ecd 100644 --- a/src/symbolic_async_graph/_impl_graph_vertices.rs +++ b/src/symbolic_async_graph/_impl_graph_vertices.rs @@ -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(¶meters_false), state_variables: self.state_variables.clone(), diff --git a/src/symbolic_async_graph/_impl_regulation_constraint.rs b/src/symbolic_async_graph/_impl_regulation_constraint.rs index a195289..6adfc58 100644 --- a/src/symbolic_async_graph/_impl_regulation_constraint.rs +++ b/src/symbolic_async_graph/_impl_regulation_constraint.rs @@ -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) }; @@ -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), }; diff --git a/src/symbolic_async_graph/_impl_symbolic_async_graph.rs b/src/symbolic_async_graph/_impl_symbolic_async_graph.rs index 83dc0a6..80c7d6b 100644 --- a/src/symbolic_async_graph/_impl_symbolic_async_graph.rs +++ b/src/symbolic_async_graph/_impl_symbolic_async_graph.rs @@ -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, ) } @@ -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) } @@ -399,7 +399,7 @@ impl SymbolicAsyncGraph { pub fn existential_extra_variable_projection(&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), ) } diff --git a/src/symbolic_async_graph/projected_iteration.rs b/src/symbolic_async_graph/projected_iteration.rs index 53ba372..b6882ee 100644 --- a/src/symbolic_async_graph/projected_iteration.rs +++ b/src/symbolic_async_graph/projected_iteration.rs @@ -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(¶meters_false), @@ -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.