LCOV - code coverage report
Current view: top level - lps/test - print_test.cpp (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 28 28 100.0 %
Date: 2020-07-11 00:44:39 Functions: 10 10 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 print_test.cpp
      10             : /// \brief Test for parser + pretty printer
      11             : 
      12             : #define BOOST_TEST_MODULE print_test
      13             : #include "mcrl2/lps/linearise.h"
      14             : #include "mcrl2/lps/parse.h"
      15             : 
      16             : #include <boost/test/included/unit_test_framework.hpp>
      17             : 
      18             : using namespace mcrl2;
      19             : using namespace mcrl2::lps;
      20             : 
      21           3 : BOOST_AUTO_TEST_CASE(rational)
      22             : {
      23             :   std::string input(
      24             :       "% This is an mCRL2 process specification which can be used for testing\n"
      25             :       "% operations on rational numbers.\n"
      26             :       "\n"
      27             :       "% Tests for unary operations floor, ceil, round, succ, pred, -, abs, succ, pred\n"
      28             :       "act  unary_operations : Real # Int # Int # Int # Real # Real # Real # Real;\n"
      29             :       "proc Test_unary_operations =\n"
      30             :       "       sum x: Int, p: Pos, r: Real. (x >= -5 && x <= 5 && p <= 10 && r == x/p)\n"
      31             :       "       -> unary_operations(r, floor(r), ceil(r), round(r), abs(r), -r, succ(r), pred(r))\n"
      32             :       "       <> delta;\n"
      33             :       "\n"
      34             :       "% Tests for binary operations <, <=, >=, >, max, min, +, -, *, /\n"
      35             :       "act  binary_operations: Real # Real # Bool # Bool # Bool # Bool # Real # Real # Real # Real # Real # Real;\n"
      36             :       "     left_operand: Real;\n"
      37             :       "proc Test_binary_operations =\n"
      38             :       "       sum x: Int, p: Pos, r: Real. (x >= -5 && x <= 5 && p <= 10 && r == x/p) ->\n"
      39             :       "         left_operand(r) .\n"
      40             :       "         (sum y: Int, q: Pos, s: Real. (y >= -5 && y <= 5 && q <= 10 && s == y/q)\n"
      41             :       "         -> binary_operations(r, s, r < s, r <= s, r >= s, r > s, min(r, s), max(r, s), r + s, r - s, r * s, r / s)\n"
      42             :       "         <> delta\n"
      43             :       "         )\n"
      44             :       "       <> delta;\n"
      45             :       "\n"
      46             :       "% Tests for exponentation\n"
      47             :       "act  base: Real;\n"
      48             :       "     exponent: Real # Int # Real;\n"
      49             :       "proc Test_exponentation =\n"
      50             :       "       sum x: Int, p: Pos, r: Real. (x >= -5 && x <= 5 && p <= 10 && r == x/p)\n"
      51             :       "       -> (base(r) . (sum y: Int. (y >= -5 && y <= 5) -> exponent(r, y, exp(r, y)) <> delta))\n"
      52             :       "       <> delta;\n"
      53             :       "\n"
      54             :       "init Test_unary_operations + Test_binary_operations + Test_exponentation;\n"
      55           2 :   );
      56             : 
      57           2 :   specification s=remove_stochastic_operators(linearise(input));
      58             : 
      59           2 :   std::string output;
      60           1 :   output = lps::pp(s);
      61             : 
      62             :   // Check whether the symbol @ occurs in the pretty printed output. If this is
      63             :   // the case, still some internal symbol is exposed. As a result, our parsers
      64             :   // will not be able to handle the specification as input.
      65           1 :   BOOST_CHECK(output.find('@') == std::string::npos);
      66           1 : }
      67             : 
      68           3 : BOOST_AUTO_TEST_CASE(no_summands)
      69             : {
      70           2 :   specification spec;
      71           2 :   std::string s = lps::pp(spec);
      72           1 :   std::cout << "--- no_summands ---\n" << s << std::endl;
      73           1 :   BOOST_CHECK(s.find("delta @ 0") != std::string::npos);
      74           1 : }
      75             : 
      76             : #ifdef MCRL2_PRINT_PROBLEM_CASES
      77             : void test_specification(const std::string& spec_text)
      78             : {
      79             :   specification x = parse_linear_process_specification(spec_text);
      80             : 
      81             :   std::string s1 = lps::pp(x);
      82             :   std::string s2 = lps::print(x);
      83             :   if (s1 != s2)
      84             :   {
      85             :     std::clog << "--- testing spec ---" << std::endl;
      86             :     std::clog << "<pp>   " << s1 << std::endl;
      87             :     std::clog << "<print>" << s2 << std::endl;
      88             :     BOOST_CHECK(s1 == s2);
      89             :   }
      90             : }
      91             : 
      92             : BOOST_AUTO_TEST_CASE(problem_cases)
      93             : {
      94             :   std::string SPEC;
      95             : 
      96             :   SPEC =
      97             :     "act  a: Bool;         \n"
      98             :     "proc P =  a(true) . P;\n"
      99             :     "init P;               \n"
     100             :     ;
     101             :   test_specification(SPEC);
     102             : }
     103             : #endif
     104             : 
     105           3 : BOOST_AUTO_TEST_CASE(ticket_1208)
     106             : {
     107             :   std::string text =
     108             :     "act a:Nat;                  \n"
     109           2 :     "init a(n whr n=m, m=3 end); \n"
     110             :     ;
     111             :   try
     112             :   {
     113           1 :     specification x = parse_linear_process_specification(text);
     114             :   }
     115           2 :   catch (const mcrl2::runtime_error& e)
     116             :   {
     117           2 :     std::string s = e.what();
     118           1 :     BOOST_CHECK(s.find("n whr n=m, m=3 end") != std::string::npos);
     119             :   }
     120           1 : }
     121             : 
     122           3 : BOOST_AUTO_TEST_CASE(ticket_1267)
     123             : {
     124             :   std::string text =
     125             :     "act a: Nat;                                      \n"
     126             :     "proc loop(n: Nat) = a(n) . loop((n + 1) mod 10); \n"
     127           2 :     "init loop(0);                                    \n"
     128             :     ;
     129           2 :   specification x = parse_linear_process_specification(text);
     130           1 :   auto const& a = x.process().action_summands().front().multi_action();
     131           2 :   std::string s = lps::pp(a);
     132           1 :   std::cout << "s = " << s << std::endl;
     133           1 :   BOOST_CHECK(s == "a(n)");
     134           4 : }
     135             : 

Generated by: LCOV version 1.13