9#ifndef MCRL2_LPS_SIMULATION_H
10#define MCRL2_LPS_SIMULATION_H
46 void truncate(std::size_t state_number,
bool probabilistic);
63 assert(state_index<
trace().size());
72 void save(
const std::string& filename)
const;
75 void load(
const std::string& filename);
85 std::uniform_int_distribution<std::size_t>
m_distrib;
Read-only balanced binary tree of terms.
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
std::deque< simulator_state_t > m_full_trace
void randomly_select_state()
Randomly choose one state among a sequence of probabilistic states.
bool m_auto_select_probabilistic_state
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.
const std::deque< simulator_state_t > & trace() const
Returns the current annotated state vector.
stochastic_specification m_specification
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.
Linear process specification.
Linear process specification.
This class contains a trace consisting of a sequence of (timed) actions possibly with intermediate st...
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...
std::vector< transition_t > transitions
std::size_t transition_number
lps::stochastic_state source_state
This class allows to flexibly manipulate traces.