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 |
---|---|
@Nullable 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.
|
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. |
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()
protected void verifyFormula(String formula)
AbstractLTSmin
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.
verifyFormula
in class AbstractLTSmin<I,MealyMachine<?,I,?,O>,MealyMachine<?,I,?,O>>
formula
- the formula to verifypublic @Nullable MealyMachine<?,I,?,O> findCounterExample(MealyMachine<?,I,?,O> automaton, Collection<? extends I> inputs, String property)
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.ModelChecker.findCounterExample(Object, Collection, Object)
Copyright © 2020. All rights reserved.