Package net.automatalib.modelchecker.ltsmin.ltl

Class AbstractLTSminLTLMealy<I,O>

java.lang.Object

net.automatalib.modelchecker.ltsmin.AbstractLTSmin<I,A,L>

net.automatalib.modelchecker.ltsmin.ltl.AbstractLTSminLTL<I,MealyMachine<?,I,?,O>,Lasso.MealyLasso<I,O>>

net.automatalib.modelchecker.ltsmin.ltl.AbstractLTSminLTLMealy<I,O>

Type Parameters:

I - the input type.

O - the output type.

All Implemented Interfaces:

LTSmin<I,MealyMachine<?,I,?,O>,Lasso.MealyLasso<I,O>>, LTSminMealy<I,O,Lasso.MealyLasso<I,O>>, ModelChecker<I,MealyMachine<?,I,?,O>,String,Lasso.MealyLasso<I,O>>, ModelChecker.MealyModelChecker<I,O,String,Lasso.MealyLasso<I,O>>, ModelCheckerLasso<I,MealyMachine<?,I,?,O>,String,Lasso.MealyLasso<I,O>>, ModelCheckerLasso.MealyModelCheckerLasso<I,O,String>

Direct Known Subclasses:

LTSminLTLAlternating, LTSminLTLIO

public abstract class AbstractLTSminLTLMealy<I,O>
extends AbstractLTSminLTL<I,MealyMachine<?,I,?,O>,Lasso.MealyLasso<I,O>>
implements ModelCheckerLasso.MealyModelCheckerLasso<I,O,String>, LTSminMealy<I,O,Lasso.MealyLasso<I,O>>

An LTL model checker using LTSmin for Mealy machines.

Nested Class Summary

Nested classes/interfaces inherited from interface net.automatalib.modelchecking.ModelChecker

ModelChecker.DFAModelChecker<I,P,R>, ModelChecker.MealyModelChecker<I,O,P,R>

Nested classes/interfaces inherited from interface net.automatalib.modelchecking.ModelCheckerLasso

ModelCheckerLasso.DFAModelCheckerLasso<I,P>, ModelCheckerLasso.MealyModelCheckerLasso<I,O,P>

Field Summary

Fields inherited from class net.automatalib.modelchecker.ltsmin.ltl.AbstractLTSminLTL

REQUIRED_VERSION

Constructor Summary

Constructors

Modifier	Constructor	Description
protected	AbstractLTSminLTLMealy(boolean keepFiles, Function<String,I> string2Input, Function<String,O> string2Output, int minimumUnfolds, double multiplier, Collection<? super O> skipOutputs)	Constructs a new AbstractLTSminLTLMealy.

Method Summary

Modifier and Type	Method	Description
@Nullable Lasso.MealyLasso<I,O>	findCounterExample(MealyMachine<?,I,?,O> automaton, Collection<? extends I> inputs, String property)	Try to find counter examples for the given property and automaton.
Collection<? super O>	getSkipOutputs()	Gets a set of outputs that need to be skipped while writing the Mealy machine to ETF.
Function<String,O>	getString2Output()	Gets a function that transforms edges in the FSM file to actual output.
void	setSkipOutputs(Collection<? super O> skipOutputs)	Sets a set of outputs that need to be skipped while writing the Mealy machine to ETF.
protected void	verifyFormula(String formula)	This method must verify that the given formula adheres to the expected syntax of the chosen serialization format for hypotheses of this model-checker.

Methods inherited from class net.automatalib.modelchecker.ltsmin.ltl.AbstractLTSminLTL

getExtraCommandLineOptions, getMinimumRequiredVersion, getMinimumUnfolds, getMultiplier, setMinimumUnfolds, setMultiplier

Methods inherited from class net.automatalib.modelchecker.ltsmin.AbstractLTSmin

findCounterExampleFSM, getString2Input, isKeepFiles

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

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

getString2Input, isKeepFiles

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

automaton2ETF, fsm2Mealy, mealy2ETF

Methods inherited from interface net.automatalib.modelchecking.ModelCheckerLasso

computeUnfolds, getMinimumUnfolds, getMultiplier, setMinimumUnfolds, setMultiplier

Constructor Detail

AbstractLTSminLTLMealy

protected AbstractLTSminLTLMealy(boolean keepFiles,
                                 Function<String,I> string2Input,
                                 Function<String,O> string2Output,
                                 int minimumUnfolds,
                                 double multiplier,
                                 Collection<? super O> skipOutputs)

Constructs a new AbstractLTSminLTLMealy.

Parameters:

string2Output - the function that transforms edges in the FSM file to actual output.

skipOutputs - the set of outputs that need to be skipped while writing the Mealy machine to ETF.

See Also:

AbstractLTSminLTL

Method Detail

getString2Output

public Function<String,O> getString2Output()

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

Specified by:

getString2Output in interface LTSminMealy<I,O,Lasso.MealyLasso<I,O>>

Returns:

the Function.

getSkipOutputs

public Collection<? super O> getSkipOutputs()

Gets a set of outputs that need to be skipped while writing the Mealy machine to ETF.

Specified by:

getSkipOutputs in interface ModelChecker.MealyModelChecker<I,O,String,Lasso.MealyLasso<I,O>>

Returns:

the Colleciton.

setSkipOutputs

public void setSkipOutputs(Collection<? super O> skipOutputs)

Sets a set of outputs that need to be skipped while writing the Mealy machine to ETF.

Specified by:

setSkipOutputs in interface ModelChecker.MealyModelChecker<I,O,String,Lasso.MealyLasso<I,O>>

Parameters:

skipOutputs - the outputs.

See Also:

ModelChecker.MealyModelChecker.getSkipOutputs()

verifyFormula

protected void verifyFormula(String formula)

Description copied from class: AbstractLTSmin

This method must verify that the given formula adheres to the expected syntax of the chosen serialization format for hypotheses of this model-checker.

If the formula does not adhere to the expected syntax, this method should throw a IllegalArgumentException, possibly containing nested causes that further elaborate on why the formula couldn't be verified.

Specified by:

verifyFormula in class AbstractLTSmin<I,MealyMachine<?,I,?,O>,Lasso.MealyLasso<I,O>>

Parameters:

formula - the formula to verify

findCounterExample

public @Nullable Lasso.MealyLasso<I,O> findCounterExample(MealyMachine<?,I,?,O> automaton,
                                                                Collection<? extends I> inputs,
                                                                String property)

Description copied from interface: ModelChecker

Try to find counter examples for the given property and automaton.

Specified by:

findCounterExample in interface ModelChecker<I,MealyMachine<?,I,?,O>,String,Lasso.MealyLasso<I,O>>

Parameters:

automaton - the automaton to check the property on.

inputs - the alphabet.

property - the property.

Returns:

the counter examples, or null if no counter examples exist.