mcrl2::pbes_system::lts2pbes_algorithm Class Reference

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

#include <lts2pbes.h>

Public Types
using	state_type = lts::lts_lts_t::states_size_type
using	edge_list = pbes_system::detail::lts2pbes_lts::edge_list

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.

Protected Member Functions
template<typename Parameters >
void	run (const state_formulas::state_formula &f, std::vector< pbes_equation > &equations, Parameters &parameters)

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

Detailed Description

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

Definition at line 22 of file lts2pbes.h.

Member Typedef Documentation

edge_list

using mcrl2::pbes_system::lts2pbes_algorithm::edge_list = pbes_system::detail::lts2pbes_lts::edge_list

Definition at line 26 of file lts2pbes.h.

state_type

using mcrl2::pbes_system::lts2pbes_algorithm::state_type = lts::lts_lts_t::states_size_type

Definition at line 25 of file lts2pbes.h.

Constructor & Destructor Documentation

lts2pbes_algorithm()

mcrl2::pbes_system::lts2pbes_algorithm::lts2pbes_algorithm ( const lts::lts_lts_t &  l )

inlineexplicit

Constructor.

Definition at line 42 of file lts2pbes.h.

Member Function Documentation

run() [1/2]

template<typename Parameters >

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

inlineprotected

Definition at line 35 of file lts2pbes.h.

run() [2/2]

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

inline

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

Definition at line 52 of file lts2pbes.h.

Member Data Documentation

lts0

const lts::lts_lts_t& mcrl2::pbes_system::lts2pbes_algorithm::lts0

protected

Definition at line 29 of file lts2pbes.h.

lts1

pbes_system::detail::lts2pbes_lts mcrl2::pbes_system::lts2pbes_algorithm::lts1

protected

Definition at line 30 of file lts2pbes.h.

m_id_generator

data::set_identifier_generator mcrl2::pbes_system::lts2pbes_algorithm::m_id_generator

protected

Definition at line 32 of file lts2pbes.h.

m_progress_meter

utilities::progress_meter mcrl2::pbes_system::lts2pbes_algorithm::m_progress_meter

protected

Definition at line 31 of file lts2pbes.h.

---

The documentation for this class was generated from the following file:

• pbes/include/mcrl2/pbes/lts2pbes.h