LCOV - code coverage report
Current view: top level - pg/include/mcrl2/pg - ParityGame.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 0 18 0.0 %
Date: 2024-03-08 02:52:28 Functions: 0 9 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             : #ifndef MCRL2_PG_PARITY_GAME_H
      11             : #define MCRL2_PG_PARITY_GAME_H
      12             : 
      13             : #include "mcrl2/utilities/exception.h"
      14             : #include "mcrl2/pg/Graph.h"
      15             : 
      16             : // Forward declaration of mcrl2::pbes_system::pbes, which may or may not be
      17             : // defined later depending on whether mCRL2 support is compiled in.
      18             : namespace mcrl2 { namespace pbes_system { class pbes; } }
      19             : 
      20             : #if __GNUC__ >= 3
      21             : #   define ATTR_PACKED  __attribute__((__packed__))
      22             : #else
      23             : #   define ATTR_PACKED
      24             : #endif
      25             : 
      26             : /*! \defgroup ParityGameData
      27             : 
      28             :     Data structures used to represent parity games in memory.
      29             : */
      30             : 
      31             : /*! Type of priorities in the game */
      32             : typedef std::size_t priority_t;
      33             : 
      34             : /*! The two players in a parity game (Even and Odd) */
      35             : enum player_t { PLAYER_EVEN =  0,  //!< Even (0)
      36             :                 PLAYER_ODD  =  1   //!< Odd (1)
      37             :               } ATTR_PACKED;
      38             : 
      39             : inline
      40           0 : player_t opponent(const player_t p)
      41             : {
      42           0 :     switch(p)
      43             :     {
      44           0 :       case PLAYER_EVEN:
      45           0 :         return PLAYER_ODD;
      46           0 :       case PLAYER_ODD:
      47           0 :         return PLAYER_EVEN;
      48           0 :       default:
      49           0 :         throw mcrl2::runtime_error("unknown player");
      50             :     }
      51             : }
      52             : 
      53             : /*! \ingroup ParityGameData
      54             : 
      55             :     Parity Game data associated with each vertex in the game graph.
      56             : 
      57             :     \sa ParityGame::Player
      58             : */
      59             : struct ParityGameVertex
      60             : {
      61             :     //! the vertex owner (i.e. next player to move)
      62             :     player_t   player;
      63             : 
      64             :     //! the priority of the vertex  between 0 and `d` (exclusive).
      65             :     priority_t priority;
      66             : };
      67             : 
      68           0 : inline bool operator== (const ParityGameVertex &a, const ParityGameVertex &b)
      69             : {
      70           0 :     return a.player == b.player && a.priority == b.priority;
      71             : }
      72             : 
      73           0 : inline bool operator!= (const ParityGameVertex &a, const ParityGameVertex &b)
      74             : {
      75           0 :     return a.player != b.player || a.priority != b.priority;
      76             : }
      77             : 
      78             : 
      79             : /*! \ingroup ParityGameData
      80             : 
      81             :     A parity game extends a directed graph by assigning a player
      82             :     (Even or Odd) and an integer priority to every vertex.
      83             :     Priorities are between 0 and `d` (exclusive). */
      84             : class ParityGame
      85             : {
      86             : public:
      87             :     typedef player_t Player;
      88             : 
      89             :     /*! A strategy determines the partitioning of the game's vertices into
      90             :         winning sets for both players and provides a deterministic strategy for
      91             :         the vertices controlled by a player in its winning set.
      92             : 
      93             :         For each vertex v owned by player p:
      94             :         - strategy[v] == NO_VERTEX if vertex v is not in p's winning set
      95             :         - strategy[v] == w if vertex v is in p's winning set, (v,w) is an edge
      96             :           in the game graph, and (v,w) is a winning move for player p. */
      97             :     typedef std::vector<verti> Strategy;
      98             : 
      99             :     /*! Construct an empty parity game */
     100             :     ParityGame();
     101             : 
     102             :     /*! Destroy a parity game */
     103             :     ~ParityGame();
     104             : 
     105             :     /*! Reset to an empty game. */
     106             :     void clear();
     107             : 
     108             :     /*! Reset the game to a copy of `game`. */
     109             :     void assign(const ParityGame &game);
     110             : 
     111             :     /*! Reset the game with the given graph and node attributes. */
     112             :     void assign(const StaticGraph& g, ParityGameVertex* na);
     113             : 
     114             :     /*! Returns whether the game is empty. */
     115           0 :     bool empty() const { return graph().empty(); }
     116             : 
     117             :     /*! Efficiently swaps the contents of this parity game with another one. */
     118             :     void swap(ParityGame &pg);
     119             : 
     120             : 
     121             :     //!\name Generation
     122             :     //!@{
     123             : 
     124             :     /*! Generate a random parity game, with vertices assigned uniformly at
     125             :         random to players, and priority assigned uniformly between 0 and d-1.
     126             : 
     127             :         The generated game is a clustered random game if clustersize > 0, or
     128             :         an unclustered random game otherwise.
     129             : 
     130             :         \param V            number of game vertices
     131             :         \param clustersize  cluster size (or 0 for no clustering)
     132             :         \param outdeg       average outdegree (at least 1)
     133             :         \param edge_dir     part of edges to store
     134             :         \param d            number of priorities (at least 1)
     135             :         \sa void StaticGraph::make_random()
     136             :     */
     137             :     void make_random( verti V, unsigned clustersize, unsigned outdeg,
     138             :                       StaticGraph::EdgeDirection edge_dir, int d );
     139             : 
     140             :     /*! Create a subgame containing only the given vertices from the original
     141             :         game. Vertices are renumbered to be in range [0..num_vertices).
     142             :         Edges going out of the vertex subset specified by `vertices` are
     143             :         removed, so every vertex must have at least one outgoing edge that stays
     144             :         within the vertex subset, or the result is not a valid parity game.
     145             : 
     146             :         \sa make_subgame(const ParityGame &, const verti *, verti, const Strategy &)
     147             :     */
     148             :     template<class ForwardIterator>
     149             :     void make_subgame( const ParityGame &game,
     150             :                        ForwardIterator vertices_begin,
     151             :                        ForwardIterator vertices_end,
     152             :                        bool proper,
     153             :                        StaticGraph::EdgeDirection edge_dir
     154             :                             = StaticGraph::EDGE_NONE );
     155             : 
     156             : #ifdef WITH_THREADS
     157             :     void make_subgame_threads( const ParityGame &game,
     158             :                                const verti *verts,
     159             :                                const verti nvert,
     160             :                                bool proper,
     161             :                                StaticGraph::EdgeDirection edge_dir
     162             :                                     = StaticGraph::EDGE_NONE );
     163             : #endif
     164             : 
     165             :     //!@}
     166             : 
     167             :     //!\name Transformation
     168             :     //!@{
     169             : 
     170             :     /*! Replaces the current game by its dual game, which uses the same game
     171             :         graph, but swaps players and changes priorities, such that the solution
     172             :         to the game is the same except with winners reversed. (A node won by
     173             :         even in the old game, is won by odd in the dual game, and vice versa.)
     174             :     */
     175             :     void make_dual();
     176             : 
     177             :     /*! Shuffles the nodes in the game. Node n becomes node perm[n], for all n.
     178             :         Requires that perm contains a permuation of 0 through graph().V()-1.
     179             : 
     180             :         NOTE: this is the reverse of what is normally understood to be a
     181             :               permutation! i.e. (2 3 1) maps 1->2, 2->3, 3->1 (instead of the
     182             :               usual interpretation of 1->3, 2->1, 3->2) */
     183             :     void shuffle(const std::vector<verti> &perm);
     184             : 
     185             :     /*! Compresses the range of priorities such that after compression,
     186             :         cardinality(p) &gt; 0, for 0 &lt; p &lt; d.
     187             : 
     188             :         If `cardinality` is 0, then the priorities for the game itself are used.
     189             :         Otherwise, `cardinality` must be an array of length `d` and the caller
     190             :         must ensure that all priorities that occur in the game have a positive
     191             :         cardinality count.
     192             : 
     193             :         If `preserve_parity` is true, then remapping preserves the parity of
     194             :         priorities and thus players of vertices. In this case, cardinality(0)
     195             :         may be zero afterwards.
     196             : 
     197             :         If `preserve_parity` is false, then players as well as priorities are
     198             :         remapped to preserve winning sets. The function returns the parity of
     199             :         the priority that was mapped to zero.
     200             :     */
     201             :     void compress_priorities( const verti cardinality[] = 0,
     202             :                               bool preserve_parity = true );
     203             : 
     204             :     /*! Propagate priorities in the graph, by changing the priority for a vertex
     205             :         to the maximum of the priorities of its successors, if this is less than
     206             :         the vertex's current priority value, and similarly for its predecessors.
     207             : 
     208             :         This preserves winners and optimal strategies, but usually shifts the
     209             :         distribution of priorities towards lower values, which benefits the
     210             :         performance in some solvers.
     211             : 
     212             :         Returns the sum of differences between old and new priority values
     213             :         for all vertices.
     214             :     */
     215             :     long long propagate_priorities();
     216             :     //!@}
     217             : 
     218             :     //!\name Input/Output
     219             :     //!@{
     220             : 
     221             :     /*! Read a game description in PGSolver format. */
     222             :     void read_pgsolver( std::istream &is,
     223             :         StaticGraph::EdgeDirection edge_dir = StaticGraph::EDGE_BIDIRECTIONAL );
     224             : 
     225             :     /*! Write a game description in PGSolver format. */
     226             :     void write_pgsolver(std::ostream &os) const;
     227             : 
     228             :     /*! Read a game description from an mCRL2 PBES. */
     229             :     void read_pbes( const std::string &file_path, verti *goal_vertex = 0,
     230             :         StaticGraph::EdgeDirection edge_dir = StaticGraph::EDGE_BIDIRECTIONAL,
     231             :         const std::string &rewrite_strategy = "jitty" );
     232             : 
     233             :     /*! Read raw parity game data from input stream */
     234             :     void read_raw(std::istream &is);
     235             : 
     236             :     /*! Write raw parity game data to output stream */
     237             :     void write_raw(std::ostream &os) const;
     238             : 
     239             :     /*! Write a game description in Graphviz DOT format */
     240             :     void write_dot(std::ostream &os) const;
     241             : 
     242             :     /*! Write human-readable description of game to error stream (intended to
     243             :         be used while debugging only) with optional strategy. */
     244             :     void write_debug( const Strategy &s = Strategy(),
     245             :         std::ostream &os = std::cerr) const;
     246             : 
     247             :     //!@}
     248             : 
     249             :     //! \name Data access
     250             :     //!@{
     251             : 
     252             :     /*! Returns the priority limit d; all priorities must be in range [0:d). */
     253           0 :     priority_t d() const { return d_; }
     254             : 
     255             :     /*! Returns the game graph */
     256           0 :     const StaticGraph &graph() const { return graph_; }
     257             : 
     258             :     /*! Returns the priority associated with vertex v */
     259           0 :     priority_t priority(verti v) const { return vertex_[v].priority; }
     260             : 
     261             :     /*! Returns the player associated with vertex v */
     262           0 :     Player player(verti v) const { return (Player)(signed char)vertex_[v].player; }
     263             : 
     264             :     /*! Returns the number of vertices with priority `p`.
     265             :         `p` must be between 0 and `d` (exclusive). */
     266           0 :     verti cardinality(int p) const { return cardinality_[p]; }
     267             : 
     268             :     /*! Returns the winner for vertex v according to strategy s. */
     269             :     template<class StrategyT>
     270             :     Player winner(const StrategyT &s, verti v) const;
     271             : 
     272             :     //!@}
     273             : 
     274             :     //!\name Verification
     275             :     //!@{
     276             : 
     277             :     /*! Checks if this is a proper game.
     278             : 
     279             :         A game is proper if every vertex has a successor in the game graph. */
     280             :     bool proper() const;
     281             : 
     282             :     /*! Verifies that the given strategy is valid in this game.
     283             : 
     284             :         \param s the strategy to be verified
     285             :         \param error if non-NULL, then *error is set NO_VERTEX if the strategy is
     286             :                      correct, and to the index of an incorrectly classified
     287             :                      vertex if the strategy is incorrect.
     288             :     */
     289             :     bool verify(const Strategy &s, verti *error) const;
     290             :     //!@}
     291             : 
     292             :     /*! Generate a parity game from an mCRL2 PBES. */
     293             :     void assign_pbes( mcrl2::pbes_system::pbes &pbes, verti *goal_vertex = 0,
     294             :         StaticGraph::EdgeDirection edge_dir = StaticGraph::EDGE_BIDIRECTIONAL,
     295             :         const std::string &rewrite_strategy = "jitty" );
     296             : 
     297             : protected:
     298             :     /*! Re-allocate memory to store information on V vertices with priorities
     299             :         between 0 and `d` (exclusive). */
     300             :     void reset(verti V, int d);
     301             : 
     302             :     /*! Recalculate cardinalities (priority frequencies) from the first
     303             :         `num_vertices` elements of `vertex_`. */
     304             :     void recalculate_cardinalities(verti num_vertices);
     305             : 
     306             :     /*! Helper function for ParityGame::propagate_priorities() that decreases
     307             :         the priority for `v` to the maximum of those in range [begin:end), if
     308             :         this is less than its current value, and returns the absolute change. */
     309             :     int propagate_priority( verti v, StaticGraph::const_iterator it,
     310             :                                      StaticGraph::const_iterator end );
     311             : 
     312             : private:
     313             :     explicit ParityGame(const ParityGame &game);
     314             :     ParityGame &operator=(const ParityGame &game);
     315             : 
     316             : private:
     317             :     int d_;                 /*!< priority limit (max. priority + 1) */
     318             :     StaticGraph graph_;     /*!< game graph */
     319             : 
     320             :     /*! Assignment of players and priorities to vertices (size graph_.V()) */
     321             :     ParityGameVertex *vertex_;
     322             : 
     323             :     /*! Cardinality counts for priorities.
     324             :         cardinality_[p] is equal to the number of vertices with priority p. */
     325             :     verti *cardinality_;
     326             : };
     327             : 
     328             : inline void swap(ParityGame &a, ParityGame &b)
     329             : {
     330             :     a.swap(b);
     331             : }
     332             : 
     333             : #include "ParityGame_impl.h"
     334             : 
     335             : #endif /* ndef MCRL2_PG_PARITY_GAME_H */

Generated by: LCOV version 1.14