File closed-set.hh

namespace mata

Main namespace including structs and algorithms for all automata.

In particular, this includes:

1. Alphabets,

2. Formula graphs and nodes,

3. Mintermization,

4. Closed sets.

Typedefs

template<typename T>
using OrdVec = mata::utils::OrdVector<T>

Enums

enum class ClosedSetType

Values:

enumerator upward_closed_set

enumerator downward_closed_set

Functions

template<typename T>
std::ostream &operator<<(std::ostream &os, const ClosedSet<T> &cs)

template<typename T>
struct ClosedSet

#include <closed-set.hh>

Closed set.

Contains discrete range borders, its type and the corresponding anti-chain. It is necessary to be able to evaluate relation operators <, <=, >, >=, ==, != over instances of this datatype T.

Template Parameters:

T – Datatype the closed set contains.

Public Types

using Node = OrdVec<T>

using Nodes = OrdVec<Node>

Public Functions

inline ClosedSet()

inline ClosedSet(const ClosedSetType type, const T &min_val, const T &max_val, const T &value)

inline ClosedSet(ClosedSetType type, const T &min_val, const T &max_val, const Node &node)

inline ClosedSet(const ClosedSetType type, const T &min_val, const T &max_val, const Nodes &antichain = Nodes())

bool operator==(const ClosedSet<T> &rhs) const = default

Two closed sets are equivalent iff their type, borders and corresponding antichains are the same. They are not equivalent otherwise.

inline bool operator<=(const ClosedSet<T> &rhs) const

inline bool operator>=(const ClosedSet<T> &rhs) const

inline bool is_upward_closed() const

inline bool is_downward_closed() const

inline ClosedSetType type()

inline ClosedSetType type() const

inline Nodes antichain()

inline Nodes antichain() const

inline T get_min()

inline T get_min() const

inline T get_max()

inline T get_max() const

bool contains(const Node &node) const

This function decides whether a set of elements is part of the closed set by subset-compraring the input with all elements of the antichain.

decides whether the closed set contains a given element

Parameters:

node – a given ordered vector of elements of the type T

Returns:

true iff the given ordered vector belongs to the current closed set

bool contains(const Nodes &nodes) const

This function decides whether a set of sets of elements is a part of the closed set by subset-compraring the input with all elements of the antichain.

decides whether the closed set contains a given set of sets of elements

Parameters:

nodes – a given ordered vector of ordered vectors of elements of the type T

Returns:

true iff the given ordered vector of ordered vectors belongs to the current closed set

bool in_interval(const Node &node) const

This function decides whether a given ordered vector of elements of the datatype T belongs to the discrete interval of the current closed set.

decides whether the given vector respects the borders

Parameters:

node – a given ordered vector of elements of the type T which will be inspected

Returns:

true iff the given ordered vector respects the borders

inline void insert(const T &el)

void insert(const Node &node)

Adds a new element to the closed set.

If the element is already contained in the closed set, the closed set remains unchanged. Otherwise, the antichain will be recomputed.

inserts a new element to the closed set

Parameters:

node – a given node which will be added to the closed set

inline void insert(const Nodes &nodes)

ClosedSet set_union(const ClosedSet &rhs) const

Performs an union over two closed sets with the same type and carrier.

This function simply adds all the elements of the antichain of the first closed set to the second closed set

performs an union over closed sets

Parameters:

rhs – a given closed set which will be unioned with the current one

Returns:

an union of the given closed sets

ClosedSet intersection(const ClosedSet &rhs) const

Performs an intersection over two closed sets with the same type and carrier.

performs an intersection over closed sets

Parameters:

rhs – a given closed set which will be intersectioned with the current one

Returns:

an intersection of the given closed sets

ClosedSet complement() const

Performs a complementation over a closed set.

The result will contain nodes which are not elements of the former closed set. The complement of an upward-closed set is always downward-closed and vice versa.

performs a complementation over a closed set

Returns:

a complement of a closed set

Private Members

ClosedSetType type_ = {ClosedSetType::upward_closed_set}

T min_val_

T max_val_

Nodes antichain_ = {}

Friends

friend std::ostream &operator<<(std::ostream &os, const ClosedSet<T> &cs)