12#ifndef MCRL2_PBES_ENUMERATOR_H
13#define MCRL2_PBES_ENUMERATOR_H
15#include "mcrl2/data/enumerator.h"
16#include "mcrl2/pbes/pbes_expression.h"
A unordered_map class in which aterms can be stored.
const data_expression & body() const
data_expression & operator=(const data_expression &) noexcept=default
The default element for the todo list of the enumerator.
existential quantification.
universal quantification.
Components for generating an arbitrary element of a sort.
representative_generator(const data_specification &specification)
Constructor with data specification as context.
Rewriter that operates on data expressions.
\brief The and operator for pbes expressions
and_(const pbes_expression &left, const pbes_expression &right)
\brief Constructor Z14.
const pbes_expression & left() const
const pbes_expression & right() const
std::set< pbes_expression > get_successors(const pbes_expression &phi)
Returns the successors of a state, which is a instantiated propositional variable....
~pbes_greybox_interface() override=default
propositional_variable_instantiation get_initial_state() override
Returns the initial state, rewritten and simplified.
virtual std::string print_successors(const std::set< pbes_expression > &successors)
Prints the set of successors states.
pbes_greybox_interface(pbes &p, bool true_false_dependencies=false, bool is_min_parity=true, data::rewriter::strategy rewrite_strategy=data::jitty)
Constructor.
pbes_system::enumerate_quantifiers_rewriter pbes_rewriter
pbes_equation get_pbes_equation(const core::identifier_string &s)
Returns the equation for variable s.
pbes_expression rewrite_and_simplify_expression(const pbes_expression &e, const bool=true)
Rewrites and simplifies an expression.
std::set< pbes_expression > get_successors(const pbes_expression &phi, const std::string &var, const pbes_expression &expr)
Returns the successors of a state, which is a instantiated propositional variable,...
virtual pbes_expression expand_group(const pbes_expression &psi, const pbes_expression &expr)
Expands a formula expr for a instantiated state variable psi, which means substituting the variables ...
virtual bool visit_inner_bounded_exists(const pbes_expression &e)
Visits a bounded existential quantifier expression within a disjunctive expression.
ppg_visitor()=default
Constructor.
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.
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.
virtual bool visit_inner_and(const pbes_expression &e)
Visits a conjunctive expression within an inner existential quantifier expression.
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.
\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...
std::string data_to_string(const data::data_expression &e)
Returns a string representation for the data expression e.
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....
std::vector< std::string > localmap_int2string
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.
std::map< std::string, int > localmap_string2int
void next_state_long(int *const &src, int group, callback &cb)
Iterates over the successors of a state for a certain transition group and invokes a callback functio...
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....
void next_state_all(int *const &src, callback &cb)
Iterates over the successors of a state and invokes a callback function for each successor state.
detail::pbes_greybox_interface * pgg
the PBES greybox interface
void initial_state(int *state)
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...
std::map< std::string, int > variable_priority
static std::vector< std::string > get_param_sequence(const data::variable_list ¶ms)
Converts a variable_sequence_type into a sequence of parameter signatures.
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 ¶ms)
Converts a variable_sequence_type into a sequence of indices of parameter signatures in the list of p...
std::vector< std::string > transition_variable_name
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
std::map< std::string, fixpoint_symbol > variable_symbol
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.
std::map< std::string, int > param_index
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...
std::vector< data_expression > param_default_values
detail::pbes_greybox_interface * pgg
bool is_read_dependent_propvar(int group)
Determines if group is read dependent on the propositional variable. Returns true,...
std::vector< pbes_expression > transition_expression
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.
static std::string get_param_signature(const variable ¶m)
Returns a signature for parameter param.
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...
std::map< std::string, propositional_variable > variables
int get_number_of_groups() const
Returns the number of transition groups.
static std::set< std::string > get_param_set(const data::variable_list ¶ms)
Converts a variable_sequence_type into a set of parameter signatures.
std::map< int, int > get_param_index_positions(const data::variable_list ¶ms)
Converts a variable_sequence_type into a map from indices of parameter signatures (in the list of par...
static std::set< std::string > occ(const pbes_expression &expr)
Computes the propositional variables used in an expression.
std::map< std::string, operation_type > variable_type
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::vector< operation_type > transition_type
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.
std::map< std::string, data::variable_list > variable_parameters
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.
static std::string get_param_signature(const std::string ¶mname, const std::string ¶mtype)
Returns a signature using name and type of a parameter.
static std::set< std::string > free(const pbes_expression &expr)
Computes the free variables read in an expression.
std::vector< pbes_expression > transition_expression_plain
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::map< std::string, pbes_expression > variable_expression
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.
std::vector< std::string > state_type_list
std::vector< std::string > state_label_types
std::vector< std::string > state_names
std::vector< int > state_type_no
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.
std::map< std::string, int > state_type_index
std::vector< std::string > edge_label_names
const std::vector< std::string > & get_state_label_types() const
Returns the sequence of state label types.
std::vector< std::string > edge_label_types
std::vector< std::string > state_types
std::size_t get_number_of_edge_labels() const
Returns the number of edge labels.
std::vector< std::string > state_label_names
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::vector< data_expression > param_values
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
or_(const pbes_expression &left, const pbes_expression &right)
\brief Constructor Z14.
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...
void compute_priorities(const std::vector< pbes_equation > &equations)
Compute priorities of PBES propositional variables.
virtual operation_type get_expression_operation(const pbes_expression &phi)
Returns the vertex type.
parity_game_generator(pbes &p, bool true_false_dependencies=false, bool is_min_parity=true, data::rewriter::strategy rewrite_strategy=data::jitty)
Constructor.
virtual void print_variable_mapping()
Prints the mapping from BES variables to the corresponding PBES expressions.
std::map< core::identifier_string, std::size_t > m_priorities
Maps propositional variables to corresponding priorities.
void compute_equation_index_map()
Compute equation index map.
pbes_expression expand_rhs(const pbes_expression &psi)
virtual operation_type get_operation(std::size_t index)
Returns the vertex type.
bool m_true_false_dependencies
Determines what kind of BES equations are generated for true and false.
virtual propositional_variable_instantiation get_initial_state()
Returns the (rewritten) initial state.
std::string print_equation_count(std::size_t size, std::size_t step=1000) const
Prints a log message for every step-th equation.
std::map< pbes_expression, std::size_t > m_pbes_expression_index
Maps PBES closed expressions to corresponding BES variables.
virtual void initialize_generation()
std::size_t m_max_priority
The maximum priority value of the game.
pbes_system::enumerate_quantifiers_rewriter R
PBES rewriter.
void make_substitution(const data::variable_list &v, const data::data_expression_list &e, substitution_function &sigma) const
Generates a substitution function for the pbesinst rewriter.
pbes & m_pbes
The PBES that is being solved.
virtual std::size_t get_priority(std::size_t index)
Returns the priority of a vertex. The priority of the first equation is 0 if it is a maximal fixpoint...
virtual std::set< std::size_t > get_initial_values()
Returns the vertices for which a solution is requested. By default a set containing the values 0,...
virtual ~parity_game_generator()=default
virtual std::string print_bes_equation(std::size_t index, const std::set< std::size_t > &rhs)
data::rewriter datar
Data rewriter.
operation_type
The operation type of the vertices.
bool m_is_min_parity_game
True if it is a min-parity game.
std::size_t add_bes_equation(pbes_expression t, std::size_t priority)
Adds a BES equation for a given PBES expression, if it not already exists.
bool m_initialized
Mark whether initialization has been initialized. Needed to properly cope with virtual inheritance!
virtual std::set< std::size_t > get_dependencies(std::size_t index)
Returns the successors of a vertex in the graph.
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=(pbes_expression &&) noexcept=default
pbes_expression & operator=(const pbes_expression &) noexcept=default
parameterized boolean equation system
propositional_variable_instantiation & initial_state()
Returns the initial state.
\brief A propositional variable instantiation
const data::data_expression_list & parameters() const
const core::identifier_string & name() const
\brief A propositional variable declaration
const core::identifier_string & name() const
propositional_variable(const core::identifier_string &name, const data::variable_list ¶meters)
\brief Constructor Z12.
#define mCRL2log(LEVEL)
mCRL2log(LEVEL) provides the stream used to log.
atermpp::aterm remove_index(const atermpp::aterm &x)
void split_finite_variables(data::variable_list variables, const data::data_specification &data, data::variable_list &finite_variables, data::variable_list &infinite_variables, data::variable_list &unused, const FILTER filter)
Splits the variables in a subset with finite sort, with infinite sort and those that are not used acc...
void split_enumerable_variables(data::variable_list variables, const data::data_specification &data, const Rewriter &rewr, data::variable_list &enumerable_variables, data::variable_list &non_enumerable_variables, data::variable_list &unused, const FILTER filter)
Splits a list of variables in those that are enumerable, non enumerable and not used,...
Namespace for system defined sort bool_.
const function_symbol & false_()
Constructor for function symbol false.
const function_symbol & true_()
Constructor for function symbol true.
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.
std::set< data::variable > significant_variables(const pbes_expression &x)
Returns the significant variables of a pbes expression.
void remove_parameters(pbes &x, const std::set< data::variable > &to_be_removed)
Removes parameters from propositional variable instantiations in a pbes expression.
void remove_parameters(pbes &x, const std::map< core::identifier_string, std::vector< std::size_t > > &to_be_removed)
Removes parameters from propositional variable instantiations in a pbes expression.
void pbesinst_finite(pbes &p, data::rewrite_strategy rewrite_strategy, const std::string &finite_parameter_selection)
Apply finite instantiation to the given PBES.
void instantiate_global_variables(pbes &p)
Attempts to eliminate the free variables of a PBES, by substituting a constant value for them....
bool is_normalized(const pbes &x)
Checks if a PBEs is normalized.
std::vector< propositional_variable > remove_unreachable_variables(pbes &p)
Removes equations that are not (syntactically) reachable from the initial state of a PBES.
bool is_bes(const pbes &x)
Returns true if a PBES is in BES form.
std::string print_removed_equations(const std::vector< propositional_variable > &removed)
Print removed equations.
void normalize(pbes &x)
The function normalize brings (embedded) pbes expressions into positive normal form,...
apply_enumerate_builder< Builder, DataRewriter, MutableSubstitution, no_substitution > make_apply_enumerate_builder(const DataRewriter &R, MutableSubstitution &sigma, const data::data_specification &dataspec, data::enumerator_identifier_generator &id_generator, bool enumerate_infinite_sorts)
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)
apply_enumerate_builder< Builder, DataRewriter, MutableSubstitution, PbesSubstitution > make_apply_enumerate_builder(const DataRewriter &R, MutableSubstitution &sigma, const PbesSubstitution &sigma_pbes, const data::data_specification &dataspec, data::enumerator_identifier_generator &id_generator, bool enumerate_infinite_sorts)
The main namespace for the PBES library.
bool is_pbes_file_format(const utilities::file_format &format)
pbes_expression join_or(FwdIt first, FwdIt last)
Returns or applied to the sequence of pbes expressions [first, last)
bool is_data(const pbes_expression &t)
Returns true if the term t is a data expression.
void load_pbes(pbes &pbes, std::istream &stream, utilities::file_format format, const std::string &)
Load a PBES from file.
std::set< pbes_expression > split_and(const pbes_expression &expr, bool split_data_expressions=false)
Splits a conjunction into a sequence of operands Given a pbes expression of the form p1 && p2 && ....
void save_pbes(const pbes &pbes, const std::string &filename, utilities::file_format format, bool welltypedness_check)
save_pbes Saves a PBES to a file.
const pbes_expression & true_()
bool is_not(const atermpp::aterm &x)
const utilities::file_format & pbes_format_internal_bes()
pbes_expression optimized_join_and(FwdIt first, FwdIt last)
Returns and applied to the sequence of pbes expressions [first, last)
pbes_expression optimized_join_or(FwdIt first, FwdIt last)
Returns or applied to the sequence of pbes expressions [first, last)
pbes_expression join_and(FwdIt first, FwdIt last)
Returns and applied to the sequence of pbes expressions [first, last)
void load_pbes(pbes &pbes, const std::string &filename, utilities::file_format format)
Load pbes from file.
const utilities::file_format & pbes_format_pgsolver()
bool is_exists(const atermpp::aterm &x)
utilities::file_format guess_format(const std::string &filename)
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)
const std::vector< utilities::file_format > & pbes_file_formats()
void save_bes_pgsolver(const pbes &bes, std::ostream &stream, bool maxpg)
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.
void save_pbes(const pbes &pbes, std::ostream &stream, utilities::file_format format)
Save a PBES in the format specified.
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 && ....
const utilities::file_format & pbes_format_internal()
bool is_propositional_variable_instantiation(const atermpp::aterm &x)
const utilities::file_format & pbes_format_text()
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.
std::set< pbes_expression > split_or(const pbes_expression &expr, bool split_data_expressions=false)
Splits a disjunction into a sequence of operands Given a pbes expression of the form p1 || p2 || ....
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_()
void apply(T &result, const data::variable &x)
void apply(T &result, const data::lambda &x)
void enumerate_exists(data_expression &result, const data::variable_list &v, const data_expression &phi)
void operator()(data_expression &result, const data_expression &x, MutableSubstitution &sigma)
data::enumerator_algorithm< self > E
The enumerator.
void apply(T &result, const forall &x)
atermpp::vector< data::data_expression > undo_substitution(const data::variable_list &variables)
enumerate_quantifiers_builder(const DataRewriter &R, MutableSubstitution &sigma, const data::data_specification &dataspec, data::enumerator_identifier_generator &id_generator, bool enumerate_infinite_sorts=true)
Constructor.
void enumerate_forall(data_expression &result, const data::variable_list &v, const data_expression &phi)
bool m_enumerate_infinite_sorts
If false, only quantifier variables over finite sort are enumerated.
void redo_substitution(const data::variable_list &v, const atermpp::vector< data::data_expression > &undo)
void apply(T &result, const data::exists &x)
const data::data_specification & m_dataspec
MutableSubstitution & m_sigma
const data::rewriter & m_rewriter
A data rewriter.
data_expression operator()(const data_expression &x, Substitution &sigma) const
data::enumerator_identifier_generator & m_id_generator
bool m_enumerate_infinite_sorts
If true, quantifier variables of infinite sort are enumerated.
enumerate_quantifiers_rewriter(const data::rewriter &R, const data::data_specification &dataspec, data::enumerator_identifier_generator &id_generator, bool enumerate_infinite_sorts=true)
const data::data_specification & m_dataspec
A data specification.
void operator()(data_expression &result, const data_expression &x, Substitution &sigma) const
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_)
SubstitutionFunction & sigma
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 imp &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_enumerate_builder(const DataRewriter &R, MutableSubstitution &sigma, const PbesSubstitution &sigma_pbes, const data::data_specification &dataspec, data::enumerator_identifier_generator &id_generator, const enumerate_quantifiers_mode enum_mode)
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)
enumerate_quantifiers_mode m_enum_mode
If false, only quantifier variables over finite sorts are enumerated.
void operator()(pbes_expression &result, const pbes_expression &x, MutableSubstitution &)
void enumerate_exists(pbes_expression &result, const data::variable_list &v, const pbes_expression &phi)
data::enumerator_identifier_generator & m_id_generator
identifier generator
void redo_substitution(const data::variable_list &v, const atermpp::vector< data::data_expression > &undo)
void apply(T &result, const exists &x)
const data::data_specification & m_dataspec
pbes_expression operator()(const pbes_expression &x, MutableSubstitution &)
void apply(T &result, const forall &x)
void enumerate_forall(pbes_expression &result, const data::variable_list &v, const pbes_expression &phi)
atermpp::vector< data::data_expression > undo_substitution(const data::variable_list &variables)
void apply(T &result, const data::data_expression &x)
enumerate_quantifiers_builder(const DataRewriter &R, MutableSubstitution &sigma, const PbesSubstitution &sigma_pbes, const data::data_specification &dataspec, data::enumerator_identifier_generator &id_generator, enumerate_quantifiers_mode enum_mode=expand_infinite_sorts_and_use_data_rewriter)
Constructor.
data::enumerator_algorithm< self > E
The enumerator.
void apply(T &result, const exists &x)
void apply_substitution(T &result, const propositional_variable_instantiation &x, const SubstitutionType &sigma)
MutableSubstitution & substitution()
const PbesSubstitution & m_sigma_pbes
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.
substitution_administration_type substitution_administration
void apply(T &result, const forall &x)
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 attempt for improving the efficiency.
void clear_identifier_generator()
void operator()(pbes_expression &result, const pbes_expression &x, MutableSubstitution &sigma) const
void thread_initialise()
Initialises this rewriter with thread dependent information.
pbes_expression operator()(const pbes_expression &x, MutableSubstitution &sigma, const PbesSubstitution &sigma_pbes) const
enumerate_quantifiers_mode m_enum_mode
If true, quantifier variables of infinite sort are enumerated.
enumerate_quantifiers_rewriter clone()
Create a clone of the rewriter in which the underlying rewriter is copied, and not passed as a shared...
data::data_specification m_dataspec
A data specification.
void operator()(pbes_expression &result, const pbes_expression &x, MutableSubstitution &sigma, const PbesSubstitution &sigma_pbes) const
enumerate_quantifiers_rewriter(const data::rewriter &R, const data::data_specification &dataspec, const enumerate_quantifiers_mode enum_mode=expand_infinite_sorts_and_use_data_rewriter)
data::enumerator_identifier_generator m_id_generator
pbes_expression operator()(const pbes_expression &x) const
data::rewriter m_rewriter
A data rewriter.
pbes_expression operator()(const pbes_expression &x, MutableSubstitution &sigma) const
bool operator()(const pbes_expression &x) const
bool operator()(const pbes_expression &x) const
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)
void apply(const forall &)
void apply(const exists &)
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
simplify_data_rewriter(const DataRewriter &R_)
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