LCOV - code coverage report
Current view: top level - lps/test - multi_action_test.cpp (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 73 73 100.0 %
Date: 2020-07-11 00:44:39 Functions: 9 9 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 multi_action_test.cpp
      10             : /// \brief Add your file description here.
      11             : 
      12             : //#define MCRL2_LPS_PARELM_DEBUG
      13             : 
      14             : #define BOOST_TEST_MODULE multi_action_test
      15             : #include "mcrl2/data/consistency.h"
      16             : #include "mcrl2/data/detail/test_rewriters.h"
      17             : #include "mcrl2/lps/print.h"
      18             : 
      19             : #include <boost/test/included/unit_test_framework.hpp>
      20             : 
      21             : using namespace mcrl2;
      22             : using namespace mcrl2::data;
      23             : using namespace mcrl2::lps;
      24             : 
      25             : /// \brief Returns a data variable of type Nat with a given name
      26             : /// \param name A string
      27             : /// \return A data variable of type Nat with a given name
      28           6 : data::variable nat(const std::string& name)
      29             : {
      30           6 :   return data::variable(core::identifier_string(name), data::sort_nat::nat());
      31             : }
      32             : 
      33          25 : process::action act(const std::string& name, data_expression_list parameters)
      34             : {
      35          50 :   std::vector<sort_expression> sorts;
      36          50 :   for (const auto & parameter : parameters)
      37             :   {
      38          25 :     sorts.push_back(parameter.sort());
      39             :   }
      40          50 :   process::action_label label(name, sort_expression_list(sorts.begin(), sorts.end()));
      41          50 :   return process::action(label, parameters);
      42             : }
      43             : 
      44          10 : void test_multi_actions(const process::action_list& a, const process::action_list& b, const data_expression& expected_result = data::undefined_data_expression())
      45             : {
      46          10 :   std::cout << "--- test_multi_actions ---" << std::endl;
      47          20 :   data_expression result = equal_multi_actions(multi_action(a), multi_action(b));
      48          10 :   std::cout << "a               = " << lps::pp(a) << std::endl;
      49          10 :   std::cout << "b               = " << lps::pp(b) << std::endl;
      50          10 :   std::cout << "result          = " << lps::pp(result) << std::endl;
      51          10 :   std::cout << "expected_result = " << lps::pp(expected_result) << std::endl;
      52          10 :   BOOST_CHECK(expected_result == data::undefined_data_expression() || result == expected_result);
      53          10 : }
      54             : 
      55           1 : void test_equal_multi_actions()
      56             : {
      57             :   namespace d = data;
      58             : 
      59           2 :   data_expression d1 = nat("d1");
      60           2 :   data_expression d2 = nat("d2");
      61           2 :   data_expression d3 = nat("d3");
      62           2 :   data_expression d4 = nat("d4");
      63           2 :   process::action_list a1  ( { act("a", data_expression_list({ d1 })) });
      64           2 :   process::action_list a2  ( { act("a", data_expression_list({ d2 })) });
      65           2 :   process::action_list b1  ( { act("b", data_expression_list({ d1 })) });
      66           2 :   process::action_list b2  ( { act("b", data_expression_list({ d2 })) });
      67           2 :   process::action_list a11 ( { act("a", data_expression_list({ d1 })), act("a", data_expression_list({ d1 })) });
      68           2 :   process::action_list a12 ( { act("a", data_expression_list({ d1 })), act("a", data_expression_list({ d2 })) });
      69           2 :   process::action_list a21 ( { act("a", data_expression_list({ d2 })), act("a", data_expression_list({ d1 })) });
      70           2 :   process::action_list a22 ( { act("a", data_expression_list({ d2 })), act("a", data_expression_list({ d2 })) });
      71           2 :   process::action_list a34 ( { act("a", data_expression_list({ d3 })), act("a", data_expression_list({ d4 })) });
      72           2 :   process::action_list a12b1 ( { act("a", data_expression_list({ d1 })), act("a", data_expression_list({ d2 })), act("b", data_expression_list({ d1 })) });
      73           2 :   process::action_list a34b2 ( { act("a", data_expression_list({ d3 })), act("a", data_expression_list({ d4 })), act("b", data_expression_list({ d2 })) });
      74           1 :   test_multi_actions(a1,  a1, d::true_());
      75           1 :   test_multi_actions(a1,  a2, d::equal_to(d1, d2));
      76           1 :   test_multi_actions(a11, a11, d::true_());
      77           1 :   test_multi_actions(a12, a21, d::true_());
      78           1 :   test_multi_actions(a21, a12, d::true_());
      79           1 :   test_multi_actions(a11, a22, d::equal_to(d1, d2));
      80           1 :   test_multi_actions(a1, a12,  d::false_());
      81           1 :   test_multi_actions(a1, b1,   d::false_());
      82           1 :   test_multi_actions(a12, a34);
      83           1 :   test_multi_actions(a12b1, a34b2);
      84             : 
      85           2 :   data_expression m1 = equal_multi_actions(multi_action(a12), multi_action(a34));
      86           2 :   data_expression m2 = equal_multi_actions(multi_action(a34), multi_action(a12));
      87           2 :   data_expression n1 = data::detail::normalize_equality(m1);
      88           2 :   data_expression n2 = data::detail::normalize_equality(m2);
      89           2 :   data_expression p1 = data::detail::normalize_and_or(n1);
      90           2 :   data_expression p2 = data::detail::normalize_and_or(n2);
      91           1 :   std::cout << "m1 = " << data::pp(m1) << std::endl;
      92           1 :   std::cout << "m2 = " << data::pp(m2) << std::endl;
      93           1 :   std::cout << "n1 = " << data::pp(n1) << std::endl;
      94           1 :   std::cout << "n2 = " << data::pp(n2) << std::endl;
      95           1 :   std::cout << "p1 = " << data::pp(p1) << std::endl;
      96           1 :   std::cout << "p2 = " << data::pp(p2) << std::endl;
      97           1 :   BOOST_CHECK(p1 == p2);
      98           1 : }
      99             : 
     100           1 : void test_pp()
     101             : {
     102           2 :   data_expression d1 = nat("d1");
     103           2 :   data_expression d2 = nat("d2");
     104           2 :   process::action_list a1  ( { act("a", data_expression_list({ d1 })) });
     105           2 :   process::action_list a2  ( { act("a", data_expression_list({ d2 })) });
     106           2 :   process::action_list b1  ( { act("b", data_expression_list({ d1 })) });
     107           2 :   process::action_list a11 ( { act("a", data_expression_list({ d1 })), act("a", data_expression_list({ d1 })) });
     108           2 :   multi_action m(a11);
     109           2 :   std::string s = lps::pp(m);
     110           1 :   std::cout << "s = " << s << std::endl;
     111           1 :   BOOST_CHECK(s == "a(d1)|a(d1)");
     112           1 : }
     113             : 
     114           3 : BOOST_AUTO_TEST_CASE(test_main)
     115             : {
     116           1 :   test_equal_multi_actions();
     117           1 :   test_pp();
     118           4 : }

Generated by: LCOV version 1.13