Line data    Source code

       1             : // Author(s): Jan Friso Groote
       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 linearization_test.cpp
      10             : /// \brief A test of the linearizer, comparing the result with the expected state space modulo strong bisimulation. 
      11             : 
      12             : #define BOOST_TEST_MODULE linearization_instantiation_compare_probabilistic_test
      13             : 
      14             : #include <boost/test/included/unit_test.hpp>
      15             : 
      16             : #include "mcrl2/utilities/test_utilities.h"
      17             : 
      18             : #include "mcrl2/data/detail/rewrite_strategies.h"
      19             : 
      20             : #include "mcrl2/lps/linearise.h"
      21             : #include "mcrl2/lts/detail/liblts_pbisim_grv.h"
      22             : #include "mcrl2/lts/state_space_generator.h"
      23             : #include "mcrl2/lts/stochastic_lts_builder.h"
      24             : 
      25             : using namespace mcrl2;
      26             : using namespace mcrl2::lps;
      27             : 
      28             : typedef data::rewriter::strategy rewrite_strategy;
      29             : typedef std::vector<rewrite_strategy> rewrite_strategy_vector;
      30             : 
      31             : template <class LTS_TYPE>
      32             : inline
      33           6 : LTS_TYPE translate_lps_to_lts(const lps::stochastic_specification& specification)
      34             : {
      35           6 :   lps::explorer_options options;
      36           6 :   options.trace_prefix = "linearization_instantiation_compare_test";
      37           6 :   options.search_strategy = lps::es_breadth;
      38           6 :   options.save_at_end = true;
      39           6 :   const std::string& output_filename = utilities::temporary_filename("linearization_instantiation_probabilistic_compare_test_file");
      40             : 
      41           6 :   LTS_TYPE result;
      42           6 :   lts::state_space_generator<true, false, lps::stochastic_specification> generator(specification, options);
      43           6 :   auto builder = create_stochastic_lts_builder(specification, options, result.type());
      44           6 :   generator.explore(*builder);
      45           6 :   builder->save(output_filename);
      46             : 
      47           6 :   result.load(output_filename); 
      48          12 :   return result;
      49           6 : }
      50             : 
      51             : static
      52           6 : void run_linearisation_instance(const std::string& spec, const t_lin_options& options, const lts::probabilistic_lts_aut_t& expected_statespace)
      53             : {
      54           6 :   std::clog << "  Linearisation method " << options.lin_method << std::endl
      55           6 :             << "    rewrite strategy: " << options.rewrite_strategy << std::endl
      56           6 :             << "    binary: " << std::boolalpha << options.binary << std::endl
      57           6 :             << "    nocluster: " << std::boolalpha << options.no_intermediate_cluster << std::endl;
      58             : 
      59           6 :   lps::stochastic_specification s=linearise(spec, options);
      60           6 :   BOOST_CHECK(s != lps::stochastic_specification());
      61             : 
      62           6 :   lts::probabilistic_lts_aut_t result = translate_lps_to_lts<lts::probabilistic_lts_aut_t>(s);
      63          12 :   utilities::execution_timer local_timer("dummy");
      64           6 :   BOOST_CHECK(probabilistic_bisimulation_compare_grv(result, expected_statespace, local_timer));
      65           6 : }
      66             : 
      67             : static
      68           1 : void run_linearisation_test_case(const std::string& spec, const lts::probabilistic_lts_aut_t& expected_statespace)
      69             : {
      70             :   // Set various rewrite strategies
      71           1 :   rewrite_strategy_vector rewrite_strategies = data::detail::get_test_rewrite_strategies(false);
      72             : 
      73           2 :   for (rewrite_strategy_vector::const_iterator i = rewrite_strategies.begin(); i != rewrite_strategies.end(); ++i)
      74             :   {
      75           1 :     t_lin_options options;
      76           1 :     options.rewrite_strategy=*i;
      77             : 
      78           1 :     run_linearisation_instance(spec, options, expected_statespace);
      79             : 
      80           1 :     options.lin_method=lmRegular2;
      81           1 :     run_linearisation_instance(spec, options, expected_statespace);
      82             : 
      83           1 :     options.lin_method=lmStack;
      84           1 :     run_linearisation_instance(spec, options, expected_statespace);
      85             : 
      86           1 :     options.binary=true;
      87           1 :     run_linearisation_instance(spec, options, expected_statespace);
      88             : 
      89           1 :     options.lin_method=lmRegular;
      90           1 :     run_linearisation_instance(spec, options, expected_statespace);
      91             : 
      92           1 :     options.binary=false; // reset binary
      93           1 :     options.no_intermediate_cluster=true;
      94           1 :     run_linearisation_instance(spec, options, expected_statespace);
      95             :   }
      96           1 : }
      97             : 
      98           2 : BOOST_AUTO_TEST_CASE(test_where_renaming_of_variables_goes_astray)
      99             : {
     100             :   const std::string spec =
     101             :       "act step:Bool;\n"
     102             :       "\n"
     103             :       "map f0:Nat->Bool;\n"
     104             :       "var n:Nat;\n"
     105             :       "eqn f0(n)=false;\n"
     106             :       "\n"
     107             :       "proc P(f:Nat->Bool)= step(f(0)). dist b:Bool[1/2].P(f[0->b]);\n"
     108             :       "\n"
     109           1 :       "init sum b:Bool.P(f0[0->b]);\n";
     110             : 
     111             :   const std::string expected_statespace =
     112             :       "des (0,5,4)\n"
     113             :       "(0,\"step(false)\",1 1/2 2)\n"
     114             :       "(0,\"step(true)\",1 1/2 2)\n"
     115             :       "(1,\"step(false)\",3 1/2 2)\n"
     116             :       "(2,\"step(true)\",3 1/2 2)\n"
     117           1 :       "(3,\"step(false)\",3 1/2 2)\n";
     118             : 
     119           1 :   std::stringstream is(expected_statespace);
     120             : 
     121           1 :   lts::probabilistic_lts_aut_t statespace;
     122           1 :   statespace.load(is);
     123           1 :   run_linearisation_test_case(spec,statespace);
     124           1 : }
     125             :