Class AbstractLTSminMonitorMealy<I,O>
- java.lang.Object
-
- net.automatalib.modelchecker.ltsmin.AbstractLTSmin<I,A,R>
-
- net.automatalib.modelchecker.ltsmin.monitor.AbstractLTSminMonitor<I,MealyMachine<?,I,?,O>,MealyMachine<?,I,?,O>>
-
- net.automatalib.modelchecker.ltsmin.monitor.AbstractLTSminMonitorMealy<I,O>
-
- Type Parameters:
I
- the input type.O
- the output type.
- All Implemented Interfaces:
LTSmin<I,MealyMachine<?,I,?,O>,MealyMachine<?,I,?,O>>
,LTSminMealy<I,O,MealyMachine<?,I,?,O>>
,ModelChecker<I,MealyMachine<?,I,?,O>,String,MealyMachine<?,I,?,O>>
,ModelChecker.MealyModelChecker<I,O,String,MealyMachine<?,I,?,O>>
- Direct Known Subclasses:
LTSminMonitorAlternating
,LTSminMonitorIO
public abstract class AbstractLTSminMonitorMealy<I,O> extends AbstractLTSminMonitor<I,MealyMachine<?,I,?,O>,MealyMachine<?,I,?,O>> implements LTSminMealy<I,O,MealyMachine<?,I,?,O>>
A monitor 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>
-
-
Field Summary
-
Fields inherited from class net.automatalib.modelchecker.ltsmin.monitor.AbstractLTSminMonitor
REQUIRED_VERSION
-
-
Constructor Summary
Constructors Modifier Constructor Description protected
AbstractLTSminMonitorMealy(boolean keepFiles, Function<String,I> string2Input, Function<String,O> string2Output, Collection<? super O> skipOutputs)
Constructs a new AbstractLTSminLTLMealy.
-
Method Summary
All Methods Instance Methods Concrete Methods Modifier and Type Method Description @Nullable MealyMachine<?,I,?,O>
findCounterExample(MealyMachine<?,I,?,O> automaton, Collection<? extends I> inputs, String property)
Converts the FSM file to aMealyMachine
.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 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.LTSminMealy
automaton2ETF, fsm2Mealy, mealy2ETF
-
-
-
-
Constructor Detail
-
AbstractLTSminMonitorMealy
protected AbstractLTSminMonitorMealy(boolean keepFiles, Function<String,I> string2Input, Function<String,O> string2Output, 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 interfaceLTSminMealy<I,O,MealyMachine<?,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 interfaceModelChecker.MealyModelChecker<I,O,String,MealyMachine<?,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 interfaceModelChecker.MealyModelChecker<I,O,String,MealyMachine<?,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 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,MealyMachine<?,I,?,O>,MealyMachine<?,I,?,O>>
- Parameters:
formula
- the formula to verify
-
findCounterExample
public @Nullable MealyMachine<?,I,?,O> findCounterExample(MealyMachine<?,I,?,O> automaton, Collection<? extends I> inputs, String property)
Converts the FSM file to aMealyMachine
.- Specified by:
findCounterExample
in interfaceModelChecker<I,MealyMachine<?,I,?,O>,String,MealyMachine<?,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. - See Also:
ModelChecker.findCounterExample(Object, Collection, Object)
-
-