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 stochastic_linearization_test.cpp
      10             : /// \brief Add your file description here.
      11             : 
      12             : #define BOOST_TEST_MODULE stochastic_linearization_test
      13             : #include <boost/test/included/unit_test.hpp>
      14             : 
      15             : #include "mcrl2/data/detail/rewrite_strategies.h"
      16             : #include "mcrl2/lps/linearise.h"
      17             : 
      18             : using namespace mcrl2;
      19             : using namespace mcrl2::lps;
      20             : 
      21             : typedef data::rewriter::strategy rewrite_strategy;
      22             : typedef std::vector<rewrite_strategy> rewrite_strategy_vector;
      23             : 
      24          30 : void run_linearisation_instance(const std::string& spec, const t_lin_options& options, bool expect_success)
      25             : {
      26          30 :   if (expect_success)
      27             :   {
      28          30 :     lps::stochastic_specification s=linearise(spec, options);
      29          30 :     BOOST_CHECK(s != lps::stochastic_specification());
      30          30 :   }
      31             :   else
      32             :   {
      33           0 :     BOOST_CHECK_THROW(linearise(spec, options), mcrl2::runtime_error);
      34             :   }
      35          30 : }
      36             : 
      37           5 : void run_linearisation_test_case(const std::string& spec, const bool expect_success = true)
      38             : {
      39             :   // Set various rewrite strategies
      40           5 :   rewrite_strategy_vector rewrite_strategies = data::detail::get_test_rewrite_strategies(false);
      41             : 
      42          10 :   for (rewrite_strategy_vector::const_iterator i = rewrite_strategies.begin(); i != rewrite_strategies.end(); ++i)
      43             :   {
      44           5 :     std::clog << std::endl << "Testing with rewrite strategy " << *i << std::endl;
      45             : 
      46           5 :     t_lin_options options;
      47           5 :     options.rewrite_strategy=*i;
      48             : 
      49           5 :     std::clog << "  Default options" << std::endl;
      50           5 :     run_linearisation_instance(spec, options, expect_success);
      51             : 
      52           5 :     std::clog << "  Linearisation method regular2" << std::endl;
      53           5 :     options.lin_method=lmRegular2;
      54           5 :     run_linearisation_instance(spec, options, expect_success);
      55             : 
      56           5 :     std::clog << "  Linearisation method stack" << std::endl;
      57           5 :     options.lin_method=lmStack;
      58           5 :     run_linearisation_instance(spec, options, expect_success);
      59             : 
      60           5 :     std::clog << "  Linearisation method stack; binary enabled" << std::endl;
      61           5 :     options.binary=true;
      62           5 :     run_linearisation_instance(spec, options, expect_success);
      63             : 
      64           5 :     std::clog << "  Linearisation method regular; binary enabled" << std::endl;
      65           5 :     options.lin_method=lmRegular;
      66           5 :     run_linearisation_instance(spec, options, expect_success);
      67             : 
      68           5 :     std::clog << "  Linearisation method regular; no intermediate clustering" << std::endl;
      69           5 :     options.binary=false; // reset binary
      70           5 :     options.no_intermediate_cluster=true;
      71           5 :     run_linearisation_instance(spec, options, expect_success);
      72             :   }
      73           5 : }
      74             : 
      75           2 : BOOST_AUTO_TEST_CASE(Check_that_a_probability_distribution_works_well_in_combination_with_a_nonterminating_initial_process)
      76             : {
      77             :   const std::string spec =
      78             :     "act a:Bool;\n"
      79           1 :     "init dist x:Bool[1/2].a(x);\n";
      80             : 
      81           1 :   run_linearisation_test_case(spec,true);
      82           1 : }
      83             : 
      84           2 : BOOST_AUTO_TEST_CASE(Check_distribution_of_dist_over_plus)
      85             : {
      86             :   const std::string spec =
      87             :     "act a,b:Bool;\n"
      88           1 :     "init dist x:Bool[1/2].a(x).delta+dist y:Bool[1/2].a(y).delta;\n";
      89             : 
      90           1 :   run_linearisation_test_case(spec,true);
      91           1 : }
      92             : 
      93           2 : BOOST_AUTO_TEST_CASE(Check_distribution_of_dist_over_sum)
      94             : {
      95             :   const std::string spec =
      96             :     "act a:Bool#Bool;\n"
      97           1 :     "init dist x:Bool[1/2].sum y:Bool.a(x,y).delta;\n";
      98             : 
      99           1 :   run_linearisation_test_case(spec,true);
     100           1 : }
     101             : 
     102             : // The test below represents a problem as the variables that were moved
     103             : // to the front were not properly renamed. Problem reported by Olav Bunte.
     104           2 : BOOST_AUTO_TEST_CASE(renaming_of_initial_stochastic_variables)
     105             : {
     106             :   const std::string spec =
     107             :     "act\n"
     108             :     "        flip: Bool;\n"
     109             :     "        dice: Nat;\n"
     110             :     "\n"
     111             :     "proc\n"
     112             :     "        COIN(s: Nat, d: Nat) =\n"
     113             :     "                (s == 0) -> dist b1:Bool[1/2].(b1 -> flip(b1).COIN(1,0) <> flip(b1).COIN(2,0))\n"
     114             :     "                <> (s == 1) -> dist b1:Bool[1/2].(b1 -> flip(b1).COIN(3,0) <> flip(b1).COIN(4,0))\n"
     115             :     "                <> (s == 2) -> dist b1:Bool[1/2].(b1 -> flip(b1).COIN(5,0) <> flip(b1).COIN(6,0))\n"
     116             :     "                <> (s == 3) -> dist b1:Bool[1/2].(b1 -> flip(b1).COIN(1,0) <> flip(b1).COIN(7,1))\n"
     117             :     "                <> (s == 4) -> dist b1:Bool[1/2].(b1 -> flip(b1).COIN(7,2) <> flip(b1).COIN(7,3))\n"
     118             :     "                <> (s == 5) -> dist b1:Bool[1/2].(b1 -> flip(b1).COIN(7,4) <> flip(b1).COIN(7,5))\n"
     119             :     "                <> (s == 6) -> dist b1:Bool[1/2].(b1 -> flip(b1).COIN(2,0) <> flip(b1).COIN(7,6))\n"
     120             :     "                <> (s == 7) -> dice(d).COIN(s,d);\n"
     121             :     "\n"
     122           1 :     "init COIN(0, 0);\n";
     123             : 
     124           1 :   run_linearisation_test_case(spec,true);
     125           1 : }
     126             : 
     127             : // Conditions must be incorporated in distributions when distributed over them.
     128             : // Problem indicated by Tim Willemse.
     129           2 : BOOST_AUTO_TEST_CASE(distribution_of_conditions_over_dist_operator)
     130             : {
     131             :   const std::string spec =
     132             :     "act a:Nat;\n"
     133             :     "\n"
     134             :     "proc P(m:Nat)=\n"
     135             :     "         (m==2) -> dist n:Nat[if(n<m,1/2,0)].a(n).P(m+1);\n"
     136             :     "\n"
     137           1 :     "init P(2);\n";
     138             : 
     139           1 :   run_linearisation_test_case(spec,true);
     140           1 : }   
     141             : 
     142             :