mcrl2::data::detail::BDD2Dot Class Reference

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>

Public Member Functions
void	output_bdd (const data_expression &a_bdd, const std::string &a_file_name)
	Writes the BDD it receives as input to a file.

Private Member Functions
void	aux_output_bdd (const data_expression &a_bdd)
	Writes the BDD it receives to BDD2Dot::f_dot_file.

Private Attributes
int	f_node_number = 0
	The smallest unused node number.
std::ofstream	f_dot_file
	The file the output is written to.
std::map< atermpp::aterm, atermpp::aterm_int >	f_visited
	A table containing all the visited nodes. It maps these nodes to the corresponding node numbers.
BDD_Info	f_bdd_info
	A class that gives information about the structure of BDDs.

Detailed Description

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 25 of file bdd2dot.h.

Member Function Documentation

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 46 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 90 of file bdd2dot.h.

Member Data Documentation

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 38 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 32 of file bdd2dot.h.

f_node_number

int mcrl2::data::detail::BDD2Dot::f_node_number = 0

private

The smallest unused node number.

Definition at line 29 of file bdd2dot.h.

f_visited

std::map< atermpp::aterm, atermpp::aterm_int> mcrl2::data::detail::BDD2Dot::f_visited

private

A table containing all the visited nodes. It maps these nodes to the corresponding node numbers.

Definition at line 35 of file bdd2dot.h.

---

The documentation for this class was generated from the following file:

• data/include/mcrl2/data/detail/prover/bdd2dot.h