Skip to main content Crate merc_symbolic Copy item path Source CubeIter Iterator over all cubes (satisfying assignments) in a BDD. CubeIterAll The same as CubeIter , but iterates over all satisfying assignments without
considering don’t care values. DependencyGraph Represents a dependency graph between variables used in symbolic transition relations. FormatConfig A helper structure to format a configuration for output. FormatConfigSet A helper structure to format configuration sets for output. Hypergraph A hypergraph representation with indices, edges, and vertex weights. PartitionDisplay Display helper that prints all vectors represented by the given signature BDD as numbers, by decoding
the BDD layers as bits, see crate::ldd_to_bdd . Relation A single relation in the dependency graph containing read and write
dependencies onto variables, given by their indices. SignatureDisplay Display helper that prints all vectors represented by the given signature BDD as numbers, by decoding
the BDD layers as bits, see crate::ldd_to_bdd . SummandGroup Represents a short vector transition relation for a group of summands. SummandGroupBdd SylvanLts A symbolic labelled transition system read from a Sylvan file. SylvanTransitionGroup A transition group read from a Sylvan file. SymbolicLts Represents a symbolic LTS encoded by a disjunctive transition relation and a set of states. SymbolicLtsBdd A symbolic LTS that uses BDDs for the symbolic representation, instead of
LDDs as done in crate::SymbolicLts . ValuesIter Iterator that yields values reconstructed from a bit cube, from a BDD obtained by
ldd_to_bdd . SymFormat SymbolicLTS A generic trait representing a symbolic LTS TransitionGroup bdd_from_cube Constructs a BDD representing the given cube (bitvector) over the given variables. bdd_from_iter Create a BDD from the given iterator over bitvector. bdd_to_ldd Converts a BDD representing a set of bitblasted vectors back into an LDD
representing the same set, i.e., the inverse of ldd_to_bdd . bdd_to_ldd_edge Recursive implementation of bdd_to_ldd . bits_to_bdd Constructs a BDD representing the given vector of (optional) bits. compute_bits Computes the number of bits required to represent the highest value at each layer. compute_highest Computes the highest value for every layer in the LDD compute_vars_bdd Creates BDD of variables for the given variable numbers. convert_symbolic_lts Converts a symbolic LTS to an explicit LTS. guess_format_from_extension Guesses the symbolic LTS file format from the file extension. Returns None if it cannot be determined. ldd_to_bdd Converts an LDD representing a set of vectors into a BDD representing the
same set by bitblasting the vector elements using the given variables as
bits. ldd_to_bdd_edge Recursive implementation of ldd_to_bdd . minus Returns the boolean set difference of two BDD functions: lhs \ rhs.
Implemented as lhs AND (NOT rhs). minus_edge Variant of minus that works on edges. parse_compacted_dependency_graph Parses a dependency graph as output by the --info option of both
lpreach and
pbessolvesymbolic . random_bdd Create a random BDD over the given variables with the given number of cubes. random_bitvectors Generate num_vectors random bitvectors of length num_vars. random_symbolic_lts Generates random symbolic LTSs for testing purposes. reachability Performs reachability analysis using the given initial state and transitions from the symbolic LTS. reachability_bdd Performs reachability analysis on the given symbolic LTS represented using BDDs. read_projection Reads the read and write projections from the given stream. read_sylvan Returns the (initial state, transitions) read from the file in Sylvan’s format. read_symbolic_lts Reads a symbolic LTS from a binary stream in the mCRL2 .sym format. reorder Default implementation of reorder when kahypar feature is not enabled. required_bits Calculate minimum bits needed to represent the value
Use 1 bit if value is 0 to ensure at least 1 bit is written required_bits_64 Calculate minimum bits needed to represent the value sigref_symbolic Computes the reduction of the given symbolic LTS using symbolic signature
refinement. support Computes the support (set of variables) of the given BDD function. to_value Reconstruct the value represented by the bits as encoded by
crate::ldd_to_bdd . So most significant bit first. variable_rename Specialized substitution function for variables renaming that only works for
f[x <- x+1] renamings. variable_rename_edge Implementation of variable_rename . variable_rename_reverse Specialized substitution function for variables renaming that only works for
f[x+1 <- x] renamings, similar to variable_rename . variable_rename_reverse_edge Implementation of variable_rename . BDDSupport The BDD representing the support variables of a BDD function. Substitution