Module net.automatalib.modelchecker.ltsmin

Package net.automatalib.modelchecker.ltsmin

Interface LTSminAlternating<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:

LTSminLTLAlternating, LTSminMonitorAlternating

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

A model checker using LTSmin for Mealy machines using alternating edge semantics.

The implementation uses FSM2MealyParserAlternating, and Mealy2ETFWriterAlternating, 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.
boolean	requiresOriginalAutomaton()	Whether this model checker requires the original Mealy machine to read the Mealy machines from an FSM.

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 Details

requiresOriginalAutomaton

boolean requiresOriginalAutomaton()

Whether this model checker requires the original Mealy machine to read the Mealy machines from an FSM.

Returns:

whether the original automaton is required.

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.