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 specification_property_map_test.cpp
      10             : /// \brief Add your file description here.
      11             : 
      12             : #define BOOST_TEST_MODULE specification_property_map_test
      13             : #include <boost/algorithm/string.hpp>
      14             : #include <boost/test/included/unit_test.hpp>
      15             : 
      16             : #include "mcrl2/lps/detail/specification_property_map.h"
      17             : #include "mcrl2/lps/detail/test_input.h"
      18             : #include "mcrl2/lps/linearise.h"
      19             : #include "mcrl2/lps/parse.h"
      20             : 
      21             : 
      22             : using namespace mcrl2;
      23             : using namespace mcrl2::lps;
      24             : 
      25             : const std::string LPSINFO =
      26             :   "declared_action_label_count  = 21                                                                                                          \n"
      27             :   "declared_action_labels       = c2, c3, c5, c6, i, r1, r2, r3, r5, r6, s2, s3, s4, s5, s6                                                   \n"
      28             :   "declared_free_variable_count = 20                                                                                                          \n"
      29             :   "declared_free_variable_names = dc, dc1, dc10, dc11, dc12, dc13, c14, dc15, dc16, dc17, dc18, dc19, dc2, dc3, dc4, dc5, dc6, dc7, dc8, dc9  \n"
      30             :   "delta_summand_count          = 1                                                                                                           \n"
      31             :   "process_parameter_count      = 11                                                                                                          \n"
      32             :   "process_parameter_names      = b_K, b_L, b_R, b_S, d_K, d_R, d_S, s31_S, s32_K, s33_L, s34_R                                               \n"
      33             :   "summand_count                = 11                                                                                                          \n"
      34             :   "tau_summand_count            = 70                                                                                                          \n"
      35             :   "used_action_label_count      = 19                                                                                                          \n"
      36             :   "used_action_labels           = c2, c3, c5, c6, i, r1, s4                                                                                   \n"
      37             :   "used_free_variable_count     = 15                                                                                                          \n"
      38             :   "used_free_variable_names     = dc1, dc11, dc12, dc13, x15, dc16, dc17, dc18, dc19, dc4, dc5, dc6, dc7, dc8, dc9                            \n"
      39             :   "used_multi_action_count      = 9                                                                                                           \n"
      40             :   "used_multi_actions           = {a1, c2}; {c3}; {c5}; {c6}; {i,j}; {r1}; {s4}                                                               \n"
      41             :   ;
      42             : 
      43           2 : BOOST_AUTO_TEST_CASE(test_main)
      44             : {
      45           2 :   specification spec=remove_stochastic_operators(linearise(lps::detail::ABP_SPECIFICATION()));
      46           1 :   lps::detail::specification_property_map<> info1(spec);
      47           1 :   std::cerr << info1.to_string() << std::endl;
      48           1 :   lps::detail::specification_property_map<> info2(LPSINFO);
      49           1 :   std::cerr << info1.compare(info2) << std::endl;
      50           1 : }