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 specification_test.cpp 10 : /// \brief Add your file description here. 11 : 12 : #define BOOST_TEST_MODULE specification_test 13 : #include <boost/test/included/unit_test.hpp> 14 : 15 : #include "mcrl2/lps/detail/test_input.h" 16 : #include "mcrl2/lps/find.h" 17 : #include "mcrl2/lps/linearise.h" 18 : #include "mcrl2/lps/parse.h" 19 : #include "mcrl2/lps/print.h" 20 : 21 : using namespace mcrl2; 22 : using namespace mcrl2::data; 23 : using namespace mcrl2::lps; 24 : 25 1 : void test_find_sort_expressions() 26 : { 27 2 : specification spec=remove_stochastic_operators(linearise(lps::detail::ABP_SPECIFICATION())); 28 1 : std::set<sort_expression> s; 29 1 : lps::find_sort_expressions(spec, std::inserter(s, s.end())); 30 1 : std::cout << core::detail::print_set(s) << std::endl; 31 1 : } 32 : 33 1 : void test_system_defined_sorts() 34 : { 35 : const std::string SPEC( 36 : "act a;\n\n" 37 : "proc X(i,j: Nat) = (i == 5) -> a. X(i,j);\n\n" 38 1 : "init X(0,1);\n"); 39 : 40 1 : specification spec=remove_stochastic_operators(linearise(SPEC)); 41 1 : function_symbol_vector r = spec.data().constructors(data::sort_nat::nat()); 42 1 : BOOST_CHECK(r.size() != 0); 43 1 : } 44 : 45 : // This test is added to demonstrate that context sorts need to be added to 46 : // the data specification of an LPS. If this is not done, the resulting 47 : // LPS is not well typed. 48 1 : void test_context_sorts() 49 : { 50 : std::string text = 51 : "proc P = sum x:Real.(x==x) -> tau.P;\n" 52 1 : "init P;\n" 53 : ; 54 : 55 1 : specification spec = parse_linear_process_specification(text); 56 1 : std::cout << "spec = " << spec << std::endl; 57 1 : BOOST_CHECK(check_well_typedness(spec)); 58 : 59 1 : stochastic_specification sspec; 60 1 : parse_lps(text, sspec); 61 1 : std::cout << "sspec = " << sspec << std::endl; 62 1 : BOOST_CHECK(check_well_typedness(sspec)); 63 1 : } 64 : 65 2 : BOOST_AUTO_TEST_CASE(test_main) 66 : { 67 1 : test_find_sort_expressions(); 68 1 : test_system_defined_sorts(); 69 1 : test_context_sorts(); 70 1 : }