Uses of Interface
net.automatalib.modelchecking.ModelChecker
-
Packages that use ModelChecker Package Description net.automatalib.modelchecker.ltsmin This package (and sub-packages) provides the integration of the model checker LTSmin as described in the paper Sound Black-Box Checking in the LearnLib by Jeroen Meijer and Jaco van de Pol.net.automatalib.modelchecker.ltsmin.ltl net.automatalib.modelchecker.ltsmin.monitor net.automatalib.modelchecker.m3c.solver net.automatalib.modelchecking -
-
Uses of ModelChecker in net.automatalib.modelchecker.ltsmin
Subinterfaces of ModelChecker in net.automatalib.modelchecker.ltsmin Modifier and Type Interface Description interface
LTSmin<I,A,R>
An LTSmin model checker.interface
LTSminAlternating<I,O,R>
A model checker using LTSmin for Mealy machines using alternating edge semantics.interface
LTSminDFA<I,R>
A model checker using LTSmin for DFAs.interface
LTSminIO<I,O,R>
A model checker using LTSmin for Mealy machines using synchronous edge semantics.interface
LTSminMealy<I,O,R>
A feature of thisModelChecker
, is that one can remove particular output symbols from the given MealyMachine hypothesis.Classes in net.automatalib.modelchecker.ltsmin that implement ModelChecker Modifier and Type Class Description class
AbstractLTSmin<I,A,R>
An LTL model checker using LTSmin. -
Uses of ModelChecker in net.automatalib.modelchecker.ltsmin.ltl
Classes in net.automatalib.modelchecker.ltsmin.ltl that implement ModelChecker Modifier and Type Class Description class
AbstractLTSminLTL<I,A,L extends Lasso<I,?>>
An LTSmin model checker for full LTL.class
AbstractLTSminLTLMealy<I,O>
An LTL model checker using LTSmin for Mealy machines.class
LTSminLTLAlternating<I,O>
An LTL model checker using LTSmin for Mealy machines using alternating edge semantics.class
LTSminLTLDFA<I>
An LTL model checker using LTSmin for DFAs.class
LTSminLTLIO<I,O>
An LTL model checker using LTSmin for Mealy machines using synchronous edge semantics. -
Uses of ModelChecker in net.automatalib.modelchecker.ltsmin.monitor
Classes in net.automatalib.modelchecker.ltsmin.monitor that implement ModelChecker Modifier and Type Class Description class
AbstractLTSminMonitor<I,A,R>
An LTSmin model checker for monitors.class
AbstractLTSminMonitorMealy<I,O>
A monitor model checker using LTSmin for Mealy machines.class
LTSminMonitorAlternating<I,O>
A monitor model checker using LTSmin for Mealy machines using alternating edge semantics.class
LTSminMonitorDFA<I>
A monitor model checker using LTSmin for DFAs.class
LTSminMonitorIO<I,O>
A monitor model checker using LTSmin for Mealy machines using synchronous edge semantics. -
Uses of ModelChecker in net.automatalib.modelchecker.m3c.solver
Classes in net.automatalib.modelchecker.m3c.solver that implement ModelChecker Modifier and Type Class Description class
ADDSolver<L,AP>
Implementation based on property transformers being represented by ADDs (Algebraic Decision Diagrams).class
BDDSolver<L,AP>
Implementation based on property transformers being represented by BDDs (Binary Decision Diagrams).class
StringADDSolver
AnADD solver
for generic, string-based formulas.class
StringBDDSolver
ABDD solver
for generic, string-based formulas.class
TypedADDSolver<L,AP>
AnADD solver
for strongly-typed formulas.class
TypedBDDSolver<L,AP>
ABDD solver
for strongly-typed formulas. -
Uses of ModelChecker in net.automatalib.modelchecking
Subinterfaces of ModelChecker in net.automatalib.modelchecking Modifier and Type Interface Description static interface
ModelChecker.DFAModelChecker<I,P,R>
static interface
ModelChecker.MealyModelChecker<I,O,P,R>
A model checker for Mealy machines.interface
ModelCheckerCache<I,A,P,R>
A model checker that caches calls tofindCounterExample(Object, Collection, Object)
.static interface
ModelCheckerCache.DFAModelCheckerCache<I,P,R>
static interface
ModelCheckerCache.MealyModelCheckerCache<I,O,P,R>
interface
ModelCheckerLasso<I,A,P,R extends Lasso<I,?>>
A model checker where the counterexample is a lasso.static interface
ModelCheckerLasso.DFAModelCheckerLasso<I,P>
static interface
ModelCheckerLasso.MealyModelCheckerLasso<I,O,P>
interface
ModelCheckerLassoCache<I,A,P,R extends Lasso<I,?>>
static interface
ModelCheckerLassoCache.DFAModelCheckerLassoCache<I,P>
static interface
ModelCheckerLassoCache.MealyModelCheckerLassoCache<I,O,P>
Classes in net.automatalib.modelchecking that implement ModelChecker Modifier and Type Class Description class
AbstractUnfoldingModelChecker<I,A,P,L extends Lasso<I,?>>
AnModelCheckerLasso
that can unfold loops of lassos.class
SizeDFAModelCheckerCache<I,P,R>
A DFAModelCheckerCache that invalidates the cached counter examples whenfindCounterExample(Object, Collection, Object)
is called with a DFA with a size different, and an input alphabet different from the previous call.class
SizeDFAModelCheckerLassoCache<I,P>
class
SizeMealyModelCheckerCache<I,O,P,R>
class
SizeMealyModelCheckerLassoCache<I,O,P>
-