mCRL2
Loading...
Searching...
No Matches
simulation.h
Go to the documentation of this file.
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
15namespace mcrl2
16{
17
18namespace lps // TODO: This should become lts. We should not declare objects in namespace lps within the lts library.
19{
20
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.
24class simulation : protected explorer<true, false, stochastic_specification>
25{
26 public:
27
28 typedef transition transition_t;
29
31 {
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
41
43 const std::deque<simulator_state_t>& trace() const { return m_full_trace; }
44
46 void truncate(std::size_t state_number, bool probabilistic);
47
49 void select_state(std::size_t state_number);
50
53
55 void select_transition(std::size_t transition_number);
56
59
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
69 void enable_auto_select_probability(bool enable);
70
72 void save(const std::string& filename) const;
73
75 void load(const std::string& filename);
76
77 virtual ~simulation()
78 {}
79
80 protected:
82
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
96
97};
98
99} // namespace lps
100
101} // namespace mcrl2
102
103#endif
Read-only balanced binary tree of terms.
Simulation process.
Definition simulation.h:25
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.
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.
bool probabilistic_state_must_be_selected(const std::size_t state_index) const
Indicate whether a probabilistic state has been selected.
Definition simulation.h:61
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)
transition transition_t
Definition simulation.h:28
void load(const std::string &filename)
Load a trace from a file.
Linear process specification.
This class contains a trace consisting of a sequence of (timed) actions possibly with intermediate st...
Definition trace.h:52
add your file description here.
rewrite_strategy
The strategy of the rewriter.
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72
std::vector< transition_t > transitions
Definition simulation.h:35
This class allows to flexibly manipulate traces.