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 function_symbol_generator_test.cpp 10 : /// \brief Add your file description here. 11 : 12 : #define BOOST_TEST_MODULE function_symbol_generator_test 13 : #include <boost/test/included/unit_test.hpp> 14 : 15 : #include "mcrl2/atermpp/aterm_io.h" 16 : #include "mcrl2/atermpp/function_symbol_generator.h" 17 : 18 : using namespace atermpp; 19 : 20 2 : BOOST_AUTO_TEST_CASE(test_generator) 21 : { 22 1 : std::string prefix("@"); 23 1 : function_symbol_generator generator(prefix); 24 1 : const function_symbol f = generator(); 25 1 : BOOST_CHECK(f.name().find(prefix) == 0); 26 1 : const function_symbol f1 = generator(); 27 1 : BOOST_CHECK(f1.name().find(prefix) == 0); 28 1 : BOOST_CHECK(f!=f1); 29 1 : const function_symbol f2 = generator(); 30 1 : BOOST_CHECK(f2.name().find(prefix) == 0); 31 1 : BOOST_CHECK(f!=f2); 32 1 : BOOST_CHECK(f1!=f2); 33 : 34 : 35 1 : prefix = "a"; 36 2 : function_symbol a10("a10", 0); 37 1 : function_symbol_generator agenerator(prefix); 38 1 : function_symbol g = agenerator(); 39 1 : BOOST_CHECK(g.name() == "a1_0"); 40 1 : BOOST_CHECK(g.name() != a10.name()); 41 : 42 2 : function_symbol a100("a1_10", 0); 43 1 : g = agenerator(); 44 1 : BOOST_CHECK(g.name() == "a1_11"); 45 : 46 2 : function_symbol_generator zgen("z"); 47 1 : function_symbol q1 = zgen(); 48 1 : zgen.clear(); 49 1 : function_symbol q2 = zgen(); 50 1 : BOOST_CHECK(q1 == q2); 51 1 : std::cout << "q1 == " << q1 << " name = " << q1.name() << " arity = " << q1.arity() << std::endl; 52 1 : std::cout << "q2 == " << q2 << " name = " << q2.name() << " arity = " << q2.arity() << std::endl; 53 1 : }