I
- the input type.R
- the type of a counterexamplepublic interface LTSminDFA<I,R> extends LTSmin<I,DFA<?,I>,R>, ModelChecker.DFAModelChecker<I,String,R>
DFAModelChecker
, is that it will check if a given DFA hypothesis is
prefix-closed.
Another important feature is that rejecting states are NOT part of the LTS. This avoids the need for an unconditional fairness constraint in LTL formulae.
DFAs.isPrefixClosed(DFA, Alphabet)
ModelChecker.DFAModelChecker<I,P,R>, ModelChecker.MealyModelChecker<I,O,P,R>
Modifier and Type | Field and Description |
---|---|
static String |
LABEL_NAME
The index in the FSM state vector for accept/reject.
|
static String |
LABEL_VALUE
The value in the state vector for acceptance.
|
Modifier and Type | Method and Description |
---|---|
default void |
automaton2ETF(DFA<?,I> automaton,
Collection<? extends I> inputs,
File etf)
Writes the given
automaton to the given etf file. |
default <S> void |
dfa2ETF(DFA<S,I> dfa,
Collection<? extends I> inputs,
File etf)
Writes the given
dfa to etf , while skipping rejecting states. |
getString2Input, isKeepFiles
findCounterExample
static final String LABEL_NAME
static final String LABEL_VALUE
default void automaton2ETF(DFA<?,I> automaton, Collection<? extends I> inputs, File etf) throws IOException
LTSmin
automaton
to the given etf
file.automaton2ETF
in interface LTSmin<I,DFA<?,I>,R>
automaton
- the automaton to write.inputs
- the alphabet.etf
- the file to write to.IOException
- when the given automaton
can not be written to etf
.default <S> void dfa2ETF(DFA<S,I> dfa, Collection<? extends I> inputs, File etf) throws IOException
dfa
to etf
, while skipping rejecting states.S
- the state typedfa
- the DFA to write.inputs
- the alphabet.etf
- the file to write to.IOException
- if the dfa couldn't be written to the provided file.ModelCheckingException
- if the dfa cannot be transformed into a valid LTS.Copyright © 2020. All rights reserved.