A timed condition, a finite conjunction of inequalities of the form \(\tau_{i} + \tau_{i + 1} \dots \tau_{j} \bowtie c\), where \({\bowtie} \in \{>,\ge,\le,<\}\) and \(c \in \mathbb{N} \). More...

#include <timed_condition.hh>

Collaboration diagram for learnta::TimedCondition:

[legend]

Public Member Functions
	TimedCondition (const std::vector< double > &accumulatedDuration)
	Construct a timed condition from concrete values of T_{i,j}. The generated timed condition is the simple timed condition containing the given concrete valuation. More...

size_t	size () const
	Return the number of the variables in this timed condition.

bool	isSimple () const
	Returns if this timed condition is simple. More...

TimedCondition	operator+ (const TimedCondition &another) const
	Concatenate two timed conditions. More...

JuxtaposedZone	operator^ (const TimedCondition &another) const
	Juxtapose two timed conditions. More...

JuxtaposedZone	juxtaposeRight (const TimedCondition &right, Eigen::Index commonVariableSize) const
	Juxtapose two timed conditions renaming variable. More...

JuxtaposedZone	juxtaposeLeft (const TimedCondition &left, Eigen::Index commonVariableSize) const
	Juxtapose two timed conditions renaming variable. More...

Bounds	getLowerBound (std::size_t i, std::size_t j) const
	Returns the lower bound of \(\tau_i + \tau_{i+1} + \dots \tau_{j} \).

Bounds	getUpperBound (std::size_t i, std::size_t j) const
	Returns the upper bound of \(\tau_i + \tau_{i+1} + \dots \tau_{j} \).

void	restrictLowerBound (std::size_t i, std::size_t j, Bounds lowerBound, bool force=false)
	Restrict the lower bound of \(\tau_i + \tau_{i+1} + \dots \tau_{j} \). More...

void	restrictUpperBound (std::size_t i, std::size_t j, Bounds upperBound, bool force=false)
	Restrict the upper bound of \(\tau_i + \tau_{i+1} + \dots \tau_{j} \). More...

void	convexHullAssign (const TimedCondition &condition)
	Make it to be the convex hull of this timed condition and the given timed condition.

TimedCondition	convexHull (const TimedCondition &condition) const
	Return the convex hull of this timed condition and the given timed condition.

void	enumerate (std::vector< TimedCondition > &simpleConditions) const
	Make a vector of simple timed conditions in this timed condition. More...

std::vector< TimedCondition >	enumerate () const
	Make a vector of simple timed conditions in this timed condition. More...

TimedCondition	successor (const std::deque< ClockVariables > &variables) const
	Make a continuous successor by elapsing variables.

void	successorAssign (const std::deque< ClockVariables > &variables)
	Make a continuous successor by elapsing variables.

void	removeEqualityUpperBoundAssign ()
	Remove the equality upper bound.

void	removeUpperBoundAssign ()
	Remove the upper bounds.

TimedCondition	predecessor (const std::deque< ClockVariables > &variables) const
	Make a continuous predecessor by backward-elapsing variables.

TimedCondition	prefix (const std::deque< ClockVariables > &variables) const
	Make a continuous prefix.

TimedCondition	suffix (const std::deque< ClockVariables > &variables) const
	Make a continuous suffix.

TimedCondition	extendN () const
	Add another variable \(x_{n+1}\) such that \(x_n = x_{n+1}\).

TimedCondition	removeN () const
	Remove \(x_{N}\).

TimedCondition	removeZero () const
	Remove \(x_{0}\) TODO: Implement it.

bool	hasEqualityN () const
	Return if there is \(\mathbb{T}_{i,N} = c\). More...

TimedCondition	extendZero () const
	Rename each variable \(x_i\) to \(x_{i+1}\) and add \(x_0\) such that \(x_0 = x_1\).

std::vector< std::size_t >	getStrictlyConstrainedVariables (const TimedCondition &originalCondition, const size_t examinedVariableSize) const
	Returns the set of variables strictly constrained compared with the original condition. More...

bool	operator== (const TimedCondition &condition) const

bool	operator!= (const TimedCondition &condition) const

std::vector< Constraint >	toGuard () const

bool	hasPrefix () const
	Return if this timed condition has a (continuous) prefix.

bool	hasSuffix () const
	Return if this timed condition has a (continuous) suffix.

bool	includes (const TimedCondition &condition) const
	Return if this timed condition includes the given timed condition.

TimedCondition	operator&& (const TimedCondition &another) const
	Returns the intersection of two timed conditions.

bool	isSatisfiableNoCanonize () const
	Returns if the timed condition is satisfiable.

	operator bool ()
	Returns if the timed condition is satisfiable.

TimedCondition	applyResets (const TATransition::Resets &resets) const

TimedCondition	applyResets (const TATransition::Resets &resets, const std::size_t targetClockSize) const
	Return the timed condition after applying the given reset. More...

bool	isPoint (std::size_t i) const
	Check if T_{i, \|T\|} is a point.

std::size_t	hash_value () const

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

Static Public Member Functions
static TimedCondition	makeExact (const std::vector< double > &accumulatedDuration)
	Construct a timed condition from concrete values of T_{i,j}. The generated timed condition only contains the given concrete valuation. More...

static TimedCondition	empty ()
	Construct the empty timed condition, i.e. \(\tau_0 = 0\).

Protected Member Functions
	TimedCondition (Zone &&zone)

Protected Attributes
Zone	zone
	A zone to represent the timing constraint.

Friends
class	NeighborConditions

Detailed Description

A timed condition, a finite conjunction of inequalities of the form \(\tau_{i} + \tau_{i + 1} \dots \tau_{j} \bowtie c\), where \({\bowtie} \in \{>,\ge,\le,<\}\) and \(c \in \mathbb{N} \).

Let \(x_0, x_1, \dots x_N\) be the variables in the zone. We use \(x_i\) to represent \(\mathbb{T}_{i,N} = \tau_{i} + \tau_{i+1} \dots \tau_{N}\). We note that the first row and column with index 0 of DBM are for the constant 0, and we have to shift the index appropriately.

Note: Policy: We wrap all the low-level DBM operations in this class.

Constructor & Destructor Documentation

◆ TimedCondition()

learnta::TimedCondition::TimedCondition ( const std::vector< double > & accumulatedDuration )

inlineexplicit

Construct a timed condition from concrete values of T_{i,j}. The generated timed condition is the simple timed condition containing the given concrete valuation.

Parameters

[in] accumulatedDuration a vector representing \(\mathbb{T}_{i,N}\), where \(N\) is the length.

Member Function Documentation

◆ applyResets()

TimedCondition learnta::TimedCondition::applyResets	(	const TATransition::Resets &	resets,
		const std::size_t	targetClockSize
	)		const

inline

Return the timed condition after applying the given reset.

Parameters

resets	The applied reset
targetClockSize	The number of the clock variables in the target language

Postcondition: There is a clock valuation in this condition such that its value after reset is in the resulting condition.

◆ enumerate() [1/2]

std::vector<TimedCondition> learnta::TimedCondition::enumerate ( ) const

inline

Make a vector of simple timed conditions in this timed condition.

The construction is as follows.

For each \(\tau_i + \tau_{i+1} + \dots \tau_{j} \), we restrict the constraints to be a point or a unit open interval.
- This can be unnecessary. In that case, we remain the timed condition as it is.
If the restricted timed condition is simple, we add it the resulting vector.
Otherwise, we keep refining it.

Precondition: zone is canonical

◆ enumerate() [2/2]

void learnta::TimedCondition::enumerate ( std::vector< TimedCondition > & simpleConditions ) const

inline

Make a vector of simple timed conditions in this timed condition.

The construction is as follows.

For each \(\tau_i + \tau_{i+1} + \dots \tau_{j} \), we restrict the constraints to be a point or a unit open interval.
- This can be unnecessary. In that case, we remain the timed condition as it is.
If the restricted timed condition is simple, we add it the resulting vector.
Otherwise, we keep refining it.

Precondition: zone is canonical

◆ getStrictlyConstrainedVariables()

std::vector<std::size_t> learnta::TimedCondition::getStrictlyConstrainedVariables	(	const TimedCondition &	originalCondition,
		const size_t	examinedVariableSize
	)		const

inline

Returns the set of variables strictly constrained compared with the original condition.

Precondition: this condition and original condition should have the same variable space.

◆ hasEqualityN()

bool learnta::TimedCondition::hasEqualityN ( ) const

inline

Return if there is \(\mathbb{T}_{i,N} = c\).

Precondition: the timed condition is simple

◆ isSimple()

bool learnta::TimedCondition::isSimple ( ) const

inline

Returns if this timed condition is simple.

Precondition: zone is canonical

◆ juxtaposeLeft()

JuxtaposedZone learnta::TimedCondition::juxtaposeLeft	(	const TimedCondition &	left,
		Eigen::Index	commonVariableSize
	)		const

inline

Juxtapose two timed conditions renaming variable.

See also: JuxtaposedZone::JuxtaposedZone

◆ juxtaposeRight()

JuxtaposedZone learnta::TimedCondition::juxtaposeRight	(	const TimedCondition &	right,
		Eigen::Index	commonVariableSize
	)		const

inline

Juxtapose two timed conditions renaming variable.

See also: JuxtaposedZone::JuxtaposedZone

◆ makeExact()

static TimedCondition learnta::TimedCondition::makeExact ( const std::vector< double > & accumulatedDuration )

inlinestatic

Construct a timed condition from concrete values of T_{i,j}. The generated timed condition only contains the given concrete valuation.

Parameters

[in] accumulatedDuration a vector representing \(\mathbb{T}_{i,N}\), where \(N\) is the length.

◆ operator+()

TimedCondition learnta::TimedCondition::operator+ ( const TimedCondition & another ) const

inline

Concatenate two timed conditions.

Let \(N\) and \(M\) be the dimensions of the concatenated timed conditions \(\Lambda\) and \(\Lambda'\). The resulting timed condition \(\Lambda''\) satisfies the following.

If \( 0 \leq i \leq j < N\), the constraint on \(\mathbb{T}''_{i,j}\) in \(\Lambda''\) is the same as the constraint on \(\mathbb{T}_{i,j}\) in \(\Lambda\).
If \( N < i \leq j \leq N + M\), the constraint on \(\mathbb{T}''_{i, j}\) in \(\Lambda''\) is the same as the constraint on \(\mathbb{T}'_{i - N, j - N}\) in \(\Lambda'\).
If \( 0 \leq i \leq N \leq j\), the constraint on \(\mathbb{T}''_{i,j}\) in \(\Lambda''\) is the same as the constraint on \(\mathbb{T}_{i, N} + \mathbb{T}'_{0, j - N}\).

Let \(A, B, C\) be the DBM representing \(\Lambda, \Lambda', \Lambda''\), respectively. To construct \(C\) from \(A\) and \(B\), what we have to do is as follows.
- If \( 0 \leq i \leq j < N\), the constraint on \(\mathbb{T}''_{i,j}\) in \(\Lambda''\) is the same as the constraint on \(\mathbb{T}_{i,j}\) in \(\Lambda\).
  - Copy \(A_{(1, 1), (N, N)}\) to \(C_{(1, 1), (N, N)}\).
- If \( N < i \leq j \leq N + M\), the constraint on \(\mathbb{T}''_{i, j}\) in \(\Lambda''\) is the same as the constraint on \(\mathbb{T}'_{i - N, j - N}\) in \(\Lambda'\).
  - Copy \(B_{(2, 2), (M - 1, M - 1)}\) to \(C_{(N + 1, N + 1), (M - 1, M - 1)}\).
  - Copy \(B_{(2, 0), (M - 1, 1)}\) to \(C_{(N + 1, 0), (M - 1, 1)}\).
  - Copy \(B_{(0, 2), (1, M - 1)}\) to \(C_{(0, N + 1), (1, M - 1)}\).
- If \( 0 \leq i \leq N \leq j\), the constraint on \(\mathbb{T}''_{i,j}\) in \(\Lambda''\) is the same as the constraint on \(\mathbb{T}_{i, N} + \mathbb{T}'_{0, j - N}\).
  - Copy \(A_{(1, 0), (N, 1)}\) to \(C_{(1, i), (N, 1)}\) for each \(i \in \{0, N, N + 1, \dots, N + M - 1\}\).
  - Copy \(A_{(0, 1), (1, N)}\) to \(C_{(i, 1), (1, N)}\) for each \(i \in \{0, N, N + 1, \dots, N + M - 1\}\).
  - Add \(B_{(2, 1), (M - 1, 1)}\) to \(C_{(N + 1, i), (M - 1, 1)}\) for each \(i \in \{1, \dots, N\}\).
  - Add \(B_{(1, 2), (1, M - 1)}\) to \(C_{(i, N + 1), (1, M - 1)}\) for each \(i \in \{1, \dots, N\}\).
  - Add \(B_{(1, 0)}\) to \(C_{(1, 0), (N, 1)}\).
  - Add \(B_{(0, 1)}\) to \(C_{(0, 1), (1, N)}\).
By combining the above, what we do is as follows.
- Copy \(A_{(0, 0), (N + 1, N + 1)}\) to \(C_{(0, 0), (N + 1, N + 1)}\).
- Copy \(A_{(1, 0), (N, 1)}\) to \(C_{(1, i), (N, 1)}\) for each \(i \in \{N, N + 1, \dots, N + M - 1\}\).
- Copy \(A_{(0, 1), (1, N)}\) to \(C_{(i, 1), (1, N)}\) for each \(i \in \{N, N + 1, \dots, N + M - 1\}\).
- Copy \(B_{(2, 2), (M - 1, M - 1)}\) to \(C_{(N + 2, N + 2), (M - 1, M - 1)}\).
- Copy \(B_{(2, 0), (M - 1, 1)}\) to \(C_{(N + 1, 0), (M - 1, 1)}\).
- Copy \(B_{(0, 2), (1, M - 1)}\) to \(C_{(0, N + 1), (1, M - 1)}\).
- Add \(B_{(2, 1), (M - 1, 1)}\) to \(C_{(N + 1, i), (M - 1, 1)}\) for each \(i \in \{1, \dots, N\}\).
- Add \(B_{(1, 2), (1, M - 1)}\) to \(C_{(i, N + 1), (1, M - 1)}\) for each \(i \in \{1, \dots, N\}\).
- Add \(B_{(1, 0)}\) to \(C_{(1, 0), (N, 1)}\).
- Add \(B_{(0, 1)}\) to \(C_{(0, 1), (1, N)}\).

Postcondition: The dimension of the resulting timed conditions is the sum of the dimensions of the inputs - 1.

◆ operator^()

JuxtaposedZone learnta::TimedCondition::operator^ ( const TimedCondition & another ) const

inline

Juxtapose two timed conditions.

See also: JuxtaposedZone::JuxtaposedZone

Postcondition: The resulting JuxtaposedZone is canonical

◆ restrictLowerBound()

void learnta::TimedCondition::restrictLowerBound	(	std::size_t	i,
		std::size_t	j,
		Bounds	lowerBound,
		bool	force = `false`
	)

inline

Restrict the lower bound of \(\tau_i + \tau_{i+1} + \dots \tau_{j} \).

Postcondition: zone is canonical

◆ restrictUpperBound()

void learnta::TimedCondition::restrictUpperBound	(	std::size_t	i,
		std::size_t	j,
		Bounds	upperBound,
		bool	force = `false`
	)

inline

Restrict the upper bound of \(\tau_i + \tau_{i+1} + \dots \tau_{j} \).

Postcondition: zone is canonical

◆ toGuard()

std::vector<Constraint> learnta::TimedCondition::toGuard ( ) const

inline

@breif Construct a guard over \({x_0, x_1,\dots,x_N}\) such that \(x_i = \mathbb{T}_{i,N}\).

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

include/timed_condition.hh

Public Member Functions

Static Public Member Functions

Protected Member Functions

Protected Attributes

Friends

Detailed Description

Constructor & Destructor Documentation

◆ TimedCondition()

Member Function Documentation

◆ applyResets()

◆ enumerate() [1/2]

◆ enumerate() [2/2]

◆ getStrictlyConstrainedVariables()

◆ hasEqualityN()

◆ isSimple()

◆ juxtaposeLeft()

◆ juxtaposeRight()

◆ makeExact()

◆ operator+()

◆ operator^()

◆ restrictLowerBound()

◆ restrictUpperBound()

◆ toGuard()