Line data Source code
1 : // Author(s): Jeroen Keiren
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 suminst.h
10 : /// \brief Instantiate summation variables.
11 :
12 : #ifndef MCRL2_LPS_SUMINST_H
13 : #define MCRL2_LPS_SUMINST_H
14 :
15 : #include "mcrl2/atermpp/set_operations.h"
16 :
17 : #include "mcrl2/data/enumerator.h"
18 :
19 : #include "mcrl2/lps/detail/lps_algorithm.h"
20 :
21 : namespace mcrl2
22 : {
23 : namespace lps
24 : {
25 :
26 : /// \brief Return a set with all finite sorts in data specification s.
27 : inline
28 5 : std::set<data::sort_expression> finite_sorts(const data::data_specification& s)
29 : {
30 5 : const std::set<data::sort_expression>& sorts = s.sorts();
31 5 : std::set<data::sort_expression> result;
32 :
33 44 : for(const data::sort_expression& sort : sorts)
34 : {
35 39 : if(s.is_certainly_finite(sort))
36 : {
37 11 : result.insert(sort);
38 : }
39 : }
40 5 : return result;
41 0 : }
42 :
43 : template<typename DataRewriter, typename Specification>
44 : class suminst_algorithm: public detail::lps_algorithm<Specification>
45 : {
46 : typedef detail::lps_algorithm<Specification> super;
47 : typedef data::enumerator_list_element_with_substitution<> enumerator_element;
48 : typedef typename Specification::process_type process_type;
49 : typedef typename process_type::action_summand_type action_summand_type;
50 : typedef std::vector<action_summand_type> action_summand_vector_type;
51 : using super::m_spec;
52 :
53 : protected:
54 : /// Sorts to be instantiated
55 : std::set<data::sort_expression> m_sorts;
56 :
57 : /// Only instantiate tau summands
58 : bool m_tau_summands_only;
59 :
60 : /// Rewriter
61 : DataRewriter m_rewriter;
62 : data::enumerator_algorithm<> m_enumerator;
63 : data::enumerator_identifier_generator m_id_generator;
64 :
65 : /// Statistiscs for verbose output
66 : std::size_t m_processed;
67 : std::size_t m_deleted;
68 : std::size_t m_added;
69 :
70 : template <typename SummandType, typename Container>
71 9 : std::size_t instantiate_summand(const SummandType& s, Container& result)
72 : {
73 : using namespace data;
74 9 : std::size_t nr_summands = 0; // Counter for the number of new summands, used for verbose output
75 9 : std::deque< variable > variables; // The variables we need to consider in instantiating
76 :
77 : // partition such that variables with finite sort precede those that do not
78 25 : for (const variable& v: s.summation_variables())
79 : {
80 7 : if(m_sorts.find(v.sort()) != m_sorts.end())
81 : {
82 6 : if (m_spec.data().is_certainly_finite(v.sort()))
83 : {
84 5 : variables.push_front(v);
85 : }
86 : else
87 : {
88 1 : variables.push_back(v);
89 : }
90 : }
91 : }
92 :
93 9 : if (variables.empty())
94 : {
95 : // Nothing to be done, return original summand
96 3 : result.push_back(s);
97 3 : nr_summands = 1;
98 : }
99 : else
100 : {
101 : // List of variables with the instantiated variables removed (can be done upfront, which is more efficient,
102 : // because we only need to calculate it once.
103 6 : const variable_list vl(variables.begin(),variables.end());
104 6 : variable_list new_summation_variables = term_list_difference(s.summation_variables(), vl);
105 :
106 : try
107 : {
108 6 : mCRL2log(log::debug) << "enumerating variables " << vl << " in condition: " << data::pp(s.condition()) << std::endl;
109 6 : data::mutable_indexed_substitution<> local_sigma;
110 6 : m_enumerator.enumerate(enumerator_element(vl, s.condition()),
111 : local_sigma,
112 98 : [&](const enumerator_element& p)
113 : {
114 14 : mutable_indexed_substitution<> sigma;
115 14 : p.add_assignments(vl, sigma, m_rewriter);
116 14 : mCRL2log(log::debug) << "substitutions: " << sigma << std::endl;
117 14 : SummandType t(s);
118 14 : t.summation_variables() = new_summation_variables;
119 14 : lps::rewrite(t, m_rewriter, sigma);
120 14 : result.push_back(t);
121 14 : ++nr_summands;
122 14 : return false;
123 14 : },
124 : sort_bool::is_false_function_symbol
125 : );
126 6 : }
127 0 : catch (mcrl2::runtime_error const& e)
128 : {
129 : // If an error occurs in enumerating, remove all summands that
130 : // have been added to result thus far, and re-add the original.
131 : // This prevents problems e.g. in case of a sort without constructors.
132 0 : mCRL2log(log::debug) << "An error occurred in enumeration, removing already added summands, and keeping the original" << std::endl;
133 0 : mCRL2log(log::debug) << e.what() << std::endl;
134 :
135 0 : result.resize(result.size() - nr_summands);
136 0 : result.push_back(s);
137 0 : nr_summands = 1;
138 : }
139 6 : }
140 9 : return nr_summands;
141 9 : }
142 :
143 8 : bool must_instantiate(const action_summand_type& summand)
144 : {
145 8 : return !m_tau_summands_only || summand.is_tau();
146 : }
147 :
148 2 : bool must_instantiate(const deadlock_summand& )
149 : {
150 2 : return !m_tau_summands_only;
151 : }
152 :
153 : template <typename SummandListType, typename Container>
154 12 : void run(const SummandListType& list, Container& result)
155 : {
156 22 : for (typename SummandListType::const_iterator i = list.begin(); i != list.end(); ++i)
157 : {
158 10 : if (must_instantiate(*i))
159 : {
160 9 : std::size_t newsummands = instantiate_summand(*i, result);
161 9 : if (newsummands > 0)
162 : {
163 9 : m_added += newsummands - 1;
164 : }
165 : else
166 : {
167 0 : ++m_deleted;
168 : }
169 : }
170 : else
171 : {
172 1 : result.push_back(*i);
173 : }
174 10 : ++m_processed;
175 10 : mCRL2log(log::status) << "Replaced " << m_processed << " summands by " << (m_processed + m_added - m_deleted)
176 0 : << " summands (" << m_deleted << " were deleted)" << std::endl;
177 : }
178 12 : }
179 :
180 : public:
181 6 : suminst_algorithm(Specification& spec,
182 : DataRewriter& r,
183 : std::set<data::sort_expression> sorts = std::set<data::sort_expression>(),
184 : bool tau_summands_only = false)
185 : : detail::lps_algorithm<Specification>(spec),
186 6 : m_sorts(sorts),
187 6 : m_tau_summands_only(tau_summands_only),
188 6 : m_rewriter(r),
189 6 : m_enumerator(r, spec.data(), r, m_id_generator, false),
190 6 : m_processed(0),
191 6 : m_deleted(0),
192 12 : m_added(0)
193 : {
194 6 : if(sorts.empty())
195 : {
196 4 : mCRL2log(log::info) << "an empty set of sorts to be unfolded was provided; defaulting to all finite sorts" << std::endl;
197 4 : m_sorts = finite_sorts(spec.data());
198 : }
199 6 : }
200 :
201 6 : void run()
202 : {
203 6 : action_summand_vector_type action_summands;
204 6 : deadlock_summand_vector deadlock_summands;
205 6 : m_added = 0;
206 6 : m_deleted = 0;
207 6 : m_processed = 0;
208 6 : run(m_spec.process().action_summands(), action_summands);
209 6 : run(m_spec.process().deadlock_summands(), deadlock_summands);
210 6 : m_spec.process().action_summands().swap(action_summands);
211 6 : m_spec.process().deadlock_summands().swap(deadlock_summands);
212 6 : mCRL2log(log::status) << std::endl;
213 6 : }
214 :
215 : }; // suminst_algorithm
216 :
217 : } // namespace lps
218 : } // namespace mcrl2
219 :
220 : #endif // MCRL2_LPS_SUMINST_H
221 :
|
