mcrl2/lts/lts_algorithm.h

Include file:

#include "mcrl2/lts/lts_algorithm.h"

Algorithms for LTS, such as equivalence reductions, determinisation, etc.

This contains the main algorithms useful to manipulate with labelled transition systems. Typically, it contains algorithms for bisimulation reduction, removal of tau loops, making an lts deterministic etc. Jan Friso Groote, Bas Ploeger, Muck van Weerdenburg

Functions

bool compare(const LTS_TYPE &l1, const LTS_TYPE &l2, const lts_equivalence eq, const bool generate_counter_examples = 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:

  • l1 The first LTS to compare.

  • l2 The second LTS to compare.

  • eq The equivalence with respect to which the LTSs will be compared.

  • generate_counter_examples If true counter examples are written to file.

Returns: * true if the LTSs are found to be equivalent.

  • false otherwise.

bool compare(const LTS_TYPE &l1, const LTS_TYPE &l2, const lts_preorder pre, const bool generate_counter_example, 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:

  • l1 The first LTS to be compared.

  • l2 The second LTS to be compared.

  • pre The preorder with respect to which the LTSs will be compared.

  • generate_counter_example Indicates whether a file containing a counter example is generated when the comparison fails.

  • strategy Choose breadth-first or depth-first for exploration strategy of the antichain algorithms.

  • preprocess Whether to allow preprocessing of the given LTSs.

Returns: * true if this LTS is smaller than LTS l according to preorder pre.

  • false otherwise.

bool mcrl2::lts::destructive_compare(LTS_TYPE &l1, LTS_TYPE &l2, const lts_equivalence eq, const bool generate_counter_examples = false)

Checks whether this LTS is equivalent to another LTS.

Parameters:

  • l1 The first LTS that will be compared.

  • l2 The second LTS that will be compared.

  • eq The equivalence with respect to which the LTSs will be compared.

  • generate_counter_examples

Returns: * true if the LTSs are found to be equivalent.

  • false otherwise.

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.

bool destructive_compare(LTS_TYPE &l1, LTS_TYPE &l2, const lts_preorder pre, const bool generate_counter_example, 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:

  • l1 The first LTS to be compared.

  • l2 The second LTS to be compared.

  • pre The preorder with respect to which the LTSs will be compared.

  • generate_counter_example Indicates whether a file containing a counter example is generated when the comparison fails.

  • strategy Choose breadth-first or depth-first for exploration strategy of the antichain algorithms.

  • preprocess Whether to allow preprocessing of the given LTSs.

Returns: * true if LTS l1 is smaller than LTS l2 according to preorder pre.

  • false otherwise.

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}$).

void determinise(LTS_TYPE &l)

Determinises this LTS.

bool is_deterministic(const LTS_TYPE &l)

Checks whether this LTS is deterministic.

Returns: * true if this LTS is deterministic;

  • false otherwise.

void mcrl2::lts::merge(LTS_TYPE &l1, const LTS_TYPE &l2)

Merge the second lts into the first lts.

Parameters:

  • l1 The transition system in which l2 is merged.

  • l2 The second transition system, which remains unchanged

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:

  • l The LTS on which reachability is checked.

  • remove_unreachable Indicates 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.

Returns: * true if all states are reachable from the initial state;

  • false otherwise.

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:

  • l The LTS on which reachability is checked.

  • remove_unreachable Indicates 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.

Returns: * true if all states are reachable from the initial state;

  • false otherwise.

void reduce(LTS_TYPE &l, lts_equivalence eq)

Applies a reduction algorithm to this LTS.

Parameters:

  • l A labelled transition system that must be reduced.

  • eq The equivalence with respect to which the LTS will be reduced.

Functions

void mcrl2::lts::detail::get_trans(const outgoing_transitions_per_state_t &begin, tree_set_store &tss, std::size_t d, std::vector<transition> &d_trans, LTS_TYPE &aut)