mCRL2
Loading...
Searching...
No Matches
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
 The smallest unused node number.
 
std::ofstream f_dot_file
 The file the output is written to.
 
std::map< atermpp::aterm, atermpp::aterm_intf_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 29 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_bddA 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_bddA binary decision diagram.
a_file_nameA file name.

Definition at line 94 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 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

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


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