0.4.2

This release introduces some new APIs, but they are mainly intended for internal use, hence this is only a minor release.

• You can now (unofficially) use 0/1 instead of false/true constants in logical expressions (applies both to .bnet and .aeon files).
• Now there is support for "extra" BDD variables managed by the SymbolicContext, so that you can create symbolic models "decorated" with additional functionality. Specifically:
  • There is a new constructor SymbolicContext::with_extra_state_variables, which you can use to create a symbolic context with an arbitrary number of extra BDD variables.
  • To access these extra variables, you can use SymbolicContext::all_extra_state_variables, SymbolicContext::extra_state_variables, SymbolicContext::extra_state_variables_by_offset, SymbolicContext::get_extra_state_variable, and SymbolicContext::mk_extra_state_variable_is_true.
  • Just in case you need it, there is now also SymbolicContext::num_state_variables, SymbolicContext::num_parameter_variables, and SymbolicContext::num_extra_state_variables.
  • Similarly, there is a new constructor SymbolicAsyncGraph::with_custom_context that you can use to create a graph with a specific context and "unit" symbolic universe. There are several caveats as to how the SymbolicAsyncGraph can break if you mix the extra symbolic variables into the existing data structures, but as long as you use them outside of the SymbolicAsyncGraph API, you should be fine.
  • There is SymbolicAsyncGraph::existential_extra_variable_projection and SymbolicAsyncGraph::universal_extra_variable_projection which project a symbolic set that uses extra state variables onto a normal set that is guaranteed to be compatible with this symbolic graph.
  • Computation of approx_cardinality and exact_cardinality has been adjusted to account for extra symbolic variables.
  • Finally, there is a new trait called BddSet which now provides default implementations for most common symbolic operations (including the whole Set trait). This removes a lot of redundant code, but some of the old methods are still included to avoid breaking compatibility. Later, we should deprecate them and remove them from the library.

0.4.1

Unfortunately, it turns out that roxmltree version 0.16.0 contains an infinite loop/memory leak and is unusable in some instances. Hence this version downgrades to 0.15.1 for now.

0.4.0

This release is actually quite big, but it mostly introduces new features (there are some minor modifications, but nothing breaking). Sadly, I don't have a tutorial for the new features yet. There is a second "batch" of features hopefully coming soon related to trap spaces. Once that is available, we can write a coherent tutorial on both releases.

Highlights

1. There is now a "solver context" (similar to "symbolic context") that can be used to rewrite certain problems as Z3 queries.
2. There are new, more efficient algorithms for computing fixed points and "projected" fixed points using both symbolic and solver methods.
3. There is a new suite of algorithms for analysing the structure of cycles in the RegulatoryGraph. This includes feedback vertex sets, independent cycles (with variants restricted to induced subgraphs and desired cycle parity), but also cycle and SCC detection in general.

Detailed changelog:

• CI changes:
  • We use a single fixed version of Rust for testing to avoid breaking the workflows randomly with new clippy issues.
  • We don't run the workflow on dev-* branches (but we still run it on pull requests). Please don't merge dev-* branches into master without a PR.
• Project level changes:
  • We now have a "flexible" dependency on lib-bdd (>=0.4.2, <1.0.0). If you make changes that depend on newer versions, you can increase the minimum 0.4.2 version, but overall this should ensure that newer versions of lib-bdd can be used without re-releasing lib-parm-bn.
  • We now depend on z3. For now, this is a dynamic dependency (i.e. the binaries will look for z3.ddl or libz3.so or whatever is required on your system). However, if you build products using lib-parm-bn, consider linking to a static version of z3 to avoid runtime errors due to version incompatibility.
• Additions to existing API:
  • BooleanNetwork::try_from_file: Read a Boolean model from a file. Automatically detects the model format based on file extension (.sbml/.bnet/.aeon).
  • BooleanNetwork::parameter_appears_in: Compute the set of variables whose update function (syntactically) depends on the given parameter.
  • BooleanNetwork::inline_inputs: Transforms variables into parameters when it's safe to do. This is still a "best effort" implementation in that some information is lost (e.g. observability/monotonicity is very hard to interpret after the transformation). However, the SymbolicAsyncGraph if the simplified network should not miss any dynamics of the original network.
  • FnUpdate::contains_parameter and FnUpdate::contains_variable: Check if a VariableId or ParameterId appears in this function (syntactically).
  • FnUpdate::to_and_or_normal_form: Eliminate all Boolean operators except for conjunction, disjuction and negation (however, negation can still appear anywhere in the formula).
  • FnUpdate::distribute_negation: Ensures negation is only applied to the literals of the formula (variables or function invocations).
  • ParameterId and VariableId now have proper usize coversion methods (to_index and from_index). Keep in mind that with great power comes great responsibility (avoid them unless you really have to).
  • RegulatoryGraph::components is now deprecated in favour of RegulatoryGraph::strongly_connected_components (which is a completely new algorithm).
  • New or reimplemented methods for analysis of a RegulatoryGraph (see SdGraph below for details):
    • RegulatoryGraph::strongly_connected_components
    • RegulatoryGraph::restricted_strongly_connected_components
    • RegulatoryGraph::transitive_regulators
    • RegulatoryGraph::transitive_targets
    • RegulatoryGraph::shortest_cycle
    • RegulatoryGraph::shortest_parity_cycle
    • RegulatoryGraph::feedback_vertex_set
    • RegulatoryGraph::parity_feedback_vertex_set
    • RegulatoryGraph::independent_cycles
    • RegulatoryGraph::independent_parity_cycles
  • FunctionTable::symbolic_variables for when you need all variables that are used to represent a single uninterpreted function.
  • GraphColoredVertices::is_subspace, GraphColoredVertices::is_singleton, plus the same thing for GraphColors and GraphVertices: Check if the set is a singleton (one value) or a subspace (can be described by a single conjunction).
    *GraphColoredVertices::fix_network_variable, GraphColoredVertices::restrict_network_variable, the same for GraphVertices: Restrict/transform the set of values without requiring interaction with the SymbolicAsyncGraph.
  • SymbolicAsyncGraph::fix_vertices_with_network_variable: The same as fix_network_variable, but the result is GraphVertices, not GraphColoredVertices, which can be faster if you don't care about colors.
  • SymbolicAsyncGraph::wrap_in_subspace: Compute the smallest subspace that contains a set of graph vertices (for now, this does not work with colors).
  • SymbolicasyncGraph::wrap_in_symbolic_subspace: Compute the smallest symbolic set that is a vertex hypercube but still contains all results. As this is a fully symbolic operations, it can also work with colors, but note that colors are not affected: i.e. the result is a subspace only in the state variables, not parameter variables.
  • SymbolicAsyncGraph::is_trap_set: Test if the given symbolic set is a trap set.
  • SymbolicAsyncGraph::restrict_variable_in_graph: Create a new SymbolicAsyncGraph that fixes the value of a certian varaible, but the erases it from the update functions. So the dynamics of the new graph are still valid in the subspace where the given variable is fixed (and possibly easier to analyse), but in general not all transitions are preserved outside of this subspace.
• Completely new API:
  • ExtendedBoolean is essentially the 1/0/* enum used to express the variable's value in a subspace:
    • The type implements an "overapproximated" Boolean algebra (negate/and/or/implies/...), such that you can evaluate Boolean expressions using ExtendedBoolean and get a valid result.
  • Space represents a hypercube of states:
    • You can index Space using VariableId to retrieve/save values.
    • Spaces implement a partial order based on inclusion.
    • You can use the ExtendedBoolean algebra with FnUpdate::eval_in_space to use Space as an input to a Boolean function and get a valid result. This is then used in Space::is_trap_space to check if a space is a trap.
  • SdGraph is a "cleaner" implementation of a "signed directed graph" on which we implement things like cycle detection (you can create it from a RegulatoryGraph and some new methods on RegulatoryGraph use it internally). Everything in here uses standard explicit graph algorithms, but should be fast enough on graphs with less than 1M nodes:
    • Find shortest cycles in the interaction graph: SdGraph::shortest_cycle_length and SdGraph::shortest_cycle.
    • Find shortest parity cycles (positive/negative): SdGraph::shortest_parity_cycle_length and SdGraph::shortest_parity_cycle.
    • Greedily find "small" feedback vertex set and parity feedback vertex set (optionally restricted to an induced subgraph): SdGraph::restricted_feedback_vertex_set and SdGraph::restricted_parity_feedback_vertex_set.
    • Greedily find "large" set of independent cycles and independent parity cycles (again, with an optional restriction): SdGraph::restricted_independent_cycles and SdGraph::restricted_independent_parity_cycles.
    • Compute forward/backward reachable vertices (with an optional restriction): SdGraph::forward_reachable, SdGraph::backward_reachable, SdGraph::restricted_forward_reachable, SdGraph::restricted_backward_reachable.
    • Compute strongly connected components: SdGraph::strongly_connected_components, SdGraph::restricted_strongly_connected_components.
    • Compute weakly connected components: SdGraph::weakly_connected_components, SdGraph::restricted_weakly_connected_components.
  • There is the BnSolverContext object, which implements an encoding of a Boolean network into a format that Z3 solver will understand. This is modelled largely to act similar to the SymbolicContext object:
    • BnSolverContext::declare_state_variables: Declare a fresh batch of variables based on the variables of the underlying Boolean network.
    • BnSolverContext::get_variable_constructor, BnSolverContext::get_explicit_parameter_constructor, BnSolverContext::get_implicit_parameter_constructor: Obtain the internal Z3 objects which represent symbol constructors for the corresponding Boolean network constructs.
    • BnSolverContext::mk_empty_solver and BnSolverContext::mk_network_solver: Create a new solver with no constraints (just the constructors/declarations) and create a new solver which also contains all static network constraints (monotonicity, essentiality, etc.).
    • BnSolverContext::mk_var, BnSolverContext::mk_explicit_parameter, BnSolverContext::mk_explicit_const_parameter, BnSolverContext::mk_implicit_parameter, BnSolverContext::mk_implicit_const_parameter, BnSolverContext::mk_update_function, BnSolverContext::mk_space: Create Z3 formula literals that are satisfied by the corresponding Boolean network objects (you can then combine these using logical connectives).
    • BnSolverContext::translate_space and BnSolverContext::translate_update_function: The same as above, but you supply your own variable constructors (e.g. after obtaining them from declare_state_variables). This means the resulting literal corresponds to your solver variables, and not the implicit ones.
  • BnSolver and BnSolverModel describe the collection of constraints to be s...

0.3.0

There are several (very minor) breaking changes in this update, plus a whole lot of quality-of-life improvements.

High-level project changes:

• Switch to Rust edition 2021.
• Remove .githooks and shields_up feature due to lack of use.
• Add dependency on num-bigint and num-traits to enable support for infinite-precision set cardinality computations.

Other API changes:

• [potentially breaking] BooleanNetwork::to_bnet now accepts a boolean argument that forces the method to rename network variables when they do not have bnet-compatible names. To migrate, just add false as argument value.
• Added BooleanNetwork::num_implicit_parameters and BooleanNetwork::implicit_parameters to easily allow enumeration of erased update functions.
• Added BooleanNetwork::infer_valid_graph that constructs the most specific RegulatoryGraph that is still consistent with every Boolean function admissible in this network.
• Added several utility functions to FnUpdate, specifically FnUpdate::evaluate, FnUpdate::is_specialisation_of, FnUpdate::walk_postorder and FnUpdate::substitute.
• [potentially breaking] RegulatoryGraph now uses a new PartialEq implementation that does not require equivalent ordering of regulations within the graph. This generally shouldn't break anything important, because any graphs that were equivalent are still equivalent, and two graphs that became equivalent due to this change are functionally equivalent in every way except for iteration order in RegulatoryGraph::regulations.
• Added RegulatoryGraph::to_dot and RegulatoryGraph::write_as_dot to allow quick conversion to .dot files for visualisation (e.g. in Python notebooks).
• [potentially breaking] Added exact_cardinality methods to all symbolic sets, using num-bigint. Additionally, all approx_cardinality methods will also attempt to use the exact method (and covert to f64 afterwards) if the approximate method returns Inf or NaN. As a consequence, cases that returned Inf with the previous implementation can now actually return a meaningful number if the exact value is small enough. In other words, now, if approx_cardinality returns Inf, you can be sure that there are indeed more than f64::MAX values within the set, whereas before, Inf could be returned due to overflow during computation.
• Added SymbolicAsyncGraph::mk_subspace and SymbolicAsyncGraph::mk_partial_vertex to make the creation of restricted symbolic sets easier.
• Added SymbolicAsyncGraph::restrict that creates a copy of the original graph that is induced by the given set of vertices. That is, the resulting graph has fewer states and transitions.
• Added SymbolicAsyncGraph::mk_subnetwork_colors, that can (for a limited syntactically verifiable set of cases) identify the specific parameter valuation that corresponds to the given BooleanNetwork within the parameter space of this (less restrictive) SymbolicAsyncGraph.
• Added SymbolicAsyncGraph::reach_forward, SymbolicAsyncGraph::reach_backward, SymbolicAsyncGraph::trap_forward and SymbolicAsyncGraph::trap_backward that provide a "reference" implementation for basic reachability procedures.
• All variable-specific transition operators in SymbolicAsyncGraph now use only one (ternary) symbolic operation, which reduces the overhead in many cases. Furthermore, a few new operators were added (var_post_out and var_pre_out).

0.2.4

Fixes two minor issues:

• Until now, it was possible to export invalid bnet models by including variables whose name starts with a number. This is now an error.
• Symbolic sets now all have the same utility methods (symbolic_size, pick_singleton, etc.). Until now, this was not supported for all types.

0.2.3

Fixes a miscommunication in the specification of will_post_within and will_pre_within: Now the functions actually compute what they intuitively mean. Previously, the functions only preserved states that could perform post/pre under all network variables.

Additionally, an _out alternative to _within is provided with the same complexity.

0.2.2

This small release introduces can_post_within, will_post_within as well as can_pre_within and will_pre_within functions to the SymbolicAsyncGraph. These functions can be used for example to trim acyclic states from a set, or to find a strong basin within a weak basin.

This functionality can be at the moment achieved using pre/post plus intersection. However, the new functions use a smaller number of BDD operations internally, and hence can achieve roughly 20-30% speedup compared to the "naive" approach.

0.2.1

Adds a set_variable_name utility method to RegulatoryGraph.

0.2.0

This release primarily includes a new experimental .bnet parser (should be working for most models, but some advanced features and safety checks are missing). But there are also a few bug fixes:

• A .bnet parser (regulations are automatically loaded as observable, but without monotonicity).
• A .bnet writer (naturally, only supports networks without parametrised functions).
• Upgraded lib-bdd to 0.3.0.
• Allow <true/> and <false/> tags in functions in SBML models.
• Fix SBML export for constant functions.
• Added BooleanNetwork::set_update_function and BooleanNetwork::as_graph_mut, however, these methods do not perform any special consistency checks, so use them with caution! (Should be later addressed in #21)
• Explicitly deprecated AsyncGraph. (Should be later addressed in #18)
• Added a new binary (bnet_parametrizer) which is able to turn an Aeon model with uninterpreted functions into a valid bnet model by "exploding" the functions into basic parameters.
• Better error message when reading an SBML file which is not a qualitative model.
• Unofficial support for essential attribute in SBML to denote observable/non-observable regulations.
• SymbolicAsyncGraph now implements Clone for convenience.

0.1.0

First stable release with working semi- and fully-symbolic asynchronous graphs, static analysis, stable SBML and many other features.