Module net.automatalib.modelchecker.m3c
Package net.automatalib.modelchecker.m3c.solver

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

java.lang.Object
net.automatalib.modelchecker.m3c.solver.SolverState<N,T,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 Details

    • 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

    • getUpdatedNodePMPG

      public L getUpdatedNodePMPG()
      Returns the name of the ProceduralModalProcessGraph which contains the node updated in this step.
      Returns:
      the name of the ProceduralModalProcessGraph which contains 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