LCOV - code coverage report
Current view: top level - lps/test - timed_linearization_test.cpp (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 112 121 92.6 %
Date: 2020-07-04 00:44:36 Functions: 36 36 100.0 %
Legend: Lines: hit not hit

          Line data    Source code
       1             : // Author(s): Jan Friso Groote
       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 timed_linearization_test.cpp
      10             : /// \brief Add your file description here.
      11             : 
      12             : #define BOOST_TEST_MODULE timed_linearization_test
      13             : #include <boost/test/included/unit_test_framework.hpp>
      14             : 
      15             : #ifndef MCRL2_SKIP_LONG_TESTS
      16             : 
      17             : #include "mcrl2/data/detail/rewrite_strategies.h"
      18             : #include "mcrl2/lps/linearise.h"
      19             : 
      20             : using namespace mcrl2;
      21             : using namespace mcrl2::lps;
      22             : 
      23             : typedef data::rewriter::strategy rewrite_strategy;
      24             : typedef std::vector<rewrite_strategy> rewrite_strategy_vector;
      25             : 
      26         180 : data::data_expression ultimate_delay(const stochastic_action_summand_vector& l)
      27             : {
      28         180 :   data::data_expression result=data::sort_real::real_("0");
      29         408 :   for(const stochastic_action_summand& s: l)
      30             :   {
      31         228 :     if (s.condition()!=data::sort_bool::false_() && s.has_time())
      32             :     {
      33         192 :       result=data::sort_real::maximum(result, s.multi_action().time());
      34             :     }
      35             :   }
      36         180 :   return result;
      37             : }
      38             : 
      39         108 : data::data_expression ultimate_delay(const deadlock_summand_vector& l)
      40             : {
      41         108 :   data::data_expression result=data::sort_real::real_("0");
      42         228 :   for(const deadlock_summand& s: l)
      43             :   {
      44         120 :     BOOST_CHECK(s.has_time());
      45         120 :     if (s.condition()!=data::sort_bool::false_())
      46             :     {
      47         120 :       result=data::sort_real::maximum(result, s.deadlock().time());
      48             :     }
      49             :   }
      50         108 :   return result;
      51             : }
      52             : 
      53          90 : void run_linearisation_instance(const std::string& spec,
      54             :                                 const t_lin_options& options,
      55             :                                 const bool expect_success,
      56             :                                 const data::data_expression max_expected_action_ultimate_delay,
      57             :                                 const bool check_max_expected_deadlock_ultimate_delay,
      58             :                                 const data::data_expression max_expected_deadlock_ultimate_delay)
      59             : {
      60          90 :   if (expect_success)
      61             :   {
      62         180 :     lps::stochastic_specification s=linearise(spec, options);
      63         180 :     data::rewriter r(s.data());
      64         180 :     data::data_expression max_action_ultimate_delay=r(ultimate_delay(s.process().action_summands()));
      65          90 :     if (r(data::equal_to(ultimate_delay(s.process().action_summands()),max_expected_action_ultimate_delay))!=data::sort_bool::true_())
      66             :     {
      67           0 :       std::clog << "Expected action time does not match:\n";
      68           0 :       std::clog << "Action time " << max_action_ultimate_delay << "\n";
      69           0 :       std::clog << "Expected maximum delay " << max_expected_action_ultimate_delay << "\n";
      70           0 :       BOOST_CHECK(r(data::equal_to(ultimate_delay(s.process().action_summands()),max_expected_action_ultimate_delay))==data::sort_bool::true_());
      71             :     }
      72          90 :     if (check_max_expected_deadlock_ultimate_delay)
      73             :     {
      74         108 :       data::data_expression max_deadlock_ultimate_delay=r(ultimate_delay(s.process().deadlock_summands()));
      75          54 :       if (r(data::equal_to(ultimate_delay(s.process().deadlock_summands()),max_expected_deadlock_ultimate_delay))!=data::sort_bool::true_())
      76             :       {
      77           0 :         std::clog << "Expected deadlock time does not match:\n";
      78           0 :         std::clog << "Deadlock time " << ultimate_delay(s.process().deadlock_summands()) << "\n";
      79           0 :         std::clog << "Expected maximum delay " << max_expected_deadlock_ultimate_delay << "\n";
      80           0 :         BOOST_CHECK(r(data::equal_to(ultimate_delay(s.process().deadlock_summands()),max_expected_deadlock_ultimate_delay))==data::sort_bool::true_());
      81             :       }
      82             :     }
      83             :   }
      84             :   else
      85             :   {
      86           0 :     BOOST_CHECK_THROW(linearise(spec, options), mcrl2::runtime_error);
      87             :   }
      88          90 : }
      89             : 
      90             : // The ultimate delays are the maximum of the ultimate delays over all actions resp. deadlocks
      91             : // not looking at the conditions of the actions or deadlocks.
      92          15 : void run_linearisation_test_case(const std::string& spec,
      93             :                                  const bool expect_success,
      94             :                                  const std::size_t max_expected_action_ultimate_delay_,
      95             :                                  const bool check_max_expected_deadlock_ultimate_delay,
      96             :                                  const std::size_t max_expected_deadlock_ultimate_delay_)
      97             : {
      98             :   // Set various rewrite strategies
      99          30 :   rewrite_strategy_vector rewrite_strategies = data::detail::get_test_rewrite_strategies(false);
     100          30 :   const data::data_expression max_expected_action_ultimate_delay=data::sort_real::real_(max_expected_action_ultimate_delay_);
     101          30 :   const data::data_expression max_expected_deadlock_ultimate_delay=data::sort_real::real_(max_expected_deadlock_ultimate_delay_);
     102             : 
     103          30 :   for (rewrite_strategy_vector::const_iterator i = rewrite_strategies.begin(); i != rewrite_strategies.end(); ++i)
     104             :   {
     105          15 :     std::clog << std::endl << "Testing with rewrite strategy " << *i << std::endl;
     106          15 :     std::clog << spec << "\n";
     107             : 
     108          15 :     t_lin_options options;
     109          15 :     options.ignore_time=false;  // Do not ignore time.
     110             : 
     111          15 :     options.rewrite_strategy=*i;
     112             : 
     113          15 :     std::clog << "  Default options" << std::endl;
     114          15 :     run_linearisation_instance(spec, options, expect_success,max_expected_action_ultimate_delay,check_max_expected_deadlock_ultimate_delay,max_expected_deadlock_ultimate_delay);
     115             : 
     116          15 :     std::clog << "  Linearisation method regular2" << std::endl;
     117          15 :     options.lin_method=lmRegular2;
     118          15 :     run_linearisation_instance(spec, options, expect_success,max_expected_action_ultimate_delay,check_max_expected_deadlock_ultimate_delay,max_expected_deadlock_ultimate_delay);
     119             : 
     120          15 :     std::clog << "  Linearisation method stack" << std::endl;
     121          15 :     options.lin_method=lmStack;
     122          15 :     run_linearisation_instance(spec, options, expect_success,max_expected_action_ultimate_delay,check_max_expected_deadlock_ultimate_delay,max_expected_deadlock_ultimate_delay);
     123             : 
     124          15 :     std::clog << "  Linearisation method stack; binary enabled" << std::endl;
     125          15 :     options.binary=true;
     126          15 :     run_linearisation_instance(spec, options, expect_success,max_expected_action_ultimate_delay,check_max_expected_deadlock_ultimate_delay,max_expected_deadlock_ultimate_delay);
     127             : 
     128          15 :     std::clog << "  Linearisation method regular; binary enabled" << std::endl;
     129          15 :     options.lin_method=lmRegular;
     130          15 :     run_linearisation_instance(spec, options, expect_success,max_expected_action_ultimate_delay,check_max_expected_deadlock_ultimate_delay,max_expected_deadlock_ultimate_delay);
     131             : 
     132          15 :     std::clog << "  Linearisation method regular; no intermediate clustering" << std::endl;
     133          15 :     options.binary=false; // reset binary
     134          15 :     options.no_intermediate_cluster=true;
     135          15 :     run_linearisation_instance(spec, options, expect_success,max_expected_action_ultimate_delay,check_max_expected_deadlock_ultimate_delay,max_expected_deadlock_ultimate_delay);
     136             :   }
     137          15 : }
     138             : 
     139           3 : BOOST_AUTO_TEST_CASE(Check_single_timed_process)
     140             : {
     141             :   const std::string spec =
     142             :     "act a;\n"
     143           2 :     "init a@2.delta@10;\n"
     144             :     ;
     145             : 
     146           1 :   run_linearisation_test_case(spec,true,2,true,10);
     147           1 : }
     148             : 
     149           3 : BOOST_AUTO_TEST_CASE(Check_parallel_timed_processes)
     150             : {
     151             :   const std::string spec =
     152             :     "act a;\n"
     153           2 :     "init a@2.delta@10 || a@4.delta@10;\n"
     154             :     ;
     155             : 
     156           1 :   run_linearisation_test_case(spec,true,4,true,10);
     157           1 : }
     158             : 
     159           3 : BOOST_AUTO_TEST_CASE(Check_parallel_timed_processes_with_the_same_time)
     160             : {
     161             :   const std::string spec =
     162             :     "act a;\n"
     163           2 :     "init a@2.delta@10 || a@2.delta@10;\n"
     164             :     ;
     165             : 
     166           1 :   run_linearisation_test_case(spec,true,2,true,10);
     167           1 : }
     168             : 
     169           3 : BOOST_AUTO_TEST_CASE(Check_parallel_timed_processes_reversed)
     170             : {
     171             :   const std::string spec =
     172             :    "act a;\n"
     173           2 :    "init a@5.delta@10 || a@3.delta@10;\n"
     174             :    ;
     175             : 
     176           1 :   run_linearisation_test_case(spec,true,5,true,10);
     177           1 : }
     178             : 
     179           3 : BOOST_AUTO_TEST_CASE(Check_parallel_deltas)
     180             : {
     181             :   const std::string spec =
     182           2 :     "init delta@2 || delta@4;\n"
     183             :     ;
     184             : 
     185           1 :   run_linearisation_test_case(spec,true,0,true,2);
     186           1 : }
     187             : 
     188           3 : BOOST_AUTO_TEST_CASE(Check_parallel_deltas_with_the_same_time)
     189             : {
     190             :   const std::string spec =
     191           2 :     "init delta@2 || delta@2;\n"
     192             :     ;
     193             : 
     194           1 :   run_linearisation_test_case(spec,true,0,true,2);
     195           1 : }
     196             : 
     197           3 : BOOST_AUTO_TEST_CASE(Check_parallel_action_and_delta_with_the_same_time)
     198             : {
     199             :   const std::string spec =
     200             :     "act a;\n"
     201           2 :     "init a@3.delta@10 || delta@3;";
     202             :     ;
     203             : 
     204           1 :   run_linearisation_test_case(spec,true,0,true,3);
     205           1 : }
     206             : 
     207           3 : BOOST_AUTO_TEST_CASE(Check_parallel_action_and_delta_with_different_time1)
     208             : {
     209             :   const std::string spec =
     210             :     "act a;\n"
     211           2 :     "init a@3.delta@10 || delta@4;";
     212             :     ;
     213             : 
     214           1 :   run_linearisation_test_case(spec,true,3,true,4);
     215           1 : }
     216             : 
     217           3 : BOOST_AUTO_TEST_CASE(Check_parallel_action_and_delta_with_different_time2)
     218             : {
     219             :   const std::string spec =
     220             :     "act a;\n"
     221           2 :     "init a@4.delta@10 || delta@3;";
     222             :     ;
     223             : 
     224           1 :   run_linearisation_test_case(spec,true,0,true,3);
     225           1 : }
     226             : 
     227           3 : BOOST_AUTO_TEST_CASE(Check_terminate)
     228             : {
     229             :   const std::string spec =
     230             :     "act a;\n"
     231           2 :     "init a@2;";
     232             :     ;
     233             : 
     234           1 :   run_linearisation_test_case(spec,true,2,false,0);
     235           1 : }
     236             : 
     237           3 : BOOST_AUTO_TEST_CASE(Check_terminate_and_parallelism)
     238             : {
     239             :   const std::string spec =
     240             :     "act a;\n"
     241           2 :     "init a@2||a@3;";
     242             :     ;
     243             : 
     244           1 :   run_linearisation_test_case(spec,true,3,false,0);
     245           1 : }
     246             : 
     247           3 : BOOST_AUTO_TEST_CASE(Check_terminate_and_synchrony)
     248             : {
     249             :   const std::string spec =
     250             :     "act a;\n"
     251           2 :     "init a@2||a@2;";
     252             :     ;
     253             : 
     254           1 :   run_linearisation_test_case(spec,true,2,false,0);
     255           1 : }
     256             : 
     257           3 : BOOST_AUTO_TEST_CASE(Check_terminate_and_parallelism_deadlock1)
     258             : {
     259             :   const std::string spec =
     260             :     "act a;\n"
     261           2 :     "init a@2||delta@3;";
     262             :     ;
     263             : 
     264           1 :   run_linearisation_test_case(spec,true,2,false,0);  // As it stands, cannot check the the deadlock. Should be "true,3".
     265           1 : }
     266             : 
     267           3 : BOOST_AUTO_TEST_CASE(Check_terminate_and_parallelism_deadlock2)
     268             : {
     269             :   const std::string spec =
     270             :     "act a;\n"
     271           2 :     "init a@4||delta@3;";
     272             :     ;
     273             : 
     274           1 :   run_linearisation_test_case(spec,true,0,false,0);
     275           1 : }
     276             : 
     277           3 : BOOST_AUTO_TEST_CASE(Check_terminate_and_synchrony_and_deadlock)
     278             : {
     279             :   const std::string spec =
     280             :     "act a;\n"
     281           2 :     "init a@2||delta@2;";
     282             :     ;
     283             : 
     284           1 :   run_linearisation_test_case(spec,true,0,false,0);
     285           4 : }
     286             : 
     287             : #else // ndef MCRL2_SKIP_LONG_TESTS
     288             : 
     289             : BOOST_AUTO_TEST_CASE(skip_test)
     290             : {
     291             : }
     292             : 
     293             : #endif // ndef MCRL2_SKIP_LONG_TESTS
     294             : 

Generated by: LCOV version 1.13