Skip to content

0.5.0
Compare
Choose a tag to compare
@daemontus daemontus released this 13 Dec 18:10
· 69 commits to 0.5.0 since this release
v0.5.0
4454841

Well, this is a big one... We are adding several new major features:

Highlights

  • We now support arbitrary expressions as arguments to uninterpreted function calls. For example, f(g(a,b), c | d) is now a valid update function.
  • We have significantly reworked the mechanism behind inline_inputs and inline_variable to be safer, faster, and hopefully easier to understand.
  • We now support symbolic inlining at the level of SymbolicAsyncGraph, i.e. without computing the actual function expression.
  • We now support basic Space percolation.
  • We can now compute minimal and maximal trap spaces, similar to fixed-point computation (see TrapSpaces API object). We can also represent arbitrary sets of spaces symbolically using NetworkSpaces and NetworkColoredSpaces.

Unfortunately, this required a bunch of breaking changes:

  • [breaking contract] Conversion FnUpdate::to_string now produces fewer parentheses around nested & / |. The result is still semantically the same function, but (a & b) & c and a & (b & c) are technically different functions that now resolve to the same string representation (i.e. a & b & c). This helps a lot with readability of DNF/CNF update functions.
  • [breaking contract] A variable with no incoming/outgoing regulations can exist in an .aeon file, as long as it has a specified update function (this function can depend on the logical parameters). While this is rather useless in practice, it can be a reasonable result of a network reduction. It is breaking because a previously invalid model can now be valid.
  • [breaking contract] In .bnet files, the targets,factors header is now treated as case-insensitive. Again, this only makes previously invalid models valid.
  • [breaking API] The signature of FnUpdate::Param changed from (ParameterId, Vec<VariableId>) to (ParameterId, Vec<FnUpdate>). This means the arguments of an uninterpreted function can now be general expressions, not just variables. This required several API changes:
    • FnUpdate::mk_param now accepts &[FnUpdate] instead of &[VariableId]. As an alternative, we provide FnUpdate::mk_basic_param, which is essentially the old function.
    • FnUpdate::as_param now returns &[FnUpdate].
    • FnUpdate::is_specialisation_of removed, as it was never that useful in the first place and became very unclear with the new features.
    • FnUpdate::substitute changed to FnUpdate::rename_all, with more flexible argument types (a map instead of a vector).
    • FnUpdate::eval_in_space removed, as it was also rather useless in the long term.
    • This also changes the signature of several methods in SymbolicContext to use &[FnUpdate] instead of &[VariableId].
  • [breaking API] New algorithms for inlining in BooleanNetwork. This changes the signature/semantics of existing methods and adds a few new ones:
    • Added BooleanNetwork::prune_unused_parameters, as it is often required after inlining.
    • BooleanNetwork::infer_valid_graph is now much more robust w.r.t. uninterpreted functions (it can preserve existing constraints and even simplify the update functions a little bit).
    • Changed the signature of BooleanNetwork::inline_inputs. Now it takes two parameters. One determines if the inputs should be detected semantically (instead of syntactically), the other determines if the RG should be repaired after the inlining (e.g. remove unused regulations).
    • Changed the signature of BooleanNetwork::inline_variable. Now it also takes a repair_graph argument which ensured the returned RG is logically consistent. It can also handle uninterpreted functions much better.
    • Added BooleanNetwork::inline_constants, which is similar to BooleanNetwork::inline_inputs, but for constants. It is essentially percolation at the level of the Boolean network.
  • [breaking API] Changed internal structure of SymbolicAsyncGraph to allow a graph with no underlying BooleanNetwork to exist. This had some relatively minor but wide-ranging consequences:
    • SymbolicAsyncGraph::new and SymbolicAsyncGraph::with_custom_context now only need a reference to a BooleanNetwork.
    • SymbolicAsyncGraph::as_network now returns Option<&BooleanNetwork>.
    • Changed the way witnesses are generated. Each witness should still use DNF instantiation of an update function, but will now have inferred regulatory graph instead of copying the original BN.
    • Renamed SymbolicAsyncGraph::empty_vertices/mk_empty_vertices to SymbolicAsyncGraph::empty_colored_vertices/mk_empty_colored_vertices. Added actual SymbolicAsyncGraph::empty_vertices/mk_empty_vertices/unit_vertices/mk_unit_vertices methods.
    • Added SymbolicAsyncGraph::new_raw, which allows SymbolicAsyncGraph to be constructed from raw update function BDDs.
    • Added a bunch of utility methods that now provide the most important introspection about the SymbolicAsyncGraph (which was previously done by examining the BooleanNetwork):
      • Added SymbolicAsyncGraph::get_variable_name as well as SymbolicContext::get_network_variable_name.
      • Added SymbolicAsyncGraph::num_vars and SymbolicAsyncGraph::variables as well as SymbolicContext::network_variables.
      • Added SymbolicContext::find_network_variable and SymbolicContext::find_state_variable.
  • [breaking API] Removed Space::is_trap_space as it was not correct for general update functions.
  • [breaking API] Removed bdd_params and async_graph modules. These have been deprecated for a long time and were incompatible with the new features.
  • [breaking API] The bin/dump_graph.rs binary is disabled. Someone can probably re-implement it if we ever need it again.
  • [deprecation] GraphVertices::materialize and the IterableVertices struct are now deprecated. You can instead use standard GraphVertices::iter or GraphVertices::into_iter.

Other API changes that are not breaking:

  • Added symbolic representation of network spaces using "dual" encodings:
    • Added SymbolicSpaceContext, which implements the actual translation necessary for the encoding (and extends the functionality of a normal SymbolicContext).
    • Added a NetworkSpaces symbolic set, which is analogous to GraphVertices.
    • Added a NetworkColoredSpaces symbolic relation, which is analogous to GraphColoredVertices.
  • Added an API object TrapSpaces which implements minimal/maximal/essential trap space search.
  • Added OwnedRawSymbolicIterator, which has (roughly) the same features as RawSymbolicIterator, but actually owns the underlying symbolic set and can be thus moved/shared without a lifetime reference.
  • Added From<Option<bool>> for ExtendedBoolean.
  • Added RegulatoryGraph::variable_names to easily obtain an owned list of variable names.
  • Added RegulatoryGraph::add_raw_regulation which can add a regulation using the Regulation object, not strings/IDs.
  • Added Space::new_raw which can create a Space object with just variable count.
  • Added Space::count_fixed as a counterpart to Space::count_any.
  • Added bin/bench_trap_spaces_minimal.rs to test the new trap space feature.
  • Added GraphVertices::iter and GraphVertices::into_iter based on raw symbolic projections.
  • Added FnUpdate::mk_conjunction and FnUpdate::mk_disjunction that simulate n-ary operators.
  • Added FnUpdate::simplify_constants, which eliminates true/false from a function.
  • Added RegulationContraint API object which implements RegulationConstraint::mk_observability, RegulationConstraint::mk_activation, and RegulationConstraint::mk_inhibition, as well as RegulationConstraint::infer_sufficient_regulation and RegulationConstraint::fix_regulation. These can be used to repair regulation graphs using BDD analysis. These are not new functions, but a refactoring of old code that can be now made public.
  • Added SymbolicContext::mk_instantiated_fn_update which can build a FnUpdate from a BddValuation.
  • Added SymbolicAsyncGraph::space_has_var_false and SymbolicAsyncGraph::space_has_var_true as well as SymbolicAsyncGraph::percolate_space. These can be used to implement percolation.
  • Added SymbolicAsyncGraph::with_space_context to create an SymbolicAsyncGraph that can be used for space and state exploration at the same time.
  • Added SymbolicAsyncGraph::get_symbolic_fn_update to retrieve the "raw" underlying update function.
  • Added SymbolicAsyncGraph::inline_symbolic, which can inline a variable at the BDD level, without constructing the underlying network. Also added SymbolicContext::eliminate_network_variable which is required here.
  • Fixed a bug in GraphColoredVertices::is_singleton and GraphColoredVertices::pick_singleton which did not account for possible extra variables.
Assets 2
Loading