Skip to content

0.4.4

Compare
Choose a tag to compare
@daemontus daemontus released this 27 Feb 16:14
· 20 commits to 0.4.0 since this release

This version introduces the ability to iterate over projections of symbolic sets. There is one breaking change regarding the way witnesses are generated, but this does not modify the API in any way.

  • [bugfix] Added missing mut in ModelAnnotation::get_mut_child.
  • Added FnUpdate::build_from_bdd, which can be used to construct DNF update functions from instantiated BDDs obtained through SymbolicContext::instantiate_*.
  • The new FnUpdate::build_from_bdd function is now used to generate update functions in witness networks. For small/simple functions, the results should be much more readable (in particular, they don't contain implication, which can be confusing).
  • Added symbolic_async_graph::projected_iteration module with the newly introduced iterators. Namely, RawProjection, StateProjection, FnUpdateProjection and MixedProjection. These allow us to interpret any symbolic set through a "view" restricted to state/parameter variables, or a mixture of both.
  • Added GraphColoredVertices::state_projection, GraphColoredVertices::fn_update_project, GraphColoredVertices::mixed_projection and GraphColoredVertices::raw_projection. Similar methods have been added to GraphColors and GraphVertices where relevant.
  • Added FixedPoints::symbolic_projection which computes a projected result directly (this is faster than computing the full result and then projecting afterwards).