A timed automaton. More...

#include <timed_automaton.hh>

Inheritance diagram for learnta::TimedAutomaton:

Collaboration diagram for learnta::TimedAutomaton:

Public Member Functions
void	deepCopy (TimedAutomaton &dest, std::unordered_map< TAState *, std::shared_ptr< TAState >> &old2new) const
	make a deep copy of this timed automaton. More...

size_t	clockSize () const
	Returns the number of clock variables used in the timed automaton.

TimedAutomaton	complement (const std::vector< Alphabet > &alphabet) const
	Take the complement of this timed automaton. More...

void	makeComplete (const std::vector< Alphabet > &alphabet)
	Add transitions to make it complete.

TimedAutomaton	mergeAdjacentTransitions ()
	simplify the transitions by reducing the duplications

void	simplifyTransitions ()
	simplify the transitions by reducing the duplications

void	removeTriviallyUnreachableStates ()
	Remove the transitions that are unreachable from the initial states abstracting the timing constraints.

void	removeDeadLoop ()
	Remove self loop of non-accepting locations.

void	removeTriviallyDeadStates ()
	Remove trivially dead states, i.e., unreachable to any of the accepting states as a graph.

TimedAutomaton	removeUselessTransitions ()
	Remove self loop of non-accepting locations.

void	removeUnusedClockVariables ()
	Optimize the timed automaton by removing unused clock variables.

TimedAutomaton	simplify ()
	Simplify the timed automaton.

TimedAutomaton	simplifyStrong ()
	Simplify the timed automaton. More...

TimedAutomaton	simplifyWithZones ()
	Simplify the timed automaton. More...

bool	deterministic () const

void	addUpperBoundForUnobservableTransitions ()

Public Member Functions inherited from learnta::Automaton< TAState >
std::size_t	stateSize () const
	Returns the number of the states.

bool	operator== (const Automaton< TAState > &A) const
	Check the equivalence of two automata.

Static Public Member Functions
static std::vector< int >	makeMaxConstants (const std::vector< std::shared_ptr< TAState >> &states)
	Make a vector showing maximum constants for each variable from a set of states.

Public Attributes
std::vector< int >	maxConstraints
	The maximum constraints for each clock variables.

Public Attributes inherited from learnta::Automaton< TAState >
std::vector< std::shared_ptr< TAState > >	states
	The states of this automaton.

std::vector< std::shared_ptr< TAState > >	initialStates
	The initial states of this automaton.

Detailed Description

A timed automaton.

Member Function Documentation

◆ complement()

TimedAutomaton learnta::TimedAutomaton::complement ( const std::vector< Alphabet > & alphabet ) const

inline

Take the complement of this timed automaton.

Precondition: This timed automaton is deterministic and the transitions are complete

◆ deepCopy()

void learnta::TimedAutomaton::deepCopy	(	TimedAutomaton &	dest,
		std::unordered_map< TAState *, std::shared_ptr< TAState >> &	old2new
	)		const

inline

make a deep copy of this timed automaton.

Parameters

[out]	dest	The destination of the deep copy.
[out]	old2new	The mapping from the original state to the corresponding new state.

◆ simplifyStrong()

TimedAutomaton learnta::TimedAutomaton::simplifyStrong ( )

inline

Simplify the timed automaton.

This function may make the resulting TA incomplete.

◆ simplifyWithZones()

TimedAutomaton learnta::TimedAutomaton::simplifyWithZones ( )

Simplify the timed automaton.

This function uses zone graph to remove useless states and transitions.

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

include/timed_automaton.hh
src/timed_automaton.cc

Public Member Functions

Static Public Member Functions

Public Attributes

Detailed Description

Member Function Documentation

◆ complement()

◆ deepCopy()

◆ simplifyStrong()

◆ simplifyWithZones()