I
- the input type.O
- the output type.public abstract class AbstractLTSminLTLMealy<I,O> extends AbstractLTSminLTL<I,MealyMachine<?,I,?,O>,Lasso.MealyLasso<I,O>> implements ModelCheckerLasso.MealyModelCheckerLasso<I,O,String>, LTSminMealy<I,O,Lasso.MealyLasso<I,O>>
AbstractLTSminLTL.BuilderDefaults
ModelCheckerLasso.DFAModelCheckerLasso<I,P>, ModelCheckerLasso.MealyModelCheckerLasso<I,O,P>
ModelChecker.DFAModelChecker<I,P,R>, ModelChecker.MealyModelChecker<I,O,P,R>
REQUIRED_VERSION
Modifier | Constructor and Description |
---|---|
protected |
AbstractLTSminLTLMealy(boolean keepFiles,
Function<String,I> string2Input,
Function<String,O> string2Output,
int minimumUnfolds,
double multiplier,
Collection<? super O> skipOutputs)
Constructs a new AbstractLTSminLTLMealy.
|
Modifier and Type | Method and Description |
---|---|
@Nullable Lasso.MealyLasso<I,O> |
findCounterExample(MealyMachine<?,I,?,O> automaton,
Collection<? extends I> inputs,
String property)
Try to find counter examples for the given
property and automaton . |
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, getMinimumUnfolds, getMultiplier, setMinimumUnfolds, setMultiplier
findCounterExampleFSM, getString2Input, isKeepFiles
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
computeUnfolds, getMinimumUnfolds, getMultiplier, setMinimumUnfolds, setMultiplier
automaton2ETF, fsm2Mealy, mealy2ETF
getString2Input, isKeepFiles
protected AbstractLTSminLTLMealy(boolean keepFiles, Function<String,I> string2Input, Function<String,O> string2Output, int minimumUnfolds, double multiplier, 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,Lasso.MealyLasso<I,O>>
public Collection<? super O> getSkipOutputs()
getSkipOutputs
in interface ModelChecker.MealyModelChecker<I,O,String,Lasso.MealyLasso<I,O>>
public void setSkipOutputs(Collection<? super O> skipOutputs)
setSkipOutputs
in interface ModelChecker.MealyModelChecker<I,O,String,Lasso.MealyLasso<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>,Lasso.MealyLasso<I,O>>
formula
- the formula to verifypublic @Nullable Lasso.MealyLasso<I,O> findCounterExample(MealyMachine<?,I,?,O> automaton, Collection<? extends I> inputs, String property)
ModelChecker
property
and automaton
.findCounterExample
in interface ModelChecker<I,MealyMachine<?,I,?,O>,String,Lasso.MealyLasso<I,O>>
automaton
- the automaton to check the property on.inputs
- the alphabet.property
- the property.null
if no counter examples exist.Copyright © 2020. All rights reserved.