Line data    Source code

       1             : // Author(s): Muck van Weerdenburg
       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 liblts_dot.cpp
      10             : 
      11             : #include "mcrl2/lts/lts_io.h"
      12             : #include "mcrl2/lts/parse.h"
      13             : #include "mcrl2/lts/detail/liblts_swap_to_from_probabilistic_lts.h"
      14             : 
      15             : using namespace mcrl2::core;
      16             : 
      17             : namespace mcrl2
      18             : {
      19             : namespace lts
      20             : {
      21             : 
      22           0 : void probabilistic_lts_dot_t::save(std::ostream& os) const
      23             : {
      24             :   // Language definition seems to suggest that the name is optional, but tools seem to think otherwise
      25           0 :   os << "digraph G {" << std::endl;
      26             :   // os << "size=\"7,10.5\";" << std::endl;
      27           0 :   os << "center = TRUE;" << std::endl;
      28           0 :   os << "mclimit = 10.0;" << std::endl;
      29           0 :   os << "nodesep = 0.05;" << std::endl;
      30           0 :   os << "node [ width=0.25, height=0.25, label=\"\" ];" << std::endl;
      31           0 :   if (num_states() > 0)
      32             :   {
      33           0 :     if (initial_probabilistic_state().size()<=1)
      34             :     { 
      35           0 :       const std::size_t initial_state=initial_probabilistic_state().get();
      36           0 :       if (has_state_info())
      37             :       {
      38           0 :         os << state_label(initial_state).name();
      39             :       }
      40             :       else
      41             :       {
      42           0 :         os << "S" << initial_state;
      43             :       }
      44             :     }
      45             :     else
      46             :     {
      47           0 :       throw mcrl2::runtime_error("Cannnot save a probabilistic transition system in .dot format.");
      48             :     }
      49             : 
      50           0 :     os << " [ peripheries=2 ];" << std::endl;
      51           0 :     for (std::size_t i=0; i<num_states(); i++)
      52             :     {
      53           0 :       if (has_state_info())
      54             :       {
      55           0 :         const std::string& label = state_label(i).label();
      56           0 :         if (!label.empty())
      57             :         {
      58           0 :           os << state_label(i).name() << " [label=\"" << label << "\"];" << std::endl;
      59             :         }
      60           0 :       }
      61             :       else
      62             :       {
      63           0 :         os << "S" << i << std::endl;
      64             :       }
      65             :     }
      66             :   }
      67             :   
      68           0 :   for (const transition& t: get_transitions())
      69             :   {
      70           0 :     if (has_state_info())
      71             :     {
      72           0 :       if (probabilistic_state(t.to()).size()>1)
      73             :       {
      74           0 :         throw mcrl2::runtime_error("Cannot save probabilistic states in .dot format.");
      75             :       }
      76           0 :       os << state_label(t.from()).name() << "->" << state_label(probabilistic_state(t.to()).get()).name() << "[label=\"" <<
      77           0 :          mcrl2::lts::pp(action_label(t.label())) << "\"];" << std::endl;
      78             :     }
      79             :     else
      80             :     {
      81           0 :       os << "S" << t.from() << " -> " << "S" << t.to() << "[label=\"" <<
      82           0 :          mcrl2::lts::pp(action_label(apply_hidden_label_map(t.label()))) << "\"];" << std::endl;
      83             :     }
      84             :   }
      85             : 
      86           0 :   os << "}" << std::endl;
      87           0 : }
      88             : 
      89           0 : void probabilistic_lts_dot_t::save(const std::string& filename) const
      90             : {
      91           0 :   std::ofstream os(filename.c_str());
      92           0 :   if (!os.is_open())
      93             :   {
      94           0 :     throw mcrl2::runtime_error("cannot open DOT file '" + filename + "' for writing.");
      95             :   }
      96           0 :   save(os);
      97           0 :   os.close();
      98           0 : }
      99             : 
     100           0 : void lts_dot_t::save(std::ostream& os) const
     101             : {
     102           0 :   probabilistic_lts_dot_t l;
     103             :   detail::translate_to_probabilistic_lts
     104             :             <state_label_dot,
     105             :              action_label_string,
     106             :              probabilistic_state<std::size_t, mcrl2::lts::probabilistic_arbitrary_precision_fraction>,
     107           0 :              detail::lts_dot_base>(*this,l);
     108           0 :   l.save(os);
     109           0 : }
     110             : 
     111           0 : void lts_dot_t::save(const std::string& filename) const
     112             : {
     113           0 :   if (filename.empty() || filename=="-")
     114             :   {
     115           0 :     save(std::cout);
     116             :   }
     117             :   else
     118             :   {
     119           0 :     std::ofstream os(filename.c_str());
     120           0 :     if (!os.is_open())
     121             :     {
     122           0 :       throw mcrl2::runtime_error("cannot open DOT file '" + filename + "' for writing.");
     123             :     }
     124           0 :     save(os);
     125           0 :     os.close();
     126           0 :   }
     127           0 : }
     128             : 
     129             : }
     130             : }