mcrl2::lps::pins¶
Include file:
#include "mcrl2/lps/ltsmin.h
-
class
mcrl2::lps::pins¶
Public types¶
-
type
mcrl2::lps::pins::guard_evaluation_t¶ Values:
- GUARD_FALSE
- GUARD_TRUE
- GUARD_MAYBE
guard evaluations have ternary logic. A guard may not always rewrite to true or false
-
type
mcrl2::lps::pins::substitution_t¶ typedef for
data::rewriter::substitution_type
Protected attributes¶
-
std::vector<pins_data_type *>
mcrl2::lps::pins::m_data_types¶
-
lps::next_state_generator
mcrl2::lps::pins::m_generator¶
-
lps::next_state_generator
mcrl2::lps::pins::m_generator_reduced¶
-
utilities::indexed_set<atermpp::aterm>
mcrl2::lps::pins::m_guards¶
-
lps::specification
mcrl2::lps::pins::m_specification¶
-
lps::specification
mcrl2::lps::pins::m_specification_reduced¶
-
std::vector<pins_data_type *>
mcrl2::lps::pins::m_unique_data_types¶ The unique type mappings (is contained in m_data_types).
Protected member functions¶
-
pins_data_type &
action_label_type_map()¶ Returns the action data type.
-
const pins_data_type &
action_label_type_map() const¶ Returns the action data type.
-
const data::data_specification &
data() const Returns the data specification of the LPS specification.
-
void
initialize_read_write_groups()¶
-
std::string
print_vector(const Container &c) const¶
-
std::string
print_vector(Iter first, Iter last) const¶
-
const linear_process &
process() const¶ Returns the process of the LPS specification.
-
const linear_process &
process_reduced() const¶ Returns the reduced process of the LPS specification, i.e. with conditions with guards removed.
-
pins_data_type &
state_type_map(std::size_t i)¶ Returns the data type of the i-th state parameter.
-
const pins_data_type &
state_type_map(std::size_t i) const¶ Returns the data type of the i-th state parameter.
Public member functions¶
-
void
_long(ltsmin_state_type const &src, std::size_t group, StateFunction &f, const ltsmin_state_type &dest, int *const &labels, lps::next_state_generator *generator)¶ Iterates over the ‘next states’ of a particular summand of state src that are generated by a group of summands, and invokes a callback function for each discovered state.
StateFunction is a callback function that must provide the function operator() with the following interface:
void operator()(ltsmin_state_type const& next_state, int* const& edge_labels, int group);where- next_state is the target state of the transition
- edge_labels is an array of edge labels
- group is the number of the summand from which the next state was generated, or -1 if it is unknown which summand
Parameters:
- src An LTSMin state.
- group the number of the summand.
- f A state function.
- dest A destination state, which is modified and passed to the callback. Must provide space for at least process_parameter_count() items.
- labels An array of labels, which is modified and passed to the callback. Must provide space for at least edge_label_count() items.
- generator The next state generator to use.
-
pins_data_type &
data_type(std::size_t i)¶ Returns a reference to the datatype map with index i.
Pre: 0 <= i < datatype_count()
-
std::size_t
datatype_count() const¶ Returns the number of unique datatype maps. Note that the datatype map for action labels is included, so this number equals the number of different process parameter types + 1.
-
std::size_t
edge_label_count() const¶ Returns the number of labels per edge.
-
std::string
edge_label_name(std::size_t) const¶ Returns the name of the i-th action label (always “action”).
Pre: 0 <= i < edge_label_count()
-
datatype_index
edge_label_type(std::size_t) const¶ Returns the datatype map index corresponding to edge label i.
Pre: 0 <= i < edge_label_count()
-
guard_evaluation_t
eval_guard_long(ltsmin_state_type const &src, std::size_t guard)¶
-
void
get_initial_state(ltsmin_state_type &s)¶ Assigns the initial state to s.
-
std::size_t
group_count() const¶ Returns the number of available groups. This equals the number of action summands of the LPS.
-
std::size_t
guard_count() const¶
-
const std::vector<std::size_t> &
guard_info(std::size_t index) const¶
-
const std::string &
guard_name(std::size_t index)¶
-
const std::vector<std::size_t> &
guard_parameters(std::size_t index) const¶
-
std::string
info()¶ Prints an overview of several relevant attributes.
-
void
next_state_all(ltsmin_state_type const &src, StateFunction &f, ltsmin_state_type const &dest, int *const &labels)¶ Iterates over the ‘next states’ of state src, and invokes a callback function for each discovered state.
StateFunction is a callback function that must provide the function operator() with the following interface:
void operator()(ltsmin_state_type const& next_state, int* const& edge_labels, int group=-1);where- next_state is the target state of the transition
- edge_labels is an array of edge labels
- group is the number of the summand from which the next state was generated, or -1 if it is unknown which summand
Parameters:
- src An LTSMin state
- f A ‘callback’ function object
- dest A destination state, which is modified and passed to the callback. Must provide space for at least process_parameter_count() items.
- labels An array of labels, which is modified and passed to the callback. Must provide space for at least edge_label_count() items.
-
void
next_state_long(ltsmin_state_type const &src, std::size_t group, StateFunction &f, ltsmin_state_type const &dest, int *const &labels)¶
-
pins(const std::string &filename, const std::string &rewriter_strategy)¶ Constructor.
Parameters:
- filename The name of a file containing an mCRL2 specification
- rewriter_strategy The rewriter strategy used for generating next states
-
std::size_t
process_parameter_count() const¶ Returns the number of process parameters of the LPS.
-
std::string
process_parameter_name(std::size_t i) const¶ Returns a human-readable, unique name for process parameter i.
-
datatype_index
process_parameter_type(std::size_t i) const¶ Returns the datatype map index corresponding to process parameter i.
Pre: 0 <= i < process_parameter_count()
-
const std::vector<std::size_t> &
read_group(std::size_t index) const¶ Indices of process parameters that influence event or next state of a summand by being read.
Parameters:
- index the selected summand
Returns: reference to a vector of indices of parameters
Pre: 0 <= i < group_count()
-
lps::specification
reduce_specification(const lps::specification &spec)¶ extracts all guards from the original specification and returns a new one with the guards removed.
-
std::set<std::string>
summand_action_names(std::size_t i) const¶ Returns the names of the actions that appear in the summand with index i, with 0 <= i < group_count().
-
const std::vector<std::size_t> &
update_group(std::size_t index) const¶ Indices of process parameters that influence event or next state of a summand by being read except from the guards.
Parameters:
- index the selected summand
Returns: reference to a vector of indices of parameters
Pre: 0 <= i < group_count()
-
void
update_long(ltsmin_state_type const &src, std::size_t group, StateFunction &f, ltsmin_state_type const &dest, int *const &labels)¶
-
const std::vector<std::size_t> &
write_group(std::size_t index) const¶ Indices of process parameters that influence event or next state of a summand by being written.
Parameters:
- index the selected summand
Returns: reference to a vector of indices of parameters
Pre: 0 <= i < group_count()
-
~pins()¶
