LCOV - code coverage report
Current view: top level - lps/source - simulation.cpp (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 1 160 0.6 %
Date: 2020-02-28 00:44:21 Functions: 2 15 13.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             : #include "mcrl2/lps/simulation.h"
      10             : 
      11             : using namespace mcrl2;
      12             : using namespace mcrl2::lps;
      13             : 
      14           0 : simulation::simulation(const stochastic_specification& specification, data::rewrite_strategy strategy)
      15             :   : m_specification(specification),
      16           0 :     m_rewriter(m_specification.data(), strategy),
      17           0 :     m_generator(stochastic_specification(m_specification), m_rewriter),
      18           0 :     m_tau_prioritization(false)
      19             : {
      20           0 :   state_t state;
      21           0 :   if (++m_generator.initial_states().begin()!=m_generator.initial_states().end()) // size()>1
      22             :   {
      23           0 :     mCRL2log(mcrl2::log::warning) << "This simulator does not take the initial distribution into account. It just picks one state.\n";
      24             :   }
      25           0 :   state.source_state = m_generator.initial_states().front().state();
      26           0 :   state.transitions = transitions(state.source_state);
      27           0 :   m_full_trace.push_back(state);
      28           0 : }
      29             : 
      30           0 : void simulation::truncate(std::size_t state_number)
      31             : {
      32           0 :   assert(state_number < m_full_trace.size());
      33           0 :   if (m_tau_prioritization)
      34             :   {
      35           0 :     m_prioritized_trace.resize(state_number + 1);
      36           0 :     m_prioritized_originals.resize(state_number + 1);
      37           0 :     m_full_trace.resize(m_prioritized_originals.back() + 1);
      38             :   }
      39             :   else
      40             :   {
      41           0 :     m_full_trace.resize(state_number + 1);
      42             :   }
      43           0 : }
      44             : 
      45           0 : void simulation::select(std::size_t transition_number)
      46             : {
      47           0 :   assert(transition_number < m_full_trace.back().transitions.size());
      48           0 :   if (m_tau_prioritization)
      49             :   {
      50           0 :     m_prioritized_trace.back().transition_number = transition_number;
      51           0 :     state_t prioritized_state;
      52           0 :     prioritized_state.source_state = m_prioritized_trace.back().transitions[transition_number].destination;
      53           0 :     prioritized_state.transitions = prioritize(transitions(prioritized_state.source_state));
      54           0 :     m_prioritized_trace.push_back(prioritized_state);
      55             : 
      56           0 :     m_full_trace.back().transition_number = transition_number;
      57           0 :     state_t full_state;
      58           0 :     full_state.source_state = m_full_trace.back().transitions[transition_number].destination;
      59           0 :     full_state.transitions = transitions(full_state.source_state);
      60           0 :     m_full_trace.push_back(full_state);
      61             : 
      62             :     while (true)
      63             :     {
      64           0 :       bool found = false;
      65           0 :       std::vector<transition_t> &transitions = m_full_trace.back().transitions;
      66           0 :       for (std::size_t index = 0; index < transitions.size(); index++)
      67             :       {
      68           0 :         if (is_prioritized(transitions[index].action))
      69             :         {
      70           0 :           m_full_trace.back().transition_number = index;
      71           0 :           state_t state;
      72           0 :           state.source_state = transitions[index].destination;
      73           0 :           state.transitions = simulation::transitions(state.source_state);
      74           0 :           m_full_trace.push_back(state);
      75           0 :           found = true;
      76           0 :           break;
      77             :         }
      78             :       }
      79           0 :       if (!found)
      80             :       {
      81           0 :         break;
      82             :       }
      83           0 :     }
      84             : 
      85           0 :     m_prioritized_originals.push_back(m_full_trace.size() - 1);
      86             :   }
      87             :   else
      88             :   {
      89           0 :     m_full_trace.back().transition_number = transition_number;
      90           0 :     state_t state;
      91           0 :     state.source_state = m_full_trace.back().transitions[transition_number].destination;
      92           0 :     state.transitions = transitions(state.source_state);
      93           0 :     m_full_trace.push_back(state);
      94             :   }
      95           0 : }
      96             : 
      97           0 : void simulation::enable_tau_prioritization(bool enable, const std::string& action)
      98             : {
      99           0 :   m_tau_prioritization = enable;
     100           0 :   m_prioritized_action = action;
     101             : 
     102           0 :   m_prioritized_trace.clear();
     103           0 :   m_prioritized_originals.clear();
     104           0 :   if (enable)
     105             :   {
     106           0 :     prioritize_trace();
     107             :   }
     108           0 : }
     109             : 
     110           0 : void simulation::save(const std::string &filename)
     111             : {
     112           0 :   trace::Trace trace;
     113           0 :   trace.setState(m_full_trace[0].source_state);
     114           0 :   for (std::size_t i = 0; i + 1 < m_full_trace.size(); i++)
     115             :   {
     116           0 :     trace.addAction(m_full_trace[i].transitions[m_full_trace[i].transition_number].action);
     117           0 :     trace.setState(m_full_trace[i+1].source_state);
     118             :   }
     119           0 :   trace.save(filename);
     120           0 : }
     121             : 
     122           0 : void simulation::load(const std::string &filename)
     123             : {
     124             :   // Load the trace from file
     125           0 :   trace::Trace trace(filename, m_specification.data(), m_specification.action_labels());
     126           0 :   trace.resetPosition();
     127             : 
     128             :   // Get the first state from the generator
     129           0 :   m_full_trace.clear();
     130           0 :   if (++m_generator.initial_states().begin()!=m_generator.initial_states().end()) // size()>1
     131             :   {
     132           0 :     mCRL2log(mcrl2::log::warning) << "This simulator does not take distributions into account. It just picks a state.\n";
     133             :   }
     134             :   // push_back(m_generator.initial_state());
     135           0 :   push_back(m_generator.initial_states().front().state());
     136             : 
     137             :   // Check that the first state (if given) matches the first state of our generator
     138           0 :   if (trace.current_state_exists() && trace.currentState() != m_full_trace.back().source_state)
     139             :   {
     140             :     throw mcrl2::runtime_error("The initial state of the trace does not match the initial state "
     141           0 :                                "of this specification");
     142             :   }
     143             : 
     144             :   // Replay the trace using the generator.
     145           0 :   if (!match_trace(trace))
     146             :   {
     147           0 :     std::stringstream ss;
     148           0 :     ss << "could not perform action " << (m_full_trace.size() - 1) << " ("
     149           0 :        << pp(trace.currentAction()) << ") from trace";
     150           0 :     throw mcrl2::runtime_error(ss.str());
     151             :   }
     152             : 
     153             :   // Perform tau-prioritization if necessary
     154           0 :   if (m_tau_prioritization)
     155             :   {
     156           0 :     m_prioritized_trace.clear();
     157           0 :     m_prioritized_originals.clear();
     158           0 :     prioritize_trace();
     159             :   }
     160           0 : }
     161             : 
     162           0 : std::vector<simulation::transition_t> simulation::transitions(const state& source_state)
     163             : {
     164             :   try
     165             :   {
     166           0 :     std::vector<simulation::transition_t> output;
     167           0 :     next_state_generator::enumerator_queue_t enumeration_queue;
     168           0 :     for (next_state_generator::iterator i = m_generator.begin(source_state, &enumeration_queue); i != m_generator.end(); i++)
     169             :     {
     170           0 :       transition_t transition;
     171           0 :       transition.destination = i->target_state();
     172           0 :       transition.action = i->action();
     173           0 :       output.push_back(transition);
     174             :     }
     175           0 :     return output;
     176             :   }
     177           0 :   catch (mcrl2::runtime_error& e)
     178             :   {
     179           0 :     mCRL2log(mcrl2::log::error) << "an error occurred while calculating the transitions from this state;\n" << e.what() << std::endl;
     180           0 :     return std::vector<simulation::transition_t>();
     181             :   }
     182             : }
     183             : 
     184           0 : std::vector<simulation::transition_t> simulation::prioritize(const std::vector<simulation::transition_t> &transitions)
     185             : {
     186           0 :   std::vector<simulation::transition_t> output;
     187           0 :   for (std::vector<simulation::transition_t>::const_iterator i = transitions.begin(); i != transitions.end(); i++)
     188             :   {
     189           0 :     simulation::transition_t transition = *i;
     190             :     while (true)
     191             :     {
     192           0 :       bool found = false;
     193           0 :       std::vector<transition_t> next_transitions = simulation::transitions(transition.destination);
     194           0 :       for (std::vector<transition_t>::iterator j = next_transitions.begin(); j != next_transitions.end(); j++)
     195             :       {
     196           0 :         if (is_prioritized(j->action))
     197             :         {
     198           0 :           transition.destination = j->destination;
     199           0 :           found = true;
     200           0 :           break;
     201             :         }
     202             :       }
     203           0 :       if (!found)
     204             :       {
     205           0 :         break;
     206             :       }
     207           0 :     }
     208           0 :     output.push_back(transition);
     209             :   }
     210           0 :   return output;
     211             : }
     212             : 
     213           0 : bool simulation::is_prioritized(const multi_action &action)
     214             : {
     215           0 :   if (m_prioritized_action == "tau")
     216             :   {
     217           0 :     return action.actions().size() == 0;
     218             :   }
     219             :   else
     220             :   {
     221           0 :     return action.actions().size() == 1 && (std::string)action.actions().front().label().name() == m_prioritized_action;
     222             :   }
     223             : }
     224             : 
     225           0 : void simulation::prioritize_trace()
     226             : {
     227           0 :   m_prioritized_trace.push_back(m_full_trace.front());
     228           0 :   for (std::size_t index = 0; index < m_full_trace.size() - 1; index++)
     229             :   {
     230           0 :     transition_t transition = m_full_trace[index].transitions[m_full_trace[index].transition_number];
     231           0 :     if (is_prioritized(transition.action))
     232             :     {
     233           0 :       m_prioritized_trace.back().source_state = transition.destination;
     234             :     }
     235             :     else
     236             :     {
     237           0 :       m_prioritized_trace.push_back(m_full_trace[index + 1]);
     238           0 :       m_prioritized_originals.push_back(index);
     239             :     }
     240             :   }
     241           0 :   m_prioritized_originals.push_back(m_full_trace.size() - 1);
     242             : 
     243           0 :   for (std::deque<state_t>::iterator i = m_prioritized_trace.begin(); i != m_prioritized_trace.end(); i++)
     244             :   {
     245           0 :     i->transitions = prioritize(transitions(i->source_state));
     246             :   }
     247           0 : }
     248             : 
     249           0 : void simulation::push_back(const lps::state& lps_state)
     250             : {
     251           0 :   state_t state;
     252           0 :   state.source_state = lps_state;
     253           0 :   state.transitions = transitions(lps_state);
     254           0 :   state.transition_number = 0;
     255           0 :   m_full_trace.push_back(state);
     256           0 : }
     257             : 
     258           0 : bool simulation::match_trace(trace::Trace& trace)
     259             : {
     260           0 :   state_t& current = m_full_trace.back();
     261           0 :   lps::multi_action action = trace.currentAction();
     262           0 :   trace.increasePosition();
     263           0 :   for (std::size_t i = 0; i < current.transitions.size(); ++i)
     264             :   {
     265           0 :     if (current.transitions[i].action == action &&
     266           0 :         (!trace.current_state_exists() ||
     267           0 :          current.transitions[i].destination == trace.currentState()))
     268             :     {
     269           0 :       current.transition_number = i;
     270           0 :       push_back(trace.currentState());
     271           0 :       if (trace.getPosition() == trace.number_of_actions() || match_trace(trace))
     272             :       {
     273           0 :         return true;
     274             :       }
     275           0 :       m_full_trace.pop_back();
     276             :     }
     277             :   }
     278           0 :   return false;
     279             : }
     280             : 
     281           0 : bool simulation::match(const state &left, const state &right)
     282             : {
     283           0 :   assert(left.size() == right.size());
     284           0 :   for (std::size_t i = 0; i < left.size(); i++)
     285             :   {
     286           0 :     if (!is_variable(left[i]) && !is_variable(right[i]) && left[i] != right[i])
     287             :     {
     288           0 :       return false;
     289             :     }
     290             :   }
     291           0 :   return true;
     292         261 : }

Generated by: LCOV version 1.13