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/pbes/io.h"
      13             : #include "mcrl2/pbes/join.h"
      14             : #include "mcrl2/pbes/normal_forms.h"
      15             : 
      16             : namespace mcrl2
      17             : {
      18             : 
      19             : namespace pbes_system
      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           0 : std::string boolean_variables2pgsolver(Iter first, Iter last, const variable_map& variables)
      29             : {
      30           0 :   std::set<std::size_t> variables_int;
      31           0 :   for (Iter i = first; i != last; ++i)
      32             :   {
      33           0 :     const propositional_variable_instantiation& b = atermpp::down_cast<propositional_variable_instantiation>(*i);
      34           0 :     variable_map::const_iterator j = variables.find(b.name());
      35           0 :     if (j == variables.end())
      36             :     {
      37           0 :       throw mcrl2::runtime_error("Found undeclared variable in boolean_variables2pgsolver: " + pbes_system::pp(b));
      38             :     }
      39           0 :     variables_int.insert(j->second);
      40             :   }
      41           0 :   return utilities::string_join(variables_int, ", ");
      42           0 : }
      43             : 
      44             : ///
      45             : /// \brief Convert a BES expression to PGSolver format.
      46             : ///
      47           0 : static std::string bes_expression2pgsolver(const pbes_expression& p, const variable_map& variables)
      48             : {
      49           0 :   std::string result;
      50           0 :   if (is_and(p))
      51             :   {
      52           0 :     std::set<pbes_expression> expressions = split_and(p);
      53           0 :     result = boolean_variables2pgsolver(expressions.begin(), expressions.end(), variables);
      54           0 :   }
      55           0 :   else if (is_or(p))
      56             :   {
      57           0 :     std::set<pbes_expression> expressions = split_or(p);
      58           0 :     result = boolean_variables2pgsolver(expressions.begin(), expressions.end(), variables);
      59           0 :   }
      60           0 :   else if (is_propositional_variable_instantiation(p))
      61             :   {
      62           0 :     const propositional_variable_instantiation& b = atermpp::down_cast<propositional_variable_instantiation>(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: " + pbes_system::pp(p));
      67             :     }
      68           0 :     std::stringstream out;
      69           0 :     out << i->second;
      70           0 :     result = out.str();
      71           0 :   }
      72             :   else
      73             :   {
      74           0 :     throw mcrl2::runtime_error("Unknown or unsupported expression encountered in bes_expression2cwi: " + pbes_system::pp(p));
      75             :   }
      76           0 :   return result;
      77           0 : }
      78             : 
      79             : ///
      80             : /// \brief Save a sequence of BES equations in to a stream in PGSolver format.
      81             : ///
      82             : template <typename Iter>
      83           0 : 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           0 :   variable_map variables;
      89           0 :   std::size_t index = 0;
      90           0 :   std::map<int, int> block_to_player;
      91             : 
      92           0 :   bool and_in_block = false;
      93           0 :   int block = 0;
      94           0 :   fixpoint_symbol sigma = fixpoint_symbol::nu();
      95           0 :   for (Iter i = first; i != last; ++i)
      96             :   {
      97           0 :     if(i->symbol() != sigma)
      98             :     {
      99           0 :       block_to_player[block++] = (and_in_block)?1:0;
     100           0 :       and_in_block = false;
     101           0 :       sigma = i->symbol();
     102             :     }
     103           0 :     variables[i->variable().name()] = index++;
     104           0 :     and_in_block = and_in_block || is_and(i->formula());
     105             :   }
     106           0 :   block_to_player[block] = (and_in_block)?1:0;
     107             : 
     108           0 :   if(maxpg && block % 2 == 1)
     109             :   {
     110           0 :     ++block;
     111             :   }
     112             : 
     113           0 :   out << "parity " << index -1 << ";\n";
     114             : 
     115           0 :   int priority = 0;
     116           0 :   sigma = fixpoint_symbol::nu();
     117           0 :   for (Iter i = first; i != last; ++i)
     118             :   {
     119           0 :     if(i->symbol() != sigma)
     120             :     {
     121           0 :       ++priority;
     122           0 :       sigma = i->symbol();
     123             :     }
     124             : 
     125           0 :     out << variables[i->variable().name()]
     126           0 :         << " "
     127           0 :         << (maxpg?(block-priority):priority)
     128           0 :         << " "
     129           0 :         << (is_and(i->formula()) ? 1 : (is_or(i->formula())?0:block_to_player[priority]))
     130             :         << " "
     131           0 :         << bes_expression2pgsolver(i->formula(), variables)
     132             : #ifdef MCRL2_BES2PGSOLVER_PRINT_VARIABLE_NAMES
     133             :         << " "
     134             :         << "\""
     135             :         << pbes_systembes::pp(i->variable())
     136             :         << "\""
     137             : #endif
     138           0 :       << ";\n";
     139             :   }
     140           0 : }
     141             : 
     142           0 : void save_bes_pgsolver(const pbes& bes, std::ostream& stream, bool maxpg)
     143             : {
     144           0 :   pbes bes_standard_form(bes);
     145           0 :   make_standard_form(bes_standard_form, true);
     146           0 :   if(bes.initial_state().name() != bes.equations().front().variable().name())
     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           0 :   }
     154           0 :   bes2pgsolver(bes_standard_form.equations().begin(), bes_standard_form.equations().end(), stream, maxpg);
     155           0 : }
     156             : 
     157             : } // namespace pbes_system
     158             : 
     159             : } // namespace mcrl2