mCRL2
Loading...
Searching...
No Matches
simulation.cpp
Go to the documentation of this file.
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>
12
13using namespace mcrl2;
14using namespace mcrl2::lps;
15
16std::vector<simulation::transition_t> simulation::transitions(const state& source_state)
17{
18 try
19 {
20 std::list<transition> outgoing_transitions = out_edges(source_state);
21 std::vector<simulation::transition_t> output(outgoing_transitions.begin(), outgoing_transitions.end());
22 return output;
23 }
24 catch (mcrl2::runtime_error& e)
25 {
26 mCRL2log(mcrl2::log::error) << "an error occurred while calculating the transitions from this state;\n" << e.what() << std::endl;
27 return std::vector<simulation::transition_t>();
28 }
29}
30
33 m_specification(specification),
34 m_gen(),
35 m_distrib(0,std::numeric_limits<std::size_t>::max())
36{
40 state.source_state = initial_state;
41 state.state_number=initial_state.size(); // This indicates that no state is selected yet.
42 m_full_trace.push_back(state);
43
45 {
46 randomly_select_state(); // There is only one state, or we select states at random. Select the state.
47 }
48}
49
50void simulation::truncate(std::size_t state_number, bool probabilistic)
51{
52 assert(state_number < m_full_trace.size());
53 m_full_trace.resize(state_number + 1);
54 if (probabilistic && m_full_trace[state_number].source_state.size()>1) // Indicate that this is a probabilistic state and forget about transitions.
55 {
56 m_full_trace[state_number].state_number=m_full_trace[state_number].source_state.size();
57 }
58
59}
60
61void simulation::select_state(std::size_t state_number)
62{
64
65 assert(state_number<state.source_state.states.size());
66 state.state_number=state_number;
67 state.transitions = transitions(state.source_state.states[state_number]);
68}
69
71{
73 std::size_t state_number=0;
74
75 if (state.source_state.states.size()>1)
76 {
77 // Generate a random size_t with random distribution.
78 double random_value=static_cast<double>(m_distrib(m_gen))/static_cast<double>(std::numeric_limits<std::size_t>::max());
79 random_value=random_value-data::sort_real::value<double>(state.source_state.probabilities[state_number]);
80 while (random_value>0)
81 {
82 state_number++;
83 assert(state_number<state.source_state.states.size());
84 random_value=random_value-data::sort_real::value<double>(state.source_state.probabilities[state_number]);
85 }
86 }
87 state.state_number=state_number;
88 state.transitions = transitions(state.source_state.states[state_number]);
89}
90
91void simulation::select_transition(std::size_t transition_number)
92{
93 assert(transition_number < m_full_trace.back().transitions.size());
94 m_full_trace.back().transition_number = transition_number;
96 state.source_state = m_full_trace.back().transitions[transition_number].state;
97 state.state_number=state.source_state.size();
98 m_full_trace.push_back(state);
99
100 if (state.source_state.size()==1 || m_auto_select_probabilistic_state)
101 {
103 }
104}
105
107{
108 std::size_t s=m_full_trace.back().transitions.size();
109 std::size_t transition_number= m_distrib(m_gen) % s;
110 select_transition(transition_number);
111}
112
114{
116}
117
118void simulation::save(const std::string& filename) const
119{
121 if (m_full_trace[0].state_number>=m_full_trace[0].source_state.size())
122 {
123 throw mcrl2::runtime_error("initial state is not set. Trace is not saved.");
124 }
125 trace.set_state(m_full_trace[0].source_state.states[m_full_trace[0].state_number]);
126 for (std::size_t i = 0; i + 1 < m_full_trace.size(); i++)
127 {
128 assert(m_full_trace[i].state_number<m_full_trace[i].source_state.size());
129 if (m_full_trace[i].transition_number<m_full_trace[i].transitions.size())
130 {
131 trace.add_action(m_full_trace[i].transitions[m_full_trace[i].transition_number].action);
132 if (m_full_trace[i+1].state_number<m_full_trace[i+1].source_state.size())
133 {
134 trace.set_state(m_full_trace[i+1].source_state.states[m_full_trace[i+1].state_number]);
135 }
136 else
137 {
138 trace.set_state(m_full_trace[i+1].source_state.states[0]);
139 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 trace.save(filename);
144}
145
146void simulation::load(const std::string& filename)
147{
148 // Load the trace from file
150 trace.reset_position();
151
152 // Get the first state from the generator
153 m_full_trace.clear();
154
157
159 // Check that the first state (if given) matches one of the probabilistic states of the specification.
160 if (trace.current_state_exists())
161 {
162 if (std::find(initial_state.states.begin(), initial_state.states.end(), trace.current_state()) == initial_state.states.end())
163 {
164 throw mcrl2::runtime_error("The initial state of the trace does not match the initial state "
165 "of this specification");
166 }
167
168
169 // Replay the trace using the generator.
171 {
172 throw mcrl2::runtime_error("Failed to perform action " + pp(trace.current_action()) + " at position "
173 + std::to_string(m_full_trace.size() - 1) + " from the trace loaded from " + filename + ".");
174 }
175 }
176}
177
178// Add a new state to m_full_trace with the indicated state.
180{
182 state.source_state = s;
183 state.state_number = s.size();
184 state.transition_number = 0;
185 m_full_trace.push_back(state);
186}
187
189{
190 if (!trace.current_state_exists())
191 {
192 return true;
193 }
194 assert(trace.current_state_exists());
195 simulator_state_t& current = m_full_trace.back();
196 for (std::size_t i = 0; i < current.source_state.size(); ++i)
197 {
198 if (current.source_state.states[i] == trace.current_state())
199 {
200 select_state(i);
202 {
203 return true;
204 }
205 }
206 }
207 return false;
208}
209
211{
212 if (!trace.current_action_exists())
213 {
214 return true;
215 }
216 simulator_state_t& current = m_full_trace.back();
217 lps::multi_action action = trace.current_action();
218 trace.increase_position();
219 for (std::size_t i = 0; i < current.transitions.size(); ++i)
220 {
221 if (current.transitions[i].action == action)
222 {
223 add_new_state(current.transitions[i].state);
224 current.transition_number = i;
226 {
227 return true;
228 }
229 m_full_trace.pop_back();
230 }
231 }
232 return false;
233}
234
Read-only balanced binary tree of terms.
size_type size() const
Returns the size of the term_balanced_tree.
size_type size() const
Returns the size of the term_list.
Definition aterm_list.h:256
const_iterator end() const
Returns a const_iterator pointing to the end of the term_list.
Definition aterm_list.h:282
const_iterator begin() const
Returns a const_iterator pointing to the beginning of the term_list.
Definition aterm_list.h:275
const data::data_expression_list & initial_state() const
Definition explorer.h:1022
void compute_stochastic_state(stochastic_state &result, const stochastic_distribution &distribution, const DataExpressionSequence &next_state, data::mutable_indexed_substitution<> &sigma, data::rewriter &rewr, data::enumerator_algorithm<> &enumerator) const
Definition explorer.h:559
typename std::conditional< Stochastic, stochastic_state, state >::type state_type
Definition explorer.h:450
std::list< transition > out_edges(const state &s, const SummandSequence &regular_summands, const SummandSequence &confluent_summands, data::mutable_indexed_substitution<> &sigma, data::rewriter &rewr, data::enumerator_algorithm<> &enumerator, data::enumerator_identifier_generator &id_generator)
Definition explorer.h:838
\brief A timed multi-action
void enable_auto_select_probability(bool enable)
If enabled, automatically a probabilistic state is chosen using its intrinsic probability.
void select_transition(std::size_t transition_number)
Choose outgoing transition indexed by transition_number and add its state to the state vector.
void add_new_state(const lps::stochastic_state &s)
std::uniform_int_distribution< std::size_t > m_distrib
Definition simulation.h:85
std::deque< simulator_state_t > m_full_trace
Definition simulation.h:88
void randomly_select_state()
Randomly choose one state among a sequence of probabilistic states.
bool m_auto_select_probabilistic_state
Definition simulation.h:83
void select_state(std::size_t state_number)
Choose one state among a sequence of probabilistic states.
simulation(const stochastic_specification &specification, data::rewrite_strategy strategy=data::rewrite_strategy())
Constructor.
void randomly_select_transition()
Randomly choose an outgoing transition and add its state to the state vector.
bool match_trace_transition(lts::trace &trace)
bool match_trace_probabilistic_state(lts::trace &trace)
void save(const std::string &filename) const
Save the trace to a file.
const std::deque< simulator_state_t > & trace() const
Returns the current annotated state vector.
Definition simulation.h:43
stochastic_specification m_specification
Definition simulation.h:81
void truncate(std::size_t state_number, bool probabilistic)
Remove states from the end of the simulation, making state_number the last state.
std::vector< transition_t > transitions(const lps::state &source_state)
void load(const std::string &filename)
Load a trace from a file.
const process::action_label_list & action_labels() const
Returns a sequence of action labels. This sequence contains all action labels occurring in the specif...
const data::data_specification & data() const
Returns the data specification.
Linear process specification.
This class contains a trace consisting of a sequence of (timed) actions possibly with intermediate st...
Definition trace.h:52
Standard exception class for reporting runtime errors.
Definition exception.h:27
#define mCRL2log(LEVEL)
mCRL2log(LEVEL) provides the stream used to log.
Definition logger.h:395
rewrite_strategy
The strategy of the rewriter.
The main namespace for the LPS library.
atermpp::term_balanced_tree< data::data_expression > state
Definition state.h:24
std::string pp(const action_summand &x)
Definition lps.cpp:26
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72
STL namespace.
Provides utilities for working with data expressions of standard sorts.
std::vector< transition_t > transitions
Definition simulation.h:35
std::vector< state > states