Line data    Source code

       1             : // Author(s): Muck van Weerdenburg, Ruud Koolen; adapted by 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             : #include <limits>
      10             : #include "mcrl2/data//standard_numbers_utility.h"
      11             : #include "mcrl2/lts/simulation.h"
      12             : 
      13             : using namespace mcrl2;
      14             : using namespace mcrl2::lps;
      15             : 
      16           0 : std::vector<simulation::transition_t> simulation::transitions(const state& source_state)
      17             : {
      18             :   try
      19             :   {
      20           0 :     std::list<transition> outgoing_transitions = out_edges(source_state);
      21           0 :     std::vector<simulation::transition_t> output(outgoing_transitions.begin(), outgoing_transitions.end());
      22           0 :     return output;
      23           0 :   }
      24           0 :   catch (mcrl2::runtime_error& e)
      25             :   {
      26           0 :     mCRL2log(mcrl2::log::error) << "an error occurred while calculating the transitions from this state;\n" << e.what() << std::endl;
      27           0 :     return std::vector<simulation::transition_t>();
      28           0 :   }
      29             : }
      30             : 
      31           0 : simulation::simulation(const stochastic_specification& specification, data::rewrite_strategy strategy)
      32           0 :   : explorer(specification, explorer_options(strategy)),
      33           0 :     m_specification(specification),
      34           0 :     m_gen(),
      35           0 :     m_distrib(0,std::numeric_limits<std::size_t>::max())
      36             : {
      37           0 :   state_type initial_state;
      38           0 :   compute_stochastic_state(initial_state, m_initial_distribution, m_initial_state, m_global_sigma, m_global_rewr, m_global_enumerator);
      39           0 :   simulator_state_t state;
      40           0 :   state.source_state = initial_state;
      41           0 :   state.state_number=initial_state.size();  // This indicates that no state is selected yet.
      42           0 :   m_full_trace.push_back(state);
      43             : 
      44           0 :   if (initial_state.size()==1 || m_auto_select_probabilistic_state)
      45             :   {
      46           0 :     randomly_select_state();  // There is only one state, or we select states at random. Select the state. 
      47             :   }
      48           0 : }
      49             : 
      50           0 : void simulation::truncate(std::size_t state_number, bool probabilistic)
      51             : {
      52           0 :   assert(state_number < m_full_trace.size());
      53           0 :   m_full_trace.resize(state_number + 1);
      54           0 :   if (probabilistic && m_full_trace[state_number].source_state.size()>1)  // Indicate that this is a probabilistic state and forget about transitions.
      55             :   {
      56           0 :     m_full_trace[state_number].state_number=m_full_trace[state_number].source_state.size();
      57             :   }
      58             :   
      59           0 : }
      60             : 
      61           0 : void simulation::select_state(std::size_t state_number)
      62             : {
      63           0 :   simulator_state_t& state = m_full_trace.back();
      64             : 
      65           0 :   assert(state_number<state.source_state.states.size());
      66           0 :   state.state_number=state_number;
      67           0 :   state.transitions = transitions(state.source_state.states[state_number]);
      68           0 : }
      69             : 
      70           0 : void simulation::randomly_select_state()
      71             : {
      72           0 :   simulator_state_t& state = m_full_trace.back();
      73           0 :   std::size_t state_number=0;
      74             :   
      75           0 :   if (state.source_state.states.size()>1)
      76             :   {
      77             :     // Generate a random size_t with random distribution. 
      78           0 :     double random_value=static_cast<double>(m_distrib(m_gen))/static_cast<double>(std::numeric_limits<std::size_t>::max()); 
      79           0 :     random_value=random_value-data::sort_real::value(state.source_state.probabilities[state_number]);
      80           0 :     while (random_value>0)
      81             :     {
      82           0 :       state_number++;
      83           0 :       assert(state_number<state.source_state.states.size());
      84           0 :       random_value=random_value-data::sort_real::value(state.source_state.probabilities[state_number]);
      85             :     }
      86             :   }
      87           0 :   state.state_number=state_number;
      88           0 :   state.transitions = transitions(state.source_state.states[state_number]);
      89           0 : }
      90             : 
      91           0 : void simulation::select_transition(std::size_t transition_number)
      92             : {
      93           0 :   assert(transition_number < m_full_trace.back().transitions.size());
      94           0 :   m_full_trace.back().transition_number = transition_number;
      95           0 :   simulator_state_t state;
      96           0 :   state.source_state = m_full_trace.back().transitions[transition_number].state;
      97           0 :   state.state_number=state.source_state.size();
      98           0 :   m_full_trace.push_back(state);
      99             : 
     100           0 :   if (state.source_state.size()==1 || m_auto_select_probabilistic_state)
     101             :   {
     102           0 :     randomly_select_state();
     103             :   }
     104           0 : }
     105             : 
     106           0 : void simulation::randomly_select_transition()
     107             : {
     108           0 :   std::size_t s=m_full_trace.back().transitions.size();
     109           0 :   std::size_t transition_number= m_distrib(m_gen) % s;
     110           0 :   select_transition(transition_number);
     111           0 : }
     112             : 
     113           0 : void simulation::enable_auto_select_probability(bool enable)
     114             : {
     115           0 :   m_auto_select_probabilistic_state=enable;
     116           0 : }
     117             : 
     118           0 : void simulation::save(const std::string& filename) const
     119             : {
     120           0 :   lts::trace trace;
     121           0 :   if (m_full_trace[0].state_number>=m_full_trace[0].source_state.size())
     122             :   {
     123           0 :     throw mcrl2::runtime_error("initial state is not set. Trace is not saved.");
     124             :   }
     125           0 :   trace.set_state(m_full_trace[0].source_state.states[m_full_trace[0].state_number]);
     126           0 :   for (std::size_t i = 0; i + 1 < m_full_trace.size(); i++)
     127             :   {
     128           0 :     assert(m_full_trace[i].state_number<m_full_trace[i].source_state.size());
     129           0 :     if (m_full_trace[i].transition_number<m_full_trace[i].transitions.size())
     130             :     {
     131           0 :       trace.add_action(m_full_trace[i].transitions[m_full_trace[i].transition_number].action);
     132           0 :       if (m_full_trace[i+1].state_number<m_full_trace[i+1].source_state.size())
     133             :       {
     134           0 :         trace.set_state(m_full_trace[i+1].source_state.states[m_full_trace[i+1].state_number]);
     135             :       }
     136             :       else
     137             :       {
     138           0 :         trace.set_state(m_full_trace[i+1].source_state.states[0]);
     139           0 :         std::cout << "the last state in the saved trace is the first concrete state from the last probabilistic state." << std::endl;
     140             :       }
     141             :     }
     142             :   }
     143           0 :   trace.save(filename);
     144           0 : }
     145             : 
     146           0 : void simulation::load(const std::string& filename)
     147             : {
     148             :   // Load the trace from file
     149           0 :   lts::trace trace(filename, m_specification.data(), m_specification.action_labels());
     150           0 :   trace.reset_position();
     151             : 
     152             :   // Get the first state from the generator
     153           0 :   m_full_trace.clear();
     154             : 
     155           0 :   state_type initial_state;
     156           0 :   compute_stochastic_state(initial_state, m_initial_distribution, m_initial_state, m_global_sigma, m_global_rewr, m_global_enumerator);
     157             : 
     158           0 :   add_new_state(initial_state);
     159             :   // Check that the first state (if given) matches one of the probabilistic states of the specification.
     160           0 :   if (trace.current_state_exists()) 
     161             :   {    
     162           0 :     if (std::find(initial_state.states.begin(), initial_state.states.end(), trace.current_state()) == initial_state.states.end())
     163             :     {
     164           0 :       throw mcrl2::runtime_error("The initial state of the trace does not match the initial state "
     165           0 :                                  "of this specification");
     166             :     }
     167             : 
     168             : 
     169             :     // Replay the trace using the generator.
     170           0 :     if (!match_trace_probabilistic_state(trace))
     171             :     {
     172           0 :       throw mcrl2::runtime_error("Failed to perform action " + pp(trace.current_action()) + " at position "
     173           0 :                                  + std::to_string(m_full_trace.size() - 1) + " from the trace loaded from " + filename + ".");
     174             :     }
     175             :   }
     176           0 : }
     177             : 
     178             : // Add a new state to m_full_trace with the indicated state. 
     179           0 : void simulation::add_new_state(const lps::stochastic_state& s)
     180             : {
     181           0 :   simulator_state_t state;
     182           0 :   state.source_state = s;
     183           0 :   state.state_number = s.size();
     184           0 :   state.transition_number = 0;
     185           0 :   m_full_trace.push_back(state);
     186           0 : } 
     187             : 
     188           0 : bool simulation::match_trace_probabilistic_state(lts::trace& trace)
     189             : {
     190           0 :   if (!trace.current_state_exists())
     191             :   {
     192           0 :     return true;
     193             :   } 
     194           0 :   assert(trace.current_state_exists());
     195           0 :   simulator_state_t& current = m_full_trace.back();
     196           0 :   for (std::size_t i = 0; i < current.source_state.size(); ++i)
     197             :   {
     198           0 :     if (current.source_state.states[i] == trace.current_state())
     199             :     {
     200           0 :       select_state(i);
     201           0 :       if (match_trace_transition(trace))
     202             :       {
     203           0 :         return true;
     204             :       }
     205             :     }
     206             :   }
     207           0 :   return false;
     208             : }
     209             : 
     210           0 : bool simulation::match_trace_transition(lts::trace& trace)
     211             : {
     212           0 :   if (!trace.current_action_exists())
     213             :   {
     214           0 :     return true;
     215             :   }
     216           0 :   simulator_state_t& current = m_full_trace.back();
     217           0 :   lps::multi_action action = trace.current_action();
     218           0 :   trace.increase_position();
     219           0 :   for (std::size_t i = 0; i < current.transitions.size(); ++i)
     220             :   {
     221           0 :     if (current.transitions[i].action == action)
     222             :     {
     223           0 :       add_new_state(current.transitions[i].state);
     224           0 :       current.transition_number = i;
     225           0 :       if (match_trace_probabilistic_state(trace))
     226             :       {
     227           0 :         return true;
     228             :       }
     229           0 :       m_full_trace.pop_back();
     230             :     }
     231             :   }
     232           0 :   return false;
     233           0 : }
     234             :