A zone constructed by juxtaposing two zones with or without shared variables. More...

#include <juxtaposed_zone.hh>

Inheritance diagram for learnta::JuxtaposedZone:

Collaboration diagram for learnta::JuxtaposedZone:

Public Member Functions
	JuxtaposedZone (const Zone &left, const Zone &right)
	Juxtapose two zones without shared variables. More...

	JuxtaposedZone (const Zone &left, const Zone &right, Eigen::Index commonVariableSize)
	Juxtapose two zones with shared variables. More...

void	addRenaming (const std::vector< std::pair< std::size_t, std::size_t >> &renaming)
	Add renaming constraints. More...

auto	makeRenaming () const
	Make renaming constraints.

Zone	getRight () const
	Return the right side zone. More...

Eigen::Index	getLeftSize () const

Public Member Functions inherited from learnta::Zone
	Zone (const Eigen::Matrix< Bounds, Eigen::Dynamic, Eigen::Dynamic > &value)
	Construct a zone from a matrix representing the zone.

	Zone (Eigen::Matrix< Bounds, Eigen::Dynamic, Eigen::Dynamic > &&value)
	Construct a zone from a matrix representing the zone.

	Zone (Eigen::Matrix< Bounds, Eigen::Dynamic, Eigen::Dynamic > value, Bounds m)
	Construct a zone from a matrix representing the zone and the bound.

	Zone (const std::vector< double > &valuation, Bounds M)
	Construct a zone containing only the given valuation.

std::size_t	getNumOfVar () const noexcept

void	tighten (ClockVariables x, ClockVariables y, Bounds c)
	add the constraint \(x - y \le (c,s)\)

void	tighten (const Constraint &constraint)
	Add a guard of a timed automaton.

void	tighten (const std::vector< Constraint > &constraints)
	Add a set of guards of a timed automaton.

void	applyResets (const std::vector< std::pair< ClockVariables, std::variant< double, ClockVariables >>> &resets)

void	revertResets (const std::vector< std::pair< ClockVariables, std::variant< double, ClockVariables >>> &resets)
	Make it the weakest precondition of the reset. More...

Zone	operator&& (const Zone &another) const
	Returns the intersection of two zones.

Zone	operator&= (const Zone &another)
	Assign the intersection of two zones.

Zone	operator^ (const Zone &another) const
	Returns the juxtaposition of two zones.

std::vector< double >	sample ()
	Return a clock valuation in this zone.

void	close1 (ClockVariables x)
	Close using only x.

void	reset (ClockVariables x)
	Assign a constant value to the clock variable x.

void	unconstrain (ClockVariables x)
	Unconstrain the constraint on this clock.

void	elapse ()
	Assign the strongest post-condition of the delay. More...

void	reverseElapse ()
	Assign the weakest pre-condition of the delay. More...

void	canonize ()
	make the zone canonical

bool	isSatisfiable ()
	check if the zone is satisfiable

bool	isSatisfiableNoCanonize () const
	check if the zone is satisfiable More...

	operator bool ()
	check if the zone is satisfiable

void	abstractize ()
	truncate the constraints compared with a constant greater than or equal to M

void	extrapolate ()
	Extrapolate the zone using the diagonal extrapolation based on maximum constants. More...

void	makeUnsat ()
	make the zone unsatisfiable

bool	includes (const Zone &zone) const
	Return if this zone includes the given zone. More...

bool	operator== (const Zone &z) const
	Check the equivalence of two zones. More...

bool	equalIgnoreZero (Zone z) const
	Check the equivalence of two zones. More...

bool	strictEqual (Zone z) const
	Check the equivalence of two zones. More...

Additional Inherited Members
Static Public Member Functions inherited from learnta::Zone
static Zone	zero (int size)
	Make the zone of size `size` such that all the values are zero.

static Zone	top (std::size_t size)
	Make the zone of size `size` with no constraints.

Public Attributes inherited from learnta::Zone
Eigen::Matrix< Bounds, Eigen::Dynamic, Eigen::Dynamic >	value
	The matrix representing the DBM.

Bounds	M
	The threshold for the normalization.

std::vector< double >	maxConstraints
	the threshold of each clock variable

Detailed Description

A zone constructed by juxtaposing two zones with or without shared variables.

Constructor & Destructor Documentation

◆ JuxtaposedZone() [1/2]

learnta::JuxtaposedZone::JuxtaposedZone	(	const Zone &	left,
		const Zone &	right
	)

inline

Juxtapose two zones without shared variables.

Let \(x_1, x_2, \dots, x_N\) be the variables in left and \(y_1, y_2, \dots, y_M\) be the variables in right. The variables \(z_1, z_2, \dots, z_{N + M}\) in the resulting zone is such that

\(x_i = z_i\) if \(1 \le i \le N\) and
\(y_{i - N} = z_i\) if \(N + 1 \le i \le N + M\).

◆ JuxtaposedZone() [2/2]

learnta::JuxtaposedZone::JuxtaposedZone	(	const Zone &	left,
		const Zone &	right,
		Eigen::Index	commonVariableSize
	)

inline

Juxtapose two zones with shared variables.

Let \(x_1, x_2, \dots, x_N\) be the variables in left and \(y_1, y_2, \dots, y_M\) be the variables in right. Let \(L\) be the size of the variables common in left and right, i.e., \(x_{N - L + 1} = y_{M - L + 1}, \dots, x_N = y_M\). The variables \(z_1, z_2, \dots, z_{N + M}\) in the resulting zone is such that

\(x_i = z_i\) if \(1 \le i \le N\) and
\(y_{i - M} = z_i\) if \(N + 1 \le i \le N + M - L\).

Member Function Documentation

◆ addRenaming()

void learnta::JuxtaposedZone::addRenaming ( const std::vector< std::pair< std::size_t, std::size_t >> & renaming )

inline

Add renaming constraints.

Parameters

renaming The renaming relation to be added

Precondition: for any (left, right) \in renaming, we have 0 <= left < leftSize and 0 <= right < rightSize; The zone is canonized

Postcondition: The zone is canonized

◆ getRight()

Zone learnta::JuxtaposedZone::getRight ( ) const

inline

Return the right side zone.

Precondition: There is no common variables

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

include/juxtaposed_zone.hh

Public Member Functions

Additional Inherited Members

Detailed Description

Constructor & Destructor Documentation

◆ JuxtaposedZone() [1/2]

◆ JuxtaposedZone() [2/2]

Member Function Documentation

◆ addRenaming()

◆ getRight()