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

Generated by: LCOV version 1.12