Computation of minimal trap spaces

[daemontus]

This PR adds the ability to compute minimal trap spaces, similar to how fixed-points can be computed already. It also slightly improves APIs related to iteration.

In terms of validation, I have only added some basic tests, but I compared the results to trappist on BBM models and everything seems to be in order. We can add an automated comparison down the line, but for now I didn't really want to bother with calling Python dependencies from Rust.

Som initial API was already present, so this tries to align with it as well as we can.

Trap space related API:

• Added a SymbolicSpaceContext, which implements the "dual" encoding of Boolean spaces (each network variable is represented as two BDD variables). The API has basic utility methods, but mostly relies on existing SymbolicContext and BddVariableSet. The most important methods are:
  • SymbolicSpaceContext::mk_can_go_to_true which returns the set of spaces where a Bdd function evaluates to true.
  • SymbolicSpaceContext::mk_super_spaces and SymbolicSpaceContext::mk_sub_spaces which for a given (colored) set of spaces compute their superset, resp. subset closure.
• Added a NetworkSpaces/NetworkColoredSpaces symbolic set/relation which serves the same purpose as GraphVertices/GraphColoredSpaces, but encodes spaces instead of states. The API almost completely mirrors the vertex-based counterpart. But the sets are not commonly used in many APIs right now, so we might add more utility methods in the future.
• Added TrapSpaces: an uninstantiable API object, similar to FixedPoints, which currently implements the following:
  • TrapSpaces::symbolic_essential computes all "essential" trap spaces (trap spaces that cannot be reduced by percolation).
  • TrapSpaces::minimize and TrapSpaces::maximize finds the minimal (res. maximal) spaces within a set.
  • TrapSpaces::symbolic_minimal uses TrapSpaces::symbolic_essential and TrapSpaces::minimize to actually compute the set of minimal trap spaces.
• Added SymbolicAsyncGraph::with_space_context to construct a SymbolicAsyncGraph compatible with the new SymbolicSpaceContext.

Updates to existing API:

• Where applicable, functions in GraphColors, GraphVertices, and GraphColoredVertices use the default implementations provided by the BddSet trait.
• Fixed a bug in GraphColoredVertices where is_singleton and pick_singleton did not account for extra symbolic variables.
• IterableVertices is now deprecated, GraphVertices::iter()/into_iter() can be used directly. Related methods are preserved for compatibility, but essentially defer to the new mechanism through which iter is implemented.
• With that said... added GraphVertices::iter and IntoIterator for GraphVertices.
• This is all implemented through a new OwnedRawSymbolicIterator. The implementation uses a small hack with unsafe lifetimes, but allows us to implement IntoIterator for RawProjection, and in the future for other similar types.

Misc changes:

• ExtendedBoolean can be constructed from Option<bool>.
• Adds one new model for testing, mostly because it is relatively simple and we know what the trap spaces should look like.
• Updated lib-bdd and roxmltree.
• Removed Space::is_trap_space as it was misleading (the test was only correct for update functions in CNF/DNF but not for truly general functions). Added Space::count_exact as a counterpart to Space::count_fixed.
• A simple binary bench_trap_spaces_minimal can be used to quickly test minimal trap space computation.

[codecov]

Codecov Report

Attention: 57 lines in your changes are missing coverage. Please review.

Comparison is base (60ea437) 78.13% compared to head (bbb1e00) 80.26%.

Files	Patch %	Lines
src/symbolic_async_graph/_impl_graph_vertices.rs	38.88%	11 Missing ⚠️
src/trap_spaces/_impl_network_colored_spaces.rs	86.74%	11 Missing ⚠️
src/trap_spaces/_impl_symbolic_space_context.rs	89.90%	11 Missing ⚠️
src/trap_spaces/_impl_network_spaces.rs	88.88%	7 Missing ⚠️
...mbolic_async_graph/_impl_graph_colored_vertices.rs	78.26%	5 Missing ⚠️
src/_impl_extended_boolean.rs	0.00%	4 Missing ⚠️
src/symbolic_async_graph/_impl_graph_colors.rs	40.00%	3 Missing ⚠️
src/trap_spaces/_impl_trap_spaces.rs	96.15%	3 Missing ⚠️
src/_impl_space.rs	0.00%	2 Missing ⚠️

Additional details and impacted files

@@            Coverage Diff             @@
##           master      #51      +/-   ##
==========================================
+ Coverage   78.13%   80.26%   +2.13%     
==========================================
  Files          67       71       +4     
  Lines        4377     4744     +367     
==========================================
+ Hits         3420     3808     +388     
+ Misses        957      936      -21     

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.