LCOV - code coverage report
Current view: top level - lps/test - data_specification_test.cpp (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 7 7 100.0 %
Date: 2020-07-04 00:44:36 Functions: 4 4 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 data_specification_test.cpp
      10             : /// \brief Test for data specifications. This test belongs to the data
      11             : /// library, but unfortunately the data library contains no parser for
      12             : /// data specifications.
      13             : 
      14             : #define BOOST_TEST_MODULE data_specification_test
      15             : #include "mcrl2/lps/linearise.h"
      16             : 
      17             : #include <boost/test/included/unit_test_framework.hpp>
      18             : 
      19             : using namespace mcrl2;
      20             : using namespace mcrl2::data;
      21             : using namespace mcrl2::lps;
      22             : 
      23           1 : const std::string SPECIFICATION =
      24             :   "act a;                                  \n"
      25             :   "                                        \n"
      26             :   "proc P(b:Bool) = a. P(b);               \n"
      27             :   "                                        \n"
      28             :   "init P(false);                          \n"
      29             :   ;
      30             : 
      31           3 : BOOST_AUTO_TEST_CASE(test_main)
      32             : {
      33           2 :   stochastic_specification spec = linearise(SPECIFICATION);
      34           2 :   data_specification data = spec.data();
      35           1 :   BOOST_CHECK(data.is_certainly_finite(sort_bool::bool_()));
      36           1 :   BOOST_CHECK(!data.is_certainly_finite(sort_nat::nat()));
      37           4 : }

Generated by: LCOV version 1.13