mcrl2/lts/lts_utilities.h

Include file:

#include "mcrl2/lts/lts_utilities.h"

This file contains some utility functions to manipulate lts’s.

The function in this file typically allow to present the transitions of a state space differently. Jan Friso Groote

Typedefs

type mcrl2::lts::outgoing_pair_t

typedef for std::pair< transition::size_type, transition::size_type >

Type for exploring transitions per state.

type mcrl2::lts::outgoing_transitions_per_state_action_t

typedef for std::multimap< std::pair< transition::size_type, transition::size_type >, transition::size_type >

Type for exploring transitions per state and action.

type mcrl2::lts::outgoing_transitions_per_state_t

typedef for detail::indexed_sorted_vector_for_transitions< outgoing_pair_t >

Functions

std::size_t mcrl2::lts::from(const outgoing_transitions_per_state_action_t::const_iterator &i)

From state of an iterator exploring transitions per outgoing state and action.

std::size_t mcrl2::lts::label(const outgoing_pair_t &p)

Label of a pair of a label and target state.

std::size_t mcrl2::lts::label(const outgoing_transitions_per_state_action_t::const_iterator &i)

Label of an iterator exploring transitions per outgoing state and action.

void mcrl2::lts::sort_transitions(std::vector<transition> &transitions, const std::set<transition::size_type> &hidden_label_set, transition_sort_style ts = src_lbl_tgt)

Sorts the transitions using a sort style.

Parameters:

  • [in/out] transitions A vector of transitions to be sorted.
  • hidden_label_set A set that tells which actions are to be interpreted as being hidden. Sorting takes place after mapping hidden actions to zero.
  • ts The sort style to use.
void mcrl2::lts::sort_transitions(std::vector<transition> &transitions, transition_sort_style ts = src_lbl_tgt)

Sorts the transitions using a sort style.

Parameters:

  • [in/out] transitions A vector of transitions to be sorted.
  • ts The sort style to use.
std::size_t mcrl2::lts::to(const outgoing_pair_t &p)

Target state of a label state pair.

std::size_t mcrl2::lts::to(const outgoing_transitions_per_state_action_t::const_iterator &i)

To state of an iterator exploring transitions per outgoing state and action.

outgoing_transitions_per_state_action_t mcrl2::lts::transitions_per_outgoing_state_action_pair(const std::vector<transition> &trans)

Provide the transitions as a multimap accessible per from state and label.

outgoing_transitions_per_state_action_t mcrl2::lts::transitions_per_outgoing_state_action_pair(const std::vector<transition> &trans, const std::set<transition::size_type> &hide_label_set)

Provide the transitions as a multimap accessible per from state and label.

outgoing_transitions_per_state_action_t mcrl2::lts::transitions_per_outgoing_state_action_pair_reversed(const std::vector<transition> &trans)

Provide the transitions as a multimap accessible per from state and label, ordered backwardly.

outgoing_transitions_per_state_action_t mcrl2::lts::transitions_per_outgoing_state_action_pair_reversed(const std::vector<transition> &trans, const std::set<transition::size_type> &hide_label_set)

Provide the transitions as a multimap accessible per from state and label, ordered backwardly.

Functions

LABEL_TYPE mcrl2::lts::detail::make_divergence_label(const std::string &s)
template<>
mcrl2::lts::action_label_lts mcrl2::lts::detail::make_divergence_label<mcrl2::lts::action_label_lts>(const std::string &s)
std::size_t mcrl2::lts::detail::mark_explicit_divergence_transitions(LTS_TYPE &l)
void mcrl2::lts::detail::unmark_explicit_divergence_transitions(LTS_TYPE &l, const std::size_t divergent_transition_label)