bdd2dot.h

Go to the documentation of this file.

// Author(s): Luc Engelen
// Copyright: see the accompanying file COPYING or copy at
// https://github.com/mCRL2org/mCRL2/blob/master/COPYING
//
// Distributed under the Boost Software License, Version 1.0.
// (See accompanying file LICENSE_1_0.txt or copy at
// http://www.boost.org/LICENSE_1_0.txt)
//
 
#ifndef MCRL2_DATA_DETAIL_PROVER_BDD2DOT_H
#define MCRL2_DATA_DETAIL_PROVER_BDD2DOT_H
 
#include "mcrl2/data/detail/prover/bdd_info.h"
#include <fstream>
 
namespace mcrl2
{
namespace data
{
namespace detail
{
 
 
class BDD2Dot
{
  private:
    int f_node_number;
 
    std::ofstream f_dot_file;
 
    std::map < atermpp::aterm, atermpp::aterm_int> f_visited;
 
    BDD_Info f_bdd_info;
 
    void aux_output_bdd(const data_expression &a_bdd)
    {
      if (f_visited.count(a_bdd)>0)  // a_bdd has already been visited.
      {
        return;
      }
 
      if (f_bdd_info.is_true(a_bdd))
      {
        f_dot_file << "  " << f_node_number << " [shape=box, label=\"T\"];" << std::endl;
      }
      else if (f_bdd_info.is_false(a_bdd))
      {
        f_dot_file << "  " << f_node_number << " [shape=box, label=\"F\"];" << std::endl;
      }
      else if (f_bdd_info.is_if_then_else(a_bdd))
      {
        const data_expression v_true_branch = f_bdd_info.get_true_branch(a_bdd);
        const data_expression v_false_branch = f_bdd_info.get_false_branch(a_bdd);
        aux_output_bdd(v_true_branch);
        aux_output_bdd(v_false_branch);
        std::size_t v_true_number = f_visited[v_true_branch].value();
        std::size_t v_false_number = f_visited[v_false_branch].value();
        const data_expression v_guard = f_bdd_info.get_guard(a_bdd);
        f_dot_file << "  " << f_node_number << " [label=\"" << mcrl2::data::pp(v_guard) << "\"];" << std::endl;
        f_dot_file << "  " << f_node_number << " -> " << v_true_number << ";" << std::endl;
        f_dot_file << "  " << f_node_number << " -> " << v_false_number << " [style=dashed];" << std::endl;
      }
      else
      {
        f_dot_file << "  " << f_node_number << " [shape=box, label=\"" << mcrl2::data::pp(a_bdd) << "\"];" << std::endl;
      }
      f_visited[a_bdd]= atermpp::aterm_int(f_node_number++);
    }
 
  public:
    void output_bdd(const data_expression &a_bdd, const std::string& a_file_name)
    {
      f_node_number = 0;
      f_dot_file.open(a_file_name);
      f_dot_file << "digraph BDD {" << std::endl;
      aux_output_bdd(a_bdd);
      f_dot_file << "}" << std::endl;
      f_dot_file.close();
    }
};
 
} // namespace detail
} // namespace data
} // namespace mcrl2
 
#endif