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 compatibility_test.cpp
      10             : /// \brief Regression test for the transformations between new and old data
      11             : ///       format.
      12             : 
      13             : #define BOOST_TEST_MODULE compatibility_test
      14             : #include <boost/test/included/unit_test.hpp>
      15             : 
      16             : #include "mcrl2/core/parse.h"
      17             : #include "mcrl2/data/data_io.h"
      18             : #include "mcrl2/data/parse.h"
      19             : 
      20             : using namespace mcrl2;
      21             : 
      22           1 : void compatibility_test()
      23             : {
      24             :   std::stringstream data_stream(
      25             :     "sort S;\n"
      26             :     "cons s:S;\n"
      27             :     "map f:S -> List(S);\n"
      28           2 :   );
      29             : 
      30           1 :   std::string text = utilities::read_text(data_stream);
      31           1 :   atermpp::aterm_appl data_spec_aterm = data::detail::data_specification_to_aterm(data::detail::parse_data_specification_new(text));
      32           1 :   if (data_spec_aterm == atermpp::aterm())
      33             :   {
      34           0 :     throw mcrl2::runtime_error("Error while parsing data specification");
      35             :   }
      36           1 :   data::data_specification data_spec(data_spec_aterm);
      37           1 :   data::typecheck_data_specification(data_spec);
      38             : 
      39             :   atermpp::aterm_appl data_spec_aterm_new =
      40             :     mcrl2::data::detail::data_specification_to_aterm(
      41             :       data_spec
      42             :       // mcrl2::data::remove_all_system_defined(
      43             :       // mcrl2::data::data_specification(data_spec_aterm)
      44             :       // )
      45           1 :     );
      46             : 
      47           1 :   BOOST_CHECK(data_spec_aterm == data_spec_aterm_new);
      48           1 : }
      49             : 
      50           2 : BOOST_AUTO_TEST_CASE(test_main)
      51             : {
      52           1 :   compatibility_test();
      53           1 : }