LCOV - code coverage report
Current view: top level - bes/test - gauss_elimination_test.cpp (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 100 108 92.6 %
Date: 2019-09-14 00:54:39 Functions: 13 13 100.0 %
Legend: Lines: hit not hit

          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 gauss_elimination_test.cpp
      10             : /// \brief Gauss elimination tests.
      11             : 
      12             : #define BOOST_TEST_MODULE gauss_elimination_test
      13             : #define MCRL2_GAUSS_ELIMINATION_DEBUG
      14             : 
      15             : #include "mcrl2/bes/gauss_elimination.h"
      16             : #include "mcrl2/data/rewriter.h"
      17             : #include "mcrl2/lps/detail/test_input.h"
      18             : #include "mcrl2/lps/linearise.h"
      19             : #include "mcrl2/modal_formula/parse.h"
      20             : #include "mcrl2/pbes/lps2pbes.h"
      21             : #include "mcrl2/pbes/pbes.h"
      22             : #include "mcrl2/pbes/pbes_gauss_elimination.h"
      23             : #include "mcrl2/pbes/replace.h"
      24             : #include "mcrl2/pbes/rewriter.h"
      25             : #include "mcrl2/pbes/txt2pbes.h"
      26             : #include <boost/algorithm/string.hpp>
      27             : #include <boost/test/included/unit_test_framework.hpp>
      28             : #include <iostream>
      29             : #include <iterator>
      30             : #include <utility>
      31             : 
      32             : using namespace mcrl2;
      33             : using namespace mcrl2::pbes_system;
      34             : 
      35           1 : std::string BES1 =
      36             :   "pbes mu X = X;                                           \n"
      37             :   "                                                         \n"
      38             :   "init X;                                                  \n"
      39             :   ;
      40             : 
      41           1 : std::string BES2 =
      42             :   "pbes nu X = X;                                           \n"
      43             :   "                                                         \n"
      44             :   "init X;                                                  \n"
      45             :   ;
      46             : 
      47           1 : std::string BES3 =
      48             :   "pbes mu X = Y;                                           \n"
      49             :   "     nu Y = X;                                           \n"
      50             :   "                                                         \n"
      51             :   "init X;                                                  \n"
      52             :   ;
      53             : 
      54           1 : std::string BES4 =
      55             :   "pbes nu Y = X;                                           \n"
      56             :   "     mu X = Y;                                           \n"
      57             :   "                                                         \n"
      58             :   "init X;                                                  \n"
      59             :   ;
      60             : 
      61           1 : std::string BES5 =
      62             :   "pbes mu X1 = X2;                                         \n"
      63             :   "     nu X2 = X1 || X3;                                   \n"
      64             :   "     mu X3 = X4 && X5;                                   \n"
      65             :   "     nu X4 = X1;                                         \n"
      66             :   "     nu X5 = X1 || X3;                                   \n"
      67             :   "                                                         \n"
      68             :   "init X1;                                                 \n"
      69             :   ;
      70             : 
      71           1 : std::string BES6 =
      72             :   "pbes nu X1 = X2 && X1;                                   \n"
      73             :   "     mu X2 = X1 || X3;                                   \n"
      74             :   "     nu X3 = X3;                                         \n"
      75             :   "                                                         \n"
      76             :   "init X1;                                                 \n"
      77             :   ;
      78             : 
      79           1 : std::string BES7 =
      80             :   "pbes nu X1 = X2 && X3;                                   \n"
      81             :   "     nu X2 = X4 && X5;                                   \n"
      82             :   "     nu X3 = true;                                       \n"
      83             :   "     nu X4 = false;                                      \n"
      84             :   "     nu X5 = X6;                                         \n"
      85             :   "     nu X6 = X5;                                         \n"
      86             :   "                                                         \n"
      87             :   "init X1;                                                 \n"
      88             :   ;
      89             : 
      90           1 : std::string BES8 =
      91             :   "pbes nu X1 = X2 && X1;                                   \n"
      92             :   "     mu X2 = X1;                                         \n"
      93             :   "                                                         \n"
      94             :   "init X1;                                                 \n"
      95             :   ;
      96             : 
      97           1 : std::string BES9 =
      98             :   "pbes mu X = false;                                       \n"
      99             :   "                                                         \n"
     100             :   "init X;                                                  \n"
     101             :   ;
     102             : 
     103           1 : std::string BES10 =
     104             :   "pbes nu X = false;                                       \n"
     105             :   "                                                         \n"
     106             :   "init X;                                                  \n"
     107             :   ;
     108             : 
     109          10 : void test_bes(const std::string& bes_spec, bool expected_result)
     110             : {
     111          20 :   pbes_system::pbes p = pbes_system::txt2pbes(bes_spec);
     112          10 :   int result = pbes_system::gauss_elimination(p);
     113          10 :   switch (result)
     114             :   {
     115             :     case 0:
     116           6 :       std::cout << "FALSE" << std::endl;
     117           6 :       break;
     118             :     case 1:
     119           4 :       std::cout << "true" << std::endl;
     120           4 :       break;
     121             :     case 2:
     122           0 :       std::cout << "UNKNOWN" << std::endl;
     123           0 :       break;
     124             :   }
     125          10 :   BOOST_CHECK((!expected_result && result == 0) || (expected_result && result == 1));
     126             : 
     127             :   // BOOST_CHECK(pbes2bool(p) == expected_result);
     128             :   // this gives assertion failures in pbes2bool
     129             : 
     130          10 : }
     131             : 
     132           1 : void test_bes_examples()
     133             : {
     134           1 :   test_bes(BES1, false);
     135           1 :   test_bes(BES2, true);
     136           1 :   test_bes(BES3, false);
     137           1 :   test_bes(BES4, true);
     138           1 :   test_bes(BES5, false);
     139           1 :   test_bes(BES6, true);
     140           1 :   test_bes(BES7, false);
     141           1 :   test_bes(BES8, true);
     142           1 :   test_bes(BES9, false);
     143           1 :   test_bes(BES10, false);
     144           1 : }
     145             : 
     146           1 : void test_abp()
     147             : {
     148           1 :   bool timed = false;
     149           2 :   std::string FORMULA = "[true*]<true*>true";
     150           2 :   lps::specification spec=remove_stochastic_operators(lps::linearise(lps::detail::ABP_SPECIFICATION()));
     151           2 :   state_formulas::state_formula formula = state_formulas::parse_state_formula(FORMULA, spec);
     152             : 
     153           2 :   pbes_system::pbes p = pbes_system::lps2pbes(spec, formula, timed);
     154           1 :   int result = pbes_system::gauss_elimination(p);
     155           1 :   switch (result)
     156             :   {
     157             :     case 0:
     158           0 :       std::cout << "FALSE" << std::endl;
     159           0 :       break;
     160             :     case 1:
     161           1 :       std::cout << "true" << std::endl;
     162           1 :       break;
     163             :     case 2:
     164           0 :       std::cout << "UNKNOWN" << std::endl;
     165           0 :       break;
     166             :   }
     167             : 
     168           1 : }
     169             : 
     170           1 : void test_bes()
     171             : {
     172             :   using namespace bes;
     173             : 
     174           2 :   boolean_variable X("X");
     175           2 :   boolean_variable Y("Y");
     176             : 
     177             :   // empty boolean equation system
     178           2 :   std::vector<boolean_equation> empty;
     179             : 
     180           2 :   pbes_system::fixpoint_symbol mu = pbes_system::fixpoint_symbol::mu();
     181           2 :   pbes_system::fixpoint_symbol nu = pbes_system::fixpoint_symbol::nu();
     182             : 
     183             :   // pbes mu X = X;
     184             :   //
     185             :   // init X;
     186           2 :   boolean_equation e1(mu, X, X);
     187           2 :   boolean_equation_system bes1(empty, X);
     188           1 :   bes1.equations().push_back(e1);
     189             : 
     190             :   // pbes nu X = X;
     191             :   //
     192             :   // init X;
     193           2 :   boolean_equation e2(nu, X, X);
     194           2 :   boolean_equation_system bes2(empty, X);
     195           1 :   bes2.equations().push_back(e2);
     196             : 
     197             :   // pbes mu X = Y;
     198             :   //      nu Y = X;
     199             :   //
     200             :   // init X;
     201           2 :   boolean_equation e3(mu, X, Y);
     202           2 :   boolean_equation e4(nu, Y, X);
     203           2 :   boolean_equation_system bes3(empty, X);
     204           1 :   bes3.equations().push_back(e3);
     205           1 :   bes3.equations().push_back(e4);
     206             : 
     207             :   // pbes nu Y = X;
     208             :   //      mu X = Y;
     209             :   //
     210             :   // init X;
     211           2 :   boolean_equation_system bes4(empty, X);
     212           1 :   bes4.equations().push_back(e4);
     213           1 :   bes4.equations().push_back(e3);
     214             : 
     215           1 :   BOOST_CHECK(!gauss_elimination(bes1));
     216           1 :   BOOST_CHECK(gauss_elimination(bes2));
     217           1 :   BOOST_CHECK(!gauss_elimination(bes3));
     218           1 :   BOOST_CHECK(gauss_elimination(bes4));
     219           1 : }
     220             : 
     221             : inline
     222           3 : bool compare(const pbes_system::pbes_expression& x, const pbes_system::pbes_expression& y)
     223             : {
     224           3 :   return x == y;
     225             : }
     226             : 
     227             : typedef bool (*compare_function)(const pbes_system::pbes_expression& x, const pbes_system::pbes_expression& y);
     228             : 
     229           1 : void test_approximate()
     230             : {
     231             :   using namespace pbes_system;
     232             :   typedef core::term_traits<pbes_expression> tr;
     233             : 
     234             :   gauss_elimination_algorithm<pbes_traits> algorithm;
     235           2 :   pbes_system::pbes p = pbes_system::txt2pbes(BES4);
     236           1 :   algorithm.run(p.equations().begin(), p.equations().end(), approximate<pbes_traits, compare_function > (compare));
     237           1 :   if (tr::is_false(p.equations().front().formula()))
     238             :   {
     239           0 :     std::cout << "FALSE" << std::endl;
     240             :   }
     241           1 :   else if (tr::is_true(p.equations().front().formula()))
     242             :   {
     243           1 :     std::cout << "true" << std::endl;
     244             :   }
     245             :   else
     246             :   {
     247           0 :     std::cout << "UNKNOWN" << std::endl;
     248             :   }
     249           1 : }
     250             : 
     251             : // simple solver that only works if the PBES is a BES
     252             : struct fixpoint_equation_solver
     253             : {
     254             : 
     255           2 :   void operator()(pbes_equation& e) const
     256             :   {
     257           4 :     pbes_expression phi = e.symbol().is_mu() ? false_() : true_();
     258           2 :     e.formula() = replace_propositional_variables(e.formula(), propositional_variable_substitution(e.variable(), phi));
     259           2 :   }
     260             : };
     261             : 
     262           1 : void tutorial1()
     263             : {
     264             :   using namespace pbes_system;
     265             : 
     266             :   std::string txt =
     267             :     "pbes nu Y = X; \n"
     268             :     "     mu X = Y; \n"
     269             :     "               \n"
     270           2 :     "init X;        \n"
     271             :     ;
     272           2 :   pbes p = txt2pbes(txt);
     273             :   gauss_elimination_algorithm<pbes_traits> algorithm;
     274           1 :   algorithm.run(p.equations().begin(), p.equations().end(), fixpoint_equation_solver());
     275           1 : }
     276             : 
     277           1 : void tutorial2()
     278             : {
     279             :   using namespace pbes_system;
     280             : 
     281             :   std::string txt =
     282             :     "pbes mu X = X; \n"
     283             :     "               \n"
     284           2 :     "init X;        \n"
     285             :     ;
     286           2 :   pbes p = txt2pbes(txt);
     287           1 :   int solution = gauss_elimination(p);
     288           1 :   assert(solution == 0); // 0 indicates false
     289           1 : }
     290             : 
     291           3 : BOOST_AUTO_TEST_CASE(test_main)
     292             : {
     293           1 :   test_bes();
     294           1 :   test_abp();
     295           1 :   test_bes_examples();
     296           1 :   test_approximate();
     297           1 :   tutorial1();
     298           1 :   tutorial2();
     299           4 : }

Generated by: LCOV version 1.12