Uses of Interface
net.automatalib.modelchecker.m3c.formula.FormulaNode

Packages that use FormulaNode

Package	Description
net.automatalib.modelchecker.m3c.formula
net.automatalib.modelchecker.m3c.formula.ctl
net.automatalib.modelchecker.m3c.formula.modalmu
net.automatalib.modelchecker.m3c.formula.parser
net.automatalib.modelchecker.m3c.formula.visitor
net.automatalib.modelchecker.m3c.solver

Uses of FormulaNode in net.automatalib.modelchecker.m3c.formula

Classes in net.automatalib.modelchecker.m3c.formula that implement FormulaNode

Modifier and Type	Class	Description
class	AbstractBinaryFormulaNode<L,AP>	Abstract super-class for binary (sub-) formulas.
class	AbstractFormulaNode<L,AP>	Abstract super-class for (sub-) formulas.
class	AbstractModalFormulaNode<L,AP>	Abstract super-class for modal (sub-) formulas.
class	AbstractUnaryFormulaNode<L,AP>	Abstract super-class for unary (sub-) formulas.
class	AndNode<L,AP>	Java representation of a "&&" (sub-)formula.
class	AtomicNode<L,AP>	Java representation of an "atomic proposition" (sub-)formula.
class	BoxNode<L,AP>	Java representation of a "[]" (sub-)formula.
class	DiamondNode<L,AP>	Java representation of a "<>" (sub-)formula.
class	FalseNode<L,AP>	Java representation of a "false" (sub-)formula.
class	NotNode<L,AP>	Java representation of a "!"
class	OrNode<L,AP>	Java representation of a "||" (sub-)formula.
class	TrueNode<L,AP>	Java representation of a "true" (sub-)formula.

Methods in net.automatalib.modelchecker.m3c.formula that return FormulaNode

Modifier and Type	Method	Description
FormulaNode<L,AP>	DependencyGraph.getAST()	Returns the abstract syntax tree of the input formula after it has been transformed into negation normal form.
FormulaNode<L,AP>	AbstractUnaryFormulaNode.getChild()
FormulaNode<L,AP>	AbstractBinaryFormulaNode.getLeftChild()
FormulaNode<L,AP>	AbstractBinaryFormulaNode.getRightChild()
default FormulaNode<L,AP>	FormulaNode.toNNF()

Methods in net.automatalib.modelchecker.m3c.formula that return types with arguments of type FormulaNode

Modifier and Type	Method	Description
List<FormulaNode<L,AP>>	DependencyGraph.getFormulaNodes()	Returns the list of all subformulas.
List<FormulaNode<L,AP>>	EquationalBlock.getNodes()

Methods in net.automatalib.modelchecker.m3c.formula with parameters of type FormulaNode

Modifier and Type	Method	Description
void	EquationalBlock.addNode(FormulaNode<L,AP> node)

Constructors in net.automatalib.modelchecker.m3c.formula with parameters of type FormulaNode

Constructor	Description
AbstractBinaryFormulaNode(FormulaNode<L,AP> leftChild, FormulaNode<L,AP> rightChild)
AbstractModalFormulaNode(@Nullable L action, FormulaNode<L,AP> node)
AbstractUnaryFormulaNode(FormulaNode<L,AP> child)
AndNode(FormulaNode<L,AP> leftChild, FormulaNode<L,AP> rightChild)
BoxNode(@Nullable L action, FormulaNode<L,AP> node)
BoxNode(FormulaNode<L,AP> node)
DependencyGraph(FormulaNode<L,AP> root)
DiamondNode(@Nullable L action, FormulaNode<L,AP> node)
DiamondNode(FormulaNode<L,AP> node)
NotNode(FormulaNode<L,AP> node)
OrNode(FormulaNode<L,AP> leftChild, FormulaNode<L,AP> rightChild)

Uses of FormulaNode in net.automatalib.modelchecker.m3c.formula.ctl

Classes in net.automatalib.modelchecker.m3c.formula.ctl that implement FormulaNode

Modifier and Type	Class	Description
class	AFNode<L,AP>	Java representation of a "AF" (sub-)formula.
class	AGNode<L,AP>	Java representation of a "AG" (sub-)formula.
class	AUNode<L,AP>	Java representation of a "AU" (sub-)formula.
class	AWUNode<L,AP>	Java representation of an "AWU" (sub-)formula.
class	EFNode<L,AP>	Java representation of a "EF" (sub-)formula.
class	EGNode<L,AP>	Java representation of a "EG" (sub-)formula.
class	EUNode<L,AP>	Java representation of a "EU" (sub-)formula.
class	EWUNode<L,AP>	Java representation of a "EWU" (sub-)formula.

Constructors in net.automatalib.modelchecker.m3c.formula.ctl with parameters of type FormulaNode

Constructor	Description
AFNode(FormulaNode<L,AP> childNode)
AGNode(FormulaNode<L,AP> node)
AUNode(FormulaNode<L,AP> leftChild, FormulaNode<L,AP> rightChild)
AWUNode(FormulaNode<L,AP> leftChild, FormulaNode<L,AP> rightChild)
EFNode(FormulaNode<L,AP> node)
EGNode(FormulaNode<L,AP> node)
EUNode(FormulaNode<L,AP> leftChild, FormulaNode<L,AP> rightChild)
EWUNode(FormulaNode<L,AP> leftChild, FormulaNode<L,AP> rightChild)

Uses of FormulaNode in net.automatalib.modelchecker.m3c.formula.modalmu

Classes in net.automatalib.modelchecker.m3c.formula.modalmu that implement FormulaNode

Modifier and Type	Class	Description
class	AbstractFixedPointFormulaNode<L,AP>	Abstract super-class for fix-point (sub-) formulas.
class	GfpNode<L,AP>	Java representation of a "nu" (sub-)formula.
class	LfpNode<L,AP>	Java representation of a "mu" (sub-)formula.
class	VariableNode<L,AP>	Java representation of an "X" (sub-)formula.

Constructors in net.automatalib.modelchecker.m3c.formula.modalmu with parameters of type FormulaNode

Constructor	Description
AbstractFixedPointFormulaNode(String variable, FormulaNode<L,AP> child)
GfpNode(String variable, FormulaNode<L,AP> node)
LfpNode(String variable, FormulaNode<L,AP> node)

Uses of FormulaNode in net.automatalib.modelchecker.m3c.formula.parser

Methods in net.automatalib.modelchecker.m3c.formula.parser that return FormulaNode

Modifier and Type	Method	Description
static FormulaNode<String,String>	M3CParser.parse(String formula)	Returns the abstract syntax tree of a given formula.
static <L,AP> FormulaNode<L,AP>	M3CParser.parse(String formula, Function<String,L> labelParser, Function<String,AP> apParser)	Returns the abstract syntax tree of a given formula.

Uses of FormulaNode in net.automatalib.modelchecker.m3c.formula.visitor

Methods in net.automatalib.modelchecker.m3c.formula.visitor that return FormulaNode

Modifier and Type	Method	Description
FormulaNode<L,AP>	CTLToMuCalc.toMuCalc(FormulaNode<L,AP> ctlFormula)
FormulaNode<L,AP>	NNFVisitor.transformToNNF(FormulaNode<L,AP> node)
FormulaNode<L,AP>	CTLToMuCalc.visit(AndNode<L,AP> node)
FormulaNode<L,AP>	CTLToMuCalc.visit(AtomicNode<L,AP> node)
FormulaNode<L,AP>	CTLToMuCalc.visit(BoxNode<L,AP> node)
FormulaNode<L,AP>	CTLToMuCalc.visit(AFNode<L,AP> node)
FormulaNode<L,AP>	CTLToMuCalc.visit(AGNode<L,AP> node)
FormulaNode<L,AP>	CTLToMuCalc.visit(AUNode<L,AP> node)
FormulaNode<L,AP>	CTLToMuCalc.visit(AWUNode<L,AP> node)
FormulaNode<L,AP>	CTLToMuCalc.visit(EFNode<L,AP> node)
FormulaNode<L,AP>	CTLToMuCalc.visit(EGNode<L,AP> node)
FormulaNode<L,AP>	CTLToMuCalc.visit(EUNode<L,AP> node)
FormulaNode<L,AP>	CTLToMuCalc.visit(EWUNode<L,AP> node)
FormulaNode<L,AP>	CTLToMuCalc.visit(DiamondNode<L,AP> node)
FormulaNode<L,AP>	CTLToMuCalc.visit(FalseNode<L,AP> node)
FormulaNode<L,AP>	CTLToMuCalc.visit(FormulaNode<L,AP> node)
FormulaNode<L,AP>	CTLToMuCalc.visit(GfpNode<L,AP> node)
FormulaNode<L,AP>	CTLToMuCalc.visit(LfpNode<L,AP> node)
FormulaNode<L,AP>	CTLToMuCalc.visit(VariableNode<L,AP> node)
FormulaNode<L,AP>	CTLToMuCalc.visit(NotNode<L,AP> node)
FormulaNode<L,AP>	CTLToMuCalc.visit(OrNode<L,AP> node)
FormulaNode<L,AP>	CTLToMuCalc.visit(TrueNode<L,AP> node)

Methods in net.automatalib.modelchecker.m3c.formula.visitor with parameters of type FormulaNode

Modifier and Type	Method	Description
FormulaNode<L,AP>	CTLToMuCalc.toMuCalc(FormulaNode<L,AP> ctlFormula)
FormulaNode<L,AP>	NNFVisitor.transformToNNF(FormulaNode<L,AP> node)
FormulaNode<L,AP>	CTLToMuCalc.visit(FormulaNode<L,AP> node)
T	FormulaNodeVisitor.visit(FormulaNode<L,AP> node)

Uses of FormulaNode in net.automatalib.modelchecker.m3c.solver

Fields in net.automatalib.modelchecker.m3c.solver declared as FormulaNode

Modifier and Type	Field	Description
FormulaNode<L,AP>	WitnessTreeState.subformula

Methods in net.automatalib.modelchecker.m3c.solver that return types with arguments of type FormulaNode

Modifier and Type	Method	Description
Mapping<N,List<FormulaNode<L,AP>>>	SolverData.getInitialSatisfiedSubformulas()	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.
List<FormulaNode<L,AP>>	SolverState.getUpdatedNodeSatisfiedSubformula()	Returns the list of satisfied subformulas the node updated in this step satisfies after the update.
static <L,AP> M3CSolver.TypedM3CSolver<FormulaNode<L,AP>>	M3CSolvers.typedADDSolver(ContextFreeModalProcessSystem<L,AP> cfmps)	Returns an ADD-backed M3CSolver.TypedM3CSolver solver for strongly-typed modal context-free process systems.
static <L,AP> M3CSolver.TypedM3CSolver<FormulaNode<L,AP>>	M3CSolvers.typedBDDSolver(ContextFreeModalProcessSystem<L,AP> cfmps)	Returns a BDD-backed M3CSolver.TypedM3CSolver solver for strongly-typed ContextFreeModalProcessSystem.
static <L,AP> M3CSolver.TypedM3CSolver<FormulaNode<L,AP>>	M3CSolvers.typedSolver(ContextFreeModalProcessSystem<L,AP> cfmps)	Returns a default M3CSolver.TypedM3CSolver solver for strongly-typed modal context-free process systems.