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             : 
      10             : #include "mcrl2/utilities/number_postfix_generator.h"
      11             : 
      12             : #define BOOST_AUTO_TEST_MAIN
      13             : #include <boost/test/included/unit_test.hpp>
      14             : 
      15             : using namespace mcrl2;
      16             : using namespace mcrl2::utilities;
      17             : 
      18           2 : BOOST_AUTO_TEST_CASE(identifier_generator_test)
      19             : {
      20           2 :   number_postfix_generator generator;
      21           1 :   generator.add_identifier("c6");
      22           1 :   std::string s;
      23             : 
      24           1 :   s = generator("c");
      25           1 :   BOOST_CHECK_EQUAL(s, "c7");
      26             : 
      27           1 :   std::vector<std::string> v;
      28           1 :   v.push_back("a1");
      29           1 :   v.push_back("c012");
      30           1 :   generator.add_identifiers(v.begin(), v.end());
      31             : 
      32           1 :   s = generator("c");
      33           1 :   BOOST_CHECK_EQUAL(s, "c13");
      34             : 
      35           1 :   s = generator("a");
      36           1 :   BOOST_CHECK_EQUAL(s, "a2");
      37             : 
      38           1 :   s = generator("a");
      39           1 :   BOOST_CHECK_EQUAL(s, "a3");
      40             : 
      41           1 :   s = generator("a2");
      42           1 :   BOOST_CHECK_EQUAL(s, "a4");
      43             : 
      44           1 :   s = generator();
      45           1 :   BOOST_CHECK_EQUAL(s, "FRESH_VAR");
      46             : 
      47           1 :   s = generator();
      48           1 :   BOOST_CHECK_EQUAL(s, "FRESH_VAR1");
      49             : 
      50           1 :   s = generator("b", false);
      51           1 :   BOOST_CHECK_EQUAL(s, "b");
      52             : 
      53           1 :   s = generator("b", false);
      54           1 :   BOOST_CHECK_EQUAL(s, "b");
      55             : 
      56           1 :   s = generator("b");
      57           1 :   BOOST_CHECK_EQUAL(s, "b");
      58             : 
      59           1 :   s = generator("b", false);
      60           1 :   BOOST_CHECK_EQUAL(s, "b1");
      61             : 
      62           1 :   generator.add_identifier("a0");
      63           1 :   s = generator("a2");
      64           1 :   BOOST_CHECK_EQUAL(s, "a5");
      65           1 : }