File synchronized-iterator.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.

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>

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 = {}