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 parelm_test.cpp 10 : /// \brief Add your file description here. 11 : 12 : #define BOOST_TEST_MODULE parelm_test 13 : #include <boost/test/included/unit_test.hpp> 14 : 15 : #include "mcrl2/lps/detail/test_input.h" 16 : #include "mcrl2/modal_formula/parse.h" 17 : #include "mcrl2/pbes/complement.h" 18 : #include "mcrl2/pbes/lps2pbes.h" 19 : #include "mcrl2/pbes/parelm.h" 20 : 21 : using namespace mcrl2; 22 : using namespace mcrl2::pbes_system; 23 : 24 : const std::string SPECIFICATION = 25 : "act a:Nat; \n" 26 : " \n" 27 : "map smaller: Nat#Nat -> Bool; \n" 28 : " \n" 29 : "var x,y : Nat; \n" 30 : " \n" 31 : "eqn smaller(x,y) = x < y; \n" 32 : " \n" 33 : "proc P(n:Nat) = sum m: Nat. a(m). P(m); \n" 34 : " \n" 35 : "init P(0); \n"; 36 : 37 : const std::string TRIVIAL_FORMULA = "[true*]<true*>true"; 38 : 39 2 : BOOST_AUTO_TEST_CASE(test_parelm1) 40 : { 41 2 : lps::specification spec = lps::remove_stochastic_operators(lps::linearise(lps::detail::ABP_SPECIFICATION())); 42 1 : state_formulas::state_formula formula = state_formulas::parse_state_formula(TRIVIAL_FORMULA, spec, false); 43 1 : bool timed = false; 44 1 : pbes p = lps2pbes(spec, formula, timed); 45 : pbes_parelm_algorithm algorithm; 46 1 : algorithm.run(p); 47 1 : BOOST_CHECK(p.is_well_typed()); 48 1 : }