Closed daemontus closed 7 months ago
Attention: 57 lines
in your changes are missing coverage. Please review.
Comparison is base (
60ea437
) 78.13% compared to head (bbb1e00
) 80.26%.
:umbrella: View full report in Codecov by Sentry.
:loudspeaker: Have feedback on the report? Share it here.
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:
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 existingSymbolicContext
andBddVariableSet
. The most important methods are:SymbolicSpaceContext::mk_can_go_to_true
which returns the set of spaces where aBdd
function evaluates totrue
.SymbolicSpaceContext::mk_super_spaces
andSymbolicSpaceContext::mk_sub_spaces
which for a given (colored) set of spaces compute their superset, resp. subset closure.NetworkSpaces
/NetworkColoredSpaces
symbolic set/relation which serves the same purpose asGraphVertices
/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.TrapSpaces
: an uninstantiable API object, similar toFixedPoints
, which currently implements the following:TrapSpaces::symbolic_essential
computes all "essential" trap spaces (trap spaces that cannot be reduced by percolation).TrapSpaces::minimize
andTrapSpaces::maximize
finds the minimal (res. maximal) spaces within a set.TrapSpaces::symbolic_minimal
usesTrapSpaces::symbolic_essential
andTrapSpaces::minimize
to actually compute the set of minimal trap spaces.SymbolicAsyncGraph::with_space_context
to construct aSymbolicAsyncGraph
compatible with the newSymbolicSpaceContext
.Updates to existing API:
GraphColors
,GraphVertices
, andGraphColoredVertices
use the default implementations provided by theBddSet
trait.GraphColoredVertices
whereis_singleton
andpick_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 whichiter
is implemented.GraphVertices::iter
andIntoIterator
forGraphVertices
.OwnedRawSymbolicIterator
. The implementation uses a small hack with unsafe lifetimes, but allows us to implementIntoIterator
forRawProjection
, and in the future for other similar types.Misc changes:
ExtendedBoolean
can be constructed fromOption<bool>
.lib-bdd
androxmltree
.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). AddedSpace::count_exact
as a counterpart toSpace::count_fixed
.bench_trap_spaces_minimal
can be used to quickly test minimal trap space computation.