Line data    Source code

       1             : // Author(s): Wieger Wesselink
       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/pbes/tools/pbesinfo.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_PBES_TOOLS_PBESINFO_H
      13             : #define MCRL2_PBES_TOOLS_PBESINFO_H
      14             : 
      15             : #include "mcrl2/pbes/detail/pbes_property_map.h"
      16             : #include "mcrl2/pbes/io.h"
      17             : 
      18             : namespace mcrl2 {
      19             : 
      20             : namespace pbes_system {
      21             : 
      22           0 : void pbesinfo(const std::string& input_filename,
      23             :               const std::string& input_file_message,
      24             :               const utilities::file_format& file_format,
      25             :               bool opt_full
      26             :              )
      27             : {
      28           0 :   pbes p;
      29           0 :   load_pbes(p, input_filename, file_format);
      30             : 
      31           0 :   detail::pbes_property_map info(p);
      32             : 
      33             :   // Show file from which PBES was read
      34           0 :   std::cout << input_file_message << "\n\n";
      35             : 
      36             :   // Show number of equations
      37           0 :   std::cout << "Number of equations:     " << p.equations().size() << std::endl;
      38             : 
      39             :   // Show number of mu's with the predicate variables from the mu's
      40           0 :   std::cout << "Number of mu's:          " << info["mu_equation_count"] << std::endl;
      41             : 
      42             :   // Show number of nu's with the predicate variables from the nu's
      43           0 :   std::cout << "Number of nu's:          " << info["nu_equation_count"] << std::endl;
      44             : 
      45             :   // Show number of nu's with the predicate variables from the nu's
      46           0 :   std::cout << "Block nesting depth:     " << info["block_nesting_depth"] << std::endl;
      47             : 
      48             :   // Show if PBES is closed and well formed
      49           0 :   std::cout << "The PBES is closed:      " << std::flush;
      50           0 :   std::cout << (p.is_closed() ? "yes" : "no ") << std::endl;
      51           0 :   std::cout << "The PBES is well formed: " << std::flush;
      52           0 :   std::cout << (p.is_well_typed() ? "yes" : "no ") << std::endl;
      53             : 
      54             :   // Show binding variables with their signature
      55           0 :   if (opt_full)
      56             :   {
      57           0 :     std::cout << "Predicate variables:\n";
      58           0 :     for (std::vector<pbes_equation>::const_iterator i = p.equations().begin(); i != p.equations().end(); ++i)
      59             :     {
      60           0 :       std::cout << core::pp(i->symbol()) << "." << pp(i->variable()) << std::endl;
      61             :     }
      62             :   }
      63           0 : }
      64             : 
      65             : } // namespace pbes_system
      66             : 
      67             : } // namespace mcrl2
      68             : 
      69             : #endif // MCRL2_PBES_TOOLS_PBESINFO_H