I
- the input typeO
- the input typeR
- the type of a counterexamplepublic interface LTSminMealy<I,O,R> extends ModelChecker.MealyModelChecker<I,O,String,R>, LTSmin<I,MealyMachine<?,I,?,O>,R>
ModelChecker
, is that one can remove particular output
symbols from the a given MealyMachine hypothesis. This is useful when those symbols are actually symbols representing
system deadlocks. When checking LTL formulae special attention has to be given to deadlock situations.ModelChecker.DFAModelChecker<I,P,R>, ModelChecker.MealyModelChecker<I,O,P,R>
Modifier and Type | Method and Description |
---|---|
default void |
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() . |
CompactMealy<I,O> |
fsm2Mealy(File fsm,
MealyMachine<?,I,?,O> originalAutomaton,
Collection<? extends I> inputs)
Converts the given
fsm to a CompactMealy . |
Function<String,O> |
getString2Output()
Gets a function that transforms edges in the FSM file to actual output.
|
void |
mealy2ETF(MealyMachine<?,I,?,O> automaton,
Collection<? extends I> inputs,
File etf)
Writes the given
MealyMachine to the etf file. |
getSkipOutputs, setSkipOutputs
getString2Input, isKeepFiles
findCounterExample
CompactMealy<I,O> fsm2Mealy(File fsm, MealyMachine<?,I,?,O> originalAutomaton, Collection<? extends I> inputs) throws IOException, FSMParseException
fsm
to a CompactMealy
.fsm
- the FSM to convert.originalAutomaton
- the original automaton on which the property is checked.inputs
- the alphabet for the returned automaton.CompactMealy
.IOException
- when fsm
can not be read.FSMParseException
- when fsm
is invalid.void mealy2ETF(MealyMachine<?,I,?,O> automaton, Collection<? extends I> inputs, File etf) throws IOException
MealyMachine
to the etf
file.automaton
- the MealyMachine
to write.inputs
- the alphabet.etf
- the file to write to.IOException
- when etf
can not be read.default void automaton2ETF(MealyMachine<?,I,?,O> mealyMachine, Collection<? extends I> inputs, File etf) throws IOException
MealyMachine
to the etf
file while pruning way the outputs given in ModelChecker.MealyModelChecker.getSkipOutputs()
.automaton2ETF
in interface LTSmin<I,MealyMachine<?,I,?,O>,R>
mealyMachine
- the MealyMachine
to write.inputs
- the alphabet.etf
- the file to write to.IOException
- see mealy2ETF(MealyMachine, Collection, File)
.Copyright © 2019. All rights reserved.