I
- the input type.A
- the automaton type.R
- the type of a counterexamplepublic abstract class AbstractLTSmin<I,A,R> extends Object implements ModelChecker<I,A,String,R>, LTSmin<I,A,R>
The user must install LTSmin in order for AbstractLTSmin
to run without exceptions. Once LTSmin is
installed the user may specify the path to the installed LTSmin binaries with the property
automatalib.ltsmin.path. If this property is not set the binaries will be run as usual (e.g. simply
by invoking etf2lts-mc, and ltsmin-convert), which means the user can also specify the location of the binaries in
the PATH environment variable.
This model checker is implemented as follows. The hypothesis automaton is first written to an LTS in ETF AbstractETFWriter
file, which serves as input for the etf2lts-mc binary. Then the etf2lts-mc binary is run, which
will write an LTS in GCF format. This LTS will be a subset of the language of the given hypothesis. Next, the GCF is
converted to FSM using the ltsmin-convert binary. Lastly, the FSM is read back into an automaton using an AbstractFSMParser
.
AbstractFSMParser
,
AbstractETFWriter
,
AutomataLibSettings
Modifier and Type | Class and Description |
---|---|
static class |
AbstractLTSmin.BuilderDefaults |
ModelChecker.DFAModelChecker<I,P,R>, ModelChecker.MealyModelChecker<I,O,P,R>
Modifier | Constructor and Description |
---|---|
protected |
AbstractLTSmin(boolean keepFiles,
Function<String,I> string2Input)
Constructs a new AbstractLTSmin.
|
Modifier and Type | Method and Description |
---|---|
protected @Nullable File |
findCounterExampleFSM(A hypothesis,
Collection<? extends I> inputs,
String formula)
Finds a counterexample for the given
formula , and given hypothesis in FSM format. |
protected abstract List<String> |
getExtraCommandLineOptions()
Returns the extra command line options that should be given to the etf2lts-mc binary.
|
protected abstract LTSminVersion |
getMinimumRequiredVersion()
Returns the minimum required version of LTSmin.
|
Function<String,I> |
getString2Input()
Returns the function that transforms edges in FSM files to actual input.
|
boolean |
isKeepFiles()
Returns whether intermediate files should be kept, e.g. etfs, gcfs, etc.
|
protected abstract 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. |
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
automaton2ETF
findCounterExample
protected AbstractLTSmin(boolean keepFiles, Function<String,I> string2Input)
keepFiles
- whether to keep intermediate files, (e.g. etfs, gcfs etc.).string2Input
- a function that transforms edges in FSM files to actual input.ModelCheckingException
- when the LTSmin binaries can not be run successfully.AbstractLTSmin
protected abstract LTSminVersion getMinimumRequiredVersion()
protected abstract List<String> getExtraCommandLineOptions()
protected abstract void verifyFormula(String formula)
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.
formula
- the formula to verifypublic boolean isKeepFiles()
LTSmin
isKeepFiles
in interface LTSmin<I,A,R>
public Function<String,I> getString2Input()
LTSmin
getString2Input
in interface LTSmin<I,A,R>
protected final @Nullable File findCounterExampleFSM(A hypothesis, Collection<? extends I> inputs, String formula)
formula
, and given hypothesis
in FSM format.hypothesis
- the hypothesis to checkinputs
- the inputs which should be regarded for checkingformula
- the formula that should be checkednull
if no such
counterexample could be found.AbstractLTSmin
Copyright © 2020. All rights reserved.