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.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           1 :   );
      32             : 
      33           1 :   specification s0=remove_stochastic_operators(linearise(text));
      34           1 :   specification s1 = s0;
      35           1 :   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           1 :   );
      65             : 
      66           1 :   specification s0=remove_stochastic_operators(linearise(text));
      67           1 :   specification s1 = s0;
      68           1 :   rewriter r;
      69           1 :   lps::untime_algorithm<specification>(s1, true, false, r).run();
      70           1 :   const action_summand_vector& summands1 = s1.process().action_summands();
      71           1 :   BOOST_CHECK(s0.process().process_parameters().size() == s1.process().process_parameters().size() - 1);
      72           3 :   for (action_summand_vector::const_iterator i = summands1.begin(); i != summands1.end(); ++i)
      73             :   {
      74           2 :     BOOST_CHECK(!i->has_time());
      75             :   }
      76           1 : }
      77             : 
      78             : /*
      79             :  * An extra process parameter (say "lat") of type Real is introduced
      80             :  * time is removed from the actions, and the condition
      81             :  * is weakened with time > lat (i.e. 2 > lat or 3 > lat in this case).
      82             :  * In the untimed summand, a summation over Real (say sum tv:Real) is introduced,
      83             :  * and the condition is weakened with tv > lat.
      84             :  * Furthermore a summand true->delta is introduced.
      85             :  */
      86           1 : void test_case_3()
      87             : {
      88             :   const std::string text(
      89             :     "act a,b;\n"
      90             :     "proc P = a@2 . b@3 . P\n"
      91             :     "       + a . P;\n"
      92             :     "init P;\n"
      93           1 :   );
      94             : 
      95           1 :   specification s0=remove_stochastic_operators(linearise(text));
      96           1 :   specification s1 = s0;
      97           1 :   rewriter r;
      98           1 :   lps::untime_algorithm<specification>(s1, true, false, r).run();
      99           1 :   const action_summand_vector& summands1 = s1.process().action_summands();
     100           1 :   BOOST_CHECK(s0.process().process_parameters().size() == s1.process().process_parameters().size() - 1);
     101           1 :   int sumvar_count = 0;
     102           4 :   for (action_summand_vector::const_iterator i = summands1.begin(); i != summands1.end(); ++i)
     103             :   {
     104           3 :     BOOST_CHECK(!i->has_time());
     105           3 :     sumvar_count += i->summation_variables().size();
     106             :   }
     107           1 :   BOOST_CHECK(sumvar_count == 1);
     108           1 : }
     109             : 
     110             : /*
     111             :  * An extra process parameter (say "lat") of type Real is introduced
     112             :  * time is removed from the actions, and the condition
     113             :  * is weakened with time > lat (i.e. 2 > lat or 3 > lat in this case).
     114             :  * In the untimed summand, a summation over Real (say sum tv:Real) is introduced,
     115             :  * and the condition is weakened with tv > lat.
     116             :  */
     117           1 : void test_case_4()
     118             : {
     119             :   const std::string text(
     120             :     "act a,b;\n"
     121             :     "proc P = a@2 . b@3 . P\n"
     122             :     "       + a . P\n"
     123             :     "       + true -> delta;\n"
     124             :     "init P;\n"
     125           1 :   );
     126             : 
     127           1 :   specification s0=remove_stochastic_operators(linearise(text));
     128           1 :   specification s1 = s0;
     129           1 :   rewriter r;
     130           1 :   lps::untime_algorithm<specification>(s1, true, false, r).run();
     131           1 :   const action_summand_vector& summands1 = s1.process().action_summands();
     132           1 :   BOOST_CHECK(s0.process().process_parameters().size() == s1.process().process_parameters().size() - 1);
     133           1 :   int sumvar_count = 0;
     134           4 :   for (action_summand_vector::const_iterator i = summands1.begin(); i != summands1.end(); ++i)
     135             :   {
     136           3 :     BOOST_CHECK(!i->has_time());
     137           3 :     sumvar_count += i->summation_variables().size();
     138             :   }
     139           1 :   BOOST_CHECK(sumvar_count == 1);
     140           1 : }
     141             : 
     142           2 : BOOST_AUTO_TEST_CASE(test_main)
     143             : {
     144           1 :   test_case_1();
     145           1 :   test_case_2();
     146           1 :   test_case_3();
     147           1 :   test_case_4();
     148           1 : }