Interface LTSminDFA<I,R>
-
- Type Parameters:
I
- the input type.R
- the type of counterexample
- All Superinterfaces:
LTSmin<I,DFA<?,I>,R>
,ModelChecker<I,DFA<?,I>,String,R>
,ModelChecker.DFAModelChecker<I,String,R>
- All Known Implementing Classes:
LTSminLTLDFA
,LTSminMonitorDFA
public interface LTSminDFA<I,R> extends LTSmin<I,DFA<?,I>,R>, ModelChecker.DFAModelChecker<I,String,R>
A model checker using LTSmin for DFAs.An important feature of this
ModelChecker.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.
- See Also:
DFAs.isPrefixClosed(DFA, Collection)
-
-
Nested Class Summary
-
Nested classes/interfaces inherited from interface net.automatalib.modelchecking.ModelChecker
ModelChecker.DFAModelChecker<I,P,R>, ModelChecker.MealyModelChecker<I,O,P,R>
-
-
Field Summary
Fields Modifier and Type Field 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.
-
Method Summary
All Methods Instance Methods Default Methods Modifier and Type Method Description default void
automaton2ETF(DFA<?,I> automaton, Collection<? extends I> inputs, File etf)
Writes the givenautomaton
to the givenetf
file.default <S> void
dfa2ETF(DFA<S,I> dfa, Collection<? extends I> inputs, File etf)
Writes the givendfa
toetf
, while skipping rejecting states.-
Methods inherited from interface net.automatalib.modelchecker.ltsmin.LTSmin
getString2Input, isKeepFiles
-
Methods inherited from interface net.automatalib.modelchecking.ModelChecker
findCounterExample
-
-
-
-
Field Detail
-
LABEL_NAME
static final String LABEL_NAME
The index in the FSM state vector for accept/reject.- See Also:
- Constant Field Values
-
LABEL_VALUE
static final String LABEL_VALUE
The value in the state vector for acceptance.- See Also:
- Constant Field Values
-
-
Method Detail
-
automaton2ETF
default void automaton2ETF(DFA<?,I> automaton, Collection<? extends I> inputs, File etf) throws IOException
Description copied from interface:LTSmin
Writes the givenautomaton
to the givenetf
file.- Specified by:
automaton2ETF
in interfaceLTSmin<I,DFA<?,I>,R>
- Parameters:
automaton
- the automaton to write.inputs
- the alphabet.etf
- the file to write to.- Throws:
IOException
- when the givenautomaton
can not be written toetf
.
-
dfa2ETF
default <S> void dfa2ETF(DFA<S,I> dfa, Collection<? extends I> inputs, File etf) throws IOException
Writes the givendfa
toetf
, while skipping rejecting states.- Type Parameters:
S
- the state type- Parameters:
dfa
- the DFA to write.inputs
- the alphabet.etf
- the file to write to.- Throws:
IOException
- if the dfa couldn't be written to the provided file.ModelCheckingException
- if the dfa cannot be transformed into a valid LTS.
-
-