Include file:

#include "mcrl2/lps/invariant_checker.h
class mcrl2::lps::detail::Invariant_Checker

Private types

type action_summand_type

typedef for process_type::action_summand_type

type action_summand_vector_type

typedef for std::vector< action_summand_type >

type process_type

typedef for Specification::process_type

Private attributes

bool f_all_violations
data::detail::BDD2Dot f_bdd2dot
data::detail::BDD_Prover f_bdd_prover
bool f_counter_example
std::string f_dot_file_name
process_initializer f_init
action_summand_vector_type f_summands

Private member functions

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)
void print_counter_example()
void save_dot_file(std::size_t a_summand_number)

Public member functions

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

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