Interface LTSminMealy<I,O,R>
-
- Type Parameters:
I
- the input typeO
- the input typeR
- the type of counterexample
- All Superinterfaces:
LTSmin<I,MealyMachine<?,I,?,O>,R>
,ModelChecker<I,MealyMachine<?,I,?,O>,String,R>
,ModelChecker.MealyModelChecker<I,O,String,R>
- All Known Subinterfaces:
LTSminAlternating<I,O,R>
,LTSminIO<I,O,R>
- All Known Implementing Classes:
AbstractLTSminLTLMealy
,AbstractLTSminMonitorMealy
,LTSminLTLAlternating
,LTSminLTLIO
,LTSminMonitorAlternating
,LTSminMonitorIO
public interface LTSminMealy<I,O,R> extends ModelChecker.MealyModelChecker<I,O,String,R>, LTSmin<I,MealyMachine<?,I,?,O>,R>
A feature of thisModelChecker
, is that one can remove particular output symbols from the 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.
-
-
Nested Class Summary
-
Nested classes/interfaces inherited from interface net.automatalib.modelchecking.ModelChecker
ModelChecker.DFAModelChecker<I,P,R>, ModelChecker.MealyModelChecker<I,O,P,R>
-
-
Method Summary
All Methods Instance Methods Abstract Methods Default Methods Modifier and Type Method Description default void
automaton2ETF(MealyMachine<?,I,?,O> mealyMachine, Collection<? extends I> inputs, File etf)
Writes theMealyMachine
to theetf
file while pruning way the outputs given inModelChecker.MealyModelChecker.getSkipOutputs()
.CompactMealy<I,O>
fsm2Mealy(File fsm, MealyMachine<?,I,?,O> originalAutomaton, Collection<? extends I> inputs)
Converts the givenfsm
to aCompactMealy
.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 givenMealyMachine
to theetf
file.-
Methods inherited from interface net.automatalib.modelchecker.ltsmin.LTSmin
getString2Input, isKeepFiles
-
Methods inherited from interface net.automatalib.modelchecking.ModelChecker
findCounterExample
-
Methods inherited from interface net.automatalib.modelchecking.ModelChecker.MealyModelChecker
getSkipOutputs, setSkipOutputs
-
-
-
-
Method Detail
-
fsm2Mealy
CompactMealy<I,O> fsm2Mealy(File fsm, MealyMachine<?,I,?,O> originalAutomaton, Collection<? extends I> inputs) throws IOException
Converts the givenfsm
to aCompactMealy
.- Parameters:
fsm
- the FSM to convert.originalAutomaton
- the original automaton on which the property is checked.inputs
- the alphabet for the returned automaton.- Returns:
- the
CompactMealy
. - Throws:
IOException
- whenfsm
can not be read.FSMFormatException
- whenfsm
is invalid.
-
mealy2ETF
void mealy2ETF(MealyMachine<?,I,?,O> automaton, Collection<? extends I> inputs, File etf) throws IOException
Writes the givenMealyMachine
to theetf
file.- Parameters:
automaton
- theMealyMachine
to write.inputs
- the alphabet.etf
- the file to write to.- Throws:
IOException
- whenetf
can not be read.
-
automaton2ETF
default void automaton2ETF(MealyMachine<?,I,?,O> mealyMachine, Collection<? extends I> inputs, File etf) throws IOException
Writes theMealyMachine
to theetf
file while pruning way the outputs given inModelChecker.MealyModelChecker.getSkipOutputs()
.- Specified by:
automaton2ETF
in interfaceLTSmin<I,O,R>
- Parameters:
mealyMachine
- theMealyMachine
to write.inputs
- the alphabet.etf
- the file to write to.- Throws:
IOException
- seemealy2ETF(MealyMachine, Collection, File)
.
-
-