mcrl2::lps::simulation

Include file:

#include "mcrl2/lps/simulation.h
class mcrl2::lps::simulation

Simulation process.

Protected attributes

std::deque<state_t> m_full_trace
next_state_generator m_generator
std::string m_prioritized_action
std::deque<std::size_t> m_prioritized_originals
std::deque<state_t> m_prioritized_trace
data::rewriter m_rewriter
stochastic_specification m_specification
next_state_generator::substitution_t m_substitution
bool m_tau_prioritization

Public member functions

void enable_tau_prioritization(bool enable, const std::string &action = "ctau")

If enabled, tau prioritization is applied to all outgoing transitions, and in-between states are hidden from the state vector.

void load(const std::string &filename)

Load a trace from a file.

void save(const std::string &filename)

Save the trace to a file.

void select(std::size_t transition_number)

Choose outgoing transition transition_number and add its state to the state vector.

simulation(const stochastic_specification &specification, data::rewrite_strategy strategy = data::rewrite_strategy())

Constructor.

const std::deque<state_t> &trace() const

Returns the current annotated state vector.

void truncate(std::size_t state_number)

Remove states from the end of the simulation, making state_number the last state.

Protected member functions

bool is_prioritized(const multi_action &action)
bool match(const state &left, const state &right)
bool match_trace(trace::Trace &trace)
std::vector<simulation::transition_t> prioritize(const std::vector<transition_t> &transitions)
void prioritize_trace()
void push_back(const lps::state &lps_state)
std::vector<simulation::transition_t> transitions(const lps::state &source_state)