Module net.automatalib.modelchecker.ltsmin

Package net.automatalib.modelchecker.ltsmin

Interface LTSminIO<I,O,R>

Type Parameters:

I - the input type.

O - the output type.

R - the type of 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>

A 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.

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 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.modelchecker.ltsmin.LTSmin

getString2Input, isKeepFiles

Methods inherited from interface net.automatalib.modelchecker.ltsmin.LTSminMealy

automaton2ETF, getString2Output

Methods inherited from interface net.automatalib.modelchecking.ModelChecker

findCounterExample

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

getSkipOutputs, setSkipOutputs

Method Detail

fsm2Mealy

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

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.

FormatException - 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.