LCOV - code coverage report
Current view: top level - lps/test - linearization_stochastic_test.cpp (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 46 47 97.9 %
Date: 2020-04-01 00:44:46 Functions: 12 12 100.0 %
Legend: Lines: hit not hit

          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_framework.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          24 : void run_linearisation_instance(const std::string& spec, const t_lin_options& options, bool expect_success)
      25             : {
      26          24 :   if (expect_success)
      27             :   {
      28          48 :     lps::stochastic_specification s=linearise(spec, options);
      29          24 :     BOOST_CHECK(s != lps::stochastic_specification());
      30             :   }
      31             :   else
      32             :   {
      33           0 :     BOOST_CHECK_THROW(linearise(spec, options), mcrl2::runtime_error);
      34             :   }
      35          24 : }
      36             : 
      37           4 : void run_linearisation_test_case(const std::string& spec, const bool expect_success = true)
      38             : {
      39             :   // Set various rewrite strategies
      40           8 :   rewrite_strategy_vector rewrite_strategies = data::detail::get_test_rewrite_strategies(false);
      41             : 
      42           8 :   for (rewrite_strategy_vector::const_iterator i = rewrite_strategies.begin(); i != rewrite_strategies.end(); ++i)
      43             :   {
      44           4 :     std::clog << std::endl << "Testing with rewrite strategy " << *i << std::endl;
      45             : 
      46           4 :     t_lin_options options;
      47           4 :     options.rewrite_strategy=*i;
      48             : 
      49           4 :     std::clog << "  Default options" << std::endl;
      50           4 :     run_linearisation_instance(spec, options, expect_success);
      51             : 
      52           4 :     std::clog << "  Linearisation method regular2" << std::endl;
      53           4 :     options.lin_method=lmRegular2;
      54           4 :     run_linearisation_instance(spec, options, expect_success);
      55             : 
      56           4 :     std::clog << "  Linearisation method stack" << std::endl;
      57           4 :     options.lin_method=lmStack;
      58           4 :     run_linearisation_instance(spec, options, expect_success);
      59             : 
      60           4 :     std::clog << "  Linearisation method stack; binary enabled" << std::endl;
      61           4 :     options.binary=true;
      62           4 :     run_linearisation_instance(spec, options, expect_success);
      63             : 
      64           4 :     std::clog << "  Linearisation method regular; binary enabled" << std::endl;
      65           4 :     options.lin_method=lmRegular;
      66           4 :     run_linearisation_instance(spec, options, expect_success);
      67             : 
      68           4 :     std::clog << "  Linearisation method regular; no intermediate clustering" << std::endl;
      69           4 :     options.binary=false; // reset binary
      70           4 :     options.no_intermediate_cluster=true;
      71           4 :     run_linearisation_instance(spec, options, expect_success);
      72             :   }
      73           4 : }
      74             : 
      75           3 : 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           2 :     "init dist x:Bool[1/2].a(x);\n";
      80             : 
      81           1 :   run_linearisation_test_case(spec,true);
      82           1 : }
      83             : 
      84           3 : BOOST_AUTO_TEST_CASE(Check_distribution_of_dist_over_plus)
      85             : {
      86             :   const std::string spec =
      87             :     "act a,b:Bool;\n"
      88           2 :     "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           3 : BOOST_AUTO_TEST_CASE(Check_distribution_of_dist_over_sum)
      94             : {
      95             :   const std::string spec =
      96             :     "act a:Bool#Bool;\n"
      97           2 :     "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           3 : 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           2 :     "init COIN(0, 0);\n";
     123             : 
     124           1 :   run_linearisation_test_case(spec,true);
     125           4 : }
     126             : 

Generated by: LCOV version 1.13