Line data Source code
1 : // Author(s): Thomas Neele 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 quantifiers_propagate_test.cpp 10 : /// \brief Test program for absinthe algorithm. 11 : 12 : #define BOOST_TEST_MODULE quantifiers_propagate_test 13 : #include <boost/test/included/unit_test.hpp> 14 : #include "mcrl2/pbes/quantifier_propagate.h" 15 : #include "mcrl2/pbes/txt2pbes.h" 16 : 17 : using namespace mcrl2; 18 : using namespace mcrl2::pbes_system; 19 : 20 2 : BOOST_AUTO_TEST_CASE(test_single_forall) 21 : { 22 : std::string PBES_TEXT = 23 : "pbes \n" 24 : " nu X(s: List(Nat)) = \n" 25 : " forall m1: Nat. Y(s, m1); \n" 26 : " mu Y(s: List(Nat), m1: Nat) = \n" 27 : " forall n: Nat. val(!(n mod 6 == m1)) || val(!(n <= 50 && n div 3 == 5)) || Y(n |> s, m1); \n" 28 1 : "init X([]); \n" 29 : ; 30 : 31 : std::string RESULT_TEXT = 32 : "pbes \n" 33 : " nu X(s: List(Nat)) = \n" 34 : " Y1(s); \n" 35 : " mu Y1(s: List(Nat)) = \n" 36 : " forall m1: Nat. forall n: Nat. val(!(n mod 6 == m1)) || val(!(n <= 50 && n div 3 == 5)) || Y(n |> s, m1); \n" 37 : " mu Y(s: List(Nat), m1: Nat) = \n" 38 : " forall n: Nat. val(!(n mod 6 == m1)) || val(!(n <= 50 && n div 3 == 5)) || Y(n |> s, m1); \n" 39 2 : "init X([]); \n" 40 : ; 41 : 42 1 : BOOST_CHECK_EQUAL(quantifier_propagate(txt2pbes(PBES_TEXT)), txt2pbes(RESULT_TEXT)); 43 1 : } 44 : 45 2 : BOOST_AUTO_TEST_CASE(test_two_quantifiers) 46 : { 47 : std::string PBES_TEXT = 48 : "pbes \n" 49 : " nu X(s: List(Nat)) = \n" 50 : " exists m2: Nat. forall m1: Nat. Y(s, m1 + m2); \n" 51 : " mu Y(s: List(Nat), m1: Nat) = \n" 52 : " forall n: Nat. val(!(n mod 6 == m1)) || val(!(n <= 50 && n div 3 == 5)) || Y(n |> s, m1); \n" 53 1 : "init X([]); \n" 54 : ; 55 : 56 : std::string RESULT_TEXT = 57 : "pbes \n" 58 : " nu X(s: List(Nat)) = \n" 59 : " Y1(s); \n" 60 : " mu Y1(s: List(Nat)) = \n" 61 : " exists m2: Nat. forall m1: Nat. forall n: Nat. val(!(n mod 6 == m1 + m2)) || val(!(n <= 50 && n div 3 == 5)) || Y(n |> s, m1 + m2); \n" 62 : " mu Y(s: List(Nat), m1: Nat) = \n" 63 : " forall n: Nat. val(!(n mod 6 == m1)) || val(!(n <= 50 && n div 3 == 5)) || Y(n |> s, m1); \n" 64 2 : "init X([]); \n" 65 : ; 66 : 67 1 : BOOST_CHECK_EQUAL(quantifier_propagate(txt2pbes(PBES_TEXT)), txt2pbes(RESULT_TEXT)); 68 1 : } 69 : 70 2 : BOOST_AUTO_TEST_CASE(test_parameter_dependency) 71 : { 72 : std::string PBES_TEXT = 73 : "pbes \n" 74 : " nu X(s: List(Nat)) = \n" 75 : " forall m1: Nat. Y(s, head(s) + m1); \n" 76 : " mu Y(s: List(Nat), m1: Nat) = \n" 77 : " forall n: Nat. val(!(n mod 6 == m1)) || val(!(n <= 50 && n div 3 == 5)) || Y(n |> s, m1); \n" 78 1 : "init X([]); \n" 79 : ; 80 : 81 : // No changes expected, since m1 depends on the parameter s in Y(s, head(s) + m1) 82 1 : std::string RESULT_TEXT = PBES_TEXT; 83 : 84 1 : BOOST_CHECK_EQUAL(quantifier_propagate(txt2pbes(PBES_TEXT)), txt2pbes(RESULT_TEXT)); 85 1 : } 86 : 87 2 : BOOST_AUTO_TEST_CASE(test_no_quantifier) 88 : { 89 : std::string PBES_TEXT = 90 : "pbes \n" 91 : " nu X(s: Nat) = \n" 92 : " Y(2); \n" 93 : " mu Y(s: Nat) = \n" 94 : " val(s == 2); \n" 95 1 : "init X(0); \n" 96 : ; 97 : 98 : // No changes expected, since there is no quantifier to propagate 99 1 : std::string RESULT_TEXT = PBES_TEXT; 100 : 101 1 : BOOST_CHECK_EQUAL(quantifier_propagate(txt2pbes(PBES_TEXT)), txt2pbes(RESULT_TEXT)); 102 1 : }