net.automatalib.modelcheckers.ltsmin

Interface LTSminIO<I,O,R>

Type Parameters:

I - the input type.

O - the output type.

R - the type of a counterexample

All Superinterfaces:

LTSmin<I,MealyMachine<?,I,?,O>,R>, LTSminMealy<I,O,R>, ModelChecker<I,MealyMachine<?,I,?,O>,String,R>, ModelChecker.MealyModelChecker<I,O,String,R>

All Known Implementing Classes:

LTSminLTLIO, LTSminMonitorIO

public interface LTSminIO<I,O,R>
extends LTSminMealy<I,O,R>

An model checker using LTSmin for Mealy machines using synchronous edge semantics. The implementation uses FSM2MealyParserIO, and Mealy2ETFWriterIO, to read the MealyMachine, and write the MealyMachine respectively.

Author:

Jeroen Meijer

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 and Description
default CompactMealy<I,O>	fsm2Mealy(File fsm, MealyMachine<?,I,?,O> originalAutomaton, Collection<? extends I> inputs) Converts the given fsm to a CompactMealy.
default 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.modelcheckers.ltsmin.LTSminMealy

automaton2ETF, getString2Output

Methods inherited from interface net.automatalib.modelchecking.ModelChecker.MealyModelChecker

getSkipOutputs, setSkipOutputs

Methods inherited from interface net.automatalib.modelcheckers.ltsmin.LTSmin

getString2Input, isKeepFiles

Methods inherited from interface net.automatalib.modelchecking.ModelChecker

findCounterExample

Method Detail

fsm2Mealy

default CompactMealy<I,O> fsm2Mealy(File fsm,
                                    MealyMachine<?,I,?,O> originalAutomaton,
                                    Collection<? extends I> inputs)
                             throws IOException,
                                    FSMParseException

Description copied from interface: LTSminMealy

Converts the given fsm to a CompactMealy.

Specified by:

fsm2Mealy in interface LTSminMealy<I,O,R>

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.

FSMParseException - when fsm is invalid.

mealy2ETF

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

Description copied from interface: LTSminMealy

Writes the given MealyMachine to the etf file.

Specified by:

mealy2ETF in interface LTSminMealy<I,O,R>

Parameters:

automaton - the MealyMachine to write.

inputs - the alphabet.

etf - the file to write to.

Throws:

IOException - when etf can not be read.