Package net.automatalib.modelchecker.m3c.solver

Class SolverState<N,​T extends AbstractPropertyTransformer<T,​L,​AP>,​L,​AP>

  • Type Parameters:
    N - node type
    T - property transformer type
    L - edge label type
    AP - atomic proposition type
    public final class SolverState<N,​T extends AbstractPropertyTransformer<T,​L,​AP>,​L,​AP>
extends Object
    Stores internal information produced during the update of a node in AbstractDDSolver.

    • Method Detail

      • getUpdatedPropTransformer

        public T getUpdatedPropTransformer​(TransformerSerializer<T,​L,​AP> serializer)
        Returns the updated property transformer. This method requires a TransformerSerializer as all property transform are stored as Strings in this class.
        Parameters:
        serializer - used to deserialize a property transformer from a String.
        Returns:
        the updated property transformer

      • getCompositions

        public List<T> getCompositions​(TransformerSerializer<T,​L,​AP> serializer)
        Returns a List of the property transformers representing the compositions of the property transformer of the outgoing edges and their target nodes. This method requires a TransformerSerializer as all property transform are stored as Strings in this class.
        Parameters:
        serializer - used to deserialize a property transformer from a String.
        Returns:
        the property transformers representing the compositions of the property transformer of the outgoing edges and their target nodes.

      • getUpdatedNodeSatisfiedSubformula

        public List<FormulaNode<L,​AP>> getUpdatedNodeSatisfiedSubformula()
        Returns the list of satisfied subformulas the node updated in this step satisfies after the update.
        Returns:
        the list of satisfied subformulas

      • getUpdatedNode

        public N getUpdatedNode()
        Returns the node updated in this step.
        Returns:
        the node updated in this step

      • getWorkSet

        public Map<L,​Set<?>> getWorkSet()
        Returns a Map which returns the set of nodes which are in the work set for each procedure after the update.
        Returns:
        a Map which returns the set of nodes which are in the work set for each procedure after the update