Package net.automatalib.modelchecker.ltsmin

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

Modifier and Type	Method	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.

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 given automaton to the given etf file.

Specified by:

automaton2ETF in interface LTSmin<I,DFA<?,I>,R>

Parameters:

automaton - the automaton to write.

inputs - the alphabet.

etf - the file to write to.

Throws:

IOException - when the given automaton can not be written to etf.

dfa2ETF

default <S> void dfa2ETF(DFA<S,I> dfa,
                         Collection<? extends I> inputs,
                         File etf)
                  throws IOException

Writes the given dfa to etf, 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.