Line data Source code
1 : // Author(s): Unknown
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 invelm_test.cpp
10 : /// \brief Add your file description here.
11 :
12 : //#define MCRL2_LPS_PARELM_DEBUG
13 :
14 : #define BOOST_TEST_MODULE invelm_test
15 : #include <boost/test/included/unit_test.hpp>
16 :
17 : #include "mcrl2/lps/invelm_algorithm.h"
18 : #include "mcrl2/lps/parse.h"
19 : #include "mcrl2/lps/print.h"
20 : #include "test_specifications.h"
21 :
22 : using namespace mcrl2;
23 :
24 : inline
25 4 : lps::specification invelm(const lps::specification& spec,
26 : const data::data_expression& invariant,
27 : bool simplify_all = false,
28 : bool no_elimination = false
29 : )
30 : {
31 4 : lps::specification specification = spec;
32 4 : data::rewriter::strategy rewrite_strategy = data::jitty;
33 4 : int time_limit = 0;
34 4 : bool path_eliminator = false;
35 4 : data::detail::smt_solver_type solver_type = mcrl2::data::detail::solver_type_cvc;
36 4 : bool apply_induction = false;
37 :
38 : lps::detail::Invariant_Checker<lps::specification> v_invariant_checker(specification,
39 : rewrite_strategy,
40 : time_limit,
41 : path_eliminator,
42 : solver_type,
43 : apply_induction,
44 : simplify_all
45 4 : );
46 4 : if (v_invariant_checker.check_invariant(invariant))
47 : {
48 : lps::invelm_algorithm<lps::specification> algorithm(specification,
49 : rewrite_strategy,
50 : time_limit,
51 : path_eliminator,
52 : solver_type,
53 : apply_induction,
54 : simplify_all
55 4 : );
56 4 : algorithm.run(invariant, !no_elimination);
57 4 : }
58 8 : return specification;
59 4 : }
60 :
61 2 : BOOST_AUTO_TEST_CASE(test_abp)
62 : {
63 1 : lps::specification specification = lps::parse_linear_process_specification(LINEAR_ABP);
64 2 : data::data_expression invariant = data::parse_data_expression("true");
65 :
66 1 : lps::specification result = invelm(specification, invariant);
67 1 : }
68 :
69 : template <typename Expr>
70 4 : bool has_identifier(const Expr& x, const std::string& id)
71 : {
72 4 : std::set<core::identifier_string> ids = lps::find_identifiers(x);
73 8 : return ids.find(core::identifier_string(id)) != ids.end();
74 4 : }
75 :
76 2 : BOOST_AUTO_TEST_CASE(test_invariant)
77 : {
78 : std::string SPEC =
79 : "act a, b, c, d; \n"
80 : " \n"
81 : "proc P(b1, b2: Bool) = \n"
82 : " b1 -> a . P(!b1, b2) \n"
83 : " + b2 -> b . P(true, b1 && b2) \n"
84 : " + (b1 && b2) -> c . P(false, false)\n"
85 : " + d . P(false, true) \n"
86 : " + delta; \n"
87 : " \n"
88 1 : "init P(false, true); \n"
89 : ;
90 :
91 1 : std::string INVARIANT = "!(b1 && b2)";
92 :
93 2 : data::data_expression invariant = data::parse_data_expression(INVARIANT, data::parse_variables("b1, b2: Bool;"));
94 1 : lps::specification spec = lps::parse_linear_process_specification(SPEC);
95 : bool simplify_all;
96 : bool no_elimination;
97 1 : lps::specification spec1;
98 1 : lps::linear_process proc;
99 1 : std::cout << lps::pp(spec) << std::endl;
100 :
101 1 : simplify_all = false;
102 1 : no_elimination = false;
103 1 : spec1 = invelm(spec, invariant, simplify_all, no_elimination);
104 1 : std::cout << lps::pp(spec1) << std::endl;
105 1 : proc = spec1.process();
106 1 : BOOST_CHECK(proc.action_summands().size() == 3);
107 1 : BOOST_CHECK(has_identifier(proc.action_summands()[2], "d"));
108 1 : BOOST_CHECK(proc.deadlock_summands().back().condition() == data::sort_bool::true_());
109 :
110 1 : simplify_all = true;
111 1 : no_elimination = false;
112 1 : spec1 = invelm(spec, invariant, simplify_all, no_elimination);
113 1 : std::cout << lps::pp(spec1) << std::endl;
114 1 : proc = spec1.process();
115 1 : BOOST_CHECK(proc.action_summands().size() == 3);
116 1 : BOOST_CHECK(has_identifier(proc.action_summands()[2], "d"));
117 1 : BOOST_CHECK(proc.deadlock_summands().back().condition() != invariant);
118 1 : BOOST_CHECK(proc.deadlock_summands().back().condition() != data::sort_bool::true_());
119 1 : BOOST_CHECK(has_identifier(proc.deadlock_summands().back().condition(), "b1"));
120 :
121 1 : simplify_all = true;
122 1 : no_elimination = true;
123 1 : spec1 = invelm(spec, invariant, simplify_all, no_elimination);
124 1 : std::cout << lps::pp(spec1) << std::endl;
125 1 : proc = spec1.process();
126 1 : BOOST_CHECK(proc.action_summands().size() == 4);
127 1 : BOOST_CHECK(has_identifier(proc.action_summands()[2], "c"));
128 1 : BOOST_CHECK(proc.deadlock_summands().back().condition() == invariant);
129 1 : }
130 :
|
