LCOV - code coverage report
Current view: top level - pg/source - ParityGame_IO.cpp (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 0 158 0.0 %
Date: 2024-03-08 02:52:28 Functions: 0 8 0.0 %
Legend: Lines: hit not hit

          Line data    Source code
       1             : // Copyright (c) 2009-2013 University of Twente
       2             : // Copyright (c) 2009-2013 Michael Weber <michaelw@cs.utwente.nl>
       3             : // Copyright (c) 2009-2013 Maks Verver <maksverver@geocities.com>
       4             : // Copyright (c) 2009-2013 Eindhoven University of Technology
       5             : //
       6             : // Distributed under the Boost Software License, Version 1.0.
       7             : // (See accompanying file LICENSE_1_0.txt or copy at
       8             : // http://www.boost.org/LICENSE_1_0.txt)
       9             : 
      10             : #include "mcrl2/pbes/io.h"
      11             : #include "mcrl2/pbes/parity_game_generator.h"
      12             : #include "mcrl2/pg/ParityGame.h"
      13             : 
      14             : /* N.B. The PGSolver I/O functions reverse the priorities when reading/writing
      15             :    the game description. This is done to preserve solutions, since PGSolver
      16             :    considers higher values to dominate lower values, while I assume the opposite
      17             :    (i.e. 0 is the `highest` priority) throughout the rest of the code. */
      18             : 
      19           0 : void ParityGame::read_pgsolver( std::istream &is,
      20             :                                 StaticGraph::EdgeDirection edge_dir )
      21             : {
      22           0 :     priority_t max_prio = 0;
      23           0 :     std::vector<ParityGameVertex> vertices;
      24           0 :     StaticGraph::edge_list edges;
      25             : 
      26             :     // Read "parity" header line (if present)
      27           0 :     char ch = 0;
      28           0 :     while (!isalnum(ch)) is.get(ch);
      29           0 :     is.putback(ch);
      30           0 :     if (!isdigit(ch))
      31             :     {
      32           0 :         std::string parity;
      33             :         verti max_vertex;
      34             : 
      35           0 :         if (!(is >> parity >> max_vertex)) return;
      36           0 :         if (parity != "parity") return;
      37           0 :         vertices.reserve(max_vertex + 1);
      38             : 
      39             :         // Skip to terminating semicolon
      40           0 :         while (is.get(ch) && ch != ';') ch = 0;
      41           0 :     }
      42             : 
      43             :     // Read and discard "start" line (if present)
      44           0 :     while (!isalnum(ch)) is.get(ch);
      45           0 :     is.putback(ch);
      46           0 :     if (!isdigit(ch))
      47             :     {
      48           0 :         std::string start;
      49             :         verti vertex;
      50             : 
      51           0 :         if (!(is >> start >> vertex)) return;
      52           0 :         if (start != "start") return;
      53             : 
      54             :         // Skip to terminating semicolon
      55           0 :         while (is.get(ch) && ch != ';') ch = 0;
      56           0 :     }
      57             : 
      58             :     // Invalid vertex (used to mark uninitialized vertices)
      59           0 :     ParityGameVertex invalid = { PLAYER_EVEN, (priority_t)-1 };
      60             : 
      61             :     // Read vertex specs
      62           0 :     while (is)
      63             :     {
      64             :         verti id;
      65             :         int prio_raw, player_raw;
      66             : 
      67           0 :         if (!(is >> id >> prio_raw >> player_raw)) break;
      68             : 
      69           0 :         assert(prio_raw >= 0);
      70           0 :         assert(prio_raw < 65536);
      71           0 :         priority_t prio = prio_raw;
      72             : 
      73           0 :         assert(player_raw == 0 || player_raw == 1);
      74           0 :         player_t player = static_cast<player_t>(player_raw);
      75             : 
      76           0 :         if (prio > max_prio) max_prio = prio;
      77           0 :         if (id >= vertices.size()) vertices.resize(id + 1, invalid);
      78             : 
      79             :         /* FIXME: the PGSolver file format description allows vertices to be
      80             :                   defined more than once (in that case, the old vertex should
      81             :                   be removed), but we currently don't support that. Instead,
      82             :                   just assert that each vertex is initialized once. */
      83           0 :         assert(vertices[id] == invalid);
      84             : 
      85           0 :         vertices[id].player   = player;
      86           0 :         vertices[id].priority = prio;
      87             : 
      88             :         // Read successors
      89             :         do {
      90             :             verti succ;
      91           0 :             if (!(is >> succ)) break;
      92           0 :             if (succ >= vertices.size()) vertices.resize(succ + 1, invalid);
      93             : 
      94           0 :             edges.push_back(std::make_pair(id, succ));
      95             : 
      96             :             // Skip to separator (comma) or end-of-list (semicolon), while
      97             :             // ignoring the contents of quoted strings.
      98           0 :             bool quoted = false, escaped = false;
      99           0 :             while (is.get(ch)) {
     100           0 :                 if (ch == '"' && !escaped) quoted = !quoted;
     101           0 :                 escaped = ch == '\\' && !escaped;
     102           0 :                 if ((ch == ',' || ch == ';') && !quoted) break;
     103             :             }
     104             : 
     105           0 :         } while (is && ch == ',');
     106             :     }
     107             : 
     108             :     // Ensure max_prio is even, so max_prio - p preserves parity:
     109           0 :     if (max_prio%2 == 1) ++max_prio;
     110             : 
     111             :     // Look for unused vertex indices:
     112           0 :     std::vector<verti> vertex_map(vertices.size(), NO_VERTEX);
     113           0 :     verti used = 0;
     114           0 :     for (verti v = 0; v < (verti)vertices.size(); ++v)
     115             :     {
     116           0 :         if (vertices[v] != invalid) {
     117           0 :             vertices[used] = vertices[v];
     118           0 :             vertex_map[v] = used++;
     119             :         }
     120             :     }
     121           0 :     if (used < (verti)vertices.size())
     122             :     {
     123             :         // Remove unused vertices:
     124           0 :         vertices.erase(vertices.begin() + used, vertices.end());
     125             : 
     126             :         // Remap edges to new vertex indices:
     127           0 :         for ( StaticGraph::edge_list::iterator it = edges.begin();
     128           0 :               it != edges.end(); ++it )
     129             :         {
     130           0 :             it->first  = vertex_map[it->first];
     131           0 :             it->second = vertex_map[it->second];
     132           0 :             assert(it->first != NO_VERTEX && it->second != NO_VERTEX);
     133             :         }
     134             :     }
     135             : 
     136             :     // Assign vertex info and recount cardinalities
     137           0 :     reset((verti)vertices.size(), max_prio + 1);
     138           0 :     for (std::size_t n = 0; n < vertices.size(); ++n)
     139             :     {
     140           0 :         assert(vertices[n] != invalid);
     141           0 :         vertex_[n].player   = vertices[n].player;
     142           0 :         vertex_[n].priority = max_prio - vertices[n].priority;
     143             :     }
     144           0 :     recalculate_cardinalities(vertices.size());
     145           0 :     vertices.clear();
     146             : 
     147             :     // Assign graph
     148           0 :     graph_.assign(edges, edge_dir);
     149           0 : }
     150             : 
     151           0 : void ParityGame::write_pgsolver(std::ostream &os) const
     152             : {
     153             :     // Get max priority and make it even so max_prio - p preserves parity:
     154           0 :     int max_prio = d();
     155           0 :     if (max_prio%2 == 1) --max_prio;
     156             : 
     157             :     // Write out graph
     158           0 :     os << "parity " << (long long)graph_.V() - 1 << ";\n";
     159           0 :     for (verti v = 0; v < graph_.V(); ++v)
     160             :     {
     161           0 :         os << v << ' ' << (max_prio - priority(v)) << ' ' << player(v);
     162           0 :         StaticGraph::const_iterator it  = graph_.succ_begin(v),
     163           0 :                                     end = graph_.succ_end(v);
     164           0 :         assert(it < end);
     165           0 :         os << ' ' << *it++;
     166           0 :         while (it != end) os << ',' << *it++;
     167           0 :         os << ";\n";
     168             :     }
     169           0 : }
     170             : 
     171           0 : void ParityGame::read_pbes( const std::string &file_path, verti *goal_vertex,
     172             :                             StaticGraph::EdgeDirection edge_dir,
     173             :                             const std::string &rewrite_strategy )
     174             : {
     175           0 :     mcrl2::pbes_system::pbes pbes;
     176           0 :     load_pbes(pbes, file_path);
     177           0 :     assign_pbes(pbes, goal_vertex, edge_dir, rewrite_strategy);
     178           0 : }
     179             : 
     180           0 : void ParityGame::assign_pbes(mcrl2::pbes_system::pbes &pbes, verti *goal_vertex,
     181             :                              StaticGraph::EdgeDirection edge_dir,
     182             :                              const std::string &rewrite_strategy)
     183             : {
     184             :     /* NOTE: this code assumes the vertices generated by parity_game_generator
     185             :              are numbered from 2 to num_vertices-1 with no gaps, with 0 and 1
     186             :              representing true and false (respectively) and 2 representing the
     187             :              initial condition. */
     188             : 
     189           0 :     if (goal_vertex) *goal_vertex = 2;
     190             : 
     191             :     // Generate min-priority parity game
     192             :     mcrl2::pbes_system::parity_game_generator pgg( pbes, true, true,
     193           0 :         mcrl2::data::parse_rewrite_strategy(rewrite_strategy) );
     194             : 
     195             :     // Build the edge list
     196           0 :     StaticGraph::edge_list edges;
     197           0 :     verti begin = 0, end = 3;
     198           0 :     for (verti v = begin; v < end; ++v)
     199             :     {
     200           0 :         std::set<std::size_t> deps = pgg.get_dependencies(v);
     201           0 :         for ( std::set<std::size_t>::const_iterator it = deps.begin();
     202           0 :                 it != deps.end(); ++it )
     203             :         {
     204           0 :             verti w = (verti)*it;
     205           0 :             assert(w >= begin);
     206           0 :             if (w >= end) end = w + 1;
     207           0 :             edges.push_back(std::make_pair(v - begin, w - begin));
     208             :         }
     209           0 :     }
     210             : 
     211             :     // Determine maximum prioirity
     212           0 :     int max_prio = 0;
     213           0 :     for (verti v = begin; v < end; ++v)
     214             :     {
     215           0 :         max_prio = std::max(max_prio, (int)pgg.get_priority(v));
     216             :     }
     217             : 
     218             :     // Assign vertex info and recount cardinalities
     219           0 :     reset(end - begin, max_prio + 1);
     220           0 :     for (verti v = begin; v < end; ++v)
     221             :     {
     222           0 :         bool and_op = pgg.get_operation(v) ==
     223           0 :                         mcrl2::pbes_system::parity_game_generator::PGAME_AND;
     224           0 :         vertex_[v - begin].player = and_op ? PLAYER_ODD : PLAYER_EVEN;
     225           0 :         vertex_[v - begin].priority = pgg.get_priority(v);
     226             :     }
     227           0 :     recalculate_cardinalities(end - begin);
     228             : 
     229             :     // Assign graph
     230           0 :     graph_.assign(edges, edge_dir);
     231           0 : }
     232             : 
     233           0 : void ParityGame::read_raw(std::istream &is)
     234             : {
     235           0 :     graph_.read_raw(is);
     236           0 :     assert(is.good());
     237             :     int d;
     238           0 :     is.read((char*)&d, sizeof(d));
     239           0 :     reset(graph_.V(), d);
     240           0 :     is.read((char*)vertex_, sizeof(ParityGameVertex)*graph_.V());
     241           0 :     is.read((char*)cardinality_, sizeof(verti)*d);
     242           0 : }
     243             : 
     244           0 : void ParityGame::write_raw(std::ostream &os) const
     245             : {
     246           0 :     graph_.write_raw(os);
     247           0 :     assert(os.good());
     248           0 :     os.write((const char*)&d_, sizeof(d_));
     249           0 :     os.write((const char*)vertex_, sizeof(ParityGameVertex)*graph_.V());
     250           0 :     os.write((const char*)cardinality_, sizeof(verti)*d_);
     251           0 : }
     252             : 
     253           0 : void ParityGame::write_dot(std::ostream &os) const
     254             : {
     255           0 :     os << "digraph {\n";
     256           0 :     for (verti v = 0; v < graph_.V(); ++v)
     257             :     {
     258           0 :         bool even = player(v) == PLAYER_EVEN;
     259           0 :         os << v << " ["
     260             :            << "shape=" << (even ? "diamond" : "box") << ", "
     261           0 :            << "label=\"" << priority(v) << " (" << v << ")\"]\n";
     262             : 
     263           0 :         if (graph_.edge_dir() & StaticGraph::EDGE_SUCCESSOR)
     264             :         {
     265           0 :             for ( StaticGraph::const_iterator it = graph_.succ_begin(v);
     266           0 :                   it != graph_.succ_end(v); ++it )
     267             :             {
     268           0 :                 os << v << " -> " << *it;
     269             :                 // if (*it < v) os << " [color=red]";
     270           0 :                 os << ";\n";
     271             :             }
     272             :         }
     273             :         else
     274             :         {
     275           0 :             for ( StaticGraph::const_iterator it = graph_.pred_begin(v);
     276           0 :                   it != graph_.pred_end(v); ++it )
     277             :             {
     278           0 :                 os << *it << " -> " << v << ";\n";
     279             :             }
     280             :         }
     281             :     }
     282           0 :     os << "}\n";
     283           0 : }
     284             : 
     285           0 : void ParityGame::write_debug(const Strategy &s, std::ostream &os) const
     286             : {
     287           0 :     for (verti v = 0; v < graph_.V(); ++v)
     288             :     {
     289           0 :         os << v << ' ';
     290             : 
     291             :         // Print controlling player and vertex priority:
     292           0 :         char l = ' ', r = ' ';
     293           0 :         if (player(v) == PLAYER_EVEN) l = '<', r = '>';
     294           0 :         if (player(v) == PLAYER_ODD)  l = '[', r = ']';
     295           0 :         os << l << priority(v) << r;
     296             : 
     297             :         // Print outgoing edges:
     298           0 :         char sep = ' ';
     299           0 :         for (StaticGraph::const_iterator it = graph_.succ_begin(v);
     300           0 :              it != graph_.succ_end(v); ++it)
     301             :         {
     302           0 :             os << sep << *it;
     303           0 :             sep = ',';
     304             :         }
     305             : 
     306             :         // Print strategy (if applicable)
     307           0 :         if (!s.empty() && s.at(v) != NO_VERTEX) os << " -> " << s.at(v);
     308             : 
     309           0 :         os << '\n';
     310             :     }
     311           0 :     os << std::flush;
     312           0 : }

Generated by: LCOV version 1.14