Package net.automatalib.modelchecker.m3c.solver

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 type

AP - 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-like Graph that represents the BFS-style exploration of the tableau generated by the WitnessTreeExtractor. 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

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

Constructor Detail

WitnessTree

public WitnessTree()

Method Detail

getWitness

public Word<L> getWitness()