Represent a tree of properties with alternating quantifiers. More...

#include <runner/nonDeterministicMachineRunner.h>

Public Types
enum	Quantifier { Quantifier::Existential, Quantifier::Universal }
	The quantifier for each node of an alternating tree. More...

typedef size_t	Uid
	The keys of leaves and sub-Trees.

Public Member Functions
void	insert (Uid subUid, Quantifier q, std::vector< std::tuple< LeafType, std::optional< bool >>> &newLeaves)
	Replace a uid with a a leaf of new leaves. More...

std::pair< const Uid, LeafType > &	pick ()
	Pick a leaf with its uid. More...

Uid	lastLeafUid ()
	The last uid of the leaves. More...

bool	hasLeaves () const
	Whether the node has leaves. More...

const std::map< Uid, std::shared_ptr< AlternatingTree< LeafType > > > &	getSubTrees ()
	Get sub trees. More...

void	decide (Uid subUid, bool d)
	Decide a leaf. More...

bool	decided () const noexcept
	Whether the node is decided. More...

std::optional< bool >	getDecision () const noexcept
	Get the optional decision. More...

template<typename CharT = char, typename Traits = std::char_traits<CharT>>
std::function< std::basic_ostream< CharT, Traits > &(std::basic_ostream< CharT, Traits > &)>	debug () const
	Debug printer for the alternating tree. More...

template<typename CharT = char, typename Traits = std::char_traits<CharT>>
std::function< std::basic_ostream< CharT, Traits > &(std::basic_ostream< CharT, Traits > &)>	debug (size_t i) const
	Debug printer for the alternating tree, with initial indentation. More...

void	compact ()
	Remove decided items, since they are useless, except for documentation.

Static Public Member Functions
static std::shared_ptr< AlternatingTree >	makeAlternatingTreeRoot (Quantifier quantifier, const std::vector< LeafType > &leaves)
	Build a new alternating tree, with provided leaves and quantifier. More...

template<typename CharT = char, typename Traits = std::char_traits<CharT>>
static std::function< std::basic_ostream< CharT, Traits > &(std::basic_ostream< CharT, Traits > &)>	debug (const Quantifier &q)
	Debug printer for a quantifier. More...

Friends
template<typename CharT = char, typename Traits = std::char_traits<CharT>>
std::basic_ostream< CharT, Traits > &	operator<< (std::basic_ostream< CharT, Traits > &os, const AlternatingTree &tree)
	Debug printer for the alternating tree. More...

Detailed Description

template<typename LeafType>
class TuringSim::Runner::AlternatingTree< LeafType >

Represent a tree of properties with alternating quantifiers.

Template Parameters

LeafType the type of leaves.

This tree is a structure ad-hoc for alternating machines. Each node has:

a quantifier, to apply between all leaves and sub-trees
a list of leaves identified: properties that can be decided.
a list of sub-trees identified

Leaves and sub-trees are identified by non conflicting integers. In addition, non-root nodes have a smart pointer to its parent, with its own id, from the point of view of its parent.

Alternating trees can only be built with leaves, but no sub-trees. Leaves can either be decided, or replaced by a sub-tree. Sub-trees with same quantifier and smashed.

When a leaf is decided, if the decision allows to decide the node, it is immediately done and propagated upwards. When a leaf is decided but does not allows to decide the node, it is removed. The same apply to the decision of sub-trees. When a node has no sub-trees and leaves left, it can be decided.

Definition at line 32 of file nonDeterministicMachineRunner.h.

Member Enumeration Documentation

◆ Quantifier

template<typename LeafType >

enum TuringSim::Runner::AlternatingTree::Quantifier

strong

The quantifier for each node of an alternating tree.

Enumerator
Existential	The node is existential.
Universal	The node is universal.

Definition at line 37 of file nonDeterministicMachineRunner.h.

Member Function Documentation

◆ debug() [1/3]

template<typename LeafType >

template<typename CharT = char, typename Traits = std::char_traits<CharT>>

std::function<std::basic_ostream<CharT, Traits>&(std::basic_ostream<CharT, Traits>&)> TuringSim::Runner::AlternatingTree< LeafType >::debug ( ) const

inline

Debug printer for the alternating tree.

Template Parameters

CharT	char type.
Traits	`std::basic_ostream` trait.

Returns: a debug printer.

Definition at line 162 of file nonDeterministicMachineRunner.h.

Here is the caller graph for this function:

◆ debug() [2/3]

template<typename LeafType >

template<typename CharT = char, typename Traits = std::char_traits<CharT>>

static std::function<std::basic_ostream<CharT, Traits>&(std::basic_ostream<CharT, Traits>&)> TuringSim::Runner::AlternatingTree< LeafType >::debug ( const Quantifier & q )

inlinestatic

Debug printer for a quantifier.

Template Parameters

CharT	char type.
Traits	`std::basic_ostream` trait.

Parameters

q	the quantifier.

Returns: a debug printer.

Definition at line 173 of file nonDeterministicMachineRunner.h.

◆ debug() [3/3]

template<typename LeafType >

template<typename CharT = char, typename Traits = std::char_traits<CharT>>

std::function<std::basic_ostream<CharT, Traits>&(std::basic_ostream<CharT, Traits>&)> TuringSim::Runner::AlternatingTree< LeafType >::debug ( size_t i ) const

inline

Debug printer for the alternating tree, with initial indentation.

Template Parameters

CharT	char type.
Traits	`std::basic_ostream` trait.

Parameters

i	the indentation level.

Returns: a debug printer.

Definition at line 206 of file nonDeterministicMachineRunner.h.

Here is the call graph for this function:

◆ decide()

template<typename LeafType >

void TuringSim::Runner::AlternatingTree< LeafType >::decide	(	Uid	subUid,
		bool	d
	)

inline

Decide a leaf.

Parameters

subUid	the uid of the leaf to decide.
d	the decision for this leaf.

Definition at line 110 of file nonDeterministicMachineRunner.h.

Here is the caller graph for this function:

◆ decided()

template<typename LeafType >

bool TuringSim::Runner::AlternatingTree< LeafType >::decided ( ) const

inlinenoexcept

Whether the node is decided.

Returns: True iff the node is decided.

Definition at line 135 of file nonDeterministicMachineRunner.h.

◆ getDecision()

template<typename LeafType >

std::optional<bool> TuringSim::Runner::AlternatingTree< LeafType >::getDecision ( ) const

inlinenoexcept

Get the optional decision.

Returns: If the node is decided, an option containing the Boolean decision. Otherwise an empty option.

Definition at line 142 of file nonDeterministicMachineRunner.h.

◆ getSubTrees()

template<typename LeafType >

const std::map<Uid, std::shared_ptr<AlternatingTree<LeafType> > >& TuringSim::Runner::AlternatingTree< LeafType >::getSubTrees ( )

inline

Get sub trees.

Returns: a const reference to a map from uid to subtrees.

Definition at line 102 of file nonDeterministicMachineRunner.h.

◆ hasLeaves()

template<typename LeafType >

bool TuringSim::Runner::AlternatingTree< LeafType >::hasLeaves ( ) const

inline

Whether the node has leaves.

Returns: True iff the node has no (more) leaves.

Definition at line 95 of file nonDeterministicMachineRunner.h.

◆ insert()

template<typename LeafType >

void TuringSim::Runner::AlternatingTree< LeafType >::insert	(	Uid	subUid,
		Quantifier	q,
		std::vector< std::tuple< LeafType, std::optional< bool >>> &	newLeaves
	)

inline

Replace a uid with a a leaf of new leaves.

Parameters

[in]	subUid	the uid of the leaf to replace.
[in]	q	the quantifier between new nodes.
[in]	newLeaves	new leaves, with optional decision.

Remove the leaf with id subUid. If q is:

the quantifier of the node, new leaves are added to node's leaves, with new, bigger ids.
the quantifier is not the one of the node, a new subtree is constructed. The new tree get the uid of the removed leaf.

For nodes with decisions, this decision is applied.

Definition at line 59 of file nonDeterministicMachineRunner.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ lastLeafUid()

template<typename LeafType >

Uid TuringSim::Runner::AlternatingTree< LeafType >::lastLeafUid ( )

inline

The last uid of the leaves.

Returns: The biggest uid of leaves.

Definition at line 88 of file nonDeterministicMachineRunner.h.

◆ makeAlternatingTreeRoot()

template<typename LeafType >

static std::shared_ptr<AlternatingTree> TuringSim::Runner::AlternatingTree< LeafType >::makeAlternatingTreeRoot	(	Quantifier	quantifier,
		const std::vector< LeafType > &	leaves
	)

inlinestatic

Build a new alternating tree, with provided leaves and quantifier.

Parameters

quantifier	the quantifier of the root node.
leaves	the list of of the root node.

Returns: a shared pointer to a fresh allocated tree.

Definition at line 151 of file nonDeterministicMachineRunner.h.

Here is the caller graph for this function:

◆ pick()

template<typename LeafType >

std::pair<const Uid, LeafType>& TuringSim::Runner::AlternatingTree< LeafType >::pick ( )

inline

Pick a leaf with its uid.

Returns: a modifying reference to a unique id and a leaf.

UB is there is no more leaves.

Definition at line 81 of file nonDeterministicMachineRunner.h.

Friends And Related Function Documentation

◆ operator<<

template<typename LeafType >

template<typename CharT = char, typename Traits = std::char_traits<CharT>>

std::basic_ostream<CharT, Traits>& operator<<	(	std::basic_ostream< CharT, Traits > &	os,
		const AlternatingTree< LeafType > &	tree
	)

friend

Debug printer for the alternating tree.

Template Parameters

CharT	char type.
Traits	`std::basic_ostream` trait.

Parameters

os	the output stream.
tree	the tree to print.

Returns: a reference to os..

Definition at line 194 of file nonDeterministicMachineRunner.h.

The documentation for this class was generated from the following file:

include/runner/nonDeterministicMachineRunner.h

Public Types

Public Member Functions

Static Public Member Functions

Friends

Detailed Description

template<typename LeafType> class TuringSim::Runner::AlternatingTree< LeafType >

Member Enumeration Documentation

◆ Quantifier

Member Function Documentation

◆ debug() [1/3]

◆ debug() [2/3]

◆ debug() [3/3]

◆ decide()

◆ decided()

◆ getDecision()

◆ getSubTrees()

◆ hasLeaves()

◆ insert()

◆ lastLeafUid()

◆ makeAlternatingTreeRoot()

◆ pick()

Friends And Related Function Documentation

◆ operator<<

template<typename LeafType>
class TuringSim::Runner::AlternatingTree< LeafType >