29 template <
typename MapContainer>
30 typename MapContainer::mapped_type
map_at(
const MapContainer& m,
typename MapContainer::key_type key)
32 typename MapContainer::const_iterator i = m.find(key);
130 std::size_t type_index;
131 std::map<std::string,int>::iterator type_index_it = this->
state_type_index.find(type);
133 type_index = type_index_it->second;
145 const std::string& type)
153 const std::string& type)
168 always_split_option(always_split),
173 throw std::runtime_error(
"PBES is not a PPG! Please rewrite with pbesrewr -pppg.");
186 std::vector<std::string> params;
187 std::map<std::string,std::string> paramtypes;
196 for (
const variable& varparam: var.parameters())
199 bool new_param =
true;
200 for (
auto & param : params) {
201 if (signature == param) new_param =
false;
204 params.push_back(signature);
205 paramtypes[signature] =
core::pp(varparam.sort());
218 for (
const std::string& signature: params) {
235 std::string varname = std::string(propvar.
name());
245 for(
const auto & value : values)
255 if (param != param_expr)
260 if (param_it != params.
end())
305 throw(std::runtime_error(
"Unexpected expression: " +
pbes_system::pp(e)));
311 std::vector<pbes_expression> result;
312 std::vector<pbes_expression> parts;
323 }
else if (
is_or(e)) {
329 bool pass_through =
true;
331 for(std::vector<pbes_expression>::iterator p_it = parts.begin(); pass_through && p_it != parts.end(); ++p_it)
344 std::string varname = std::string(propvar.
name());
349 if ((priority == current_priority) &&
351 vars_stack.find(varname) == vars_stack.end())
361 std::set<std::string> new_vars_stack(vars_stack.begin(), vars_stack.end());
362 new_vars_stack.insert(varname);
364 result.insert(result.end(), part_result.begin(), part_result.end());
368 result.push_back(part);
373 pass_through =
false;
378 pass_through =
false;
411 std::string name =
"true";
451 std::string variable_name = eqn.variable().name();
452 this->
variables[variable_name] = eqn.variable();
456 if (eqn.symbol() != symbol) {
458 symbol = eqn.symbol();
460 mCRL2log(
log::debug) <<
"Adding var " << variable_name <<
", priority=" << priority <<
", symbol=" << symbol << std::endl;
470 std::set<std::string> variable_set;
473 std::queue<std::string> variable_queue;
474 variable_queue.push(
init.name());
475 variable_set.insert(
init.name());
476 while (!variable_queue.empty())
478 std::string var = variable_queue.
front();
479 variable_queue.pop();
483 std::set<std::string> vars_stack;
485 for (std::vector<pbes_expression>::const_iterator e =
486 expression_parts.begin(); e != expression_parts.end(); ++e) {
488 for (
const auto & var_str : variable_set)
490 occ_vars.erase(var_str);
492 for(
const auto & occ_var : occ_vars)
494 variable_queue.push(occ_var);
496 variable_set.insert(occ_vars.begin(), occ_vars.end());
500 for (
const auto & var_str : variable_set)
508 std::string variable_name = eqn.variable().name();
509 if (variable_set.find(variable_name) != variable_set.end())
514 std::set<std::string> vars_stack;
515 mCRL2log(
log::debug) << std::endl <<
"Generating groups for equation " << variable_name << std::endl;
517 for (std::vector<pbes_expression>::const_iterator e =
518 expression_parts.begin(); e != expression_parts.end(); ++e) {
541 std::vector<bool> dep_row;
542 std::vector<bool> read_row;
543 std::vector<bool> write_row;
547 dep_row.push_back(d);
548 read_row.push_back(r);
549 write_row.push_back(w);
555 dep_row.push_back(d);
556 read_row.push_back(r);
557 write_row.push_back(w);
688 if (group==0 || group==1)
return false;
690 mCRL2log(
log::debug) <<
"is_read_dependent_parameter (group=" << group <<
", part=" << part <<
" [" <<
p <<
"]" << std::endl;
694 if (params.find(
p) == params.end())
700 std::set<std::string> usedSet =
used(phi);
701 std::set<std::string> changedSet =
changed(phi);
702 std::set<std::string> copySet =
copied(phi);
703 std::set<std::string> changedAndCopied;
704 std::set_intersection(changedSet.begin(), changedSet.end(), copySet.begin(), copySet.end(),
705 std::inserter(changedAndCopied, changedAndCopied.end()));
707 if (usedSet.find(
p) == usedSet.end() && changedAndCopied.find(
p) == changedAndCopied.end())
723 if (group==0 || group==1)
return false;
735 else if (
occ.size() == 1)
737 bool containsX =
occ.find(X) !=
occ.end();
749 if (group==0 || group==1)
return false;
760 std::set<std::string> resetSet =
reset(phi, params);
761 if (resetSet.find(
p) != resetSet.end())
766 std::set<std::string> changedSet =
changed(phi);
767 bool changedSetContainsP = (changedSet.find(
p) != changedSet.end());
768 return changedSetContainsP;
774 std::set<std::string> empty;
781 std::set<std::string> result;
789 result.insert(l.begin(), l.end());
791 result.insert(r.begin(), r.end());
795 std::set<std::string> LL;
796 LL.insert(L.begin(), L.end());
806 std::vector<std::string> var_param_signatures =
809 assert(var_param_signatures.size() == values.
size());
811 for (std::vector<std::string>::const_iterator param =
812 var_param_signatures.
begin(); param != var_param_signatures.
end(); ++param) {
813 std::string param_signature = *param;
816 const variable& value = atermpp::down_cast<variable>(*val);
818 if (param_signature != value_signature || L.find(value_signature) != L.end())
820 result.insert(param_signature);
825 result.insert(param_signature);
827 if (val != values.
end()) {
838 std::set<std::string> result;
846 result.insert(l.begin(), l.end());
848 result.insert(r.begin(), r.end());
856 std::set<std::string> params;
857 std::vector<std::string> var_params =
859 for (std::vector<std::string>::const_iterator param =
860 var_params.
begin(); param != var_params.
end(); ++param) {
861 std::string signature = *param;
862 params.insert(signature);
864 for (
auto signature : d) {
865 if (params.find(signature) == params.end())
867 result.insert(signature);
899 std::set<std::string> result;
902 result.insert(atermpp::down_cast<propositional_variable_instantiation>(expr).name());
907 result.insert(l.begin(), l.end());
909 result.insert(r.begin(), r.end());
921 std::set<std::string> result;
932 std::set<std::string> emptySet;
933 return used(expr, emptySet);
940 std::set<std::string> result;
943 std::set<std::string> fv =
free(expr);
944 result.insert(fv.begin(), fv.end());
949 variable_parameters[atermpp::down_cast<propositional_variable_instantiation>(expr).name()];
951 assert(var_params.
size() == values.
size());
953 for (
auto parameter : var_params) {
957 const variable& value = atermpp::down_cast<variable>(*val);
959 if (param_signature != value_signature || L.find(value_signature) != L.end())
961 result.insert(value_signature);
967 std::set<std::string> l =
used(*val, L);
968 result.insert(l.begin(), l.end());
970 if (val != values.
end()) {
978 result.insert(l.begin(), l.end());
980 result.insert(r.begin(), r.end());
988 std::set<std::string> LL;
989 LL.insert(L.begin(), L.end());
1003 std::set<std::string> emptySet;
1004 return copied(expr, emptySet);
1011 std::set<std::string> result;
1019 variable_parameters[atermpp::down_cast<propositional_variable_instantiation>(expr).name()];
1021 assert(var_params.
size() == values.
size());
1023 for (
auto parameter : var_params) {
1027 const variable& value = atermpp::down_cast<variable>(*val);
1029 if (param_signature == value_signature && L.find(value_signature) == L.end())
1031 result.insert(value_signature);
1034 if (val != values.
end()) {
1042 result.insert(l.begin(), l.end());
1044 result.insert(r.begin(), r.end());
1052 std::set<std::string> LL;
1053 LL.insert(L.begin(), L.end());
1069 std::stringstream ss;
1072 ss <<
":" << state.get_variable();
1074 const std::vector<data_expression>& param_values = state.get_parameter_values();
1075 std::vector<std::string> param_signatures =
1077 std::vector<std::string>::const_iterator param_signature =
1078 param_signatures.begin();
1079 for (std::vector<data_expression>::const_iterator param_value =
1080 param_values.begin(); param_value != param_values.end(); ++param_value) {
1081 if (param_value != param_values.begin())
1083 ss << *param_signature <<
" = ";
1085 if (param_signature != param_signatures.end())
1098 std::set<std::string> result;
1099 for (
auto parameter : params) {
1108 std::vector<std::string> result;
1109 for (
auto parameter : params) {
1118 std::vector<int> result;
1119 for (
auto parameter : params) {
1121 result.push_back(index);
1129 std::map<int,int> result;
1131 for (
auto parameter : params) {
1133 result.insert(std::make_pair(index,i));
1148 std::string paramname = param.name();
1149 std::string paramtype =
core::pp(param.sort());
1159 const std::string& paramtype)
1161 return paramname +
":" + paramtype;
1171 this->
var = varname;
1180 this->
var = varname;
1182 assert(std::string(atermpp::down_cast<propositional_variable_instantiation>(e).name()) == varname);
1185 for (
const auto & value : values)
1187 if (value == novalue)
1189 throw(std::runtime_error(
"Error in ltsmin_state: state expression contains NoValue: "
1197 throw(std::runtime_error(
"Not a valid state expression! " +
pp(e)));
1203 if (this->
var < other.
var)
return true;
1204 else if (this->
var == other.
var)
1218 return this->
var==other.
var
1246 parameter_values.push_back(param_value);
1259 std::stringstream ss;
1262 ss <<
"[" << std::endl;
1263 for (std::vector<data_expression>::const_iterator entry =
1266 ss << std::endl <<
" value = ";
1279explorer::explorer(
const std::string& filename,
const std::string& rewrite_strategy =
"jittyc",
bool reset_flag =
false,
bool always_split_flag =
false)
1283 std::string variable_name = eqn.variable().name();
1296 for (std::size_t i = 0; i <
info->
get_lts_type().get_number_of_state_types(); ++i) {
1297 std::map<data_expression,int> data2int_map;
1299 std::vector<data_expression> int2data_map;
1306explorer::explorer(
const pbes& p_,
const std::string& rewrite_strategy =
"jittyc",
bool reset_flag =
false,
bool always_split_flag =
false)
1312 for (std::size_t i = 0; i <
info->
get_lts_type().get_number_of_state_types(); i++) {
1313 std::map<data_expression,int> data2int_map;
1315 std::vector<data_expression> int2data_map;
1356 std::string varname = expr.
name();
1419 std::map<data_expression,int>::iterator it = data2int_map.find(value);
1421 if (it != data2int_map.end()) {
1426 data2int_map.insert(std::make_pair(value,index));
1441 std::string src_varname;
1442 bool same_var =
false;
1443 if (!(src==
nullptr)) {
1445 same_var = (varname==src_varname);
1458 std::vector < data_expression > values(state_length);
1462 for (
int i = 1; i < state_length; i++) {
1464 values[i] = default_value;
1469 for (
int i = 1; i < state_length; i++) {
1475 std::vector<int> parameter_indices =
1477 std::vector<std::string> parameter_signatures =
1479 std::vector<std::string>::iterator param_signature = parameter_signatures.begin();
1480 int value_index = 0;
1481 for(
int & parameter_indice : parameter_indices)
1483 int i = parameter_indice + 1;
1485 values[i] = parameter_values[value_index];
1486 if (values[i]==novalue)
1499 std::map<int,int>::iterator src_param_index_position_it = src_param_index_positions.find(parameter_indice);
1500 if ( src_param_index_position_it != src_param_index_positions.end()
1512 if (param_signature != parameter_signatures.end())
1520 throw(std::runtime_error(
"Error in to_state_vector: NoValue in parameters of dst_state: "
1551 throw(std::runtime_error(
"Error in get_string_value: Value not found for index " + std::to_string(index) +
"."));
1560 if (index >= (
int)(int2data_map.size()))
1562 throw(std::runtime_error(
"Error in get_data_value: Value not found for type_no "
1563 + std::to_string(type_no) +
" at index " + std::to_string(index) +
"."));
1565 return int2data_map.at(index);
1581 std::vector <data_expression> values(state_length);
1584 for (
int i = 1; i < state_length; i++) {
1592 std::vector<int> parameter_indices =
1594 for (
int & parameter_indice : parameter_indices) {
1595 if (values[parameter_indice+1]==novalue)
1600 parameters.push_back(values[parameter_indice+1]);
1604 throw(std::runtime_error(
"Error in from_state_vector: NoValue in parameters."));
1618 std::vector<ltsmin_state> result;
1622 if (state.get_variable()==
"true")
1625 result.push_back(state);
1627 else if (state.get_variable()==
"false")
1630 result.push_back(state);
1634 std::set<pbes_expression> successors
1637 for (
const auto & successor : successors) {
1639 result.push_back(
get_state(atermpp::down_cast<propositional_variable_instantiation>(successor)));
1640 }
else if (
is_true(successor)) {
1651 throw(std::runtime_error(
"!! Successor is NOT a propvar: " +
pbes_system::pp(successor)));
1663 std::vector<ltsmin_state> result;
1665 if (group == 0 && state.get_variable()==
"true")
1668 result.push_back(state);
1670 else if (group == 1 && state.get_variable()==
"false")
1673 result.push_back(state);
1677 std::string varname = state.get_variable();
1679 if (varname==group_varname)
1682 std::set<pbes_expression> successors
1686 for (
const auto & successor : successors) {
1689 result.push_back(
get_state(atermpp::down_cast<propositional_variable_instantiation>(successor)));
1690 }
else if (
is_true(successor)) {
1701 throw(std::runtime_error(
"!! Successor is NOT a propvar: " +
pbes_system::pp(successor)));
Term containing a string.
size_type size() const
Returns the size of the term_list.
const_iterator end() const
Returns a const_iterator pointing to the end of the term_list.
const Term & front() const
Returns the first element of the list.
const_iterator begin() const
Returns a const_iterator pointing to the beginning of the term_list.
Components for generating an arbitrary element of a sort.
std::set< pbes_expression > get_successors(const pbes_expression &phi)
Returns the successors of a state, which is a instantiated propositional variable....
pbes_equation get_pbes_equation(const core::identifier_string &s)
Returns the equation for variable s.
propositional_variable_instantiation get_initial_state()
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.
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< std::vector< data_expression > > localmaps_int2data
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
std::vector< std::map< data_expression, int > > localmaps_data2int
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
void initial_state(int *state)
static fixpoint_symbol nu()
Returns the nu symbol.
static fixpoint_symbol mu()
Returns the mu symbol.
bool is_write_dependent_propvar(int group)
Determines if group is write dependent on the propositional variable. Returns true if propositional v...
const std::map< std::string, std::map< int, int > > & get_variable_parameter_index_positions() const
Returns the map from variable names to the map from indices of parameter signatures for the variable ...
std::map< std::string, int > variable_priority
const std::map< int, std::vector< bool > > & get_read_matrix() const
Returns the read dependency matrix.
const std::map< int, std::vector< bool > > & get_write_matrix() const
Returns the write dependency matrix.
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, std::vector< std::string > > & get_variable_parameter_signatures() const
Returns the map from variable names to the list of parameters signatures 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::map< std::string, std::vector< std::string > > variable_parameter_signatures
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::map< int, std::vector< bool > > read_matrix
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::map< int, std::vector< bool > > & get_dependency_matrix() const
Returns the dependency matrix.
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)
Computes the free variables actually used, not only passed through, in an expression.
std::map< std::string, std::map< int, int > > variable_parameter_index_positions
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::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::map< int, std::vector< bool > > matrix
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::set< std::string > free(const pbes_expression &expr)
Computes the free variables read in an expression.
std::vector< pbes_expression > transition_expression_plain
std::map< int, std::vector< bool > > write_matrix
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.
std::map< std::string, std::vector< int > > variable_parameter_indices
void compute_transition_groups()
Computes transition groups from PBES.
const std::map< std::string, std::vector< int > > & get_variable_parameter_indices() const
Returns the map from variable names to the list of indices of the parameters signatures for the varia...
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 the player or type of the state (And/Or, Abelard/Eloise, Odd/Even).
bool operator<(const ltsmin_state &other) const
Compares two PBES_State objects. Uses lexicographical ordering on priority, type, variable and parame...
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 the priority for the state, which depends on the fixpoint operator of the equation of the pro...
const std::vector< data_expression > & get_parameter_values() const
Returns the list of parameter values.
virtual operation_type get_expression_operation(const pbes_expression &phi)
Returns the vertex type.
operation_type
The operation type of the vertices.
parameterized boolean equation system
const data::data_specification & data() const
Returns the data specification.
const propositional_variable_instantiation & initial_state() const
Returns the initial state.
const std::vector< pbes_equation > & equations() const
Returns the equations.
\brief A propositional variable instantiation
const core::identifier_string & name() const
\brief A propositional variable declaration
const data::variable_list & parameters() const
const core::identifier_string & name() const
Standard exception class for reporting runtime errors.
add your file description here.
MCRL2_EXPORT bool init(rewriter_interface *i, RewriterCompilingJitty *this_rewriter)
#define mCRL2log(LEVEL)
mCRL2log(LEVEL) provides the stream used to log.
aterm read_term_from_string(const std::string &s)
Reads an aterm from a string. The string can be in either binary or text format.
bool check_term_PropVarInst(const Term &t)
std::string pp(const identifier_string &x)
atermpp::aterm_string identifier_string
String type of the LPS library. Identifier strings are represented internally as ATerms.
atermpp::aterm add_index(const atermpp::aterm &x)
atermpp::aterm remove_index(const atermpp::aterm &x)
std::vector< data_expression > data_expression_vector
\brief vector of data_expressions
std::string pp(const abstraction &x)
atermpp::term_list< variable > variable_list
\brief list of variables
rewrite_strategy parse_rewrite_strategy(const std::string &s)
standard conversion from string to rewrite strategy
bool is_variable(const atermpp::aterm &x)
Returns true if the term t is a variable.
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.
void normalize(pbes &x)
The function normalize brings (embedded) pbes expressions into positive normal form,...
pbes to_ppg(pbes x)
Rewrites a PBES to a PPG.
bool is_ppg(const T &x)
Determines if an expression is a PPG expression.
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)
void load_pbes(pbes &pbes, std::istream &stream, utilities::file_format format, const std::string &source="")
Load a PBES from file.
bool is_exists(const atermpp::aterm &x)
void find_free_variables(const T &x, OutputIterator o)
bool is_or(const atermpp::aterm &x)
const data::variable_list & quantifier_variables(const pbes_expression &x)
bool is_forall(const atermpp::aterm &x)
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 || ....
pbes_expression formula(std::set< identifier_t > const &v, const owner_t owner, const std::string &prefix="X")
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)
std::string pp(const fixpoint_symbol &x)
bool is_and(const atermpp::aterm &x)
bool is_imp(const atermpp::aterm &x)
bool is_simple_expression(const T &x)
Determines if an expression is a simple expression. An expression is simple if it is free of proposit...
bool is_true(const pbes_expression &t)
Test for the value true.
const pbes_expression & false_()
T && return_std_move(T &t)
This is a workaround for the return by value diagnostic (clang -Wreturn-std-move)....
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
IO routines for boolean equation systems.
Visitor class for Parameterised Parity Games (PPG), PBES expressions of the form: PPG :== /_{i: I} f_...
Component for generating representatives of sorts.