LCOV - code coverage report
Current view: top level - bes/source - pgsolver.cpp (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 56 71 78.9 %
Date: 2019-06-26 00:32:26 Functions: 6 6 100.0 %
Legend: Lines: hit not hit

          Line data    Source code
       1             : // Author(s): Sjoerd Cranen
       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 pgsolver.cpp
      10             : /// \brief Add your file description here.
      11             : 
      12             : #include "mcrl2/bes/io.h"
      13             : #include "mcrl2/bes/normal_forms.h"
      14             : 
      15             : namespace mcrl2
      16             : {
      17             : 
      18             : namespace bes
      19             : {
      20             : 
      21             : typedef std::map<core::identifier_string, std::size_t> variable_map;
      22             : 
      23             : ///
      24             : /// \brief Convert a sequence of Boolean variables to PGSolver format.
      25             : ///
      26             : template <typename Iter>
      27           2 : std::string boolean_variables2pgsolver(Iter first, Iter last, const variable_map& variables)
      28             : {
      29           4 :   std::set<std::size_t> variables_int;
      30           6 :   for (Iter i = first; i != last; ++i)
      31             :   {
      32           4 :     const boolean_variable& b = atermpp::down_cast<boolean_variable>(*i);
      33           4 :     variable_map::const_iterator j = variables.find(b.name());
      34           4 :     if (j == variables.end())
      35             :     {
      36           0 :       throw mcrl2::runtime_error("Found undeclared variable in boolean_variables2pgsolver: " + bes::pp(b));
      37             :     }
      38           4 :     variables_int.insert(j->second);
      39             :   }
      40           4 :   return utilities::string_join(variables_int, ", ");
      41             : }
      42             : 
      43             : ///
      44             : /// \brief Convert a BES expression to PGSolver format.
      45             : ///
      46           2 : static std::string bes_expression2pgsolver(const boolean_expression& p, const variable_map& variables)
      47             : {
      48           2 :   std::string result;
      49           2 :   if (is_and(p))
      50             :   {
      51           2 :     std::set<boolean_expression> expressions = split_and(p);
      52           1 :     result = boolean_variables2pgsolver(expressions.begin(), expressions.end(), variables);
      53             :   }
      54           1 :   else if (is_or(p))
      55             :   {
      56           2 :     std::set<boolean_expression> expressions = split_or(p);
      57           1 :     result = boolean_variables2pgsolver(expressions.begin(), expressions.end(), variables);
      58             :   }
      59           0 :   else if (is_boolean_variable(p))
      60             :   {
      61           0 :     const boolean_variable& b = atermpp::down_cast<boolean_variable>(p);
      62           0 :     variable_map::const_iterator i = variables.find(b.name());
      63           0 :     if (i == variables.end())
      64             :     {
      65           0 :       throw mcrl2::runtime_error("Found undeclared variable in bes_expression2cwi: " + bes::pp(p));
      66             :     }
      67           0 :     std::stringstream out;
      68           0 :     out << i->second;
      69           0 :     result = out.str();
      70             :   }
      71             :   else
      72             :   {
      73           0 :     throw mcrl2::runtime_error("Unknown or unsupported expression encountered in bes_expression2cwi: " + bes::pp(p));
      74             :   }
      75           2 :   return result;
      76             : }
      77             : 
      78             : ///
      79             : /// \brief Save a sequence of BES equations in to a stream in PGSolver format.
      80             : ///
      81             : template <typename Iter>
      82           1 : void bes2pgsolver(Iter first, Iter last, std::ostream& out, bool maxpg)
      83             : {
      84             :   // Number the variables of the equations 0, 1, ... and put them in the map variables.
      85             :   // Also store player to which variables without operand are assigned, per
      86             :   // block, in block_to_player.
      87           2 :   variable_map variables;
      88           1 :   std::size_t index = 0;
      89           2 :   std::map<int, int> block_to_player;
      90             : 
      91           1 :   bool and_in_block = false;
      92           1 :   int block = 0;
      93           2 :   fixpoint_symbol sigma = fixpoint_symbol::nu();
      94           3 :   for (Iter i = first; i != last; ++i)
      95             :   {
      96           2 :     if(i->symbol() != sigma)
      97             :     {
      98           1 :       block_to_player[block++] = (and_in_block)?1:0;
      99           1 :       and_in_block = false;
     100           1 :       sigma = i->symbol();
     101             :     }
     102           2 :     variables[i->variable().name()] = index++;
     103           2 :     and_in_block = and_in_block || is_and(i->formula());
     104             :   }
     105           1 :   block_to_player[block] = (and_in_block)?1:0;
     106             : 
     107           1 :   if(maxpg && block % 2 == 1)
     108             :   {
     109           1 :     ++block;
     110             :   }
     111             : 
     112           1 :   out << "parity " << index -1 << ";\n";
     113             : 
     114           1 :   int priority = 0;
     115           1 :   sigma = fixpoint_symbol::nu();
     116           3 :   for (Iter i = first; i != last; ++i)
     117             :   {
     118           2 :     if(i->symbol() != sigma)
     119             :     {
     120           1 :       ++priority;
     121           1 :       sigma = i->symbol();
     122             :     }
     123             : 
     124           4 :     out << variables[i->variable().name()]
     125           2 :         << " "
     126           4 :         << (maxpg?(block-priority):priority)
     127           2 :         << " "
     128           4 :         << (is_and(i->formula()) ? 1 : (is_or(i->formula())?0:block_to_player[priority]))
     129           2 :         << " "
     130           6 :         << bes_expression2pgsolver(i->formula(), variables)
     131             : #ifdef MCRL2_BES2PGSOLVER_PRINT_VARIABLE_NAMES
     132             :         << " "
     133             :         << "\""
     134             :         << bes::pp(i->variable())
     135             :         << "\""
     136             : #endif
     137             :       << ";\n";
     138             :   }
     139           1 : }
     140             : 
     141           1 : void save_bes_pgsolver(const boolean_equation_system& bes, std::ostream& stream, bool maxpg)
     142             : {
     143           2 :   boolean_equation_system bes_standard_form(bes);
     144           1 :   make_standard_form(bes_standard_form, true);
     145           1 :   if(bes.initial_state() != bes.equations().front().variable())
     146             :   {
     147           0 :     std::stringstream ss;
     148           0 :     ss << "The initial state " << bes_standard_form.initial_state() << " and the left hand side "
     149           0 :           "of the first equation (" << bes_standard_form.equations().front().variable() << ") do "
     150           0 :           "not correspond. Cannot save BES to PGSolver format.";
     151           0 :     throw mcrl2::runtime_error(ss.str());
     152             :   }
     153           1 :   bes2pgsolver(bes_standard_form.equations().begin(), bes_standard_form.equations().end(), stream, maxpg);
     154           1 : }
     155             : 
     156             : } // namespace bes
     157             : 
     158          21 : } // namespace mcrl2

Generated by: LCOV version 1.12