I
- the input type.A
- the automaton type.R
- the type of a counterexamplepublic interface LTSmin<I,A,R> extends ModelChecker<I,A,String,R>
ModelChecker.DFAModelChecker<I,P,R>, ModelChecker.MealyModelChecker<I,O,P,R>
Modifier and Type | Method and Description |
---|---|
void |
automaton2ETF(A automaton,
Collection<? extends I> inputs,
File etf)
Writes the given
automaton to the given etf file. |
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.
|
findCounterExample
void automaton2ETF(A automaton, Collection<? extends I> inputs, File etf) throws IOException
automaton
to the given etf
file.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
.ModelCheckingException
- when the given automaton
cannot be transformed into a valid LTS.boolean isKeepFiles()
Copyright © 2020. All rights reserved.