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