Modifier and Type | Class and Description |
---|---|
static class |
MealyMachine.MealyGraphView<S,I,T,O,A extends MealyMachine<S,I,T,O>> |
Modifier and Type | Interface and Description |
---|---|
interface |
MutableMealyMachine<S,I,T,O> |
interface |
StateLocalInputMealyMachine<S,I,T,O> |
Modifier and Type | Class and Description |
---|---|
class |
FastMealy<I,O>
A fast implementation of a Mealy machine.
|
Modifier and Type | Class and Description |
---|---|
class |
CompactMealy<I,O> |
Modifier and Type | Method and Description |
---|---|
@Nullable Word<I> |
IncrementalMealyDAGBuilder.findSeparatingWord(MealyMachine<?,I,?,O> target,
Collection<? extends I> inputs,
boolean omitUndefined) |
Modifier and Type | Method and Description |
---|---|
@Nullable Word<I> |
AbstractIncrementalMealyTreeBuilder.findSeparatingWord(MealyMachine<?,I,?,O> target,
Collection<? extends I> inputs,
boolean omitUndefined) |
Modifier and Type | Method and Description |
---|---|
default void |
LTSminMealy.automaton2ETF(MealyMachine<?,I,?,O> mealyMachine,
Collection<? extends I> inputs,
File etf)
Writes the
MealyMachine to the etf file while pruning way the outputs given in ModelChecker.MealyModelChecker.getSkipOutputs() . |
default CompactMealy<I,O> |
LTSminIO.fsm2Mealy(File fsm,
MealyMachine<?,I,?,O> originalAutomaton,
Collection<? extends I> inputs) |
default CompactMealy<I,O> |
LTSminAlternating.fsm2Mealy(File fsm,
MealyMachine<?,I,?,O> originalAutomaton,
Collection<? extends I> inputs) |
CompactMealy<I,O> |
LTSminMealy.fsm2Mealy(File fsm,
MealyMachine<?,I,?,O> originalAutomaton,
Collection<? extends I> inputs)
Converts the given
fsm to a CompactMealy . |
default void |
LTSminIO.mealy2ETF(MealyMachine<?,I,?,O> automaton,
Collection<? extends I> inputs,
File etf) |
default void |
LTSminAlternating.mealy2ETF(MealyMachine<?,I,?,O> automaton,
Collection<? extends I> inputs,
File etf) |
void |
LTSminMealy.mealy2ETF(MealyMachine<?,I,?,O> automaton,
Collection<? extends I> inputs,
File etf)
Writes the given
MealyMachine to the etf file. |
Modifier and Type | Method and Description |
---|---|
@Nullable Lasso.MealyLasso<I,O> |
AbstractLTSminLTLMealy.findCounterExample(MealyMachine<?,I,?,O> automaton,
Collection<? extends I> inputs,
String property) |
Modifier and Type | Method and Description |
---|---|
@Nullable MealyMachine<?,I,?,O> |
AbstractLTSminMonitorMealy.findCounterExample(MealyMachine<?,I,?,O> automaton,
Collection<? extends I> inputs,
String property)
Converts the FSM file to a
MealyMachine . |
Modifier and Type | Method and Description |
---|---|
@Nullable MealyMachine<?,I,?,O> |
AbstractLTSminMonitorMealy.findCounterExample(MealyMachine<?,I,?,O> automaton,
Collection<? extends I> inputs,
String property)
Converts the FSM file to a
MealyMachine . |
Modifier and Type | Interface and Description |
---|---|
static interface |
Lasso.MealyLasso<I,O>
A MealyLasso is a lasso for
MealyMachine s. |
Modifier and Type | Class and Description |
---|---|
class |
MealyLassoImpl<I,O>
A MealyLasso is a lasso for
MealyMachine s. |
Modifier and Type | Method and Description |
---|---|
protected void |
Mealy2ETFWriterIO.writeETF(PrintWriter pw,
MealyMachine<?,I,?,O> mealy,
Alphabet<I> inputs)
Write ETF parts specific for Mealy machines with IO semantics.
|
protected void |
Mealy2ETFWriterAlternating.writeETF(PrintWriter pw,
MealyMachine<?,I,?,O> mealy,
Alphabet<I> inputs)
Write the specific parts of the ETF for Mealy machines with alternating edge semantics.
|
void |
Mealy2ETFWriterIO.writeModel(OutputStream os,
MealyMachine<?,I,?,O> model,
Alphabet<I> alphabet) |
void |
Mealy2ETFWriterAlternating.writeModel(OutputStream os,
MealyMachine<?,I,?,O> model,
Alphabet<I> alphabet) |
Modifier and Type | Method and Description |
---|---|
InputModelData<String,MealyMachine<?,String,?,String>> |
TAFSerializationMealy.readModel(InputStream is) |
Modifier and Type | Method and Description |
---|---|
void |
TAFSerializationMealy.writeModel(OutputStream os,
MealyMachine<?,String,?,?> model,
Alphabet<String> alphabet) |
Modifier and Type | Method and Description |
---|---|
static <I> void |
TAFWriter.mealyToString(MealyMachine<?,I,?,?> mealy,
Collection<? extends I> inputs) |
static <I> void |
TAFWriter.writeMealy(MealyMachine<?,I,?,?> mealy,
Collection<? extends I> inputs,
Appendable out) |
static <I> void |
TAFWriter.writeMealy(MealyMachine<?,I,?,?> mealy,
Collection<? extends I> inputs,
File out) |
Modifier and Type | Method and Description |
---|---|
static <S,I,T,O> Pair<ADSNode<S,I,O>,ADSNode<S,I,O>> |
ADSUtil.buildFromTrace(MealyMachine<S,I,T,O> automaton,
Word<I> trace,
S state) |
static <S,I,O> LYResult<S,I,O> |
LeeYannakakis.compute(MealyMachine<S,I,?,O> automaton,
Alphabet<I> input)
Computes an ADS using the algorithm of Lee and Yannakakis.
|
static <S,I,O> Optional<ADSNode<S,I,O>> |
StateEquivalence.compute(MealyMachine<S,I,?,O> automaton,
Alphabet<I> input,
Set<S> states)
Computes a two-state ADS by using
Automata.findSeparatingWord(UniversalDeterministicAutomaton,
UniversalDeterministicAutomaton, Collection) . |
static <S,I,O> Optional<ADSNode<S,I,O>> |
ADS.compute(MealyMachine<S,I,?,O> automaton,
Alphabet<I> input,
Set<S> states)
Compute an adaptive distinguishing sequence for the given automaton and the given set of states.
|
static <S,I,O> Optional<ADSNode<S,I,O>> |
BacktrackingSearch.compute(MealyMachine<S,I,?,O> automaton,
Alphabet<I> input,
Set<S> states)
Computes an ADS by constructing (growing) splitting words for the current set of states and recursively computing
sub-ADSs for the induced partitions.
|
static <S,I,O> Optional<ADSNode<S,I,O>> |
BacktrackingSearch.computeOptimal(MealyMachine<S,I,?,O> automaton,
Alphabet<I> input,
Set<S> states,
BacktrackingSearch.CostAggregator costAggregator)
Computes an ADS by iterating over the successor tree in a breadth-first manner, yielding an optimal (dependant on
the passed optimization function) ADS.
|
Modifier and Type | Method and Description |
---|---|
static <S,I,T,O,A extends MealyMachine<S,I,T,O> & InputAlphabetHolder<I>> |
HopcroftMinimization.minimizeMealy(A mealy)
Minimizes the given Mealy machine.
|
static <S,I,T,O,A extends MealyMachine<S,I,T,O> & InputAlphabetHolder<I>> |
HopcroftMinimization.minimizeMealy(A mealy,
HopcroftMinimization.PruningMode pruningMode)
Minimizes the given Mealy machine.
|
Modifier and Type | Method and Description |
---|---|
static <I,O> CompactMealy<I,O> |
HopcroftMinimization.minimizeMealy(MealyMachine<?,I,?,O> mealy,
Alphabet<I> alphabet)
Minimizes the given Mealy machine.
|
static <I,O> CompactMealy<I,O> |
HopcroftMinimization.minimizeMealy(MealyMachine<?,I,?,O> mealy,
Alphabet<I> alphabet,
HopcroftMinimization.PruningMode pruningMode)
Minimizes the given Mealy machine.
|
static <A extends MutableMealyMachine<?,I,?,O>,I,O> |
HopcroftMinimization.minimizeMealy(MealyMachine<?,I,?,O> mealy,
Alphabet<I> alphabet,
HopcroftMinimization.PruningMode pruningMode,
AutomatonCreator<A,I> creator)
Minimizes the given Mealy machine.
|
Modifier and Type | Method and Description |
---|---|
static <S,I,T,O,A extends MealyMachine<S,I,T,O> & InputAlphabetHolder<I>> |
PaigeTarjanMinimization.minimizeMealy(A mealy)
Minimizes the given Mealy machine.
|
Modifier and Type | Method and Description |
---|---|
static <I,O> CompactMealy<I,O> |
PaigeTarjanMinimization.minimizeMealy(MealyMachine<?,I,?,O> mealy,
Alphabet<I> alphabet)
Minimizes the given Mealy machine.
|
static <A extends MutableMealyMachine<?,I,?,O>,I,O> |
PaigeTarjanMinimization.minimizeMealy(MealyMachine<?,I,?,O> mealy,
Alphabet<I> alphabet,
AutomatonCreator<A,I> creator)
Minimizes the given Mealy machine.
|
Modifier and Type | Method and Description |
---|---|
static <I,O1,O2> CompactMealy<I,Pair<O1,O2>> |
MealyMachines.combine(MealyMachine<?,I,?,O1> mealy1,
MealyMachine<?,I,?,O2> mealy2,
Alphabet<I> inputAlphabet)
Constructs the product automaton for two Mealy Machines.
|
static <I,O1,O2> CompactMealy<I,Pair<O1,O2>> |
MealyMachines.combine(MealyMachine<?,I,?,O1> mealy1,
MealyMachine<?,I,?,O2> mealy2,
Alphabet<I> inputAlphabet)
Constructs the product automaton for two Mealy Machines.
|
static <I,O1,O2,A extends MutableMealyMachine<?,I,?,Pair<O1,O2>>> |
MealyMachines.combine(MealyMachine<?,I,?,O1> mealy1,
MealyMachine<?,I,?,O2> mealy2,
Collection<? extends I> inputs,
A out)
Constructs the product automaton for two Mealy Machines.
|
static <I,O1,O2,A extends MutableMealyMachine<?,I,?,Pair<O1,O2>>> |
MealyMachines.combine(MealyMachine<?,I,?,O1> mealy1,
MealyMachine<?,I,?,O2> mealy2,
Collection<? extends I> inputs,
A out)
Constructs the product automaton for two Mealy Machines.
|
static <I,O> CompactMealy<I,O> |
MealyMachines.complete(MealyMachine<?,I,?,O> mealy,
Alphabet<I> inputs,
O undefinedOutput)
Constructs a copy of the given Mealy machine in which every transition (with regards to the specified alphabet)
is guaranteed to be defined.
|
static <S,I,T,O,A extends MutableMealyMachine<S,I,T,O>> |
MealyMachines.complete(MealyMachine<?,I,?,O> mealy,
Collection<? extends I> inputs,
O undefinedOutput,
A out)
Constructs a copy of the given Mealy machine in which every transition (with regards to the specified alphabet)
is guaranteed to be defined.
|
static <I,O> CompactMealy<I,O> |
MealyFilter.filterByOutput(MealyMachine<?,I,?,O> in,
Alphabet<I> inputs,
Predicate<? super O> outputPred) |
static <S1,T1,S2,I,O> |
MealyFilter.filterByOutput(MealyMachine<S1,I,T1,O> in,
Collection<? extends I> inputs,
MutableMealyMachine<S2,I,?,O> out,
Predicate<? super O> outputPred) |
static <I,O> CompactMealy<I,O> |
MealyFilter.pruneTransitionsWithOutput(MealyMachine<?,I,?,O> in,
Alphabet<I> inputs,
Collection<? super O> outputs)
Returns a Mealy machine with all transitions removed that have one of the specified output values.
|
static <I,O> CompactMealy<I,O> |
MealyFilter.pruneTransitionsWithOutput(MealyMachine<?,I,?,O> in,
Alphabet<I> inputs,
O... outputs)
Returns a Mealy machine with all transitions removed that have one of the specified output values.
|
static <I,O> CompactMealy<I,O> |
MealyFilter.retainTransitionsWithOutput(MealyMachine<?,I,?,O> in,
Alphabet<I> inputs,
Collection<? super O> outputs)
Returns a Mealy machine with all transitions removed that have an output not among the specified values.
|
static <I,O> CompactMealy<I,O> |
MealyFilter.retainTransitionsWithOutput(MealyMachine<?,I,?,O> in,
Alphabet<I> inputs,
O... outputs)
Returns a Mealy machine with all transitions removed that have an output not among the specified values.
|
Copyright © 2020. All rights reserved.