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

Generated by: LCOV version 1.12