mcrl2/pbes/structure_graph.h

Include file:

#include "mcrl2/pbes/structure_graph.h"

add your file description here.

Classes

  • mcrl2::pbes_system::structure_graph::integers_not_contained_in
  • mcrl2::pbes_system::structure_graph
  • mcrl2::pbes_system::structure_graph::vertex
  • mcrl2::pbes_system::structure_graph::vertices_not_contained_in

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.

std::ostream &mcrl2::pbes_system::operator<<(std::ostream &out, const simple_structure_graph &G)
std::ostream &mcrl2::pbes_system::operator<<(std::ostream &out, const structure_graph &G)
std::ostream &mcrl2::pbes_system::operator<<(std::ostream &out, const structure_graph::decoration_type &decoration)
std::ostream &mcrl2::pbes_system::operator<<(std::ostream &out, const structure_graph::vertex &u)
std::ostream &mcrl2::pbes_system::print_structure_graph(std::ostream &out, const StructureGraph &G)
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.
std::vector<typename StructureGraph::index_type> mcrl2::pbes_system::structure_graph_predecessors(const StructureGraph &G, typename StructureGraph::index_type u)
std::vector<typename StructureGraph::index_type> mcrl2::pbes_system::structure_graph_successors(const StructureGraph &G, typename StructureGraph::index_type u)
constexpr unsigned int mcrl2::pbes_system::undefined_vertex()

Functions

bool mcrl2::pbes_system::detail::call_dynamic_bitset_all(const T &t)
auto mcrl2::pbes_system::detail::call_dynamic_bitset_all_helper(T t, int) -> decltype(t.all())
auto mcrl2::pbes_system::detail::call_dynamic_bitset_all_helper(T t, long) -> bool