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 absinthe_test.cpp 10 : /// \brief Test program for absinthe algorithm. 11 : 12 : #define BOOST_TEST_MODULE absinthe_test 13 : #include <boost/test/included/unit_test.hpp> 14 : #include "mcrl2/pbes/absinthe.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_separate_keyword_section) 21 : { 22 : std::string text = 23 : "\n" 24 : "\n" 25 : "absmap\n" 26 1 : "h: Nat -> AbsNat\n" 27 : ; 28 : 29 5 : std::vector<std::string> all_keywords = { "sort", "absmap" }; 30 2 : std::pair<std::string, std::string> q = utilities::detail::separate_keyword_section(text, "absmap", all_keywords); 31 1 : BOOST_CHECK(q.first.find("absmap") == 0); 32 1 : BOOST_CHECK(utilities::trim_copy(q.second).empty()); 33 1 : } 34 : 35 1 : void test_absinthe(const std::string& pbes_text, const std::string& abstraction_text, bool is_over_approximation) 36 : { 37 1 : pbes p = txt2pbes(pbes_text); 38 1 : absinthe_algorithm algorithm; 39 1 : algorithm.run(p, abstraction_text, is_over_approximation); 40 1 : } 41 : 42 : // test with structured sorts 43 2 : BOOST_AUTO_TEST_CASE(test_structured_sorts) 44 : { 45 : std::string PBES_TEXT = 46 : "sort Bit = struct e0 | e1; \n" 47 : " \n" 48 : "map inv : Bit -> Bit; \n" 49 : " \n" 50 : "eqn \n" 51 : " inv(e0) = e1; \n" 52 : " inv(e1) = e0; \n" 53 : " \n" 54 : "pbes \n" 55 : " \n" 56 : "nu X(b:Bit) = val (b == e0) && X(inv(inv(b))); \n" 57 : " \n" 58 1 : "init X(e0); \n" 59 : ; 60 : 61 : std::string ABSTRACTION_TEXT = 62 : "sort \n" 63 : " AbsBit = struct arbitrary; \n" 64 : " \n" 65 : "var \n" 66 : " b:Bit; \n" 67 : "eqn \n" 68 : " h(b) = arbitrary; \n" 69 : " abseq(arbitrary,arbitrary) = {true,false}; \n" 70 : " absinv(arbitrary) = {arbitrary}; \n" 71 : " \n" 72 : "absmap \n" 73 : "h: Bit -> AbsBit; \n" 74 : " \n" 75 : "absfunc \n" 76 : " ==: Bit # Bit -> Bool := abseq : AbsBit # AbsBit -> Set(Bool) \n" 77 1 : " inv: Bit -> Bit := absinv : AbsBit -> Set(AbsBit) \n" 78 : ; 79 : 80 1 : test_absinthe(PBES_TEXT, ABSTRACTION_TEXT, true); 81 1 : }