Line data    Source code

       1             : // Author(s): Muck van Weerdenbrug, Jan Friso Groote
       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 read_plain.cpp
      10             : 
      11             : #define BOOST_TEST_MODULE read_plain
      12             : #include <boost/test/included/unit_test.hpp>
      13             : 
      14             : #include "mcrl2/process/parse.h"
      15             : #include "mcrl2/lps/parse.h"
      16             : #include "mcrl2/lts/trace.h"
      17             : 
      18             : using namespace mcrl2;
      19             : using namespace mcrl2::lts;
      20             : using namespace mcrl2::data;
      21             : 
      22             : const std::string filename = "trace_plain.trc";
      23             : 
      24           4 : static bool read_trace(trace& t, const std::string& input_file)
      25             : {
      26             :   try
      27             :   {
      28           4 :     t.load(input_file);
      29             :   }
      30           0 :   catch (...)
      31             :   {
      32           0 :     throw;
      33             :     return false;
      34           0 :   }
      35             : 
      36           4 :   return true;
      37             : }
      38             : 
      39           6 : void test_next_action(trace& t, const char* s)
      40             : {
      41           6 :   mcrl2::lps::multi_action a = t.current_action();
      42           6 :   t.increase_position();
      43           6 :   BOOST_CHECK(a != mcrl2::lps::multi_action());
      44           6 :   if (a != mcrl2::lps::multi_action())
      45             :   {
      46           6 : std::cerr << "Current action " << a << " compare to " << s << "\n";
      47           6 :     BOOST_CHECK(a.actions().size() == 1);
      48           6 :     BOOST_CHECK(pp(a)==s);
      49             :   }
      50           6 : }
      51             : 
      52           2 : BOOST_AUTO_TEST_CASE(test_main)
      53             : {
      54           1 :   mcrl2::log::logger::set_reporting_level(mcrl2::log::debug);
      55           1 :   trace t;
      56             : 
      57           2 :   process::action_label_list action_decls = process::parse_action_declaration("a;") +
      58           2 :                                             process::parse_action_declaration("b:Nat#Bool;") +
      59           3 :                                             process::parse_action_declaration("c;");
      60             : 
      61           1 :   t.add_action(mcrl2::lps::parse_multi_action("a", action_decls));
      62           1 :   t.add_action(mcrl2::lps::parse_multi_action("b(1, true)", action_decls));
      63           1 :   t.add_action(mcrl2::lps::parse_multi_action("c", action_decls));
      64             : 
      65           1 :   t.save(filename,trace::tfPlain);
      66           1 :   BOOST_REQUIRE(read_trace(t,filename));
      67             : 
      68           1 :   BOOST_REQUIRE(t.number_of_actions() == 3);
      69           1 :   BOOST_REQUIRE(t.number_of_states() == 0);
      70             : 
      71           1 :   test_next_action(t,"a");
      72           1 :   test_next_action(t,"b(1, true)");
      73           1 :   test_next_action(t,"c");
      74             : 
      75             :   // now check this with explicit states. 
      76             : 
      77           1 :   t.reset_position();
      78           1 :   t.set_state(lps::state(sort_bool::true_()));
      79           1 :   t.increase_position();
      80           1 :   t.set_state(lps::state(sort_bool::false_()));
      81           1 :   t.increase_position();
      82           1 :   t.set_state(lps::state(sort_bool::true_()));
      83           1 :   t.increase_position();
      84           1 :   t.set_state(lps::state(sort_bool::false_()));
      85             : 
      86           1 :   t.save(filename,trace::tfPlain);
      87           1 :   BOOST_REQUIRE(read_trace(t,filename));
      88             : 
      89           1 :   BOOST_REQUIRE(t.number_of_actions() == 3);
      90           1 : std::cerr << "Number of states " << t.number_of_states() << "\n";
      91           1 :   BOOST_REQUIRE(t.number_of_states() == 0);  // In plain format states are not read back. 
      92             : 
      93           1 :   test_next_action(t,"a");
      94           1 :   test_next_action(t,"b(1, true)");
      95           1 :   test_next_action(t,"c");
      96           1 : }
      97             : 
      98             : 
      99           2 : BOOST_AUTO_TEST_CASE(test_empty)
     100             : {
     101           1 :   trace t;
     102             : 
     103           1 :   t.save(filename,trace::tfPlain);
     104           1 :   BOOST_REQUIRE(read_trace(t,filename));
     105             : 
     106           1 :   BOOST_REQUIRE(t.number_of_actions() == 0);
     107           1 :   BOOST_REQUIRE(t.number_of_states() == 0);
     108             : 
     109             :   // now check this with explicit states. 
     110             : 
     111           1 :   t.set_state(lps::state(sort_bool::true_()));
     112             : 
     113           1 :   t.save(filename);
     114           1 :   BOOST_REQUIRE(read_trace(t,filename));
     115             : 
     116           1 :   BOOST_REQUIRE(t.number_of_actions() == 0);
     117           1 :   BOOST_REQUIRE(t.number_of_states() == 1);
     118             : 
     119           1 :   BOOST_CHECK(t.current_state()==lps::state(sort_bool::true_()));
     120           1 : } 
     121             :