LCOV - code coverage report
Current view: top level - lps/test - parelm_test.cpp (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 37 37 100.0 %
Date: 2020-07-04 00:44:36 Functions: 6 6 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 parelm_test.cpp
      10             : /// \brief Add your file description here.
      11             : 
      12             : //#define MCRL2_LPS_PARELM_DEBUG
      13             : 
      14             : #define BOOST_TEST_MODULE parelm_test
      15             : #include <boost/algorithm/string.hpp>
      16             : #include <boost/test/included/unit_test_framework.hpp>
      17             : 
      18             : #include "mcrl2/lps/detail/specification_property_map.h"
      19             : #include "mcrl2/lps/parelm.h"
      20             : #include "mcrl2/lps/parse.h"
      21             : 
      22             : using namespace mcrl2;
      23             : using namespace mcrl2::data;
      24             : using namespace mcrl2::lps;
      25             : 
      26           1 : const std::string case_1(
      27             :   "act a;\n\n"
      28             :   "proc X(i: Nat) = a.X(i);\n\n"
      29             :   "init X(2);\n");
      30           1 : const std::string expected_1 = "process_parameter_names = ";
      31             : 
      32           1 : const std::string case_2(
      33             :   "act a: Nat;\n\n"
      34             :   "proc X(i,j: Nat) = a(i). X(i,j);\n\n"
      35             :   "init X(0,1);\n");
      36           1 : const std::string expected_2 = "process_parameter_names = i";
      37             : 
      38           1 : const std::string case_3(
      39             :   "act a;\n\n"
      40             :   "proc X(i,j: Nat)   = (i == 5) -> a. X(i,j);\n\n"
      41             :   "init X(0,1);\n");
      42           1 : const std::string expected_3 = "process_parameter_names = i";
      43             : 
      44           1 : const std::string case_4(
      45             :   "act a;\n\n"
      46             :   "proc X(i,j: Nat) = a@i.X(i,j);\n\n"
      47             :   "init X(0,4);\n");
      48           1 : const std::string expected_4 = "process_parameter_names = i";
      49             : 
      50           1 : const std::string case_5(
      51             :   "act a: Nat;\n"
      52             :   "act b;\n\n"
      53             :   "proc X(i,j,k: Nat) =  a(i).X(k,j,k) +\n"
      54             :   "                         b.X(j,j,k);\n\n"
      55             :   "init X(1,2,3);");
      56           1 : const std::string expected_5 = "process_parameter_names = i, j, k";
      57             : 
      58             : // % non-linear process corresponding to case 6
      59             : // act act1, act2, act3: Nat;
      60             : // proc X(i: Nat)   = (i <  5) -> act1(i).X(i+1) +
      61             : //                    (i == 5) -> act3(i).Y(i, i);
      62             : //      Y(i,j: Nat) = act2(j).Y(i,j+1);
      63             : // init X(0);
      64           1 : const std::string case_6 =
      65             :   "act  act1,act2,act3: Nat;          \n"
      66             :   "                                   \n"
      67             :   "var  dc1: Nat;                     \n"
      68             :   "proc P(s3_X: Pos, i_X,j_X: Nat) =  \n"
      69             :   "       (s3_X == 1 && i_X == 5) ->  \n"
      70             :   "         act3(i_X) .               \n"
      71             :   "         P(2, i_X, i_X)            \n"
      72             :   "     + (s3_X == 1 && i_X < 5) ->   \n"
      73             :   "         act1(i_X) .               \n"
      74             :   "         P(1, i_X + 1, dc1)        \n"
      75             :   "     + (s3_X == 2) ->              \n"
      76             :   "         act2(j_X) .               \n"
      77             :   "         P(2, i_X, j_X + 1);       \n"
      78             :   "                                   \n"
      79             :   "var  dc: Nat;                      \n"
      80             :   "init P(1, 0, dc);                  \n"
      81             :   ;
      82             : 
      83           1 : const std::string case_7(
      84             :   "act act1, act2, act3: Nat;\n\n"
      85             :   "proc X(i,z,j: Nat)   = (i <  5) -> act1(i)@z.X(i+1,z, j) +\n"
      86             :   "                       (i == 5) -> act3(i).X(i, j, 4);\n\n"
      87             :   "init X(0,5, 1);\n"
      88             : );
      89           1 : const std::string expected_7 = "process_parameter_names = i, z, j";
      90             : 
      91             : // Example given by Jan Friso. Parameter xi08 is erroneously found.
      92           1 : const std::string case_8 =
      93             :   "sort Comp = struct smaller?is_smaller | equal?is_equal | larger?is_larger;                                           \n"
      94             :   "                                                                                                                     \n"
      95             :   "map  k: Real;                                                                                                        \n"
      96             :   "                                                                                                                     \n"
      97             :   "eqn  k  =  2;                                                                                                        \n"
      98             :   "                                                                                                                     \n"
      99             :   "act  get,_get,__get,set,_set,__set: Nat;                                                                             \n"
     100             :   "     cs_in,cs_out: Pos;                                                                                              \n"
     101             :   "                                                                                                                     \n"
     102             :   "proc P(s32_P_init1,s31_P_init1: Pos, id_ID: Nat, xi,xi00,xi01,xi02,xi03,xi04,xi05,xi06,xi07,xi08: Comp) =            \n"
     103             :   "    ((((!is_smaller(xi08) && !is_smaller(xi04)) && !is_smaller(xi03)) && !is_smaller(xi02)) && !is_smaller(xi00)) -> \n"
     104             :   "         delta;                                                                                                      \n"
     105             :   "                                                                                                                     \n"
     106             :   " init P(1, 1, 0, equal, equal, equal, larger, equal, larger, equal, equal, equal, equal);                            \n"
     107             :   ;
     108           1 : const std::string expected_8 = "process_parameter_names = xi00, xi02, xi03, xi04, xi08";
     109             : 
     110           7 : void test_parelm(const std::string& message, const std::string& spec_text, const std::string& expected_result)
     111             : {
     112          14 :   specification spec1 = parse_linear_process_specification(spec_text);
     113          14 :   specification spec2 = spec1;
     114           7 :   parelm(spec1, true);
     115           7 :   parelm(spec2, false);
     116          14 :   lps::detail::specification_property_map<> info1(spec1);
     117          14 :   lps::detail::specification_property_map<> info2(spec2);
     118           7 :   BOOST_CHECK(data::detail::compare_property_maps(message + "a", info1, expected_result));
     119           7 :   BOOST_CHECK(data::detail::compare_property_maps(message + "b", info2, expected_result));
     120           7 : }
     121             : 
     122           1 : void test_parelm()
     123             : {
     124           1 :   test_parelm("case_1", case_1, expected_1);
     125           1 :   test_parelm("case_2", case_2, expected_2);
     126           1 :   test_parelm("case_3", case_3, expected_3);
     127           1 :   test_parelm("case_4", case_4, expected_4);
     128           1 :   test_parelm("case_5", case_5, expected_5);
     129           1 :   test_parelm("case_7", case_7, expected_7);
     130           1 :   test_parelm("case_8", case_8, expected_8);
     131           1 : }
     132             : 
     133           3 : BOOST_AUTO_TEST_CASE(test_main)
     134             : {
     135           1 :   test_parelm();
     136           4 : }

Generated by: LCOV version 1.13