Line data    Source code

       1             : // Author(s): Jan Friso Groote; Based on a simulator by Ruud Koolen and Muck van Weerdenburg.
       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             : #ifndef MCRL2_LPS_SIMULATION_H
      10             : #define MCRL2_LPS_SIMULATION_H
      11             : 
      12             : #include "mcrl2/lps/explorer.h"
      13             : #include "mcrl2/lts/trace.h"
      14             : 
      15             : namespace mcrl2
      16             : {
      17             : 
      18             : namespace lps  // TODO: This should become lts. We should not declare objects in namespace lps within the lts library. 
      19             : {
      20             : 
      21             : /// \brief Simulation process.
      22             : // A simulation is effectively a trace annotated with outgoing transition information
      23             : // and an operation to extend the trace with an outgoing transition from the last state.
      24             : class simulation : protected explorer<true, false, stochastic_specification>
      25             : {
      26             :   public:
      27             : 
      28             :     typedef transition transition_t;
      29             : 
      30             :     struct simulator_state_t
      31             :     {
      32             :       lps::stochastic_state source_state;
      33             :       std::size_t state_number; // This represents the number of the selected probabilistic state, or a number out of range
      34             :                                 // if not source state is chosen.
      35             :       std::vector<transition_t> transitions;
      36             :       std::size_t transition_number; // This indicates the chosen transition, or a number out of range if no transition is chosen.
      37             :     };
      38             : 
      39             :     /// Constructor.
      40             :     simulation(const stochastic_specification& specification, data::rewrite_strategy strategy = data::rewrite_strategy());
      41             : 
      42             :     /// Returns the current annotated state vector.
      43             :     const std::deque<simulator_state_t>& trace() const { return m_full_trace; }
      44             : 
      45             :     /// Remove states from the end of the simulation, making \a state_number the last state.
      46             :     void truncate(std::size_t state_number, bool probabilistic);
      47             : 
      48             :     /// Choose one state among a sequence of probabilistic states. 
      49             :     void select_state(std::size_t state_number);
      50             : 
      51             :     /// Randomly choose one state among a sequence of probabilistic states. 
      52             :     void randomly_select_state();
      53             : 
      54             :     /// Choose outgoing transition indexed by transition_number and add its state to the state vector.
      55             :     void select_transition(std::size_t transition_number);
      56             : 
      57             :     /// Randomly choose an outgoing transition and add its state to the state vector.
      58             :     void randomly_select_transition();
      59             : 
      60             :     /// Indicate whether a probabilistic state has been selected.
      61             :     bool probabilistic_state_must_be_selected(const std::size_t state_index) const
      62             :     {
      63             :       assert(state_index<trace().size());
      64             :       const simulator_state_t& current_state = trace()[state_index];
      65             :       return current_state.state_number>=current_state.source_state.size();
      66             :     }
      67             : 
      68             :     /// If enabled, automatically a probabilistic state is chosen using its intrinsic probability. 
      69             :     void enable_auto_select_probability(bool enable);
      70             : 
      71             :     /// Save the trace to a file.
      72             :     void save(const std::string& filename) const;
      73             : 
      74             :     /// Load a trace from a file.
      75             :     void load(const std::string& filename);
      76             : 
      77           0 :     virtual ~simulation()
      78           0 :     {}
      79             : 
      80             :   protected:
      81             :     stochastic_specification m_specification;
      82             : 
      83             :     bool m_auto_select_probabilistic_state=false;
      84             :     std::mt19937 m_gen; // mersenne_twister_engine seeded with rd().
      85             :     std::uniform_int_distribution<std::size_t> m_distrib; // A random generator with a uniform distribution. 
      86             : 
      87             :     // The complete trace.
      88             :     std::deque<simulator_state_t> m_full_trace;
      89             : 
      90             :     std::vector<transition_t> transitions(const lps::state& source_state);
      91             : 
      92             :     bool match_trace_probabilistic_state(lts::trace& trace);
      93             :     bool match_trace_transition(lts::trace& trace);
      94             :     void add_new_state(const lps::stochastic_state& s);
      95             :     void add_transitions();
      96             : 
      97             : };
      98             : 
      99             : } // namespace lps
     100             : 
     101             : } // namespace mcrl2
     102             : 
     103             : #endif