Biodivine Parametrised Boolean Networks

You can now also access the full functionality of lib-param-bn from Python! The library is available as part of the AEON.py package.

Rust library for working with (parametrised) Boolean networks. Supports:

• Read/Write Boolean network models from .aeon, .bnet, and .sbml formats.
• Basic static analysis, like monotonicity checking or network decomposition.
• Network parameters and partially unknown update functions.
• Fully symbolic asynchronous transition graphs.
• (Legacy) semi-symbolic asynchronous transition graphs.

To learn more, check out the documentation in our tutorial module.

Utility binaries

Aside from the main library, there are a few basic binaries that are used for testing or benchmarking the functionality of the main library. At the moment, these binaries are not a part of the automated testing process as they need to be compiled with optimizations and generally utilize a completely different workflow than standard Cargo tests. In the future, these should be included as separate workflows, but for now, you can use them for manual testing in case you change something in the associated algorithms.

In general, all of these binaries assume a single argument and that is a path to a Boolean network file in any of the supported formats (however, .bnet is not recommended for tests that involve regulation monotonicity). As such, you can run the following command to execute any of the tests (using your desired BINARY_NAME):

cargo run --release --bin BINARY_NAME --features print-progress -- MODEL_PATH

Some algorithms can print intermediate progress when the print-progress feature flag is active. If you don't want this behaviour, remove --features print-progress from the command.

Testing feedback-vertex-set and independent-cycles

Feedback vertex set problem asks to compute the set of vertices such that without these vertices, the graph becomes acyclic. A minimum such set is typically desired.

Independent cycles problem asks to compute the set of non-intersecting cycles such that once removed, the graph becomes acyclic (i.e. every other cycle intersects with a member of this independent set). A maximum such set is typically desired.

There are four binaries related to this feature: check_fvs, check_ic, check_nfvs, and check_nic. The first two test greedy optimizing search for feedback vertex sets and independent cycles. The other two then test the negative variant of the problem (we don't test the positive variant as functionally it is symmetrical to the negative case). Every binary checks the validity of basic invariants that should hold for any correct result.

As these are greedy, non-optimal algorithms, you should expect the algorithms to finish even for very large networks (e.g. >1000 variables). In particular, every model in the BBM benchmark can be processed in less than a second without issues.

Testing fixed-points and projected fixed-points

Fixed-point problem asks to identify every vertex (or combination of parametrisation and vertex for parametrised networks) with no outgoing transitions.

Projected fixed-points problem asks to identify valuations of the desired subset of variables for which there exists at least one fixed-point. In particular, fixed-point vertex x is a vertex for which there exists a color c (parameter valuation) such that x is a fixed-point in c. Symmetrically, color c is a fixed-point color if there exists a vertex x such that x is a fixed-point in c.

There is one test binary check_fixed_points which compares the results of several algorithms to ensure correctness. Additionally, there is bench_fixed_points_naive, bench_fixed_points_symbolic, bench_fixed_points_solver, bench_fixed_points_symbolic_vertices, and bench_fixed_points_symbolic_colors which independently test the performance of each algorithm.

Note that the naive algorithm often runs out of memory on non-trivial models. As such, check_fixed_points can fail once the network is large or has many parameters. That's why benchmarks are separated into individual binaries: because some algorithms can and will time out or OOM.

PBN to colour graph dump

To analyse (very) small networks, it can be useful to dump them as explicit coloured graphs. There is a binary called dump-graph that does exactly this:

cargo build --release
./target/release/dump-graph MODEL_PATH > graph_edges.txt

The binary takes a path to a model file as the first argument, and dumps the graph to standard output.

Since the graph is explicit, expect the output size to be unmanageable for PBNs with roughly >10 variables and >1000 valid parametrizations (with parametrizations being the bigger bottleneck).

You can test the functionality on aeon_models/g2a_*.aeon models which should all be sufficiently small.