mCRL2
Loading...
Searching...
No Matches
mcrl2::lts Namespace Reference

The main LTS namespace. More...

Namespaces

namespace  detail
 A base class for the lts_dot labelled transition system.
 

Classes

class  action_label_lts
 A class containing the values for action labels for the .lts format. More...
 
class  action_label_string
 This class contains strings to be used as values for action labels in lts's. More...
 
struct  fsm_writer
 
class  lts
 A class that contains a labelled transition system. More...
 
class  lts_aut_builder
 
class  lts_aut_disk_builder
 
class  lts_aut_t
 A simple labelled transition format with only strings as action labels. More...
 
struct  lts_builder
 
class  lts_default_base
 
class  lts_dot_builder
 
class  lts_dot_t
 A class to contain labelled transition systems in graphviz format. More...
 
class  lts_fsm_builder
 
class  lts_fsm_t
 The class lts_fsm_t contains labelled transition systems in .fsm format. More...
 
class  lts_lts_builder
 
class  lts_lts_disk_builder
 
class  lts_lts_t
 This class contains labelled transition systems in .lts format. More...
 
class  lts_none_builder
 
class  probabilistic_lts
 A class that contains a labelled transition system. More...
 
class  probabilistic_lts_aut_t
 A simple labelled transition format with only strings as action labels. More...
 
class  probabilistic_lts_dot_t
 A class to contain labelled transition systems in graphviz format. More...
 
class  probabilistic_lts_fsm_t
 The class lts_fsm_t contains labelled transition systems in .fsm format. More...
 
class  probabilistic_lts_lts_t
 This class contains probabilistic labelled transition systems in .lts format. More...
 
class  probabilistic_state
 A class that contains a probabilistic state. More...
 
struct  refinement_statistics
 
class  signature
 Base class for signature computation. More...
 
class  signature_bisim
 Class for computing the signature for strong bisimulation. More...
 
class  signature_branching_bisim
 Class for computing the signature for branching bisimulation. More...
 
class  signature_divergence_preserving_branching_bisim
 Class for computing the signature for divergence preserving branching bisimulation. More...
 
class  sigref
 Signature based reductions for labelled transition systems. More...
 
class  state_label_dot
 This class contains labels for states in dot format. More...
 
class  state_label_empty
 Contains empty state values, used for lts's without state valued. More...
 
class  state_label_fsm
 This class contains state labels for the fsm format. More...
 
class  state_label_lts
 This class contains state labels for an labelled transition system in .lts format. More...
 
struct  state_space_generator
 
class  stochastic_lts_aut_builder
 
struct  stochastic_lts_builder
 
class  stochastic_lts_fsm_builder
 
class  stochastic_lts_lts_builder
 
class  stochastic_lts_none_builder
 
class  trace
 This class contains a trace consisting of a sequence of (timed) actions possibly with intermediate states. More...
 
class  transition
 A class containing triples, source label and target representing transitions. More...
 
class  tree_set_store
 

Typedefs

typedef std::pair< transition::size_type, transition::size_typeoutgoing_pair_t
 Type for exploring transitions per state.
 
typedef detail::indexed_sorted_vector_for_transitions< outgoing_pair_toutgoing_transitions_per_state_t
 
typedef std::multimap< std::pair< transition::size_type, transition::size_type >, transition::size_typeoutgoing_transitions_per_state_action_t
 Type for exploring transitions per state and action.
 
typedef std::set< std::pair< std::size_t, std::size_t > > signature_t
 A signature is a pair of an action label and a block.
 

Enumerations

enum class  refinement_type { trace , failures , failures_divergence }
 
enum  lts_equivalence {
  lts_eq_none , lts_eq_bisim , lts_eq_bisim_gv , lts_eq_bisim_gjkw ,
  lts_eq_bisim_sigref , lts_eq_branching_bisim , lts_eq_branching_bisim_gv , lts_eq_branching_bisim_gjkw ,
  lts_eq_branching_bisim_sigref , lts_eq_divergence_preserving_branching_bisim , lts_eq_divergence_preserving_branching_bisim_gv , lts_eq_divergence_preserving_branching_bisim_gjkw ,
  lts_eq_divergence_preserving_branching_bisim_sigref , lts_eq_weak_bisim , lts_eq_divergence_preserving_weak_bisim , lts_eq_sim ,
  lts_eq_ready_sim , lts_eq_trace , lts_eq_weak_trace , lts_eq_coupled_sim ,
  lts_red_tau_star , lts_red_determinisation
}
 LTS equivalence relations. More...
 
enum  data_file_type_t { none_e , data_e , lps_e , mcrl2_e }
 Type for data files that contain extra information for an lts in .aut or .fsm format. Typically this is a data_specification (data_e), a linear process (lps_e) or an .mcrl2 file. The value none_e indicates that no information is available. More...
 
enum  lts_preorder {
  lts_pre_none , lts_pre_sim , lts_pre_ready_sim , lts_pre_trace ,
  lts_pre_weak_trace , lts_pre_trace_anti_chain , lts_pre_weak_trace_anti_chain , lts_pre_failures_refinement ,
  lts_pre_weak_failures_refinement , lts_pre_failures_divergence_refinement , lts_preorder_min = lts_pre_none , lts_preorder_max = lts_pre_failures_divergence_refinement
}
 LTS preorder relations. More...
 
enum  lts_probabilistic_equivalence { lts_probabilistic_eq_none , lts_probabilistic_bisim_bem , lts_probabilistic_bisim_grv }
 LTS equivalence relations. More...
 
enum  lts_probabilistic_preorder { lts_probabilistic_pre_none }
 LTS preorder relations. More...
 
enum  lts_type {
  lts_none , lts_lts , lts_aut , lts_fsm ,
  lts_dot , lts_lts_probabilistic , lts_aut_probabilistic , lts_fsm_probabilistic ,
  lts_type_min =lts_none , lts_type_max =lts_dot
}
 The enumerated type lts_type contains an index for every type type of labelled transition system that is supported by the system. More...
 
enum  transition_sort_style { src_lbl_tgt , lbl_tgt_src }
 Transition sort styles. More...
 

Functions

std::string pp (const action_label_string &l)
 
template<typename T >
void report_statistics (refinement_statistics< T > &stats)
 Print a message to debugging containing information about the given statistics.
 
template<typename LTS_TYPE >
std::pair< std::size_t, bool > reduce (LTS_TYPE &lts, const bool weak_reduction, const bool preserve_divergence, std::size_t l2_init)
 Preprocess the LTS for destructive refinement checking.
 
template<class LTS_TYPE , class COUNTER_EXAMPLE_CONSTRUCTOR = detail::dummy_counter_example_constructor>
bool destructive_refinement_checker (LTS_TYPE &l1, LTS_TYPE &l2, const refinement_type refinement, const bool weak_reduction, const lps::exploration_strategy strategy, const bool preprocess=true, COUNTER_EXAMPLE_CONSTRUCTOR generate_counter_example=detail::dummy_counter_example_constructor())
 This function checks using algorithms in the paper mentioned above whether transition system l1 is included in transition system l2, in the sense of trace inclusions, failures inclusion and divergence failures inclusion.
 
template<class LTS_TYPE >
void scc_reduce (LTS_TYPE &l, const bool preserve_divergence_loops=false)
 
lps::specification transform_lts2lps (const lts_lts_t &l)
 transform an lts in lts format into a linear process.
 
lps::specification transform_lts2lps (const lts_aut_t &l1, const data_specification &data, const process::action_label_list &action_labels, const variable_list &process_parameters)
 transform an lts in aut format into a linear process.
 
lps::specification transform_lts2lps (const lts_fsm_t &l1, const data_specification &data, const process::action_label_list &action_labels, const variable_list &process_parameters)
 transform an lts in fsm format into a linear process.
 
template<class LTS_TYPE >
void reduce (LTS_TYPE &l, lts_equivalence eq)
 Applies a reduction algorithm to this LTS.
 
template<class LTS_TYPE >
bool destructive_compare (LTS_TYPE &l1, LTS_TYPE &l2, const lts_equivalence eq, const bool generate_counter_examples=false, const std::string &counter_example_file=std::string(), const bool structured_output=false)
 Checks whether this LTS is equivalent to another LTS.
 
template<class LTS_TYPE >
bool compare (const LTS_TYPE &l1, const LTS_TYPE &l2, const lts_equivalence eq, const bool generate_counter_examples=false, const std::string &counter_example_file="", const bool structured_output=false)
 Checks whether this LTS is equivalent to another LTS.
 
template<class LTS_TYPE >
bool destructive_compare (LTS_TYPE &l1, LTS_TYPE &l2, const lts_preorder pre, const bool generate_counter_example, const std::string &counter_example_file="", const bool structured_output=false, const lps::exploration_strategy strategy=lps::es_breadth, const bool preprocess=true)
 Checks whether this LTS is smaller than another LTS according to a preorder.
 
template<class LTS_TYPE >
bool compare (const LTS_TYPE &l1, const LTS_TYPE &l2, const lts_preorder pre, const bool generate_counter_example, const std::string &counter_example_file="", const bool structured_output=false, const lps::exploration_strategy strategy=lps::es_breadth, const bool preprocess=true)
 Checks whether this LTS is smaller than another LTS according to a preorder.
 
template<class LTS_TYPE >
void determinise (LTS_TYPE &l)
 Determinises this LTS.
 
template<class SL , class AL , class BASE >
bool reachability_check (lts< SL, AL, BASE > &l, bool remove_unreachable=false)
 Checks whether all states in this LTS are reachable from the initial state and remove unreachable states if required.
 
template<class SL , class AL , class PROBABILISTIC_STATE , class BASE >
bool reachability_check (probabilistic_lts< SL, AL, PROBABILISTIC_STATE, BASE > &l, bool remove_unreachable=false)
 Checks whether all states in a probabilistic LTS are reachable from the initial state and remove unreachable states if required.
 
template<class LTS_TYPE >
bool is_deterministic (const LTS_TYPE &l)
 Checks whether this LTS is deterministic.
 
template<class LTS_TYPE >
void merge (LTS_TYPE &l1, const LTS_TYPE &l2)
 Merge the second lts into the first lts.
 
lps::state remove_time_stamp (const lps::state &s)
 Removes the last element from state s.
 
std::unique_ptr< lts_buildercreate_lts_builder (const lps::specification &lpsspec, const lps::explorer_options &options, lts_type output_format, const std::string &output_filename="")
 
std::string pp (const state_label_dot &l)
 Pretty print function for a state_label_dot. Only prints the label field.
 
lts_equivalence parse_equivalence (std::string const &s)
 Determines the equivalence from a string.
 
std::istream & operator>> (std::istream &is, lts_equivalence &eq)
 
std::string print_equivalence (const lts_equivalence eq)
 Gives the short name of an equivalence.
 
std::ostream & operator<< (std::ostream &os, const lts_equivalence eq)
 
std::string description (const lts_equivalence eq)
 Gives a description of an equivalence.
 
std::string pp (const state_label_fsm &label)
 Pretty print an fsm state label.
 
template<class LTS_TYPE >
void load_lts (LTS_TYPE &result, const std::string &infilename, lts_type type, const data_file_type_t extra_data_file_type=none_e, const std::string &extra_data_file_name="")
 Loads an lts of the indicated type, transforms it to an lts of the form lts_lts_t using the additional data parameters.
 
void load_lts_as_fsm_file (const std::string &path, lts_fsm_t &l)
 Read a labelled transition system and return it in fsm format.
 
atermpp::aterm_istreamoperator>> (atermpp::aterm_istream &stream, lts_lts_t &lts)
 Read a (probabilistic) LTS from the given stream.
 
atermpp::aterm_istreamoperator>> (atermpp::aterm_istream &stream, probabilistic_lts_lts_t &lts)
 
atermpp::aterm_ostreamoperator<< (atermpp::aterm_ostream &stream, const lts_lts_t &lts)
 Write a (probabilistic) LTS to the given stream at once.
 
atermpp::aterm_ostreamoperator<< (atermpp::aterm_ostream &stream, const probabilistic_lts_lts_t &lts)
 
void write_lts_header (atermpp::aterm_ostream &stream, const data::data_specification &data, const data::variable_list &parameters, const process::action_label_list &action_labels)
 Writes the start of an LTS stream.
 
void write_transition (atermpp::aterm_ostream &stream, std::size_t from, const lps::multi_action &label, std::size_t to)
 Write a transition to the LTS stream.
 
void write_transition (atermpp::aterm_ostream &stream, std::size_t from, const lps::multi_action &label, const probabilistic_lts_lts_t::probabilistic_state_t &to)
 
void write_state_label (atermpp::aterm_ostream &stream, const state_label_lts &label)
 Write a state label to the LTS stream.
 
void write_initial_state (atermpp::aterm_ostream &stream, std::size_t index)
 Write the initial state to the LTS stream.
 
std::string pp (const state_label_lts &label)
 Pretty print a state value of this LTS.
 
std::string pp (const action_label_lts &l)
 Print the action label to string.
 
action_label_lts parse_lts_action (const std::string &multi_action_string, const data::data_specification &data_spec, lps::multi_action_type_checker &typechecker)
 Parse a string into an action label.
 
lts_preorder parse_preorder (std::string const &s)
 Determines the preorder from a string.
 
std::istream & operator>> (std::istream &is, lts_preorder &eq)
 
std::string print_preorder (const lts_preorder pre)
 Gives the short name of a preorder.
 
std::ostream & operator<< (std::ostream &os, const lts_preorder pre)
 
std::string description (const lts_preorder pre)
 Gives a description of a preorder.
 
lts_probabilistic_equivalence parse_probabilistic_equivalence (const std::string &s)
 Determines the equivalence from a string.
 
std::istream & operator>> (std::istream &is, lts_probabilistic_equivalence &eq)
 
std::string print_probabilistic_equivalence (const lts_probabilistic_equivalence &eq)
 Gives the short name of an equivalence.
 
std::ostream & operator<< (std::ostream &os, const lts_probabilistic_equivalence &eq)
 
std::string description (const lts_probabilistic_equivalence &eq)
 Gives a description of an equivalence.
 
lts_probabilistic_preorder parse_probabilistic_preorder (std::string const &s)
 Determines the probabilistic preorder from a string.
 
std::istream & operator>> (std::istream &is, lts_probabilistic_preorder &eq)
 
std::string print_probabilistic_preorder (const lts_probabilistic_preorder &pre)
 Gives the short name of an preorder.
 
std::ostream & operator<< (std::ostream &os, const lts_probabilistic_preorder &pre)
 
std::string description (const lts_probabilistic_preorder &pre)
 Gives a description of an preorder.
 
void 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.
 
void sort_transitions (std::vector< transition > &transitions, transition_sort_style ts=src_lbl_tgt)
 Sorts the transitions using a sort style.
 
std::size_t label (const outgoing_pair_t &p)
 Label of a pair of a label and target state.
 
std::size_t to (const outgoing_pair_t &p)
 Target state of a label state pair.
 
std::size_t 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 label (const outgoing_transitions_per_state_action_t::const_iterator &i)
 Label of an iterator exploring transitions per outgoing state and action.
 
std::size_t 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 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 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 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 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.
 
void parse_fsm_specification (std::istream &from, probabilistic_lts_fsm_t &result)
 
void parse_fsm_specification (const std::string &text, probabilistic_lts_fsm_t &result)
 
template<class STATE , class PROBABILITY >
std::string pp (const probabilistic_state< STATE, PROBABILITY > &l)
 
template<class STATE , class PROBABILITY >
std::ostream & operator<< (std::ostream &out, const probabilistic_state< STATE, PROBABILITY > &l)
 Pretty print to an outstream.
 
std::string pp (const state_label_empty &)
 
std::ostream & operator<< (std::ostream &out, const lps::state &s)
 
const lps::statefirst_state (const lps::state &s)
 
const lps::statefirst_state (const lps::stochastic_state &s)
 
std::unique_ptr< stochastic_lts_buildercreate_stochastic_lts_builder (const lps::stochastic_specification &lpsspec, const lps::explorer_options &options, lts_type output_format)
 
atermpp::aterm_ostreamoperator<< (atermpp::aterm_ostream &stream, const probabilistic_lts_lts_t::probabilistic_state_t &state)
 Converts a probabilistic state into an aterm that encodes it.
 
atermpp::aterm_istreamoperator>> (atermpp::aterm_istream &stream, probabilistic_lts_lts_t::probabilistic_state_t &state)
 

Variables

static const std::size_t const_tau_label_index =0
 

Detailed Description

The main LTS namespace.

The namespace for traces.

This namespace contains all data structures and members of the LTS library.

The namespace trace contains all data structures and members of the trace library.

Typedef Documentation

◆ outgoing_pair_t

Type for exploring transitions per state.

Definition at line 171 of file lts_utilities.h.

◆ outgoing_transitions_per_state_action_t

Type for exploring transitions per state and action.

Definition at line 192 of file lts_utilities.h.

◆ outgoing_transitions_per_state_t

◆ signature_t

typedef std::set<std::pair<std::size_t, std::size_t> > mcrl2::lts::signature_t

A signature is a pair of an action label and a block.

Definition at line 25 of file sigref.h.

Enumeration Type Documentation

◆ data_file_type_t

Type for data files that contain extra information for an lts in .aut or .fsm format. Typically this is a data_specification (data_e), a linear process (lps_e) or an .mcrl2 file. The value none_e indicates that no information is available.

Enumerator
none_e 
data_e 
lps_e 
mcrl2_e 

Definition at line 33 of file lts_io.h.

◆ lts_equivalence

LTS equivalence relations.

This enumerated type defines equivalence relations on LTSs. They can be used to reduce an LTS or decide whether two LTSs are equivalent.

Enumerator
lts_eq_none 

Unknown or no equivalence

lts_eq_bisim 

Strong bisimulation equivalence using the O(m log n) algorithm [Jansen/Groote/Keiren/Wijs 2019]

lts_eq_bisim_gv 

Strong bisimulation equivalence using the O(mn) algorithm [Groote/Vaandrager 1990]

lts_eq_bisim_gjkw 

Strong bisimulation equivalence using the O(m log m) algorithm [Groote/Jansen/Keiren/Wijs 2017]

lts_eq_bisim_sigref 

Strong bisimulation equivalence using the signature refinement algorithm [Blom/Orzan 2003]

lts_eq_branching_bisim 

Branching bisimulation equivalence using the O(m log n) algorithm [Jansen/Groote/Keiren/Wijs 2019]

lts_eq_branching_bisim_gv 

Branching bisimulation equivalence using the O(mn) algorithm [Groote/Vaandrager 1990]

lts_eq_branching_bisim_gjkw 

Branching bisimulation equivalence using the O(m log m) algorithm [Groote/Jansen/Keiren/Wijs 2017

lts_eq_branching_bisim_sigref 

Branching bisimulation equivalence using the signature refinement algorithm [Blom/Orzan 2003]

lts_eq_divergence_preserving_branching_bisim 

Divergence-preserving branching bisimulation equivalence using the O(m log n) algorithm [Jansen/Groote/Keiren/Wijs 2019]

lts_eq_divergence_preserving_branching_bisim_gv 

Divergence-preserving branching bisimulation equivalence using the O(mn) algorithm [Groote/Vaandrager 1990]

lts_eq_divergence_preserving_branching_bisim_gjkw 

Divergence-preserving branching bisimulation equivalence using the O(m log m) algorithm [Groote/Jansen/Keiren/Wijs 2017]

lts_eq_divergence_preserving_branching_bisim_sigref 
lts_eq_weak_bisim 

Divergence-preserving branching bisimulation equivalence using the signature refinement algorithm [Blom/Orzan 2003] Weak bisimulation equivalence

lts_eq_divergence_preserving_weak_bisim 

Divergence-preserving weak bisimulation equivalence

lts_eq_sim 

Strong simulation equivalence

lts_eq_ready_sim 

Strong ready-simulation equivalence

lts_eq_trace 

Strong trace equivalence

lts_eq_weak_trace 

Weak trace equivalence

lts_eq_coupled_sim 
lts_red_tau_star 

Coupled Similarity TODO Tau star reduction

lts_red_determinisation 

Used for a determinisation reduction

Definition at line 31 of file lts_equivalence.h.

◆ lts_preorder

LTS preorder relations.

This enumerated type defines preorder relations on LTSs. They can be used to decide whether one LTS is behaviourally contained in another LTS.

Enumerator
lts_pre_none 

Unknown or no preorder

lts_pre_sim 

Strong simulation preorder

lts_pre_ready_sim 

Strong ready simulation preorder

lts_pre_trace 

Strong trace preorder

lts_pre_weak_trace 

Weak trace preorder

lts_pre_trace_anti_chain 

Trace preorder based on anti chains

lts_pre_weak_trace_anti_chain 

Weak trace preorder based on anti chains

lts_pre_failures_refinement 

Failures refinement based on anti chains

lts_pre_weak_failures_refinement 

Weak failures refinement based on anti chains

lts_pre_failures_divergence_refinement 

Failures divergence refinement based on anti chains, which is automatically weak

lts_preorder_min 
lts_preorder_max 

Definition at line 31 of file lts_preorder.h.

◆ lts_probabilistic_equivalence

LTS equivalence relations.

This enumerated type defines equivalence relations on LTSs. They can be used to reduce an LTS or decide whether two LTSs are equivalent.

Enumerator
lts_probabilistic_eq_none 

Unknown or no equivalence

lts_probabilistic_bisim_bem 

Probabilistic bisimulation equivalence using the O(mn (log n + log m)) algorithm [Bier]

lts_probabilistic_bisim_grv 

Probabilistic bisimulation equivalence using the O(m(log n)) algorithm by Groote, Rivera Verduzco and de Vink

Definition at line 31 of file lts_probabilistic_equivalence.h.

◆ lts_probabilistic_preorder

LTS preorder relations.

This enumerated type defines equivalence relations on LTSs. They can be used to reduce an LTS or decide whether two LTSs are equivalent.

Enumerator
lts_probabilistic_pre_none 

Unknown or no preorder

Definition at line 136 of file lts_probabilistic_equivalence.h.

◆ lts_type

The enumerated type lts_type contains an index for every type type of labelled transition system that is supported by the system.

Every type has an associated labelled transition format. E.g. for lts_lts the type of the lts is lts_lts_t. Similarly, lts_aut_t, etc. are available. Files in which the lts's are stored have the name file.lts, file.aut, etc.

Enumerator
lts_none 

unknown or no format

lts_lts 

mCRL2 SVC format

lts_aut 

Aldébaran format (CADP)

lts_fsm 

FSM format

lts_dot 

GraphViz format

lts_lts_probabilistic 
lts_aut_probabilistic 
lts_fsm_probabilistic 
lts_type_min 
lts_type_max 

Definition at line 36 of file lts_type.h.

◆ refinement_type

enum class mcrl2::lts::refinement_type
strong
Enumerator
trace 
failures 
failures_divergence 

Definition at line 191 of file liblts_failures_refinement.h.

◆ transition_sort_style

Transition sort styles.

This enumerated type defines sort styles for transitions. They can be used to sort the transitions of an LTS based on various criteria.

Enumerator
src_lbl_tgt 

Sort first on source state, then on label, then on target state

lbl_tgt_src 

Sort first on label, then on target state, then on source state

Definition at line 33 of file transition.h.

Function Documentation

◆ compare() [1/2]

template<class LTS_TYPE >
bool mcrl2::lts::compare ( const LTS_TYPE &  l1,
const LTS_TYPE &  l2,
const lts_equivalence  eq,
const bool  generate_counter_examples = false,
const std::string &  counter_example_file = "",
const bool  structured_output = false 
)

Checks whether this LTS is equivalent to another LTS.

The input labelled transition systems are duplicated in memory to carry out the comparison. When space efficiency is a concern, one can consider to use destructive_compare.

Parameters
[in]l1The first LTS to compare.
[in]l2The second LTS to compare.
[in]eqThe equivalence with respect to which the LTSs will be compared.
[in]generate_counter_examplesWhether to generate a counter example
[in]counter_example_fileThe file to store the counter example in
Return values
trueif the LTSs are found to be equivalent.
falseotherwise.

Definition at line 850 of file lts_algorithm.h.

◆ compare() [2/2]

template<class LTS_TYPE >
bool mcrl2::lts::compare ( const LTS_TYPE &  l1,
const LTS_TYPE &  l2,
const lts_preorder  pre,
const bool  generate_counter_example,
const std::string &  counter_example_file = "",
const bool  structured_output = false,
const lps::exploration_strategy  strategy = lps::es_breadth,
const bool  preprocess = true 
)

Checks whether this LTS is smaller than another LTS according to a preorder.

Parameters
[in]l1The first LTS to be compared.
[in]l2The second LTS to be compared.
[in]preThe preorder with respect to which the LTSs will be compared.
[in]generate_counter_examplesWhether to generate a counter example
[in]counter_example_fileThe file to store the counter example in
[in]strategyChoose breadth-first or depth-first for exploration strategy of the antichain algorithms.
[in]preprocessWhether to allow preprocessing of the given LTSs.
Return values
trueif this LTS is smaller than LTS l according to preorder pre.
falseotherwise.

Definition at line 865 of file lts_algorithm.h.

◆ create_lts_builder()

std::unique_ptr< lts_builder > mcrl2::lts::create_lts_builder ( const lps::specification lpsspec,
const lps::explorer_options options,
lts_type  output_format,
const std::string &  output_filename = "" 
)
inline

Definition at line 332 of file lts_builder.h.

◆ create_stochastic_lts_builder()

std::unique_ptr< stochastic_lts_builder > mcrl2::lts::create_stochastic_lts_builder ( const lps::stochastic_specification lpsspec,
const lps::explorer_options options,
lts_type  output_format 
)
inline

Definition at line 308 of file stochastic_lts_builder.h.

◆ description() [1/4]

std::string mcrl2::lts::description ( const lts_equivalence  eq)
inline

Gives a description of an equivalence.

Parameters
[in]eqThe equivalence type.
Returns
A string describing the equivalence specified by eq.

Definition at line 311 of file lts_equivalence.h.

◆ description() [2/4]

std::string mcrl2::lts::description ( const lts_preorder  pre)
inline

Gives a description of a preorder.

Parameters
[in]preThe preorder type.
Returns
A string describing the preorder specified by eq.

Definition at line 169 of file lts_preorder.h.

◆ description() [3/4]

std::string mcrl2::lts::description ( const lts_probabilistic_equivalence eq)
inline

Gives a description of an equivalence.

Parameters
[in]eqThe equivalence type.
Returns
A string describing the equivalence specified by eq.

Definition at line 116 of file lts_probabilistic_equivalence.h.

◆ description() [4/4]

std::string mcrl2::lts::description ( const lts_probabilistic_preorder pre)
inline

Gives a description of an preorder.

Parameters
[in]preThe preorder type.
Returns
A string describing the preorder specified by pre.

Definition at line 206 of file lts_probabilistic_equivalence.h.

◆ destructive_compare() [1/2]

template<class LTS_TYPE >
bool mcrl2::lts::destructive_compare ( LTS_TYPE &  l1,
LTS_TYPE &  l2,
const lts_equivalence  eq,
const bool  generate_counter_examples = false,
const std::string &  counter_example_file = std::string(),
const bool  structured_output = false 
)

Checks whether this LTS is equivalent to another LTS.

Parameters
[in]l1The first LTS that will be compared.
[in]l2The second LTS that will be compared.
[in]eqThe equivalence with respect to which the LTSs will be compared.
[in]generate_counter_examplesWhether to generate a counter example
[in]counter_example_fileThe file to store the counter example in
Return values
trueif the LTSs are found to be equivalent.
falseotherwise.
Warning
This function alters the internal data structure of both LTSs for efficiency reasons. After comparison, this LTS is equivalent to the original LTS by equivalence eq, and similarly for the LTS l.

Definition at line 69 of file lts_algorithm.h.

◆ destructive_compare() [2/2]

template<class LTS_TYPE >
bool mcrl2::lts::destructive_compare ( LTS_TYPE &  l1,
LTS_TYPE &  l2,
const lts_preorder  pre,
const bool  generate_counter_example,
const std::string &  counter_example_file = "",
const bool  structured_output = false,
const lps::exploration_strategy  strategy = lps::es_breadth,
const bool  preprocess = true 
)

Checks whether this LTS is smaller than another LTS according to a preorder.

Parameters
[in]l1The first LTS to be compared.
[in]l2The second LTS to be compared.
[in]preThe preorder with respect to which the LTSs will be compared.
[in]generate_counter_examplesWhether to generate a counter example
[in]counter_example_fileThe file to store the counter example in
[in]strategyChoose breadth-first or depth-first for exploration strategy of the antichain algorithms.
[in]preprocessWhether to allow preprocessing of the given LTSs.
Return values
trueif LTS l1 is smaller than LTS l2 according to preorder pre.
falseotherwise.
Warning
This function alters the internal data structure of both LTSs for efficiency reasons. After comparison, this LTS is equivalent to the original LTS by equivalence eq, and similarly for the LTS l, where eq is the equivalence induced by the preorder pre (i.e. $eq = pre \cap
pre^{-1}$).

Definition at line 873 of file lts_algorithm.h.

◆ destructive_refinement_checker()

template<class LTS_TYPE , class COUNTER_EXAMPLE_CONSTRUCTOR = detail::dummy_counter_example_constructor>
bool mcrl2::lts::destructive_refinement_checker ( LTS_TYPE &  l1,
LTS_TYPE &  l2,
const refinement_type  refinement,
const bool  weak_reduction,
const lps::exploration_strategy  strategy,
const bool  preprocess = true,
COUNTER_EXAMPLE_CONSTRUCTOR  generate_counter_example = detail::dummy_counter_example_constructor() 
)

This function checks using algorithms in the paper mentioned above whether transition system l1 is included in transition system l2, in the sense of trace inclusions, failures inclusion and divergence failures inclusion.

Parameters
weak_reductionRemove inert tau loops.
strategyChoose between breadth and depth first.
preprocessUses (divergence preserving) branching bisimulation and tau scc reduction to reduce the input LTSs.
generate_counter_exampleIf set, a labelled transition system is generated that can act as a counterexample. It consists of a trace, followed by outgoing transitions representing a refusal set.

Definition at line 260 of file liblts_failures_refinement.h.

◆ determinise()

template<class LTS_TYPE >
void mcrl2::lts::determinise ( LTS_TYPE &  l)

Determinises this LTS.

Definition at line 1067 of file lts_algorithm.h.

◆ first_state() [1/2]

const lps::state & mcrl2::lts::first_state ( const lps::state s)
inline

Definition at line 28 of file state_space_generator.h.

◆ first_state() [2/2]

const lps::state & mcrl2::lts::first_state ( const lps::stochastic_state s)
inline

Definition at line 34 of file state_space_generator.h.

◆ from()

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

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

Definition at line 195 of file lts_utilities.h.

◆ is_deterministic()

template<class LTS_TYPE >
bool mcrl2::lts::is_deterministic ( const LTS_TYPE &  l)

Checks whether this LTS is deterministic.

Return values
trueif this LTS is deterministic;
falseotherwise.

Definition at line 1000 of file lts_algorithm.h.

◆ label() [1/2]

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

Label of a pair of a label and target state.

Definition at line 176 of file lts_utilities.h.

◆ label() [2/2]

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

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

Definition at line 201 of file lts_utilities.h.

◆ load_lts()

template<class LTS_TYPE >
void mcrl2::lts::load_lts ( LTS_TYPE &  result,
const std::string &  infilename,
lts_type  type,
const data_file_type_t  extra_data_file_type = none_e,
const std::string &  extra_data_file_name = "" 
)
inline

Loads an lts of the indicated type, transforms it to an lts of the form lts_lts_t using the additional data parameters.

The file can refer to any file in lts, aut, fsm, or dot format. After reading it is is translated into .lts format. For this a file is read with the name extra_data_file, which is interpreted as a data specification if extra_data_file_type has type data_e, a linear process specification if it has value lps_e, and an mcrl2 file if it has value mcrl2_e.

Parameters
[out]resultThe lts in which the transition system is put.
[in]infilenameThe name of the file containing the lts.
[in]typeThe type of the lts file, i.e. .lts, .fsm, .dot or .aut.
[in]extra_data_file_typeThe type of the file containing extra information, such as a data specification.
[in]extra_data_file_nameThe name of the file containing extra information.

Definition at line 202 of file lts_io.h.

◆ load_lts_as_fsm_file()

void mcrl2::lts::load_lts_as_fsm_file ( const std::string &  path,
lts_fsm_t l 
)
inline

Read a labelled transition system and return it in fsm format.

The file can refer to any file in lts, aut, fsm, or dot format. After reading it is is attempted to translate it into fsm format.

Parameters
[in]pathA string with the name of the file.
[out]lThe lts in which the transition system is put.

Definition at line 253 of file lts_io.h.

◆ merge()

template<class LTS_TYPE >
void mcrl2::lts::merge ( LTS_TYPE &  l1,
const LTS_TYPE &  l2 
)

Merge the second lts into the first lts.

Parameters
[in,out]l1The transition system in which l2 is merged.
[in]l2The second transition system, which remains unchanged

Definition at line 617 of file lts_algorithm.h.

◆ operator<<() [1/9]

atermpp::aterm_ostream & mcrl2::lts::operator<< ( atermpp::aterm_ostream stream,
const lts_lts_t lts 
)

Write a (probabilistic) LTS to the given stream at once.

Definition at line 439 of file liblts_lts.cpp.

◆ operator<<() [2/9]

atermpp::aterm_ostream & mcrl2::lts::operator<< ( atermpp::aterm_ostream stream,
const probabilistic_lts_lts_t lts 
)

Definition at line 445 of file liblts_lts.cpp.

◆ operator<<() [3/9]

atermpp::aterm_ostream & mcrl2::lts::operator<< ( atermpp::aterm_ostream stream,
const probabilistic_lts_lts_t::probabilistic_state_t state 
)

Converts a probabilistic state into an aterm that encodes it.

Definition at line 23 of file liblts_lts.cpp.

◆ operator<<() [4/9]

std::ostream & mcrl2::lts::operator<< ( std::ostream &  os,
const lts_equivalence  eq 
)
inline

Definition at line 301 of file lts_equivalence.h.

◆ operator<<() [5/9]

std::ostream & mcrl2::lts::operator<< ( std::ostream &  os,
const lts_preorder  pre 
)
inline

Definition at line 158 of file lts_preorder.h.

◆ operator<<() [6/9]

std::ostream & mcrl2::lts::operator<< ( std::ostream &  os,
const lts_probabilistic_equivalence eq 
)
inline

Definition at line 106 of file lts_probabilistic_equivalence.h.

◆ operator<<() [7/9]

std::ostream & mcrl2::lts::operator<< ( std::ostream &  os,
const lts_probabilistic_preorder pre 
)
inline

Definition at line 196 of file lts_probabilistic_equivalence.h.

◆ operator<<() [8/9]

std::ostream & mcrl2::lts::operator<< ( std::ostream &  out,
const lps::state s 
)
inline

Definition at line 22 of file state_space_generator.h.

◆ operator<<() [9/9]

template<class STATE , class PROBABILITY >
std::ostream & mcrl2::lts::operator<< ( std::ostream &  out,
const probabilistic_state< STATE, PROBABILITY > &  l 
)
inline

Pretty print to an outstream.

Definition at line 356 of file probabilistic_state.h.

◆ operator>>() [1/7]

atermpp::aterm_istream & mcrl2::lts::operator>> ( atermpp::aterm_istream stream,
lts_lts_t lts 
)

Read a (probabilistic) LTS from the given stream.

Definition at line 427 of file liblts_lts.cpp.

◆ operator>>() [2/7]

atermpp::aterm_istream & mcrl2::lts::operator>> ( atermpp::aterm_istream stream,
probabilistic_lts_lts_t lts 
)

Definition at line 433 of file liblts_lts.cpp.

◆ operator>>() [3/7]

Definition at line 53 of file liblts_lts.cpp.

◆ operator>>() [4/7]

std::istream & mcrl2::lts::operator>> ( std::istream &  is,
lts_equivalence eq 
)
inline

Definition at line 214 of file lts_equivalence.h.

◆ operator>>() [5/7]

std::istream & mcrl2::lts::operator>> ( std::istream &  is,
lts_preorder eq 
)
inline

Definition at line 107 of file lts_preorder.h.

◆ operator>>() [6/7]

std::istream & mcrl2::lts::operator>> ( std::istream &  is,
lts_probabilistic_equivalence eq 
)
inline

Definition at line 69 of file lts_probabilistic_equivalence.h.

◆ operator>>() [7/7]

std::istream & mcrl2::lts::operator>> ( std::istream &  is,
lts_probabilistic_preorder eq 
)
inline

Definition at line 163 of file lts_probabilistic_equivalence.h.

◆ parse_equivalence()

lts_equivalence mcrl2::lts::parse_equivalence ( std::string const &  s)
inline

Determines the equivalence from a string.

The following strings may be used:

  • "none" for identity equivalence;
  • "bisim" for strong bisimilarity using the O(m log n) algorithm [Groote/Jansen/Keiren/Wijs 2017];
  • "bisim-gv" for strong bisimilarity using the O(mn) algorithm [Groote/Vaandrager 1990];
  • "bisim-sig" for strong bisimilarity using the signature refinement algorithm [Blom/Orzan 2003];
  • "branching-bisim" for branching bisimilarity using the O(m log n) algorithm [Groote/Jansen/Keiren/Wijs 2017];
  • "branching-bisim-gv" for branching bisimilarity using the O(mn) algorithm [Groote/Vaandrager 1990];
  • "branching-bisim-sig" for branching bisimilarity using the signature refinement algorithm [Blom/Orzan 2003];
  • "dpbranching-bisim" for divergence-preserving branching bisimilarity using the O(m log n) algorithm [Groote/Jansen/Keiren/Wijs 2017];
  • "dpbranching-bisim-gv" for divergence-preserving branching bisimilarity using the O(mn) algorithm [Groote/Vaandrager 1990];
  • "dpbranching-bisim-sig" for divergence-preserving branching bisimilarity using the signature refinement algorithm [Blom/Orzan 2003];
  • "weak-bisim" for weak bisimilarity;
  • "dpweak-bisim" for divergence-preserving weak bisimilarity;
  • "sim" for strong simulation equivalence;
  • "trace" for strong trace equivalence;
  • "weak-trace" for weak trace equivalence;
  • "determinisation" for a determinisation reduction.
Parameters
[in]sThe string specifying the equivalence.
Returns
The equivalence type specified by s. If s is none of the above values then lts_eq_none is returned.

Definition at line 98 of file lts_equivalence.h.

◆ parse_fsm_specification() [1/2]

void mcrl2::lts::parse_fsm_specification ( const std::string &  text,
probabilistic_lts_fsm_t result 
)
inline

Definition at line 176 of file parse.h.

◆ parse_fsm_specification() [2/2]

void mcrl2::lts::parse_fsm_specification ( std::istream &  from,
probabilistic_lts_fsm_t result 
)
inline

Definition at line 169 of file parse.h.

◆ parse_lts_action()

action_label_lts mcrl2::lts::parse_lts_action ( const std::string &  multi_action_string,
const data::data_specification data_spec,
lps::multi_action_type_checker typechecker 
)
inline

Parse a string into an action label.

The string is typechecked against the data specification and list of declared actions. If parsing or type checking fails, an mcrl2::runtime_error is thrown.

Parameters
[in]multi_action_stringThe string to be parsed.
[in]data_specThe data specification used for parsing.
[in]act_declsAction declarations.
Returns
The parsed and type checked multi action.

Definition at line 208 of file lts_lts.h.

◆ parse_preorder()

lts_preorder mcrl2::lts::parse_preorder ( std::string const &  s)
inline

Determines the preorder from a string.

The following strings may be used:

  • "sim" for strong simulation preorder;
  • "trace" for strong trace preorder;
  • "weak-trace" for weak trace preorder.
Parameters
[in]sThe string specifying the preorder.
Returns
The preorder type specified by s. If s is none of the above values then lts_pre_none is returned.

Definition at line 57 of file lts_preorder.h.

◆ parse_probabilistic_equivalence()

lts_probabilistic_equivalence mcrl2::lts::parse_probabilistic_equivalence ( const std::string &  s)
inline

Determines the equivalence from a string.

The following strings may be used:

  • "none" for identity equivalence;
  • "pbisim" for Probabilistic bisimulation equivalence using the O(mn (log n + log m)) algorithm [Bier];
Parameters
[in]sThe string specifying the equivalence.
Returns
The equivalence type specified by s. If s is none of the above values then lts_probabilistic_eq_none is returned.

Definition at line 47 of file lts_probabilistic_equivalence.h.

◆ parse_probabilistic_preorder()

lts_probabilistic_preorder mcrl2::lts::parse_probabilistic_preorder ( std::string const &  s)
inline

Determines the probabilistic preorder from a string.

The following strings may be used:

  • "none" for identity preorder;
Parameters
[in]sThe string specifying the equivalence.
Returns
The equivalence type specified by s. If s is none of the above values then lts_probabilistic_pre_none is returned.

Definition at line 149 of file lts_probabilistic_equivalence.h.

◆ pp() [1/7]

std::string mcrl2::lts::pp ( const action_label_lts l)
inline

Print the action label to string.

Definition at line 195 of file lts_lts.h.

◆ pp() [2/7]

std::string mcrl2::lts::pp ( const action_label_string l)
inline

Definition at line 193 of file action_label_string.h.

◆ pp() [3/7]

template<class STATE , class PROBABILITY >
std::string mcrl2::lts::pp ( const probabilistic_state< STATE, PROBABILITY > &  l)
inline

Definition at line 323 of file probabilistic_state.h.

◆ pp() [4/7]

std::string mcrl2::lts::pp ( const state_label_dot l)
inline

Pretty print function for a state_label_dot. Only prints the label field.

Definition at line 101 of file lts_dot.h.

◆ pp() [5/7]

std::string mcrl2::lts::pp ( const state_label_empty )
inline

Definition at line 57 of file state_label_empty.h.

◆ pp() [6/7]

std::string mcrl2::lts::pp ( const state_label_fsm label)
inline

Pretty print an fsm state label.

Definition at line 71 of file lts_fsm.h.

◆ pp() [7/7]

std::string mcrl2::lts::pp ( const state_label_lts label)
inline

Pretty print a state value of this LTS.

The label is printed as (t1,...,tn) if it consists of a single label. Otherwise the labels are printed with square brackets surrounding it.

Parameters
[in]labelThe state value to pretty print.
Returns
The pretty-printed representation of value.

Definition at line 101 of file lts_lts.h.

◆ print_equivalence()

std::string mcrl2::lts::print_equivalence ( const lts_equivalence  eq)
inline

Gives the short name of an equivalence.

Parameters
[in]eqThe equivalence type.
Returns
A short string representing the equivalence specified by eq. The returned value is one of the strings listed for parse_equivalence.

Definition at line 234 of file lts_equivalence.h.

◆ print_preorder()

std::string mcrl2::lts::print_preorder ( const lts_preorder  pre)
inline

Gives the short name of a preorder.

Parameters
[in]preThe preorder type.
Returns
A short string representing the preorder specified by pre. The returned value is one of the strings listed for parse_preorder.

Definition at line 128 of file lts_preorder.h.

◆ print_probabilistic_equivalence()

std::string mcrl2::lts::print_probabilistic_equivalence ( const lts_probabilistic_equivalence eq)
inline

Gives the short name of an equivalence.

Parameters
[in]eqThe equivalence type.
Returns
A short string representing the equivalence specified by eq. The returned value is one of the strings listed for parse_equivalence.

Definition at line 89 of file lts_probabilistic_equivalence.h.

◆ print_probabilistic_preorder()

std::string mcrl2::lts::print_probabilistic_preorder ( const lts_probabilistic_preorder pre)
inline

Gives the short name of an preorder.

Parameters
[in]preThe preorder type.
Returns
A short string representing the preorder specified by pre. The returned value is one of the strings listed for parse_preorder.

Definition at line 183 of file lts_probabilistic_equivalence.h.

◆ reachability_check() [1/2]

template<class SL , class AL , class BASE >
bool mcrl2::lts::reachability_check ( lts< SL, AL, BASE > &  l,
bool  remove_unreachable = false 
)

Checks whether all states in this LTS are reachable from the initial state and remove unreachable states if required.

Runs in O(num_states * num_transitions) time.

Parameters
[in]lThe LTS on which reachability is checked.
[in]remove_unreachableIndicates whether all unreachable states should be removed from the LTS. This option does not influence the return value; the return value is with respect to the original LTS.
Return values
trueif all states are reachable from the initial state;
falseotherwise.

Definition at line 341 of file lts_algorithm.h.

◆ reachability_check() [2/2]

template<class SL , class AL , class PROBABILISTIC_STATE , class BASE >
bool mcrl2::lts::reachability_check ( probabilistic_lts< SL, AL, PROBABILISTIC_STATE, BASE > &  l,
bool  remove_unreachable = false 
)

Checks whether all states in a probabilistic LTS are reachable from the initial state and remove unreachable states if required.

Runs in O(num_states * num_transitions) time.

Parameters
[in]lThe LTS on which reachability is checked.
[in]remove_unreachableIndicates whether all unreachable states should be removed from the LTS. This option does not influence the return value; the return value is with respect to the original LTS.
Return values
trueif all states are reachable from the initial state;
falseotherwise.

Definition at line 450 of file lts_algorithm.h.

◆ reduce() [1/2]

template<class LTS_TYPE >
void mcrl2::lts::reduce ( LTS_TYPE &  l,
lts_equivalence  eq 
)

Applies a reduction algorithm to this LTS.

Parameters
[in]lA labelled transition system that must be reduced.
[in]eqThe equivalence with respect to which the LTS will be reduced.

Definition at line 629 of file lts_algorithm.h.

◆ reduce() [2/2]

template<typename LTS_TYPE >
std::pair< std::size_t, bool > mcrl2::lts::reduce ( LTS_TYPE &  lts,
const bool  weak_reduction,
const bool  preserve_divergence,
std::size_t  l2_init 
)

Preprocess the LTS for destructive refinement checking.

Parameters
ltsThe lts to preprocess.
initThe initial state of the right LTS that was merged.
Returns
A pair where the first element is the state number of init in the reduced lts and the second value indicate whether this state in equal to lts.initial_state.

Definition at line 226 of file liblts_failures_refinement.h.

◆ remove_time_stamp()

lps::state mcrl2::lts::remove_time_stamp ( const lps::state s)
inline

Removes the last element from state s.

Definition at line 25 of file lts_builder.h.

◆ report_statistics()

template<typename T >
void mcrl2::lts::report_statistics ( refinement_statistics< T > &  stats)

Print a message to debugging containing information about the given statistics.

Definition at line 211 of file liblts_failures_refinement.h.

◆ scc_reduce()

template<class LTS_TYPE >
void mcrl2::lts::scc_reduce ( LTS_TYPE &  l,
const bool  preserve_divergence_loops = false 
)

Definition at line 362 of file liblts_scc.h.

◆ sort_transitions() [1/2]

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 
)
inline

Sorts the transitions using a sort style.

Parameters
[in/out]transitions A vector of transitions to be sorted.
[in]hidden_label_setA set that tells which actions are to be interpreted as being hidden. Sorting takes place after mapping hidden actions to zero.
[in]tsThe sort style to use.

Definition at line 36 of file lts_utilities.h.

◆ sort_transitions() [2/2]

void mcrl2::lts::sort_transitions ( std::vector< transition > &  transitions,
transition_sort_style  ts = src_lbl_tgt 
)
inline

Sorts the transitions using a sort style.

Parameters
[in/out]transitions A vector of transitions to be sorted.
[in]tsThe sort style to use.

Definition at line 63 of file lts_utilities.h.

◆ to() [1/2]

std::size_t mcrl2::lts::to ( const outgoing_pair_t p)
inline

Target state of a label state pair.

Definition at line 182 of file lts_utilities.h.

◆ to() [2/2]

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

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

Definition at line 207 of file lts_utilities.h.

◆ transform_lts2lps() [1/3]

lps::specification mcrl2::lts::transform_lts2lps ( const lts_aut_t l1,
const data_specification data,
const process::action_label_list action_labels,
const variable_list process_parameters 
)

transform an lts in aut format into a linear process.

Parameters
l1A labelled transition system in aut format.
dataA separate data specification.
action_labelsA list containing the action labels used in the lts.
process_parametersThe process parameters of the current process.
Returns
The function returns a linear process with the same behaviour as the lts.

Definition at line 73 of file lts2lps.h.

◆ transform_lts2lps() [2/3]

lps::specification mcrl2::lts::transform_lts2lps ( const lts_fsm_t l1,
const data_specification data,
const process::action_label_list action_labels,
const variable_list process_parameters 
)

transform an lts in fsm format into a linear process.

Parameters
l1A labelled transition system in fsm format.
dataA separate data specification.
action_labelsA list containing the action labels used in the lts.
process_parametersThe process parameters of the current process. XXXXX Is this needed????
Returns
The function returns a linear process with the same behaviour as the lts.

Definition at line 90 of file lts2lps.h.

◆ transform_lts2lps() [3/3]

lps::specification mcrl2::lts::transform_lts2lps ( const lts_lts_t l)

transform an lts in lts format into a linear process.

Parameters
lA labelled transition system in lts format.
Returns
The function returns a linear process with the same behaviour as the lts.

Definition at line 32 of file lts2lps.h.

◆ transitions_per_outgoing_state_action_pair() [1/2]

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

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

Definition at line 213 of file lts_utilities.h.

◆ transitions_per_outgoing_state_action_pair() [2/2]

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 
)
inline

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

Definition at line 225 of file lts_utilities.h.

◆ transitions_per_outgoing_state_action_pair_reversed() [1/2]

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

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

Definition at line 239 of file lts_utilities.h.

◆ transitions_per_outgoing_state_action_pair_reversed() [2/2]

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 
)
inline

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

Definition at line 251 of file lts_utilities.h.

◆ write_initial_state()

void mcrl2::lts::write_initial_state ( atermpp::aterm_ostream stream,
std::size_t  index 
)

Write the initial state to the LTS stream.

Definition at line 496 of file liblts_lts.cpp.

◆ write_lts_header()

void mcrl2::lts::write_lts_header ( atermpp::aterm_ostream stream,
const data::data_specification data,
const data::variable_list parameters,
const process::action_label_list action_labels 
)

Writes the start of an LTS stream.

Definition at line 451 of file liblts_lts.cpp.

◆ write_state_label()

void mcrl2::lts::write_state_label ( atermpp::aterm_ostream stream,
const state_label_lts label 
)

Write a state label to the LTS stream.

Definition at line 490 of file liblts_lts.cpp.

◆ write_transition() [1/2]

void mcrl2::lts::write_transition ( atermpp::aterm_ostream stream,
std::size_t  from,
const lps::multi_action label,
const probabilistic_lts_lts_t::probabilistic_state_t to 
)

Definition at line 474 of file liblts_lts.cpp.

◆ write_transition() [2/2]

void mcrl2::lts::write_transition ( atermpp::aterm_ostream stream,
std::size_t  from,
const lps::multi_action label,
std::size_t  to 
)

Write a transition to the LTS stream.

Definition at line 466 of file liblts_lts.cpp.

Variable Documentation

◆ const_tau_label_index

const std::size_t mcrl2::lts::const_tau_label_index =0
static

Definition at line 27 of file transition.h.