Line data    Source code

       1             : // Author(s): Frank Stappers
       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 lpsparunfold_test.cpp
      10             : /// \brief Add your file description here.
      11             : 
      12             : #define BOOST_TEST_MODULE lpsparunfold_test
      13             : #include <boost/algorithm/string.hpp>
      14             : #include <boost/test/included/unit_test.hpp>
      15             : 
      16             : #include "mcrl2/lps/lpsparunfoldlib.h"
      17             : #include "mcrl2/lps/parse.h"
      18             : 
      19             : using namespace mcrl2;
      20             : using namespace mcrl2::data;
      21             : using namespace mcrl2::lps;
      22             : 
      23             : 
      24           2 : BOOST_AUTO_TEST_CASE(test_main)
      25             : {
      26             :     /**
      27             :       * Unfold Pos process parameter at index 0
      28             :       *
      29             :       **/
      30             : 
      31             :     std::string case_1 =
      32             :       "% Test Case 1 -- Unfold Pos                                                      \n"
      33             :       "%                                                                                \n"
      34             :       "% The first process parameter i of type Pos is is unfolded                       \n"
      35             :       "                                                                                 \n"
      36             :       "act action :Pos;                                                                 \n"
      37             :       "                                                                                 \n"
      38             :       "proc P(i: Pos) = action(i). P(i);                                                \n"
      39             :       "                                                                                 \n"
      40           1 :       "init P(1);                                                                       \n"
      41             :       ;
      42             : 
      43             : 
      44           1 :     stochastic_specification s0;
      45           1 :     parse_lps(case_1,s0);
      46           1 :     variable_list p0 = s0.process().process_parameters();
      47             : 
      48             :     /* Requirements */
      49           1 :     if (p0.size() != 1)
      50             :     {
      51           0 :       std::clog << "--- failed test ---" << std::endl;
      52           0 :       std::clog << case_1 << std::endl;
      53           0 :       std::clog << "expected 1 process parameter" << std::endl;
      54           0 :       std::clog << "encountered " << p0.size() << "process parameters" << std::endl;
      55             :     }
      56           1 :     BOOST_CHECK(p0.size() == 1);
      57             : 
      58           1 :     std::string t0 = data::pp(p0.front().sort());
      59           1 :     if (t0.compare("Pos") != 0)
      60             :     {
      61           0 :       std::clog << "--- failed test ---" << std::endl;
      62           0 :       std::clog << case_1 << std::endl;
      63           0 :       std::clog << "expected process parameter to be of type Pos" << std::endl;
      64           0 :       std::clog << "encountered process parameter of type " << p0.front().sort() << std::endl;
      65             :     }
      66           1 :     BOOST_CHECK(t0.compare("Pos") == 0);
      67             : 
      68             :     /* Return */
      69             : 
      70           1 :     std::map< mcrl2::data::sort_expression , lps::unfold_cache_element > unfold_cache;
      71           1 :     lpsparunfold lpsparunfold(s0, unfold_cache);
      72           1 :     lpsparunfold.algorithm(0);
      73           1 :     variable_list p1 = s0.process().process_parameters();
      74           1 :     if (p1.size() != 3)
      75             :     {
      76           0 :       std::clog << "--- failed test ---" << std::endl;
      77           0 :       std::clog << case_1 << std::endl;
      78           0 :       std::clog << "expected result to have 3 process parameters" << std::endl;
      79           0 :       std::clog << "computed " << p1.size() << " process parameters" << std::endl;
      80             :     }
      81             : 
      82           4 :     for (variable_list::iterator i = p1.begin(); i != p1.end(); ++i)
      83             :     {
      84           3 :       if (std::distance(p1.begin(), i) == 1 && data::pp(i->sort()).compare("Bool") != 0)
      85             :       {
      86           0 :         std::clog << "--- failed test ---" << std::endl;
      87           0 :         std::clog << lps::pp(s0) << std::endl;
      88           0 :         std::clog << "expected 2nd process parameter to be of type Bool" << std::endl;
      89           0 :         std::clog << "computed process parameter of type "  << data::pp(i->sort()) << std::endl;
      90             :       }
      91           3 :       BOOST_CHECK(!(std::distance(p1.begin(), i) == 1 && data::pp(i->sort()).compare("Bool") != 0));
      92             : 
      93           3 :       if (std::distance(p1.begin(), i) == 2 && data::pp(i->sort()).compare("Pos") != 0)
      94             :       {
      95           0 :         std::clog << "--- failed test ---" << std::endl;
      96           0 :         std::clog << lps::pp(s0) << std::endl;
      97           0 :         std::clog << "expected 3th process parameter to be of type Pos " << std::endl;
      98           0 :         std::clog << "computed process parameter of type "  << data::pp(i->sort()) << std::endl;
      99             :       }
     100           3 :       BOOST_CHECK(!(std::distance(p1.begin(), i) == 2 && data::pp(i->sort()).compare("Pos") != 0));
     101             :     }
     102           1 : }
     103             :