LCOV - code coverage report
Current view: top level - lps/test - invelm_test.cpp (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 55 55 100.0 %
Date: 2020-07-04 00:44:36 Functions: 9 9 100.0 %
Legend: Lines: hit not hit

          Line data    Source code
       1             : // Author(s): Unknown
       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 invelm_test.cpp
      10             : /// \brief Add your file description here.
      11             : 
      12             : //#define MCRL2_LPS_PARELM_DEBUG
      13             : 
      14             : #define BOOST_TEST_MODULE invelm_test
      15             : #include "mcrl2/lps/invelm_algorithm.h"
      16             : #include "mcrl2/lps/parse.h"
      17             : #include "mcrl2/lps/print.h"
      18             : #include "test_specifications.h"
      19             : 
      20             : #include <boost/test/included/unit_test_framework.hpp>
      21             : 
      22             : using namespace mcrl2;
      23             : 
      24             : inline
      25           4 : lps::specification invelm(const lps::specification& spec,
      26             :                           const data::data_expression& invariant,
      27             :                           bool simplify_all = false,
      28             :                           bool no_elimination = false
      29             :                          )
      30             : {
      31           4 :   lps::specification specification = spec;
      32           4 :   data::rewriter::strategy rewrite_strategy = data::jitty;
      33           4 :   int time_limit = 0;
      34           4 :   bool path_eliminator = false;
      35           4 :   data::detail::smt_solver_type solver_type = mcrl2::data::detail::solver_type_cvc;
      36           4 :   bool apply_induction = false;
      37             : 
      38             :   lps::detail::Invariant_Checker<lps::specification> v_invariant_checker(specification,
      39             :                                                      rewrite_strategy,
      40             :                                                      time_limit,
      41             :                                                      path_eliminator,
      42             :                                                      solver_type,
      43             :                                                      apply_induction,
      44             :                                                      simplify_all
      45           8 :                                                     );
      46           4 :   if (v_invariant_checker.check_invariant(invariant))
      47             :   {
      48             :     lps::invelm_algorithm<lps::specification> algorithm(specification,
      49             :                                     rewrite_strategy,
      50             :                                     time_limit,
      51             :                                     path_eliminator,
      52             :                                     solver_type,
      53             :                                     apply_induction,
      54             :                                     simplify_all
      55           8 :                                    );
      56           4 :     algorithm.run(invariant, !no_elimination);
      57             :   }
      58           8 :   return specification;
      59             : }
      60             : 
      61           3 : BOOST_AUTO_TEST_CASE(test_abp)
      62             : {
      63           2 :   lps::specification specification = lps::parse_linear_process_specification(LINEAR_ABP);
      64           2 :   data::data_expression invariant = data::parse_data_expression("true");
      65             : 
      66           1 :   lps::specification result = invelm(specification, invariant);
      67           1 : }
      68             : 
      69             : template <typename Expr>
      70           4 : bool has_identifier(const Expr& x, const std::string& id)
      71             : {
      72           8 :   std::set<core::identifier_string> ids = lps::find_identifiers(x);
      73           8 :   return ids.find(core::identifier_string(id)) != ids.end();
      74             : }
      75             : 
      76           3 : BOOST_AUTO_TEST_CASE(test_invariant)
      77             : {
      78             :   std::string SPEC =
      79             :     "act a, b, c, d;                         \n"
      80             :     "                                        \n"
      81             :     "proc P(b1, b2: Bool) =                  \n"
      82             :     "       b1 -> a . P(!b1, b2)             \n"
      83             :     "     + b2 -> b . P(true, b1 && b2)      \n"
      84             :     "     + (b1 && b2) -> c . P(false, false)\n"
      85             :     "     + d . P(false, true)               \n"
      86             :     "     + delta;                           \n"
      87             :     "                                        \n"
      88           2 :     "init P(false, true);                    \n"
      89             :     ;
      90             : 
      91           2 :   std::string INVARIANT = "!(b1 && b2)";
      92             : 
      93           2 :   data::data_expression invariant = data::parse_data_expression(INVARIANT, data::parse_variables("b1, b2: Bool;"));
      94           2 :   lps::specification spec = lps::parse_linear_process_specification(SPEC);
      95             :   bool simplify_all;
      96             :   bool no_elimination;
      97           2 :   lps::specification spec1;
      98           2 :   lps::linear_process proc;
      99           1 :   std::cout << lps::pp(spec) << std::endl;
     100             : 
     101           1 :   simplify_all = false;
     102           1 :   no_elimination = false;
     103           1 :   spec1 = invelm(spec, invariant, simplify_all, no_elimination);
     104           1 :   std::cout << lps::pp(spec1) << std::endl;
     105           1 :   proc = spec1.process();
     106           1 :   BOOST_CHECK(proc.action_summands().size() == 3);
     107           1 :   BOOST_CHECK(has_identifier(proc.action_summands()[2], "d"));
     108           1 :   BOOST_CHECK(proc.deadlock_summands().back().condition() == data::sort_bool::true_());
     109             : 
     110           1 :   simplify_all = true;
     111           1 :   no_elimination = false;
     112           1 :   spec1 = invelm(spec, invariant, simplify_all, no_elimination);
     113           1 :   std::cout << lps::pp(spec1) << std::endl;
     114           1 :   proc = spec1.process();
     115           1 :   BOOST_CHECK(proc.action_summands().size() == 3);
     116           1 :   BOOST_CHECK(has_identifier(proc.action_summands()[2], "d"));
     117           1 :   BOOST_CHECK(proc.deadlock_summands().back().condition() != invariant);
     118           1 :   BOOST_CHECK(proc.deadlock_summands().back().condition() != data::sort_bool::true_());
     119           1 :   BOOST_CHECK(has_identifier(proc.deadlock_summands().back().condition(), "b1"));
     120             : 
     121           1 :   simplify_all = true;
     122           1 :   no_elimination = true;
     123           1 :   spec1 = invelm(spec, invariant, simplify_all, no_elimination);
     124           1 :   std::cout << lps::pp(spec1) << std::endl;
     125           1 :   proc = spec1.process();
     126           1 :   BOOST_CHECK(proc.action_summands().size() == 4);
     127           1 :   BOOST_CHECK(has_identifier(proc.action_summands()[2], "c"));
     128           1 :   BOOST_CHECK(proc.deadlock_summands().back().condition() == invariant);
     129           4 : }
     130             : 

Generated by: LCOV version 1.13