LCOV - code coverage report
Current view: top level - lps/test - untime_test.cpp (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 60 62 96.8 %
Date: 2020-02-21 00:44:40 Functions: 8 8 100.0 %
Legend: Lines: hit not hit

          Line data    Source code
       1             : // Author(s): Jeroen Keiren
       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 untime_test.cpp
      10             : /// \brief Add your file description here.
      11             : 
      12             : #define BOOST_TEST_MODULE untime_test
      13             : #include <boost/test/included/unit_test_framework.hpp>
      14             : 
      15             : #include "mcrl2/lps/linearise.h"
      16             : #include "mcrl2/lps/untime.h"
      17             : 
      18             : using namespace mcrl2;
      19             : using namespace mcrl2::data;
      20             : using namespace mcrl2::lps;
      21             : 
      22             : /*
      23             :  * Trivial test: LPS should be left as is, because there is no time involved.
      24             :  */
      25           1 : void test_case_1()
      26             : {
      27             :   const std::string text(
      28             :     "act a,b;\n"
      29             :     "proc P = a . b . P;\n"
      30             :     "init P;\n"
      31           2 :   );
      32             : 
      33           2 :   specification s0=remove_stochastic_operators(linearise(text));
      34           2 :   specification s1 = s0;
      35           2 :   rewriter r;
      36           1 :   lps::untime_algorithm<specification>(s1, false, false, r).run();
      37           1 :   const action_summand_vector& summands1 = s1.process().action_summands();
      38           3 :   for (action_summand_vector::const_iterator i = summands1.begin(); i != summands1.end(); ++i)
      39             :   {
      40           2 :     BOOST_CHECK(!i->has_time());
      41             :   }
      42             : 
      43           1 :   BOOST_CHECK(s0 == s1);
      44             : 
      45           1 :   if (s0 != s1)
      46             :   {
      47           0 :     std::clog << "Input specification  : " << lps::pp(s0) << std::endl
      48           0 :               << "Output specification : " << lps::pp(s1) << std::endl;
      49             :   }
      50           1 : }
      51             : 
      52             : /*
      53             :  * An extra process parameter (say "lat") of type Real is introduced
      54             :  * time is removed from the actions, and the condition
      55             :  * is weakened with time > lat (i.e. 2 > lat or 3 > lat in this case).
      56             :  * Furthermore a summand true->delta is introduced.
      57             :  */
      58           1 : void test_case_2()
      59             : {
      60             :   const std::string text(
      61             :     "act a,b;\n"
      62             :     "proc P = a@2 . b@3 . P;\n"
      63             :     "init P;\n"
      64           2 :   );
      65             : 
      66           2 :   specification s0=remove_stochastic_operators(linearise(text));
      67           2 :   specification s1 = s0;
      68           2 :   rewriter r;
      69           1 :   lps::untime_algorithm<specification>(s1, true, false, r).run();
      70           1 :   const action_summand_vector& summands0 = s0.process().action_summands();
      71           1 :   const action_summand_vector& summands1 = s1.process().action_summands();
      72           1 :   BOOST_CHECK(s0.process().process_parameters().size() == s1.process().process_parameters().size() - 1);
      73           3 :   for (action_summand_vector::const_iterator i = summands1.begin(); i != summands1.end(); ++i)
      74             :   {
      75           2 :     BOOST_CHECK(!i->has_time());
      76             :   }
      77           1 : }
      78             : 
      79             : /*
      80             :  * An extra process parameter (say "lat") of type Real is introduced
      81             :  * time is removed from the actions, and the condition
      82             :  * is weakened with time > lat (i.e. 2 > lat or 3 > lat in this case).
      83             :  * In the untimed summand, a summation over Real (say sum tv:Real) is introduced,
      84             :  * and the condition is weakened with tv > lat.
      85             :  * Furthermore a summand true->delta is introduced.
      86             :  */
      87           1 : void test_case_3()
      88             : {
      89             :   const std::string text(
      90             :     "act a,b;\n"
      91             :     "proc P = a@2 . b@3 . P\n"
      92             :     "       + a . P;\n"
      93             :     "init P;\n"
      94           2 :   );
      95             : 
      96           2 :   specification s0=remove_stochastic_operators(linearise(text));
      97           2 :   specification s1 = s0;
      98           2 :   rewriter r;
      99           1 :   lps::untime_algorithm<specification>(s1, true, false, r).run();
     100           1 :   const action_summand_vector& summands0 = s0.process().action_summands();
     101           1 :   const action_summand_vector& summands1 = s1.process().action_summands();
     102           1 :   BOOST_CHECK(s0.process().process_parameters().size() == s1.process().process_parameters().size() - 1);
     103           1 :   int sumvar_count = 0;
     104           4 :   for (action_summand_vector::const_iterator i = summands1.begin(); i != summands1.end(); ++i)
     105             :   {
     106           3 :     BOOST_CHECK(!i->has_time());
     107           3 :     sumvar_count += i->summation_variables().size();
     108             :   }
     109           1 :   BOOST_CHECK(sumvar_count == 1);
     110           1 : }
     111             : 
     112             : /*
     113             :  * An extra process parameter (say "lat") of type Real is introduced
     114             :  * time is removed from the actions, and the condition
     115             :  * is weakened with time > lat (i.e. 2 > lat or 3 > lat in this case).
     116             :  * In the untimed summand, a summation over Real (say sum tv:Real) is introduced,
     117             :  * and the condition is weakened with tv > lat.
     118             :  */
     119           1 : void test_case_4()
     120             : {
     121             :   const std::string text(
     122             :     "act a,b;\n"
     123             :     "proc P = a@2 . b@3 . P\n"
     124             :     "       + a . P\n"
     125             :     "       + true -> delta;\n"
     126             :     "init P;\n"
     127           2 :   );
     128             : 
     129           2 :   specification s0=remove_stochastic_operators(linearise(text));
     130           2 :   specification s1 = s0;
     131           2 :   rewriter r;
     132           1 :   lps::untime_algorithm<specification>(s1, true, false, r).run();
     133           1 :   const action_summand_vector& summands0 = s0.process().action_summands();
     134           1 :   const action_summand_vector& summands1 = s1.process().action_summands();
     135           1 :   BOOST_CHECK(s0.process().process_parameters().size() == s1.process().process_parameters().size() - 1);
     136           1 :   int sumvar_count = 0;
     137           4 :   for (action_summand_vector::const_iterator i = summands1.begin(); i != summands1.end(); ++i)
     138             :   {
     139           3 :     BOOST_CHECK(!i->has_time());
     140           3 :     sumvar_count += i->summation_variables().size();
     141             :   }
     142           1 :   BOOST_CHECK(sumvar_count == 1);
     143           1 : }
     144             : 
     145           3 : BOOST_AUTO_TEST_CASE(test_main)
     146             : {
     147           1 :   test_case_1();
     148           1 :   test_case_2();
     149           1 :   test_case_3();
     150           1 :   test_case_4();
     151           4 : }

Generated by: LCOV version 1.13