LCOV - code coverage report
Current view: top level - bes/include/mcrl2/bes - pg_parse.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 80 84 95.2 %
Date: 2020-10-20 00:45:57 Functions: 20 20 100.0 %
Legend: Lines: hit not hit

          Line data    Source code
       1             : // Author(s): Jeroen Keiren, 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/bes/pg_parse.h
      10             : /// \brief Parsing of parity games in the format used by PGSolver.
      11             : 
      12             : #ifndef MCRL2_BES_PG_PARSE_H
      13             : #define MCRL2_BES_PG_PARSE_H
      14             : 
      15             : #include <fstream>
      16             : 
      17             : #include "mcrl2/bes/boolean_equation_system.h"
      18             : #include "mcrl2/bes/join.h"
      19             : #include "mcrl2/core/parser_utility.h"
      20             : 
      21             : extern "C"
      22             : {
      23             :   extern D_ParserTables parser_tables_pg;
      24             : }
      25             : 
      26             : namespace mcrl2
      27             : {
      28             : 
      29             : namespace bes
      30             : {
      31             : 
      32             : typedef unsigned long long identifier_t;
      33             : typedef unsigned short priority_t;
      34             : 
      35             : typedef bool owner_t;
      36             : 
      37         640 : struct node_t
      38             : {
      39             :   identifier_t id;
      40             :   priority_t prio;
      41             :   owner_t owner;
      42             :   std::set<identifier_t> successors;
      43             : 
      44             :   bool operator<(node_t const& other)
      45             :   {
      46             :     return id < other.id;
      47             :   }
      48             : };
      49             : 
      50             : // Build a formula from the strings in v. if p = 0, than a disjunction is built,
      51             : // otherwise the result is a conjunction.
      52             : // Prefix is added to each of the identifiers in v.
      53             : inline
      54         128 : boolean_expression formula(std::set<identifier_t> const& v, const owner_t owner, const std::string& prefix = "X")
      55             : {
      56         256 :   std::set<boolean_expression> v_prefixed;
      57         352 :   for (identifier_t i: v)
      58             :   {
      59         448 :     std::stringstream id;
      60         224 :     id << prefix << i;
      61         224 :     v_prefixed.insert(boolean_variable(id.str()));
      62             :   }
      63             : 
      64         128 :   if (owner == 0)
      65             :   {
      66          40 :     return join_or(v_prefixed.begin(), v_prefixed.end());
      67             :   }
      68             :   else
      69             :   {
      70          88 :     return join_and(v_prefixed.begin(), v_prefixed.end());
      71             :   }
      72             : }
      73             : 
      74           4 : struct pg_actions: public core::default_parser_actions
      75             : {
      76             :   // Parse node specifications (store in map)
      77             :   std::map<identifier_t, node_t> game;
      78             :   identifier_t initial_node;
      79             : 
      80           4 :   pg_actions(const core::parser& parser_)
      81           4 :     : core::default_parser_actions(parser_),
      82           4 :       initial_node((std::numeric_limits<identifier_t>::max)())
      83           4 :   {}
      84             : 
      85             :   template <typename T, typename Function>
      86             :   std::set<T> parse_set(const core::parse_node& node, const std::string& type, Function f)
      87             :   {
      88             :     std::set<T> result;
      89             :     traverse(node, make_set_collector(m_parser, type, result, f));
      90             :     return result;
      91             :   }
      92             : 
      93           4 :   void create_boolean_equation_system(boolean_equation_system& b, bool maxpg)
      94             :   {
      95             :     // Build Boolean equation system. First we group equations by block
      96           8 :     std::map<priority_t, std::set<boolean_equation> > blocks;
      97             :     // Translation scheme:
      98             :     // prefix every id with X. Owner 0 means ||, owner 1 means &&
      99             : 
     100         132 :     for (std::map<identifier_t, node_t>::const_iterator i = game.begin(); i != game.end(); ++i)
     101             :     {
     102         256 :       std::stringstream id;
     103         128 :       id << "X" << i->second.id;
     104             : 
     105         256 :       fixpoint_symbol fp(fixpoint_symbol::mu());
     106         128 :       if (i->second.prio % 2 == 0)
     107             :       {
     108          64 :         fp = fixpoint_symbol::nu();
     109             :       }
     110             : 
     111         256 :       boolean_equation eqn(fp, boolean_variable(id.str()), formula(i->second.successors, i->second.owner));
     112             : 
     113         128 :       blocks[i->second.prio].insert(eqn);
     114             :     }
     115             : 
     116           8 :     std::vector<boolean_equation> eqns;
     117           4 :     if(maxpg)
     118             :     {
     119          16 :       for (std::map<priority_t, std::set<boolean_equation> >::reverse_iterator i = blocks.rbegin(); i != blocks.rend(); ++i)
     120             :       {
     121          12 :         eqns.insert(eqns.end(), i->second.begin(), i->second.end());
     122             :       }
     123             :     }
     124             :     else
     125             :     {
     126           0 :       for (std::map<priority_t, std::set<boolean_equation> >::const_iterator i = blocks.begin(); i != blocks.end(); ++i)
     127             :       {
     128           0 :         eqns.insert(eqns.end(), i->second.begin(), i->second.end());
     129             :       }
     130             :     }
     131             : 
     132           4 :     b.equations() = eqns;
     133           8 :     std::stringstream init_id;
     134           4 :     init_id << initial_node;
     135           4 :     b.initial_state() = boolean_variable("X" + init_id.str());
     136           4 :   }
     137             : 
     138           4 :   void parse_ParityGame(const core::parse_node& node, boolean_equation_system& result, bool maxpg)
     139             :   {
     140           4 :     if(node.child_count() == 5)
     141             :     {
     142             : 
     143           0 :       initial_node = parse_Id(node.child(3));
     144             :     }
     145           4 :     if(node.child_count() == 3 && node.child(0).string() == "start")
     146             :     {
     147           0 :       initial_node = parse_Id(node.child(1));
     148             :     }
     149             : 
     150           4 :     game.clear();
     151           4 :     parse_NodeSpecList(node.child(node.child_count()-1));
     152           4 :     create_boolean_equation_system(result, maxpg);
     153           4 :   }
     154             : 
     155         128 :   void parse_NodeSpec(const core::parse_node& node)
     156             :   {
     157         256 :     node_t result;
     158         128 :     result.id = parse_Id(node.child(0));
     159         128 :     result.prio = parse_Priority(node.child(1));
     160         128 :     result.owner = parse_Owner(node.child(2));
     161         128 :     result.successors = parse_Successors(node.child(3));
     162         128 :     if (game.empty() && initial_node == (std::numeric_limits<identifier_t>::max)())
     163             :     {
     164           4 :       initial_node = result.id;
     165             :     }
     166         128 :     game[result.id] = result;
     167         128 :   }
     168             : 
     169           4 :   void parse_NodeSpecList(const core::parse_node& node)
     170             :   {
     171         132 :     traverse(node, make_visitor(m_parser.symbol_table(), "NodeSpec", [&](const core::parse_node& node) { return parse_NodeSpec(node); }));
     172           4 :   }
     173             : 
     174         352 :   identifier_t parse_Id(const core::parse_node& node)
     175             :   {
     176         352 :     return parse_Number<identifier_t>(node.child(0));
     177             :   }
     178             : 
     179         128 :   priority_t parse_Priority(const core::parse_node& node)
     180             :   {
     181         128 :     return parse_Number<priority_t>(node.child(0));
     182             :   }
     183             : 
     184         128 :   bool parse_Owner(const core::parse_node& node)
     185             :   {
     186         128 :     return node.string() == "1";
     187             :   }
     188             : 
     189         128 :   std::set<identifier_t> parse_Successors(const core::parse_node& node)
     190             :   {
     191         128 :     std::set<identifier_t> result;
     192         352 :     traverse(node, make_set_collector(m_parser.symbol_table(), "Id", result, [&](const core::parse_node& node) { return parse_Id(node); }));
     193         128 :     return result;
     194             :   }
     195             : 
     196             :   template <typename T>
     197         480 :   T parse_Number(const core::parse_node& node)
     198             :   {
     199             :     T result;
     200         960 :     std::stringstream tmp;
     201         480 :     tmp << node.string();
     202         480 :     tmp >> result;
     203         960 :     return result;
     204             :   }
     205             : };
     206             : 
     207             : /// \brief Reads a parity game from an input stream, and stores it as a BES.
     208             : /// \param text A string
     209             : /// \param result A boolean equation system
     210             : /// \param maxpg If true a max-parity game is generated in \a result, otherwise a min-parity
     211             : ///        game is obtained.
     212             : inline
     213           4 : void parse_pgsolver_string(const std::string& text, boolean_equation_system& result, bool maxpg = true)
     214             : {
     215           8 :   core::parser p(parser_tables_pg);
     216           4 :   unsigned int start_symbol_index = p.start_symbol_index("ParityGame");
     217           4 :   bool partial_parses = false;
     218           8 :   core::parse_node node = p.parse(text, start_symbol_index, partial_parses);
     219           4 :   pg_actions(p).parse_ParityGame(node, result, maxpg);
     220           4 : }
     221             : 
     222             : /// \brief Reads a parity game from an input stream, and stores it as a BES.
     223             : /// \param from An input stream
     224             : /// \param result A boolean equation system
     225             : /// \param maxpg If true a max-parity game is generated in \a result, otherwise a min-parity
     226             : ///        game is obtained.
     227             : inline
     228           4 : void parse_pgsolver(std::istream& from, boolean_equation_system& result, bool maxpg = true)
     229             : {
     230           8 :   std::string text = utilities::read_text(from);
     231           4 :   parse_pgsolver_string(text, result, maxpg);
     232           4 : }
     233             : 
     234             : /// \brief Parse parity game in PGSolver format from filename, and store the
     235             : ///        resulting BES in b.
     236             : inline void parse_pgsolver(const std::string& filename, boolean_equation_system& b, bool maxpg = true)
     237             : {
     238             :   if(filename == "-" || filename.empty())
     239             :   {
     240             :     parse_pgsolver(std::cin, b, maxpg);
     241             :   }
     242             :   else
     243             :   {
     244             :     std::ifstream f;
     245             :     f.open(filename.c_str());
     246             :     if(!f)
     247             :     {
     248             :       throw mcrl2::runtime_error("cannot open file " + filename + " for reading");
     249             :     }
     250             :     parse_pgsolver(f, b, maxpg);
     251             :   }
     252             : }
     253             : 
     254             : } // namespace bes
     255             : 
     256             : } // namespace mcrl2
     257             : 
     258             : #endif // MCRL2_BES_PG_PARSE_H

Generated by: LCOV version 1.13