I
- the input type.O
- the output type.public abstract class AbstractLTSminMonitorMealy<I,O> extends AbstractLTSminMonitor<I,MealyMachine<?,I,?,O>,MealyMachine<?,I,?,O>> implements LTSminMealy<I,O,MealyMachine<?,I,?,O>>
AbstractLTSmin.BuilderDefaults
ModelChecker.DFAModelChecker<I,P,R>, ModelChecker.MealyModelChecker<I,O,P,R>
REQUIRED_VERSION
Modifier | Constructor and Description |
---|---|
protected |
AbstractLTSminMonitorMealy(boolean keepFiles,
Function<String,I> string2Input,
Function<String,O> string2Output,
Collection<? super O> skipOutputs)
Constructs a new AbstractLTSminLTLMealy.
|
Modifier and Type | Method and Description |
---|---|
MealyMachine<?,I,?,O> |
findCounterExample(MealyMachine<?,I,?,O> automaton,
Collection<? extends I> inputs,
String property)
Converts the FSM file to a
MealyMachine . |
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.
|
getExtraCommandLineOptions, getMinimumRequiredVersion
findCounterExampleFSM, getString2Input, isKeepFiles
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
automaton2ETF, fsm2Mealy, mealy2ETF
getString2Input, isKeepFiles
protected AbstractLTSminMonitorMealy(boolean keepFiles, Function<String,I> string2Input, Function<String,O> string2Output, Collection<? super O> skipOutputs)
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.AbstractLTSminLTL
public Function<String,O> getString2Output()
getString2Output
in interface LTSminMealy<I,O,MealyMachine<?,I,?,O>>
public Collection<? super O> getSkipOutputs()
getSkipOutputs
in interface ModelChecker.MealyModelChecker<I,O,String,MealyMachine<?,I,?,O>>
public void setSkipOutputs(Collection<? super O> skipOutputs)
setSkipOutputs
in interface ModelChecker.MealyModelChecker<I,O,String,MealyMachine<?,I,?,O>>
skipOutputs
- the outputs.ModelChecker.MealyModelChecker.getSkipOutputs()
@Nullable public MealyMachine<?,I,?,O> findCounterExample(MealyMachine<?,I,?,O> automaton, Collection<? extends I> inputs, String property) throws ModelCheckingException
MealyMachine
.findCounterExample
in interface ModelChecker<I,MealyMachine<?,I,?,O>,String,MealyMachine<?,I,?,O>>
automaton
- the automaton to check the property on.inputs
- the alphabet.property
- the property.null
if no counter examples exist.ModelCheckingException
- when this model checker can not check the property.ModelChecker.findCounterExample(Object, Collection, Object)
Copyright © 2019. All rights reserved.