LCOV - code coverage report
Current view: top level - pbes/test - absinthe_test.cpp (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 17 17 100.0 %
Date: 2024-03-08 02:52:28 Functions: 5 5 100.0 %
Legend: Lines: hit not hit

          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 : }

Generated by: LCOV version 1.14