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 <boost/test/included/unit_test.hpp> 16 : 17 : #include "mcrl2/lps/linearise.h" 18 : 19 : using namespace mcrl2; 20 : using namespace mcrl2::data; 21 : using namespace mcrl2::lps; 22 : 23 : 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 2 : BOOST_AUTO_TEST_CASE(test_main) 32 : { 33 1 : stochastic_specification spec = linearise(SPECIFICATION); 34 1 : 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 1 : }