LCOV - code coverage report
Current view: top level - pbes/test - typecheck_test.cpp (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 15 18 83.3 %
Date: 2024-03-08 02:52:28 Functions: 5 5 100.0 %
Legend: Lines: hit not hit

          Line data    Source code
       1             : // Author(s): Aad Mathijssen, 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 typecheck_test.cpp
      10             : /// \brief Add your file description here.
      11             : 
      12             : #define BOOST_TEST_MODULE typecheck_test
      13             : #include <boost/test/included/unit_test.hpp>
      14             : #include "mcrl2/core/parse.h"
      15             : #include "mcrl2/pbes/parse.h"
      16             : 
      17             : using namespace mcrl2;
      18             : 
      19           2 : void test_pbes_specification(const std::string& pbes_in, bool test_type_checker = true)
      20             : {
      21           2 :   pbes_system::pbes p = pbes_system::detail::parse_pbes_new(pbes_in).construct_pbes();
      22           2 :   if (test_type_checker)
      23             :   {
      24           2 :     pbes_system::typecheck_pbes(p);
      25           2 :     std::string pbes_out = pbes_system::pp(p);
      26             : 
      27           2 :     if (pbes_in!=pbes_out)
      28             :     {
      29           0 :       std::cerr << "PBES IN AND PBES OUT ARE DIFFERENT (with typechecking).\n";
      30           0 :       std::cerr << "PBES IN: " << pbes_in << "\n";
      31           0 :       std::cerr << "PBES OUT: " << pbes_out << "\n";
      32             :     }
      33           2 :     BOOST_CHECK(pbes_in == pbes_out);
      34           2 :   }
      35           2 : }
      36             : 
      37           2 : BOOST_AUTO_TEST_CASE(test_pbes_specification1)
      38             : {
      39             :   //test PBES specification involving global variables
      40           1 :   test_pbes_specification(
      41             :     "glob dc: Bool;\n"
      42             :     "\n"
      43             :     "pbes nu X(b: Bool) =\n"
      44             :     "       val(b) && X(dc);\n"
      45             :     "\n"
      46             :     "init X(dc);\n"
      47             :   );
      48           1 : }
      49             : 
      50           2 : BOOST_AUTO_TEST_CASE(test_pbes_specification2)
      51             : {
      52             :   //test PBES specification where the type of [10,m] should become List(Nat), not List(Pos).
      53             :   //This failed in revision 10180 and before.
      54           1 :   test_pbes_specification(
      55             :    "pbes nu X0(m: Nat) =\n"
      56             :    "       forall i: Nat. val(!(i < 2)) || X0([10, m] . i);\n"
      57             :    "\n"
      58             :    "init X0(0);\n"
      59             :   );
      60           1 : }

Generated by: LCOV version 1.14