LCOV - code coverage report
Current view: top level - data/test - linear_inequalities_test.cpp (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 174 191 91.1 %
Date: 2024-03-08 02:52:28 Functions: 11 11 100.0 %
Legend: Lines: hit not hit

          Line data    Source code
       1             : // Author(s): 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 linear_inequalities_test.cpp
      10             : /// \brief Test the linear_inequality functionality.
      11             : 
      12             : #define BOOST_TEST_MODULE linear_inequalities_test
      13             : #include <boost/test/included/unit_test.hpp>
      14             : 
      15             : #include "mcrl2/data/fourier_motzkin.h"
      16             : #include "mcrl2/data/join.h"
      17             : #include "mcrl2/data/parse.h"
      18             : 
      19             : 
      20             : using namespace mcrl2;
      21             : using namespace mcrl2::core;
      22             : using namespace mcrl2::data;
      23             : 
      24          12 : void check(bool result, std::string message)
      25             : {
      26          12 :   if(!result) {
      27           0 :     std::cout << message << std::endl;
      28             :   }
      29          12 :   BOOST_CHECK(result);
      30          12 : }
      31             : 
      32           1 : void test_linear_inequality()
      33             : {
      34           1 :   data_specification data_spec;
      35           1 :   data_spec.add_context_sort(sort_real::real_());
      36           1 :   rewriter rewr(data_spec);
      37             : 
      38           2 :   variable vx("x", sort_real::real_());
      39           2 :   variable vy("y", sort_real::real_());
      40           1 :   linear_inequality li;
      41           1 :   data_expression expr;
      42             : 
      43           1 :   expr = less(real_zero(), real_zero());
      44           1 :   li = linear_inequality(expr, rewr);
      45           1 :   check(li.is_false(rewr), "Expected " + pp(expr) + "' to be false");
      46           1 :   check(li.lhs().empty(), "Expected left hand side of '" + pp(expr) + "' to be empty " + pp(li.lhs()));
      47             : 
      48           1 :   expr = less_equal(real_zero(), real_zero());
      49           1 :   li = linear_inequality(expr, rewr);
      50           1 :   check(li.is_true(rewr), "Expected '" + pp(expr) + "' to be true");
      51           1 :   check(li.lhs().empty(), "Expected left hand side of '" + pp(expr) + "' to be empty");
      52             : 
      53           1 :   expr = less_equal(sort_real::minus(vx, vx), real_one());
      54           1 :   li = linear_inequality(expr, rewr);
      55           1 :   check(li.is_true(rewr), "Expected '" + pp(expr) + "' to be true");
      56           1 :   check(li.lhs().empty(), "Expected left hand side of '" + pp(expr) + "' to be empty");
      57             : 
      58           1 :   expr = less_equal(sort_real::minus(vx, vx), real_one());
      59           1 :   li = linear_inequality(expr, rewr);
      60           1 :   check(li.is_true(rewr), "Expected '" + pp(expr) + "' to be true");
      61           1 :   check(li.lhs().empty(), "Expected left hand side of '" + pp(expr) + "' to be empty");
      62             : 
      63           1 :   expr = less_equal(sort_real::plus(vx, vy), vx);
      64           1 :   li = linear_inequality(expr, rewr);
      65           1 :   check(!li.is_true(rewr), "Expected '" + pp(expr) + "' to not be true");
      66           1 :   check(!li.lhs().empty(), "Expected left hand side of '" + pp(expr) + "' not to be empty");
      67           1 :   check(li.transform_to_data_expression() == less_equal(sort_real::times(real_one(), vy), real_zero()),
      68           2 :     "Expression '" + pp(expr) + "' parsing/output problem " + pp(li.transform_to_data_expression()));
      69             : 
      70           1 :   bool got_exception = false;
      71             :   try
      72             :   {
      73           1 :     expr = not_equal_to(vx, vy);
      74           1 :     li = linear_inequality(expr, rewr);
      75             :   }
      76           1 :   catch(const mcrl2::runtime_error&)
      77             :   {
      78           1 :     got_exception = true;
      79           1 :   }
      80           1 :   check(got_exception, "Expected an exception while parsing x != y.");
      81           1 : }
      82             : 
      83          47 : void split_conjunction_of_inequalities_set(const data_expression& e, std::vector < linear_inequality >& v, const rewriter& r)
      84             : {
      85          47 :   if (sort_bool::is_and_application(e))
      86             :   {
      87          19 :     split_conjunction_of_inequalities_set(application(e)[0],v,r);
      88          19 :     split_conjunction_of_inequalities_set(application(e)[1],v,r);
      89             :   }
      90             :   else
      91             :   {
      92          28 :     v.push_back(linear_inequality(e,r));
      93             :   }
      94          47 : }
      95             : 
      96           7 : bool test_consistency_of_inequalities(const std::string& vars,
      97             :                                       const std::string& inequalities,
      98             :                                       const bool expect_consistent)
      99             : {
     100             :   // Take care that reals are part of the data type.
     101           7 :   data_specification data_spec;
     102           7 :   variable_list variables=parse_variables(vars);
     103           7 :   data_spec.add_context_sort(sort_real::real_());
     104           7 :   const data_expression e=parse_data_expression(inequalities,variables,data_spec);
     105             : 
     106           7 :   rewriter r(data_spec);
     107           7 :   std::vector < linear_inequality > v_inequalities;
     108           7 :   split_conjunction_of_inequalities_set(e,v_inequalities,r);
     109             : 
     110           7 :   if (is_inconsistent(v_inequalities,r))
     111             :   {
     112           2 :     if (expect_consistent)
     113             :     {
     114           0 :       std::cout << "Expected consistent, found inconsistent\n";
     115           0 :       std::cout << variables << ": " << inequalities << "\n";
     116           0 :       std::cout << "Internal inequalities: " << pp_vector(v_inequalities) << "\n";
     117           0 :       return false;
     118             :     }
     119             :   }
     120             :   else
     121             :   {
     122           5 :     if (!expect_consistent)
     123             :     {
     124           0 :       std::cout << "Expected inconsistent, found consistent\n";
     125           0 :       std::cout << variables << ": " << inequalities << "\n";
     126           0 :       std::cout << "Internal inequalities: " << pp_vector(v_inequalities) << "\n";
     127           0 :       return false;
     128             :     }
     129             :   }
     130           7 :   return true;
     131           7 : }
     132             : 
     133           2 : bool test_application_of_Fourier_Motzkin(const std::string& vars,
     134             :                                          const std::string& variables_to_be_eliminated,
     135             :                                          const std::string& inequalities,
     136             :                                          const std::string& inconsistent_with,
     137             :                                          bool check_consistent = false)
     138             : {
     139             :   // Take care that reals are part of the data type.
     140           2 :   data_specification data_spec;
     141           2 :   data_spec.add_context_sort(sort_real::real_());
     142           2 :   const variable_list variables=parse_variables(vars);
     143           2 :   const data_expression e_in=parse_data_expression(inequalities,variables,data_spec);
     144           2 :   const variable_list v_elim= data::detail::parse_variables(variables_to_be_eliminated);
     145             : 
     146           2 :   rewriter r(data_spec);
     147           2 :   std::vector < linear_inequality > v_inequalities;
     148           2 :   split_conjunction_of_inequalities_set(e_in,v_inequalities,r);
     149             : 
     150           2 :   std::vector < linear_inequality> resulting_inequalities;
     151           2 :   fourier_motzkin(v_inequalities, v_elim.begin(), v_elim.end(), resulting_inequalities, r);
     152             : 
     153           2 :   std::vector < linear_inequality> inconsistent_inequalities=resulting_inequalities;
     154           2 :   inconsistent_inequalities.push_back(linear_inequality(parse_data_expression(inconsistent_with,variables,data_spec),r));
     155           2 :   if (!(check_consistent ^ is_inconsistent(inconsistent_inequalities,r, false)))
     156             :   {
     157           0 :     std::cout << "Expected set of inequations to be " << (check_consistent ? "" : "in") << "consistent with given inequality after applying Fourier-Motzkin elimination\n";
     158           0 :     std::cout << "Input: " << variables << ": " << inequalities << "\n";
     159           0 :     std::cout << "Parsed input : " << pp_vector(v_inequalities) << "\n";
     160           0 :     std::cout << "Variables to be eliminated: " << v_elim << "\n";
     161           0 :     std::cout << "Input after applying Fourier Motzkin: " << pp_vector(resulting_inequalities) << "\n";
     162           0 :     std::cout << "Should be " << (check_consistent ? "" : "in") << "consistent with " << inconsistent_with << "\n";
     163           0 :     std::cout << (check_consistent ? "Consistent" : "Inconsistent")  << " inequality after parsing " << pp(linear_inequality(parse_data_expression(inconsistent_with,variables,data_spec),r)) << "\n";
     164           0 :     return false;
     165             :   }
     166           2 :   return true;
     167           2 : }
     168             : 
     169           1 : void test_high_level_fourier_motzkin()
     170             : {
     171           1 :   data_specification data_spec;
     172           1 :   data_spec.add_context_sort(sort_real::real_());
     173           1 :   rewriter rewr(data_spec);
     174           2 :   variable vx("x", sort_real::real_());
     175           2 :   variable vy("y", sort_real::real_());
     176             : 
     177           2 :   data_expression expr = sort_bool::and_(equal_to(vx, vy), less(vy, sort_real::real_(2)));
     178           3 :   variable_list elim_vars({variable("y", sort_real::real_())});
     179           1 :   data_expression out;
     180           1 :   variable_list vars_out;
     181           1 :   fourier_motzkin(expr, elim_vars, out, vars_out, rewr);
     182             : 
     183           1 :   BOOST_CHECK(vars_out.empty());
     184           1 :   BOOST_CHECK(out == less(sort_real::times(real_one(), vx), sort_real::real_(2)));
     185           1 : }
     186             : 
     187           1 : void test_high_level_fourier_motzkin_non_linear()
     188             : {
     189           1 :   data_specification data_spec;
     190           1 :   data_spec.add_context_sort(sort_real::real_());
     191           1 :   rewriter rewr(data_spec);
     192           2 :   variable vx("x", sort_real::real_());
     193             : 
     194           2 :   data_expression expr = less(sort_real::times(vx,vx), sort_real::real_(0));
     195           2 :   variable_list elim_vars({vx});
     196           1 :   data_expression out;
     197           1 :   variable_list vars_out;
     198           1 :   fourier_motzkin(expr, elim_vars, out, vars_out, rewr);
     199             : 
     200             :   // Fourier Motzkin should fail, because the expression is not linear
     201             :   // Original result should be returned
     202           1 :   BOOST_CHECK(vars_out == elim_vars);
     203           1 :   BOOST_CHECK(out == expr);
     204           1 : }
     205             : 
     206           6 : void split_conditions_helper(const std::string& vars,
     207             :                              const std::string& expr,
     208             :                              std::vector< data_expression_list >& real_conditions,
     209             :                              std::vector< data_expression >& non_real_conditions)
     210             : {
     211           6 :   data_specification data_spec;
     212           6 :   data_spec.add_context_sort(sort_real::real_());
     213           6 :   const variable_list variables=parse_variables(vars);
     214           6 :   const data_expression e_in=parse_data_expression(expr,variables,data_spec);
     215             : 
     216           6 :   data::detail::split_condition(e_in, real_conditions, non_real_conditions);
     217           6 : }
     218             : 
     219           1 : void test_split_conditions()
     220             : {
     221           1 :   std::vector < data_expression_list > real_conditions;
     222           1 :   std::vector < data_expression > non_real_conditions;
     223             : 
     224           1 :   split_conditions_helper("x,y:Real, a,b,c:Bool;", "a && b", real_conditions, non_real_conditions);
     225           1 :   BOOST_CHECK(real_conditions.size() == 1);
     226           1 :   BOOST_CHECK(non_real_conditions.size() == 1);
     227           1 :   BOOST_CHECK(real_conditions[0].size() == 0);
     228           1 :   BOOST_CHECK(sort_bool::is_and_application(non_real_conditions[0]));
     229           1 :   real_conditions.clear(); non_real_conditions.clear();
     230             : 
     231           1 :   split_conditions_helper("x,y:Real, a,b,c:Bool;", "(a || b) && c", real_conditions, non_real_conditions);
     232           1 :   BOOST_CHECK(real_conditions.size() == 1);
     233           1 :   BOOST_CHECK(non_real_conditions.size() == 1);
     234           1 :   BOOST_CHECK(real_conditions[0].size() == 0);
     235           1 :   BOOST_CHECK(sort_bool::is_and_application(non_real_conditions[0]));
     236           1 :   BOOST_CHECK(sort_bool::is_or_application(sort_bool::left(non_real_conditions[0])));
     237           1 :   real_conditions.clear(); non_real_conditions.clear();
     238             : 
     239           1 :   split_conditions_helper("x,y:Real, a,b,c:Bool;", "(a || b) && x < 5", real_conditions, non_real_conditions);
     240           1 :   BOOST_CHECK(real_conditions.size() == 1);
     241           1 :   BOOST_CHECK(non_real_conditions.size() == 1);
     242           1 :   BOOST_CHECK(real_conditions[0].size() == 1);
     243           1 :   BOOST_CHECK(is_less_application(real_conditions[0].front()));
     244           1 :   BOOST_CHECK(sort_bool::is_or_application(non_real_conditions[0]));
     245           1 :   real_conditions.clear(); non_real_conditions.clear();
     246             : 
     247           1 :   split_conditions_helper("x,y:Real, a,b,c:Bool;", "(a || b) && (x == 3 || y > 4)", real_conditions, non_real_conditions);
     248           1 :   BOOST_CHECK(real_conditions.size() == 2);
     249           1 :   BOOST_CHECK(non_real_conditions.size() == 2);
     250           1 :   BOOST_CHECK(real_conditions[0].size() == 1);
     251           1 :   BOOST_CHECK(real_conditions[1].size() == 1);
     252           1 :   BOOST_CHECK((is_equal_to_application(real_conditions[0].front()) && is_greater_application(real_conditions[1].front())) ||
     253             :               (is_equal_to_application(real_conditions[1].front()) && is_greater_application(real_conditions[0].front())));
     254           1 :   BOOST_CHECK(non_real_conditions[0] == non_real_conditions[1]);
     255           1 :   real_conditions.clear(); non_real_conditions.clear();
     256             : 
     257           1 :   split_conditions_helper("x,y:Real, a,b,c:Bool;", "(x == y || y < 0) && (x == 3 || y > 4)", real_conditions, non_real_conditions);
     258           1 :   BOOST_CHECK(real_conditions.size() == 4);
     259           1 :   BOOST_CHECK(non_real_conditions.size() == 4);
     260           5 :   for(int i = 0; i < 4; i++)
     261             :   {
     262           4 :     BOOST_CHECK(real_conditions[i].size() == 2);
     263           4 :     BOOST_CHECK(non_real_conditions[i] == sort_bool::true_());
     264             :   }
     265           1 :   real_conditions.clear(); non_real_conditions.clear();
     266             : 
     267           1 :   split_conditions_helper("x,y:Real, a,b,c:Bool;", "(x == y || a) && (x == 3 || b)", real_conditions, non_real_conditions);
     268           1 :   BOOST_CHECK(real_conditions.size() == 4);
     269           1 :   BOOST_CHECK(non_real_conditions.size() == 4);
     270           5 :   for(int i = 0; i < 4; i++)
     271             :   {
     272           4 :     std::set< data_expression > split_without_true = split_and(non_real_conditions[i]);
     273           4 :     split_without_true.erase(sort_bool::true_());
     274           4 :     BOOST_CHECK(real_conditions[i].size() + split_without_true.size() == 2);
     275           4 :   }
     276           1 :   real_conditions.clear(); non_real_conditions.clear();
     277           1 : }
     278             : 
     279           2 : BOOST_AUTO_TEST_CASE(test_main)
     280             : {
     281           1 :   test_linear_inequality();
     282           1 :   test_split_conditions();
     283             : 
     284           1 :   BOOST_CHECK(test_consistency_of_inequalities("x:Real;", "x<3  && x>=4", false));
     285           1 :   BOOST_CHECK(test_consistency_of_inequalities("x:Real;", "x<3  && x>=2", true));
     286           1 :   BOOST_CHECK(test_consistency_of_inequalities("x:Real;", "x<3  && x>=3", false));
     287           1 :   BOOST_CHECK(test_consistency_of_inequalities("x:Real;", "x<=3  && x>=3", true));
     288           1 :   BOOST_CHECK(test_consistency_of_inequalities("u:Real;","0 <= u && -u <= -4 && -u < 0",true));
     289           1 :   BOOST_CHECK(test_consistency_of_inequalities("u,t:Real;","u + -t <= 1 && -u <= -4 && t < u && -u < 0 && -t <= 0 ",true));
     290           1 :   BOOST_CHECK(test_consistency_of_inequalities("u,t,l:Real;","u + -t <= 1 && -u <= -4 && -u + l < 0 && -u < 0 && -t <= 0 && -l + t <= 0",true));
     291             : 
     292           1 :   BOOST_CHECK(test_application_of_Fourier_Motzkin("x,y:Real;", "y:Real;", "-y + x < 0 &&  y < 2", "x>=2"));
     293           1 :   BOOST_CHECK(test_application_of_Fourier_Motzkin("cup1,cup2,add:Real;", "add:Real;", "add <= 2 && 0 <= add && cup2 + 2 - add <= cup1 + add && 3 < cup1 + add - 2", "cup2 - cup1 >= 2", true));
     294           1 :   test_high_level_fourier_motzkin();
     295           1 :   test_high_level_fourier_motzkin_non_linear();
     296           1 : }

Generated by: LCOV version 1.14