Line data Source code
1 : // Author(s): Luc Engelen 2 : // Copyright: see the accompanying file COPYING or copy at 3 : // https://github.com/mCRL2org/mCRL2/blob/master/COPYING 4 : // 5 : // Distributed under the Boost Software License, Version 1.0. 6 : // (See accompanying file LICENSE_1_0.txt or copy at 7 : // http://www.boost.org/LICENSE_1_0.txt) 8 : // 9 : /// \file mcrl2/utilities/bdd2dot.h 10 : /// \brief Interface to class BDD2Dot 11 : 12 : #ifndef MCRL2_DATA_DETAIL_PROVER_BDD2DOT_H 13 : #define MCRL2_DATA_DETAIL_PROVER_BDD2DOT_H 14 : 15 : #include "mcrl2/data/detail/prover/bdd_info.h" 16 : #include <fstream> 17 : 18 : namespace mcrl2 19 : { 20 : namespace data 21 : { 22 : namespace detail 23 : { 24 : 25 : /// \brief The class BDD2Dot offers the ability to write binary decision diagrams to dot files. 26 : /// The method BDD2Dot::output_bdd receives a binary decision diagram as parameter a_bdd and writes it to a file in dot 27 : /// format with the name passed as parameter a_file_name. 28 : 29 : class BDD2Dot 30 : { 31 : private: 32 : /// \brief The smallest unused node number. 33 : int f_node_number; 34 : 35 : /// \brief The file the output is written to. 36 : std::ofstream f_dot_file; 37 : 38 : /// \brief A table containing all the visited nodes. It maps these nodes to the corresponding node numbers. 39 : std::map < atermpp::aterm_appl, atermpp::aterm_int> f_visited; 40 : 41 : /// \brief A class that gives information about the structure of BDDs. 42 : BDD_Info f_bdd_info; 43 : 44 : /// \brief Writes the BDD it receives to BDD2Dot::f_dot_file. 45 : /// \param a_bdd A binary decision diagram. 46 : /// \pre The argument passed as parameter a_bdd is a data expression in internal mCRL2 format with the 47 : /// following restrictions: It either represents the constant true or the constant false, or it is an if-then-else 48 : /// expression with an expression of Bool as guard, and a then-branch and an else-branch that again follow these 49 : /// restrictions 50 0 : void aux_output_bdd(const data_expression &a_bdd) 51 : { 52 0 : if (f_visited.count(a_bdd)>0) // a_bdd has already been visited. 53 : { 54 0 : return; 55 : } 56 : 57 0 : if (f_bdd_info.is_true(a_bdd)) 58 : { 59 0 : f_dot_file << " " << f_node_number << " [shape=box, label=\"T\"];" << std::endl; 60 : } 61 0 : else if (f_bdd_info.is_false(a_bdd)) 62 : { 63 0 : f_dot_file << " " << f_node_number << " [shape=box, label=\"F\"];" << std::endl; 64 : } 65 0 : else if (f_bdd_info.is_if_then_else(a_bdd)) 66 : { 67 0 : const data_expression v_true_branch = f_bdd_info.get_true_branch(a_bdd); 68 0 : const data_expression v_false_branch = f_bdd_info.get_false_branch(a_bdd); 69 0 : aux_output_bdd(v_true_branch); 70 0 : aux_output_bdd(v_false_branch); 71 0 : std::size_t v_true_number = f_visited[v_true_branch].value(); 72 0 : std::size_t v_false_number = f_visited[v_false_branch].value(); 73 0 : const data_expression v_guard = f_bdd_info.get_guard(a_bdd); 74 0 : f_dot_file << " " << f_node_number << " [label=\"" << mcrl2::data::pp(v_guard) << "\"];" << std::endl; 75 0 : f_dot_file << " " << f_node_number << " -> " << v_true_number << ";" << std::endl; 76 0 : f_dot_file << " " << f_node_number << " -> " << v_false_number << " [style=dashed];" << std::endl; 77 0 : } 78 : else 79 : { 80 0 : f_dot_file << " " << f_node_number << " [shape=box, label=\"" << mcrl2::data::pp(a_bdd) << "\"];" << std::endl; 81 : } 82 0 : f_visited[a_bdd]= atermpp::aterm_int(f_node_number++); 83 : } 84 : 85 : public: 86 : /// \brief Writes the BDD it receives as input to a file 87 : /// \brief in dot format with the name received as input. 88 : /// precondition: The argument passed as parameter a_bdd is a data expression in internal mCRL2 format with the 89 : /// following restrictions: It either represents the constant true or the constant false, or it is an if-then-else 90 : /// expression with an expression of Bool as guard, and a then-branch and an else-branch that again follow these 91 : /// restrictions 92 : /// \param a_bdd A binary decision diagram. 93 : /// \param a_file_name A file name. 94 0 : void output_bdd(const data_expression &a_bdd, const std::string& a_file_name) 95 : { 96 0 : f_node_number = 0; 97 0 : f_dot_file.open(a_file_name); 98 0 : f_dot_file << "digraph BDD {" << std::endl; 99 0 : aux_output_bdd(a_bdd); 100 0 : f_dot_file << "}" << std::endl; 101 0 : f_dot_file.close(); 102 0 : } 103 : }; 104 : 105 : } // namespace detail 106 : } // namespace data 107 : } // namespace mcrl2 108 : 109 : #endif