LCOV - code coverage report
Current view: top level - lps/test - ltsmin_test.cpp (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 169 171 98.8 %
Date: 2020-09-22 00:46:14 Functions: 14 14 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 ltsmin_test.cpp
      10             : /// \brief Test for the pins class that connects mCRL2 with LTSMin (http://fmt.cs.utwente.nl/tools/ltsmin/).
      11             : 
      12             : #define BOOST_TEST_MODULE ltsmin_test
      13             : 
      14             : #include <boost/test/included/unit_test_framework.hpp>
      15             : 
      16             : #include "mcrl2/lps/detail/test_input.h"
      17             : #include "mcrl2/lps/linearise.h"
      18             : #include "mcrl2/lps/ltsmin.h"
      19             : 
      20             : using namespace mcrl2;
      21             : 
      22             : typedef int* state_vector;
      23             : 
      24             : inline
      25          14 : std::string print_state(const state_vector& s, std::size_t size, const std::string& msg = "state: ")
      26             : {
      27          14 :   int* first = s;
      28          14 :   int* last = s + size;
      29             : 
      30          28 :   std::ostringstream out;
      31          14 :   out << msg << "[";
      32         168 :   for (int* i = first; i != last; ++i)
      33             :   {
      34         154 :     if (i != first)
      35             :     {
      36         140 :       out << ", ";
      37             :     }
      38         154 :     out << *i;
      39             :   }
      40          14 :   out << "]";
      41          28 :   return out.str();
      42             : }
      43             : 
      44             : struct state_callback_function
      45             : {
      46             :   std::size_t state_size;
      47             :   std::size_t state_count;
      48             : 
      49          26 :   explicit state_callback_function(std::size_t size)
      50          26 :     : state_size(size),
      51          26 :       state_count(0)
      52          26 :   {}
      53             : 
      54          12 :   void operator()(state_vector const& next_state, int* const& labels, int group=-1)
      55             :   {
      56          12 :     state_count++;
      57          12 :     std::cout << print_state(next_state, state_size, "visit state: ") << " edge label = " << labels[0] << " group = " << group << std::endl;
      58          12 :   }
      59             : };
      60             : 
      61           2 : void test_data_type(lps::pins_data_type& type)
      62             : {
      63           2 :   std::cout << "test_data_type(" << type.name() << ")" << std::endl;
      64             : 
      65             :   // check serialize/deserialize
      66           6 :   for (std::size_t i = 0; i < type.size(); ++i)
      67             :   {
      68           8 :     std::string s = type.serialize(i);
      69           4 :     std::cout << "serialize(" << i << ") = " << type.serialize(i) << std::endl;
      70           4 :     std::size_t j = type.deserialize(s);
      71           4 :     BOOST_CHECK(i == j);
      72             :   }
      73             : 
      74             :   // check print/parse
      75           6 :   for (std::size_t i = 0; i < type.size(); ++i)
      76             :   {
      77           8 :     std::string s = type.print(i);
      78           4 :     std::cout << "print(" <<  i << ") = " << s << std::endl;
      79           4 :     std::size_t j = type.parse(s);
      80           4 :     std::cout << "parse(" <<  s << ") = " << j << std::endl;
      81             :   }
      82             : 
      83             :   // test iterator
      84           2 :   std::size_t index = 0;
      85           6 :   for (auto i = type.index_begin(); i != type.index_end(); ++i)
      86             :   {
      87           4 :     std::cout << "iterator " << index << " -> " << *i << std::endl;
      88           4 :     BOOST_CHECK(*i == index);
      89           4 :     index++;
      90             :   }
      91           2 : }
      92             : 
      93           2 : void test_ltsmin(const lps::specification& lpsspec, const std::string& filename, const std::string& rewriter_strategy)
      94             : {
      95           4 :   lps::pins p(filename, rewriter_strategy);
      96           2 :   std::size_t N = p.process_parameter_count();
      97             : 
      98           2 :   BOOST_CHECK(p.process_parameter_count() == 11);
      99             : 
     100           2 :   std::size_t G = p.guard_count();
     101             : 
     102           2 :   BOOST_CHECK(G == 13);
     103           2 :   BOOST_CHECK(p.guard_parameters(0).size() == 1);
     104           2 :   BOOST_CHECK(p.guard_info(5).size() == 2);
     105             :   // Check below is removed as the result is unpredictable, since processes are put into a set instead of
     106             :   // a vector. The result below depends on the ordering in which process identifiers are stored in memory.
     107             :   // BOOST_CHECK(p.guard_name(0) == "s1_S == 2" || p.guard_name(0) == "s1_S == 1");
     108             : 
     109           2 :   BOOST_CHECK(p.edge_label_count() == 1);
     110           4 :   for (std::size_t i = 0; i < p.edge_label_count(); i++)
     111             :   {
     112           2 :     BOOST_CHECK(p.edge_label_type(i) == p.datatype_count() - 1);
     113             :   }
     114             : 
     115           4 :   std::set<data::sort_expression> params;
     116          24 :   for (const data::variable& v: lpsspec.process().process_parameters())
     117             :   {
     118          22 :     params.insert(v.sort());
     119             :   }
     120           2 :   BOOST_CHECK(p.datatype_count() == params.size() + 1);
     121           2 :   BOOST_CHECK(p.group_count() == 10);
     122             : 
     123           2 :   std::size_t index = 0;
     124          24 :   for (const data::variable& v: lpsspec.process().process_parameters())
     125             :   {
     126          22 :         const lps::pins_data_type& type = p.data_type(p.process_parameter_type(index++));
     127          22 :         BOOST_CHECK(type.name() == data::pp(v.sort()));
     128             :   }
     129             : 
     130             :   // get the initial state
     131           2 :   state_vector initial_state = new int[N];
     132           2 :   state_vector dest_state = new int[N];
     133           2 :   int* labels = new int[p.edge_label_count()];
     134           2 :   p.get_initial_state(initial_state);
     135           2 :   std::cout << print_state(initial_state, N, "initial state: ") << std::endl;
     136             : 
     137             :   // find all successors of the initial state
     138           2 :   state_callback_function f_all(p.process_parameter_count());
     139           2 :   p.next_state_all(initial_state, f_all, dest_state, labels);
     140           2 :   std::cout << "f_all.state_count = " << f_all.state_count << std::endl;
     141             : 
     142             :   // find successors of the initial state for individual groups
     143           2 :   std::size_t count = 0;
     144          22 :   for (std::size_t group = 0; group < p.group_count(); group++)
     145             :   {
     146          20 :     state_callback_function f_long(p.process_parameter_count());
     147          20 :     p.next_state_long(initial_state, group, f_long, dest_state, labels);
     148          20 :     std::cout << "group " << group << " count = " << f_long.state_count << std::endl;
     149          20 :     count += f_long.state_count;
     150             :   }
     151           2 :   BOOST_CHECK(count == f_all.state_count);
     152             : 
     153             :   // find successors (without evaluating condition) of the initial state for individual groups
     154           2 :   count = 0;
     155          22 :   for (std::size_t group = 0; group < p.group_count(); group++)
     156             :   {
     157             : 
     158          20 :     std::size_t all_true = p.GUARD_TRUE;
     159          40 :     for(std::size_t guard = 0; guard < p.guard_info(group).size() && all_true == p.GUARD_TRUE; guard++) {
     160          20 :       all_true = p.eval_guard_long(initial_state, p.guard_info(group)[guard]);
     161             :     }
     162             : 
     163          20 :     if (all_true == p.GUARD_TRUE) {
     164           4 :       state_callback_function f_long(p.process_parameter_count());
     165           4 :       p.update_long(initial_state, group, f_long, dest_state, labels);
     166           4 :       std::cout << "group " << group << " count = " << f_long.state_count << std::endl;
     167           4 :       count += f_long.state_count;
     168             :     }
     169             :   }
     170           2 :   BOOST_CHECK(count == f_all.state_count);
     171             : 
     172           2 :   lps::pins_data_type& action_label_type = p.data_type(p.datatype_count() - 1);
     173           2 :   test_data_type(action_label_type);
     174             : 
     175           2 :   delete[] initial_state;
     176           2 :   delete[] dest_state;
     177           2 :   delete[] labels;
     178             : 
     179           2 :   std::cout << p.info() << std::endl;
     180             : 
     181             :   // test summand_action_names()
     182           2 :   std::cout << "--- summand action names ---" << std::endl;
     183          22 :   for (std::size_t i = 0; i < p.group_count(); i++)
     184             :   {
     185          20 :     std::cout << i << " {";
     186          40 :     std::set<std::string> s = p.summand_action_names(i);
     187          40 :     for (auto j = s.begin(); j != s.end(); ++j)
     188             :     {
     189          20 :       if (j != s.begin())
     190             :       {
     191           0 :         std::cout << ", ";
     192             :       }
     193          20 :       std::cout << *j;
     194             :     }
     195          20 :     std::cout << "}" << std::endl;
     196             :   }
     197           2 : }
     198             : 
     199           1 : void test_ltsmin()
     200             : {
     201           2 :   lps::specification abp_spec = remove_stochastic_operators(lps::linearise(lps::detail::ABP_SPECIFICATION()));
     202           2 :   std::string abp_filename = "temporary_abp.lps";
     203           1 :   save_lps(abp_spec, abp_filename);
     204           1 :   test_ltsmin(abp_spec, abp_filename, "jitty");
     205             : #ifdef MCRL2_JITTYC_AVAILABLE
     206           1 :   test_ltsmin(abp_spec, abp_filename, "jittyc");
     207             : #endif // MCRL2_JITTYC_AVAILABLE
     208           1 :   std::remove(abp_filename.c_str());
     209           1 : }
     210             : 
     211             : template <typename Iter>
     212           6 : std::string print_vector(Iter first, Iter last)
     213             : {
     214          12 :   std::ostringstream out;
     215           6 :   out << "[";
     216           8 :   for (Iter i = first; i != last; ++i)
     217             :   {
     218           2 :     if (i != first)
     219             :     {
     220           0 :       out << ", ";
     221             :     }
     222           2 :     out << *i;
     223             :   }
     224           6 :   out << "]";
     225          12 :   return out.str();
     226             : }
     227             : 
     228             : template <typename Container>
     229           6 : std::string print_vector(const Container& c)
     230             : {
     231           6 :   return print_vector(c.begin(), c.end());
     232             : }
     233             : 
     234             : inline
     235             : std::string read_groups(const lps::pins& p)
     236             : {
     237             :   std::ostringstream out;
     238             :   for (std::size_t i = 0; i < p.group_count(); i++)
     239             :   {
     240             :     out << print_vector(p.read_group(i)) << std::endl;
     241             :   }
     242             :   return out.str();
     243             : }
     244             : 
     245             : inline
     246             : std::string write_groups(const lps::pins& p)
     247             : {
     248             :   std::ostringstream out;
     249             :   for (std::size_t i = 0; i < p.group_count(); i++)
     250             :   {
     251             :     out << print_vector(p.write_group(i)) << std::endl;
     252             :   }
     253             :   return out.str();
     254             : }
     255             : 
     256             : inline
     257             : std::string update_groups(const lps::pins& p)
     258             : {
     259             :   std::ostringstream out;
     260             :   for (std::size_t i = 0; i < p.group_count(); i++)
     261             :   {
     262             :     out << print_vector(p.update_group(i)) << std::endl;
     263             :   }
     264             :   return out.str();
     265             : }
     266             : 
     267             : inline
     268           1 : void test_dependency_matrix()
     269             : {
     270             :   std::string ONEBIT =
     271             :     "proc P(b: Bool) =          \n"
     272             :     "       tau . P(b = false); \n"
     273             :     "                           \n"
     274           2 :     "init P(true);              \n"
     275             :     ;
     276             : 
     277           2 :   lps::specification spec = lps::parse_linear_process_specification(ONEBIT);
     278           2 :   std::string filename = "temporary_onebit.lps";
     279           1 :   save_lps(spec, filename);
     280           2 :   lps::pins p(filename, "jitty");
     281             : 
     282           2 :   for (std::size_t i = 0; i < p.group_count(); i++)
     283             :   {
     284           1 :     std::cout << "\n";
     285           1 :     std::cout << "  read_group(" << i << ") = " << print_vector(p.read_group(i)) << std::endl;
     286           1 :     std::cout << " write_group(" << i << ") = " << print_vector(p.write_group(i)) << std::endl;
     287           1 :     std::cout << "update_group(" << i << ") = " << print_vector(p.update_group(i)) << std::endl;
     288             :   }
     289           1 :   BOOST_CHECK(print_vector(p.read_group(0)) == "[]");
     290           1 :   BOOST_CHECK(print_vector(p.write_group(0)) == "[0]");
     291           1 :   BOOST_CHECK(print_vector(p.update_group(0)) == "[]");
     292             : 
     293             :   // cleanup temporary files
     294           1 :   std::remove(filename.c_str());
     295           1 : }
     296             : 
     297             : inline
     298           1 : void test_serialisation()
     299             : {
     300             :   std::string EXAMPLE  =
     301             :     "sort Piece = struct Red | Yellow | None;   \n"
     302             :     "                                           \n"
     303             :     "proc P(i: Pos, j: Nat, p: Piece) =         \n"
     304             :     "       tau . P(i = 1, j = 0, p = Red);     \n"
     305             :     "                                           \n"
     306           2 :     "init P(1, 1, None);                        \n"
     307             :     ;
     308             : 
     309           2 :   lps::specification spec = lps::parse_linear_process_specification(EXAMPLE);
     310           2 :   std::string filename = "temporary_onebit.lps";
     311           1 :   save_lps(spec, filename);
     312           2 :   lps::pins p1(filename, "jitty");
     313           2 :   lps::pins p2(filename, "jitty");
     314           1 :   std::cout << "datatypes: " << p1.datatype_count() << std::endl;
     315           5 :   for(std::size_t i=0; i < p1.datatype_count(); i++)
     316             :   {
     317           4 :     std::cout << i << ": " << p1.data_type(i).name() << std::endl;
     318             :   }
     319           2 :   std::vector<std::pair<std::string, std::size_t>> expressions;
     320           7 :   expressions.push_back(std::make_pair("1", 0));
     321           1 :   expressions.push_back(std::make_pair("0", 1));
     322           1 :   expressions.push_back(std::make_pair("1", 1));
     323           3 :   expressions.push_back(std::make_pair("Red", 2));
     324           3 :   expressions.push_back(std::make_pair("Yellow", 2));
     325             : 
     326           6 :   for(auto e : expressions)
     327             :   {
     328          10 :     std::string s = e.first;
     329           5 : std::cerr << "STRING " << s << "\n";
     330           5 :     std::size_t type = e.second;
     331           5 : std::cerr << "TYPE " << type << "\n";
     332             : 
     333          10 :     data::data_expression d1 = data::parse_data_expression(s, spec.data());
     334           5 : std::cerr << "DATA EXPRESSION " << d1 << "\n";
     335          10 :     std::string serialised = p1.data_type(type).serialize(p1.data_type(type)[d1]);
     336          10 :     data::data_expression d2(p2.data_type(type).get(p2.data_type(type).deserialize(serialised)));
     337           5 :     std::cout << "string:     " << s << std::endl;
     338           5 :     std::cout << "expression: " << d1 << std::endl;
     339           5 :     std::cout << "serialised: " << serialised << std::endl;
     340           5 :     std::cout << "result:     " << d2 << std::endl;
     341           5 :     BOOST_CHECK(d1==d2);
     342             :   }
     343             : 
     344             :   // cleanup temporary files
     345           1 :   std::remove(filename.c_str());
     346           1 : }
     347             : 
     348           3 : BOOST_AUTO_TEST_CASE(test_main)
     349             : {
     350           1 :   test_dependency_matrix();
     351           1 :   test_serialisation();
     352           1 :   test_ltsmin();
     353           4 : }

Generated by: LCOV version 1.13