net.automatalib.serialization.fsm.parser

Class FSM2MealyParserAlternating<I,O>

java.lang.Object

net.automatalib.serialization.fsm.parser.AbstractFSMParser<I>

net.automatalib.serialization.fsm.parser.AbstractFSM2MealyParser<I,O>

net.automatalib.serialization.fsm.parser.FSM2MealyParserAlternating<I,O>

Type Parameters:

I - the input type

O - the output type

All Implemented Interfaces:

ModelDeserializer<CompactMealy<I,O>>

public final class FSM2MealyParserAlternating<I,O>
extends AbstractFSM2MealyParser<I,O>

Parses a Mealy machine with alternating edge semantics from an FSM source. Some public static parse() methods accept an Output object. This is used as follows. If the Mealy machine that is read from the FSM file has no defined output symbol after an input word. The last output symbol is taken from Output.computeOutput(Iterable). If a parse() method is used that does not accept an Output object an exception is thrown when the FSM does not define an output symbol after an input word. Furthermore, if Output.computeOutput(Iterable) returns null an exception is throws as well.

A use case where supplying an Output object to a parse() method is necessary is when one is model checking with monitors. With alternating semantics the model checker can conclude the monitor is in a rejecting state after an input symbol (and hence every output symbol is incorrect). To construct an input-enabled Mealy machine this parser needs to know the correct output symbol. Note that this situation does not arise with synchronous semantics.

Nested Class Summary

Nested classes/interfaces inherited from class net.automatalib.serialization.fsm.parser.AbstractFSMParser

AbstractFSMParser.Part

Field Summary

Fields

Modifier and Type	Field and Description
static String	INPUT_HAS_NO_OUTPUT
static String	PARTIAL_FSM

Fields inherited from class net.automatalib.serialization.fsm.parser.AbstractFSMParser

EXPECT_CHAR, EXPECT_IDENTIFIER, EXPECT_NUMBER, EXPECT_STRING, NO_SUCH_STATE, NON_DETERMINISM_DETECTED, targetInputs

Method Summary

Modifier and Type	Method and Description
protected void	checkTransitions(StreamTokenizer streamTokenizer) Creates the actual Mealy machine transitions.
static <E> FSM2MealyParserAlternating<E,E>	getParser(Collection<? extends E> targetInputs, Output<E,Word<E>> output, Function<String,E> edgeParser)
static <I,O> FSM2MealyParserAlternating<I,O>	getParser(Collection<? extends I> targetInputs, Output<I,Word<O>> output, Function<String,I> inputParser, Function<String,O> outputParser)
static <E> FSM2MealyParserAlternating<E,E>	getParser(Function<String,E> edgeParser)
static <I,O> FSM2MealyParserAlternating<I,O>	getParser(Function<String,I> inputParser, Function<String,O> outputParser)
protected void	parseTransition(StreamTokenizer streamTokenizer) Parse a transition.

Methods inherited from class net.automatalib.serialization.fsm.parser.AbstractFSM2MealyParser

checkDataDefinitions, checkStateVectors, getOutputParser, getStates, getTransitions, parseDataDefinition, parseMealy, parseStateVector, readModel

Methods inherited from class net.automatalib.serialization.fsm.parser.AbstractFSMParser

getInputParser, getInputs, getPartLineNumber, getStreamTokenizer, parse

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Methods inherited from interface net.automatalib.serialization.ModelDeserializer

readModel, readModel, readModel

Field Detail

PARTIAL_FSM

public static final String PARTIAL_FSM

See Also:

Constant Field Values

INPUT_HAS_NO_OUTPUT

public static final String INPUT_HAS_NO_OUTPUT

See Also:

Constant Field Values

Method Detail

parseTransition

protected void parseTransition(StreamTokenizer streamTokenizer)
                        throws FSMParseException,
                               IOException

Parse a transition.

Specified by:

parseTransition in class AbstractFSMParser<I>

Parameters:

streamTokenizer - tokenizer containing the input

Throws:

FSMParseException - when the FSM source is invalid.

IOException - see StreamTokenizer.nextToken().

checkTransitions

protected void checkTransitions(StreamTokenizer streamTokenizer)
                         throws FSMParseException

Creates the actual Mealy machine transitions.

Specified by:

checkTransitions in class AbstractFSMParser<I>

Parameters:

streamTokenizer - tokenizer containing the input

Throws:

FSMParseException - when the Mealy machine is partial.

getParser

public static <I,O> FSM2MealyParserAlternating<I,O> getParser(@Nullable
                                                              Collection<? extends I> targetInputs,
                                                              @Nullable
                                                              Output<I,Word<O>> output,
                                                              Function<String,I> inputParser,
                                                              Function<String,O> outputParser)

getParser

public static <I,O> FSM2MealyParserAlternating<I,O> getParser(Function<String,I> inputParser,
                                                              Function<String,O> outputParser)

getParser

public static <E> FSM2MealyParserAlternating<E,E> getParser(@Nullable
                                                            Collection<? extends E> targetInputs,
                                                            @Nullable
                                                            Output<E,Word<E>> output,
                                                            Function<String,E> edgeParser)

getParser

public static <E> FSM2MealyParserAlternating<E,E> getParser(Function<String,E> edgeParser)