Line data Source code
1 : // Author(s): Jeroen Keiren 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_equation_test.cpp 10 : /// \brief Basic regression test for data equations. 11 : 12 : #define BOOST_TEST_MODULE data_equation_test 13 : #include <boost/test/included/unit_test.hpp> 14 : 15 : #include "mcrl2/data/data_equation.h" 16 : 17 : using namespace mcrl2; 18 : using namespace mcrl2::data; 19 : 20 1 : void data_equation_test() 21 : { 22 2 : basic_sort s("S"); 23 2 : data::function_symbol c("c", s); 24 2 : data::function_symbol f("f", s); 25 2 : variable x("x", s); 26 2 : variable_list xl = { x }; 27 : 28 1 : data_equation e(xl, c, x, f); 29 1 : BOOST_CHECK(e.variables() == xl); 30 1 : BOOST_CHECK(e.condition() == c); 31 1 : BOOST_CHECK(e.lhs() == x); 32 1 : BOOST_CHECK(e.rhs() == f); 33 1 : } 34 : 35 2 : BOOST_AUTO_TEST_CASE(test_main) 36 : { 37 1 : data_equation_test(); 38 1 : } 39 : 40 :