Class LTSminLTLDFA<I>
- java.lang.Object
-
- net.automatalib.modelchecker.ltsmin.AbstractLTSmin<I,A,L>
-
- net.automatalib.modelchecker.ltsmin.ltl.AbstractLTSminLTL<I,DFA<?,I>,Lasso.DFALasso<I>>
-
- net.automatalib.modelchecker.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.
-
-
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 Modifier and Type Field 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.modelchecker.ltsmin.ltl.AbstractLTSminLTL
REQUIRED_VERSION
-
-
Constructor Summary
Constructors Constructor Description LTSminLTLDFA(boolean keepFiles, Function<String,I> string2Input, int minimumUnfolds, double multiplier)
-
Method Summary
All Methods Instance Methods Concrete Methods Modifier and Type Method Description @Nullable Lasso.DFALasso<I>
findCounterExample(DFA<?,I> automaton, Collection<? extends I> inputs, String property)
Converts the FSM file to aLasso.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 ofthis
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.LTSminDFA
automaton2ETF, dfa2ETF
-
Methods inherited from interface net.automatalib.modelchecking.ModelCheckerLasso
computeUnfolds, getMinimumUnfolds, getMultiplier, setMinimumUnfolds, setMultiplier
-
-
-
-
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
-
-
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 ofthis
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 classAbstractLTSmin<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 aLasso.DFALasso
.- Specified by:
findCounterExample
in interfaceModelChecker<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)
-
-