net.automatalib.modelcheckers.ltsmin.ltl

Class LTSminLTLDFA<I>

java.lang.Object

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

net.automatalib.modelcheckers.ltsmin.ltl.AbstractLTSminLTL<I,DFA<?,I>,Lasso.DFALasso<I>>

net.automatalib.modelcheckers.ltsmin.ltl.LTSminLTLDFA<I>

Type Parameters:

I - the input type

All Implemented Interfaces:

LTSmin<I,DFA<?,I>,Lasso.DFALasso<I>>, LTSminDFA<I,Lasso.DFALasso<I>>, ModelChecker<I,DFA<?,I>,String,Lasso.DFALasso<I>>, ModelChecker.DFAModelChecker<I,String,Lasso.DFALasso<I>>, ModelCheckerLasso<I,DFA<?,I>,String,Lasso.DFALasso<I>>, ModelCheckerLasso.DFAModelCheckerLasso<I,String>

public class LTSminLTLDFA<I>
extends AbstractLTSminLTL<I,DFA<?,I>,Lasso.DFALasso<I>>
implements ModelCheckerLasso.DFAModelCheckerLasso<I,String>, LTSminDFA<I,Lasso.DFALasso<I>>

An LTL model checker using LTSmin for DFAs.

Author:

Jeroen Meijer

Nested Class Summary

Nested classes/interfaces inherited from class net.automatalib.modelcheckers.ltsmin.ltl.AbstractLTSminLTL

AbstractLTSminLTL.BuilderDefaults

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

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

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

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

Field Summary

Fields

Modifier and Type	Field and Description
static String	LABEL_NAME The index in the FSM state vector for accept/reject.
static String	LABEL_VALUE The value in the state vector for acceptance.

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

REQUIRED_VERSION

Constructor Summary

Constructors

Constructor and Description
LTSminLTLDFA(boolean keepFiles, Function<String,I> string2Input, int minimumUnfolds, double multiplier)

Method Summary

Modifier and Type	Method and Description
@Nullable Lasso.DFALasso<I>	findCounterExample(DFA<?,I> automaton, Collection<? extends I> inputs, String property) Converts the FSM file to a Lasso.DFALasso.
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.modelcheckers.ltsmin.ltl.AbstractLTSminLTL

getExtraCommandLineOptions, getMinimumRequiredVersion, getMinimumUnfolds, getMultiplier, setMinimumUnfolds, setMultiplier

Methods inherited from class net.automatalib.modelcheckers.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.modelchecking.ModelCheckerLasso

computeUnfolds, getMinimumUnfolds, getMultiplier, setMinimumUnfolds, setMultiplier

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

automaton2ETF, dfa2ETF

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

getString2Input, isKeepFiles

Field Detail

LABEL_NAME

public static final String LABEL_NAME

The index in the FSM state vector for accept/reject.

See Also:

Constant Field Values

LABEL_VALUE

public static final String LABEL_VALUE

The value in the state vector for acceptance.

See Also:

Constant Field Values

Constructor Detail

LTSminLTLDFA

public LTSminLTLDFA(boolean keepFiles,
                    Function<String,I> string2Input,
                    int minimumUnfolds,
                    double multiplier)

Method Detail

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,DFA<?,I>,Lasso.DFALasso<I>>

Parameters:

formula - the formula to verify

findCounterExample

public @Nullable Lasso.DFALasso<I> findCounterExample(DFA<?,I> automaton,
                                                      Collection<? extends I> inputs,
                                                      String property)

Converts the FSM file to a Lasso.DFALasso.

Specified by:

findCounterExample in interface ModelChecker<I,DFA<?,I>,String,Lasso.DFALasso<I>>

Parameters:

automaton - the DFA used to compute the number of loop unrolls.

inputs - the alphabet.

property - the property.

Returns:

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

See Also:

ModelChecker.findCounterExample(Object, Collection, Object)