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: 73 73 100.0 %
Date: 2020-07-04 00:44:36 Functions: 26 26 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_framework.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           3 : BOOST_AUTO_TEST_CASE(test_empty_distribution)
      28             : {
      29           2 :   stochastic_distribution dist;
      30           1 :   std::cout << "empty dist = " << dist << std::endl;
      31           1 :   BOOST_CHECK(!dist.is_defined());
      32           1 : }
      33             : 
      34           3 : BOOST_AUTO_TEST_CASE(test_remove_stochastic_operators)
      35             : {
      36             :   std::string text =
      37             :     "act a;\n"
      38             :     "proc P = a.P;\n"
      39           2 :     "init P;"
      40             :     ;
      41             : 
      42           2 :   stochastic_specification src;
      43           1 :   parse_lps(text, src);
      44           1 :   BOOST_CHECK(!is_stochastic(src));
      45             : 
      46           2 :   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           3 : 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           2 :     "init P;                                 \n"
      59             :     ;
      60           2 :   stochastic_specification spec;
      61           1 :   parse_lps(text, spec);
      62           1 :   BOOST_CHECK(is_stochastic(spec));
      63             : 
      64           1 :   text =
      65             :     "act  throw: Bool;         \n"
      66             :     "                          \n"
      67             :     "proc P = throw(true) . P; \n"
      68             :     "                          \n"
      69             :     "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           3 : 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           2 :     "init dist p: Bool[1 / 2] . P(1, true);\n"
      88             :     ;
      89           2 :   stochastic_specification spec;
      90           1 :   parse_lps(text, spec);
      91           2 :   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           3 : 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           2 :     "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           2 :     "init dist b1: Bool[1 / 2] . P(b1);\n"
     113             :     ;
     114             : 
     115           2 :   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           3 : 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           2 :     "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           2 :     "init dist b3,b4: Bool[if(b3, 1 / 8, 3 / 8)] . P(b3, b4);\n"
     138             :     ;
     139             : 
     140           2 :   stochastic_specification spec=linearise(text);
     141           1 :   BOOST_CHECK_EQUAL(lps::pp(spec),result);
     142           1 : }  
     143             : 
     144             : // This test checks whether the outward distribution of dist operators is going 
     145             : // correctely.
     146           3 : BOOST_AUTO_TEST_CASE(test_push_dist_outward)
     147             : {
     148             :   std::string text =
     149             :     "sort Coin = struct head_ | tail_;\n"
     150             :     "\n"
     151             :     "act throw:Coin;\n"
     152             :     "    success;\n"
     153             :     "\n"
     154             :     "proc X(head_seen:Bool) =  dist c:Coin[1/2].throw(c).\n"
     155             :     "                           ((c==head_ && head_seen) -> success.delta+\n"
     156             :     "                            (c==head_ && !head_seen) -> X(true)+\n"
     157             :     "                            (c==tail_) -> X(false));\n"
     158             :     "\n"
     159           2 :     "init X(false);\n"
     160             :     ;
     161             : 
     162           2 :   stochastic_specification spec=linearise(text);
     163           1 :   BOOST_CHECK(lps::detail::is_well_typed(spec));
     164           1 : }  
     165             : 
     166             : 
     167           3 : BOOST_AUTO_TEST_CASE(test_parelm)
     168             : {
     169           2 :   stochastic_specification spec = linearise(lps::detail::ABP_SPECIFICATION());
     170           2 :   std::set<data::variable> v = lps::find_all_variables(spec);
     171           1 :   parelm(spec);
     172           1 :   BOOST_CHECK(lps::detail::is_well_typed(spec));
     173           1 : }
     174             : 
     175             : /* This test case caused the lineariser to incorrectly handle bound variables in the distribution operator */
     176           3 : BOOST_AUTO_TEST_CASE(bound_variable)
     177             : {
     178             :   std::string text =
     179             :     "act a;\n"
     180           2 :     "init dist x0: Bool[if(x0,1/3,2/3)].(x0 -> (a . dist x1: Bool[1/2].(x1 -> a)));\n";
     181           2 :   stochastic_specification spec=linearise(text);
     182           1 :   BOOST_CHECK(lps::detail::is_well_typed(spec));
     183           1 : }
     184             : 
     185             : /* The following test case requires that the sum operator is distributed over the dist operator.
     186             :  * This is only possible, as it stands for finite domains. */
     187           3 : BOOST_AUTO_TEST_CASE(distributed_sum_over_dist1)
     188             : {
     189             :   std::string text =
     190             :     "act\n"
     191             :     "  c:Bool#Bool;\n"
     192             :     "\n"
     193             :     "proc\n"
     194             :     "  Q = sum b1: Bool. dist x0: Bool[if(x0,1/4,3/4)].c(b1,x0).delta;\n"
     195             :     "  \n"
     196           2 :     "init Q;\n";
     197           2 :   stochastic_specification spec=linearise(text);
     198           1 :   BOOST_CHECK(lps::detail::is_well_typed(spec));
     199           1 : }
     200             : 
     201             : /* A more elaborate example of the previous test case, where there are also distributions
     202             :  * inside the linear process. */
     203           3 : BOOST_AUTO_TEST_CASE(distributed_sum_over_dist2)
     204             : {
     205             :   std::string text =
     206             :     "act  c: Bool # Bool;\n"
     207             :     "  \n"
     208             :     "glob dc,dc1,dc2,dc3: Bool;\n"
     209             :     "\n"
     210             :     "proc P(s1_Q: Pos, x: Bool) = \n"
     211             :     "       (s1_Q == 2) ->\n"
     212             :     "         c(true, x) .\n"
     213             :     "         P(s1_Q = 1, x = dc)\n"
     214             :     "     + delta;\n"
     215             :     "         \n"
     216           2 :     "init dist x: Bool[if(x, 1 / 4, 3 / 4)] . P(2, x);\n";
     217           2 :   stochastic_specification spec=linearise(text);
     218           1 :   BOOST_CHECK(lps::detail::is_well_typed(spec));
     219           1 : }
     220             : /* The following example shows an initial distribution with variables
     221             :  * that are not used in the body. */
     222           3 : BOOST_AUTO_TEST_CASE(non_bound_initial_stochastic_variables)
     223             : {
     224             :   std::string text =
     225             :     "act a;\n"
     226             :     "\n"
     227             :     "proc P = (true -> delta <> (dist x0: Bool[1 / 2] . x0 -> a)) . P;\n"
     228             :     "\n"
     229           2 :     "init P;\n";
     230           2 :   stochastic_specification spec=linearise(text);
     231           1 :   BOOST_CHECK(lps::detail::is_well_typed(spec));
     232           4 : }
     233             : 

Generated by: LCOV version 1.13