12#ifndef MCRL2_LPS_DETAIL_LPS_ALGORITHM_H
13#define MCRL2_LPS_DETAIL_LPS_ALGORITHM_H
30template <
typename Specification = specification>
39 std::set<data::variable> tmp;
42 result.insert(tmp.begin(), tmp.end());
45 result.insert(tmp.begin(), tmp.end());
48 result.insert(tmp.begin(), tmp.end());
53 std::set<data::variable> tmp;
56 result.insert(tmp.begin(), tmp.end());
59 result.insert(tmp.begin(), tmp.end());
62 template <
typename SummandType>
67 std::set<data::variable> occurring_vars;
70 std::set<data::variable> summation_variables(summand_.summation_variables().begin(),summand_.summation_variables().end());
71 std::set_intersection(summation_variables.begin(), summation_variables.end(),
72 occurring_vars.begin(), occurring_vars.end(),
73 std::inserter(new_summation_variables, new_summation_variables.end()));
75 summand_.summation_variables() =
data::variable_list(new_summation_variables.begin(),new_summation_variables.end());
132 auto& v =
m_spec.process().action_summands();
133 std::for_each(v.begin(),
135 [
this](
action_summand& s){lps_algorithm::summand_remove_unused_summand_variables<typename Specification::process_type::action_summand_type>(s); });
137 auto& w =
m_spec.process().deadlock_summands();
138 std::for_each(w.begin(),
140 [
this](
deadlock_summand& s){lps_algorithm::summand_remove_unused_summand_variables<deadlock_summand>(s); });
\brief Assignment of a data expression to a variable
LPS summand containing a multi-action.
const lps::multi_action & multi_action() const
Returns the multi-action of this summand.
const data::assignment_list & assignments() const
Returns the sequence of assignments.
LPS summand containing a deadlock.
const lps::deadlock & deadlock() const
Returns the deadlock of this summand.
Algorithm class for algorithms on linear process specifications. It can be instantiated with lps::spe...
void remove_parameters(const std::set< data::variable > &to_be_removed)
Removes formal parameters from the specification.
void remove_unused_summand_variables()
Removes unused summand variables.
void sumelm_find_variables(const action_summand &s, std::set< data::variable > &result) const
void summand_remove_unused_summand_variables(SummandType &summand_)
void sumelm_find_variables(const deadlock_summand &s, std::set< data::variable > &result) const
data::data_expression next_state(const action_summand &s, const data::variable &v) const
Applies the next state substitution to the variable v.
bool verbose() const
Flag for verbose output.
void remove_singleton_sorts()
Removes parameters with a singleton sort.
void remove_trivial_summands()
Removes summands with condition equal to false.
void instantiate_free_variables()
Attempts to eliminate the free variables of the specification, by substituting a constant value for t...
lps_algorithm(Specification &spec)
Constructor.
Specification & m_spec
The specification that is processed by the algorithm.
const data::data_expression & condition() const
Returns the condition expression.
add your file description here.
add your file description here.
std::vector< variable > variable_vector
\brief vector of variables
std::set< data::variable > find_free_variables(const data::data_expression &x)
atermpp::term_list< variable > variable_list
\brief list of variables
data::mutable_map_substitution instantiate_global_variables(Specification &lpsspec)
Eliminates the global variables of an LPS, by substituting a constant value for them....
void remove_parameters(Object &x, const std::set< data::variable > &to_be_removed)
Rewrites an LPS data type.
std::set< data::variable > find_free_variables(const lps::deadlock &x)
void remove_singleton_sorts(Specification &spec)
Removes parameters with a singleton sort from a linear process specification.
void remove_trivial_summands(Specification &spec)
Removes summands with condition equal to false from a linear process specification.
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...