Elementary language with its neighbor conditions. More...

#include <neighbor_conditions.hh>

Public Member Functions
auto	preciseClocksAfterReset (const TATransition &transition) const
	Make precise clocks after applying a reset.

NeighborConditions	reconstruct (std::unordered_set< ClockVariables > currentPreciseClocks) const
	Reconstruct the neighbor conditions with new precise clocks.

	NeighborConditions (const NeighborConditions &conditions)=default

	NeighborConditions (NeighborConditions &&conditions)=default

NeighborConditions &	operator= (const NeighborConditions &conditions)=default

NeighborConditions &	operator= (NeighborConditions &&conditions)=default

	NeighborConditions (ForwardRegionalElementaryLanguage original, std::unordered_set< ClockVariables > preciseClocks)

	NeighborConditions (ForwardRegionalElementaryLanguage original, const std::vector< ClockVariables > &preciseClocks)

NeighborConditions	makeAfterTransition (const Alphabet action, const TATransition &transition) const
	Construct the neighbor conditions after a transition.

auto	toOriginalGuard () const
	Return the guard of the original elementary language. More...

bool	match (const std::vector< Constraint > &guard) const
	Return if the given guard matches with this elementary language.

size_t	getClockSize () const

bool	precise () const
	Returns if the relaxed guard is precise.

bool	match (const TATransition &transition) const
	Return if the given transition matches with this elementary language.

auto	toRelaxedGuard () const
	Return the guard of the original elementary language and its neighbors.

NeighborConditions	successor (const Alphabet action) const

NeighborConditions	successor () const

void	successorAssign ()

std::vector< ClockVariables >	impreciseClocks () const
	Returns the list of imprecise clocks. More...

std::vector< double >	toOriginalValuation () const
	Construct the reset to embed to the target condition.

std::vector< double >	toOriginalValuation (const std::size_t minSize) const
	Construct the reset to embed to the target condition.

NeighborConditions	applyResets (const TATransition::Resets &resets) const
	Return the neighbor conditions after applying the given resets.

bool	isInternal (const TATransition &transition) const
	Check if the transition from the current neighbor is internal.

ForwardRegionalElementaryLanguage	constructOriginalAfterTransition (const Alphabet action, const TATransition &transition) const

std::ostream &	print (std::ostream &os) const

bool	operator== (const NeighborConditions &conditions) const

bool	operator!= (const NeighborConditions &conditions) const

std::size_t	hash_value () const

Static Public Member Functions
static auto	preciseClocksAfterReset (const std::unordered_set< ClockVariables > &preciseClocks, const TATransition &transition)
	Make precise clocks after applying a reset.

static auto	makeNeighbors (const ForwardRegionalElementaryLanguage &original, const std::unordered_set< ClockVariables > &preciseClocks)

static std::size_t	computeClockSize (const TAState *state)

static std::size_t	computeTargetClockSize (const TATransition &transition)

Detailed Description

Elementary language with its neighbor conditions.

This is mainly used to handle imprecise clocks in the DTA construction.

See also: ObservationTable

Invariant: std::all_of(neighbors.begin(), neighbors.end(), [&] (const auto &neighbor) {return neighbor.getWord() == original.getWord();}); std::all_of(neighbors.begin(), neighbors.end(), [&] (const auto &neighbor) {return neighbor.getTimedCondition().size() == original.getTimedCondition().size();}); clockSize == original.getTimedCondition().size(); std::all_of(neighbors.begin(), neighbors.end(), [&] (const auto &neighbor) {return neighbor.getTimedCondition().size() == clockSize;})

Member Function Documentation

◆ impreciseClocks()

std::vector<ClockVariables> learnta::NeighborConditions::impreciseClocks ( ) const

inline

Returns the list of imprecise clocks.

Postcondition: The result is sorted

◆ toOriginalGuard()

auto learnta::NeighborConditions::toOriginalGuard ( ) const

inline

Return the guard of the original elementary language.

This is intended to be used to match with a transition

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

include/neighbor_conditions.hh

Public Member Functions

Static Public Member Functions

Detailed Description

Member Function Documentation

◆ impreciseClocks()

◆ toOriginalGuard()