Classes
class	ExperimentRunner

class	OtaJsonParser
	Parser of one clock TAs in the json format of https://github.com/Leslieaj/OTALearning. More...

class	BackwardRegionalElementaryLanguage
	A back regional elementary language. More...

struct	Automaton
	An automaton. More...

struct	Constraint
	A constraint in a guard of transitions. More...

class	ConstraintMaker

class	ElementaryLanguage
	An elementary language. More...

class	EquivalenceOracleChain
	A chain of the equivalence oracles. More...

class	EquivalenceOracle
	Interface of the equivalence oracle. More...

class	EquivalenceOracleByRandomTest
	The equivalence oracle by random test. More...

class	EquivalenceOracleByTest
	Interface of the equivalence oracle. More...

class	EquivalenceOracleMemo
	Wrapper of an equivalence oracle to cache the queries. More...

class	ExternalTransitionMaker
	A class to make a transition from P to ext(P) More...

class	ForwardRegionalElementaryLanguage
	A forward regional elementary language. More...

class	FractionalOrder
	Order on the fractional part of the variables. More...

class	ImpreciseClockHandler
	Relax guards to handle imprecise clock variables. More...

class	InternalTransitionMaker
	A class to make a transition from P to P. More...

class	JuxtaposedZone
	A zone constructed by juxtaposing two zones with or without shared variables. More...

class	JuxtaposedZoneSet

class	Learner
	The deterministic timed automata learner. More...

class	MembershipOracle
	Interface of a membership oracle. More...

class	SULMembershipOracle
	Membership oracle defined by an SUL. More...

class	MembershipOracleCache
	Wrapper of a membership oracle to cache the result. More...

class	NeighborConditions
	Elementary language with its neighbor conditions. More...

class	ObservationTable
	Timed observation table. More...

class	RecognizableLanguage
	Recognizable timed language in [MP04]. More...

class	RenamingRelation

class	SingleMorphism
	Morphism from an external elementary language to an internal one. More...

class	SUL
	Interface of the system under learning. More...

class	SymbolicMembershipOracle
	The oracle to answer symbolic membership queries. More...

class	SymbolicRun
	Run of a zone automaton. More...

class	ComplementTimedAutomataEquivalenceOracle
	Equivalence oracle with a timed automaton recognizing the complement of the target language. More...

struct	TAState
	A state of timed automata. More...

struct	TATransition
	A state of timed automata. More...

struct	TimedAutomaton
	A timed automaton. More...

class	TimedAutomatonRunner
	Class to execute a timed automaton. More...

class	TimedCondition
	A timed condition, a finite conjunction of inequalities of the form \(\tau_{i} + \tau_{i + 1} \dots \tau_{j} \bowtie c\), where \({\bowtie} \in \{>,\ge,\le,<\}\) and \(c \in \mathbb{N} \). More...

class	TimedConditionSet
	A set of timed conditions to represent non-convex constraints. More...

class	TimedWord
	A timed word. More...

struct	Zone
	Implementation of a zone with DBM. More...

struct	ZoneAutomaton
	A Zone automaton. More...

struct	ZAState
	A state of a zone automaton. More...

struct	ManualEqTester

Typedefs
using	Bounds = std::pair< double, bool >

typedef char	Alphabet

typedef uint8_t	ClockVariables

using	IntBounds = std::pair< int, bool >

using	RenamingGraph = std::pair< std::vector< std::vector< std::size_t > >, std::vector< std::vector< std::size_t > >>

Enumerations
enum class	Order { LT , EQ , GT }
	The return values of comparison of two values. Similar to strcmp.

enum class	CellStatus { bottom , top , middle }
	The status of a cell of the observation table. More...

Functions
static std::ostream &	operator<< (std::ostream &os, const learnta::BackwardRegionalElementaryLanguage &lang)

std::size_t	hash_value (learnta::BackwardRegionalElementaryLanguage const &lang)

static bool	isPoint (const Bounds &upperBound, const Bounds &lowerBound)
	Check if the upper and lower bounds define a point.

static bool	isUnitOpen (const Bounds &upperBound, const Bounds &lowerBound)

static bool	isSimple (const Bounds &upperBound, const Bounds &lowerBound)

static std::ostream &	print (std::ostream &os, const learnta::Bounds &b)

static std::ostream &	print (std::ostream &os, learnta::Bounds &&b)

template<class T >
bool	is_ascending (const std::vector< T > &container)
	Check if the elements are sorted in the ascending order.

template<class T >
bool	is_strict_ascending (const std::vector< T > &container)
	Check if the elements are sorted in the strict ascending order.

template<class T , class U >
T	first (const std::pair< T, U > &pair)
	Return the first element of a pair.

template<class T , class U >
U	second (const std::pair< T, U > &pair)
	Return the second element of a pair.

template<class T , class U >
auto	is_first (const T &value)
	Return a function checking if the first element equal to the given value.

template<class T , class U >
auto	is_second (const U &value)
	Return a function checking if the second element equal to the given value.

bool	toBool (Order odr)

int	orderToInt (learnta::Constraint::Order order)

std::size_t	hash_value (const Constraint guard)

static bool	isWeaker (const std::vector< Constraint > &left, const std::vector< Constraint > &right)

static std::ostream &	operator<< (std::ostream &os, const Constraint::Order &odr)

static std::ostream &	operator<< (std::ostream &os, const Constraint &p)

static void	widen (std::vector< Constraint > &guard)
	remove any inequality x > c or x >= c

std::vector< Constraint >	negateAll (const std::vector< Constraint > &constraints)

std::vector< Constraint >	conjunction (const std::vector< Constraint > &left, const std::vector< Constraint > &right)

auto	toBounds (const std::vector< Constraint > &constraints)

std::vector< ClockVariables >	simpleVariables (const std::vector< Constraint > &constraints)
	Return the variables that are bounded by a simple constraint, i.e., c < x < c + 1 or x = c. More...

bool	satisfiable (const std::vector< Constraint > &constraints)

std::vector< Constraint >	simplify (const std::vector< Constraint > &constraints)

Bounds	lowerBoundDurationToSatisfy (const std::vector< Constraint > &guard, const std::vector< double > &valuation)

static std::ostream &	operator<< (std::ostream &os, const std::vector< Constraint > &guards)

std::vector< std::vector< Constraint > >	negate (const std::vector< std::vector< Constraint >> &dnfConstraints)

static auto	unionHull (const std::vector< std::vector< Constraint >> &guards)
	Return the strongest guard that is weaker than all of the given guards.

static auto	unionHull (const std::vector< Constraint > &left, const std::vector< Constraint > &right)
	Return the strongest guard that is weaker than the given guards.

void	addUpperBound (std::vector< Constraint > &guard)

static bool	adjacent (const std::vector< Constraint > &left, const std::vector< Constraint > &right)
	Check if two guards are adjacent.

static std::optional< TimedWord >	analyzeCEX (const TimedWord &word, MembershipOracle &oracle, const RecognizableLanguage &hypothesis, const std::vector< BackwardRegionalElementaryLanguage > &currentSuffixes={})
	Rivest-Schapire-style counterexample analysis. More...

std::ostream &	operator<< (std::ostream &os, const ElementaryLanguage &language)

std::size_t	hash_value (learnta::ElementaryLanguage const &lang)

static bool	equivalence (const ElementaryLanguage &left, const std::vector< TimedConditionSet > &leftRow, const ElementaryLanguage &right, const std::vector< TimedConditionSet > &rightRow, const std::vector< BackwardRegionalElementaryLanguage > &suffixes, const RenamingRelation &renaming)
	Return if two elementary languages are equivalent. More...

static bool	equivalence (const ElementaryLanguage &left, const std::vector< TimedConditionSet > &leftRow, const std::vector< TimedCondition > &leftConcatenation, const ElementaryLanguage &right, const std::vector< TimedConditionSet > &rightRow, const std::vector< TimedCondition > &rightConcatenation, const std::vector< BackwardRegionalElementaryLanguage > &suffixes, const RenamingRelation &renaming)
	Return if two elementary languages are equivalent. More...

static bool	equivalence (JuxtaposedZone leftRightJuxtaposition, const std::vector< JuxtaposedZoneSet > &leftJuxtapositions, const std::vector< JuxtaposedZoneSet > &rightJuxtapositions, const RenamingRelation &renaming)
	Return if two elementary languages are equivalent. More...

static RenamingGraph	toGraph (const TimedCondition &left, const TimedCondition &right)
	Construct the intermediate bipartite graph for candidate generation from timed conditions. More...

static std::vector< RenamingRelation >	generateDeterministicCandidates (const TimedCondition &left, const TimedCondition &right, const std::vector< std::size_t > &leftConstrained, const std::vector< std::size_t > &rightConstrained, const RenamingGraph &graph)
	Construct candidate renaming relations that are deterministic, i.e., the corresponding reset only makes precise clocks. More...

static CellStatus	decideStatus (const TimedCondition &concatenation, const TimedConditionSet &cell)
	Compute the status of a cell of the observation table. More...

static std::pair< std::vector< std::size_t >, std::vector< std::size_t > >	makeConstrainedVariables (const std::vector< TimedConditionSet > &leftRow, const std::vector< TimedConditionSet > &rightRow, const std::vector< TimedCondition > &leftConcatenations, const std::vector< TimedCondition > &rightConcatenations, const std::size_t N, const std::size_t M)
	Return the constrained variables in the symbolic membership. More...

static std::optional< RenamingRelation >	findDeterministicEquivalentRenaming (const ElementaryLanguage &left, const std::vector< TimedConditionSet > &leftRow, const ElementaryLanguage &right, const std::vector< TimedConditionSet > &rightRow, const std::vector< BackwardRegionalElementaryLanguage > &suffixes)
	Return a renaming constraint if two elementary languages are equivalent. More...

static std::optional< RenamingRelation >	findDeterministicEquivalentRenaming (const ElementaryLanguage &left, const std::vector< TimedConditionSet > &leftRow, const std::vector< TimedCondition > &leftConcatenations, const ElementaryLanguage &right, const std::vector< TimedConditionSet > &rightRow, const std::vector< TimedCondition > &rightConcatenations, const std::vector< BackwardRegionalElementaryLanguage > &suffixes)
	Return a renaming constraint if two elementary languages are equivalent. More...

static std::optional< RenamingRelation >	findEquivalentRenaming (const ElementaryLanguage &left, const std::vector< TimedConditionSet > &leftRow, const ElementaryLanguage &right, const std::vector< TimedConditionSet > &rightRow, const std::vector< BackwardRegionalElementaryLanguage > &suffixes)
	Construct a renaming constraint if two elementary languages are equivalent. More...

static std::ostream &	operator<< (std::ostream &os, const learnta::ForwardRegionalElementaryLanguage &lang)

std::size_t	hash_value (learnta::ForwardRegionalElementaryLanguage const &lang)

static std::ostream &	operator<< (std::ostream &os, const learnta::FractionalOrder &order)

std::size_t	hash_value (learnta::FractionalOrder const &order)

void	intersectionTA (const TimedAutomaton &in1, const TimedAutomaton &in2, TimedAutomaton &out, boost::unordered_map< std::pair< TAState , TAState >, std::shared_ptr< TAState >> &toIState)

void	updateInitAccepting (const TimedAutomaton &in1, const TimedAutomaton &in2, TimedAutomaton &out, boost::unordered_map< std::pair< TAState , TAState >, std::shared_ptr< TAState >> toIState)

void	intersectionSignalTA (const TimedAutomaton &in1, const TimedAutomaton &in2, TimedAutomaton &out)

static std::ostream &	operator<< (std::ostream &os, const learnta::NeighborConditions &conditions)

static std::size_t	hash_value (const NeighborConditions &conditions)

static std::ostream &	operator<< (std::ostream &os, const learnta::SymbolicRun &run)
	Print the symbolic run.

void	ta2za (const TimedAutomaton &TA, ZoneAutomaton &ZA, bool quickReturn=true)
	Generate a zone automaton from a timed automaton. More...

std::size_t	hash_value (const TATransition &transition)

static std::ostream &	operator<< (std::ostream &os, const TimedAutomaton &TA)

static std::unordered_map< ClockVariables, std::variant< double, ClockVariables > >	asMap (const TATransition::Resets &resets)

static TATransition::Resets	composition (const TATransition::Resets &left, const TATransition::Resets &right)
	Construct the composition ( \(left \circ right\)) of the resets.

static TATransition::Resets	addDefault (const TATransition::Resets &original, const TATransition::Resets &defaultReset)

static TATransition::Resets	clean (const TATransition::Resets &resets)

static std::ostream &	print (std::ostream &os, const learnta::TimedCondition &cond)

static std::ostream &	operator<< (std::ostream &os, const learnta::TimedCondition &b)

std::size_t	hash_value (learnta::TimedCondition const &timedCondition)

static std::ostream &	print (std::ostream &os, const learnta::TimedWord &word)

static std::ostream &	operator<< (std::ostream &os, const learnta::TimedWord &word)

static std::size_t	hash_value (const TimedWord &word)

static std::ostream &	print (std::ostream &os, const learnta::Zone &zone)
	Print the zone.

static std::ostream &	operator<< (std::ostream &os, const learnta::Zone &zone)

std::size_t	hash_value (learnta::Zone const &zone)

std::vector< ClockVariables >	impreciseClocksAfterTransition (const TATransition &transition)
	Returns the imprecise clocks after transition.

TATransition	mergeTransitions (const TATransition &left, const TATransition &right)
	Merge two TATransitions. More...

Variables
const Alphabet	UNOBSERVABLE = 0

const auto	UNOBSERVABLE_STRING = "ε"

Detailed Description

Author: Masaki Waga

Date: 2022/09/09.

Author: Masaki Waga

Date: 2022/09/16.

Author: Masaki Waga

Date: 2022/03/07.

Author: Masaki Waga

Date: 2022/03/06.

Author: Masaki Waga

Date: 2023/01/20.

Author: Masaki Waga

Date: 2022/11/30.

Author: Masaki Waga

Date: 2022/03/04.

Author: Masaki Waga

Date: 2022/03/31.

Author: Masaki Waga

Date: 2022/03/15.

Author: Masaki Waga

Date: 2022/09/20.

Author: Masaki Waga

Date: 2022/03/27.

Author: Masaki Waga

Date: 2022/03/05.

Author: Masaki Waga

Date: 2023/01/10.

Author: Masaki Waga

Date: 2022/09/14.

Author: Masaki Waga

Date: 2022/03/13.

Author: Masaki Waga

Date: 2022/03/20.

Author: Masaki Waga

Date: 2022/11/29.

Author: Masaki Waga

Date: 2022/12/29.

Author: Masaki Waga

Date: 2022/11/03.

Author: Masaki Waga

Date: 2022/03/21.

Author: Masaki Waga

Date: 2022/11/01.

Author: Masaki Waga

Date: 2022/12/23.

Author: Masaki Waga

Date: 2022/09/04.

Author: Masaki Waga

Date: 2022/04/02.

Enumeration Type Documentation

◆ CellStatus

enum learnta::CellStatus

strong

The status of a cell of the observation table.

CellStatus::bottom: \(mem(p \cdot s) = \bot\)
CellStatus::top: \(mem(p \cdot s) = \top\)
CellStatus::middle: otherwise

Function Documentation

◆ analyzeCEX()

static std::optional<TimedWord> learnta::analyzeCEX	(	const TimedWord &	word,
		MembershipOracle &	oracle,
		const RecognizableLanguage &	hypothesis,
		const std::vector< BackwardRegionalElementaryLanguage > &	currentSuffixes = `{}`
	)

inlinestatic

Rivest-Schapire-style counterexample analysis.

Parameters

[in]	word	The analyzed counterexample
[in]	oracle	The membership oracle
[in]	hypothesis	The hypothesis recognizable language

Precondition: word is a counterexample. Namely, we should have oracle->answerQuery(word) != hypothesis.contains(word)

◆ decideStatus()

static CellStatus learnta::decideStatus	(	const TimedCondition &	concatenation,
		const TimedConditionSet &	cell
	)

inlinestatic

Compute the status of a cell of the observation table.

Precondition: If concatenation == cell, we have cell.size() == 1 and concatenation == cell.front()

◆ equivalence() [1/3]

static bool learnta::equivalence	(	const ElementaryLanguage &	left,
		const std::vector< TimedConditionSet > &	leftRow,
		const ElementaryLanguage &	right,
		const std::vector< TimedConditionSet > &	rightRow,
		const std::vector< BackwardRegionalElementaryLanguage > &	suffixes,
		const RenamingRelation &	renaming
	)

static

Return if two elementary languages are equivalent.

Precondition: leftRow.size() == rightRow.size() == suffixes.size()

◆ equivalence() [2/3]

static bool learnta::equivalence	(	const ElementaryLanguage &	left,
		const std::vector< TimedConditionSet > &	leftRow,
		const std::vector< TimedCondition > &	leftConcatenation,
		const ElementaryLanguage &	right,
		const std::vector< TimedConditionSet > &	rightRow,
		const std::vector< TimedCondition > &	rightConcatenation,
		const std::vector< BackwardRegionalElementaryLanguage > &	suffixes,
		const RenamingRelation &	renaming
	)

static

Return if two elementary languages are equivalent.

Precondition: leftRow.size() == rightRow.size() == suffixes.size()

◆ equivalence() [3/3]

static bool learnta::equivalence	(	JuxtaposedZone	leftRightJuxtaposition,
		const std::vector< JuxtaposedZoneSet > &	leftJuxtapositions,
		const std::vector< JuxtaposedZoneSet > &	rightJuxtapositions,
		const RenamingRelation &	renaming
	)

static

Return if two elementary languages are equivalent.

Parameters

leftRightJuxtaposition	juxtaposition of left and right prefixes
leftJuxtapositions	list of juxtaposition of mem(left + suffix) and (right + suffix)
rightJuxtapositions	list of juxtaposition of (left + suffix) and mem(right + suffix)

Precondition: leftJuxtapositions.size() == rightJuxtapositions.size()

◆ findDeterministicEquivalentRenaming() [1/2]

static std::optional<RenamingRelation> learnta::findDeterministicEquivalentRenaming	(	const ElementaryLanguage &	left,
		const std::vector< TimedConditionSet > &	leftRow,
		const ElementaryLanguage &	right,
		const std::vector< TimedConditionSet > &	rightRow,
		const std::vector< BackwardRegionalElementaryLanguage > &	suffixes
	)

inlinestatic

Return a renaming constraint if two elementary languages are equivalent.

The outline of our construction is as follows.

We construct the bipartite graph based on the timed conditions.
We generate deterministic candidate renaming equations
We return a renaming equation witnessing the equivalence, if exists

In the first part, we construct a bipartite graph \((V_1, V_2, E)\) such that:

\(V_1\) and \(V_2\) consists of the variables in left and right, respectively, and
\((v_1, v_2) \in E\) if and only if \(v_1 = v_2\) does not contradict to the given constraints.

We note that each disjoint part of this bipartite graph is complete.

Precondition: leftRow.size() == rightRow.size() == suffixes.size(); left and right are simple

◆ findDeterministicEquivalentRenaming() [2/2]

static std::optional<RenamingRelation> learnta::findDeterministicEquivalentRenaming	(	const ElementaryLanguage &	left,
		const std::vector< TimedConditionSet > &	leftRow,
		const std::vector< TimedCondition > &	leftConcatenations,
		const ElementaryLanguage &	right,
		const std::vector< TimedConditionSet > &	rightRow,
		const std::vector< TimedCondition > &	rightConcatenations,
		const std::vector< BackwardRegionalElementaryLanguage > &	suffixes
	)

inlinestatic

Return a renaming constraint if two elementary languages are equivalent.

The outline of our construction is as follows.

We construct the bipartite graph based on the timed conditions.
We generate deterministic candidate renaming equations
We return a renaming equation witnessing the equivalence, if exists

In the first part, we construct a bipartite graph \((V_1, V_2, E)\) such that:

\(V_1\) and \(V_2\) consists of the variables in left and right, respectively, and
\((v_1, v_2) \in E\) if and only if \(v_1 = v_2\) does not contradict to the given constraints.

We note that each disjoint part of this bipartite graph is complete.

Precondition: leftRow.size() == rightRow.size() == suffixes.size(); left and right are simple

◆ findEquivalentRenaming()

static std::optional<RenamingRelation> learnta::findEquivalentRenaming	(	const ElementaryLanguage &	left,
		const std::vector< TimedConditionSet > &	leftRow,
		const ElementaryLanguage &	right,
		const std::vector< TimedConditionSet > &	rightRow,
		const std::vector< BackwardRegionalElementaryLanguage > &	suffixes
	)

inlinestatic

Construct a renaming constraint if two elementary languages are equivalent.

The outline of our construction is as follows.

We construct the bipartite graph based on the timed conditions.
We make the set of the strictly constrained variables in the symbolic membership.
We generate a candidate of renaming constraints and return it if it witnesses the equivalence

In the first part, we construct a bipartite graph \((V_1, V_2, E)\) such that:

\(V_1\) and \(V_2\) consists of the variables in left and right, respectively, and
\((v_1, v_2) \in E\) if and only if \(v_1 = v_2\) does not contradict to the given constraints.

We note that each disjoint part of this bipartite graph is complete.

In the second part, we list the variables strictly constrained in the symbolic membership. We do this simply by comparing the coefficients in the zone thanks to the canonicity of the zones. Since these strictly constrained variables must also be constrained by the renaming constraints, they are the candidates in the construction of the renaming constraints.

In the third part, we construct the renaming constraints by taking the largest or smallest edges in each disjoint part of the bipartite graph.

Precondition: leftRow.size() == rightRow.size() == suffixes.size(); left and right are simple

◆ generateDeterministicCandidates()

static std::vector<RenamingRelation> learnta::generateDeterministicCandidates	(	const TimedCondition &	left,
		const TimedCondition &	right,
		const std::vector< std::size_t > &	leftConstrained,
		const std::vector< std::size_t > &	rightConstrained,
		const RenamingGraph &	graph
	)

inlinestatic

Construct candidate renaming relations that are deterministic, i.e., the corresponding reset only makes precise clocks.

Parameters

left	The left timed condition in the renaming
right	The right timed condition in the renaming
leftConstrained	The variables strictly constrained in mem(left ・ suffix)
rightConstrained	The variables strictly constrained in mem(right ・ suffix)
graph	The renaming graph

Precondition: leftConstrained and rightConstrained are strictly ascending.

◆ makeConstrainedVariables()

static std::pair<std::vector<std::size_t>, std::vector<std::size_t> > learnta::makeConstrainedVariables	(	const std::vector< TimedConditionSet > &	leftRow,
		const std::vector< TimedConditionSet > &	rightRow,
		const std::vector< TimedCondition > &	leftConcatenations,
		const std::vector< TimedCondition > &	rightConcatenations,
		const std::size_t	N,
		const std::size_t	M
	)

inlinestatic

Return the constrained variables in the symbolic membership.

Parameters

leftRow	mem(left ・ suffix)
rightRow	mem(right ・ suffix)
leftConcatenations	left ・ suffix
rightConcatenations	right ・ suffix
N	\|left\|
M	\|right\|

Returns: The constrained variables in strictly ascending order

◆ mergeTransitions()

TATransition learnta::mergeTransitions	(	const TATransition &	left,
		const TATransition &	right
	)

Merge two TATransitions.

The construction is as follows.

We basically use the transition with less imprecise clocks after it.
The target state and the reset is the ones of the above transition.
The guard is the union of the guards of the given transitions.

◆ simpleVariables()

std::vector<ClockVariables> learnta::simpleVariables ( const std::vector< Constraint > & constraints )

inline

Return the variables that are bounded by a simple constraint, i.e., c < x < c + 1 or x = c.

Returns: list of variables with simple bounds in the ascending order

◆ ta2za()

void learnta::ta2za	(	const TimedAutomaton &	TA,
		ZoneAutomaton &	ZA,
		bool	quickReturn = `true`
	)

Generate a zone automaton from a timed automaton.

Template Parameters

NVar	the number of variable in TA

TA to ZA adds states with BFS. Initial configuration is the initial states of ZA. The ZA contain only the states reachable from initial states.

number of states of ZA

Make initial state, that is Current configuration of BFS

translater from TAState and Zone to its corresponding state in ZA.

The type is like this. (TAState,Zone) -> ZAState

number of states of ZA

Make initial state, that is Current configuration of BFS

translater from TAState and Zone to its corresponding state in ZA.

The type is like this. (TAState,Zone) -> ZAState

◆ toGraph()

static RenamingGraph learnta::toGraph	(	const TimedCondition &	left,
		const TimedCondition &	right
	)

inlinestatic

Construct the intermediate bipartite graph for candidate generation from timed conditions.

The constructed graph has an edge between v1.at(i) and v2.at(j) if and only if left.getUpperBound(i, N - 1) == right.getUpperBound(j, M - 1)

Precondition: left and right are simple

Classes

Typedefs

Enumerations

Functions

Variables

Detailed Description

Enumeration Type Documentation

◆ CellStatus

Function Documentation

◆ analyzeCEX()

◆ decideStatus()

◆ equivalence() [1/3]

◆ equivalence() [2/3]

◆ equivalence() [3/3]

◆ findDeterministicEquivalentRenaming() [1/2]

◆ findDeterministicEquivalentRenaming() [2/2]

◆ findEquivalentRenaming()

◆ generateDeterministicCandidates()

◆ makeConstrainedVariables()

◆ mergeTransitions()

◆ simpleVariables()

◆ ta2za()

◆ toGraph()