LCOV - code coverage report
Current view: top level - lts/include/mcrl2/lts - lts_lts.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 46 69 66.7 %
Date: 2019-09-14 00:54:39 Functions: 24 26 92.3 %
Legend: Lines: hit not hit

          Line data    Source code
       1             : // Author(s): 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             : 
      10             : /** \file lts_lts.h
      11             :  *
      12             :  * \brief This file contains a class that contains labelled transition systems in lts (mcrl2) format.
      13             :  * \details A labelled transition system in lts/mcrl2 format is a transition system
      14             :  * with as state labels vectors of strings, and as transition labels strings.
      15             :  * \author Jan Friso Groote
      16             :  */
      17             : 
      18             : 
      19             : #ifndef MCRL2_LTS_LTS_MCRL2_H
      20             : #define MCRL2_LTS_LTS_MCRL2_H
      21             : 
      22             : #include <string>
      23             : #include <vector>
      24             : #include "mcrl2/utilities/logger.h"
      25             : #include "mcrl2/core/detail/function_symbols.h"
      26             : #include "mcrl2/core/parse.h"
      27             : #include "mcrl2/data/variable.h"
      28             : #include "mcrl2/process/parse.h"
      29             : #include "mcrl2/lps/parse.h"
      30             : #include "mcrl2/lps/print.h"
      31             : #include "mcrl2/lps/specification.h"
      32             : #include "mcrl2/lps/multi_action.h"
      33             : #include "mcrl2/lps/typecheck.h"
      34             : #include "mcrl2/lps/state.h"
      35             : #include "mcrl2/lps/probabilistic_data_expression.h"
      36             : #include "mcrl2/lts/probabilistic_state.h"
      37             : #include "mcrl2/lts/probabilistic_lts.h"
      38             : 
      39             : namespace mcrl2
      40             : {
      41             : namespace lts
      42             : {
      43             : 
      44             : /** \brief This class contains state labels for an labelled transition system in .lts format.
      45             :     \details A state label in .lts format consists of lists of balanced tree of data expressions.
      46             :              These represent sets of state vectors. The reason for the sets is that states can
      47             :              be merged by operations on state spaces, and if so, the sets of labels can easily
      48             :              be joined.
      49             : */
      50       13092 : class state_label_lts : public atermpp::term_list< lps::state >
      51             : {
      52             :   public:
      53             :     typedef atermpp::term_list< lps::state > super;
      54             : 
      55             :     /** \brief Default constructor.
      56             :     */
      57        3216 :     state_label_lts()
      58        3216 :     {}
      59             : 
      60             :     /** \brief Copy constructor. */
      61        7464 :     state_label_lts(const state_label_lts& )=default;
      62             : 
      63             :     /** \brief Copy assignment. */
      64             :     state_label_lts& operator=(const state_label_lts& )=default;
      65             : 
      66             :     /** \brief Construct a single state label out of the elements in a container.
      67             :     */
      68             :     template < class CONTAINER >
      69             :     explicit state_label_lts(const CONTAINER& l)
      70             :     {
      71             :       static_assert(std::is_same<typename CONTAINER::value_type, data::data_expression>::value,"Value type must be a data_expression");
      72             :       this->push_front(lps::state(l.begin(),l.size()));
      73             :     }
      74             : 
      75             :     /** \brief Construct a state label out of a balanced tree of data expressions, representing a state label.
      76             :     */
      77        1608 :     explicit state_label_lts(const lps::state& l)
      78        1608 :     {
      79        1608 :       this->push_front(lps::state(l.begin(),l.size()));
      80        1608 :     }
      81             : 
      82             :     /** \brief Construct a state label out of list of balanced trees of data expressions, representing a state label.
      83             :     */
      84             :     explicit state_label_lts(const super& l)
      85             :       : super(l)
      86             :     {
      87             :     }
      88             : 
      89             :     /** \brief An operator to concatenate two state labels.
      90             :         \details Is optimal whenever |l| is smaller than the left operand, i.e. |l| < |this|.
      91             :      */
      92           0 :     state_label_lts operator+(const state_label_lts& l) const
      93             :     {
      94             :       // The order of the state labels should not matter. For efficiency the elements of l are inserted in front of the aterm_list.
      95           0 :       state_label_lts result(*this);
      96             : 
      97           0 :       for (const lps::state& el : l)
      98             :       {
      99           0 :         result.push_front(el);
     100             :       }
     101             : 
     102           0 :       return result;
     103             :     }
     104             : };
     105             : 
     106             : /** \brief Pretty print a state value of this LTS.
     107             :     \details The label is printed as (t1,...,tn) if it consists of a single label.
     108             :              Otherwise the labels are printed with square brackets surrounding it.
     109             :     \param[in] label  The state value to pretty print.
     110             :     \return           The pretty-printed representation of value. */
     111             : 
     112           0 : inline std::string pp(const state_label_lts& label)
     113             : {
     114           0 :   std::string s;
     115           0 :   if (label.size()!=1)
     116             :   {
     117           0 :     s += "[";
     118             :   }
     119           0 :   bool first=true;
     120           0 :   for(const lps::state& l: label)
     121             :   {
     122           0 :     if (!first)
     123             :     {
     124           0 :       s += ", ";
     125             :     }
     126           0 :     first = false;
     127           0 :     s += "(";
     128           0 :     for (lps::state::iterator i=l.begin(); i!=l.end(); ++i)
     129             :     {
     130           0 :       if (i!=l.begin())
     131             :       {
     132           0 :         s += ",";
     133             :       }
     134           0 :       s += data::pp(*i);
     135             :     }
     136           0 :     s += ")";
     137             :   }
     138           0 :   if (label.size()!=1)
     139             :   {
     140           0 :     s += "]";
     141             :   }
     142           0 :   return s;
     143             : }
     144             : 
     145             : /** \brief A class containing the values for action labels for the .lts format.
     146             :     \details An action label is a multi_action. */
     147       13317 : class action_label_lts: public mcrl2::lps::multi_action
     148             : {
     149             :   public:
     150             : 
     151             :     /** \brief Default constructor. */
     152           2 :     action_label_lts()
     153           2 :     {}
     154             : 
     155             :     /** \brief Copy constructor. */
     156       10681 :     action_label_lts(const action_label_lts& )=default;
     157             : 
     158             :     /** \brief Copy assignment. */
     159             :     action_label_lts& operator=(const action_label_lts& )=default;
     160             : 
     161             :     /** \brief Constructor. */
     162        2634 :     explicit action_label_lts(const mcrl2::lps::multi_action& a)
     163        2634 :      : mcrl2::lps::multi_action(a)
     164             :     {
     165        2634 :     }
     166             : 
     167             :     /** \brief Hide the actions with labels in tau_actions.
     168             :         \return Returns whether the hidden action becomes empty, i.e. a tau or hidden action.
     169             :     */
     170             :     void hide_actions(const std::vector<std::string>& tau_actions)
     171             :     {
     172             :       const process::action_list mas = this->actions();
     173             :       process::action_list new_action_list;
     174             :       for (process::action_list:: const_iterator i=mas.begin(); i!=mas.end(); ++i)
     175             :       {
     176             :         const process::action a=*i;
     177             : 
     178             :         if (std::find(tau_actions.begin(),tau_actions.end(),
     179             :                       std::string(a.label().name()))==tau_actions.end())  // this action must not be hidden.
     180             :         {
     181             :           new_action_list.push_front(a);
     182             :         }
     183             :       }
     184             :       m_actions=new_action_list;
     185             :     }
     186             : 
     187             :     /* \brief The action label that represents the internal action.
     188             :     */
     189        5584 :     static const action_label_lts& tau_action()
     190             :     {
     191        5584 :       static action_label_lts tau_action=action_label_lts();
     192        5584 :       return tau_action;
     193             :     }
     194             : 
     195             : };
     196             : 
     197             : /** \brief Print the action label to string. */
     198         986 : inline std::string pp(const action_label_lts& l)
     199             : {
     200         986 :   return lps::pp(mcrl2::lps::multi_action(l));
     201             : }
     202             : 
     203             : /** \brief Parse a string into an action label.
     204             :     \details The string is typechecked against the data specification and
     205             :              list of declared actions. If parsing or type checking fails, an
     206             :              mcrl2::runtime_error is thrown.
     207             :     \param[in] multi_action_string The string to be parsed.
     208             :     \param[in] data_spec The data specification used for parsing.
     209             :     \param[in] act_decls Action declarations.
     210             :     \return The parsed and type checked multi action. */
     211             : inline action_label_lts parse_lts_action(
     212             :   const std::string& multi_action_string,
     213             :   const data::data_specification& data_spec,
     214             :   lps::multi_action_type_checker& typechecker)
     215             : {
     216             :   std::string l(multi_action_string);
     217             :   lps::multi_action al;
     218             :   // Find an @ symbol in the action, in which case it is timed.
     219             :   size_t position_of_at=l.find_first_of('@');
     220             :   std::string time_expression_string;
     221             :   if (position_of_at!=std::string::npos)
     222             :   {
     223             :     // The at symbol is found. It is a timed action.
     224             :     time_expression_string=l.substr(position_of_at+1,l.size());
     225             :     l=l.substr(0,position_of_at-1);
     226             :   }
     227             :   try
     228             :   {
     229             :     al=lps::parse_multi_action(l, typechecker, data_spec);
     230             :   }
     231             :   catch (mcrl2::runtime_error& e)
     232             :   {
     233             :     throw mcrl2::runtime_error("Parse error in action label " + multi_action_string + ".\n" + e.what());
     234             :   }
     235             : 
     236             :   if (time_expression_string.size()>0)
     237             :   {
     238             :     try
     239             :     {
     240             :       data::data_expression time=parse_data_expression(time_expression_string,data::variable_list(),data_spec);
     241             :       // Translate the sort of time to a real.
     242             :       if (time.sort()==data::sort_pos::pos())
     243             :       {
     244             :         time = data::sort_nat::cnat(time);
     245             :       }
     246             :       if (time.sort()==data::sort_nat::nat())
     247             :       {
     248             :         time = data::sort_int::cint(time);
     249             :       }
     250             :       if (time.sort()==data::sort_int::int_())
     251             :       {
     252             :         time = data::sort_real::creal(time, data::sort_pos::c1());
     253             :       }
     254             :       if (time.sort()!=data::sort_real::real_())
     255             :       {
     256             :         throw mcrl2::runtime_error("The time is not of sort Pos, Nat, Int or Real\n");
     257             :       }
     258             :       return action_label_lts(lps::multi_action(al.actions(),time));
     259             :     }
     260             :     catch (mcrl2::runtime_error& e)
     261             :     {
     262             :       throw mcrl2::runtime_error("Parse error in the time expression " + multi_action_string + ".\n" + e.what());
     263             :     }
     264             :   }
     265             :   return action_label_lts(al);
     266             : }
     267             : 
     268             : namespace detail
     269             : {
     270             : 
     271             : /** \brief a base class for lts_lts_t and probabilistic_lts_t.
     272             :  */
     273         445 : class lts_lts_base
     274             : {
     275             :   protected:
     276             :     data::data_specification m_data_spec;
     277             :     data::variable_list m_parameters;
     278             :     process::action_label_list m_action_decls;
     279             : 
     280             :   public:
     281             :     /// \brief Default constructor
     282         445 :     lts_lts_base()
     283         445 :     {}
     284             : 
     285             :     /// \brief Copy constructor
     286             :     lts_lts_base(const lts_lts_base& l)
     287             :     : m_data_spec(l.m_data_spec),
     288             :       m_parameters(l.m_parameters),
     289             :       m_action_decls(l.m_action_decls)
     290             :     {}
     291             : 
     292             :     void swap(lts_lts_base& l)
     293             :     {
     294             :       const data::data_specification auxd=m_data_spec;
     295             :       m_data_spec=l.m_data_spec;
     296             :       l.m_data_spec=auxd;
     297             :       m_parameters.swap(l.m_parameters);
     298             :       m_action_decls.swap(l.m_action_decls);
     299             :     }
     300             : 
     301             :     /** \brief Yields the type of this lts, in this case lts_lts. */
     302         108 :     lts_type type() const
     303             :     {
     304         108 :       return lts_lts;
     305             :     }
     306             : 
     307             :     /** \brief Returns the mCRL2 data specification of this LTS.
     308             :     */
     309         108 :     const data::data_specification& data() const
     310             :     {
     311         108 :       return m_data_spec;
     312             :     }
     313             : 
     314             :     /** \brief Return action label declarations stored in this LTS.
     315             :     */
     316         108 :     const process::action_label_list& action_label_declarations() const
     317             :     {
     318         108 :       return m_action_decls;
     319             :     }
     320             : 
     321             :     /** \brief Set the action label information for this LTS.
     322             :      * \param[in] decls  The action labels to be set in this lts.
     323             :     */
     324         324 :     void set_action_label_declarations(const process::action_label_list& decls)
     325             :     {
     326         324 :       m_action_decls=decls;
     327         324 :     }
     328             : 
     329             :     /** \brief Set the mCRL2 data specification of this LTS.
     330             :      * \param[in] spec  The mCRL2 data specification for this LTS.
     331             :     */
     332         324 :     void set_data(const data::data_specification& spec)
     333             :     {
     334         324 :       m_data_spec=spec;
     335         324 :     }
     336             : 
     337             :     /** \brief Return the process parameters stored in this LTS.
     338             :     */
     339         596 :     const data::variable_list& process_parameters() const
     340             :     {
     341         596 :       return m_parameters;
     342             :     }
     343             : 
     344             :     /** \brief Returns the i-th parameter of the state vectors stored in this LTS.
     345             :      * \return The state parameters stored in this LTS.
     346             :     */
     347             :     const data::variable& process_parameter(std::size_t i) const
     348             :     {
     349             :       assert(i<m_parameters.size());
     350             :       data::variable_list::const_iterator j=m_parameters.begin();
     351             :       for(std::size_t c=0; c!=i; ++j, ++c)
     352             :       {}
     353             :       return *j;
     354             :     }
     355             : 
     356             : 
     357             :     /** \brief Set the state parameters for this LTS.
     358             :      * \param[in] params  The state parameters for this lts.
     359             :     */
     360         324 :     void set_process_parameters(const data::variable_list& params)
     361             :     {
     362         324 :       m_parameters=params;
     363         324 :     }
     364             : 
     365             : };
     366             : 
     367             : } // namespace detail
     368             : 
     369             : 
     370             : /** \brief This class contains labelled transition systems in .lts format.
     371             :     \details In this .lts format, an action label is a multi action, and a
     372             :            state label is an expression of the form STATE(t1,...,tn) where
     373             :            ti are data expressions.
     374             : */
     375          52 : class lts_lts_t : public lts< state_label_lts, action_label_lts, detail::lts_lts_base >
     376             : {
     377             :   public:
     378             :     typedef lts< state_label_lts, action_label_lts, detail::lts_lts_base > super;
     379             : 
     380             :     /** \brief Creates an object containing no information. */
     381          52 :     lts_lts_t()
     382          52 :     {}
     383             : 
     384             :     /** \brief Creates an object containing a muCRL specification.
     385             :      * \param[in] t The muCRL specification that will be stored in the object. */
     386             :     lts_lts_t(const atermpp::aterm& t);
     387             : 
     388             :     /** \brief Creates an object containing an mCRL2 specification.
     389             :      * \param[in] spec The mCRL2 specification that will be stored in the object. */
     390             :     lts_lts_t(lps::specification const& spec);
     391             : 
     392             :     /** \brief Copy constructor */
     393             :     lts_lts_t(const lts_lts_t& l):
     394             :       super(l)
     395             :     {}
     396             : 
     397             :     /** \brief Load the labelled transition system from file.
     398             :      *  \details If the filename is empty, the result is read from stdout.
     399             :      *  \param[in] filename Name of the file to which this lts is written.
     400             :      */
     401             :     void load(const std::string& filename);
     402             : 
     403             :     /** \brief Save the labelled transition system to file.
     404             :      *  \details If the filename is empty, the result is read from stdin.
     405             :      *  \param[in] filename Name of the file from which this lts is read.
     406             :      */
     407             :     void save(const std::string& filename) const;
     408             : };
     409             : 
     410             : /** \brief This class contains probabilistic labelled transition systems in .lts format.
     411             :     \details In this .lts format, an action label is a multi action, and a
     412             :            state label is an expression of the form STATE(t1,...,tn) where
     413             :            ti are data expressions.
     414             : */
     415         393 : class probabilistic_lts_lts_t :
     416             :          public probabilistic_lts< state_label_lts,
     417             :                                    action_label_lts,
     418             :                                    probabilistic_state<std::size_t, lps::probabilistic_data_expression>,
     419             :                                    detail::lts_lts_base >
     420             : {
     421             :   public:
     422             :     typedef probabilistic_lts< state_label_lts,
     423             :                                action_label_lts,
     424             :                                probabilistic_state_t,
     425             :                                detail::lts_lts_base > super;
     426             : 
     427             :     /** \brief Creates an object containing no information. */
     428         393 :     probabilistic_lts_lts_t()
     429         393 :     {}
     430             : 
     431             :     /** \brief Creates an object containing a muCRL specification.
     432             :      * \param[in] t The muCRL specification that will be stored in the object. */
     433             :     probabilistic_lts_lts_t(const atermpp::aterm& t);
     434             : 
     435             :     /** \brief Creates an object containing an mCRL2 specification.
     436             :      * \param[in] spec The mCRL2 specification that will be stored in the object. */
     437             :     probabilistic_lts_lts_t(lps::specification const& spec);
     438             : 
     439             :     /** \brief Copy constructor */
     440             :     probabilistic_lts_lts_t(const probabilistic_lts_lts_t& l):
     441             :       super(l)
     442             :     {}
     443             : 
     444             :     /** \brief Load the labelled transition system from file.
     445             :      *  \details If the filename is empty, the result is read from stdout.
     446             :      *  \param[in] filename Name of the file to which this lts is written.
     447             :      */
     448             :     void load(const std::string& filename);
     449             : 
     450             :     /** \brief Save the labelled transition system to file.
     451             :      *  \details If the filename is empty, the result is read from stdin.
     452             :      *  \param[in] filename Name of the file from which this lts is read.
     453             :      */
     454             :     void save(const std::string& filename) const;
     455             : };
     456             : } // namespace lts
     457             : } // namespace mcrl2
     458             : 
     459             : #endif

Generated by: LCOV version 1.12