LCOV - code coverage report
Current view: top level - lps/test - stochastic_specification_test.cpp (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 85 85 100.0 %
Date: 2024-03-08 02:52:28 Functions: 28 28 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 stochastic_specification_test.cpp
      10             : /// \brief Add your file description here.
      11             : 
      12             : #define BOOST_TEST_MODULE stochastic_specification_test
      13             : #include <boost/test/included/unit_test.hpp>
      14             : 
      15             : #include "mcrl2/lps/detail/test_input.h"
      16             : #include "mcrl2/lps/is_stochastic.h"
      17             : #include "mcrl2/lps/linearise.h"
      18             : #include "mcrl2/lps/parelm.h"
      19             : #include "mcrl2/lps/parse.h"
      20             : #include "mcrl2/lps/print.h"
      21             : #include "mcrl2/lps/is_well_typed.h"
      22             : 
      23             : using namespace mcrl2;
      24             : using namespace mcrl2::data;
      25             : using namespace mcrl2::lps;
      26             : 
      27           2 : BOOST_AUTO_TEST_CASE(test_empty_distribution)
      28             : {
      29           1 :   stochastic_distribution dist;
      30           1 :   std::cout << "empty dist = " << dist << std::endl;
      31           1 :   BOOST_CHECK(!dist.is_defined());
      32           1 : }
      33             : 
      34           2 : BOOST_AUTO_TEST_CASE(test_remove_stochastic_operators)
      35             : {
      36             :   std::string text =
      37             :     "act a;\n"
      38             :     "proc P = a.P;\n"
      39           1 :     "init P;"
      40             :     ;
      41             : 
      42           1 :   stochastic_specification src;
      43           1 :   parse_lps(text, src);
      44           1 :   BOOST_CHECK(!is_stochastic(src));
      45             : 
      46           1 :   specification dest = remove_stochastic_operators(src);
      47           1 :   std::cout << "dest = " << dest;
      48           1 :   BOOST_CHECK(lps::pp(src) == lps::pp(dest));
      49           1 : }
      50             : 
      51           2 : BOOST_AUTO_TEST_CASE(test_is_stochastic)
      52             : {
      53             :   std::string text =
      54             :     "act  throw: Bool;                       \n"
      55             :     "                                        \n"
      56             :     "proc P = dist b:Bool[1/2].throw(b) . P; \n"
      57             :     "                                        \n"
      58           1 :     "init P;                                 \n"
      59             :     ;
      60           1 :   stochastic_specification spec;
      61           1 :   parse_lps(text, spec);
      62           1 :   BOOST_CHECK(is_stochastic(spec));
      63             : 
      64             :   text =
      65             :     "act  throw: Bool;         \n"
      66             :     "                          \n"
      67             :     "proc P = throw(true) . P; \n"
      68             :     "                          \n"
      69           1 :     "init dist b:Bool[1/2] . P;\n"
      70             :     ;
      71           1 :   parse_lps(text, spec);
      72           1 :   BOOST_CHECK(is_stochastic(spec));
      73           1 : }
      74             : 
      75           2 : BOOST_AUTO_TEST_CASE(test_print)
      76             : {
      77             :   std::string text =
      78             :     "act  a: Bool;\n"
      79             :     "\n"
      80             :     "proc P(s3: Pos, p: Bool) =\n"
      81             :     "       (s3 == 1) ->\n"
      82             :     "         a(p) .\n"
      83             :     "         dist p: Bool[1 / 2] .\n"
      84             :     "         P(s3 = 2, p = true)\n"
      85             :     "     + delta;\n"
      86             :     "\n"
      87           1 :     "init dist p: Bool[1 / 2] . P(1, true);\n"
      88             :     ;
      89           1 :   stochastic_specification spec;
      90           1 :   parse_lps(text, spec);
      91           1 :   std::string result = lps::pp(spec);
      92           1 :   BOOST_CHECK_EQUAL(text, result);
      93           1 : }
      94             : 
      95             : // The following specification did not linearise, due to an infinite loop.
      96           2 : BOOST_AUTO_TEST_CASE(test_linearisation)
      97             : {
      98             :   std::string text =
      99             :     "act a:Bool;\n"
     100             :     "proc X=dist b:Bool[1/2].a(b).X;\n"
     101           1 :     "init X;\n"
     102             :     ;
     103             : 
     104             :   std::string result =
     105             :     "act  a: Bool;\n"
     106             :     "\n"
     107             :     "proc P(b1_X: Bool) =\n"
     108             :     "       a(b1_X) .\n"
     109             :     "         dist b1_X1: Bool[1 / 2] .\n"
     110             :     "         P(b1_X = b1_X1);\n"
     111             :     "\n"
     112           1 :     "init dist b1: Bool[1 / 2] . P(b1);\n"
     113             :     ;
     114             : 
     115           1 :   stochastic_specification spec=linearise(text);
     116           1 :   BOOST_CHECK_EQUAL(lps::pp(spec),result);
     117           1 : }  
     118             : 
     119             : // This test checks whether multiple parameters in a stochastic operator are translated 
     120             : // correctely.
     121           2 : BOOST_AUTO_TEST_CASE(test_multiple_stochastic_parameters)
     122             : {
     123             :   std::string text =
     124             :     "act a:Bool#Bool;\n"
     125             :     "proc X=dist b1,b2:Bool[if(b1,1/8,3/8)].a(b1,b2).X;\n"
     126           1 :     "init X;\n"
     127             :     ;
     128             : 
     129             :   std::string result =
     130             :     "act  a: Bool # Bool;\n"
     131             :     "\n"
     132             :     "proc P(b3_X,b4_X: Bool) =\n"
     133             :     "       a(b3_X, b4_X) .\n"
     134             :     "         dist b3_X1,b4_X1: Bool[if(b3_X1, 1 / 8, 3 / 8)] .\n"
     135             :     "         P(b3_X = b3_X1, b4_X = b4_X1);\n"
     136             :     "\n"
     137           1 :     "init dist b3,b4: Bool[if(b3, 1 / 8, 3 / 8)] . P(b3, b4);\n"
     138             :     ;
     139             : 
     140           1 :   stochastic_specification spec=linearise(text);
     141           1 :   BOOST_CHECK_EQUAL(lps::pp(spec),result);
     142           1 : }  
     143             : 
     144             : // This test checks whether a parameter in a stochastic operator are translated 
     145             : // correctely.
     146           2 : BOOST_AUTO_TEST_CASE(test_properly_change_bound_variables)
     147             : {
     148             :   std::string text =
     149             :     "map distribution: Bool#Pos#Pos->Real;\n"
     150             :     "\n"
     151             :     "act win, lose;\n"
     152             :     "    hold:Bool;\n"
     153             :     "\n"
     154             :     "proc Play(round_: Nat, hold3:Bool, r3: Pos) = \n"
     155             :     "       dist s3:Pos[distribution(hold3, r3, s3)].\n"
     156             :     "         (\n"
     157             :     "            (round_==1) -> lose.delta\n"
     158             :     "                        <>  sum b3: Bool. hold(b3).Play(round_+1, b3, s3 )\n"
     159             :     "        );\n"
     160             :     "\n"
     161           1 :     "init Play(0, false, 1);\n"
     162             : ;
     163             : 
     164             :   std::string result1 =
     165             :     "map  distribution: Bool # Pos # Pos -> Real;\n"
     166             :     "\n"
     167             :     "act  win,lose;\n"
     168             :     "     hold: Bool;\n"
     169             :     "\n"
     170             :     "glob dc: Pos;\n"
     171             :     "     dc1: Nat;\n"
     172             :     "\n"
     173             :     "proc P(s4_Play,s1_Play: Pos, round__Play: Nat) =\n"
     174             :     "       sum b1_Play: Bool.\n"
     175             :     "         (s4_Play == 2 && !(round__Play == 1)) ->\n"
     176             :     "         hold(b1_Play) .\n"
     177             :     "         dist s2_Play: Pos[distribution(b1_Play, s1_Play, s2_Play)] .\n"
     178             :     "         P(s4_Play = 2, s1_Play = s2_Play, round__Play = round__Play + 1)\n"
     179             :     "     + (s4_Play == 2 && round__Play == 1) ->\n"
     180             :     "         lose .\n"
     181             :     "         P(s4_Play = 1, s1_Play = dc, round__Play = dc1)\n"
     182             :     "     + delta;\n"
     183             :     "\n"
     184           1 :     "init dist s1: Pos[distribution(false, 1, s1)] . P(2, s1, 0);\n"
     185             :     ;
     186             : 
     187             :   std::string result2 =
     188             :     "map  distribution: Bool # Pos # Pos -> Real;\n"
     189             :     "\n"
     190             :     "act  win,lose;\n"
     191             :     "     hold: Bool;\n"
     192             :     "\n"
     193             :     "glob dc: Pos;\n"
     194             :     "     dc1: Nat;\n"
     195             :     "\n"
     196             :     "proc P(s4_Play,s1_Play: Pos, round__Play: Nat) =\n"
     197             :     "       sum b1_Play: Bool.\n"
     198             :     "         (s4_Play == 1 && !(round__Play == 1)) ->\n"
     199             :     "         hold(b1_Play) .\n"
     200             :     "         dist s2_Play: Pos[distribution(b1_Play, s1_Play, s2_Play)] .\n"
     201             :     "         P(s4_Play = 1, s1_Play = s2_Play, round__Play = round__Play + 1)\n"
     202             :     "     + (s4_Play == 1 && round__Play == 1) ->\n"
     203             :     "         lose .\n"
     204             :     "         P(s4_Play = 2, s1_Play = dc, round__Play = dc1)\n"
     205             :     "     + delta;\n"
     206             :     "\n"
     207           1 :     "init dist s1: Pos[distribution(false, 1, s1)] . P(1, s1, 0);\n"
     208             :     ;
     209             : 
     210           1 :   stochastic_specification spec=linearise(text);
     211           1 :   BOOST_CHECK(lps::pp(spec)==result1 ||   // The lineariser can up with multiple results, depending on how terms are stored internally. 
     212             :               lps::pp(spec)==result2);
     213           1 : }  
     214             : 
     215             : // This test checks whether the outward distribution of dist operators is going 
     216             : // correctely.
     217           2 : BOOST_AUTO_TEST_CASE(test_push_dist_outward)
     218             : {
     219             :   std::string text =
     220             :     "sort Coin = struct head_ | tail_;\n"
     221             :     "\n"
     222             :     "act throw:Coin;\n"
     223             :     "    success;\n"
     224             :     "\n"
     225             :     "proc X(head_seen:Bool) =  dist c:Coin[1/2].throw(c).\n"
     226             :     "                           ((c==head_ && head_seen) -> success.delta+\n"
     227             :     "                            (c==head_ && !head_seen) -> X(true)+\n"
     228             :     "                            (c==tail_) -> X(false));\n"
     229             :     "\n"
     230           1 :     "init X(false);\n"
     231             :     ;
     232             : 
     233           1 :   stochastic_specification spec=linearise(text);
     234           1 :   BOOST_CHECK(lps::detail::is_well_typed(spec));
     235           1 : }  
     236             : 
     237             : 
     238           2 : BOOST_AUTO_TEST_CASE(test_parelm)
     239             : {
     240           1 :   stochastic_specification spec = linearise(lps::detail::ABP_SPECIFICATION());
     241           1 :   std::set<data::variable> v = lps::find_all_variables(spec);
     242           1 :   parelm(spec);
     243           1 :   BOOST_CHECK(lps::detail::is_well_typed(spec));
     244           1 : }
     245             : 
     246             : /* This test case caused the lineariser to incorrectly handle bound variables in the distribution operator */
     247           2 : BOOST_AUTO_TEST_CASE(bound_variable)
     248             : {
     249             :   std::string text =
     250             :     "act a;\n"
     251           1 :     "init dist x0: Bool[if(x0,1/3,2/3)].(x0 -> (a . dist x1: Bool[1/2].(x1 -> a)));\n";
     252           1 :   stochastic_specification spec=linearise(text);
     253           1 :   BOOST_CHECK(lps::detail::is_well_typed(spec));
     254           1 : }
     255             : 
     256             : /* The following test case requires that the sum operator is distributed over the dist operator.
     257             :  * This is only possible, as it stands for finite domains. */
     258           2 : BOOST_AUTO_TEST_CASE(distributed_sum_over_dist1)
     259             : {
     260             :   std::string text =
     261             :     "act\n"
     262             :     "  c:Bool#Bool;\n"
     263             :     "\n"
     264             :     "proc\n"
     265             :     "  Q = sum b1: Bool. dist x0: Bool[if(x0,1/4,3/4)].c(b1,x0).delta;\n"
     266             :     "  \n"
     267           1 :     "init Q;\n";
     268           1 :   stochastic_specification spec=linearise(text);
     269           1 :   BOOST_CHECK(lps::detail::is_well_typed(spec));
     270           1 : }
     271             : 
     272             : /* A more elaborate example of the previous test case, where there are also distributions
     273             :  * inside the linear process. */
     274           2 : BOOST_AUTO_TEST_CASE(distributed_sum_over_dist2)
     275             : {
     276             :   std::string text =
     277             :     "act  c: Bool # Bool;\n"
     278             :     "  \n"
     279             :     "glob dc,dc1,dc2,dc3: Bool;\n"
     280             :     "\n"
     281             :     "proc P(s1_Q: Pos, x: Bool) = \n"
     282             :     "       (s1_Q == 2) ->\n"
     283             :     "         c(true, x) .\n"
     284             :     "         P(s1_Q = 1, x = dc)\n"
     285             :     "     + delta;\n"
     286             :     "         \n"
     287           1 :     "init dist x: Bool[if(x, 1 / 4, 3 / 4)] . P(2, x);\n";
     288           1 :   stochastic_specification spec=linearise(text);
     289           1 :   BOOST_CHECK(lps::detail::is_well_typed(spec));
     290           1 : }
     291             : 
     292             : /* The following example shows an initial distribution with variables
     293             :  * that are not used in the body. */
     294           2 : BOOST_AUTO_TEST_CASE(non_bound_initial_stochastic_variables)
     295             : {
     296             :   std::string text =
     297             :     "act a;\n"
     298             :     "\n"
     299             :     "proc P = (true -> delta <> (dist x0: Bool[1 / 2] . x0 -> a)) . P;\n"
     300             :     "\n"
     301           1 :     "init P;\n";
     302           1 :   stochastic_specification spec=linearise(text);
     303           1 :   BOOST_CHECK(lps::detail::is_well_typed(spec));
     304           1 : }
     305             : 
     306             : /* The following example was not linearised correctly, as
     307             :    an expression sum x:D.a.P was returned
     308             :    unchanged when P had an initial distribution. 
     309             :  */
     310           2 : BOOST_AUTO_TEST_CASE(distribution_insided_sum_bug)
     311             : {
     312             :   std::string text =
     313             :     "act a,b;\n"
     314             :     "\n"
     315             :     "proc Environment = \n"
     316             :     "        sum realReading: Nat . (realReading<2) ->\n"
     317             :     "            a . EnvironmentSensorProcess;\n"
     318             :     "\n"
     319             :     "proc EnvironmentSensorProcess =\n"
     320             :     "        dist f:Bool[if(f, 1/4, 3/4)].f->b.delta;\n"
     321             :     "\n"
     322           1 :     "init Environment;\n";
     323           1 :   stochastic_specification spec=linearise(text);
     324           1 :   BOOST_CHECK(lps::detail::is_well_typed(spec));
     325           1 : }
     326             : 
     327             : 

Generated by: LCOV version 1.14