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 lps_algorithm_test.cpp
      10             : /// \brief Add your file description here.
      11             : 
      12             : #define BOOST_TEST_MODULE lps_algorithm_test
      13             : #include <boost/test/included/unit_test.hpp>
      14             : 
      15             : #include "mcrl2/lps/detail/lps_algorithm.h"
      16             : #include "mcrl2/lps/linearise.h"
      17             : 
      18             : 
      19             : using namespace mcrl2;
      20             : using namespace mcrl2::lps;
      21             : using namespace mcrl2::lps::detail;
      22             : 
      23             : std::string SPECIFICATION =
      24             :   "% This file contains the alternating bit protocol, as described in W.J.    \n"
      25             :   "% Fokkink, J.F. Groote and M.A. Reniers, Modelling Reactive Systems.       \n"
      26             :   "%                                                                          \n"
      27             :   "% The only exception is that the domain D consists of two data elements to \n"
      28             :   "% facilitate simulation.                                                   \n"
      29             :   "                                                                           \n"
      30             :   "sort                                                                       \n"
      31             :   "  D     = struct d1 | d2;                                                  \n"
      32             :   "  Error = struct e;                                                        \n"
      33             :   "                                                                           \n"
      34             :   "act                                                                        \n"
      35             :   "  r1,s4: D;                                                                \n"
      36             :   "  s2,r2,c2: D # Bool;                                                      \n"
      37             :   "  s3,r3,c3: D # Bool;                                                      \n"
      38             :   "  s3,r3,c3: Error;                                                         \n"
      39             :   "  s5,r5,c5: Bool;                                                          \n"
      40             :   "  s6,r6,c6: Bool;                                                          \n"
      41             :   "  s6,r6,c6: Error;                                                         \n"
      42             :   "  i;                                                                       \n"
      43             :   "                                                                           \n"
      44             :   "proc                                                                       \n"
      45             :   "  S(b:Bool)     = sum d:D. r1(d).T(d,b);                                   \n"
      46             :   "  T(d:D,b:Bool) = s2(d,b).(r6(b).S(!b)+(r6(!b)+r6(e)).T(d,b));             \n"
      47             :   "                                                                           \n"
      48             :   "  R(b:Bool)     = sum d:D. r3(d,b).s4(d).s5(b).R(!b)+                      \n"
      49             :   "                  (sum d:D.r3(d,!b)+r3(e)).s5(!b).R(b);                    \n"
      50             :   "                                                                           \n"
      51             :   "  K             = sum d:D,b:Bool. r2(d,b).(i.s3(d,b)+i.s3(e)).K;           \n"
      52             :   "                                                                           \n"
      53             :   "  L             = sum b:Bool. r5(b).(i.s6(b)+i.s6(e)).L;                   \n"
      54             :   "                                                                           \n"
      55             :   "init                                                                       \n"
      56             :   "  allow({r1,s4,c2,c3,c5,c6,i},                                             \n"
      57             :   "    comm({r2|s2->c2, r3|s3->c3, r5|s5->c5, r6|s6->c6},                     \n"
      58             :   "        S(true) || K || L || R(true)                                       \n"
      59             :   "    )                                                                      \n"
      60             :   "  );                                                                       \n";
      61             : 
      62             : 
      63           1 : void test_remove_unused_summand_variables()
      64             : {
      65           1 :   specification spec = remove_stochastic_operators(linearise(SPECIFICATION));
      66           1 :   lps::detail::lps_algorithm<> algorithm(spec);
      67           1 :   algorithm.remove_unused_summand_variables();
      68           1 : }
      69             : 
      70           2 : BOOST_AUTO_TEST_CASE(test_main)
      71             : {
      72           1 :   test_remove_unused_summand_variables();
      73           1 : }