Class WitnessTree<L,AP>
- java.lang.Object
-
- net.automatalib.graph.base.AbstractCompactGraph<CompactEdge<EP>,NP,EP>
-
- net.automatalib.graph.CompactGraph<WitnessTreeState<?,L,?,AP>,String>
-
- net.automatalib.modelchecker.m3c.solver.WitnessTree<L,AP>
-
- Type Parameters:
L
- label typeAP
- atomic proposition type
- All Implemented Interfaces:
Iterable<Integer>
,FiniteRepresentation
,NodeIDs<Integer>
,Graph<Integer,CompactEdge<String>>
,Graph.IntAbstraction<CompactEdge<String>>
,IndefiniteGraph<Integer,CompactEdge<String>>
,IndefiniteSimpleGraph<Integer>
,MutableGraph<Integer,CompactEdge<String>,WitnessTreeState<?,L,?,AP>,String>
,MutableGraph.IntAbstraction<CompactEdge<String>,WitnessTreeState<?,L,?,AP>,String>
,SimpleGraph<Integer>
,SimpleGraph.IntAbstraction
,UniversalGraph<Integer,CompactEdge<String>,WitnessTreeState<?,L,?,AP>,String>
,UniversalGraph.IntAbstraction<CompactEdge<String>,WitnessTreeState<?,L,?,AP>,String>
,UniversalIndefiniteGraph<Integer,CompactEdge<String>,WitnessTreeState<?,L,?,AP>,String>
public class WitnessTree<L,AP> extends CompactGraph<WitnessTreeState<?,L,?,AP>,String>
A tree-likeGraph
that represents the BFS-style exploration of the tableau generated by theWitnessTreeExtractor
. Edges may represent the extraction of inner subformulae, procedural calls/returns to/from other procedures, or actual steps in the transition system (modal nodes).
-
-
Nested Class Summary
-
Nested classes/interfaces inherited from interface net.automatalib.graph.MutableGraph
MutableGraph.IntAbstraction<E,NP,EP>
-
-
Constructor Summary
Constructors Constructor Description WitnessTree()
-
Method Summary
All Methods Instance Methods Concrete Methods Modifier and Type Method Description Word<L>
getWitness()
-
Methods inherited from class net.automatalib.graph.CompactGraph
createEdge, getNodeProperty, setNodeProperty
-
Methods inherited from class net.automatalib.graph.base.AbstractCompactGraph
addIntNode, addNode, connect, connect, getEdgeProperty, getIntTarget, getNode, getNodeId, getNodeProperty, getNodes, getOutgoingEdges, getOutgoingEdges, getTarget, nodeIDs, setEdgeProperty, setNodeProperty, size
-
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
-
Methods inherited from interface net.automatalib.graph.Graph
getAdjacentNodes, getOutgoingEdgesIterator, getVisualizationHelper
-
Methods inherited from interface net.automatalib.graph.Graph.IntAbstraction
getEdgesBetween, getOutgoingEdgesIterator, isConnected
-
Methods inherited from interface net.automatalib.graph.IndefiniteGraph
getAdjacentNodesIterator, getEdgesBetween
-
Methods inherited from interface net.automatalib.graph.IndefiniteSimpleGraph
createDynamicNodeMapping, createStaticNodeMapping, isConnected
-
Methods inherited from interface java.lang.Iterable
forEach, spliterator
-
Methods inherited from interface net.automatalib.graph.MutableGraph
addNode, connect
-
Methods inherited from interface net.automatalib.graph.MutableGraph.IntAbstraction
addIntNode, connect
-
Methods inherited from interface net.automatalib.graph.SimpleGraph
iterator
-
-