mCRL2
Loading...
Searching...
No Matches
no_substitution.h
Go to the documentation of this file.
1// Author(s): Wieger Wesselink
2// Copyright: see the accompanying file COPYING or copy at
3// https://github.com/mCRL2org/mCRL2/blob/master/COPYING
4//
5// Distributed under the Boost Software License, Version 1.0.
6// (See accompanying file LICENSE_1_0.txt or copy at
7// http://www.boost.org/LICENSE_1_0.txt)
8//
9/// \file mcrl2/data/substitutions/no_substitution.h
10/// \brief add your file description here.
11
12#ifndef MCRL2_DATA_SUBSTITUTIONS_NO_SUBSTITUTION_H
13#define MCRL2_DATA_SUBSTITUTIONS_NO_SUBSTITUTION_H
14
15#include <iostream>
16#include "mcrl2/data/variable.h"
17
18namespace mcrl2::data
19{
20
21/// \brief An empty struct that is used to denote the absence of a substitution.
22/// Used for rewriters.
24{
25 static constexpr bool is_identity_substitution=true;
26
27 /* static constexpr bool is_trivial()
28 {
29 return true;
30 } */
31
32 const variable& operator()(const variable& v) const
33 {
34 return v;
35 }
36};
37
38inline
40{
41 return out << "[]";
42}
43
44} // namespace mcrl2::data
45
46#endif // MCRL2_DATA_SUBSTITUTIONS_NO_SUBSTITUTION_H
A unordered_map class in which aterms can be stored.
Components for generating an arbitrary element of a sort.
representative_generator(const data_specification &specification)
Constructor with data specification as context.
\brief A data variable
Definition variable.h:25
\brief The and operator for pbes expressions
const pbes_expression & left() const
const pbes_expression & right() const
propositional_variable_instantiation get_initial_state() override
Returns the initial state, rewritten and simplified.
pbes_expression rewrite_and_simplify_expression(const pbes_expression &e, const bool=true)
Rewrites and simplifies an expression.
virtual bool visit_inner_bounded_exists(const pbes_expression &e)
Visits a bounded existential quantifier expression within a disjunctive expression.
Definition ppg_visitor.h:88
virtual ~ppg_visitor()=default
Destructor.
virtual bool visit_inner_implies(const pbes_expression &e)
Visits a disjunctive expression within an inner universal quantifier expression.
virtual bool visit_or(const pbes_expression &e)
Visits a disjunctive expression.
static std::string print_brief(const pbes_expression &e)
Returns a string representation of the type of the root node of the expression.
Definition ppg_visitor.h:38
virtual bool visit_and(const pbes_expression &e)
Visits a conjunctive expression.
virtual bool visit_propositional_variable(const pbes_expression &e)
Visits a propositional variable expression.
Definition ppg_visitor.h:56
virtual bool visit_inner_and(const pbes_expression &e)
Visits a conjunctive expression within an inner existential quantifier expression.
Definition ppg_visitor.h:68
virtual bool visit_ppg_expression(const pbes_expression &e)
Visits a PPG expression.
virtual bool visit_inner_bounded_forall(const pbes_expression &e)
Visits a bounded universal quantifier expression within a conjunctive expression.
virtual bool visit_simple_expression(const pbes_expression &e)
Visits a simple expression. An expression is simple if it does not contain propositional variables.
Definition ppg_visitor.h:47
\brief The existential quantification operator for pbes expressions
const data::variable_list & variables() const
const pbes_expression & body() const
static ltsmin_state false_state()
Returns the state representing false.
ltsmin_state get_state(const propositional_variable_instantiation &expr) const
Returns a PBES_State object for expr.
std::vector< ltsmin_state > get_successors(const ltsmin_state &state, int group)
Computes successor states for a state as defined in transition group group. Serves as a wrapper aroun...
int get_index(int type_no, const std::string &s)
Returns the index of value in the local store for the data type with number type_no....
ltsmin_state get_initial_state() const
Returns the initial state.
static ltsmin_state true_state()
Returns the state representing true.
void to_state_vector(const ltsmin_state &dst_state, int *dst, const ltsmin_state &src_state, int *const &src)
Transforms a PBES state to a state vector, represented by an array of integers.
std::string get_value(int type_no, int index)
Returns the value at position index in the local store for the data type with number type_no....
int get_value_index(int type_no, const data_expression &value)
Returns the index of value in the local store for the data type with number type_no....
explorer(const std::string &filename, const std::string &rewrite_strategy, bool reset_flag, bool always_split_flag)
Constructor.
explorer(const pbes &p_, const std::string &rewrite_strategy, bool reset_flag, bool always_split_flag)
Constructor.
ltsmin_state from_state_vector(int *const &src)
Transforms a state vector src into a PBES_State object object containing the variable and parameter v...
int get_string_index(const std::string &s)
Returns the index of s in the local store for string values. This store is reserved for the string re...
const std::string & get_string_value(int index)
Returns the string at position index in the local store for string values. An exception is thrown if ...
std::vector< ltsmin_state > get_successors(const ltsmin_state &state)
Computes successor states for a state. Serves as a wrapper around the get_successors function of the ...
data::data_expression string_to_data(const std::string &s)
Returns a data expression for the string representation s.
lts_info * get_info() const
Returns the PBES_Info object.
const data_expression & get_data_value(int type_no, int index)
Returns the value at position index in the local store for the data type with number type_no....
detail::pbes_greybox_interface * pgg
the PBES greybox interface
static fixpoint_symbol nu()
Returns the nu symbol.
fixpoint_symbol & operator=(fixpoint_symbol &&) noexcept=default
static fixpoint_symbol mu()
Returns the mu symbol.
\brief The universal quantification operator for pbes expressions
const pbes_expression & body() const
const data::variable_list & variables() const
\brief The implication operator for pbes expressions
const pbes_expression & left() const
const pbes_expression & right() const
bool is_write_dependent_propvar(int group)
Determines if group is write dependent on the propositional variable. Returns true if propositional v...
bool is_read_dependent_parameter(int group, int part)
Determines if group is read dependent on part part of the state vector. Returns true if the parameter...
std::vector< int > get_param_indices(const data::variable_list &params)
Converts a variable_sequence_type into a sequence of indices of parameter signatures in the list of p...
bool is_pass_through_state(const propositional_variable_instantiation &propvar)
Determines if the propositional variable instantiation is one that only copies parameters from the cu...
const std::map< std::string, fixpoint_symbol > & get_variable_symbols() const
Returns the map from variable names to the fixpoint operator of the equation for the variable.
static std::map< variable, std::string > variable_signatures
const std::map< std::string, data::variable_list > & get_variable_parameters() const
Returns the map from variable names to the sequence of parameters for the variable.
const std::map< std::string, propositional_variable > & get_variables() const
Returns the map from variable names to the variable object for the variable.
int get_index(const std::string &signature)
Returns the index for a parameter signature in the list of parameter signatures for the system.
const lts_type & get_lts_type() const
Returns the LTS Type.
bool get_reset_option() const
Returns if the reset option is set.
std::set< std::string > copied(const pbes_expression &expr, const std::set< std::string > &L)
Computes the free variables which are copied/passed through (to a recursive variable) in an expressio...
const std::vector< pbes_expression > & get_transition_expressions() const
Returns the map from transition group number to the expression of the transition group.
std::set< std::string > copied(const pbes_expression &expr)
Computes the free variables which are copied/passed through (to a recursive variable) in an expressio...
detail::pbes_greybox_interface * pgg
bool is_read_dependent_propvar(int group)
Determines if group is read dependent on the propositional variable. Returns true,...
const std::vector< operation_type > & get_transition_types() const
Returns the map from transition group number to the type of the right hand side of the equation to wh...
std::set< std::string > used(const pbes_expression &expr, const std::set< std::string > &L)
Computes the free variables actually used, not only passed through, in an expression.
std::set< std::string > used(const pbes_expression &expr)
Computes the free variables actually used, not only passed through, in an expression.
const std::map< std::string, operation_type > & get_variable_types() const
Returns the map from variable names to the type of the right hand side of the equation for the variab...
void compute_dependency_matrix()
Computes dependency matrix from PBES.
lts_info(pbes &p, detail::pbes_greybox_interface *pgg, bool reset, bool always_split)
Constructor.
static bool tf(const pbes_expression &phi)
Determines if the term phi contains a branch that directly results in true or false (not a variable).
std::vector< pbes_expression > split_expression_and_substitute_variables(const pbes_expression &e, int current_priority, operation_type current_type, std::set< std::string > vars_stack)
Splits the expression into parts (disjuncts or conjuncts) and recursively tries to substitute the pro...
int get_number_of_groups() const
Returns the number of transition groups.
std::map< int, int > get_param_index_positions(const data::variable_list &params)
Converts a variable_sequence_type into a map from indices of parameter signatures (in the list of par...
int count_variables(const pbes_expression &e)
Counts the number of propositional variables in an expression.
void compute_lts_type()
Computes LTS Type from PBES.
std::set< std::string > changed(const pbes_expression &phi, const std::set< std::string > &L)
Computes the set of parameters changed in the expression.
std::string state_to_string(const ltsmin_state &state)
Returns a string representation for state state.
const std::map< std::string, int > & get_variable_priorities() const
Returns the map from variable names to the priority of the equation for the variable.
const data_expression & get_default_value(int index)
Returns a default value for the sort of a parameter signature.
const std::vector< std::string > & get_transition_variable_names() const
Returns the map from transition group number to the variable name of the equation to which the transi...
std::set< std::string > reset(const pbes_expression &phi, const std::set< std::string > &d)
Computes the set of parameters reset in the expression.
bool is_write_dependent_parameter(int group, int part)
Determines if group is read dependent on part part of the state vector. Returns true if the parameter...
std::set< std::string > changed(const pbes_expression &phi)
Computes the set of parameters changed in the expression.
void compute_transition_groups()
Computes transition groups from PBES.
const std::vector< std::string > & get_edge_label_types() const
Returns the sequence of edge label types.
std::size_t get_number_of_state_types() const
Returns the number of state types.
const std::vector< std::string > & get_edge_labels() const
Returns the sequence of edge labels.
int get_state_type_no(int part) const
Returns the state type index for the state part part.
void add_state(const std::string &name, const std::string &type)
Adds a state part of type type with name name.
void add_state_label(const std::string &name, const std::string &type)
Adds a state label of type type with name name.
lts_type(int state_length)
Contructor.
std::string get_state_type_name(int type_no) const
Returns the name of the state type with number type_no.
int get_state_length() const
Returns the state length.
const std::vector< std::string > & get_state_label_types() const
Returns the sequence of state label types.
std::size_t get_number_of_edge_labels() const
Returns the number of edge labels.
const std::vector< std::string > & get_state_types() const
Returns the sequence of state part types.
void add_edge_label(const std::string &name, const std::string &type)
Adds an edge label of type type with name name.
const std::vector< std::string > & get_state_labels() const
Returns the sequence of state labels.
const std::vector< std::string > & get_state_names() const
Returns the sequence of state part names.
std::size_t get_number_of_state_labels() const
Returns the number of state labels.
void add_parameter_value(const data_expression &)
Adds a parameter value to the list of parameter values.
pbes_expression to_pbes_expression() const
Returns a PBES expression representing the state.
std::string state_to_string() const
Returns a string representation of the state.
bool operator<(const ltsmin_state &other) const
Compares two PBES_State objects. Uses lexicographical ordering on priority, type, variable and parame...
ltsmin_state(const std::string &varname)
Constructor.
bool operator==(const ltsmin_state &other) const
Checks if two PBES_State objects are equal.
ltsmin_state(const std::string &varname, const pbes_expression &e)
Constructor.
std::string get_variable() const
Returns a string representation of the propositional variable of the state.
const std::vector< data_expression > & get_parameter_values() const
Returns the list of parameter values.
\brief The not operator for pbes expressions
const pbes_expression & operand() const
\brief The or operator for pbes expressions
const pbes_expression & left() const
const pbes_expression & right() const
Class for generating a BES from a PBES. This BES can be interpreted as a graph corresponding to a par...
const pbes_expression & formula() const
Returns the predicate formula on the right hand side of the equation.
const fixpoint_symbol & symbol() const
Returns the fixpoint symbol of the equation.
const propositional_variable & variable() const
Returns the pbes variable of the equation.
pbes_expression & operator=(const pbes_expression &) noexcept=default
parameterized boolean equation system
Definition pbes.h:54
propositional_variable_instantiation & initial_state()
Returns the initial state.
Definition pbes.h:195
\brief A propositional variable instantiation
const data::data_expression_list & parameters() const
\brief A propositional variable declaration
const core::identifier_string & name() const
propositional_variable(const core::identifier_string &name, const data::variable_list &parameters)
\brief Constructor Z12.
#define mCRL2log(LEVEL)
mCRL2log(LEVEL) provides the stream used to log.
Definition logger.h:393
atermpp::aterm remove_index(const atermpp::aterm &x)
Definition io.h:50
bool is_data_expression(const atermpp::aterm &x)
Test for a data_expression expression.
std::ostream & operator<<(std::ostream &out, const no_substitution &)
The namespace for accessor functions on pbes expressions.
const pbes_expression & arg(const pbes_expression &t)
Returns the pbes expression argument of expressions of type not, exists and forall.
const pbes_expression & left(const pbes_expression &t)
Returns the left hand side of an expression of type and, or or imp.
const pbes_expression & right(const pbes_expression &t)
Returns the right hand side of an expression of type and, or or imp.
static void inc_indent()
Increases the current indent level.
bool is_counter_example_equation(const pbes_equation &equation)
Guesses if the PBES equation is a counter example equation.
static std::regex negative("Zneg_(\\d+)_.*")
bool is_counter_example_positive(const core::identifier_string &name)
Returns true iff the name is Zpos, name must be a counter example name.
apply_data_rewriter_with_pbes_substitution_builder< Builder, DataRewriter, MutableSubstitution, PbesSubstitution > make_apply_data_rewriter_with_pbes_substitution_builder(const DataRewriter &R, MutableSubstitution &sigma, const PbesSubstitution &sigma_pbes)
mcrl2::pbes_system::pbes remove_counterexample_info(const pbes_system::pbes &pbes, bool remove_Lplus=true, bool remove_Lminus=true, bool remove_Lequations=true)
Removes all equations and expressions related to counter examples from the input PBES.
void data_rewrite(data::data_expression &result, const data::data_expression &x, const DataRewriter &R, SubstitutionFunction &sigma)
bool is_counter_example_instantiation(const propositional_variable_instantiation &inst)
Guesses if the PBES variable instantiation is for counter example equation.
void data_rewrite(data::data_expression &result, const data::data_expression &x, const DataRewriter &R, data::no_substitution &)
bool has_counter_example_information(const pbes &pbesspec)
Guesses if a pbes has counter example information.
static void indent()
Indents according to the current indent level.
static std::regex positive("Zpos_(\\d+)_.*")
static void dec_indent()
Decreases the current indent level.
bool is_counter_example_variable(const propositional_variable &X)
static std::regex positive_or_negative("Z(neg|pos)_(\\d+)_.*")
static int indent_count
The current indent level. Used for debug output.
apply_rewriter_builder< Builder, DataRewriter, SubstitutionFunction > make_apply_rewriter_builder(const DataRewriter &datar, SubstitutionFunction &sigma)
bool is_counter_example_name(const core::identifier_string &name)
apply_data_rewriter_with_pbes_substitution_builder< Builder, DataRewriter, MutableSubstitution, no_substitution > make_apply_data_rewriter_with_pbes_substitution_builder(const DataRewriter &R, MutableSubstitution &sigma)
MapContainer::mapped_type map_at(const MapContainer &m, typename MapContainer::key_type key)
bool is_data(const pbes_expression &t)
Returns true if the term t is a data expression.
const pbes_expression & true_()
bool is_not(const atermpp::aterm &x)
bool is_exists(const atermpp::aterm &x)
bool is_or(const atermpp::aterm &x)
bool is_non_simple_conjunct(const pbes_expression &t)
Test for a conjunction.
bool is_simple_expression(const T &x, bool allow_counter_example_propvar)
Determines if an expression is a simple expression. An expression is simple if it is free of proposit...
bool is_forall(const atermpp::aterm &x)
bool is_pbes_or(const pbes_expression &t)
Returns true if the term t is an or expression.
bool is_false(const pbes_expression &t)
Test for the value false.
std::vector< pbes_expression > split_disjuncts(const pbes_expression &expr, bool split_simple_expr=false)
Splits a disjunction into a sequence of operands. Given a pbes expression of the form p1 || p2 || ....
bool is_pbes_and(const pbes_expression &t)
Returns true if the term t is an and expression.
std::vector< pbes_expression > split_conjuncts(const pbes_expression &expr, bool split_simple_expr=false)
Splits a conjunction into a sequence of operands Given a pbes expression of the form p1 && p2 && ....
bool is_propositional_variable_instantiation(const atermpp::aterm &x)
bool is_and(const atermpp::aterm &x)
std::string print_brief(const T &x)
Returns a string representation of the root node of a PBES.
bool is_non_simple_disjunct(const pbes_expression &t)
Test for a disjunction.
bool is_imp(const atermpp::aterm &x)
bool is_true(const pbes_expression &t)
Test for the value true.
const pbes_expression & false_()
An empty struct that is used to denote the absence of a substitution. Used for rewriters.
const variable & operator()(const variable &v) const
static constexpr bool is_identity_substitution
A rewriter that applies a data rewriter to data expressions in a term.
pbes_expression operator()(const pbes_expression &x, SubstitutionFunction &sigma) const
pbes_expression operator()(const pbes_expression &x) const
data_rewriter(const DataRewriter &R_)
void apply(T &result, const data::data_expression &x)
add_data_rewriter(const DataRewriter &R_, SubstitutionFunction &sigma_)
void apply(T &result, const propositional_variable_instantiation &x)
void apply(T &result, const forall &x)
void apply(T &result, const exists &x)
void apply(T &result, const or_ &x)
void apply(T &result, const not_ &x)
void apply(T &result, const and_ &x)
apply_data_rewriter_with_pbes_substitution_builder(const DataRewriter &R, MutableSubstitution &sigma)
apply_data_rewriter_with_pbes_substitution_builder(const DataRewriter &R, MutableSubstitution &sigma, const PbesSubstitution &sigma_pbes)
apply_rewriter_builder(const DataRewriter &datar, SubstitutionFunction &sigma)
A visitor class for PBES equations in BQNF. There is a visit_<node> function for each type of node....
bool debug
flag that indicates if debug output should be printed.
virtual bool visit_bqnf_equation(const pbes_equation &eqn)
Visits a BQNF equation.
virtual bool visit_inner_bounded_exists(const fixpoint_symbol &sigma, const propositional_variable &var, const pbes_expression &e)
Visits a bounded existential quantifier expression within a disjunctive expression.
static std::string print_brief(const pbes_expression &e)
Returns a string representation of the type of the root node of the expression.
virtual bool visit_bounded_forall(const fixpoint_symbol &sigma, const propositional_variable &var, const pbes_expression &e)
Visits a bounded universal quantifier expression.
virtual bool visit_bounded_quantifier(const fixpoint_symbol &sigma, const propositional_variable &var, const pbes_expression &e)
Visits a bounded quantifier expression.
virtual bool visit_inner_and(const fixpoint_symbol &sigma, const propositional_variable &var, const pbes_expression &e)
Visits a conjunctive expression within an inner existential quantifier expression.
virtual bool visit_propositional_variable(const fixpoint_symbol &, const propositional_variable &, const pbes_expression &e)
Visits a propositional variable expression.
static bool is_inner_implies(const pbes_expression &e)
Determines if an expression if of the form phi => psi or of the form phi \/ psi where phi is a simple...
virtual bool visit_simple_expression(const fixpoint_symbol &sigma, const propositional_variable &var, const pbes_expression &e)
Visits a simple expression. An expression is simple if it does not contain propositional variables.
virtual bool visit_bqnf_expression(const pbes_expression &e)
Visits a BQNF expression. In the current BQNF visitor sigma and var parameters are added for use in b...
virtual bool visit_and(const fixpoint_symbol &sigma, const propositional_variable &var, const pbes_expression &e)
Visits a conjunctive expression.
virtual bool visit_bqnf_expression(const fixpoint_symbol &sigma, const propositional_variable &var, const pbes_expression &e)
Visits a BQNF expression.
static bool is_inner_and(const pbes_expression &e)
Determines if an expression if of the form phi /\ psi where phi is a simple expression and psi is an ...
virtual ~bqnf_visitor()=default
Destructor.
virtual bool visit_or(const fixpoint_symbol &sigma, const propositional_variable &var, const pbes_expression &e)
Visits a disjunctive expression.
virtual bool visit_bqnf_equation_debug(const pbes_equation &eqn)
Visits a BQNF equation in debug mode.
virtual bool visit_bounded_exists(const fixpoint_symbol &sigma, const propositional_variable &var, const pbes_expression &e)
Visits a bounded existential quantifier expression.
virtual bool visit_inner_bounded_forall(const fixpoint_symbol &sigma, const propositional_variable &var, const pbes_expression &e)
Visits a bounded universal quantifier expression within a conjunctive expression.
data_rewriter_builder(const DataRewriter &R, SubstitutionFunction &sigma)
void apply_substitution(T &result, const propositional_variable_instantiation &x, const SubstitutionType &sigma)
simplify_data_rewriter_builder(const DataRewriter &R, MutableSubstitution &sigma)
void apply_substitution(T &, const propositional_variable_instantiation &, const no_substitution &)
Overload to have a trivial function in case the substitution is no_substitution.
simplify_data_rewriter_builder(const DataRewriter &R, MutableSubstitution &sigma, const PbesSubstitution &sigma_pbes)
void apply(T &result, const propositional_variable_instantiation &x)
void apply(T &result, const propositional_variable_instantiation &x)
subsitute_counterexample(bool replace_Lplus, bool replace_Lminus)
An empty struct that can be used to indicate that there is no substitution that should be applied to ...
Visitor for printing the root node of a PBES.
void apply(const pbes_equation &x)
void apply(const propositional_variable_instantiation &x)
A rewriter that simplifies boolean expressions in a term, and rewrites data expressions using DataRew...
pbes_expression operator()(const pbes_expression &x) const
pbes_expression operator()(const pbes_expression &x, Substitution &sigma, const PbesSubstitution &sigma_pbes) const
void operator()(pbes_expression &result, const pbes_expression &x, Substitution &sigma, const PbesSubstitution &sigma_pbes) const
void operator()(pbes_expression &result, const pbes_expression &x, Substitution &sigma) const
pbes_expression operator()(const pbes_expression &x, Substitution &sigma) const
A rewriter that simplifies boolean expressions in a term.
void operator()(pbes_expression &result, const pbes_expression &x) const
pbes_expression operator()(const pbes_expression &x, const PbesSubstitution &sigma) const
pbes_expression operator()(const pbes_expression &x) const
void operator()(pbes_expression &result, const pbes_expression &x, const PbesSubstitution &sigma) const