mCRL2
Loading...
Searching...
No Matches
mcrl2::lps::invelm_algorithm< Specification > Class Template Reference

#include <invelm_algorithm.h>

Inheritance diagram for mcrl2::lps::invelm_algorithm< Specification >:
mcrl2::lps::detail::lps_algorithm< Specification >

Public Member Functions

 invelm_algorithm (Specification &a_lps, const data::rewriter::strategy a_rewrite_strategy=data::jitty, const int a_time_limit=0, const bool a_path_eliminator=false, const data::detail::smt_solver_type a_solver_type=data::detail::solver_type_cvc, const bool a_apply_induction=false, const bool a_simplify_all=false)
 
void run (const data::data_expression &invariant, bool apply_prover)
 
- Public Member Functions inherited from mcrl2::lps::detail::lps_algorithm< Specification >
 lps_algorithm (Specification &spec)
 Constructor.
 
bool verbose () const
 Flag for verbose output.
 
data::data_expression next_state (const action_summand &s, const data::variable &v) const
 Applies the next state substitution to the variable v.
 
void instantiate_free_variables ()
 Attempts to eliminate the free variables of the specification, by substituting a constant value for them. If no constant value is found for one of the variables, an exception is thrown.
 
void remove_parameters (const std::set< data::variable > &to_be_removed)
 Removes formal parameters from the specification.
 
void remove_singleton_sorts ()
 Removes parameters with a singleton sort.
 
void remove_trivial_summands ()
 Removes summands with condition equal to false.
 
void remove_unused_summand_variables ()
 Removes unused summand variables.
 

Private Types

typedef detail::lps_algorithm< Specification > super
 
typedef Specification::process_type process_type
 
typedef process_type::action_summand_type action_summand_type
 

Private Member Functions

void simplify_summand (summand_base &s, const data::data_expression &invariant, bool apply_prover)
 Adds an invariant to the condition of the summand s, and optionally applies the prover to it.
 
template<typename SummandSequence >
void simplify_summands (SummandSequence &summands, const data::data_expression &invariant, bool apply_prover)
 

Private Attributes

data::detail::BDD_Prover f_bdd_prover
 
bool f_simplify_all
 

Additional Inherited Members

- Protected Member Functions inherited from mcrl2::lps::detail::lps_algorithm< Specification >
void sumelm_find_variables (const action_summand &s, std::set< data::variable > &result) const
 
void sumelm_find_variables (const deadlock_summand &s, std::set< data::variable > &result) const
 
void summand_remove_unused_summand_variables (SummandType &summand_)
 
- Protected Attributes inherited from mcrl2::lps::detail::lps_algorithm< Specification >
Specification & m_spec
 The specification that is processed by the algorithm.
 

Detailed Description

template<class Specification>
class mcrl2::lps::invelm_algorithm< Specification >

The class invariant_eliminator is initialized with an LPS using the constructor invariant_eliminator::invariant_eliminator. After initialization, the method invariant_eliminator::simplify can be called any number of times to simplify or eliminate the summands of this LPS using an invariant. A new instance of the class invariant_eliminator has to be created for each new LPS that has to be processed.

The class invariant_eliminator uses an instance of the class BDD_Prover to simplify or eliminate summands of an mCRL2 LPS. The constructor invariant_eliminator::invariant_eliminator initializes the BDD based prover with the parameters a_rewrite_strategy, a_time_limit, a_path_eliminator, a_solver_type, and the data specification of the LPS passed as parameter a_lps. The parameter a_rewrite_strategy specifies which rewrite strategy is used by the prover's rewriter. It can be set to either GS_REWR_JITTY or GS_REWR_JITTYC. The parameter a_time_limit specifies the maximum amount of time in seconds to be spent by the prover on proving a single expression. If a_time_limit is set to 0, no time limit will be enforced. The parameter a_path_eliminator specifies whether or not path elimination is applied. When path elimination is applied, the prover uses an SMT solver to remove inconsistent paths from BDDs. The parameter a_solver_type specifies which SMT solver is used for path elimination. Either the SMT solver ario (http://www.eecs.umich.edu/~ario/) or cvc-lite (http://www.cs.nyu.edu/acsys/cvcl/) can be used. To use one of these solvers, the directory containing the corresponding executable must be in the path. If the parameter a_path_eliminator is set to false, the parameter a_solver_type is ignored. The parameter a_apply_induction indicates whether or not induction on list will be applied.

The parameter a_dot_file_name specifies whether a file in dot format of the resulting BDD is saved each time the prover cannot determine whether an expression is a contradiction or a tautology. If the parameter is set to 0, no .dot files are saved. If a string is passed as parameter a_dot_file_name, this string will be used as the prefix of the filenames. An instance of the class BDD2Dot is used to save these files in dot format.

If the parameter a_simplify_all is set to false, the summands whose conditions in conjunction with the invariant prove to be a contradiction are eliminated. If parameter a_simplify_all is set to true, in addition to removing those summands, the conditions of all other summands of the LPS are simplified when calling method invariant_eliminator::simplify.

The method invariant_eliminator::simplify returns the LPS passed as parameter a_lps of the constructor after simplification or elimination using the invariant passed as parameter a_invariant. If a_summand_number differs from 0, only the summand with the number passed as parameter a_summand_number will be eliminated or simplified. One instance of the class invariant_eliminator can check any number of invariants on the same LPS. For each new LPS to be checked, a new instance of the class has to be created.

Given an LPS,

P(d: D) = ...

  • sum ei: Ei. ci(d, ei) -> ai(fi(d, ei)) . P(gi(d, ei))
  • ...;

an instance of the class invariant_eliminator will generate a formula of the form

inv(d) /\ ci(d, ei)

for each of the summands or for the chosen summand only, where inv() is the invariant passed as parameter a_invariant. If such a formula is a contradiction according to the prover, the corresponding summand will be eliminated. If the parameter a_simplify_all is set, the condition of each summand is replaced by the BDD obtained from the prover after proving that summand's formula.

Definition at line 76 of file invelm_algorithm.h.

Member Typedef Documentation

◆ action_summand_type

template<class Specification >
typedef process_type::action_summand_type mcrl2::lps::invelm_algorithm< Specification >::action_summand_type
private

Definition at line 80 of file invelm_algorithm.h.

◆ process_type

template<class Specification >
typedef Specification::process_type mcrl2::lps::invelm_algorithm< Specification >::process_type
private

Definition at line 79 of file invelm_algorithm.h.

◆ super

template<class Specification >
typedef detail::lps_algorithm<Specification> mcrl2::lps::invelm_algorithm< Specification >::super
private

Definition at line 78 of file invelm_algorithm.h.

Constructor & Destructor Documentation

◆ invelm_algorithm()

template<class Specification >
mcrl2::lps::invelm_algorithm< Specification >::invelm_algorithm ( Specification &  a_lps,
const data::rewriter::strategy  a_rewrite_strategy = data::jitty,
const int  a_time_limit = 0,
const bool  a_path_eliminator = false,
const data::detail::smt_solver_type  a_solver_type = data::detail::solver_type_cvc,
const bool  a_apply_induction = false,
const bool  a_simplify_all = false 
)
inline

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 119 of file invelm_algorithm.h.

Member Function Documentation

◆ run()

template<class Specification >
void mcrl2::lps::invelm_algorithm< Specification >::run ( const data::data_expression invariant,
bool  apply_prover 
)
inline

Definition at line 133 of file invelm_algorithm.h.

◆ simplify_summand()

template<class Specification >
void mcrl2::lps::invelm_algorithm< Specification >::simplify_summand ( summand_base s,
const data::data_expression invariant,
bool  apply_prover 
)
inlineprivate

Adds an invariant to the condition of the summand s, and optionally applies the prover to it.

Parameters
sThe summand that needs to be simplified
invariantA data expression
apply_proverIf true, the prover is applied to the condition

Definition at line 91 of file invelm_algorithm.h.

◆ simplify_summands()

template<class Specification >
template<typename SummandSequence >
void mcrl2::lps::invelm_algorithm< Specification >::simplify_summands ( SummandSequence &  summands,
const data::data_expression invariant,
bool  apply_prover 
)
inlineprivate

Definition at line 107 of file invelm_algorithm.h.

Member Data Documentation

◆ f_bdd_prover

template<class Specification >
data::detail::BDD_Prover mcrl2::lps::invelm_algorithm< Specification >::f_bdd_prover
private

Definition at line 84 of file invelm_algorithm.h.

◆ f_simplify_all

template<class Specification >
bool mcrl2::lps::invelm_algorithm< Specification >::f_simplify_all
private

Definition at line 85 of file invelm_algorithm.h.


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