be.ac.umons.jsonlearning

Interface IVPDAJSONEquivalenceOracle

All Superinterfaces:

de.learnlib.api.oracle.EquivalenceOracle<net.automatalib.automata.vpda.OneSEVPA<?,JSONSymbol>,JSONSymbol,Boolean>

All Known Implementing Classes:

VPDAJSONEquivalenceOracle, VPDAJSONEquivalenceOracle

public interface IVPDAJSONEquivalenceOracle
extends de.learnlib.api.oracle.EquivalenceOracle<net.automatalib.automata.vpda.OneSEVPA<?,JSONSymbol>,JSONSymbol,Boolean>

The common interface for equivalence oracles for VPDAs.

Author:

Gaëtan Staquet

Nested Class Summary

Nested Classes

Modifier and Type	Interface and Description
static class	IVPDAJSONEquivalenceOracle.CounterexampleWithRelations<L> The ReachabilityRelation and OnAcceptingPathRelation computed to construct a key graph, and a counterexample.

Nested classes/interfaces inherited from interface de.learnlib.api.oracle.EquivalenceOracle

de.learnlib.api.oracle.EquivalenceOracle.DFAEquivalenceOracle<I>, de.learnlib.api.oracle.EquivalenceOracle.MealyEquivalenceOracle<I,O>, de.learnlib.api.oracle.EquivalenceOracle.RestrictedAutomatonEquivalenceOracle<I>, de.learnlib.api.oracle.EquivalenceOracle.ROCAEquivalenceOracle<I>, de.learnlib.api.oracle.EquivalenceOracle.VCAEquivalenceOracle<I>

Method Summary

Modifier and Type	Method and Description
default <L1,L2> IVPDAJSONEquivalenceOracle.CounterexampleWithRelations<L2>	counterexampleAndRelationFromKeyGraph(net.automatalib.automata.vpda.OneSEVPA<L1,JSONSymbol> previousHypothesis, ReachabilityRelation<L1> previousReachabilityRelation, OnAcceptingPathRelation<L1> previousOnAcceptingPathRelation, net.automatalib.automata.vpda.OneSEVPA<L2,JSONSymbol> currentHypothesis) Constructs the key graph for the hypothesis by reusing information computed at the previous equivalence query and, if it is invalid, provides a counterexample.
default <L> IVPDAJSONEquivalenceOracle.CounterexampleWithRelations<L>	counterexampleAndRelationFromKeyGraph(net.automatalib.automata.vpda.OneSEVPA<L,JSONSymbol> hypo) Constructs the key graph for the hypothesis and, if it is invalid, provides a counterexample.
default <L> de.learnlib.api.query.DefaultQuery<JSONSymbol,Boolean>	counterexampleByLoopingOverInitial(net.automatalib.automata.vpda.OneSEVPA<L,JSONSymbol> hypo, Random random) If there is a loop over the initial location reading an internal symbol, we can construct a counterexample by concatenating the symbol with a word that is accepted by the hypothesis.
default <L> de.learnlib.api.query.DefaultQuery<JSONSymbol,Boolean>	counterexampleFromKeyGraph(net.automatalib.automata.vpda.OneSEVPA<L,JSONSymbol> hypo) Constructs the key graph for the hypothesis and, if it is invalid, provides a counterexample.

Methods inherited from interface de.learnlib.api.oracle.EquivalenceOracle

findCounterExample

Method Detail

counterexampleByLoopingOverInitial

@Nullable
default <L> de.learnlib.api.query.DefaultQuery<JSONSymbol,Boolean> counterexampleByLoopingOverInitial(net.automatalib.automata.vpda.OneSEVPA<L,JSONSymbol> hypo,
                                                                                                                Random random)

If there is a loop over the initial location reading an internal symbol, we can construct a counterexample by concatenating the symbol with a word that is accepted by the hypothesis.

Since the resulting word starts by a symbol that is not {, it must actually be rejected.

Type Parameters:

L - Location type

Parameters:

hypo - The hypothesis

random - The random generator

Returns:

A counterexample, or null

counterexampleFromKeyGraph

@Nullable
default <L> de.learnlib.api.query.DefaultQuery<JSONSymbol,Boolean> counterexampleFromKeyGraph(net.automatalib.automata.vpda.OneSEVPA<L,JSONSymbol> hypo)

Constructs the key graph for the hypothesis and, if it is invalid, provides a counterexample.

Type Parameters:

L - Location type

Parameters:

hypo - The hypothesis

Returns:

A counterexample, or null

See Also:

KeyGraph.getWitnessInvalid()

counterexampleAndRelationFromKeyGraph

default <L> IVPDAJSONEquivalenceOracle.CounterexampleWithRelations<L> counterexampleAndRelationFromKeyGraph(net.automatalib.automata.vpda.OneSEVPA<L,JSONSymbol> hypo)

Constructs the key graph for the hypothesis and, if it is invalid, provides a counterexample. In all cases, also returns the computed relations.

Type Parameters:

L - Location type

Parameters:

hypo - The hypothesis

Returns:

The relations, alongside a counterexample. The counterexample may be null.

See Also:

KeyGraph.getWitnessInvalid()

counterexampleAndRelationFromKeyGraph

default <L1,L2> IVPDAJSONEquivalenceOracle.CounterexampleWithRelations<L2> counterexampleAndRelationFromKeyGraph(net.automatalib.automata.vpda.OneSEVPA<L1,JSONSymbol> previousHypothesis,
                                                                                                                 ReachabilityRelation<L1> previousReachabilityRelation,
                                                                                                                 OnAcceptingPathRelation<L1> previousOnAcceptingPathRelation,
                                                                                                                 net.automatalib.automata.vpda.OneSEVPA<L2,JSONSymbol> currentHypothesis)

Constructs the key graph for the hypothesis by reusing information computed at the previous equivalence query and, if it is invalid, provides a counterexample. In all cases, also returns the computed relations.

Type Parameters:

L1 - Previous hypothesis location type

L2 - Current hypothesis location type

Parameters:

previousHypothesis - The previous hypothesis

previousReachabilityRelation - The reachability relation for the previous hypothesis

previousOnAcceptingPathRelation - The Z_A relation for the previous hypothesis

currentHypothesis - The current hypothesis

Returns:

The new relations, alongside a counterexample. The counterexample may be null.