Line data Source code
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 : //
9 : /// \file enumerator_test.cpp
10 : /// \brief Add your file description here.
11 :
12 : #define BOOST_TEST_MODULE enumerator_test
13 : #include <boost/test/included/unit_test.hpp>
14 :
15 : #include "mcrl2/data/substitutions/mutable_map_substitution.h"
16 : #include "mcrl2/data/enumerator_with_iterator.h"
17 : #include "mcrl2/pbes/enumerator.h"
18 : #include "mcrl2/pbes/detail/parse.h"
19 : #include "mcrl2/pbes/rewriters/simplify_rewriter.h"
20 :
21 : using namespace mcrl2;
22 : using namespace mcrl2::pbes_system;
23 :
24 : const std::string VARSPEC =
25 : "datavar \n"
26 : " m: Nat; \n"
27 : " n: Nat; \n"
28 : " b: Bool; \n"
29 : " c: Bool; \n"
30 : " \n"
31 : "predvar \n"
32 : " X: Bool, Pos; \n"
33 : " Y: Nat; \n"
34 : ;
35 :
36 2 : BOOST_AUTO_TEST_CASE(test_enumerator)
37 : {
38 : typedef pbes_system::simplify_data_rewriter<data::rewriter> pbes_rewriter;
39 : typedef data::enumerator_list_element<pbes_expression> enumerator_element;
40 :
41 1 : data::data_specification data_spec;
42 1 : data_spec.add_context_sort(data::sort_nat::nat());
43 1 : data::rewriter datar(data_spec);
44 1 : pbes_rewriter R(datar);
45 :
46 1 : data::variable_list v;
47 1 : v.push_front(data::variable("n", data::sort_nat::nat()));
48 2 : pbes_expression phi = parse_pbes_expression("val(n < 2)", VARSPEC);
49 1 : data::mutable_indexed_substitution<> sigma;
50 2 : data::enumerator_identifier_generator id_generator("x");
51 1 : bool accept_solutions_with_variables = true;
52 1 : data::enumerator_algorithm<pbes_rewriter> E(R, data_spec, datar, id_generator, accept_solutions_with_variables);
53 1 : std::set<pbes_system::pbes_expression> solutions;
54 1 : E.enumerate(enumerator_element(v, phi),
55 : sigma,
56 2 : [&](const enumerator_element& p)
57 : {
58 2 : solutions.insert(p.expression());
59 2 : return false; // do not interrupt
60 : },
61 : is_false
62 : );
63 1 : std::clog << "solutions = " << core::detail::print_list(solutions) << std::endl;
64 1 : BOOST_CHECK(solutions.size() == 1);
65 1 : }
66 :
67 2 : BOOST_AUTO_TEST_CASE(test_enumerator_with_iterator)
68 : {
69 : typedef pbes_system::simplify_data_rewriter<data::rewriter> pbes_rewriter;
70 : typedef data::enumerator_list_element<pbes_expression> enumerator_element;
71 :
72 1 : data::data_specification data_spec;
73 1 : data_spec.add_context_sort(data::sort_nat::nat());
74 1 : data::rewriter datar(data_spec);
75 1 : pbes_rewriter R(datar);
76 :
77 1 : data::variable_list v;
78 1 : v.push_front(data::variable("n", data::sort_nat::nat()));
79 2 : pbes_expression phi = parse_pbes_expression("val(n < 2)", VARSPEC);
80 1 : data::mutable_indexed_substitution<> sigma;
81 2 : data::enumerator_identifier_generator id_generator;
82 1 : data::enumerator_algorithm_with_iterator<pbes_rewriter, enumerator_element, pbes_system::is_not_true> E(R, data_spec, datar, id_generator, 20);
83 1 : std::vector<pbes_system::pbes_expression> solutions;
84 :
85 1 : data::enumerator_queue<enumerator_element> P;
86 1 : P.push_back(enumerator_element(v, phi));
87 5 : for (auto i = E.begin(sigma, P); i != E.end(); ++i)
88 : {
89 4 : solutions.push_back(i->expression());
90 : }
91 1 : std::clog << "solutions = " << core::detail::print_list(solutions) << std::endl;
92 1 : BOOST_CHECK(solutions.size() >= 1);
93 1 : }
94 :
95 2 : BOOST_AUTO_TEST_CASE(test_enumerator_with_substitutions)
96 : {
97 : typedef pbes_system::simplify_data_rewriter<data::rewriter> pbes_rewriter;
98 : typedef data::enumerator_list_element_with_substitution<pbes_expression> enumerator_element;
99 :
100 1 : data::data_specification data_spec;
101 1 : data_spec.add_context_sort(data::sort_nat::nat());
102 1 : data::rewriter datar(data_spec);
103 1 : pbes_rewriter R(datar);
104 :
105 1 : data::variable_list v;
106 1 : v.push_front(data::variable("n", data::sort_nat::nat()));
107 2 : pbes_expression phi = parse_pbes_expression("val(n < 2)", VARSPEC);
108 1 : data::mutable_indexed_substitution<> sigma;
109 2 : data::enumerator_identifier_generator id_generator;
110 1 : data::enumerator_algorithm_with_iterator<pbes_rewriter, enumerator_element, pbes_system::is_not_false> E(R, data_spec, datar, id_generator);
111 1 : std::vector<pbes_system::pbes_expression> solutions;
112 :
113 1 : data::enumerator_queue<enumerator_element> P;
114 1 : P.push_back(enumerator_element(v, phi));
115 3 : for (auto i = E.begin(sigma, P); i != E.end(); ++i)
116 : {
117 2 : solutions.push_back(i->expression());
118 2 : data::mutable_map_substitution<> sigma;
119 2 : i->add_assignments(v, sigma, datar);
120 2 : std::clog << " solutions " << i->expression() << " substitution = " << sigma << std::endl;
121 2 : BOOST_CHECK(R(phi, sigma) == i->expression());
122 2 : }
123 1 : std::clog << "solutions = " << core::detail::print_list(solutions) << std::endl;
124 1 : BOOST_CHECK(solutions.size() >= 1);
125 1 : }
126 :
127 2 : BOOST_AUTO_TEST_CASE(enumerate_callback)
128 : {
129 : typedef pbes_system::simplify_data_rewriter<data::rewriter> pbes_rewriter;
130 : typedef data::enumerator_list_element<pbes_expression> enumerator_element;
131 2 : data::enumerator_identifier_generator id_generator;
132 1 : data::data_specification dataspec;
133 1 : dataspec.add_context_sort(data::sort_int::int_());
134 1 : std::size_t max_count = 10;
135 1 : data::rewriter r(dataspec);
136 1 : pbes_rewriter R(r);
137 1 : data::enumerator_algorithm<pbes_rewriter> E(R, dataspec, r, id_generator, max_count);
138 :
139 2 : auto enumerate = [&](const pbes_expression& x)
140 : {
141 2 : data::rewriter::substitution_type sigma;
142 2 : pbes_expression result;
143 2 : id_generator.clear();
144 2 : if (is_forall(x))
145 : {
146 1 : const pbes_system::forall& x_ = atermpp::down_cast<pbes_system::forall>(x);
147 1 : result = pbes_system::true_();
148 1 : E.enumerate(enumerator_element(x_.variables(), R(x_.body())),
149 : sigma,
150 1 : [&](const enumerator_element& p)
151 : {
152 1 : data::optimized_and(result, result, p.expression());
153 1 : return is_false(result);
154 : },
155 : pbes_system::is_true,
156 : pbes_system::is_false
157 : );
158 : }
159 1 : else if (is_exists(x))
160 : {
161 1 : const pbes_system::exists& x_ = atermpp::down_cast<pbes_system::exists>(x);
162 1 : result = pbes_system::false_();
163 1 : E.enumerate(enumerator_element(x_.variables(), R(x_.body())),
164 : sigma,
165 1 : [&](const enumerator_element& p)
166 : {
167 1 : data::optimized_or(result, result, p.expression());
168 1 : return is_true(result);
169 : },
170 : pbes_system::is_false,
171 : pbes_system::is_true
172 : );
173 : }
174 4 : return result;
175 3 : };
176 :
177 1 : BOOST_CHECK_EQUAL(enumerate(parse_pbes_expression("forall n: Nat. val(n < 2)")), false_());
178 1 : BOOST_CHECK_EQUAL(enumerate(parse_pbes_expression("exists n: Nat. val(n < 2)")), true_());
179 1 : }
|
