learnta::Zone Struct Reference

Implementation of a zone with DBM. More...

#include <zone.hh>

Inheritance diagram for learnta::Zone:

Public Member Functions
	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...

Static Public Member Functions
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
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

Implementation of a zone with DBM.

Note

internally, the variable 0 is used for the constant while externally, the actual clock variable is 0 origin, i.e., the variable 0 for the user is the variable 1 internally. So, we need increment or decrement to fill the gap.

Member Function Documentation

elapse()

void learnta::Zone::elapse ( )

inline

Assign the strongest post-condition of the delay.

Note

We allow time elapse of duration zero

equalIgnoreZero()

bool learnta::Zone::equalIgnoreZero ( Zone  z ) const

inline

Check the equivalence of two zones.

Note

We do not assume that the diagonal elements are equal.

extrapolate()

void learnta::Zone::extrapolate ( )

inline

Extrapolate the zone using the diagonal extrapolation based on maximum constants.

See [Behrmann+, TACAS'04] for the detail.

Note

We are currently using this simple extrapolation for simplicity. If we need more speed, we will consider using more sophisticated methods, e.g., LU extrapolation.

getNumOfVar()

std::size_t learnta::Zone::getNumOfVar ( ) const

inlinenoexcept

Returns the number of the variables represented by this zone

Returns

the number of the variables

includes()

bool learnta::Zone::includes ( const Zone &  zone ) const

inline

Return if this zone includes the given zone.

Precondition

both this and the given zones are canonized

isSatisfiableNoCanonize()

bool learnta::Zone::isSatisfiableNoCanonize ( ) const

inline

check if the zone is satisfiable

Precondition

The zone is canonical

operator==()

bool learnta::Zone::operator== ( const Zone &  z ) const

inline

Check the equivalence of two zones.

Note

We assume that the diagonal elements are equal.

reverseElapse()

void learnta::Zone::reverseElapse ( )

inline

Assign the weakest pre-condition of the delay.

Note

We allow time elapse of duration zero

Since clock variables cannot be negative, SAT(elapsed(Z) && Z') does not imply SAT(Z && reverseElapsed(Z'))

revertResets()

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

inline

Make it the weakest precondition of the reset.

In addition to unconstrain the updated variables, we use the renaming information

strictEqual()

bool learnta::Zone::strictEqual ( Zone  z ) const

inline

Check the equivalence of two zones.

Note

We do not assume that the diagonal elements are equal.

---

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

• include/zone.hh