The class BDD2Dot offers the ability to write binary decision diagrams to dot files. The method BDD2Dot::output_bdd receives a binary decision diagram as parameter a_bdd and writes it to a file in dot format with the name passed as parameter a_file_name.
More...
#include <bdd2dot.h>
|
void | output_bdd (const data_expression &a_bdd, const std::string &a_file_name) |
| Writes the BDD it receives as input to a file.
|
|
The class BDD2Dot offers the ability to write binary decision diagrams to dot files. The method BDD2Dot::output_bdd receives a binary decision diagram as parameter a_bdd and writes it to a file in dot format with the name passed as parameter a_file_name.
Definition at line 29 of file bdd2dot.h.
◆ aux_output_bdd()
void mcrl2::data::detail::BDD2Dot::aux_output_bdd |
( |
const data_expression & |
a_bdd | ) |
|
|
inlineprivate |
Writes the BDD it receives to BDD2Dot::f_dot_file.
- Parameters
-
a_bdd | A binary decision diagram. |
- Precondition
- The argument passed as parameter a_bdd is a data expression in internal mCRL2 format with the following restrictions: It either represents the constant true or the constant false, or it is an if-then-else expression with an expression of Bool as guard, and a then-branch and an else-branch that again follow these restrictions
Definition at line 50 of file bdd2dot.h.
◆ output_bdd()
void mcrl2::data::detail::BDD2Dot::output_bdd |
( |
const data_expression & |
a_bdd, |
|
|
const std::string & |
a_file_name |
|
) |
| |
|
inline |
Writes the BDD it receives as input to a file.
in dot format with the name received as input. precondition: The argument passed as parameter a_bdd is a data expression in internal mCRL2 format with the following restrictions: It either represents the constant true or the constant false, or it is an if-then-else expression with an expression of Bool as guard, and a then-branch and an else-branch that again follow these restrictions
- Parameters
-
a_bdd | A binary decision diagram. |
a_file_name | A file name. |
Definition at line 94 of file bdd2dot.h.
◆ f_bdd_info
BDD_Info mcrl2::data::detail::BDD2Dot::f_bdd_info |
|
private |
A class that gives information about the structure of BDDs.
Definition at line 42 of file bdd2dot.h.
◆ f_dot_file
std::ofstream mcrl2::data::detail::BDD2Dot::f_dot_file |
|
private |
The file the output is written to.
Definition at line 36 of file bdd2dot.h.
◆ f_node_number
int mcrl2::data::detail::BDD2Dot::f_node_number |
|
private |
The smallest unused node number.
Definition at line 33 of file bdd2dot.h.
◆ f_visited
A table containing all the visited nodes. It maps these nodes to the corresponding node numbers.
Definition at line 39 of file bdd2dot.h.
The documentation for this class was generated from the following file:
- data/include/mcrl2/data/detail/prover/bdd2dot.h