A B C D E F G H I L M N O P S T U V W
All Classes All Packages

A

AbstractBinaryFormulaNode<L,AP> - Class in net.automatalib.modelchecker.m3c.formula

Abstract super-class for binary (sub-) formulas.

AbstractBinaryFormulaNode(FormulaNode<L, AP>, FormulaNode<L, AP>) - Constructor for class net.automatalib.modelchecker.m3c.formula.AbstractBinaryFormulaNode

AbstractFixedPointFormulaNode<L,AP> - Class in net.automatalib.modelchecker.m3c.formula.modalmu

Abstract super-class for fix-point (sub-) formulas.

AbstractFixedPointFormulaNode(String, FormulaNode<L, AP>) - Constructor for class net.automatalib.modelchecker.m3c.formula.modalmu.AbstractFixedPointFormulaNode

AbstractFormulaNode<L,AP> - Class in net.automatalib.modelchecker.m3c.formula

Abstract super-class for (sub-) formulas.

AbstractFormulaNode() - Constructor for class net.automatalib.modelchecker.m3c.formula.AbstractFormulaNode

AbstractModalFormulaNode<L,AP> - Class in net.automatalib.modelchecker.m3c.formula

Abstract super-class for modal (sub-) formulas.

AbstractModalFormulaNode(L, FormulaNode<L, AP>) - Constructor for class net.automatalib.modelchecker.m3c.formula.AbstractModalFormulaNode

AbstractPropertyTransformer<T extends AbstractPropertyTransformer<T,L,AP>,L,AP> - Class in net.automatalib.modelchecker.m3c.transformer

Base class used to represent a property transformer, i.e., a function which maps a subset of formulas to a subset of formulas.

AbstractUnaryFormulaNode<L,AP> - Class in net.automatalib.modelchecker.m3c.formula

Abstract super-class for unary (sub-) formulas.

AbstractUnaryFormulaNode(FormulaNode<L, AP>) - Constructor for class net.automatalib.modelchecker.m3c.formula.AbstractUnaryFormulaNode

accept(FormulaNodeVisitor<T, L, AP>) - Method in class net.automatalib.modelchecker.m3c.formula.AndNode

accept(FormulaNodeVisitor<T, L, AP>) - Method in class net.automatalib.modelchecker.m3c.formula.AtomicNode

accept(FormulaNodeVisitor<T, L, AP>) - Method in class net.automatalib.modelchecker.m3c.formula.BoxNode

accept(FormulaNodeVisitor<T, L, AP>) - Method in class net.automatalib.modelchecker.m3c.formula.ctl.AFNode

accept(FormulaNodeVisitor<T, L, AP>) - Method in class net.automatalib.modelchecker.m3c.formula.ctl.AGNode

accept(FormulaNodeVisitor<T, L, AP>) - Method in class net.automatalib.modelchecker.m3c.formula.ctl.AUNode

accept(FormulaNodeVisitor<T, L, AP>) - Method in class net.automatalib.modelchecker.m3c.formula.ctl.AWUNode

accept(FormulaNodeVisitor<T, L, AP>) - Method in class net.automatalib.modelchecker.m3c.formula.ctl.EFNode

accept(FormulaNodeVisitor<T, L, AP>) - Method in class net.automatalib.modelchecker.m3c.formula.ctl.EGNode

accept(FormulaNodeVisitor<T, L, AP>) - Method in class net.automatalib.modelchecker.m3c.formula.ctl.EUNode

accept(FormulaNodeVisitor<T, L, AP>) - Method in class net.automatalib.modelchecker.m3c.formula.ctl.EWUNode

accept(FormulaNodeVisitor<T, L, AP>) - Method in class net.automatalib.modelchecker.m3c.formula.DiamondNode

accept(FormulaNodeVisitor<T, L, AP>) - Method in class net.automatalib.modelchecker.m3c.formula.FalseNode

accept(FormulaNodeVisitor<T, L, AP>) - Method in interface net.automatalib.modelchecker.m3c.formula.FormulaNode

accept(FormulaNodeVisitor<T, L, AP>) - Method in class net.automatalib.modelchecker.m3c.formula.modalmu.GfpNode

accept(FormulaNodeVisitor<T, L, AP>) - Method in class net.automatalib.modelchecker.m3c.formula.modalmu.LfpNode

accept(FormulaNodeVisitor<T, L, AP>) - Method in class net.automatalib.modelchecker.m3c.formula.modalmu.VariableNode

accept(FormulaNodeVisitor<T, L, AP>) - Method in class net.automatalib.modelchecker.m3c.formula.NotNode

accept(FormulaNodeVisitor<T, L, AP>) - Method in class net.automatalib.modelchecker.m3c.formula.OrNode

accept(FormulaNodeVisitor<T, L, AP>) - Method in class net.automatalib.modelchecker.m3c.formula.TrueNode

addNode(FormulaNode<L, AP>) - Method in class net.automatalib.modelchecker.m3c.formula.EquationalBlock

addSolver(ContextFreeModalProcessSystem<String, String>) - Static method in class net.automatalib.modelchecker.m3c.solver.M3CSolvers

Returns an ADD-backed M3CSolver solver for string-based modal context-free process systems.

ADDSolver<L,AP> - Class in net.automatalib.modelchecker.m3c.solver

Implementation based on property transformers being represented by ADDs (Algebraic Decision Diagrams).

ADDSolver(ContextFreeModalProcessSystem<L, AP>) - Constructor for class net.automatalib.modelchecker.m3c.solver.ADDSolver

ADDTransformer<L,AP> - Class in net.automatalib.modelchecker.m3c.transformer

An ADDTransformer represents a property transformer for a single ADD (Algebraic Decision Diagram).

ADDTransformer(XDDManager<BooleanVector>) - Constructor for class net.automatalib.modelchecker.m3c.transformer.ADDTransformer

Creates the identity function.

ADDTransformer(XDDManager<BooleanVector>, L, TP, DependencyGraph<L, AP>) - Constructor for class net.automatalib.modelchecker.m3c.transformer.ADDTransformer

Constructor used to create the property transformer for an edge.

ADDTransformer(XDDManager<BooleanVector>, DependencyGraph<L, AP>) - Constructor for class net.automatalib.modelchecker.m3c.transformer.ADDTransformer

Constructor used to initialize the property transformer of a node.

ADDTransformerSerializer<L,AP> - Class in net.automatalib.modelchecker.m3c.transformer

This class can be used to serialize and deserialize ADDTransformers.

ADDTransformerSerializer(XDDManager<BooleanVector>) - Constructor for class net.automatalib.modelchecker.m3c.transformer.ADDTransformerSerializer

AFNode<L,AP> - Class in net.automatalib.modelchecker.m3c.formula.ctl

Java representation of a "AF" (sub-)formula.

AFNode(FormulaNode<L, AP>) - Constructor for class net.automatalib.modelchecker.m3c.formula.ctl.AFNode

AGNode<L,AP> - Class in net.automatalib.modelchecker.m3c.formula.ctl

Java representation of a "AG" (sub-)formula.

AGNode(FormulaNode<L, AP>) - Constructor for class net.automatalib.modelchecker.m3c.formula.ctl.AGNode

AndNode<L,AP> - Class in net.automatalib.modelchecker.m3c.formula

Java representation of a "&&" (sub-)formula.

AndNode(FormulaNode<L, AP>, FormulaNode<L, AP>) - Constructor for class net.automatalib.modelchecker.m3c.formula.AndNode

apply(BooleanVector) - Method in class net.automatalib.modelchecker.m3c.transformer.DiamondOperationDeadlock

apply(BooleanVector, BooleanVector) - Method in class net.automatalib.modelchecker.m3c.transformer.DiamondOperation

AtomicNode<L,AP> - Class in net.automatalib.modelchecker.m3c.formula

Java representation of an "atomic proposition" (sub-)formula.

AtomicNode(AP) - Constructor for class net.automatalib.modelchecker.m3c.formula.AtomicNode

AUNode<L,AP> - Class in net.automatalib.modelchecker.m3c.formula.ctl

Java representation of a "AU" (sub-)formula.

AUNode(FormulaNode<L, AP>, FormulaNode<L, AP>) - Constructor for class net.automatalib.modelchecker.m3c.formula.ctl.AUNode

AWUNode<L,AP> - Class in net.automatalib.modelchecker.m3c.formula.ctl

Java representation of an "AWU" (sub-)formula.

AWUNode(FormulaNode<L, AP>, FormulaNode<L, AP>) - Constructor for class net.automatalib.modelchecker.m3c.formula.ctl.AWUNode

B

bddSolver(ContextFreeModalProcessSystem<String, String>) - Static method in class net.automatalib.modelchecker.m3c.solver.M3CSolvers

Returns a BDD-backed M3CSolver solver for string-based ContextFreeModalProcessSystem.

BDDSolver<L,AP> - Class in net.automatalib.modelchecker.m3c.solver

Implementation based on property transformers being represented by BDDs (Binary Decision Diagrams).

BDDSolver(ContextFreeModalProcessSystem<L, AP>) - Constructor for class net.automatalib.modelchecker.m3c.solver.BDDSolver

BDDTransformer<L,AP> - Class in net.automatalib.modelchecker.m3c.transformer

A BDDTransformer represents a property transformer for a list of BDDs (Binary Decision Diagrams), one per subformula.

BDDTransformer(BDDManager, int) - Constructor for class net.automatalib.modelchecker.m3c.transformer.BDDTransformer

The Property Transformer representing the identity function.

BDDTransformer(BDDManager, L, TP, DependencyGraph<L, AP>) - Constructor for class net.automatalib.modelchecker.m3c.transformer.BDDTransformer

Constructor used to create the property transformer for an edge.

BDDTransformer(BDDManager, DependencyGraph<L, AP>) - Constructor for class net.automatalib.modelchecker.m3c.transformer.BDDTransformer

Constructor used to initialize the property transformer of a node.

BDDTransformerSerializer<L,AP> - Class in net.automatalib.modelchecker.m3c.transformer

This class can be used to serialize and deserialize BDDTransformers.

BDDTransformerSerializer(BDDManager) - Constructor for class net.automatalib.modelchecker.m3c.transformer.BDDTransformerSerializer

BoxNode<L,AP> - Class in net.automatalib.modelchecker.m3c.formula

Java representation of a "[]" (sub-)formula.

BoxNode(L, FormulaNode<L, AP>) - Constructor for class net.automatalib.modelchecker.m3c.formula.BoxNode

BoxNode(FormulaNode<L, AP>) - Constructor for class net.automatalib.modelchecker.m3c.formula.BoxNode

C

ColorVisualizationHelper - Class in net.automatalib.modelchecker.m3c.visualization

A VisualizationHelper for WitnessTrees that emphasizes nodes and edges of the witness and de-emphasizes the remaining ones.

ColorVisualizationHelper(WitnessTree<?, ?>) - Constructor for class net.automatalib.modelchecker.m3c.visualization.ColorVisualizationHelper

compose(ADDTransformer<L, AP>) - Method in class net.automatalib.modelchecker.m3c.transformer.ADDTransformer

compose(BDDTransformer<L, AP>) - Method in class net.automatalib.modelchecker.m3c.transformer.BDDTransformer

compose(T) - Method in class net.automatalib.modelchecker.m3c.transformer.AbstractPropertyTransformer

Returns the composition h of this and other such that h(x) = this(other(x)).

context - Variable in class net.automatalib.modelchecker.m3c.solver.WitnessTreeState

createInitTransformerEdge(DependencyGraph<L, AP>, L, TP) - Method in class net.automatalib.modelchecker.m3c.solver.ADDSolver

createInitTransformerEdge(DependencyGraph<L, AP>, L, TP) - Method in class net.automatalib.modelchecker.m3c.solver.BDDSolver

createInitTransformerEndNode(DependencyGraph<L, AP>) - Method in class net.automatalib.modelchecker.m3c.solver.ADDSolver

createInitTransformerEndNode(DependencyGraph<L, AP>) - Method in class net.automatalib.modelchecker.m3c.solver.BDDSolver

createInitTransformerNode(DependencyGraph<L, AP>) - Method in class net.automatalib.modelchecker.m3c.solver.ADDSolver

createInitTransformerNode(DependencyGraph<L, AP>) - Method in class net.automatalib.modelchecker.m3c.solver.BDDSolver

createUpdate(Set<AP>, List<ADDTransformer<L, AP>>, EquationalBlock<L, AP>) - Method in class net.automatalib.modelchecker.m3c.transformer.ADDTransformer

createUpdate(Set<AP>, List<BDDTransformer<L, AP>>, EquationalBlock<L, AP>) - Method in class net.automatalib.modelchecker.m3c.transformer.BDDTransformer

createUpdate(Set<AP>, List<T>, EquationalBlock<L, AP>) - Method in class net.automatalib.modelchecker.m3c.transformer.AbstractPropertyTransformer

Returns the updated property transformer of a node.

CTLToMuCalc<L,AP> - Class in net.automatalib.modelchecker.m3c.formula.visitor

A visitor that transforms a given CTL formula to an equivalent mu-calculus formula.

CTLToMuCalc() - Constructor for class net.automatalib.modelchecker.m3c.formula.visitor.CTLToMuCalc

currentToken - Variable in exception net.automatalib.modelchecker.m3c.formula.parser.ParseException

This is the last token that has been consumed successfully.

D

DependencyGraph<L,AP> - Class in net.automatalib.modelchecker.m3c.formula

A dependency graph is used to represent a hierarchical equational system.

DependencyGraph(FormulaNode<L, AP>) - Constructor for class net.automatalib.modelchecker.m3c.formula.DependencyGraph

deserialize(List<String>) - Method in class net.automatalib.modelchecker.m3c.transformer.ADDTransformerSerializer

deserialize(List<String>) - Method in class net.automatalib.modelchecker.m3c.transformer.BDDTransformerSerializer

deserialize(List<String>) - Method in interface net.automatalib.modelchecker.m3c.transformer.TransformerSerializer

Deserializes a given transformer from its List-based String representation.

DiamondNode<L,AP> - Class in net.automatalib.modelchecker.m3c.formula

Java representation of a "<>" (sub-)formula.

DiamondNode(L, FormulaNode<L, AP>) - Constructor for class net.automatalib.modelchecker.m3c.formula.DiamondNode

DiamondNode(FormulaNode<L, AP>) - Constructor for class net.automatalib.modelchecker.m3c.formula.DiamondNode

DiamondOperation<AP> - Class in net.automatalib.modelchecker.m3c.transformer

Implementation of the diamond function.

DiamondOperation(Set<AP>, EquationalBlock<?, AP>) - Constructor for class net.automatalib.modelchecker.m3c.transformer.DiamondOperation

DiamondOperationDeadlock<AP> - Class in net.automatalib.modelchecker.m3c.transformer

Implementation of the diamond function when the node has exactly one successor.

DiamondOperationDeadlock(Set<AP>, EquationalBlock<?, AP>) - Constructor for class net.automatalib.modelchecker.m3c.transformer.DiamondOperationDeadlock

displayLabel - Variable in class net.automatalib.modelchecker.m3c.solver.WitnessTreeState

E

edgeLabel - Variable in class net.automatalib.modelchecker.m3c.solver.WitnessTreeState

EdgeVisualizationHelper - Class in net.automatalib.modelchecker.m3c.visualization

A VisualizationHelper for WitnessTrees that emphasizes edges of the witness and de-emphasizes the remaining ones.

EdgeVisualizationHelper(WitnessTree<?, ?>) - Constructor for class net.automatalib.modelchecker.m3c.visualization.EdgeVisualizationHelper

EFNode<L,AP> - Class in net.automatalib.modelchecker.m3c.formula.ctl

Java representation of a "EF" (sub-)formula.

EFNode(FormulaNode<L, AP>) - Constructor for class net.automatalib.modelchecker.m3c.formula.ctl.EFNode

EGNode<L,AP> - Class in net.automatalib.modelchecker.m3c.formula.ctl

Java representation of a "EG" (sub-)formula.

EGNode(FormulaNode<L, AP>) - Constructor for class net.automatalib.modelchecker.m3c.formula.ctl.EGNode

EOL - Static variable in exception net.automatalib.modelchecker.m3c.formula.parser.ParseException

The end of line string for this machine.

equals(Object) - Method in class net.automatalib.modelchecker.m3c.formula.AbstractBinaryFormulaNode

equals(Object) - Method in class net.automatalib.modelchecker.m3c.formula.AbstractFormulaNode

equals(Object) - Method in class net.automatalib.modelchecker.m3c.formula.AbstractModalFormulaNode

equals(Object) - Method in class net.automatalib.modelchecker.m3c.formula.AbstractUnaryFormulaNode

equals(Object) - Method in class net.automatalib.modelchecker.m3c.formula.AtomicNode

equals(Object) - Method in class net.automatalib.modelchecker.m3c.formula.modalmu.AbstractFixedPointFormulaNode

equals(Object) - Method in class net.automatalib.modelchecker.m3c.formula.modalmu.VariableNode

equals(Object) - Method in class net.automatalib.modelchecker.m3c.transformer.ADDTransformer

equals(Object) - Method in class net.automatalib.modelchecker.m3c.transformer.BDDTransformer

EquationalBlock<L,AP> - Class in net.automatalib.modelchecker.m3c.formula

Represents an equational block that aggregates its reference formula nodes.

EquationalBlock(boolean) - Constructor for class net.automatalib.modelchecker.m3c.formula.EquationalBlock

EUNode<L,AP> - Class in net.automatalib.modelchecker.m3c.formula.ctl

Java representation of a "EU" (sub-)formula.

EUNode(FormulaNode<L, AP>, FormulaNode<L, AP>) - Constructor for class net.automatalib.modelchecker.m3c.formula.ctl.EUNode

evaluate(boolean[]) - Method in class net.automatalib.modelchecker.m3c.transformer.AbstractPropertyTransformer

Returns the set of variable numbers of subformulas y with f(input)=y, where f is the property transformer represented by this.

evaluate(boolean[]) - Method in class net.automatalib.modelchecker.m3c.transformer.ADDTransformer

evaluate(boolean[]) - Method in class net.automatalib.modelchecker.m3c.transformer.BDDTransformer

EWUNode<L,AP> - Class in net.automatalib.modelchecker.m3c.formula.ctl

Java representation of a "EWU" (sub-)formula.

EWUNode(FormulaNode<L, AP>, FormulaNode<L, AP>) - Constructor for class net.automatalib.modelchecker.m3c.formula.ctl.EWUNode

expectedTokenSequences - Variable in exception net.automatalib.modelchecker.m3c.formula.parser.ParseException

Each entry in this array is an array of integers.

F

FalseNode<L,AP> - Class in net.automatalib.modelchecker.m3c.formula

Java representation of a "false" (sub-)formula.

FalseNode() - Constructor for class net.automatalib.modelchecker.m3c.formula.FalseNode

FormulaNode<L,AP> - Interface in net.automatalib.modelchecker.m3c.formula

Generic interface for formulas return by M3CParsers.

FormulaNodeVisitor<T,L,AP> - Interface in net.automatalib.modelchecker.m3c.formula.visitor

G

getAction() - Method in class net.automatalib.modelchecker.m3c.formula.AbstractModalFormulaNode

getAdd() - Method in class net.automatalib.modelchecker.m3c.transformer.ADDTransformer

Returns the ADD which represents the property transformer.

getAST() - Method in class net.automatalib.modelchecker.m3c.formula.DependencyGraph

Returns the abstract syntax tree of the input formula after it has been transformed into negation normal form.

getBDD(int) - Method in class net.automatalib.modelchecker.m3c.transformer.BDDTransformer

Returns the BDD used to compute the satisfiability of subformula with variable number var.

getBlock(int) - Method in class net.automatalib.modelchecker.m3c.formula.DependencyGraph

Returns the equational block for the given index.

getBlocks() - Method in class net.automatalib.modelchecker.m3c.formula.DependencyGraph

Returns all equational blocks of the equational system.

getChild() - Method in class net.automatalib.modelchecker.m3c.formula.AbstractUnaryFormulaNode

getCompositions(TransformerSerializer<T, L, AP>) - Method in class net.automatalib.modelchecker.m3c.solver.SolverState

Returns a List of the property transformers representing the compositions of the property transformer of the outgoing edges and their target nodes.

getData() - Method in class net.automatalib.modelchecker.m3c.solver.SolverHistory

Returns a Map containing information per procedure name.

getEdgeProperties(Integer, CompactEdge<String>, Integer, Map<String, String>) - Method in class net.automatalib.modelchecker.m3c.visualization.ColorVisualizationHelper

getEdgeProperties(Integer, CompactEdge<String>, Integer, Map<String, String>) - Method in class net.automatalib.modelchecker.m3c.visualization.EdgeVisualizationHelper

getFormulaNodes() - Method in class net.automatalib.modelchecker.m3c.formula.DependencyGraph

Returns the list of all subformulas.

getInitialPropertyTransformers(TransformerSerializer<T, L, AP>) - Method in class net.automatalib.modelchecker.m3c.solver.SolverData

Returns a Mapping which maps nodes to their initial property transformer.

getInitialSatisfiedSubformulas() - Method in class net.automatalib.modelchecker.m3c.solver.SolverData

Returns a Mapping which contains the list of the initial satisfied subformulas for each node of the ProceduralModalProcessGraph whose data is stored in an instance of this class.

getLeftChild() - Method in class net.automatalib.modelchecker.m3c.formula.AbstractBinaryFormulaNode

getMayTransformers(TransformerSerializer<T, L, AP>) - Method in class net.automatalib.modelchecker.m3c.solver.SolverHistory

Returns a Map which maps the edge label of may edges to their property transformer.

getMustTransformers(TransformerSerializer<T, L, AP>) - Method in class net.automatalib.modelchecker.m3c.solver.SolverHistory

Returns a Map which maps the edge label of must edges to their property transformer.

getNodeIDs() - Method in class net.automatalib.modelchecker.m3c.solver.SolverData

Returns the NodeIDs of the ProceduralModalProcessGraph returned by SolverData.getPmpg().

getNodeProperties(Integer, Map<String, String>) - Method in class net.automatalib.modelchecker.m3c.visualization.ColorVisualizationHelper

getNodeProperties(Integer, Map<String, String>) - Method in class net.automatalib.modelchecker.m3c.visualization.HTMLVisualizationHelper

getNodeProperties(Integer, Map<String, String>) - Method in class net.automatalib.modelchecker.m3c.visualization.NodeVisualizationHelper

getNodes() - Method in class net.automatalib.modelchecker.m3c.formula.EquationalBlock

getNumberOfVars() - Method in class net.automatalib.modelchecker.m3c.transformer.BDDTransformer

Returns the number of subformulas.

getNumVariables() - Method in class net.automatalib.modelchecker.m3c.formula.DependencyGraph

Returns the number of variables which is equal to the number of subformulas.

getPmpg() - Method in class net.automatalib.modelchecker.m3c.solver.SolverData

Returns the ProceduralModalProcessGraph whose data is stored in an instance of this class.

getProposition() - Method in class net.automatalib.modelchecker.m3c.formula.AtomicNode

getRightChild() - Method in class net.automatalib.modelchecker.m3c.formula.AbstractBinaryFormulaNode

getSerializer() - Method in class net.automatalib.modelchecker.m3c.solver.ADDSolver

getSerializer() - Method in class net.automatalib.modelchecker.m3c.solver.BDDSolver

getSolverStates() - Method in class net.automatalib.modelchecker.m3c.solver.SolverHistory

Returns the list of SolverStates, one per update of a node.

getUpdatedNode() - Method in class net.automatalib.modelchecker.m3c.solver.SolverState

Returns the node updated in this step.

getUpdatedNodePMPG() - Method in class net.automatalib.modelchecker.m3c.solver.SolverState

Returns the name of the ProceduralModalProcessGraph which contains the node updated in this step.

getUpdatedNodeSatisfiedSubformula() - Method in class net.automatalib.modelchecker.m3c.solver.SolverState

Returns the list of satisfied subformulas the node updated in this step satisfies after the update.

getUpdatedPropTransformer(TransformerSerializer<T, L, AP>) - Method in class net.automatalib.modelchecker.m3c.solver.SolverState

Returns the updated property transformer.

getVariable() - Method in class net.automatalib.modelchecker.m3c.formula.modalmu.AbstractFixedPointFormulaNode

getVariable() - Method in class net.automatalib.modelchecker.m3c.formula.modalmu.VariableNode

getVarNumber() - Method in class net.automatalib.modelchecker.m3c.formula.AbstractFormulaNode

getVarNumber() - Method in interface net.automatalib.modelchecker.m3c.formula.FormulaNode

getVarNumberChild() - Method in class net.automatalib.modelchecker.m3c.formula.AbstractUnaryFormulaNode

getVarNumberLeft() - Method in class net.automatalib.modelchecker.m3c.formula.AbstractBinaryFormulaNode

getVarNumberRight() - Method in class net.automatalib.modelchecker.m3c.formula.AbstractBinaryFormulaNode

getWitness() - Method in class net.automatalib.modelchecker.m3c.solver.WitnessTree

getWorkSet() - Method in class net.automatalib.modelchecker.m3c.solver.SolverState

Returns a Map which returns the set of nodes which are in the work set for each procedure after the update.

GfpNode<L,AP> - Class in net.automatalib.modelchecker.m3c.formula.modalmu

Java representation of a "nu" (sub-)formula.

GfpNode(String, FormulaNode<L, AP>) - Constructor for class net.automatalib.modelchecker.m3c.formula.modalmu.GfpNode

H

hashCode() - Method in class net.automatalib.modelchecker.m3c.formula.AbstractBinaryFormulaNode

hashCode() - Method in class net.automatalib.modelchecker.m3c.formula.AbstractFormulaNode

hashCode() - Method in class net.automatalib.modelchecker.m3c.formula.AbstractModalFormulaNode

hashCode() - Method in class net.automatalib.modelchecker.m3c.formula.AbstractUnaryFormulaNode

hashCode() - Method in class net.automatalib.modelchecker.m3c.formula.AtomicNode

hashCode() - Method in class net.automatalib.modelchecker.m3c.formula.modalmu.AbstractFixedPointFormulaNode

hashCode() - Method in class net.automatalib.modelchecker.m3c.formula.modalmu.VariableNode

hashCode() - Method in class net.automatalib.modelchecker.m3c.transformer.ADDTransformer

hashCode() - Method in class net.automatalib.modelchecker.m3c.transformer.BDDTransformer

HTMLVisualizationHelper - Class in net.automatalib.modelchecker.m3c.visualization

A VisualizationHelper for WitnessTrees that renders the node labels as an HTML-based table.

HTMLVisualizationHelper(WitnessTree<?, ?>) - Constructor for class net.automatalib.modelchecker.m3c.visualization.HTMLVisualizationHelper

HTMLVisualizationHelper(WitnessTree<?, ?>, boolean) - Constructor for class net.automatalib.modelchecker.m3c.visualization.HTMLVisualizationHelper

I

initDDManager(DependencyGraph<L, AP>) - Method in class net.automatalib.modelchecker.m3c.solver.ADDSolver

initDDManager(DependencyGraph<L, AP>) - Method in class net.automatalib.modelchecker.m3c.solver.BDDSolver

isIdentity() - Method in class net.automatalib.modelchecker.m3c.transformer.ADDTransformer

Returns whether the property transformer is the identity function.

isMaxBlock() - Method in class net.automatalib.modelchecker.m3c.formula.EquationalBlock

isMust() - Method in class net.automatalib.modelchecker.m3c.transformer.AbstractPropertyTransformer

Returns whether the property transformer belongs to a node or to a must edge.

isPartOfResult - Variable in class net.automatalib.modelchecker.m3c.solver.WitnessTreeState

isSat() - Method in class net.automatalib.modelchecker.m3c.solver.SolverHistory

Returns whether the formula put into AbstractDDSolver.solveAndRecordHistory(FormulaNode) is satisfied.

L

LfpNode<L,AP> - Class in net.automatalib.modelchecker.m3c.formula.modalmu

Java representation of a "mu" (sub-)formula.

LfpNode(String, FormulaNode<L, AP>) - Constructor for class net.automatalib.modelchecker.m3c.formula.modalmu.LfpNode

M

M3CParser - Class in net.automatalib.modelchecker.m3c.formula.parser

This class can be used to parse formulas in CTL and the mu-calculus.

M3CSolver<F> - Interface in net.automatalib.modelchecker.m3c.solver

An interface for a generic M3C solver which may need to parse the given formula and thus may throw an exception when doing so.

M3CSolver.TypedM3CSolver<F> - Interface in net.automatalib.modelchecker.m3c.solver

A specialized M3CSolver which no longer throws a ParseException when solving a formula, but requires a type-safe formula object.

M3CSolvers - Class in net.automatalib.modelchecker.m3c.solver

A factory for constructing M3CSolvers depending on the given ContextFreeModalProcessSystem.

N

net.automatalib.modelchecker.m3c - package net.automatalib.modelchecker.m3c

This package (and sub-packages) provides the implementation of the model checker presented in the paper M3C: Modal Meta Model Checking by Bernhard Steffen and Alnis Murtovi.

net.automatalib.modelchecker.m3c.formula - package net.automatalib.modelchecker.m3c.formula

net.automatalib.modelchecker.m3c.formula.ctl - package net.automatalib.modelchecker.m3c.formula.ctl

net.automatalib.modelchecker.m3c.formula.modalmu - package net.automatalib.modelchecker.m3c.formula.modalmu

net.automatalib.modelchecker.m3c.formula.parser - package net.automatalib.modelchecker.m3c.formula.parser

net.automatalib.modelchecker.m3c.formula.visitor - package net.automatalib.modelchecker.m3c.formula.visitor

net.automatalib.modelchecker.m3c.solver - package net.automatalib.modelchecker.m3c.solver

net.automatalib.modelchecker.m3c.transformer - package net.automatalib.modelchecker.m3c.transformer

net.automatalib.modelchecker.m3c.visualization - package net.automatalib.modelchecker.m3c.visualization

NNFVisitor<L,AP> - Class in net.automatalib.modelchecker.m3c.formula.visitor

A visitor that transforms a given mu-calculus or CTL formula to negation-normal-form.

NNFVisitor() - Constructor for class net.automatalib.modelchecker.m3c.formula.visitor.NNFVisitor

NodeVisualizationHelper - Class in net.automatalib.modelchecker.m3c.visualization

A VisualizationHelper for WitnessTrees that emphasizes nodes of the witness and de-emphasizes the remaining ones.

NodeVisualizationHelper(WitnessTree<?, ?>) - Constructor for class net.automatalib.modelchecker.m3c.visualization.NodeVisualizationHelper

NotNode<L,AP> - Class in net.automatalib.modelchecker.m3c.formula

Java representation of a "!"

NotNode(FormulaNode<L, AP>) - Constructor for class net.automatalib.modelchecker.m3c.formula.NotNode

O

OrNode<L,AP> - Class in net.automatalib.modelchecker.m3c.formula

Java representation of a "||" (sub-)formula.

OrNode(FormulaNode<L, AP>, FormulaNode<L, AP>) - Constructor for class net.automatalib.modelchecker.m3c.formula.OrNode

P

parentId - Variable in class net.automatalib.modelchecker.m3c.solver.WitnessTreeState

parse(String) - Static method in class net.automatalib.modelchecker.m3c.formula.parser.M3CParser

Returns the abstract syntax tree of a given formula.

parse(String, Function<String, L>, Function<String, AP>) - Static method in class net.automatalib.modelchecker.m3c.formula.parser.M3CParser

Returns the abstract syntax tree of a given formula.

ParseException - Exception in net.automatalib.modelchecker.m3c.formula.parser

This exception is thrown when parse errors are encountered.

ParseException() - Constructor for exception net.automatalib.modelchecker.m3c.formula.parser.ParseException

The following constructors are for use by you for whatever purpose you can think of.

ParseException(String) - Constructor for exception net.automatalib.modelchecker.m3c.formula.parser.ParseException

Constructor with message.

ParseException(Token, int[][], String[]) - Constructor for exception net.automatalib.modelchecker.m3c.formula.parser.ParseException

This constructor is used by the method "generateParseException" in the generated parser.

pmpg - Variable in class net.automatalib.modelchecker.m3c.solver.WitnessTreeState

print(Appendable) - Method in class net.automatalib.modelchecker.m3c.formula.AndNode

print(Appendable) - Method in class net.automatalib.modelchecker.m3c.formula.AtomicNode

print(Appendable) - Method in class net.automatalib.modelchecker.m3c.formula.BoxNode

print(Appendable) - Method in class net.automatalib.modelchecker.m3c.formula.ctl.AFNode

print(Appendable) - Method in class net.automatalib.modelchecker.m3c.formula.ctl.AGNode

print(Appendable) - Method in class net.automatalib.modelchecker.m3c.formula.ctl.AUNode

print(Appendable) - Method in class net.automatalib.modelchecker.m3c.formula.ctl.AWUNode

print(Appendable) - Method in class net.automatalib.modelchecker.m3c.formula.ctl.EFNode

print(Appendable) - Method in class net.automatalib.modelchecker.m3c.formula.ctl.EGNode

print(Appendable) - Method in class net.automatalib.modelchecker.m3c.formula.ctl.EUNode

print(Appendable) - Method in class net.automatalib.modelchecker.m3c.formula.ctl.EWUNode

print(Appendable) - Method in class net.automatalib.modelchecker.m3c.formula.DiamondNode

print(Appendable) - Method in class net.automatalib.modelchecker.m3c.formula.FalseNode

print(Appendable) - Method in class net.automatalib.modelchecker.m3c.formula.modalmu.GfpNode

print(Appendable) - Method in class net.automatalib.modelchecker.m3c.formula.modalmu.LfpNode

print(Appendable) - Method in class net.automatalib.modelchecker.m3c.formula.modalmu.VariableNode

print(Appendable) - Method in class net.automatalib.modelchecker.m3c.formula.NotNode

print(Appendable) - Method in class net.automatalib.modelchecker.m3c.formula.OrNode

print(Appendable) - Method in class net.automatalib.modelchecker.m3c.formula.TrueNode

printBinaryFormulaNode(Appendable, String) - Method in class net.automatalib.modelchecker.m3c.formula.AbstractBinaryFormulaNode

printMuCalcNode(Appendable, char, char) - Method in class net.automatalib.modelchecker.m3c.formula.AbstractModalFormulaNode

printMuCalcNode(Appendable, String) - Method in class net.automatalib.modelchecker.m3c.formula.modalmu.AbstractFixedPointFormulaNode

printUnaryFormulaNode(Appendable, String) - Method in class net.automatalib.modelchecker.m3c.formula.AbstractUnaryFormulaNode

printUntilNode(Appendable, char, char) - Method in class net.automatalib.modelchecker.m3c.formula.AbstractBinaryFormulaNode

procedure - Variable in class net.automatalib.modelchecker.m3c.solver.WitnessTreeState

S

serialize(ADDTransformer<L, AP>) - Method in class net.automatalib.modelchecker.m3c.transformer.ADDTransformerSerializer

serialize(BDDTransformer<L, AP>) - Method in class net.automatalib.modelchecker.m3c.transformer.BDDTransformerSerializer

serialize(T) - Method in interface net.automatalib.modelchecker.m3c.transformer.TransformerSerializer

Serializes a given transformer to List-based String representation.

setVarNumber(int) - Method in class net.automatalib.modelchecker.m3c.formula.AbstractFormulaNode

setVarNumber(int) - Method in interface net.automatalib.modelchecker.m3c.formula.FormulaNode

shutdownDDManager() - Method in class net.automatalib.modelchecker.m3c.solver.ADDSolver

shutdownDDManager() - Method in class net.automatalib.modelchecker.m3c.solver.BDDSolver

solve(F) - Method in interface net.automatalib.modelchecker.m3c.solver.M3CSolver

Checks whether the given formula is satisfied.

solve(F) - Method in interface net.automatalib.modelchecker.m3c.solver.M3CSolver.TypedM3CSolver

Checks whether the given formula is satisfied.

solve(String) - Method in class net.automatalib.modelchecker.m3c.solver.StringADDSolver

solve(String) - Method in class net.automatalib.modelchecker.m3c.solver.StringBDDSolver

solver(ContextFreeModalProcessSystem<String, String>) - Static method in class net.automatalib.modelchecker.m3c.solver.M3CSolvers

Returns a default M3CSolver solver for string-based modal context-free process systems.

SolverData<N,T extends AbstractPropertyTransformer<T,L,AP>,L,AP> - Class in net.automatalib.modelchecker.m3c.solver

A class used to store ProceduralModalProcessGraph-specific data for the SolverHistory.

SolverHistory<T extends AbstractPropertyTransformer<T,L,AP>,L,AP> - Class in net.automatalib.modelchecker.m3c.solver

A class used to store internal information produced by AbstractDDSolver.solveAndRecordHistory(net.automatalib.modelchecker.m3c.formula.FormulaNode<L, AP>) while checking the satisfiability of a formula.

SolverState<N,T extends AbstractPropertyTransformer<T,L,AP>,L,AP> - Class in net.automatalib.modelchecker.m3c.solver

Stores internal information produced during the update of a node in AbstractDDSolver.

stack - Variable in class net.automatalib.modelchecker.m3c.solver.WitnessTreeState

state - Variable in class net.automatalib.modelchecker.m3c.solver.WitnessTreeState

StringADDSolver - Class in net.automatalib.modelchecker.m3c.solver

An ADD solver for generic, string-based formulas.

StringBDDSolver - Class in net.automatalib.modelchecker.m3c.solver

A BDD solver for generic, string-based formulas.

subformula - Variable in class net.automatalib.modelchecker.m3c.solver.WitnessTreeState

T

toBoolArray(BitSet) - Method in class net.automatalib.modelchecker.m3c.formula.DependencyGraph

Returns a boolean array that is sized according to DependencyGraph.getNumVariables() such that every index provided in satisfiedVars is set to true.

tokenImage - Variable in exception net.automatalib.modelchecker.m3c.formula.parser.ParseException

This is a reference to the "tokenImage" array of the generated parser within which the parse error occurred.

toMuCalc(FormulaNode<L, AP>) - Method in class net.automatalib.modelchecker.m3c.formula.visitor.CTLToMuCalc

toNNF() - Method in interface net.automatalib.modelchecker.m3c.formula.FormulaNode

TransformerSerializer<T extends AbstractPropertyTransformer<T,L,AP>,L,AP> - Interface in net.automatalib.modelchecker.m3c.transformer

Utility interface for serializing AbstractPropertyTransformer implementations.

transformToNNF(FormulaNode<L, AP>) - Method in class net.automatalib.modelchecker.m3c.formula.visitor.NNFVisitor

TrueNode<L,AP> - Class in net.automatalib.modelchecker.m3c.formula

Java representation of a "true" (sub-)formula.

TrueNode() - Constructor for class net.automatalib.modelchecker.m3c.formula.TrueNode

typedADDSolver(ContextFreeModalProcessSystem<L, AP>) - Static method in class net.automatalib.modelchecker.m3c.solver.M3CSolvers

Returns an ADD-backed M3CSolver.TypedM3CSolver solver for strongly-typed modal context-free process systems.

TypedADDSolver<L,AP> - Class in net.automatalib.modelchecker.m3c.solver

An ADD solver for strongly-typed formulas.

typedBDDSolver(ContextFreeModalProcessSystem<L, AP>) - Static method in class net.automatalib.modelchecker.m3c.solver.M3CSolvers

Returns a BDD-backed M3CSolver.TypedM3CSolver solver for strongly-typed ContextFreeModalProcessSystem.

TypedBDDSolver<L,AP> - Class in net.automatalib.modelchecker.m3c.solver

A BDD solver for strongly-typed formulas.

typedSolver(ContextFreeModalProcessSystem<L, AP>) - Static method in class net.automatalib.modelchecker.m3c.solver.M3CSolvers

Returns a default M3CSolver.TypedM3CSolver solver for strongly-typed modal context-free process systems.

U

unit - Variable in class net.automatalib.modelchecker.m3c.solver.WitnessTreeState

V

VariableNode<L,AP> - Class in net.automatalib.modelchecker.m3c.formula.modalmu

Java representation of an "X" (sub-)formula.

VariableNode(String) - Constructor for class net.automatalib.modelchecker.m3c.formula.modalmu.VariableNode

visit(AndNode<L, AP>) - Method in class net.automatalib.modelchecker.m3c.formula.visitor.CTLToMuCalc

visit(AndNode<L, AP>) - Method in interface net.automatalib.modelchecker.m3c.formula.visitor.FormulaNodeVisitor

visit(AtomicNode<L, AP>) - Method in class net.automatalib.modelchecker.m3c.formula.visitor.CTLToMuCalc

visit(AtomicNode<L, AP>) - Method in interface net.automatalib.modelchecker.m3c.formula.visitor.FormulaNodeVisitor

visit(BoxNode<L, AP>) - Method in class net.automatalib.modelchecker.m3c.formula.visitor.CTLToMuCalc

visit(BoxNode<L, AP>) - Method in interface net.automatalib.modelchecker.m3c.formula.visitor.FormulaNodeVisitor

visit(AFNode<L, AP>) - Method in class net.automatalib.modelchecker.m3c.formula.visitor.CTLToMuCalc

visit(AFNode<L, AP>) - Method in interface net.automatalib.modelchecker.m3c.formula.visitor.FormulaNodeVisitor

visit(AGNode<L, AP>) - Method in class net.automatalib.modelchecker.m3c.formula.visitor.CTLToMuCalc

visit(AGNode<L, AP>) - Method in interface net.automatalib.modelchecker.m3c.formula.visitor.FormulaNodeVisitor

visit(AUNode<L, AP>) - Method in class net.automatalib.modelchecker.m3c.formula.visitor.CTLToMuCalc

visit(AUNode<L, AP>) - Method in interface net.automatalib.modelchecker.m3c.formula.visitor.FormulaNodeVisitor

visit(AWUNode<L, AP>) - Method in class net.automatalib.modelchecker.m3c.formula.visitor.CTLToMuCalc

visit(AWUNode<L, AP>) - Method in interface net.automatalib.modelchecker.m3c.formula.visitor.FormulaNodeVisitor

visit(EFNode<L, AP>) - Method in class net.automatalib.modelchecker.m3c.formula.visitor.CTLToMuCalc

visit(EFNode<L, AP>) - Method in interface net.automatalib.modelchecker.m3c.formula.visitor.FormulaNodeVisitor

visit(EGNode<L, AP>) - Method in class net.automatalib.modelchecker.m3c.formula.visitor.CTLToMuCalc

visit(EGNode<L, AP>) - Method in interface net.automatalib.modelchecker.m3c.formula.visitor.FormulaNodeVisitor

visit(EUNode<L, AP>) - Method in class net.automatalib.modelchecker.m3c.formula.visitor.CTLToMuCalc

visit(EUNode<L, AP>) - Method in interface net.automatalib.modelchecker.m3c.formula.visitor.FormulaNodeVisitor

visit(EWUNode<L, AP>) - Method in class net.automatalib.modelchecker.m3c.formula.visitor.CTLToMuCalc

visit(EWUNode<L, AP>) - Method in interface net.automatalib.modelchecker.m3c.formula.visitor.FormulaNodeVisitor

visit(DiamondNode<L, AP>) - Method in class net.automatalib.modelchecker.m3c.formula.visitor.CTLToMuCalc

visit(DiamondNode<L, AP>) - Method in interface net.automatalib.modelchecker.m3c.formula.visitor.FormulaNodeVisitor

visit(FalseNode<L, AP>) - Method in class net.automatalib.modelchecker.m3c.formula.visitor.CTLToMuCalc

visit(FalseNode<L, AP>) - Method in interface net.automatalib.modelchecker.m3c.formula.visitor.FormulaNodeVisitor

visit(FormulaNode<L, AP>) - Method in class net.automatalib.modelchecker.m3c.formula.visitor.CTLToMuCalc

visit(FormulaNode<L, AP>) - Method in interface net.automatalib.modelchecker.m3c.formula.visitor.FormulaNodeVisitor

visit(GfpNode<L, AP>) - Method in class net.automatalib.modelchecker.m3c.formula.visitor.CTLToMuCalc

visit(GfpNode<L, AP>) - Method in interface net.automatalib.modelchecker.m3c.formula.visitor.FormulaNodeVisitor

visit(LfpNode<L, AP>) - Method in class net.automatalib.modelchecker.m3c.formula.visitor.CTLToMuCalc

visit(LfpNode<L, AP>) - Method in interface net.automatalib.modelchecker.m3c.formula.visitor.FormulaNodeVisitor

visit(VariableNode<L, AP>) - Method in class net.automatalib.modelchecker.m3c.formula.visitor.CTLToMuCalc

visit(VariableNode<L, AP>) - Method in interface net.automatalib.modelchecker.m3c.formula.visitor.FormulaNodeVisitor

visit(NotNode<L, AP>) - Method in class net.automatalib.modelchecker.m3c.formula.visitor.CTLToMuCalc

visit(NotNode<L, AP>) - Method in interface net.automatalib.modelchecker.m3c.formula.visitor.FormulaNodeVisitor

visit(OrNode<L, AP>) - Method in class net.automatalib.modelchecker.m3c.formula.visitor.CTLToMuCalc

visit(OrNode<L, AP>) - Method in interface net.automatalib.modelchecker.m3c.formula.visitor.FormulaNodeVisitor

visit(TrueNode<L, AP>) - Method in class net.automatalib.modelchecker.m3c.formula.visitor.CTLToMuCalc

visit(TrueNode<L, AP>) - Method in interface net.automatalib.modelchecker.m3c.formula.visitor.FormulaNodeVisitor

W

WitnessTree<L,AP> - Class in net.automatalib.modelchecker.m3c.solver

A tree-like Graph that represents the BFS-style exploration of the tableau generated by the WitnessTreeExtractor.

WitnessTree() - Constructor for class net.automatalib.modelchecker.m3c.solver.WitnessTree

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

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

A B C D E F G H I L M N O P S T U V W
All Classes All Packages