mcrl2/pbes/solve_structure_graph.h

Include file:

#include "mcrl2/pbes/solve_structure_graph.h"

add your file description here.

Functions

std::tuple<std::size_t, std::size_t, vertex_set> mcrl2::pbes_system::get_minmax_rank(const structure_graph &G)
bool mcrl2::pbes_system::has_counter_example_information(const pbes &pbesspec)

Guesses if a pbes has counter example information.

bool mcrl2::pbes_system::solve_structure_graph(structure_graph &G, bool check_strategy = false)
std::pair<bool, lps::specification> mcrl2::pbes_system::solve_structure_graph_with_counter_example(structure_graph &G, const lps::specification &lpsspec, const pbes &p, const pbes_equation_index &p_index)
bool mcrl2::pbes_system::solve_structure_graph_with_counter_example(structure_graph &G, lts::lts_lts_t &ltsspec)

Solve this pbes_system using a structure graph generating a counter example.

Parameters:

  • G The structure graph.
  • ltsspec The original LTS that was used to create the PBES.