LCOV - code coverage report
Current view: top level - lts/include/mcrl2/lts/detail - exploration.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 11 19 57.9 %
Date: 2020-07-11 00:44:39 Functions: 5 15 33.3 %
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             : 
      10             : #ifndef MCRL2_LTS_DETAIL_EXPLORATION_NEW_H
      11             : #define MCRL2_LTS_DETAIL_EXPLORATION_NEW_H
      12             : 
      13             : #include "mcrl2/trace/trace.h"
      14             : #include "mcrl2/lts/detail/bithashtable.h"
      15             : #include "mcrl2/lts/detail/queue.h"
      16             : #include "mcrl2/lts/detail/lts_generation_options.h"
      17             : 
      18             : 
      19             : namespace mcrl2
      20             : {
      21             : namespace lts
      22             : {
      23             : namespace detail
      24             : {
      25             : 
      26             :     template <class COUNTER_EXAMPLE_GENERATOR>
      27           0 :     class state_index_pair
      28             :     {
      29             :       protected:
      30             :         lps::state m_state;
      31             :         typename COUNTER_EXAMPLE_GENERATOR::index_type m_index;
      32             : 
      33             :       public:
      34           0 :         state_index_pair(const lps::state& state, typename COUNTER_EXAMPLE_GENERATOR::index_type index)
      35             :          : m_state(state),
      36           0 :            m_index(index)
      37           0 :         {}
      38             : 
      39           0 :         lps::state state() const
      40             :         {
      41           0 :           return m_state;
      42             :         }
      43             : 
      44           0 :         typename COUNTER_EXAMPLE_GENERATOR::index_type index() const
      45             :         {
      46           0 :           return m_index;
      47             :         }
      48             :     };
      49             : 
      50             :     // The class below is used to get a unique number for a multi-action which can contain time. 
      51             :     // The class is a little complex because a multi-action is a pair of actions and time, and
      52             :     // not by itself an aterm. 
      53         374 :     class multi_action_indexed_set 
      54             :     {
      55             :       protected:
      56             :         utilities::indexed_set<action_label_lts> storage;
      57             :       
      58             :       public:
      59             :         inline
      60        1827 :         std::pair<std::size_t, bool> put(const lps::multi_action& ma) 
      61             :         {
      62        1827 :           return storage.insert(action_label_lts(ma));
      63             :         }
      64             :     };
      65             : 
      66             : } // end namespace detail
      67             : 
      68             : class lps2lts_algorithm
      69             : {
      70             :   private:
      71             :     typedef lps::next_state_generator next_state_generator;
      72             : 
      73             :   private:
      74             :     lts_generation_options m_options;
      75             :     next_state_generator *m_generator;
      76             :     next_state_generator::summand_subset_t *m_main_subset;
      77             : 
      78             :     bool m_use_confluence_reduction;
      79             :     next_state_generator::summand_subset_t m_nonprioritized_subset;
      80             :     next_state_generator::summand_subset_t m_prioritized_subset;
      81             : 
      82             :     utilities::indexed_set<lps::state> m_state_numbers;
      83             : 
      84             :     bit_hash_table m_bit_hash_table;
      85             : 
      86             :     probabilistic_lts_lts_t m_output_lts;
      87             :     detail::multi_action_indexed_set m_action_label_numbers;
      88             :     std::ofstream m_aut_file;
      89             : 
      90             :     bool m_maintain_traces;
      91             :     bool m_value_prioritize;
      92             : 
      93             :     next_state_generator::summand_subset_t m_tau_summands;
      94             : 
      95             :     std::vector<bool> m_detected_action_summands;
      96             : 
      97             :     std::map<lps::state, lps::state> m_backpointers;
      98             :     std::size_t m_traces_saved;
      99             : 
     100             :     std::size_t m_num_states;
     101             :     std::size_t m_num_transitions;
     102             :     next_state_generator::transition_t::state_probability_list m_initial_states;
     103             :     std::size_t m_level;
     104             : 
     105             :     std::unordered_set<lps::state> non_divergent_states;  // This set is filled with states proven not to be divergent,
     106             :                                                           // when lps2lts_algorithm is requested to search for divergencies.
     107             : 
     108             :     volatile bool m_must_abort;
     109             : 
     110             :   public:
     111         187 :     lps2lts_algorithm() :
     112             :       m_generator(nullptr),
     113         187 :       m_must_abort(false)
     114             :     {
     115         187 :       m_action_label_numbers.put(action_label_lts::tau_action());  // The action tau has index 0 by default.
     116         187 :     }
     117             : 
     118         187 :     ~lps2lts_algorithm()
     119         187 :     {
     120         187 :       delete m_generator;
     121         187 :     }
     122             : 
     123             :     bool generate_lts(const lts_generation_options& options);
     124             : 
     125             :     void abort()
     126             :     {
     127             :       // Stops the exploration algorithm if it is running by making sure
     128             :       // not a single state can be generated anymore.
     129             :       if (!m_must_abort)
     130             :       {
     131             :         m_must_abort = true;
     132             :         mCRL2log(log::warning) << "state space generation was aborted prematurely" << std::endl;
     133             :       }
     134             :     }
     135             : 
     136             :   private:
     137             :     void initialise_lts_generation(const lts_generation_options& options);
     138             :     void finalise_lts_generation();
     139             :     data::data_expression_vector generator_state(const lps::state& storage_state);
     140             :     lps::state storage_state(const data::data_expression_vector& generator_state);
     141             :     void set_prioritised_representatives(next_state_generator::transition_t::state_probability_list& states);
     142             :     lps::state get_prioritised_representative(const lps::state& state1);
     143             :     void value_prioritize(std::vector<next_state_generator::transition_t>& transitions);
     144             :     bool save_trace(const lps::state& state1, const std::string& filename);
     145             :     bool save_trace(const lps::state& state1, const next_state_generator::transition_t& transition, const std::string& filename);
     146             :     void construct_trace(const lps::state& state1, mcrl2::trace::Trace& trace);
     147             : 
     148             :     bool is_nondeterministic(std::vector<lps2lts_algorithm::next_state_generator::transition_t>& transitions,
     149             :                              next_state_generator::transition_t& nondeterminist_transition);
     150             :     template <class COUNTER_EXAMPLE_GENERATOR>
     151             :     bool search_divergence(const detail::state_index_pair<COUNTER_EXAMPLE_GENERATOR>& state,
     152             :                            std::set<lps::state>& current_path, std::set<lps::state>& visited,
     153             :                            COUNTER_EXAMPLE_GENERATOR& divergence_loop);
     154             :     template <class COUNTER_EXAMPLE_GENERATOR>
     155             :     void check_divergence(const detail::state_index_pair<COUNTER_EXAMPLE_GENERATOR>& state,
     156             :                           COUNTER_EXAMPLE_GENERATOR divergence_loop);
     157             :     void save_actions(const lps::state& state, const next_state_generator::transition_t& transition);
     158             :     void save_deadlock(const lps::state& state);
     159             :     void save_nondeterministic_state(const lps::state& state, const next_state_generator::transition_t& nondeterminist_transition);
     160             :     void save_error(const lps::state& state);
     161             :     std::pair<std::size_t, bool> get_state_number(const lps::state& target_state);
     162             :     std::size_t add_target_state(
     163             :                          const lps::state& source_state, 
     164             :                          const lps::state& target_state,
     165             :                          const std::function<void(const lps::state&)> add_state_to_todo_queue_function);
     166             :     void add_transition(const lps::state& source_state, 
     167             :                          const next_state_generator::transition_t& transition,
     168             :                          const std::function<void(const lps::state&)> add_state_to_todo_queue_function);
     169             :     void get_transitions(const lps::state& state,
     170             :                          std::vector<lps2lts_algorithm::next_state_generator::transition_t>& transitions,
     171             :                          next_state_generator::enumerator_queue_t& enumeration_queue
     172             :     );
     173             :     void generate_lts_breadth_todo_max_is_npos(const next_state_generator::transition_t::state_probability_list& initial_states);
     174             :     void generate_lts_breadth_todo_max_is_not_npos(const next_state_generator::transition_t::state_probability_list& initial_states);
     175             :     void generate_lts_breadth_bithashing(const next_state_generator::transition_t::state_probability_list& initial_states);
     176             :     void generate_lts_depth(const next_state_generator::transition_t::state_probability_list& initial_states);
     177             :     void generate_lts_random(const next_state_generator::transition_t::state_probability_list& initial_states);
     178             :     void print_target_distribution_in_aut_format(
     179             :                const lps::next_state_generator::transition_t::state_probability_list& state_probability_list,
     180             :                const std::size_t last_state_number,
     181             :                const lps::state& source_state,
     182             :                const std::function<void(const lps::state&)> add_state_to_todo_queue_function);
     183             :     void print_target_distribution_in_aut_format(
     184             :                 const lps::next_state_generator::transition_t::state_probability_list& state_probability_list,
     185             :                 const lps::state& source_state,
     186             :                 const std::function<void(const lps::state&)> add_state_to_todo_queue_function);
     187             :     probabilistic_state<std::size_t, lps::probabilistic_data_expression> transform_initial_probabilistic_state_list
     188             :                  (const next_state_generator::transition_t::state_probability_list& initial_states);
     189             :     probabilistic_state<std::size_t, lps::probabilistic_data_expression> create_a_probabilistic_state_from_target_distribution(
     190             :                const std::size_t base_state_number,
     191             :                const next_state_generator::transition_t::state_probability_list& other_probabilities,
     192             :                const lps::state& source_state,
     193             :                const std::function<void(const lps::state&)> add_state_to_todo_queue_function);
     194             : 
     195             : 
     196             : };
     197             : 
     198             : } // namespace lps
     199             : 
     200             : } // namespace mcrl2
     201             : 
     202             : #endif // MCRL2_LTS_DETAIL_EXPLORATION_H

Generated by: LCOV version 1.13