LCOV - code coverage report
Current view: top level - trace/include/mcrl2/trace - trace.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 139 221 62.9 %
Date: 2020-02-28 00:44:21 Functions: 23 31 74.2 %
Legend: Lines: hit not hit

          Line data    Source code
       1             : // Author(s): Muck van Weerdenburg. Documentation 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 mcrl2/trace/trace.h
      10             : /// \brief This library allows to flexibly manipulate traces.
      11             : /// \details This library allows to build, traverse and store traces.
      12             : /// Traces are sequences of state-action-time triples.
      13             : /// The state is a vector of data values, the action is the outgoing
      14             : /// action in this state, and the time is an absolute
      15             : /// real number indicating the current time or NIL if the trace
      16             : /// is untimed.
      17             : /// \author Muck van Weerdenburg
      18             : 
      19             : #ifndef _TRACE_H__
      20             : #define _TRACE_H__
      21             : 
      22             : // #include <iostream>
      23             : #include <fstream>
      24             : #include "mcrl2/lps/parse.h"
      25             : #include "mcrl2/lps/state.h"
      26             : 
      27             : namespace mcrl2
      28             : {
      29             : /** \brief The namespace for traces.
      30             : * \details The namespace trace contains all data structures and members of the
      31             : * trace library.
      32             : */
      33             : namespace trace
      34             : {
      35             : 
      36             : 
      37             : ////////////////////////////////////////////////////////////
      38             : //
      39             : /// \brief Formats in which traces can be saved on disk
      40             : /// \details There are several formats for traces.
      41             : /// The tfMcrl2 format saves a trace as an mCRL2 term in aterm internal format.
      42             : /// This is a compact but unreadable format.
      43             : /// The tfPlain format is an ascii representation of the trace, which is
      44             : /// human readable but only contains the actions and no time or state information.
      45             : /// tfUnknown is only used to read traces, when it is
      46             : /// not known what the format is. In this case it is determined based
      47             : /// on the format of the input file.
      48             : 
      49             : enum TraceFormat
      50             : {
      51             :   tfMcrl2,  /**< Format is stored as an aterm */
      52             :   tfPlain,  /**< Format is stored in plain text. In this format there are only actions */
      53             :   tfUnknown /**< This value indicates that the format is unknown */
      54             : };
      55             : 
      56             : /// \brief This class contains a trace consisting of a sequence of (timed) actions possibly with intermediate states
      57             : /// \details A trace is a sequence of actions. Actions can have a time
      58             : /// tag as a positive real number. Between two actions, before the first action and after the last
      59             : /// action there can be a state. In the current version of the trace library an action, a state and
      60             : /// a time tag are arbitrary expressions of sort AtermAppl. It is expected that this will change
      61             : /// in the near future to match the data types used in the LPS library.
      62             : ///
      63             : /// An important property of a state is its current position. All operations on a state
      64             : /// operate with respect to its current position. A trace can be traversed by increasing
      65             : /// and decreasing the current position between 0 up to the length. If a new action is
      66             : /// added to a trace, the trace above the current position is lost. For each action
      67             : /// a state can only be added once.
      68             : ///
      69             : /// States can be saved in two formats. A human readable ascii format containging only a
      70             : /// sequence of untimed actions and a more compact aterm format also containing time and
      71             : /// state information.
      72           7 : class Trace
      73             : {
      74             :   private:
      75             :     // The number of states is always less then one plus the number of actions.
      76             :     // In case all states are there, then it is one more than the number of actions.
      77             :     // Otherwise there are less.  So, an invariant is actions.size()+1 >= states.size();
      78             :     // The states and actions are supposed to be contiguous,
      79             :     // in the sense that if a state, or action, at position n exists, then also the
      80             :     // states and actions at positions n'<n exist.
      81             : 
      82             :     std::vector < mcrl2::lps::state > m_states;
      83             :     std::vector < mcrl2::lps::multi_action > m_actions;
      84             :     std::size_t pos; // Invariant: pos <= actions.size().
      85             : 
      86             :     mcrl2::data::data_specification m_spec;
      87             :     process::action_label_list m_act_decls;
      88             :     bool m_data_specification_and_act_decls_are_defined;
      89             : 
      90           6 :     const atermpp::function_symbol& trace_pair() const
      91             :     {
      92           6 :       static atermpp::function_symbol trace_pair = atermpp::function_symbol("pair",2);
      93           6 :       return trace_pair;
      94             :     }
      95             : 
      96             : #define TRACE_MCRL2_MARKER "mCRL2Trace"
      97             : #define TRACE_MCRL2_MARKER_SIZE 10
      98             : #define TRACE_MCRL2_VERSION "\x01\x00"
      99             : #define TRACE_MCRL2_VERSION_SIZE 2
     100             : 
     101             : #define INIT_BUF_SIZE 64
     102             : 
     103             :   public:
     104             :     /// \brief Default constructor for an empty trace.
     105             :     /// \details The current position
     106             :     /// and length of trace are set to 0.
     107           2 :     Trace()
     108           2 :       : m_data_specification_and_act_decls_are_defined(false)
     109             :     {
     110           2 :       init();
     111           2 :     }
     112             : 
     113             :     /// \brief Constructor for an empty trace.
     114             :     /// \details The current position
     115             :     /// and length of trace are set to 0.
     116             :     /// \param[in] spec The data specification that is used when parsing multi actions.
     117             :     /// \param[in] act_decls An action label list with action declarations that is used to parse multi actions.
     118           1 :     Trace(const mcrl2::data::data_specification& spec, const mcrl2::process::action_label_list& act_decls)
     119           1 :       : m_spec(spec),
     120             :         m_act_decls(act_decls),
     121           1 :         m_data_specification_and_act_decls_are_defined(true)
     122             :     {
     123           1 :       init();
     124           1 :     }
     125             : 
     126             : 
     127             :     /// \brief Construct the trace in the basis of an input stream.
     128             :     /// \details A trace is read from the input stream. If the format is tfUnknown it
     129             :     /// is automatically determined what the format of the trace is.
     130             :     /// \param[in] is The input stream from which the trace is read.
     131             :     /// \param[in] tf The format in which the trace was stored. Default: '''tfUnknown'''.
     132             :     /// \exception mcrl2::runtime_error message in case of failure
     133             :     Trace(std::istream& is, TraceFormat tf = tfUnknown)
     134             :       : m_data_specification_and_act_decls_are_defined(false)
     135             :     {
     136             :       init();
     137             :       try
     138             :       {
     139             :         load(is,tf);
     140             :       }
     141             :       catch (...)
     142             :       {
     143             :         throw;
     144             :       }
     145             :     }
     146             : 
     147             :     /// \brief Construct the trace in the basis of an input stream.
     148             :     /// \details A trace is read from the input stream. If the format is tfUnknown it
     149             :     /// is automatically determined what the format of the trace is.
     150             :     /// \param[in] is The input stream from which the trace is read.
     151             :     /// \param[in] tf The format in which the trace was stored. Default: '''tfUnknown'''.
     152             :     /// \param[in] spec The data specification that is used when parsing multi actions.
     153             :     /// \param[in] act_decls An action label list with action declarations that is used to parse multi actions.
     154             :     /// \exception mcrl2::runtime_error message in case of failure
     155             :     Trace(std::istream& is,
     156             :           const mcrl2::data::data_specification& spec,
     157             :           const mcrl2::process::action_label_list& act_decls,
     158             :           TraceFormat tf = tfUnknown)
     159             :       : m_spec(spec),
     160             :         m_act_decls(act_decls),
     161             :         m_data_specification_and_act_decls_are_defined(true)
     162             :     {
     163             :       init();
     164             :       try
     165             :       {
     166             :         load(is,tf);
     167             :       }
     168             :       catch (...)
     169             :       {
     170             :         throw;
     171             :       }
     172             :     }
     173             : 
     174             :     /// \brief Construct the trace on the basis of an input file.
     175             :     /// \details A trace is read from the input file. If the format is tfUnknown it
     176             :     /// is automatically determined what the format of the trace is.
     177             :     /// \param[in] filename The name of the file from which the trace is read.
     178             :     /// \param[in] tf The format in which the trace was stored. Default: '''tfUnknown'''.
     179             :     /// \exception mcrl2::runtime_error message in case of failure
     180             :     Trace(std::string const& filename, TraceFormat tf = tfUnknown)
     181             :       : m_data_specification_and_act_decls_are_defined(false)
     182             :     {
     183             :       init();
     184             :       try
     185             :       {
     186             :         load(filename,tf);
     187             :       }
     188             :       catch (...)
     189             :       {
     190             :         throw;
     191             :       }
     192             :     }
     193             : 
     194             :     /// \brief Construct the trace on the basis of an input file.
     195             :     /// \details A trace is read from the input file. If the format is tfUnknown it
     196             :     /// is automatically determined what the format of the trace is.
     197             :     /// \param[in] filename The name of the file from which the trace is read.
     198             :     /// \param[in] spec A data specification.
     199             :     /// \param[in] act_decls A list of action declarations.
     200             :     /// \param[in] tf The format in which the trace was stored. Default: '''tfUnknown'''.
     201             :     /// \exception mcrl2::runtime_error message in case of failure
     202           0 :     Trace(std::string const& filename,
     203             :           const mcrl2::data::data_specification& spec,
     204             :           const mcrl2::process::action_label_list& act_decls,
     205             :           TraceFormat tf = tfUnknown)
     206           0 :       : m_spec(spec),
     207             :         m_act_decls(act_decls),
     208           0 :         m_data_specification_and_act_decls_are_defined(true)
     209             :     {
     210           0 :       init();
     211             :       try
     212             :       {
     213           0 :         load(filename,tf);
     214             :       }
     215           0 :       catch (...)
     216             :       {
     217           0 :         throw;
     218             :       }
     219           0 :     }
     220             : 
     221           0 :     bool operator <(const Trace& t) const
     222             :     {
     223           0 :       return ((m_states<t.m_states) ||
     224           0 :               (m_states==t.m_states && m_actions<t.m_actions));
     225             :     }
     226             : 
     227             :     /// \brief Set the current position back to the beginning of the trace
     228             :     /// \details The trace itself remains unaltered.
     229           4 :     void resetPosition()
     230             :     {
     231           4 :       assert(m_actions.size()+1 >= m_states.size() && pos <=m_actions.size());
     232           4 :       pos = 0;
     233           4 :     }
     234             : 
     235             :     /// \brief Increase the current position by one, except if this brings one beyond the end of the trace.
     236             :     /// \details The initial position corresponds to pos=0.
     237           6 :     void increasePosition()
     238             :     {
     239           6 :       if (pos < m_actions.size())
     240             :       {
     241           6 :         ++pos;
     242             :       }
     243           6 :     }
     244             : 
     245             :     /// \brief Decrease the current position in the trace by one provided the largest position is larger than 0.
     246             :     /// \details The initial position corresponds to pos=0.
     247             :     void decreasePosition()
     248             :     {
     249             :       if (pos >0)
     250             :       {
     251             :         --pos;
     252             :       }
     253             :     }
     254             : 
     255             :     /// \brief Set the current position after the pos'th action of the trace.
     256             :     /// \details The initial position corresponds to pos=0. If pos is larger than
     257             :     /// the length of the trace, no new position is set.
     258             :     /// \param[in] pos The new position in the trace.
     259             :     void setPosition(std::size_t pos)
     260             :     {
     261             :       if (pos <= m_actions.size())
     262             :       {
     263             :         this->pos = pos;
     264             :       }
     265             :     }
     266             : 
     267             :     /// \brief Get the current position in the trace.
     268             :     /// \details The current position of the trace is a non negative number
     269             :     /// smaller than the length of the trace.
     270             :     /// \return The current position of the trace.
     271           0 :     std::size_t getPosition() const
     272             :     {
     273           0 :       assert(m_actions.size()+1 >= m_states.size() && pos <=m_actions.size());
     274           0 :       return pos;
     275             :     }
     276             : 
     277             :     /// \brief Get the number of actions in the current trace.
     278             :     /// \return A positive number indicating the number of actions in the trace.
     279           2 :     std::size_t number_of_actions() const
     280             :     {
     281           2 :       assert(m_actions.size()+1 >= m_states.size() && pos <=m_actions.size());
     282           2 :       return m_actions.size();
     283             :     }
     284             : 
     285             :     /// \brief Get the number of states in the current trace.
     286             :     /// \return A positive number indicating the number of states in the trace.
     287             :     std::size_t number_of_states() const
     288             :     {
     289             :       assert(m_actions.size()+1 >= m_states.size() && pos <=m_actions.size());
     290             :       return m_states.size();
     291             :     }
     292             : 
     293             :     /// \brief Remove the current state and all states following it.
     294             :     void clear_current_state()
     295             :     {
     296             :       assert(m_actions.size()+1 >= m_states.size() && pos <=m_actions.size());
     297             :       m_states.resize(pos);
     298             :     }
     299             : 
     300             :     /// \brief Indicate whether a current state exists.
     301             :     /// \return A boolean indicating whether the current state exists.
     302           0 :     bool current_state_exists() const
     303             :     {
     304           0 :       assert(m_actions.size()+1 >= m_states.size() && pos <=m_actions.size());
     305           0 :       return m_states.size()>pos;
     306             :     }
     307             : 
     308             :     /// \brief Get the state at the current position in the trace.
     309             :     /// \details The state at
     310             :     /// position 0 is the initial state. If no state is defined at
     311             :     /// the next position an exception is thrown.
     312             :     /// \return The state at the current position of the trace.
     313             :     const mcrl2::lps::state& nextState() const
     314             :     {
     315             :       assert(m_actions.size()+1 >= m_states.size() && pos+1 <=m_actions.size());
     316             :       if (pos>=m_states.size())
     317             :       {
     318             :         throw mcrl2::runtime_error("Requesting a state in a trace at a non existing position " + std::to_string(pos+1) + ".");
     319             :       }
     320             :       return m_states[pos+1];
     321             :     }
     322             : 
     323             :     /// \brief Get the state at the current position in the trace.
     324             :     /// \details The state at
     325             :     /// position 0 is the initial state. If no state is defined at
     326             :     /// the current position an exception is thrown.
     327             :     /// \return The state at the current position of the trace.
     328           0 :     const mcrl2::lps::state& currentState() const
     329             :     {
     330           0 :       assert(m_actions.size()+1 >= m_states.size() && pos <=m_actions.size());
     331           0 :       if (pos>=m_states.size())
     332             :       {
     333           0 :         throw mcrl2::runtime_error("Requesting a state in a trace at a non existing position " + std::to_string(pos) + ".");
     334             :       }
     335           0 :       return m_states[pos];
     336             :     }
     337             : 
     338             :     /// \brief Get the outgoing action from the current position in the trace.
     339             :     /// \details This routine returns the action at the current position of the
     340             :     /// trace. It is not allowed to request an action if no action is available.
     341             :     /// \return An action_list representing the action at the current position of the
     342             :     /// trace.
     343           6 :     mcrl2::lps::multi_action currentAction()
     344             :     {
     345           6 :       assert(m_actions.size()+1 >= m_states.size() && pos <=m_actions.size());
     346           6 :       assert(pos < m_actions.size());
     347           6 :       return m_actions[pos];
     348             :     }
     349             : 
     350             :     /// \brief Get the time of the current state in the trace.
     351             :     /// \details This is the time at which
     352             :     /// the last action occurred (if any).
     353             :     /// \return A data_expression representing the current time, or a default data_expression if the time is not defined.
     354             :     mcrl2::data::data_expression currentTime()
     355             :     {
     356             :       assert(m_actions.size()+1 >= m_states.size() && pos <=m_actions.size());
     357             :       return m_actions[pos].time();
     358             :     }
     359             : 
     360             :     /// \brief Truncates the trace at the current position.
     361             :     /// \details This function removes the next action at the current position and all
     362             :     /// subsequent actions and states. The state and the time at the current
     363             :     /// position remain untouched.
     364          15 :     void truncate()
     365             :     {
     366          15 :       m_actions.resize(pos);
     367          15 :       if (pos+1<m_states.size())  // Only throw states away that exist.
     368             :       {
     369           0 :         m_states.resize(pos+1);
     370             :       }
     371          15 :     }
     372             : 
     373             :     /// \brief Add an action to the current trace.
     374             :     /// \details Add an action to the current trace at the current position. The current
     375             :     /// position is increased and the length of the trace is set to this new current position.
     376             :     /// The old actions in the trace at the current at higher positions are removed.
     377             :     /// \param [in] action The multi_action to be stored in the trace.
     378             : 
     379          10 :     void addAction(const mcrl2::lps::multi_action& action)
     380             :     {
     381          10 :       assert(m_actions.size()+1 >= m_states.size() && pos <=m_actions.size());
     382          10 :       truncate(); // Take care that actions and states have the appropriate size.
     383          10 :       pos++;
     384          10 :       m_actions.push_back(action);
     385          10 :     }
     386             : 
     387             :     /// \brief Set the state at the current position.
     388             :     /// \details It is necessary that all states at earlier positions are also set.
     389             :     /// If not an mcrl2::runtime_error exception is thrown.
     390             :     /// \param [in] s The new state.
     391           0 :     void setState(const mcrl2::lps::state& s)
     392             :     {
     393           0 :       assert(m_actions.size()+1 >= m_states.size() && pos <=m_actions.size());
     394           0 :       if (pos>m_states.size())
     395             :       {
     396           0 :         throw mcrl2::runtime_error("Setting a state in a trace at a position " + std::to_string(pos) +
     397           0 :                                    " where there are no states at earlier positions.");
     398             :       }
     399             : 
     400           0 :       if (m_states.size()==pos)
     401             :       {
     402           0 :         m_states.push_back(s);
     403             :       }
     404             :       else
     405             :       {
     406           0 :         m_states[pos] = s;
     407             :       }
     408           0 :     }
     409             : 
     410             :     /// \brief Replace the trace with the content of the stream.
     411             :     /// \details The trace is replaced with the trace in the stream.
     412             :     /// If a problem occurs while reading the stream, a core dump occurs.
     413             :     /// If the format is tfPlain the trace can only consist of actions.
     414             :     /// \param [in] is The stream from which the trace is read.
     415             :     /// \param [in] tf The expected format of the trace in the stream (default: tfUnknown).
     416             :     /// \exception mcrl2::runtime_error message in case of failure
     417             : 
     418           2 :     void load(std::istream& is, TraceFormat tf = tfUnknown)
     419             :     {
     420             :       try
     421             :       {
     422             : 
     423           2 :         if (tf == tfUnknown)
     424             :         {
     425           1 :           tf = detectFormat(is);
     426             :         }
     427             : 
     428           2 :         switch (tf)
     429             :         {
     430           1 :           case tfMcrl2:
     431           1 :             loadMcrl2(is);
     432           1 :             break;
     433           1 :           case tfPlain:
     434           1 :             loadPlain(is);
     435           1 :             break;
     436           0 :           default:
     437           0 :             break;
     438             :         }
     439             : 
     440             :       }
     441           0 :       catch (mcrl2::runtime_error& err)
     442             :       {
     443           0 :         std::string s;
     444           0 :         s = "error loading trace: ";
     445           0 :         s += err.what();
     446           0 :         s += ".";
     447           0 :         throw mcrl2::runtime_error(s);
     448             :       }
     449           2 :     }
     450             : 
     451             :     /// \brief Replace the trace with the trace in the file.
     452             :     /// \details The trace is replaced with the trace in the file.
     453             :     /// If the format is tfPlain the trace can only consist of actions.
     454             :     /// \param [in] filename The name of the file from which the trace is read.
     455             :     /// \param [in] tf The expected format of the trace in the stream (default: tfUnknown).
     456             :     /// \exception mcrl2::runtime_error message in case of failure
     457             : 
     458           0 :     void load(const std::string& filename, TraceFormat tf = tfUnknown)
     459             :     {
     460             :       using std::ifstream;
     461           0 :       ifstream is(filename.c_str(),ifstream::binary|ifstream::in);
     462             : 
     463           0 :       if (!is.is_open())
     464             :       {
     465           0 :         throw runtime_error("Error loading trace (could not open file " + filename +").");
     466             :       }
     467             : 
     468             :       try
     469             :       {
     470           0 :         load(is, tf);
     471             :       }
     472           0 :       catch (...)
     473             :       {
     474           0 :         is.close();
     475           0 :         throw;
     476             :       }
     477             : 
     478           0 :       is.close();
     479           0 :     }
     480             : 
     481             :     /// \brief Output the trace into the indicated stream.
     482             :     /// \details Output the trace into the indicated stream.
     483             :     /// If a problem occurs, this routine dumps core.
     484             :     /// \param [in] os The stream to which the trace is written.
     485             :     /// \param [in] tf The format used to represent the trace in the stream. If
     486             :     /// the format is tfPlain only actions are written. Default: tfMcrl2.
     487             :     /// \exception mcrl2::runtime_error message in case of failure
     488             : 
     489           2 :     void save(std::ostream& os, TraceFormat tf = tfMcrl2)
     490             :     {
     491             :       try
     492             :       {
     493           2 :         switch (tf)
     494             :         {
     495           1 :           case tfMcrl2:
     496           1 :             saveMcrl2(os);
     497           1 :             break;
     498           1 :           case tfPlain:
     499           1 :             savePlain(os);
     500           1 :             break;
     501           0 :           default:
     502           0 :             break;
     503             :         }
     504             :       }
     505           0 :       catch (runtime_error& err)
     506             :       {
     507           0 :         throw runtime_error(std::string("Error saving trace (") + err.what() + ").");
     508             :       }
     509           2 :     }
     510             : 
     511             :     /// \brief Output the trace into a file with the indicated name.
     512             :     /// \details Write the trace to a file with the indicated name.
     513             :     /// \param [in] filename The name of the file that is written.
     514             :     /// \param [in] tf The format used to represent the trace in the stream. If
     515             :     /// the format is tfPlain only actions are written. Default: tfMcrl2.
     516             :     /// \exception mcrl2::runtime_error message in case of failure
     517             : 
     518           1 :     void save(std::string const& filename, TraceFormat tf = tfMcrl2)
     519             :     {
     520             :       using std::ofstream;
     521           2 :       ofstream os(filename.c_str(),ofstream::binary|ofstream::out|ofstream::trunc);
     522           1 :       if (!os.is_open())
     523             :       {
     524           0 :         throw runtime_error("error saving trace (could not open file)");
     525             :       }
     526             : 
     527             :       try
     528             :       {
     529           1 :         save(os, tf);
     530             :       }
     531           0 :       catch (...)
     532             :       {
     533           0 :         os.close();
     534           0 :         throw;
     535             :       }
     536             : 
     537           1 :       os.close();
     538           1 :     }
     539             : 
     540           0 :     const std::vector<lps::state>& states() const
     541             :     {
     542           0 :       return m_states;
     543             :     }
     544             : 
     545             :     const std::vector<lps::multi_action>& actions() const
     546             :     {
     547             :       return m_actions;
     548             :     }
     549             : 
     550             :   private:
     551             : 
     552           3 :     bool isTimedMAct(const atermpp::aterm_appl& t)
     553             :     {
     554           3 :       return t.type_is_appl() && t.function()==trace_pair();
     555             :     }
     556             : 
     557           3 :     atermpp::aterm_appl makeTimedMAct(const mcrl2::lps::multi_action& ma)
     558             :     {
     559           3 :       return atermpp::aterm_appl(trace_pair(),ma.actions(), ma.time());
     560             :     }
     561             : 
     562           3 :     void init()
     563             :     {
     564           3 :       pos = 0;
     565           3 :       truncate(); // Take care that pos 0 exists.
     566           3 :     }
     567             : 
     568           1 :     TraceFormat detectFormat(std::istream& is)
     569             :     {
     570             :       char buf[TRACE_MCRL2_MARKER_SIZE];
     571           1 :       TraceFormat fmt = tfPlain;
     572             : 
     573           1 :       is.read(buf,TRACE_MCRL2_MARKER_SIZE);
     574           1 :       if (is.bad())
     575             :       {
     576           0 :         throw runtime_error("Could not read from stream.");
     577             :       }
     578           1 :       is.clear();
     579             : 
     580           1 :       if ((is.gcount() == TRACE_MCRL2_MARKER_SIZE) && !strncmp(buf,TRACE_MCRL2_MARKER,TRACE_MCRL2_MARKER_SIZE))
     581             :       {
     582           0 :         fmt = tfMcrl2;
     583             :       }
     584             : 
     585           1 :       is.seekg(-is.gcount(),std::ios::cur);
     586           1 :       if (is.fail())
     587             :       {
     588           0 :         throw runtime_error("Could not set position in stream.");
     589             :       }
     590             : 
     591           1 :       return fmt;
     592             :     }
     593             : 
     594           1 :     atermpp::aterm readATerm(std::istream& is)
     595             :     {
     596           1 :       atermpp::aterm t;
     597           1 :       atermpp::binary_aterm_istream(is) >> mcrl2::data::detail::add_index_impl >> t;
     598             : 
     599           1 :       if (!t.defined())
     600             :       {
     601           0 :         throw runtime_error("Failed to read aterm from stream.");
     602             :       }
     603             : 
     604           1 :       return t;
     605             :     }
     606             : 
     607           1 :     void loadMcrl2(std::istream& is)
     608             :     {
     609             :       using namespace atermpp;
     610             :       char buf[TRACE_MCRL2_MARKER_SIZE+TRACE_MCRL2_VERSION_SIZE];
     611           1 :       is.read(buf,TRACE_MCRL2_MARKER_SIZE+TRACE_MCRL2_VERSION_SIZE);
     612           1 :       if (is.bad() || strncmp(buf,TRACE_MCRL2_MARKER,TRACE_MCRL2_MARKER_SIZE))
     613             :       {
     614           0 :         throw runtime_error("stream does not contain an mCRL2 trace");
     615             :       }
     616           1 :       is.clear();
     617             : 
     618           1 :       resetPosition();
     619           1 :       truncate();
     620           2 :       aterm_list trace = atermpp::down_cast<aterm_list>(readATerm(is));
     621           1 :       assert(trace.type_is_list());
     622           7 :       for (; !trace.empty(); trace=trace.tail())
     623             :       {
     624             :         using namespace mcrl2::lps;
     625           3 :         const aterm& e = trace.front();
     626             : 
     627           3 :         if (e.type_is_appl() && lps::is_multi_action(down_cast<aterm_appl>(e)))   // To be compatible with old untimed version
     628             :         {
     629           0 :           addAction(multi_action(down_cast<process::action_list>(e)));
     630             :         }
     631           3 :         else if (e.type_is_appl() && isTimedMAct(down_cast<aterm_appl>(e)))
     632             :         {
     633           3 :           if (down_cast<aterm_appl>(e)[1]==data::undefined_real())  // There is no time tag.
     634             :           {
     635           3 :             addAction(multi_action(down_cast<process::action_list>(down_cast<aterm_appl>(e)[0])));
     636             :           }
     637             :           else
     638             :           {
     639           0 :             addAction(multi_action(down_cast<process::action_list>(down_cast<aterm_appl>(e)[0]),
     640           0 :                                    mcrl2::data::data_expression(down_cast<aterm_appl>(e)[1])));
     641             :           }
     642             :         }
     643             :         else
     644             :         {
     645             :           // So, e is a list of data expressions.
     646           0 :           data::data_expression_list l=atermpp::down_cast<data::data_expression_list>(e);
     647           0 :           mcrl2::lps::state s(l.begin(), l.size());
     648           0 :           setState(s);
     649             :         }
     650             :       }
     651             : 
     652           1 :       resetPosition();
     653           1 :     }
     654             : 
     655           1 :     void loadPlain(std::istream& is)
     656             :     {
     657             : #define MAX_LINE_SIZE 1024
     658             :       char buf[MAX_LINE_SIZE];
     659           1 :       resetPosition();
     660           1 :       truncate();
     661             : 
     662           9 :       while (!is.eof())
     663             :       {
     664           4 :         is.getline(buf,MAX_LINE_SIZE);
     665           4 :         if (is.bad())
     666             :         {
     667           0 :           throw mcrl2::runtime_error("Error while reading from stream.");
     668             :         }
     669           4 :         if ((strlen(buf) > 0) && (buf[strlen(buf)-1] == '\r'))
     670             :         {
     671             :           // remove CR
     672           0 :           buf[strlen(buf)-1] = '\0';
     673             :         }
     674             : 
     675           4 :         if (is.gcount() > 0)
     676             :         {
     677           3 :           if (m_data_specification_and_act_decls_are_defined)
     678             :           {
     679           0 :             addAction(mcrl2::lps::parse_multi_action(buf,m_act_decls,m_spec));
     680             :           }
     681             :           else
     682             :           {
     683           3 :             addAction(mcrl2::lps::multi_action(mcrl2::process::action(
     684           6 :                       mcrl2::process::action_label(mcrl2::core::identifier_string(buf),mcrl2::data::sort_expression_list()),
     685           6 :                                            mcrl2::data::data_expression_list())));
     686             :           }
     687             :         }
     688             :       }
     689           1 :       is.clear();
     690             : 
     691           1 :       resetPosition();
     692           1 :     }
     693             : 
     694           1 :     void saveMcrl2(std::ostream& os)
     695             :     {
     696           1 :       assert(m_actions.size()+1 >= m_states.size());
     697           2 :       atermpp::aterm_list trace;
     698             : 
     699           1 :       std::size_t i=m_actions.size()+1;
     700           9 :       while (i > 0)
     701             :       {
     702           4 :         i--;
     703           4 :         if (i<m_actions.size())
     704             :         {
     705           3 :           assert(m_actions.size()>i);
     706           3 :           trace.push_front(atermpp::aterm(makeTimedMAct(m_actions[i])));
     707             :         }
     708           4 :         if (m_states.size()>i)
     709             :         {
     710             :           using namespace mcrl2::lps;
     711             :           // Translate the vector into a list of aterms representing data expressions.
     712           0 :           atermpp::aterm_list l;
     713           0 :           const state& s=m_states[i];
     714           0 :           for(mcrl2::lps::state::iterator j=s.begin(); j!=s.end(); ++j)
     715             :           {
     716           0 :             l.push_front(atermpp::aterm(*j));
     717             :           }
     718           0 :           trace.push_front(atermpp::aterm(reverse(l)));
     719             :         }
     720             :       }
     721             : 
     722             :       // write marker
     723           1 :       os << TRACE_MCRL2_MARKER;
     724           1 :       os.write(TRACE_MCRL2_VERSION,TRACE_MCRL2_VERSION_SIZE);
     725           1 :       if (os.bad())
     726             :       {
     727           0 :         throw runtime_error("Could not write to stream.");
     728             :       }
     729             : 
     730             :       // write trace
     731           1 :       atermpp::binary_aterm_ostream(os) << data::detail::remove_index_impl << trace;
     732           1 :       if (os.bad())
     733             :       {
     734           0 :         throw runtime_error("Could not write to stream.");
     735             :       }
     736           1 :     }
     737             : 
     738           1 :     void savePlain(std::ostream& os)
     739             :     {
     740           2 :       for (std::size_t i=0; i<m_actions.size(); i++)
     741             :       {
     742           1 :         os << pp(m_actions[i]);
     743           1 :         os << std::endl;
     744           1 :         if (os.bad())
     745             :         {
     746           0 :           throw runtime_error("Could not write to stream.");
     747             :         }
     748             :       }
     749           1 :     }
     750             : };
     751             : 
     752             : }
     753             : }
     754             : #endif

Generated by: LCOV version 1.13