learnta::SymbolicRun Class Reference

Run of a zone automaton. More...

#include <symbolic_run.hh>

Public Member Functions
	SymbolicRun (const std::shared_ptr< ZAState > &initialState)
void	push_back (const learnta::TATransition &transition, char action, const std::shared_ptr< ZAState > &state)
	Push a new edge and state in the end of the run.
std::shared_ptr< ZAState >	stateAt (int i) const
	Returns the i-th state in the symbolic run.
learnta::TATransition	edgeAt (int i) const
	Returns the i-th edge in the symbolic run.
learnta::Zone	tightZoneAt (int i) const
std::shared_ptr< ZAState >	back () const
	Returns the last state in the symbolic run.
std::optional< TimedWord >	reconstructWord () const
	Reconstruct a timed word from a symbolic run. More...
bool	validate (const std::vector< double > &durations) const
	Check if the given list of durations is consistent with the symbolic run.

Static Public Member Functions
static std::ostream &	print (std::ostream &os, const learnta::SymbolicRun &run)
	Print the symbolic run.

Detailed Description

Run of a zone automaton.

See also

ZoneAutomaton

Member Function Documentation

reconstructWord()

std::optional<TimedWord> learnta::SymbolicRun::reconstructWord ( ) const

inline

Reconstruct a timed word from a symbolic run.

We use the reconstruction algorithm in [Andre+, NFM'22]. Due to the state merging in the zone construction, the reconstruction may fail. We note that our zone construction is state –time_elapse--> intermediate –discrete_jump--> next_state.

---

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

• include/symbolic_run.hh