Package net.automatalib.modelchecker.ltsmin

Interface LTSminMealy<I,O,R>

Type Parameters:

I - the input type

O - the input type

R - 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 this ModelChecker, 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

Modifier and Type	Method	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.

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 given fsm to a CompactMealy.

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 - when fsm can not be read.

FSMFormatException - when fsm is invalid.

mealy2ETF

void mealy2ETF(MealyMachine<?,I,?,O> automaton,
               Collection<? extends I> inputs,
               File etf)
        throws IOException

Writes the given MealyMachine to the etf file.

Parameters:

automaton - the MealyMachine to write.

inputs - the alphabet.

etf - the file to write to.

Throws:

IOException - when etf can not be read.

automaton2ETF

default void automaton2ETF(MealyMachine<?,I,?,O> mealyMachine,
                           Collection<? extends I> inputs,
                           File etf)
                    throws IOException

Writes the MealyMachine to the etf file while pruning way the outputs given in ModelChecker.MealyModelChecker.getSkipOutputs().

Specified by:

automaton2ETF in interface LTSmin<I,O,R>

Parameters:

mealyMachine - the MealyMachine to write.

inputs - the alphabet.

etf - the file to write to.

Throws:

IOException - see mealy2ETF(MealyMachine, Collection, File).

getString2Output

Function<String,O> getString2Output()

Gets a function that transforms edges in the FSM file to actual output.

Returns:

the Function.