text: // Author(s): Wieger Wesselink
  // Copyright: see the accompanying file COPYING or copy at
  // https://github.com/mCRL2org/mCRL2/blob/master/COPYING
  //
  // Distributed under the Boost Software License, Version 1.0.
  // (See accompanying file LICENSE_1_0.txt or copy at
  // http://www.boost.org/LICENSE_1_0.txt)
  //
  /// \file lps_algorithm_test.cpp
  /// \brief Add your file description here.
  
  #define BOOST_TEST_MODULE lps_algorithm_test
  #include "mcrl2/lps/detail/lps_algorithm.h"
  #include "mcrl2/lps/linearise.h"
  
  #include <boost/test/included/unit_test_framework.hpp>
  
  using namespace mcrl2;
  using namespace mcrl2::lps;
  using namespace mcrl2::lps::detail;
  
  std::string SPECIFICATION =
    "% This file contains the alternating bit protocol, as described in W.J.    \n"
    "% Fokkink, J.F. Groote and M.A. Reniers, Modelling Reactive Systems.       \n"
    "%                                                                          \n"
    "% The only exception is that the domain D consists of two data elements to \n"
    "% facilitate simulation.                                                   \n"
    "                                                                           \n"
    "sort                                                                       \n"
    "  D     = struct d1 | d2;                                                  \n"
    "  Error = struct e;                                                        \n"
    "                                                                           \n"
    "act                                                                        \n"
    "  r1,s4: D;                                                                \n"
    "  s2,r2,c2: D # Bool;                                                      \n"
    "  s3,r3,c3: D # Bool;                                                      \n"
    "  s3,r3,c3: Error;                                                         \n"
    "  s5,r5,c5: Bool;                                                          \n"
    "  s6,r6,c6: Bool;                                                          \n"
    "  s6,r6,c6: Error;                                                         \n"
    "  i;                                                                       \n"
    "                                                                           \n"
    "proc                                                                       \n"
    "  S(b:Bool)     = sum d:D. r1(d).T(d,b);                                   \n"
    "  T(d:D,b:Bool) = s2(d,b).(r6(b).S(!b)+(r6(!b)+r6(e)).T(d,b));             \n"
    "                                                                           \n"
    "  R(b:Bool)     = sum d:D. r3(d,b).s4(d).s5(b).R(!b)+                      \n"
    "                  (sum d:D.r3(d,!b)+r3(e)).s5(!b).R(b);                    \n"
    "                                                                           \n"
    "  K             = sum d:D,b:Bool. r2(d,b).(i.s3(d,b)+i.s3(e)).K;           \n"
    "                                                                           \n"
    "  L             = sum b:Bool. r5(b).(i.s6(b)+i.s6(e)).L;                   \n"
    "                                                                           \n"
    "init                                                                       \n"
    "  allow({r1,s4,c2,c3,c5,c6,i},                                             \n"
    "    comm({r2|s2->c2, r3|s3->c3, r5|s5->c5, r6|s6->c6},                     \n"
    "        S(true) || K || L || R(true)                                       \n"
    "    )                                                                      \n"
    "  );                                                                       \n";
  
  
  void test_remove_unused_summand_variables()
  {
    specification spec = remove_stochastic_operators(linearise(SPECIFICATION));
    lps::detail::lps_algorithm<> algorithm(spec);
    algorithm.remove_unused_summand_variables();
  }
  
  BOOST_AUTO_TEST_CASE(test_main)
  {
    test_remove_unused_summand_variables();
  }
  