Utils

Closed Set

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)

Sparse Set

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.

namespace utils

SparseSet.h Implements a class template of a sparse set of unsigned integers.

Non-automata-related structures and algorithms.

In particular, this includes:

1. Predicates,

2. Ordered Vectors,

3. Iterators,

4. Printers,

5. Other helper functions.

Author

Sam Griffiths www.computist.xyz https://gist.github.com/sjgriffiths/06732c6076b9db8a7cf4dfe3a7aed43a

template<typename Number>
class SparseSet

#include <sparse-set.hh>

Implementation of a set of non-negative numbers using sparse-set.

This class implements the interface of a set (similar to std::set) using sparse-set date structure, that is, a pair of vectors dense and sparse (… google it). Importantly

• Insertion and removal are constant time.

• Iteration is linear in the number of stored elements.

• It takes a lot of space, the sparse and dense vectors allocate as many indexes as the maximal stored number.

Template Parameters:

Number – Number type: type of numbers contained in the container.

Public Types

using iterator = typename std::vector<Number>::const_iterator

using const_iterator = typename std::vector<Number>::const_iterator

Public Functions

inline iterator begin()

inline const_iterator begin() const

inline iterator end()

inline const_iterator end() const

inline size_t size() const

inline size_t domain_size() const

inline bool empty() const

inline void clear()

inline void reserve(size_t u)

inline bool contains(const Number val) const

inline void insert(const Number val)

inline void erase_nocheck(const Number number)

Erase number from the set without checking for its existence.

Parameters:

number – Number to be erased.

Pre:

number exists in the set.

inline void erase(const Number val)

SparseSet() = default

New Mata code.

inline explicit SparseSet(Number domain_size)

Basic constructor where you may reserve a domain size.

inline SparseSet(std::initializer_list<Number> list)

template<class InputIterator>
inline explicit SparseSet(InputIterator first, InputIterator last)

template<class T>
inline explicit SparseSet(T &container)

inline explicit SparseSet(const BoolVector &bv)

SparseSet(const SparseSet<Number> &rhs) = default

inline SparseSet(SparseSet<Number> &&other) noexcept

SparseSet<Number> &operator=(const SparseSet<Number> &rhs) = default

inline SparseSet<Number> &operator=(SparseSet<Number> &&other) noexcept

bool operator==(const SparseSet<Number>&) const = default

inline bool consistent()

inline bool operator[](Number q) const

Returns:

True if predicate for q is set. False otherwise (even if q is out of range of the predicate).

template<class InputIterator>
inline void insert(InputIterator first, InputIterator last)

template<Iterable T>
inline void insert(const T &set)

inline void insert(const std::initializer_list<Number> &list)

template<class InputIterator>
inline void erase(InputIterator first, InputIterator last)

template<Iterable T>
inline void erase(const T &set)

inline void erase(const std::initializer_list<Number> &list)

template<class T>
inline bool intersects_with(const T &set) const

inline void complement(Number new_domain_size)

template<typename F>
inline void filter(F &&is_staying)

inline void sort()

template<typename F>
inline void rename(F &&renaming)

inline Number max()

Maximal Number in set.

Expensive operation as it has to compute the maximal Number in linear time.

inline void truncate()

Private Members

std::vector<Number> dense = {}

std::vector<Number> sparse = {}

size_t size_ = 0

Number of elements which are in the set (current size).

size_t domain_size_ = 0

Over-approximation of Number in sparse set. It represents the Numbers which were in the set throughout the life of the set until now.

truncate() will update the domain size to the current maximal Number + 1. Constructor can preallocate the sparse set and set domain size to the requested value. The structures are preallocated to at least domain_size_ size (can be more when maximal Number is removed).

Friends

inline friend bool are_disjoint(const SparseSet &A, const SparseSet &B)

OrdVector

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.

namespace utils

SparseSet.h Implements a class template of a sparse set of unsigned integers.

Non-automata-related structures and algorithms.

In particular, this includes:

1. Predicates,

2. Ordered Vectors,

3. Iterators,

4. Printers,

5. Other helper functions.

Author

Sam Griffiths www.computist.xyz https://gist.github.com/sjgriffiths/06732c6076b9db8a7cf4dfe3a7aed43a

Functions

template<class T>
bool are_disjoint(const utils::OrdVector<T> &lhs, const utils::OrdVector<T> &rhs)

template<class Key>
bool is_sorted(const std::vector<Key> &vec)

template<class Key>
class OrdVector

#include <ord-vector.hh>

Implementation of a set using ordered vector.

This class implements the interface of a set (the same interface as std::set) using ordered vector as the underlying data structure.

Template Parameters:

Key – Key type: type of the elements contained in the container. Each elements in a set is also its key.

Public Types

using VectorType = std::vector<Key>

using value_type = Key

using size_type = size_t

using iterator = typename VectorType::iterator

using const_iterator = typename VectorType::const_iterator

using const_reference = typename VectorType::const_reference

using reference = typename VectorType::reference

Public Functions

inline OrdVector()

inline explicit OrdVector(const VectorType &vec)

inline explicit OrdVector(const std::set<Key> &set)

template<class T>
inline explicit OrdVector(const T &set)

inline OrdVector(std::initializer_list<Key> list)

OrdVector(const OrdVector &rhs) = default

inline OrdVector(OrdVector &&other) noexcept

inline explicit OrdVector(const Key &key)

template<class InputIterator>
inline explicit OrdVector(InputIterator first, InputIterator last)

inline OrdVector &operator=(const OrdVector &other)

inline OrdVector &operator=(OrdVector &&other) noexcept

virtual ~OrdVector() = default

inline void insert(iterator itr, const Key &x)

template<typename ...Args>
inline reference emplace_back(Args&&... args)

inline reference push_back(const Key &t)

inline reference push_back(Key &&t)

inline virtual void reserve(size_t size)

inline virtual void resize(size_t size)

inline virtual iterator erase(const_iterator pos)

inline virtual iterator erase(const_iterator first, const_iterator last)

inline virtual void insert(const Key &x)

inline virtual void insert(const OrdVector &vec)

inline void clear()

inline virtual size_t size() const

inline size_t count(const Key &key) const

inline OrdVector difference(const OrdVector &rhs) const

Compute set difference as this minus rhs.

Parameters:

rhs – Other vector with symbols to be excluded.

Returns:

this minus rhs.

inline OrdVector intersection(const OrdVector &rhs) const

inline virtual const_iterator find(const Key &key) const

inline virtual iterator find(const Key &key)

inline virtual const Key &front() const

inline virtual Key &front()

inline bool contains(const Key &key) const

Check whether key exists in the ordered vector.

inline size_t erase(const Key &k)

Remove k from sorted vector.

This function expects the vector to be sorted.

inline virtual bool empty() const

template<typename Fun>
inline void filter_indexes(const Fun &&is_staying)

template<typename Fun>
inline void filter(const Fun &&is_staying)

inline virtual const_reference back() const

inline virtual reference back()

Get reference to the last element in the vector.

Modifying the underlying value in the reference could break sortedness.

inline virtual void pop_back()

inline virtual const_iterator begin() const

inline virtual const_iterator end() const

inline virtual iterator begin()

inline virtual iterator end()

inline virtual const_iterator cbegin() const

inline virtual const_iterator cend() const

inline bool operator==(const OrdVector &rhs) const

inline bool operator<(const OrdVector &rhs) const

inline const std::vector<Key> &to_vector() const

inline bool is_subset_of(const OrdVector &bigger) const

inline bool is_intersection_empty_with(const OrdVector &rhs) const

inline void rename(const std::vector<Key> &renaming)

Public Static Functions

static inline OrdVector with_reserved(const size_t capacity)

Create OrdVector with reserved capacity.

Parameters:

capacity – [in] Capacity of OrdVector to reserve.

Returns:

Newly create OrdVector.

static inline OrdVector difference(const OrdVector &lhs, const OrdVector &rhs)

static inline void set_union(const OrdVector &lhs, const OrdVector &rhs, OrdVector &result)

static inline OrdVector set_union(const OrdVector &lhs, const OrdVector &rhs)

static inline OrdVector intersection(const OrdVector &lhs, const OrdVector &rhs)

Private Functions

inline bool is_sorted() const

Private Members

VectorType vec_

Friends

inline friend std::ostream &operator<<(std::ostream &os, const OrdVector &vec)

Overloaded << operator.

Overloaded << operator for output stream.

See also

to_str()

Parameters:

• os – [in] The output stream

• vec – [in] Assignment to the variables

Returns:

Modified output stream

namespace std

STL namespace.

template<class Key>
struct hash<mata::utils::OrdVector<Key>>

#include <ord-vector.hh>

Public Functions

inline std::size_t operator()(const mata::utils::OrdVector<Key> &vec) const

Synchronized Iterator

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.

namespace utils

SparseSet.h Implements a class template of a sparse set of unsigned integers.

Non-automata-related structures and algorithms.

In particular, this includes:

1. Predicates,

2. Ordered Vectors,

3. Iterators,

4. Printers,

5. Other helper functions.

Author

Sam Griffiths www.computist.xyz https://gist.github.com/sjgriffiths/06732c6076b9db8a7cf4dfe3a7aed43a

Functions

template<class Container>
void push_back(SynchronizedIterator<typename Container::const_iterator> &i, const Container &container)

In order to make initialisation of the sync.

iterator nicer than inputting v.begin() and v.end() as the two parameters of the method push_back, this function wraps the method push_back, takes the iterator and v and extracts the v.begin() and v.end() from v.

template<typename Iterator>
class SynchronizedExistentialIterator : public mata::utils::SynchronizedIterator<Iterator>

#include <synchronized-iterator.hh>

Public Functions

inline Iterator get_current_minimum()

inline bool is_synchronized() const

inline virtual bool advance() override

Advances all positions just above current_minimum, that is, to or above next_minimum.

Those at next_minimum are added to currently_synchronized. Since next_minimum becomes the current minimum, new next_minimum must be updated too.

inline virtual const std::vector<Iterator> &get_current() const override

Returns the vector of current still active positions.

Beware, they will be ordered differently from how there were input into the iterator. This is due to swapping of the emptied positions with positions at the end.

inline virtual void push_back(const Iterator &begin, const Iterator &end) override

This is supposed to be called only before an iteration, after constructor of reset.

Calling after advance breaks the iterator. Specifies begin and end of one vector, to initialise before the iteration starts.

inline explicit SynchronizedExistentialIterator(const size_t size = 0)

inline void reset(const size_t size = 0)

inline void reserve(const size_t size)

Public Members

std::vector<Iterator> currently_synchronized = {}

Iterator next_minimum = {}

std::vector<Iterator> positions = {}

std::vector<Iterator> ends = {}

template<typename Iterator>
class SynchronizedIterator

#include <synchronized-iterator.hh>

Two classes that provide “synchronized” iterators through a vector of ordered vectors, (or of some ordered OrdContainer that have a similar iterator), needed in computation of post in subset construction, product, and non-determinization.

The Type stored in OrdContainers must be comparable with <,>,==,!=,<=,>=, and it must be a total (linear) ordering. The intended usage in, for instance, determinisation is for Type to be TransSymbolStates. TransSymbolStates is ordered by the symbol.

SynchronisedIterator is the parent virtual class. It stores a vector of end-iterators for the OrdContainer v and a vector of current positions. They are filled in using the function push_back(begin,end), that adds begin and end iterators of v to positions and ends, respectively Method advance advances all positions forward so that they are synchronized on the next smallest equiv class (next smallest symbol in the case of TransSymbolStates).

There are two versions of the class. i) In product, ALL positions must point to currently the smallest equiv. class (Moves with the same symbol). Method get_current then returns the vector of all position iterators, synchronized. ii) In determinization, it is enough that there EXISTS a position that points to the smallest class. Method get_current then returns the vector of only those positions that point to the smallest equiv. class.

Usage: 0) construct, 1) fill in using push_back, iterate using advance and get_current, 2) reset, goto 1)

The memory allocated internally for positions and ends is kept after reset, so it is advisable to use the same iterator for many iterations, as opposed to creating a new one for each iteration. Class implementing synchronized iteration.

Subclassed by SynchronizedExistentialIterator< Iterator >, SynchronizedUniversalIterator< Iterator >

Public Functions

inline explicit SynchronizedIterator(const size_t size = 0)

Parameters:

size – Number of elements to reserve up-front for positions and ends.

inline virtual void push_back(const Iterator &begin, const Iterator &end)

This is supposed to be called only before an iteration, after constructor of reset.

Calling after advance breaks the iterator. Specifies begin and end of one vector, to initialise before the iteration starts.

inline void reset(const size_t size = 0)

Empties positions and ends.

Though they should keep the allocated space.

Parameters:

size – Number of elements to reserve up-front for positions and ends.

inline void reserve(const size_t size)

virtual bool advance() = 0

virtual const std::vector<Iterator> &get_current() const = 0

virtual ~SynchronizedIterator() = default

Public Members

std::vector<Iterator> positions = {}

std::vector<Iterator> ends = {}

template<typename Iterator>
class SynchronizedUniversalIterator : public mata::utils::SynchronizedIterator<Iterator>

#include <synchronized-iterator.hh>

Public Functions

inline virtual bool advance()

Advances all positions to the NEXT minimum and returns true (though the next minimum might be the current state if synchronized_at_current_minimum is false), or returns false if positions cannot be synchronized.

If positions are synchronized to start with, then synchronized_at_current_minimum decides whether to stay or advance further. The general of the algorithm is to synchronize everybody with position[0].

inline virtual const std::vector<Iterator> &get_current() const

Returns the vector of current positions.

inline explicit SynchronizedUniversalIterator(const size_t size = 0)

inline void reset(const size_t size = 0)

inline virtual void push_back(const Iterator &begin, const Iterator &end)

This is supposed to be called only before an iteration, after constructor of reset.

Calling after advance breaks the iterator. Specifies begin and end of one vector, to initialise before the iteration starts.

inline void reserve(const size_t size)

Public Members

bool synchronized_at_current_minimum = false

“minimum” would be the smallest class bounded from below by all positions that appears in all OrdContainers.

Are we sure that all positions at this class? Invariant: it can be true only if all positions are indeed synchronized.

std::vector<Iterator> positions = {}

std::vector<Iterator> ends = {}

Other Utils

Defines

PRINT_VERBOSE_LVL(lvl, title, x)

macro for debug outputs

PRINT_VERBOSE_LVL_LN(lvl, title, x)

DEBUG_PRINT(x)

DEBUG_PRINT_LN(x)

DEBUG_VM_HIGH_PRINT(x)

DEBUG_VM_HIGH_PRINT_LN(x)

DEBUG_VM_LOW_PRINT(x)

DEBUG_VM_LOW_PRINT_LN(x)

WARN_PRINT(x)

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.

Variables

unsigned LOG_VERBOSITY

log verbosity

const std::string g_GIT_SHA1

git sha

class BoolVector : public std::vector<uint8_t>

#include <utils.hh>

Representation of bool vector by a vector of uint8_t.

Public Functions

inline BoolVector(size_t size, bool value)

BoolVector(const BoolVector&) = default

BoolVector(BoolVector&&) noexcept = default

BoolVector() = default

inline BoolVector(std::initializer_list<uint8_t> uint8_ts)

inline explicit BoolVector(const std::vector<uint8_t> &uint8_ts)

BoolVector &operator=(const BoolVector&) = default

BoolVector &operator=(BoolVector&&) noexcept = default

inline size_t count() const

Count the number of set elements.

template<typename T>
inline T &get_elements(T &element_set)

Public Static Functions

template<typename T>
static inline T *get_elements(T *element_set, const BoolVector &bool_vec)

namespace utils

SparseSet.h Implements a class template of a sparse set of unsigned integers.

Non-automata-related structures and algorithms.

In particular, this includes:

1. Predicates,

2. Ordered Vectors,

3. Iterators,

4. Printers,

5. Other helper functions.

Author

Sam Griffiths www.computist.xyz https://gist.github.com/sjgriffiths/06732c6076b9db8a7cf4dfe3a7aed43a

Functions

inline std::string replace_all(const std::string &input, const std::string &needle, const std::string &replace)

Replace all occurrences of a substring in a string.

Parameters:

• input – The input string

• needle – The substring to be replaced

• replace – The replacement string

Returns:

A new string with all occurrences of the substring replaced.

template<class T>
bool are_disjoint(const std::set<T> &lhs, const std::set<T> &rhs)

Are two sets disjoint?

template<class T, class Cont>
bool is_in(const T &elem, const Cont &cont)

Is there an element in a container?

template<class T>
inline size_t hash_combine(size_t lhs, const T &rhs)

Combine two hash values.

Values taken from http://www.boost.org/doc/libs/1_64_0/boost/functional/hash/hash.hpp

TODO: fix to be more suitable for 64b

template<typename It>
size_t hash_range(It first, It last)

Hashes a range.

Inspired by http://www.boost.org/doc/libs/1_64_0/boost/functional/hash/hash.hpp

template<class T, class K>
inline bool haskey(const T &cont, const K &key)

checks whether a container with find contains a key

template<template<class, class, class...> class Map, class T1, class T2, class ...Args>
Map<T2, T1> invert_map(const Map<T1, T2> &mp)

inverts a map (should work for std::map and std::unordered_map)

template<class Vector>
inline void reserve_on_insert(Vector &vec, size_t needed_capacity = 0, size_t extension = 32)

template<class Vector, typename Index>
void defragment(Vector &vec, const std::vector<Index> &renaming)

template<class Vector, typename Index>
void rename(Vector &vec, const std::vector<Index> &renaming)

template<class Vector, typename Fun>
void filter_indexes(Vector &vec, const Fun &&is_staying)

template<class Vector, typename Fun>
void filter(Vector &vec, const Fun &&is_staying)

template<class Vector>
inline void sort_and_rmdupl(Vector &vec)

template<class Tuple, size_t N>
struct TuplePrinter

#include <utils.hh>

Public Static Functions

static inline std::string print(const Tuple &t)

template<class Tuple>
struct TuplePrinter<Tuple, 1>

#include <utils.hh>

Public Static Functions

static inline std::string print(const Tuple &t)

static inline std::string print(const Tuple &t)

namespace std

STL namespace.

Functions

template<class A>
std::string to_string(const A &value)

arbitrary type with the << operator

template<class A>
std::string to_string(const std::set<A> &st)

set to string

template<class A>
std::string to_string(const std::vector<A> &vec)

Vector to string.

template<class A>
std::string to_string(const std::list<A> &vec)

List to string.

template<class A>
std::string to_string(const std::stack<A> &stck)

stack to string

template<class A>
std::string to_string(const std::function<A> &fun)

function to string

template<class A, class B>
std::string to_string(const std::pair<A, B> &p)

template<class A, class B>
std::string to_string(const std::map<A, B> &mp)

map to string

template<class A, class B>
std::string to_string(const std::unordered_map<A, B> &unmap)

unordered_map to string

template<class A, class B>
std::string to_string(const std::unordered_multimap<A, B> &unmap)

unordered_multimap to string

inline std::string to_string(char ch)

Character to string.

inline std::string to_string(const std::string &str)

String to string.

template<class ...Ts>
std::string to_string(const std::tuple<Ts...> &tup)

tuple to string

template<class A, class B>
struct hash<std::pair<A, B>>

#include <utils.hh>

A hasher for pairs.

Public Functions

inline size_t operator()(const std::pair<A, B> &k) const

template<class A>
struct hash<std::set<A>>

#include <utils.hh>

A hasher for sets.

Public Functions

inline size_t operator()(const std::set<A> &cont) const

template<class A>
struct hash<std::vector<A>>

#include <utils.hh>

A hasher for vectors.

Public Functions

inline size_t operator()(const std::vector<A> &cont) const