LCOV - code coverage report
Current view: top level - lps/include/mcrl2/lps - next_state_generator.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 51 54 94.4 %
Date: 2020-09-16 00:45:56 Functions: 40 43 93.0 %
Legend: Lines: hit not hit

          Line data    Source code
       1             : // Author(s): Ruud Koolen
       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 next_state_generator.h
      10             : 
      11             : #ifndef MCRL2_LPS_NEXT_STATE_GENERATOR_H
      12             : #define MCRL2_LPS_NEXT_STATE_GENERATOR_H
      13             : 
      14             : #include "mcrl2/atermpp/detail/shared_subset.h"
      15             : #include "mcrl2/data/enumerator_with_iterator.h"
      16             : #include "mcrl2/lps/probabilistic_data_expression.h"
      17             : #include "mcrl2/lps/state.h"
      18             : #include "mcrl2/lps/state_probability_pair.h"
      19             : #include "mcrl2/lps/stochastic_specification.h"
      20             : 
      21             : namespace mcrl2
      22             : {
      23             : 
      24             : namespace lps
      25             : {
      26             : 
      27             : class next_state_generator
      28             : {
      29             :   public:
      30             :     typedef std::list<data::data_expression_list> summand_enumeration_t;
      31             :     typedef atermpp::term_appl<data::data_expression> condition_arguments_t;
      32             : 
      33             :     typedef data::rewriter rewriter_t;
      34             :     typedef data::enumerator_algorithm_with_iterator<> enumerator_t;
      35             :     typedef enumerator_t::iterator enumerator_iterator_t;
      36             :     typedef data::enumerator_queue<data::enumerator_list_element_with_substitution<> > enumerator_queue_t;
      37             : 
      38             :     typedef data::rewriter::substitution_type substitution_t;
      39             : 
      40             :   protected:
      41        3336 :     struct action_internal_t
      42             :     {
      43             :       process::action_label label;
      44             :       data::data_expression_vector arguments;
      45             :     };
      46             : 
      47        3562 :     struct summand_t
      48             :     {
      49             :       stochastic_action_summand *summand;
      50             :       data::variable_list variables;
      51             :       data::data_expression condition;
      52             :       stochastic_distribution distribution;
      53             :       data::data_expression_vector result_state;
      54             :       std::vector<action_internal_t> action_label;
      55             :       data::data_expression time_tag;
      56             : 
      57             :       std::vector<std::size_t> condition_parameters;
      58             :       atermpp::function_symbol condition_arguments_function;
      59             :       atermpp::aterm_appl condition_arguments_function_dummy;
      60             :       std::map<condition_arguments_t, summand_enumeration_t> enumeration_cache;
      61             :     };
      62             : 
      63        2909 :     struct pruning_tree_node_t
      64             :     {
      65             :       atermpp::detail::shared_subset<summand_t> summand_subset;
      66             :       std::map<data::data_expression, pruning_tree_node_t> children;
      67             :     };
      68             : 
      69             :   public:
      70             :     class iterator;
      71             : 
      72        1278 :     class summand_subset_t
      73             :     {
      74             :       friend class next_state_generator;
      75             :       friend class next_state_generator::iterator;
      76             : 
      77             :       public:
      78             :         /// \brief Trivial constructor. Constructs an invalid command subset.
      79         784 :         summand_subset_t() {}
      80             : 
      81             :         /// \brief Constructs the full summand subset for the given generator.
      82             :         summand_subset_t(next_state_generator *generator, bool use_summand_pruning);
      83             : 
      84             :         /// \brief Constructs the summand subset containing the given commands.
      85             :         summand_subset_t(next_state_generator *generator, const stochastic_action_summand_vector& summands, bool use_summand_pruning);
      86             : 
      87             :       private:
      88             :         next_state_generator *m_generator;
      89             :         bool m_use_summand_pruning;
      90             : 
      91             :         std::vector<std::size_t> m_summands;
      92             : 
      93             :         pruning_tree_node_t m_pruning_tree;
      94             :         std::vector<std::size_t> m_pruning_parameters;
      95             :         substitution_t m_pruning_substitution;
      96             : 
      97             :         static bool summand_set_contains(const std::set<stochastic_action_summand>& summand_set, const summand_t& summand);
      98             :         void build_pruning_parameters(const stochastic_action_summand_vector& summands);
      99             :         bool is_not_false(const summand_t& summand);
     100             :         atermpp::detail::shared_subset<summand_t>::iterator begin(const lps::state& state);
     101             :     };
     102             : 
     103             :     typedef mcrl2::lps::state_probability_pair<lps::state, lps::probabilistic_data_expression> state_probability_pair;
     104             : 
     105       32046 :     class transition_t
     106             :     {
     107             :       public:
     108             :         typedef std::forward_list<state_probability_pair> state_probability_list;
     109             : 
     110             :       protected:
     111             :         lps::multi_action m_action;
     112             :         lps::state m_target_state;
     113             :         std::size_t m_summand_index;
     114             :         // The following list contains all but one target states with their probabity.
     115             :         // m_target_state is the other state, with the residual probability, such
     116             :         // that all probabilities add up to 1.
     117             :         state_probability_list m_other_target_states;
     118             : 
     119             :       public:
     120        5069 :         const lps::multi_action& action() const
     121             :         {
     122        5069 :           return m_action;
     123             :         }
     124             : 
     125        3278 :         void set_action(const lps::multi_action& action)
     126             :         {
     127        3278 :           m_action=action;
     128        3278 :         }
     129             : 
     130        5026 :         const lps::state& target_state() const { return m_target_state; }
     131        3842 :         void set_target_state(const lps::state& target_state)
     132             :         {
     133        3842 :           m_target_state=target_state;
     134        3842 :         }
     135             : 
     136           0 :         std::size_t summand_index() const { return m_summand_index; }
     137        3278 :         void set_summand_index(const std::size_t summand_index)
     138             :         {
     139        3278 :           m_summand_index=summand_index;
     140        3278 :         }
     141             : 
     142        2513 :         const state_probability_list& other_target_states() const { return m_other_target_states; }
     143        3278 :         void set_other_target_states(const state_probability_list& other_target_states)
     144             :         {
     145        3278 :           m_other_target_states=other_target_states;
     146        3278 :         }
     147             :     };
     148             : 
     149       15796 :     class iterator: public boost::iterator_facade<iterator, const transition_t, boost::forward_traversal_tag>
     150             :     {
     151             :       protected:
     152             :         transition_t m_transition;
     153             :         next_state_generator* m_generator;
     154             :         lps::state m_state;
     155             :         substitution_t* m_substitution;
     156             :         substitution_t* m_base_substitution;
     157             : 
     158             :         bool m_single_summand;
     159             :         std::size_t m_single_summand_index;
     160             :         bool m_use_summand_pruning;
     161             :         std::vector<std::size_t>::iterator m_summand_iterator;
     162             :         std::vector<std::size_t>::iterator m_summand_iterator_end;
     163             :         atermpp::detail::shared_subset<summand_t>::iterator m_summand_subset_iterator;
     164             :         summand_t *m_summand;
     165             : 
     166             :         bool m_cached;
     167             :         summand_enumeration_t::iterator m_enumeration_cache_iterator;
     168             :         summand_enumeration_t::iterator m_enumeration_cache_end;
     169             :         enumerator_iterator_t m_enumeration_iterator;
     170             :         bool m_caching;
     171             :         condition_arguments_t m_enumeration_cache_key;
     172             :         summand_enumeration_t m_enumeration_log;
     173             : 
     174             :         enumerator_queue_t* m_enumeration_queue;
     175             : 
     176             :         /// \brief Enumerate <variables, phi> with substitution sigma.
     177       14572 :         void enumerate(const data::variable_list& variables, const data::data_expression& phi, data::mutable_indexed_substitution<>& sigma)
     178             :         {
     179       14572 :           m_enumeration_queue->clear();
     180       14572 :           m_enumeration_queue->push_back(data::enumerator_list_element_with_substitution<>(variables, phi));
     181             :           try
     182             :           {
     183       14572 :             m_enumeration_iterator = m_generator->m_enumerator.begin(sigma, *m_enumeration_queue);
     184             :           }
     185           0 :           catch (mcrl2::runtime_error &e)
     186             :           {
     187           0 :             throw mcrl2::runtime_error(std::string(e.what()) + "\nProblem occurred when enumerating variables " + data::pp(variables) + " in " + data::pp(phi));
     188             :           }
     189       14572 :         }
     190             : 
     191             : 
     192             :       public:
     193        4021 :         iterator()
     194        4021 :           : m_generator(nullptr)
     195             :         {
     196        4021 :         }
     197             : 
     198             :         iterator(next_state_generator* generator, const lps::state& state, substitution_t* substitution, substitution_t* base_substitution, summand_subset_t& summand_subset, enumerator_queue_t* enumeration_queue);
     199             : 
     200             :         iterator(next_state_generator* generator, const lps::state& state, substitution_t* substitution, substitution_t* base_substitution, std::size_t summand_index, enumerator_queue_t* enumeration_queue);
     201             : 
     202       11771 :         operator bool() const
     203             :         {
     204       11771 :           return m_generator != nullptr;
     205             :         }
     206             : 
     207             :       private:
     208             :         friend class boost::iterator_core_access;
     209             : 
     210        4021 :         bool equal(const iterator& other) const
     211             :         {
     212        4021 :           return (!(bool)*this && !(bool)other) || (this == &other);
     213             :         }
     214             : 
     215        5218 :         const transition_t& dereference() const
     216             :         {
     217        5218 :           return m_transition;
     218             :         }
     219             : 
     220             :         void increment();
     221             :         bool summand_finished();
     222             :     };
     223             : 
     224             :   protected:
     225             :     stochastic_specification m_specification;
     226             :     rewriter_t m_rewriter;
     227             :     substitution_t m_substitution;
     228             :     substitution_t m_base_substitution;
     229             :     data::enumerator_identifier_generator m_id_generator;
     230             :     enumerator_t m_enumerator;
     231             : 
     232             :     bool m_use_enumeration_caching;
     233             : 
     234             :     data::variable_vector m_process_parameters;
     235             :     std::vector<summand_t> m_summands;
     236             :     transition_t::state_probability_list m_initial_states;
     237             : 
     238             :     summand_subset_t m_all_summands;
     239             : 
     240             :   public:
     241             :     /// \brief Constructor.
     242             :     /// \param spec The process specification.
     243             :     /// \param rewriter The rewriter used.
     244             :     /// \param base_substitution A substitution from variables to terms in normal form, used to replace variables occurring the in
     245             :     ///        the specification. The rhs's in the substitution are assumed to be in normal form. It can be useful to replace closed
     246             :     ///        expressions in the lps by variables, and put there rhs's in the base_substitution to avoid rewriting these expressions
     247             :     ///        repeatedly.
     248             :     /// \param use_enumeration_caching Cache intermediate enumeration results.
     249             :     /// \param use_summand_pruning Preprocess summands using pruning strategy.
     250             :     next_state_generator(const stochastic_specification& spec,
     251             :                          const data::rewriter& rewriter,
     252             :                          const substitution_t& base_substitution = data::mutable_indexed_substitution<>(),
     253             :                          bool use_enumeration_caching = false,
     254             :                          bool use_summand_pruning = false);
     255             : 
     256             :     ~next_state_generator();
     257             : 
     258             :     /// \brief Returns an iterator for generating the successors of the given state.
     259         312 :     iterator begin(const state& state, enumerator_queue_t* enumeration_queue)
     260             :     {
     261         312 :       return iterator(this, state, &m_substitution, &m_base_substitution, m_all_summands, enumeration_queue);
     262             :     }
     263             : 
     264             :     /// \brief Returns an iterator for generating the successors of the given state.
     265        1919 :     iterator begin(const state& state, summand_subset_t& summand_subset, enumerator_queue_t* enumeration_queue)
     266             :     {
     267        1919 :       return iterator(this, state, &m_substitution, &m_base_substitution, summand_subset, enumeration_queue);
     268             :     }
     269             : 
     270             :     /// \brief Returns an iterator for generating the successors of the given state.
     271             :     /// Only the successors with respect to the summand with the given index are generated.
     272        2996 :     iterator begin(const state& state, std::size_t summand_index, enumerator_queue_t* enumeration_queue)
     273             :     {
     274        2996 :       return iterator(this, state, &m_substitution, &m_base_substitution, summand_index, enumeration_queue);
     275             :     }
     276             : 
     277             :     /// \brief Returns an iterator pointing to the end of a next state list.
     278        4021 :     iterator end()
     279             :     {
     280        4021 :       return iterator();
     281             :     }
     282             : 
     283             :     /// \brief Gets the initial state.
     284         217 :     const transition_t::state_probability_list& initial_states() const
     285             :     {
     286         217 :       return m_initial_states;
     287             :     }
     288             : 
     289             :     /// \brief Returns the rewriter associated with this generator.
     290         129 :     rewriter_t& get_rewriter()
     291             :     {
     292         129 :       return m_rewriter;
     293             :     }
     294             : 
     295             :     /// \brief Returns a reference to the summand subset containing all summands.
     296         175 :     summand_subset_t& full_subset()
     297             :     {
     298         175 :       return m_all_summands;
     299             :     }
     300             : 
     301             :     // Calculate the set of states with associated probabilities from a symbolic state
     302             :     // and an associated stochastic distribution for the free variables in that state.
     303             :     // The result is a list of closed states with associated probabilities.
     304             :     const transition_t::state_probability_list calculate_distribution(
     305             :                          const stochastic_distribution& dist,
     306             :                          const data::data_expression_vector& state_args,
     307             :                          substitution_t& sigma);
     308             : };
     309             : 
     310             : } // namespace lps
     311             : 
     312             : } // namespace mcrl2
     313             : 
     314             : #endif // MCRL2_LPS_NEXT_STATE_GENERATOR_H

Generated by: LCOV version 1.13