Line data    Source code

       1             : // Author(s): Wieger Wesselink, 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 utility.h
      10             : /// \brief Add your file description here.
      11             : 
      12             : #ifndef MCRL2_LPS_TEST_UTILITY_H
      13             : #define MCRL2_LPS_TEST_UTILITY_H
      14             : 
      15             : #include "mcrl2/lps/is_well_typed.h"
      16             : #include "mcrl2/lps/linearise.h"
      17             : 
      18             : typedef data::rewriter::strategy rewrite_strategy;
      19             : typedef std::vector<rewrite_strategy> rewrite_strategy_vector;
      20             : 
      21         474 : void run_linearisation_instance(const std::string& spec, const t_lin_options& options, bool expect_success)
      22             : {
      23         474 :   if (expect_success)
      24             :   {
      25         456 :     BOOST_CHECK(mcrl2::lps::detail::is_well_typed(linearise(spec, options))); 
      26             :   }
      27             :   else
      28             :   {
      29          36 :     BOOST_CHECK_THROW(linearise(spec, options), mcrl2::runtime_error);
      30             :   }
      31         474 : }
      32             : 
      33          79 : void run_linearisation_test_case(const std::string& spec, const bool expect_success = true)
      34             : {
      35             :   // Set various rewrite strategies
      36          79 :   rewrite_strategy_vector rewrite_strategies = data::detail::get_test_rewrite_strategies(false);
      37             : 
      38         158 :   for (rewrite_strategy_vector::const_iterator i = rewrite_strategies.begin(); i != rewrite_strategies.end(); ++i)
      39             :   {
      40          79 :     std::clog << std::endl << "Testing with rewrite strategy " << *i << std::endl;
      41             : 
      42          79 :     t_lin_options options;
      43          79 :     options.rewrite_strategy=*i;
      44             : 
      45          79 :     std::clog << "  Default options" << std::endl;
      46          79 :     run_linearisation_instance(spec, options, expect_success);
      47             : 
      48          79 :     std::clog << "  Linearisation method regular2" << std::endl;
      49          79 :     options.lin_method=lmRegular2;
      50          79 :     run_linearisation_instance(spec, options, expect_success);
      51             : 
      52          79 :     std::clog << "  Linearisation method stack" << std::endl;
      53          79 :     options.lin_method=lmStack;
      54          79 :     run_linearisation_instance(spec, options, expect_success);
      55             : 
      56          79 :     std::clog << "  Linearisation method stack; binary enabled" << std::endl;
      57          79 :     options.binary=true;
      58          79 :     run_linearisation_instance(spec, options, expect_success);
      59             : 
      60          79 :     std::clog << "  Linearisation method regular; binary enabled" << std::endl;
      61          79 :     options.lin_method=lmRegular;
      62          79 :     run_linearisation_instance(spec, options, expect_success);
      63             : 
      64          79 :     std::clog << "  Linearisation method regular; no intermediate clustering" << std::endl;
      65          79 :     options.binary=false; // reset binary
      66          79 :     options.no_intermediate_cluster=true;
      67          79 :     run_linearisation_instance(spec, options, expect_success);
      68             :   }
      69          79 : }
      70             : 
      71             : #endif // MCRL2_LPS_TEST_UTILITY_H