mcrl2::pbes_system::lts2pbes_algorithm

Include file:

#include "mcrl2/pbes/lts2pbes.h
class mcrl2::pbes_system::lts2pbes_algorithm

Algorithm for translating a state formula and an untimed specification to a pbes.

Public types

type mcrl2::pbes_system::lts2pbes_algorithm::edge_list

typedef for pbes_system::detail::lts2pbes_lts::edge_list

type mcrl2::pbes_system::lts2pbes_algorithm::state_type

typedef for lts::lts_lts_t::states_size_type

Protected attributes

const lts::lts_lts_t &mcrl2::pbes_system::lts2pbes_algorithm::lts0
pbes_system::detail::lts2pbes_lts mcrl2::pbes_system::lts2pbes_algorithm::lts1
data::set_identifier_generator mcrl2::pbes_system::lts2pbes_algorithm::m_id_generator
utilities::progress_meter mcrl2::pbes_system::lts2pbes_algorithm::m_progress_meter

Protected member functions

void run(const state_formulas::state_formula &f, std::vector<pbes_equation> &equations, Parameters &parameters)

Public member functions

lts2pbes_algorithm(const lts::lts_lts_t &l)

Constructor.

pbes run(const state_formulas::state_formula_specification &formspec, bool preprocess_modal_operators = false, bool generate_counter_example = false)

Runs the translation algorithm.

Parameters:

  • formspec A state formula specification.
  • preprocess_modal_operators A boolean indicating that the modal operators can be preprocessed
  • generate_counter_example A boolean indicating whether a counterexample must be generated.

Returns: The result of the translation