mcrl2::pbes_system::parity_game_generator

Include file:

#include "mcrl2/pbes/parity_game_generator.h
class mcrl2::pbes_system::parity_game_generator

Class for generating a BES from a PBES. This BES can be interpreted as a graph corresponding to a parity game problem. The proposition variables of the BES correspond to the vertices of the graph. An interface to the graph is provided in which the vertices correspond to integer values. The values are in the range [0, 1, …, n], i.e. there are no holes in the sequence. Each vertex is labeled with a priority value, which is the block nesting depth of the proposition variable in the BES.

Public types

type mcrl2::pbes_system::parity_game_generator::operation_type

Values:

  • PGAME_OR
  • PGAME_AND

The operation type of the vertices.

Protected types

type mcrl2::pbes_system::parity_game_generator::substitution_function

typedef for data::rewriter::substitution_type

Substitution function type used by the PBES rewriter.

Protected attributes

data::rewriter mcrl2::pbes_system::parity_game_generator::datar

Data rewriter.

std::vector<std::pair<pbes_expression, std::size_t>> mcrl2::pbes_system::parity_game_generator::m_bes

Contains intermediate results of the BES that is being generated. m_bes[i] represents a BES equation corresponding to BES variable i. m_bes[i].first is the right hand side of the BES equation m_bes[i].second is the block nesting depth of the corresponding PBES variable.

bool mcrl2::pbes_system::parity_game_generator::m_initialized

Mark whether initialization has been initialized. Needed to properly cope with virtual inheritance!

bool mcrl2::pbes_system::parity_game_generator::m_is_min_parity_game

True if it is a min-parity game.

std::size_t mcrl2::pbes_system::parity_game_generator::m_max_priority

The maximum priority value of the game.

pbes &mcrl2::pbes_system::parity_game_generator::m_pbes

The PBES that is being solved.

std::map<core::identifier_string, std::vector<pbes_equation>::const_iterator> mcrl2::pbes_system::parity_game_generator::m_pbes_equation_index

Maps propositional variables to corresponding PBES equations.

std::map<pbes_expression, std::size_t> mcrl2::pbes_system::parity_game_generator::m_pbes_expression_index

Maps PBES closed expressions to corresponding BES variables.

std::map<core::identifier_string, std::size_t> mcrl2::pbes_system::parity_game_generator::m_priorities

Maps propositional variables to corresponding priorities.

bool mcrl2::pbes_system::parity_game_generator::m_true_false_dependencies

Determines what kind of BES equations are generated for true and false.

pbes_system::enumerate_quantifiers_rewriter mcrl2::pbes_system::parity_game_generator::R

PBES rewriter.

Protected member functions

std::size_t add_bes_equation(pbes_expression t, std::size_t priority)

Adds a BES equation for a given PBES expression, if it not already exists.

Parameters:

  • t A PBES expression
  • priority A positive integer

Returns: The index of a BES equation corresponding to the given PBES expression. If no equation exists for the expression, a new one is added.

void compute_equation_index_map()

Compute equation index map.

void compute_priorities(const std::vector<pbes_equation> &equations)

Compute priorities of PBES propositional variables.

pbes_expression expand_rhs(const pbes_expression &psi)
virtual void initialize_generation()
void make_substitution(const data::variable_list &v, const data::data_expression_list &e, substitution_function &sigma) const

Generates a substitution function for the pbesinst rewriter.

Parameters:

  • v A sequence of data variables
  • e A sequence of data expressions
  • sigma The result.
virtual std::string print_bes_equation(std::size_t index, const std::set<std::size_t> &rhs)
std::string print_equation_count(std::size_t size, std::size_t step = 1000) const

Prints a log message for every step-th equation.

Public member functions

virtual std::set<std::size_t> get_dependencies(std::size_t index)

Returns the successors of a vertex in the graph.

Parameters:

  • index A positive integer

Returns: The indices of the proposition variables that appear in the right hand side of the BES equation of the given index.

virtual operation_type get_expression_operation(const pbes_expression &phi)

Returns the vertex type.

Parameters:

  • phi A PBES expression

Returns: PGAME_AND if the expression is a conjunction, PGAME_OR if it is a disjunction.

virtual propositional_variable_instantiation get_initial_state()

Returns the (rewritten) initial state.

Returns: the initial state rewritten by R

virtual std::set<std::size_t> get_initial_values()

Returns the vertices for which a solution is requested. By default a set containing the values 0, 1 and 2 is returned, corresponding to the expressions true, false and the initial state of the PBES.

Returns: A set of indices corresponding to proposition variables of the generated BES.

virtual operation_type get_operation(std::size_t index)

Returns the vertex type.

Parameters:

  • index A positive integer

Returns: PGAME_AND if the corresponding BES equation is a conjunction, PGAME_OR if it is a disjunction.

virtual std::size_t get_priority(std::size_t index)

Returns the priority of a vertex. The priority of the first equation is 0 if it is a maximal fixpoint, and 1 if it is a minimal fixpoint.

Parameters:

  • index A positive integer

Returns: The block nesting depth of the variable in the BES.

parity_game_generator(pbes &p, bool true_false_dependencies = false, bool is_min_parity = true, data::rewriter::strategy rewrite_strategy = data::jitty)

Constructor.

Parameters:

  • p A PBES
  • true_false_dependencies If true, nodes are generated for the values true and false.
  • is_min_parity If true a min-parity game is produced, otherwise a max-parity game
  • rewrite_strategy Strategy to use for the data rewriter
virtual void print_variable_mapping()

Prints the mapping from BES variables to the corresponding PBES expressions.

virtual ~parity_game_generator() = default