Class LTSminMonitorDFA<I>
- java.lang.Object
-
- net.automatalib.modelchecker.ltsmin.AbstractLTSmin<I,A,R>
-
- net.automatalib.modelchecker.ltsmin.monitor.AbstractLTSminMonitor<I,DFA<?,I>,DFA<?,I>>
-
- net.automatalib.modelchecker.ltsmin.monitor.LTSminMonitorDFA<I>
-
- Type Parameters:
I
- the input type
- All Implemented Interfaces:
LTSmin<I,DFA<?,I>,DFA<?,I>>
,LTSminDFA<I,DFA<?,I>>
,ModelChecker<I,DFA<?,I>,String,DFA<?,I>>
,ModelChecker.DFAModelChecker<I,String,DFA<?,I>>
public class LTSminMonitorDFA<I> extends AbstractLTSminMonitor<I,DFA<?,I>,DFA<?,I>> implements LTSminDFA<I,DFA<?,I>>
A monitor 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>
-
-
Field Summary
-
Fields inherited from class net.automatalib.modelchecker.ltsmin.monitor.AbstractLTSminMonitor
REQUIRED_VERSION
-
Fields inherited from interface net.automatalib.modelchecker.ltsmin.LTSminDFA
LABEL_NAME, LABEL_VALUE
-
-
Constructor Summary
Constructors Constructor Description LTSminMonitorDFA(boolean keepFiles, Function<String,I> string2Input)
-
Method Summary
All Methods Instance Methods Concrete Methods Modifier and Type Method Description @Nullable DFA<?,I>
findCounterExample(DFA<?,I> automaton, Collection<? extends I> inputs, String property)
Converts the FSM file to aDFA
.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.monitor.AbstractLTSminMonitor
getExtraCommandLineOptions, getMinimumRequiredVersion
-
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
-
-
-
-
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>,DFA<?,I>>
- Parameters:
formula
- the formula to verify
-
findCounterExample
public @Nullable DFA<?,I> findCounterExample(DFA<?,I> automaton, Collection<? extends I> inputs, String property)
Converts the FSM file to aDFA
.- Specified by:
findCounterExample
in interfaceModelChecker<I,DFA<?,I>,String,DFA<?,I>>
- 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. - See Also:
ModelChecker.findCounterExample(Object, Collection, Object)
-
-