Line data    Source code

       1             : // Author(s): Muck van Weerdenburg, 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_mcrl2.cpp
      10             : /// \brief Test input and output of traces. 
      11             : 
      12             : #define BOOST_TEST_MODULE read_mcrl2
      13             : 
      14             : #include <boost/test/included/unit_test.hpp>
      15             : #include <exception>
      16             : 
      17             : #include "mcrl2/lts/trace.h"
      18             : 
      19             : using namespace mcrl2;
      20             : using namespace mcrl2::lts;
      21             : 
      22             : const std::string trace_data = "trace_mcrl2.trc";
      23             : 
      24             : 
      25           6 : void test_next_action(trace& t, const char* s)
      26             : {
      27           6 :   mcrl2::lps::multi_action a = t.current_action();
      28           6 :   t.increase_position();
      29           6 :   BOOST_CHECK((a != mcrl2::lps::multi_action()));
      30           6 :   if (a != mcrl2::lps::multi_action())
      31             :   {
      32           6 :     std::string action(pp(a));
      33           6 :     BOOST_CHECK(action == s);
      34           6 :     if (action != s)
      35             :     {
      36           0 :       std::cout << "--- error detected ---\n";
      37           0 :       std::cout << "result         : " << action << std::endl;
      38           0 :       std::cout << "expected result: " << s << std::endl;
      39             :     }
      40           6 :   }
      41           6 : }
      42             : 
      43           2 : BOOST_AUTO_TEST_CASE(test_main)
      44             : {
      45             :   using namespace mcrl2::data;
      46             :   using namespace mcrl2::lps;
      47             :   using namespace mcrl2::core;
      48           1 :   mcrl2::data::data_specification data_spec;
      49           1 :   process::action_label_list act_decls;
      50           1 :   act_decls.push_front(process::action_label(identifier_string("a"),sort_expression_list()));
      51           1 :   sort_expression_list s;
      52           1 :   s.push_front(sort_bool::bool_());
      53           1 :   s.push_front(sort_pos::pos());
      54           1 :   act_decls.push_front(process::action_label("b",s));
      55           1 :   act_decls.push_front(process::action_label(identifier_string("c"),sort_expression_list()));
      56             : 
      57           1 :   trace t(data_spec, act_decls);
      58           1 :   t.add_action(parse_multi_action("a",act_decls,data_spec));
      59           1 :   t.add_action(parse_multi_action("b(1,true)",act_decls,data_spec));
      60           1 :   t.add_action(parse_multi_action("c",act_decls,data_spec));
      61             : 
      62           1 :   t.save(trace_data);
      63             : 
      64             :   try
      65             :   {
      66           1 :     t.load(trace_data);
      67             :   }
      68           0 :   catch (const mcrl2::runtime_error& e)
      69             :   {
      70           0 :     BOOST_ERROR(e.what());
      71           0 :   }
      72             : 
      73           1 :   BOOST_CHECK(t.number_of_actions() == 3);
      74           1 : std::cerr << "STATE  " << t.number_of_states() << "\n";
      75           1 :   BOOST_CHECK(t.number_of_states() == 0);  // There are no explicit states in this trace.
      76             : 
      77           1 :   test_next_action(t,"a");
      78           1 :   test_next_action(t,"b(1, true)");
      79           1 :   test_next_action(t,"c");
      80             : 
      81             :   // Now add a few explicit states. 
      82           1 :   lps::state local_state1( sort_bool::true_() );
      83           1 :   lps::state local_state2( sort_bool::false_() );
      84             : 
      85           1 :   t.reset_position();
      86           1 :   t.set_state(local_state1);
      87           1 :   t.increase_position();
      88           1 :   t.set_state(local_state2);
      89           1 :   t.increase_position();
      90           1 :   t.set_state(local_state1);
      91           1 :   t.increase_position();
      92           1 :   t.set_state(local_state2);
      93             : 
      94           1 :   t.save(trace_data);
      95             : 
      96             :   try
      97             :   { 
      98           1 :     t.load(trace_data);
      99             :   }
     100           0 :   catch (const mcrl2::runtime_error& e)
     101             :   { 
     102           0 :     BOOST_ERROR(e.what());
     103           0 :   }
     104             : 
     105           1 :   BOOST_CHECK(t.number_of_actions() == 3);
     106           1 : std::cerr << "STATE  " << t.number_of_states() << "\n";
     107           1 :   BOOST_CHECK(t.number_of_states() == 4);  // There are no explicit states in this trace.
     108           1 : std::cerr << "ASTATE " << t.current_state() << "\n";
     109           1 :   BOOST_CHECK(t.current_state()==local_state1);
     110           1 : std::cerr << "NSTATE " << t.next_state() << "\n";
     111           1 :   BOOST_CHECK(t.next_state()==local_state2);
     112           1 :   test_next_action(t,"a");
     113           1 : std::cerr << "ASTATE " << t.current_state() << "\n";
     114           1 :   BOOST_CHECK(t.current_state()==local_state2);
     115           1 : std::cerr << "NSTATE " << t.next_state() << "\n";
     116           1 :   BOOST_CHECK(t.next_state()==local_state1);
     117           1 :   test_next_action(t,"b(1, true)");
     118           1 :   test_next_action(t,"c");
     119           1 : }
     120             : 
     121           2 : BOOST_AUTO_TEST_CASE(test_empty_trace)
     122             : {
     123             :   using namespace mcrl2::data;
     124             :   using namespace mcrl2::lps;
     125             :   using namespace mcrl2::core;
     126           1 :   mcrl2::data::data_specification data_spec;
     127           1 :   process::action_label_list act_decls;
     128             : 
     129           1 :   trace t(data_spec, act_decls);
     130             : 
     131           1 :   t.save(trace_data);
     132             : 
     133             :   try
     134             :   {
     135           1 :     t.load(trace_data);
     136             :   }
     137           0 :   catch (const mcrl2::runtime_error& e)
     138             :   {
     139           0 :     BOOST_ERROR(e.what());
     140           0 :   }
     141             : 
     142           1 :   BOOST_CHECK(t.number_of_actions() == 0);
     143           1 :   BOOST_CHECK(t.number_of_states() == 0);
     144             : 
     145             :   // Now add an initial state.
     146             :   
     147           1 :   lps::state local_state1( sort_bool::true_() );
     148             : 
     149           1 :   t.set_state(local_state1);
     150             : 
     151           1 :   t.save(trace_data);
     152             : 
     153             :   try
     154             :   {
     155           1 :     t.load(trace_data);
     156             :   }
     157           0 :   catch (const mcrl2::runtime_error& e)
     158             :   {
     159           0 :     BOOST_ERROR(e.what());
     160           0 :   }
     161             : 
     162           1 :   BOOST_CHECK(t.number_of_actions() == 0);
     163           1 :   BOOST_CHECK(t.number_of_states() == 1);
     164             : 
     165           1 :   BOOST_CHECK(t.current_state()==local_state1);
     166             : 
     167           1 : }