learnta::TAState Struct Reference

A state of timed automata. More...

#include <timed_automaton.hh>

Public Member Functions
	TAState (bool isMatch=false)
	TAState (bool isMatch, std::unordered_map< Alphabet, std::vector< TATransition >> next)
bool	deterministic () const
	Check if the transitions is deterministic. More...
void	addUpperBoundForUnobservableTransitions ()
void	removeTransitionsWithWeakerGuards ()
	Remove transitions with weaker guards if they have the same target. More...
void	mergeNondeterministicBranchingWithSameTarget ()
bool	needSplitting () const
	Check if there is a non-deterministic branching due to different set of imprecise clocks.
void	mergeNondeterministicBranching ()
	Make it deterministic by merging transitions. More...
void	mergeNondeterministicBranching (const std::unordered_set< ClockVariables > &preciseClocks)
	Make it deterministic by merging transitions. More...

Public Attributes
bool	isMatch
	The value is true if and only if the state is an accepting state.
std::unordered_map< Alphabet, std::vector< TATransition > >	next
	A mapping of a character to the transitions. More...

Detailed Description

A state of timed automata.

Member Function Documentation

deterministic()

bool learnta::TAState::deterministic

(

)

const

Check if the transitions is deterministic.

Check if the outgoing transitions are deterministic.

mergeNondeterministicBranching() [1/2]

void learnta::TAState::mergeNondeterministicBranching

(

)

Make it deterministic by merging transitions.

This is intended to be used to merge the transitions generated by guard relaxation.

mergeNondeterministicBranching() [2/2]

void learnta::TAState::mergeNondeterministicBranching

(

const std::unordered_set< ClockVariables > &

preciseClocks

)

Make it deterministic by merging transitions.

This is intended to be used to merge the transitions generated by guard relaxation.

removeTransitionsWithWeakerGuards()

void learnta::TAState::removeTransitionsWithWeakerGuards

(

)

Remove transitions with weaker guards if they have the same target.

This is intended to be used to remove the redundant transitions due to the guard relaxation.

Member Data Documentation

next

std::unordered_map<Alphabet, std::vector<TATransition> > learnta::TAState::next

A mapping of a character to the transitions.

Note

Because of non-determinism, the second element is a vector.

---

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

• include/timed_automaton.hh
• src/timed_automaton.cc