Package net.automatalib.modelchecker.m3c.solver

Class WitnessTreeState<N,L,E,AP>

java.lang.Object

net.automatalib.modelchecker.m3c.solver.WitnessTreeState<N,L,E,AP>

Type Parameters:

N - node type of the referenced ProceduralModalProcessGraph

L - label type

E - edge type of the referenced ProceduralModalProcessGraph

AP - atomic proposition type

public class WitnessTreeState<N,L,E,AP>
extends Object

A utility class that represents a current configuration (node property) in the WitnessTree.

Field Summary

Fields

Modifier and Type	Field	Description
BitSet	context
String	displayLabel
@Nullable L	edgeLabel
boolean	isPartOfResult
int	parentId
ProceduralModalProcessGraph<N,L,E,AP,?>	pmpg
L	procedure
@Nullable WitnessTreeState<?,L,?,AP>	stack
N	state
FormulaNode<L,AP>	subformula
net.automatalib.modelchecker.m3c.solver.AbstractDDSolver.WorkUnit<N,E>	unit

Method Summary

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

stack

public final @Nullable WitnessTreeState<?,L,?,AP> stack

unit

public final net.automatalib.modelchecker.m3c.solver.AbstractDDSolver.WorkUnit<N,E> unit

procedure

public final L procedure

pmpg

public final ProceduralModalProcessGraph<N,L,E,AP,?> pmpg

state

public final N state

subformula

public final FormulaNode<L,AP> subformula

context

public final BitSet context

displayLabel

public final String displayLabel

edgeLabel

public final @Nullable L edgeLabel

parentId

public final int parentId

isPartOfResult

public boolean isPartOfResult