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

#include <lps2pbes.h>

Public Member Functions
	lps2pbes_algorithm (bool check_only=false)
	Constructor.

pbes	run (const state_formulas::state_formula &formula, const lps::stochastic_specification &lpsspec, bool structured=false, bool unoptimized=false, bool preprocess_modal_operators=false, bool generate_counter_example=false, const data::variable &T=data::undefined_real_variable())
	Runs the translation algorithm.

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

Protected Attributes
data::set_identifier_generator	m_generator

bool	m_check_only = false

Detailed Description

Algorithm for translating a state formula and a timed specification to a pbes.

Definition at line 32 of file lps2pbes.h.

Constructor & Destructor Documentation

◆ lps2pbes_algorithm()

mcrl2::pbes_system::lps2pbes_algorithm::lps2pbes_algorithm ( bool check_only = false )

inlineexplicit

Constructor.

Definition at line 67 of file lps2pbes.h.

Member Function Documentation

◆ run() [1/2]

template<typename Parameters >

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

inlineprotected

Definition at line 39 of file lps2pbes.h.

◆ run() [2/2]

pbes mcrl2::pbes_system::lps2pbes_algorithm::run	(	const state_formulas::state_formula &	formula,
		const lps::stochastic_specification &	lpsspec,
		bool	structured = `false`,
		bool	unoptimized = `false`,
		bool	preprocess_modal_operators = `false`,
		bool	generate_counter_example = `false`,
		const data::variable &	T = `data::undefined_real_variable()`
	)

inline

Runs the translation algorithm.

Parameters

formula	A modal formula that represents a property about the system modeled by the given specification
lpsspec	A linear process specification
structured	use the 'structured' approach of generating equations
unoptimized	do not optimize the resulting PBES.
preprocess_modal_operators	insert dummy fixpoints in modal operators, which may lead to smaller PBESs
generate_counter_example	If true, then the PBES is enhanced with additional equations that are used to extract a counter example.
T	The time parameter. If T == data::variable() the untimed version of lps2pbes is applied.

Returns: A PBES that encodes the property applied to the given specification

Definition at line 80 of file lps2pbes.h.

Member Data Documentation

◆ m_check_only

bool mcrl2::pbes_system::lps2pbes_algorithm::m_check_only = false

protected

Definition at line 36 of file lps2pbes.h.

◆ m_generator

data::set_identifier_generator mcrl2::pbes_system::lps2pbes_algorithm::m_generator

protected

Definition at line 35 of file lps2pbes.h.

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

pbes/include/mcrl2/pbes/lps2pbes.h

Public Member Functions

Protected Member Functions

Protected Attributes