mcrl2::lps::detail::Invariant_Checker< Specification > Class Template Reference

#include <invariant_checker.h>

Public Member Functions
	Invariant_Checker (const Specification &a_lps, data::rewriter::strategy a_rewrite_strategy=data::jitty, int a_time_limit=0, bool a_path_eliminator=false, data::detail::smt_solver_type a_solver_type=data::detail::solver_type_cvc, bool a_apply_induction=false, bool a_counter_example=false, bool a_all_violations=false, const std::string &a_dot_file_name=std::string())
bool	check_invariant (const data::data_expression &a_invariant)
	precondition: the argument passed as parameter a_invariant is a valid expression in internal mCRL2 format

Private Types
typedef Specification::process_type	process_type
typedef process_type::action_summand_type	action_summand_type
typedef std::vector< action_summand_type >	action_summand_vector_type

Private Member Functions
void	print_counter_example ()
void	save_dot_file (std::size_t a_summand_number)
bool	check_init (const data::data_expression &a_invariant)
bool	check_summand (const data::data_expression &a_invariant, const action_summand_type &a_summand, const std::size_t a_summand_number)
bool	check_summands (const data::data_expression &a_invariant)

Private Attributes
const Specification &	f_spec
data::detail::BDD_Prover	f_bdd_prover
data::detail::BDD2Dot	f_bdd2dot
process_initializer	f_init
action_summand_vector_type	f_summands
bool	f_counter_example
bool	f_all_violations
std::string	f_dot_file_name

Detailed Description

template<typename Specification>
class mcrl2::lps::detail::Invariant_Checker< Specification >

Definition at line 72 of file invariant_checker.h.

Member Typedef Documentation

action_summand_type

template<typename Specification >

typedef process_type::action_summand_type mcrl2::lps::detail::Invariant_Checker< Specification >::action_summand_type

private

Definition at line 75 of file invariant_checker.h.

action_summand_vector_type

template<typename Specification >

typedef std::vector<action_summand_type> mcrl2::lps::detail::Invariant_Checker< Specification >::action_summand_vector_type

private

Definition at line 76 of file invariant_checker.h.

process_type

template<typename Specification >

typedef Specification::process_type mcrl2::lps::detail::Invariant_Checker< Specification >::process_type

private

Definition at line 74 of file invariant_checker.h.

Constructor & Destructor Documentation

Invariant_Checker()

template<typename Specification >

mcrl2::lps::detail::Invariant_Checker< Specification >::Invariant_Checker	(	const Specification &	a_lps,
		data::rewriter::strategy	a_rewrite_strategy = data::jitty,
		int	a_time_limit = 0,
		bool	a_path_eliminator = false,
		data::detail::smt_solver_type	a_solver_type = data::detail::solver_type_cvc,
		bool	a_apply_induction = false,
		bool	a_counter_example = false,
		bool	a_all_violations = false,
		const std::string &	a_dot_file_name = std::string()
	)

precondition: the argument passed as parameter a_lps is a valid mCRL2 LPS precondition: the argument passed as parameter a_time_limit is greater than or equal to 0. If the argument is equal to 0, no time limit will be enforced

Definition at line 238 of file invariant_checker.h.

Member Function Documentation

check_init()

template<typename Specification >

bool mcrl2::lps::detail::Invariant_Checker< Specification >::check_init ( const data::data_expression &  a_invariant )

private

Definition at line 151 of file invariant_checker.h.

check_invariant()

template<typename Specification >

bool mcrl2::lps::detail::Invariant_Checker< Specification >::check_invariant

(

const data::data_expression &

a_invariant

)

precondition: the argument passed as parameter a_invariant is a valid expression in internal mCRL2 format

Definition at line 256 of file invariant_checker.h.

check_summand()

template<typename Specification >

bool mcrl2::lps::detail::Invariant_Checker< Specification >::check_summand ( const data::data_expression &  a_invariant, const action_summand_type &  a_summand, const std::size_t  a_summand_number  )

private

Definition at line 183 of file invariant_checker.h.

check_summands()

template<typename Specification >

bool mcrl2::lps::detail::Invariant_Checker< Specification >::check_summands ( const data::data_expression &  a_invariant )

private

Definition at line 222 of file invariant_checker.h.

print_counter_example()

template<typename Specification >

void mcrl2::lps::detail::Invariant_Checker< Specification >::print_counter_example

private

Definition at line 117 of file invariant_checker.h.

save_dot_file()

template<typename Specification >

void mcrl2::lps::detail::Invariant_Checker< Specification >::save_dot_file ( std::size_t  a_summand_number )

private

Definition at line 130 of file invariant_checker.h.

Member Data Documentation

f_all_violations

template<typename Specification >

bool mcrl2::lps::detail::Invariant_Checker< Specification >::f_all_violations

private

Definition at line 85 of file invariant_checker.h.

f_bdd2dot

template<typename Specification >

data::detail::BDD2Dot mcrl2::lps::detail::Invariant_Checker< Specification >::f_bdd2dot

private

Definition at line 81 of file invariant_checker.h.

f_bdd_prover

template<typename Specification >

data::detail::BDD_Prover mcrl2::lps::detail::Invariant_Checker< Specification >::f_bdd_prover

private

Definition at line 80 of file invariant_checker.h.

f_counter_example

template<typename Specification >

bool mcrl2::lps::detail::Invariant_Checker< Specification >::f_counter_example

private

Definition at line 84 of file invariant_checker.h.

f_dot_file_name

template<typename Specification >

std::string mcrl2::lps::detail::Invariant_Checker< Specification >::f_dot_file_name

private

Definition at line 86 of file invariant_checker.h.

f_init

template<typename Specification >

process_initializer mcrl2::lps::detail::Invariant_Checker< Specification >::f_init

private

Definition at line 82 of file invariant_checker.h.

f_spec

template<typename Specification >

const Specification& mcrl2::lps::detail::Invariant_Checker< Specification >::f_spec

private

Definition at line 79 of file invariant_checker.h.

f_summands

template<typename Specification >

action_summand_vector_type mcrl2::lps::detail::Invariant_Checker< Specification >::f_summands

private

Definition at line 83 of file invariant_checker.h.

---

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

• lps/include/mcrl2/lps/invariant_checker.h