mcrl2::lps::detail::Invariant_Checker

Include file:

#include "mcrl2/lps/invariant_checker.h

class mcrl2::lps::detail::Invariant_Checker

Private types

type mcrl2::lps::detail::Invariant_Checker::action_summand_type

typedef for process_type::action_summand_type

type mcrl2::lps::detail::Invariant_Checker::action_summand_vector_type

typedef for std::vector< action_summand_type >

type mcrl2::lps::detail::Invariant_Checker::process_type

typedef for Specification::process_type

Private attributes

bool mcrl2::lps::detail::Invariant_Checker::f_all_violations

data::detail::BDD2Dot mcrl2::lps::detail::Invariant_Checker::f_bdd2dot

data::detail::BDD_Prover mcrl2::lps::detail::Invariant_Checker::f_bdd_prover

bool mcrl2::lps::detail::Invariant_Checker::f_counter_example

std::string mcrl2::lps::detail::Invariant_Checker::f_dot_file_name

process_initializer mcrl2::lps::detail::Invariant_Checker::f_init

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

action_summand_vector_type mcrl2::lps::detail::Invariant_Checker::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