mcrl2::lps::simulation

Include file:

#include "mcrl2/lts/simulation.h

class mcrl2::lps::simulation

Simulation process.

Protected attributes

std::deque<state_t> mcrl2::lps::simulation::m_full_trace

next_state_generator mcrl2::lps::simulation::m_generator

std::string mcrl2::lps::simulation::m_prioritized_action

std::deque<std::size_t> mcrl2::lps::simulation::m_prioritized_originals

std::deque<state_t> mcrl2::lps::simulation::m_prioritized_trace

data::rewriter mcrl2::lps::simulation::m_rewriter

stochastic_specification mcrl2::lps::simulation::m_specification

next_state_generator::substitution_t mcrl2::lps::simulation::m_substitution

bool mcrl2::lps::simulation::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(lts::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)