public class SPASSWriter
extends java.lang.Object
A SPASS input file consists of the following parts:
SPASSModalReasoner
Modifier and Type | Field and Description |
---|---|
(package private) java.io.Writer |
writer
Output is redirected to this writer.
|
Constructor and Description |
---|
SPASSWriter()
Creates a new SPASSWriter.
|
SPASSWriter(java.io.Writer writer)
Creates a new SPASSWriter.
|
Modifier and Type | Method and Description |
---|---|
void |
close() |
private java.lang.String |
printDescription()
Generates a generic description part for a SPASS problem file.
|
private java.lang.String |
printFormula(RelationalFormula f) |
private java.lang.String |
printFormulas(ModalBeliefSet kb,
RelationalFormula formula)
Prints the axioms declaration and conjectures declaration for a SPASS input file.
|
void |
printProblem(ModalBeliefSet kb,
RelationalFormula formula)
Prints the contents of a SPASS problem file for a given knowledge base and a formula.
|
private java.lang.String |
printSignature(FolSignature signature)
Prints the symbols declaration for a SPASS input file.
|
public SPASSWriter(java.io.Writer writer)
writer
- Output is redirected to this writer.public SPASSWriter()
public void printProblem(ModalBeliefSet kb, RelationalFormula formula) throws ParserException, java.io.IOException
kb
- a knowledge baseformula
- a relational formulaParserException
java.io.IOException
private java.lang.String printDescription()
private java.lang.String printSignature(FolSignature signature)
signature
- FolSignature of the problemprivate java.lang.String printFormulas(ModalBeliefSet kb, RelationalFormula formula)
kb
- a knowledge base of relational formulas that will be used as the axioms declarationsformula
- a formula that will be used as the conjectures declarationprivate java.lang.String printFormula(RelationalFormula f)
public void close() throws java.io.IOException
java.io.IOException