Class Mealy2ETFWriterAlternating<I,​O>

  • Type Parameters:
    I - the input type
    O - the output type
    All Implemented Interfaces:
    InputModelSerializer<I,​MealyMachine<?,​I,​?,​O>>, ModelSerializer<InputModelData<I,​MealyMachine<?,​I,​?,​O>>>

    public final class Mealy2ETFWriterAlternating<I,​O>
    extends AbstractETFWriter<I,​MealyMachine<?,​I,​?,​O>>
    Write a Mealy machine with alternating edge semantics. Alternating means that a new edge (and state) is added to the LTS. So, instead of having two labels on one edge, input and output are alternated. Having alternating edge semantics may change the outcomes of temporal formulae.
    See Also:
    RERS 2017
    • Constructor Detail

      • Mealy2ETFWriterAlternating

        public Mealy2ETFWriterAlternating()
    • Method Detail

      • writeEdge

        protected void writeEdge​(PrintWriter pw)
        With alternating edge semantics, there are only edges with one label. Both input and output of the Mealy machine is generalized to a label named 'letter', of type 'letter'.
        Specified by:
        writeEdge in class AbstractETFWriter<I,​MealyMachine<?,​I,​?,​O>>
        Parameters:
        pw - the Writer.
      • writeETF

        protected void writeETF​(PrintWriter pw,
                                MealyMachine<?,​I,​?,​O> mealy,
                                Alphabet<I> inputs)
        Write the specific parts of the ETF for Mealy machines with alternating edge semantics.

        Writes: - the initial state, - the transitions, - the valuations for the state ids, - the letters from the alphabet.

        Note that in this context, the alphabet that is written to ETF is not just the inputs, it is the union of inputs and outputs, of type 'letter'.

        Specified by:
        writeETF in class AbstractETFWriter<I,​MealyMachine<?,​I,​?,​O>>
        Parameters:
        pw - the Writer.
        mealy - the MealyMachine to write to ETF.
        inputs - the alphabet, the input alphabet.
      • writeModel

        public void writeModel​(OutputStream os,
                               MealyMachine<?,​I,​?,​O> model,
                               Alphabet<I> alphabet)
        Description copied from interface: InputModelSerializer
        Writes the model to the given output stream.

        Note: the output stream will not be closed.

        Parameters:
        os - the output stream to write to
        model - the model to write
        alphabet - the inputs of the model to which serialization should be limited