LCOV - code coverage report
Current view: top level - lts/include/mcrl2/lts/detail - fsm_builder.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 105 113 92.9 %
Date: 2020-07-11 00:44:39 Functions: 23 23 100.0 %
Legend: Lines: hit not hit

          Line data    Source code
       1             : // Author(s): Wieger Wesselink
       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/lts/detail/fsm_builder.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_LTS_DETAIL_FSM_BUILDER_H
      13             : #define MCRL2_LTS_DETAIL_FSM_BUILDER_H
      14             : 
      15             : #include "mcrl2/lts/lts_fsm.h"
      16             : #include "mcrl2/utilities/parse_numbers.h"
      17             : 
      18             : namespace mcrl2::lts::detail {
      19             : 
      20             : // Read a numeric value before a symbol c1 or c2, and remove it from s, including the symbol.
      21         672 : inline std::string split_string_until(std::string& s, const std::string& c1, const std::string& c2="")
      22             : {
      23         672 :   std::size_t n=s.find(c1);
      24         672 :   if (!c2.empty())
      25             :   {
      26         224 :     n=std::min(n,s.find(c2));
      27             :   }
      28         672 :   if (n==std::string::npos)
      29             :   {
      30           0 :     if (c2.empty())
      31             :     { 
      32           0 :       throw mcrl2::runtime_error("Expect '" + c1 + "' in distribution " + s + ".");
      33             :     }
      34             :     else
      35             :     {
      36           0 :       throw mcrl2::runtime_error("Expect either '" + c1 + "' or '" + c2 + " in distribution " + s + ".");
      37             :     }
      38             :   }
      39         672 :   std::string result=s.substr(0,n);
      40         672 :   s=s.substr(n+1);
      41         672 :   return result;
      42             : }
      43             : 
      44        1665 : inline lts_fsm_base::probabilistic_state parse_distribution(const std::string& distribution)
      45             : {
      46        1665 :   if (distribution.find('[')==std::string::npos) // So the distribution must consist of a state index.
      47             :   {
      48        1553 :     std::size_t state_number=utilities::parse_natural_number(distribution);
      49        1553 :     if (state_number==0)
      50             :     {
      51           0 :       throw mcrl2::runtime_error("Transition has a zero as target state number.");
      52             :     }
      53        1553 :     return lts_fsm_base::probabilistic_state(state_number-1);
      54             :   }
      55             :   
      56             :   // Otherwise the distribution has the shape [state1 enumerator1/denominator1 ... staten enumeratorn/denominatorn]
      57         224 :   std::vector<lts_fsm_base::state_probability_pair> result;
      58         224 :   std::string s = utilities::trim_copy(distribution);
      59         112 :   if (s.substr(0,1) != "[")
      60             :   {
      61           0 :     throw mcrl2::runtime_error("Distribution does not start with ']': " + distribution + ".");
      62             :   }
      63         112 :   s = s.substr(1);  // Remove initial "[";
      64         560 :   for(; s.size() > 1; s = utilities::trim_copy(s))
      65             :   {
      66         224 :     std::size_t state_number = utilities::parse_natural_number(split_string_until(s," "));
      67         224 :     if (state_number == 0)
      68             :     {
      69           0 :       throw mcrl2::runtime_error("Transition has a zero as target state number.");
      70             :     }
      71         448 :     std::string enumerator = split_string_until(s,"/");
      72         448 :     std::string denominator = split_string_until(s," ","]");
      73         224 :     result.emplace_back(state_number - 1, probabilistic_arbitrary_precision_fraction(enumerator,denominator));
      74             :   }
      75         112 :   return lts_fsm_base::probabilistic_state(result.begin(), result.end());
      76             : }
      77             : 
      78         528 : class fsm_parameter
      79             : {
      80             :   protected:
      81             :     std::string m_name;
      82             :     std::size_t m_cardinality;
      83             :     std::string m_sort;
      84             :     std::vector<std::string> m_values;
      85             : 
      86             :   public:
      87         180 :     fsm_parameter(const std::string& name, const std::string& cardinality, const std::string& sort, const std::vector<std::string>& values)
      88         180 :       : m_name(name),
      89         180 :         m_cardinality(utilities::parse_natural_number(cardinality)),
      90             :         m_sort(sort),
      91         360 :         m_values(values)
      92         180 :     {}
      93             : 
      94         180 :     const std::string& name() const
      95             :     {
      96         180 :       return m_name;
      97             :     }
      98             : 
      99             :     std::string& name()
     100             :     {
     101             :       return m_name;
     102             :     }
     103             : 
     104         180 :     const std::string& sort() const
     105             :     {
     106         180 :       return m_sort;
     107             :     }
     108             : 
     109             :     std::string& sort()
     110             :     {
     111             :       return m_sort;
     112             :     }
     113             : 
     114             :     // If the cardinality is zero, the sort and the values are ignored in the FSM.
     115         180 :     std::size_t cardinality() const
     116             :     {
     117         180 :       return m_cardinality;
     118             :     }
     119             : 
     120             :     std::size_t& cardinality()
     121             :     {
     122             :       return m_cardinality;
     123             :     }
     124             : 
     125         180 :     const std::vector<std::string>& values() const
     126             :     {
     127         180 :       return m_values;
     128             :     }
     129             : 
     130             :     std::vector<std::string>& values()
     131             :     {
     132             :       return m_values;
     133             :     }
     134             : };
     135             : 
     136             : /// \brief Transitions in an FSM
     137             : ///
     138             : /// \note All state numbers in an FSM file are larger or equal to 1. When reading one is subtracted.
     139        1657 : class fsm_transition
     140             : {
     141             :   protected:
     142             :     std::size_t m_source;
     143             :     detail::lts_fsm_base::probabilistic_state m_target;
     144             :     std::string m_label;
     145             : 
     146             :   public:
     147             :     fsm_transition(std::size_t source, std::size_t target, const std::string& label)
     148             :       : m_source(source - 1),
     149             :         m_target(detail::lts_fsm_base::probabilistic_state(target - 1)),
     150             :         m_label(label)
     151             :     {
     152             :       if (source == 0 || target == 0)
     153             :       {
     154             :         throw mcrl2::runtime_error("A transition contains a state with state number 0.");
     155             :       }
     156             :     }
     157             : 
     158        1657 :     fsm_transition(const std::string& source_text, const std::string& target_text, const std::string& label)
     159        1657 :       : m_label(label)
     160             :     {
     161        1657 :       std::size_t source = utilities::parse_natural_number(source_text);
     162        1657 :       if (source == 0)
     163             :       {
     164           0 :         throw mcrl2::runtime_error("A transition constains a source state with number 0.");
     165             :       }
     166        1657 :       m_source = source - 1;
     167        1657 :       m_target = parse_distribution(target_text);
     168        1657 :     }
     169             : 
     170             :     std::size_t source() const
     171             :     {
     172             :       return m_source;
     173             :     }
     174             : 
     175        3314 :     std::size_t& source()
     176             :     {
     177        3314 :       return m_source;
     178             :     }
     179             : 
     180             :     const lts_fsm_base::probabilistic_state& target() const
     181             :     {
     182             :       return m_target;
     183             :     }
     184             : 
     185        3314 :     lts_fsm_base::probabilistic_state& target()
     186             :     {
     187        3314 :       return m_target;
     188             :     }
     189             : 
     190             :     const std::string& label() const
     191             :     {
     192             :       return m_label;
     193             :     }
     194             : 
     195        4381 :     std::string& label()
     196             :     {
     197        4381 :       return m_label;
     198             :     }
     199             : };
     200             : 
     201         119 : struct fsm_builder
     202             : {
     203         119 :   explicit fsm_builder(probabilistic_lts_fsm_t& fsm_)
     204         119 :     : fsm(fsm_),
     205         119 :       m_initial_state_is_set(false)
     206         119 :   {}
     207             : 
     208             :   // Contains the result
     209             :   probabilistic_lts_fsm_t& fsm;
     210             : 
     211             :   // The parameters of the FSM
     212             :   std::vector<fsm_parameter> parameters;
     213             : 
     214             :   // Maps labels of the FSM to numbers
     215             :   std::map<std::string, std::size_t> labels;
     216             : 
     217             :   // This variable records if the initial state is set explicitly.
     218             :   // If not it needs to be done while finishing the fsm.
     219             :   bool m_initial_state_is_set;
     220             : 
     221         119 :   void start()
     222             :   {
     223         119 :     parameters.clear();
     224         119 :     labels.clear();
     225         119 :     labels[action_label_string::tau_action()] = 0; // The label 0 is the tau action by default.
     226         119 :     fsm.clear();
     227         119 :   }
     228             : 
     229        1657 :   void add_transition(const std::string& source, const std::string& target, const std::string& label)
     230             :   {
     231        3314 :     fsm_transition t(source, target, label);
     232        1657 :     std::size_t max = t.source();
     233        3418 :     for (const detail::lts_fsm_base::state_probability_pair& p: t.target())
     234             :     {
     235        1761 :       max = std::max(max, p.state());
     236             :     }
     237        1657 :     max += 1; // Apply a correction for the mismatch between numbering in lts_fsm and the fsm file format
     238        1657 :     if (fsm.num_states() <= max)
     239             :     {
     240         797 :       fsm.set_num_states(max, fsm.has_state_info());
     241             :     }
     242        1657 :     auto i = labels.find(t.label());
     243        1657 :     lts_fsm_t::labels_size_type label_index = 0;
     244        1657 :     if (i == labels.end())
     245             :     {
     246         908 :       assert(t.label() != action_label_string::tau_action());
     247         908 :       label_index = fsm.add_action(action_label_string(t.label()));
     248         908 :       labels[t.label()] = label_index;
     249             :     }
     250             :     else
     251             :     {
     252         749 :       label_index = i->second;
     253             :     }
     254             : 
     255        1657 :     const std::size_t probabilistic_state_index = fsm.add_probabilistic_state(detail::lts_fsm_base::probabilistic_state(t.target()));
     256        1657 :     fsm.add_transition(transition(t.source(), label_index, probabilistic_state_index));
     257        1657 :   }
     258             : 
     259         820 :   void add_state(const std::vector<std::size_t>& values)
     260             :   {
     261         820 :     fsm.add_state(state_label_fsm(values));
     262         820 :   }
     263             : 
     264         180 :   void add_parameter(const std::string& name, const std::string& cardinality, const std::string& sort, const std::vector<std::string>& domain_values)
     265             :   {
     266         180 :     parameters.emplace_back(name, cardinality, sort, domain_values);
     267         180 :   }
     268             : 
     269           8 :   void add_initial_distribution(const std::string& distribution)
     270             :   {
     271           8 :     fsm.set_initial_probabilistic_state(parse_distribution(distribution));
     272           8 :     m_initial_state_is_set = true;
     273           8 :   }
     274             : 
     275         119 :   void write_parameters()
     276             :   {
     277         119 :     std::size_t index = 0;
     278         299 :     for (const fsm_parameter& param: parameters)
     279             :     {
     280         180 :       if (param.cardinality() > 0)
     281             :       {
     282         180 :         fsm.add_process_parameter(param.name(), param.sort());
     283         636 :         for (const std::string& value: param.values())
     284             :         {
     285         456 :           fsm.add_state_element_value(index, value);
     286             :         }
     287             :       }
     288         180 :       index++;
     289             :     }
     290         119 :   }
     291             : 
     292         119 :   void finish()
     293             :   {
     294             :     // guarantee that the LTS has at least one state
     295         119 :     if (fsm.num_states() == 0)
     296             :     {
     297           0 :       fsm.add_state();
     298             :     }
     299         119 :     if (!m_initial_state_is_set)
     300             :     {
     301         111 :       fsm.set_initial_probabilistic_state(detail::lts_fsm_base::probabilistic_state(0));
     302             :     }
     303         119 :   }
     304             : };
     305             : 
     306             : } // namespace mcrl2::lts::detail
     307             : 
     308             : #endif // MCRL2_LTS_DETAIL_FSM_BUILDER_H

Generated by: LCOV version 1.13