Package | Description |
---|---|
jtabwbx.modal.basic |
Basic classes and interfaces for propositional modla formulas.
|
jtabwbx.modal.formula |
An implementation of propositional modal formulas based on graphs.
|
Modifier and Type | Method and Description |
---|---|
ModalFormula |
_ModalFormulaSet.getFirst() |
ModalFormula[] |
_ModalFormulaSet.toArray() |
Modifier and Type | Method and Description |
---|---|
java.util.Collection<ModalFormula> |
_ModalFormulaSet.getAllFormulas() |
java.util.Iterator<ModalFormula> |
_ModalFormulaSet.iterator() |
Modifier and Type | Method and Description |
---|---|
boolean |
_ModalFormulaSet.add(ModalFormula wff)
Add the specified formula to this set and returns
true if this
set did not already contain the specified formula. |
boolean |
_ModalFormulaSet.contains(ModalFormula swff) |
static ModalFormulaType |
ModalFormulaType.getFormulaType(ModalFormula wff)
Returns the type for the specified formula.
|
boolean |
_ModalFormulaSet.remove(ModalFormula wff) |
Modifier and Type | Class and Description |
---|---|
class |
ModalFormulaProposition
An propositional variable.
|
Modifier and Type | Method and Description |
---|---|
ModalFormula |
ModalFormulaFactory.buildCompound(ModalConnective mainConnective,
ModalFormula... subFormulas)
Builds the formula having the specified logical constant as main connective
and the specified subformulas as direct subformulas.
|
ModalFormula |
ModalFormulaFactory.buildFrom(BTModalFormula wff)
Build an instance of the specified
BTModalFormula . |
ModalFormula |
ModalFormulaFactory.buildFrom(ModalFormula wff)
Build an instance of the specified
ModalFormula in this factory. |
ModalFormula |
ModalFormulaFactory.buildFrom(org.antlr.v4.runtime.tree.ParseTree parseTree)
Build a modal formula from the specified parse-tree.
|
ModalFormula |
ModalFormulaFactory.getByIndex(int index)
Returns the formula with the specified index.
|
ModalFormula |
BitSetOfModalFormulas.getFirst() |
ModalFormula |
BitSetOfModalFormulas.getFirst(ModalFormulaType type) |
ModalFormula |
BitSetOfModalFormulas.getFirstAndRemove()
Returns the first formula in this bitset and removes it from the bitset.
|
ModalFormula |
BitSetOfModalFormulas.getFirstAndRemove(ModalFormulaType type)
Returns the first formula with the specified type in this bitset and it
removes such a formula from the bitset.
|
ModalFormula[] |
ModalFormulaProposition.immediateSubformulas() |
abstract ModalFormula[] |
ModalFormula.immediateSubformulas()
The subformulas of this formula.
|
ModalFormula[] |
BitSetOfModalFormulas.toArray() |
Modifier and Type | Method and Description |
---|---|
java.util.ArrayList<ModalFormula> |
ModalFormulaFactory.generatedFormulas()
Returns a copy of the list of formulas generated by this factory.
|
java.util.Collection<ModalFormula> |
BitSetOfModalFormulas.getAllFormulas()
Returns the collection containing all the formulas in this set or null if
this set is empty.
|
java.util.Collection<ModalFormula> |
BitSetOfModalFormulas.getAllFormulas(ModalFormulaType formulaType)
Returns a collection containing all formulas with the specified formula
type in this set or null if this set does not contain any formulas with the
specified formula type.
|
java.util.Iterator<ModalFormula> |
BitSetOfModalFormulas.iterator() |
Modifier and Type | Method and Description |
---|---|
java.lang.String |
ModalFormulaLatexFormatter._toLatex(ModalFormula wff,
boolean parenthesize) |
boolean |
BitSetOfModalFormulas.add(ModalFormula wff) |
ModalFormula |
ModalFormulaFactory.buildCompound(ModalConnective mainConnective,
ModalFormula... subFormulas)
Builds the formula having the specified logical constant as main connective
and the specified subformulas as direct subformulas.
|
ModalFormula |
ModalFormulaFactory.buildFrom(ModalFormula wff)
Build an instance of the specified
ModalFormula in this factory. |
boolean |
BitSetOfModalFormulas.contains(ModalFormula wff) |
boolean |
BitSetOfModalFormulas.remove(ModalFormula wff) |
java.lang.String |
ModalFormulaLatexFormatter.toLatex(ModalFormula wff)
Returns the LaTex source of the specified formula, the result of this
method must placed in math mode.
|
java.lang.String |
ModalFormulaLatexFormatter.toLatex(ModalFormula[] formulas,
java.lang.String separator)
Returns the LaTex source of the formulas in the given array; formulas are
separated by the specified separator.
|
Modifier and Type | Method and Description |
---|---|
java.lang.String |
ModalFormulaLatexFormatter.toLatex(java.util.Collection<ModalFormula> formulas,
java.lang.String separator)
Returns the LaTex source of the formulas in the given collection; formulas
are separated by the specified separator.
|