I
- the input type.O
- the output type.R
- the type of a counterexamplepublic interface LTSminAlternating<I,O,R> extends LTSminMealy<I,O,R>
FSM2MealyParserAlternating
, and Mealy2ETFWriterAlternating
, to read the
MealyMachine
, and write the MealyMachine
respectively.ModelChecker.DFAModelChecker<I,P,R>, ModelChecker.MealyModelChecker<I,O,P,R>
Modifier and Type | Method and Description |
---|---|
default CompactMealy<I,O> |
fsm2Mealy(File fsm,
MealyMachine<?,I,?,O> originalAutomaton,
Collection<? extends I> inputs)
Converts the given
fsm to a CompactMealy . |
default void |
mealy2ETF(MealyMachine<?,I,?,O> automaton,
Collection<? extends I> inputs,
File etf)
Writes the given
MealyMachine to the etf file. |
boolean |
requiresOriginalAutomaton()
Whether this model checker requires the original Mealy machine to read the Mealy machines from an FSM.
|
automaton2ETF, getString2Output
getSkipOutputs, setSkipOutputs
getString2Input, isKeepFiles
findCounterExample
boolean requiresOriginalAutomaton()
default CompactMealy<I,O> fsm2Mealy(File fsm, MealyMachine<?,I,?,O> originalAutomaton, Collection<? extends I> inputs) throws IOException, FSMParseException
LTSminMealy
fsm
to a CompactMealy
.fsm2Mealy
in interface LTSminMealy<I,O,R>
fsm
- the FSM to convert.originalAutomaton
- the original automaton on which the property is checked.inputs
- the alphabet for the returned automaton.CompactMealy
.IOException
- when fsm
can not be read.FSMParseException
- when fsm
is invalid.default void mealy2ETF(MealyMachine<?,I,?,O> automaton, Collection<? extends I> inputs, File etf) throws IOException
LTSminMealy
MealyMachine
to the etf
file.mealy2ETF
in interface LTSminMealy<I,O,R>
automaton
- the MealyMachine
to write.inputs
- the alphabet.etf
- the file to write to.IOException
- when etf
can not be read.Copyright © 2019. All rights reserved.