mCRL2
Loading...
Searching...
No Matches
lps_algorithm.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//
11
12#ifndef MCRL2_LPS_DETAIL_LPS_ALGORITHM_H
13#define MCRL2_LPS_DETAIL_LPS_ALGORITHM_H
14
15#include "mcrl2/data/rewriter.h"
17#include "mcrl2/lps/rewrite.h"
18
19namespace mcrl2
20{
21
22namespace lps
23{
24
25namespace detail
26{
27
30template <typename Specification = specification>
32{
33 protected:
35 Specification& m_spec;
36
37 void sumelm_find_variables(const action_summand& s, std::set<data::variable>& result) const
38 {
39 std::set<data::variable> tmp;
40
42 result.insert(tmp.begin(), tmp.end());
43
45 result.insert(tmp.begin(), tmp.end());
46
48 result.insert(tmp.begin(), tmp.end());
49 }
50
51 void sumelm_find_variables(const deadlock_summand& s, std::set<data::variable>& result) const
52 {
53 std::set<data::variable> tmp;
54
56 result.insert(tmp.begin(), tmp.end());
57
59 result.insert(tmp.begin(), tmp.end());
60 }
61
62 template <typename SummandType>
63 void summand_remove_unused_summand_variables(SummandType& summand_)
64 {
65 data::variable_vector new_summation_variables;
66
67 std::set<data::variable> occurring_vars;
68 sumelm_find_variables(summand_, occurring_vars);
69
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()));
74
75 summand_.summation_variables() = data::variable_list(new_summation_variables.begin(),new_summation_variables.end());
76 }
77
78 public:
80 lps_algorithm(Specification& spec)
81 : m_spec(spec)
82 {}
83
85 bool verbose() const
86 {
87 return mCRL2logEnabled(log::verbose);
88 }
89
92 {
93 for (const data::assignment& a: s.assignments())
94 {
95 if (a.lhs() == v)
96 {
97 return a.rhs();
98 }
99 }
100 return v; // no assignment to v found, so return v itself
101 }
102
107 {
109 }
110
112 void remove_parameters(const std::set<data::variable>& to_be_removed)
113 {
114 lps::remove_parameters(m_spec, to_be_removed);
115 }
116
119 {
121 }
122
125 {
127 }
128
131 {
132 auto& v = m_spec.process().action_summands();
133 std::for_each(v.begin(),
134 v.end(),
135 [this](action_summand& s){lps_algorithm::summand_remove_unused_summand_variables<typename Specification::process_type::action_summand_type>(s); });
136
137 auto& w = m_spec.process().deadlock_summands();
138 std::for_each(w.begin(),
139 w.end(),
140 [this](deadlock_summand& s){lps_algorithm::summand_remove_unused_summand_variables<deadlock_summand>(s); });
141 }
142};
143
144} // namespace detail
145
146} // namespace lps
147
148} // namespace mcrl2
149
150#endif // MCRL2_LPS_DETAIL_LPS_ALGORITHM_H
\brief Assignment of a data expression to a variable
Definition assignment.h:91
\brief A data variable
Definition variable.h:28
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.
Definition summand.h:60
The class rewriter.
add your file description here.
add your file description here.
std::vector< variable > variable_vector
\brief vector of variables
Definition variable.h:89
std::set< data::variable > find_free_variables(const data::data_expression &x)
Definition data.cpp:99
atermpp::term_list< variable > variable_list
\brief list of variables
@ verbose
Definition logger.h:37
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.
Definition remove.h:190
std::set< data::variable > find_free_variables(const lps::deadlock &x)
Definition lps.cpp:54
void remove_singleton_sorts(Specification &spec)
Removes parameters with a singleton sort from a linear process specification.
Definition remove.h:211
void remove_trivial_summands(Specification &spec)
Removes summands with condition equal to false from a linear process specification.
Definition remove.h:199
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72