Inheritance diagram for IntermediateZone:

Collaboration diagram for IntermediateZone:

Public Member Functions
	IntermediateZone (const Interval &interval)
	construct an intermediate zone from an interval

	IntermediateZone (Zone zone, std::size_t currentNewestClock=0)
	construct an intermediate zone from a zone More...

ClockVariables	alloc (const std::pair< double, bool > &upperBound, const std::pair< double, bool > &lowerBound)

void	update (const std::vector< boost::variant< double, ClockVariables >> &resetTime)

void	toAns (Zone &ansZone) const

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

void	tighten (const ClockVariables x, const Constraint &c, const ClockVariables reset=0)

void	tighten (const ClockVariables x, const Constraint &c, const double t)

void	tighten (const std::vector< Constraint > &constraints, const std::vector< boost::variant< double, ClockVariables >> &resetTime)

void	tighten (const std::vector< Constraint > &constraints, const std::vector< boost::variant< double, ClockVariables >> &resetTime, const double t)

bool	isSatisfiableCanonized ()

void	deallocate (const ClockVariables x)

Public Member Functions inherited from Zone
std::size_t	getNumOfVar () const noexcept

void	cutVars (std::shared_ptr< Zone > &out, std::size_t from, std::size_t to)

std::tuple< std::vector< Bounds >, Bounds >	toTuple () const

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

void	close1 (ClockVariables x)

void	reset (ClockVariables x)

void	elapse ()

void	canonize ()

bool	isSatisfiable ()

void	abstractize ()

void	makeUnsat ()
	make the zone unsatisfiable

std::vector< Constraint >	makeGuard ()
	make the strongest guard including the zone

bool	operator== (Zone z) const

void	intersectionAssign (Zone z)

Public Attributes
ClockVariables	newestClock

std::vector< Interval >	intervals

bool	useInterval

Public Attributes inherited from Zone
Eigen::Matrix< Bounds, Eigen::Dynamic, Eigen::Dynamic >	value

Bounds	M

Additional Inherited Members
Public Types inherited from Zone
using	Tuple = std::tuple< std::vector< Bounds >, Bounds >

Static Public Member Functions inherited from Zone
static Zone	zero (int size)

static Zone	universal (int size)

Constructor & Destructor Documentation

◆ IntermediateZone()

IntermediateZone::IntermediateZone	(	Zone	zone,
		std::size_t	currentNewestClock = `0`
	)

inline

construct an intermediate zone from a zone

x0 is the special constant variable (x0 == 0) as usual. When x1, the trimming starts and the last variable is the newest one.

Member Function Documentation

◆ alloc()

ClockVariables IntermediateZone::alloc	(	const std::pair< double, bool > &	upperBound,
		const std::pair< double, bool > &	lowerBound
	)

inline

Note: lowerBound is not a bound but a cell in DBM

Note: this allocation is expected to be avoided by preallocation; Eigen's resize changes the value.

◆ tighten()

void IntermediateZone::tighten	(	const ClockVariables	x,
		const ClockVariables	y,
		Bounds	c
	)

inline

add the constraint x - y \le (c,s)

Note: This is different from Zone::tighten because we have to handle x0, too. That is unnecessary and harmful in zone construction.

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

intermediate_zone.hh

Public Member Functions

Public Attributes

Additional Inherited Members

Constructor & Destructor Documentation

◆ IntermediateZone()

Member Function Documentation

◆ alloc()

◆ tighten()