Phenotype control alpha release 3

0.4.0-alpha3

versions

0.3.0

This release adds some new functionality and incorporates a lot of the latest changes in biodivine libraries. As opposed to the transition from 0.1.0 to 0.2.0, transition to 0.3.0 should not have any breaking changes.

Complete list of changes:

• Added bindings for HCTL and attractor property classification:
  • run_hctl_classification, run_attractor_classification: compute HCTL or attractor classification map.
  • save_class_archive, load_class_archive: load/store classification results for later use or GUI analysis.
  • get_model_assertions, get_model_properties: read HCTL assertions/properties from an annotated .aeon model.
• Added bindings for HCTL model checking:
  • A HctlTreeNode class is used to manipulate and represent HCTL formulas at runtime.
  • get_extended_stg: extends a SymbolicAsyncGraph with a collection of symbolic variables necessary for model checking.
  • model_check, model_check_multiple: Basic model checking.
  • model_check_extended, model_check_extended_multiple: Model checking, but with "extended" propositions that can map to arbitrary subsets of states.
  • mc_analysis, mc_analysis_multiple: Run model checking with progress printing, sanitization, etc.
• Fixed #13, so BddValuation and BddPartialValuation are now actually iterable objects.
• Added BddVariableSet::transfer_from, SymbolicContext::transfer_from, and SymbolicAsyncGraph::transfer_from/SymbolicAsyncGraph::transfer_colors_from/SymbolicAsyncGraph::transfer_vertices_from. These methods are used to translate a Bdd or a symbolic set between two symbolic domains.
• Added BooleanNetwork::inline_variable and FnUpdate::substitute_variable, which can be used to implement network reduction.
• Added three new example workflow notebooks:
  • classification.ipynb: Classification of network instantiations based on HCTL and attractor properties.
  • file-formats.ipynb: A quick overview of supported file formats and their properties/limitations.
  • model-checking.ipynb: Model checking of HCTL properties on (partially specified) Boolean networks.
  • Examples for the network reduction process will be added later once we resolve a few remaining issues in the Rust backend.

Phenotype control alpha release 2

0.4.0-alpha2

Improved interface for control

Phenotype control alpha release

0.4.0-alphaa1

Bump lib version

Phenotype control alpha version

0.4.0-alpha1

Bump lib version

0.2.0

This is a second "major" release of AEON.py. It adds some of the latest functionality from the internal biodivine libraries (although, still not everything is covered). It also improves significantly on several issues of the original 0.1.0 version, which unfortunately means a few breaking changes in the public API. However, we are getting closer to the stable 1.0.0 release, hopefully later this year, which will then have full ongoing backwards compatibility support and proper API documentation. It is almost certain that there will still be further breaking changes between 0.2.0 and 1.0.0 (e.g. we plan to subdivide AEON.py into proper modules), but many of the new APIs introduced in this version can be considered essentially final.

Key highlights:

• Added support for faster fixed point computation (FixedPoints class).
• Added support for projected enumeration of symbolic sets (SymbolicProjection class).
• Much better coverage of low-level symbolic operations provided by lib-bdd.
• Many new "static analysis" methods like feedback vertex set, independent cycles computation, regulatory graph inference, input inlining, etc.

Complete list of changes (compared to 0.1.1, some of this was previously available as the 0.2.0aX pre-releases):

• AEON.py now comes with a bundled Z3 solver used for some internal features.
• Upgraded to Python 3.11 and Rust 1.69.0, both on PyPI and Conda.
• There is now a more complete set of available workflows and case studies in the example directory.
• Changes in bdd implementation:
  • [breaking] Methods implementing logical operators are now all prefixed with l_* to avoid clashing with Python keywords. Furthermore, logical operations accept an optional limit argument which allows them to fail when the result is too large.
  • [breaking] Replaced Bdd.var_project and Bdd.project with a single polymorphic Bdd.project_exists method.
  • [breaking] Replaced Bdd.var_pick and Bdd.pick with a single polymorphic Bdd.pick method.
  • [breaking] Replaced Bdd.var_select and Bdd.select with a single polymorphic Bdd.select method.
  • [breaking] Replaced Bdd.sat_witness with a richer API for extracting satisfying valuations (see below).
  • Added a BddValuation class. This is essentially a mutable fixed-length list indexed by BddVariable objects. This replaces normal "generic" lists in many places as the "default" argument type. However, whenever possible, the API also accepts normal lists and performs the conversion automatically.
  • Added a BddPartialValuation class. This is essentially a mutable dictionary indexed by BddVariable objects which returns None instead of throwing a KeyError for missing values. Similar to BddValuation, this also now appears in many method types, but the API should be also fine with plain dictionaries.
  • Added actual API to the BooleanExpression class. Now we can manipulate Boolean expressions in Python, but there is a lot of memory copying involved. There is a plan how to fix this in the 1.0 version though, so stay tuned :)
  • Added a Bdd.sem_eq semantic equality method (default == implementation only supports structural equality).
  • Added a Bdd.pick_random method: similar to Bdd.pick, but selects a random valuation. Can be parametrized with a seed.
  • Added a Bdd.project_for_all method: similar to project_exists, but universal instead of existential quantification.
  • Added a Bdd.restrict operator: a combination of select and project_exists.
  • Added Bdd.support_set to retrieve the variables in the BDD and Bdd.size_per_variable to retrieve the number of nodes that utilize individual variables.
  • Added Bdd.valuation_witness and Bdd.valuation_random as well as Bdd.clause_witness and Bdd.clause_random which allow picking elements (either full valuations or partial "cubes"/"clauses").
  • Added Bdd.valuation_iterator and Bdd.clause_iterator which are actual iterable objects through which we can explore all satisfying valuations of a BDD. These are implemented through BddValuationIterator and BddClauseIterator classes.
  • Added BddVariableSet.mk_valuation which "materializes" a BddValuation (or a compatible type) into a singleton Bdd (this was already supported for BddPartialValuation).
  • Bdd.to_dot now optionally supports zero-pruned argument (default True matches the previous behavior).
• Changes in the param-bn implementation:
  • [breaking] A BooleanNetwork now inherits from a RegulatoryNetwork. This means that all methods available on the RegulatoryNetwork are available on a BooleanNetwork as well, typically with no performance impact. As such, some of the original re-implementations were removed.
  • [breaking] Instead of using just strings, there is now a FnUpdate type which represents a single update function that can be queried and manipulated similar to the BooleanExpression. In general, the API should still accept a string wherever possible, but some new methods only accept FnUpdate.
  • [breaking] RegulatoryGraph.targets, RegulatoryGraph.regulators, RegulatoryGraph.targets_transitive and RegulatoryGraph.regulators_transitive now return a set instead of a list.
  • [breaking] RegulatoryGraph.components replaced with a better RegulatoryGraph.strongly_connected_components implementation.
  • Added a ModelAnnotation class which can extract annotation data from .aeon files.
  • Added a new SymbolicContext class which provides mostly the same low-level functionality as its Rust counterpart.
  • Added a SymbolicProjection class which allows iteration over projected elements of a symbolic set (both the state data as well as the "mateiralized" update functions).
  • Classes BooleanNetwork and RegulatoryGraph can now be "pickled". Later, this should extend to more classes, but it will require careful consideration for things like the symbolic sets (ideally, we should just make everything serializable by default, but that will need a bit more work).
  • VariableId and ParameterId now support explicit conversions from/to numbers (from_index and to_index).
  • Added RegulatoryNetwork.shortest_cycle, RegulatoryNetwork.feedback_vertex_set and RegulatoryNetwork.independent_cycles that provide naive algorithms for exploring the network structure.
  • Added BooleanNetwork.num_implicit_parameters and BooleanNetwork.implicit_parameters to list variables with no update functions.
  • Added BooleanNetwork.parameter_appears_in to track which functions contain a specific parameter.
  • Added BooleanNetwork.infer_regulatory_graph (creates a new regulatory graph which is compliant with the current update functions) and BooleanNetwork.inline_inputs (turns input nodes into explicit parameters).
  • Added a FixedPoints class which implements various algorithms for quickly computing fixed points of a symbolic state transition graph. Right now, some of the methods return lists instead of iterators, which will be fixed in the 1.0 release.
  • Added GraphColoredVertices.is_subspace, GraphColoredVertices.is_singleton, GraphColoredVertices.fix_network_variable and GraphColoredVertices.restrict_network_variable. Also added a GraphColoredVertices.new which constructs the set from a "raw" Bdd object. Similar methods were added to GraphColors and GraphVertices.
  • GraphVertices.list_vertices replaced with GraphVertices.iterator (and native __iter__ method), which actually iterates through the members of the set instead of listing them directly.
  • Added several methods for creating and inspecting symbolic sets: SymbolicAsyncGraph.fix_variable_in_vertices, SymbolicAsyncGraph.wrap_in_subspace, SymbolicAsyncGraph.wrap_in_symbolic_subspace, SymbolicAsyncGraph.fix_subspace, SymbolicAsyncGraph.fix_subnetwork_colors, and SymbolicAsyncGraph.is_trap_set.
  • Added several naive fixed-point algorithms for exploring the symbolic graph: SymbolicAsyncGraph.reach_forward, SymbolicAsyncGraph.reach_backward, SymbolicAsyncGraph.trap_forward, and SymbolicAsyncGraph.trap_backward.
  • BooleanNetwork.to_bnet now has an optional rename_if_necessary argument (default False, i.e. previous behavior).
• Other:
  • find_attractors can be now optionally restricted to a specific subset of states.

Internal changes:

• There is now a Wrapper derivation macro which automatically implements From and AsNative conversions between Rust types and their Python wrapper types. In the future, we might be able to also generate other Python-related functionality, such as a working Eq and Ord translation.
• Upgraded to maturin version 1.0.1 for hopefully fewer CI breaking changes in the future and added a custom manylinux Docker image for linux packaging.

0.1.2-alpha

Conda deploy needs build

0.1.1

Several bugfixes to the 0.1.0 release. Mainly, improved to_string implementations for some of the data structures and added hash implementations for types that override equality operator.

0.1.0

First feature complete release of AEON.py

It includes symbolic processing using BDDs, partially specified Boolean networks, attractor detection and source-target control.

0.0.8

Adds preliminary support for target-attractor control.