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 pbes_test.cpp
      10             : /// \brief Add your file description here.
      11             : 
      12             : #define BOOST_TEST_MODULE pbes_test
      13             : #include <boost/test/included/unit_test.hpp>
      14             : 
      15             : #include "mcrl2/lps/detail/test_input.h"
      16             : #include "mcrl2/modal_formula/parse.h"
      17             : #include "mcrl2/pbes/complement.h"
      18             : #include "mcrl2/pbes/detail/instantiate_global_variables.h"
      19             : #include "mcrl2/pbes/is_bes.h"
      20             : #include "mcrl2/pbes/lps2pbes.h"
      21             : #include "mcrl2/pbes/txt2pbes.h"
      22             : 
      23             : using namespace mcrl2;
      24             : using namespace mcrl2::pbes_system;
      25             : 
      26           2 : BOOST_AUTO_TEST_CASE(test_pbes)
      27             : {
      28             :   const std::string SPECIFICATION =
      29             :     "act a:Nat;                               \n"
      30             :     "                                         \n"
      31             :     "map smaller: Nat#Nat -> Bool;            \n"
      32             :     "                                         \n"
      33             :     "var x,y : Nat;                           \n"
      34             :     "                                         \n"
      35             :     "eqn smaller(x,y) = x < y;                \n"
      36             :     "                                         \n"
      37             :     "proc P(n:Nat) = sum m: Nat. a(m). P(m);  \n"
      38             :     "                                         \n"
      39           1 :     "init P(0);                               \n";
      40             : 
      41           1 :   const std::string FORMULA2 = "forall m:Nat. [a(m)]false";
      42             : 
      43           1 :   lps::specification spec = lps::remove_stochastic_operators(lps::linearise(SPECIFICATION));
      44           1 :   state_formulas::state_formula formula = state_formulas::parse_state_formula(FORMULA2, spec, false);
      45           1 :   bool timed = false;
      46           1 :   pbes p = lps2pbes(spec, formula, timed);
      47             : 
      48           1 :   pbes_expression e = p.equations().front().formula();
      49             : 
      50           1 :   BOOST_CHECK(!is_bes(p));
      51           1 :   BOOST_CHECK(!is_bes(e));
      52             : 
      53             :   try
      54             :   {
      55           4 :     load_pbes(p, "non-existing file");
      56           0 :     BOOST_CHECK(false); // loading is expected to fail
      57             :   }
      58           1 :   catch (mcrl2::runtime_error e)
      59             :   {
      60           1 :   }
      61             : 
      62           1 :   std::string filename = "write_term_to_text_stream.pbes";
      63             :   try
      64             :   {
      65           2 :     atermpp::aterm t = atermpp::read_term_from_string("f(x)");
      66           1 :     std::ofstream os;
      67           1 :     os.open(filename.c_str());
      68           1 :     atermpp::write_term_to_text_stream(t, os);
      69           1 :     os.close();
      70           2 :     load_pbes(p, filename);
      71           0 :     BOOST_CHECK(false); // loading is expected to fail
      72           2 :   }
      73           1 :   catch (mcrl2::runtime_error e)
      74             :   {
      75           1 :     remove(filename.c_str());
      76           1 :   }
      77           1 :   filename = "pbes_test_file.pbes";
      78           1 :   save_pbes(p, filename);
      79           1 :   load_pbes(p, filename);
      80           1 :   remove(filename.c_str());
      81           1 : }
      82             : 
      83           2 : BOOST_AUTO_TEST_CASE(test_global_variables)
      84             : {
      85             :   std::string TEXT =
      86             :     "glob k, m, n:Nat;                        \n"
      87             :     "                                         \n"
      88             :     "pbes                                     \n"
      89             :     "   mu X1(n1, m1:Nat) = X2(n1) || X2(m1); \n"
      90             :     "   mu X2(n2:Nat)     = X1(n2, n);        \n"
      91             :     "                                         \n"
      92             :     "init                                     \n"
      93           1 :     "   X1(m, n);                             \n"
      94             :     ;
      95             : 
      96           1 :   pbes p;
      97           1 :   std::stringstream s(TEXT);
      98           1 :   s >> p;
      99           1 :   std::set<data::variable> freevars = p.global_variables();
     100           1 :   BOOST_CHECK(freevars.size() == 3);  // The global variable k does not occur in the specification,
     101             :   // but occurs in the global variables list.
     102           1 : }
     103             : 
     104           2 : BOOST_AUTO_TEST_CASE(test_complement_method_builder)
     105             : {
     106             :   using namespace pbes_system;
     107             : 
     108           2 :   data::variable X("x", data::bool_());
     109           2 :   data::variable Y("y", data::bool_());
     110             : 
     111           2 :   pbes_expression p = or_(and_(X,Y), and_(Y,X));
     112           2 :   pbes_expression q = and_(or_(data::not_(X), data::not_(Y)), or_(data::not_(Y), data::not_(X)));
     113           1 :   std::cout << "p             = " << mcrl2::pbes_system::pp(p) << std::endl;
     114           1 :   std::cout << "q             = " << mcrl2::pbes_system::pp(q) << std::endl;
     115           1 :   std::cout << "complement(p) = " << mcrl2::pbes_system::pp(complement(p)) << std::endl;
     116             : 
     117           1 :   BOOST_CHECK(complement(p) == q);
     118           1 : }
     119             : 
     120           2 : BOOST_AUTO_TEST_CASE(test_pbes_expression)
     121             : {
     122           2 :   data::variable x1("x1", data::basic_sort("X"));
     123           1 :   pbes_expression e = x1;
     124           1 : }
     125             : 
     126           2 : BOOST_AUTO_TEST_CASE(test_trivial)
     127             : {
     128           1 :   const std::string TRIVIAL_FORMULA  = "[true*]<true*>true";
     129           2 :   lps::specification spec = lps::remove_stochastic_operators(lps::linearise(lps::detail::ABP_SPECIFICATION()));
     130           1 :   state_formulas::state_formula formula = state_formulas::parse_state_formula(TRIVIAL_FORMULA, spec, false);
     131           1 :   bool timed = false;
     132           1 :   pbes p = lps2pbes(spec, formula, timed);
     133           1 :   BOOST_CHECK(p.is_well_typed());
     134           1 : }
     135             : 
     136           2 : BOOST_AUTO_TEST_CASE(test_instantiate_global_variables)
     137             : {
     138             :   std::string spec_text =
     139             :     "act a,b:Nat;             \n"
     140             :     "    d;                   \n"
     141             :     "proc P(n:Nat)=a(n).delta;\n"
     142           1 :     "init d.P(1);             \n"
     143             :     ;
     144           1 :   std::string formula_text = "([true*.a(1)]  (mu X.([!a(1)]X && <true> true)))";
     145           1 :   lps::specification spec = lps::remove_stochastic_operators(lps::linearise(spec_text));
     146           1 :   state_formulas::state_formula formula = state_formulas::parse_state_formula(formula_text, spec, false);
     147           1 :   bool timed = false;
     148           1 :   pbes p = lps2pbes(spec, formula, timed);
     149           1 :   std::cout << "<before>" << mcrl2::pbes_system::pp(p) << std::endl;
     150           1 :   std::cout << "<lps>" << lps::pp(spec) << std::endl;
     151           1 :   pbes_system::detail::instantiate_global_variables(p);
     152           1 :   std::cout << "<after>" << pbes_system::pp(p) << std::endl;
     153           1 : }
     154             : 
     155           2 : BOOST_AUTO_TEST_CASE(test_find_sort_expressions)
     156             : {
     157           1 :   const std::string TRIVIAL_FORMULA  = "[true*]<true*>true";
     158           2 :   lps::specification spec = lps::remove_stochastic_operators(lps::linearise(lps::detail::ABP_SPECIFICATION()));
     159           1 :   state_formulas::state_formula formula = state_formulas::parse_state_formula(TRIVIAL_FORMULA, spec, false);
     160           1 :   bool timed = false;
     161           1 :   pbes p = lps2pbes(spec, formula, timed);
     162           1 :   std::set<data::sort_expression> s;
     163           1 :   pbes_system::find_sort_expressions(p, std::inserter(s, s.end()));
     164           1 :   std::cout << core::detail::print_set(s) << std::endl;
     165           1 : }
     166             : 
     167           2 : BOOST_AUTO_TEST_CASE(test_io)
     168             : {
     169             :   using namespace pbes_system;
     170             : 
     171             :   std::string PBES_SPEC =
     172             :     "pbes nu X1 = X2; \n"
     173             :     "     mu X2 = X2; \n"
     174             :     "                 \n"
     175           1 :     "init X1;         \n"
     176             :     ;
     177           1 :   pbes p = txt2pbes(PBES_SPEC);
     178           1 :   save_pbes(p, "pbes.pbes",  pbes_format_internal());
     179           1 :   load_pbes(p, "pbes.pbes",  pbes_format_internal());
     180           1 :   save_pbes(p, "pbes.txt",   pbes_format_text());
     181           1 :   load_pbes(p, "pbes.txt",   pbes_format_text());
     182           1 : }
     183             : 
     184           2 : BOOST_AUTO_TEST_CASE(test_is_bes)
     185             : {
     186             :   // found with random testing 14-1-2011
     187             :   using namespace pbes_system;
     188             :   std::string text =
     189             :     "pbes nu X =       \n"
     190             :     "       val(true); \n"
     191             :     "                  \n"
     192           1 :     "init X;           \n"
     193             :     ;
     194           1 :   pbes p = txt2pbes(text);
     195           1 :   BOOST_CHECK(is_bes(p));
     196           1 : }