Line data Source code
1 : // Author(s): Jan Friso Groote
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 linearization_test.cpp
10 : /// \brief A test of the linearizer, comparing the result with the expected state space modulo strong bisimulation.
11 :
12 : #define BOOST_TEST_MODULE linearization_instantiation_compare_test
13 :
14 : #include <boost/test/included/unit_test.hpp>
15 :
16 : #include "mcrl2/utilities/test_utilities.h"
17 :
18 : #include "mcrl2/data/detail/rewrite_strategies.h"
19 :
20 : #include "mcrl2/lps/linearise.h"
21 : #include "mcrl2/lts/lts_algorithm.h"
22 : #include "mcrl2/lts/state_space_generator.h"
23 : #include "mcrl2/lts/stochastic_lts_builder.h"
24 :
25 : using namespace mcrl2;
26 : using namespace mcrl2::lps;
27 :
28 : typedef data::rewriter::strategy rewrite_strategy;
29 : typedef std::vector<rewrite_strategy> rewrite_strategy_vector;
30 :
31 : template <class LTS_TYPE>
32 : inline
33 12 : LTS_TYPE translate_lps_to_lts(const lps::stochastic_specification& specification)
34 : {
35 12 : lps::explorer_options options;
36 12 : options.trace_prefix = "linearization_instantiation_compare_test";
37 12 : options.search_strategy = lps::es_breadth;
38 12 : options.save_at_end = true;
39 12 : const std::string& output_filename = utilities::temporary_filename("linearization_instantiation_compare_test_file");
40 :
41 12 : LTS_TYPE result;
42 12 : lts::state_space_generator<false, false, lps::stochastic_specification> generator(specification, options);
43 12 : lps::specification lpsspec = lps::remove_stochastic_operators(specification);
44 24 : auto builder = create_lts_builder(lpsspec, options, result.type());
45 12 : generator.explore(*builder);
46 12 : builder->save(output_filename);
47 :
48 12 : result.load(output_filename);
49 24 : return result;
50 12 : }
51 :
52 : static
53 12 : void run_linearisation_instance(const std::string& spec, const t_lin_options& options, const lts::lts_aut_t& expected_statespace)
54 : {
55 12 : std::clog << " Linearisation method " << options.lin_method << std::endl
56 12 : << " rewrite strategy: " << options.rewrite_strategy << std::endl
57 12 : << " binary: " << std::boolalpha << options.binary << std::endl
58 12 : << " nocluster: " << std::boolalpha << options.no_intermediate_cluster << std::endl;
59 :
60 12 : lps::stochastic_specification s=linearise(spec, options);
61 12 : BOOST_CHECK(s != lps::stochastic_specification());
62 :
63 12 : lts::lts_aut_t result = translate_lps_to_lts<lts::lts_aut_t>(s);
64 12 : BOOST_CHECK(lts::compare(result, expected_statespace, lts::lts_eq_bisim));
65 12 : }
66 :
67 : static
68 2 : void run_linearisation_test_case(const std::string& spec, const lts::lts_aut_t& expected_statespace)
69 : {
70 : // Set various rewrite strategies
71 2 : rewrite_strategy_vector rewrite_strategies = data::detail::get_test_rewrite_strategies(false);
72 :
73 4 : for (rewrite_strategy_vector::const_iterator i = rewrite_strategies.begin(); i != rewrite_strategies.end(); ++i)
74 : {
75 2 : t_lin_options options;
76 2 : options.rewrite_strategy=*i;
77 :
78 2 : run_linearisation_instance(spec, options, expected_statespace);
79 :
80 2 : options.lin_method=lmRegular2;
81 2 : run_linearisation_instance(spec, options, expected_statespace);
82 :
83 2 : options.lin_method=lmStack;
84 2 : run_linearisation_instance(spec, options, expected_statespace);
85 :
86 2 : options.binary=true;
87 2 : run_linearisation_instance(spec, options, expected_statespace);
88 :
89 2 : options.lin_method=lmRegular;
90 2 : run_linearisation_instance(spec, options, expected_statespace);
91 :
92 2 : options.binary=false; // reset binary
93 2 : options.no_intermediate_cluster=true;
94 2 : run_linearisation_instance(spec, options, expected_statespace);
95 : }
96 2 : }
97 :
98 2 : BOOST_AUTO_TEST_CASE(bad_renaming_non_bisimilar)
99 : {
100 : const std::string spec =
101 : "sort D = struct d1;\n"
102 : "act a, b;\n"
103 : "proc\n"
104 : "P(p:D) = a. Q(p);\n"
105 : "Q(q:D) = sum l:List(D). (#l<=1) ->\n"
106 : " b.\n"
107 : " (([] == l) -> P(q) <> Q());\n"
108 1 : "init P(d1);\n";
109 :
110 : const std::string expected_statespace =
111 : "des (0,6,4)\n"
112 : "(0,\"a\",1)\n"
113 : "(1,\"b\",2)\n"
114 : "(1,\"b\",3)\n"
115 : "(2,\"a\",1)\n"
116 : "(3,\"b\",2)\n"
117 1 : "(3,\"b\",3)\n";
118 1 : std::stringstream is(expected_statespace);
119 :
120 1 : lts::lts_aut_t statespace;
121 1 : statespace.load(is);
122 1 : run_linearisation_test_case(spec,statespace);
123 1 : }
124 :
125 :
126 2 : BOOST_AUTO_TEST_CASE(where_clauses_in_conditions_of_rewrite_rules)
127 : {
128 : const std::string spec =
129 : "act a:Bool;\n"
130 : "\n"
131 : "map is_null:List(Bool) -> Bool;\n"
132 : "\n"
133 : "var L:List(Bool);\n"
134 : "eqn (n>0 whr n=#L end) -> is_null(L)=false;\n"
135 : " (n==0 whr n=#L end) -> is_null(L)= true;\n"
136 : "\n"
137 : "proc X(L:List(Bool))=a(is_null(L)).X([true]);\n"
138 1 : "init X([]);\n";
139 :
140 : const std::string expected_statespace =
141 : "des (0,2,2)\n"
142 : "(0,\"a(true)\",1)\n"
143 1 : "(1,\"a(false)\",1)\n";
144 :
145 1 : std::stringstream is(expected_statespace);
146 :
147 1 : lts::lts_aut_t statespace;
148 1 : statespace.load(is);
149 1 : run_linearisation_test_case(spec,statespace);
150 1 : }
151 :
|
