Expand description
A fully symbolic coloured graph representation of the Asynchronous Boolean Network.
Internally, this uses the same type of encoding as “normal” AsyncGraph, but it uses
extra BDD variables to represent network state variables (note the distinction between
state and BDD variables).
To the end user, this representation is available via three data structures: GraphVertices,
GraphColors and GraphColoredVertices. The first two represent just the subsets of $V$
and $C$ respectively, while the last is a full subset of $V \times C$.
There is a range of methods that enable (or simplify) the conversion between these three
types of sets (mainly provided by GraphColoredVertices in the form of projections and
vertex-wise operations). Additionally, a VertexSet can be iterated with ArrayBitVectors
used to represent the set elements.
The types of conversions and convenience methods are mainly motivated by SCC decomposition algorithms - if we need something else in the future, it will be implemented.
SymbolicAsyncGraph does not implement the Graph trait because it was not useful
in the fully symbolic context. It provides post, pre, and similar methods directly.
Internally, the representation is maintained by the SymbolicContext which maps each
BDD variable either to a state variable of the network, or to a parameter stored in some
implicit or explicit FunctionTable. The BDD variables are ordered in such a way that
the network parameters follow the variable which they are most closely related to, but
please do not rely on this ordering, it probably will be changed in the future. Overall,
by accessing the SymbolicContext (via SymbolicAsyncGraph) allows implementing almost
any custom BDD operations, but it should be used with caution.
Modules
(internal) Implementing conversion between FnUpdate and BooleanExpression.
(internal) Implementation for FunctionTable and FunctionTableIterator.
(internal) Implement set operations for GraphColoredVertices.
(internal) Implement set operations for GraphColors.
(internal) Implement set operations for GraphVertices.
(internal) Utility methods for validation of static constraints on network regulations.
(internal) Utility methods for SymbolicAsyncGraph.
(internal) Implementation of symbolic utility algorithms.
(internal) Implement symbolic graph operators (pre/post/…).
(internal) Implementation of the SymbolicContext.
Structs
Function table maps one the table of an uninterpreted function to corresponding Bdd variables.
Iterator over elements of the FunctionTable.
Symbolic representation of a coloured set of graph vertices, i.e. a subset of $V \times C$.
Symbolic representation of a color set.
Iterator over graph vertices.
Symbolic representation of a vertex set.
A helper struct that we need in order to make GraphVertices iterable. Elements of such
iterable set are bitvectors, specifically ArrayBitVector.
A symbolic encoding of asynchronous transition system of a BooleanNetwork.
Symbolic context manages the mapping between entities of the Boolean network
(variables, parameters, uninterpreted functions) and BddVariables used in bdd-lib.