Modifier and Type | Method and Description |
---|---|
protected File |
AbstractLTSmin.findCounterExampleFSM(A hypothesis,
Collection<? extends I> inputs,
String formula)
Finds a counterexample for the given
formula , and given hypothesis in FSM format. |
Constructor and Description |
---|
AbstractLTSmin(boolean keepFiles,
Function<String,I> string2Input)
Constructs a new AbstractLTSmin.
|
Modifier and Type | Method and Description |
---|---|
Lasso.DFALasso<I> |
LTSminLTLDFA.findCounterExample(DFA<?,I> automaton,
Collection<? extends I> inputs,
String property)
Converts the FSM file to a
Lasso.DFALasso . |
Lasso.MealyLasso<I,O> |
AbstractLTSminLTLMealy.findCounterExample(MealyMachine<?,I,?,O> automaton,
Collection<? extends I> inputs,
String property) |
Constructor and Description |
---|
AbstractLTSminLTL(boolean keepFiles,
Function<String,I> string2Input,
int minimumUnfolds,
double multiplier)
Constructs a new AbstractLTSminLTL.
|
Modifier and Type | Method and Description |
---|---|
DFA<?,I> |
LTSminMonitorDFA.findCounterExample(DFA<?,I> automaton,
Collection<? extends I> inputs,
String property)
Converts the FSM file to a
DFA . |
MealyMachine<?,I,?,O> |
AbstractLTSminMonitorMealy.findCounterExample(MealyMachine<?,I,?,O> automaton,
Collection<? extends I> inputs,
String property)
Converts the FSM file to a
MealyMachine . |
Constructor and Description |
---|
AbstractLTSminMonitor(boolean keepFiles,
Function<String,I> string2Input)
Constructs a new AbstractLTSminMonitor.
|
Modifier and Type | Method and Description |
---|---|
R |
ModelChecker.findCounterExample(A automaton,
Collection<? extends I> inputs,
P property)
Try to find counter examples for the given
property and automaton . |
Copyright © 2019. All rights reserved.