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

Generated by: LCOV version 1.12