Difference between revisions of "XTC Format Specification"
From Termination-Portal.org
Jump to navigationJump to search| Line 1: | Line 1: | ||
= Schema = | = Schema = | ||
For now see http://dev.aspsimon.org/xtc.xsd | For now see http://dev.aspsimon.org/xtc.xsd | ||
| + | |||
| + | = XML Structure = | ||
| + | The XML structure has the following main blocks: | ||
| + | |||
| + | * <trs>: this block contains all the information pertinent to the TRS itself. A more detailed description is below. | ||
| + | * <strategy>: this corresponds to the (STRATEGY ) block in the TPDB format. | ||
| + | * <startterm>: this is an extension for complexity analysis | ||
| + | * <status>: this is a meta-information block which contains information relating to the known termination status of a given problem. | ||
| + | *<metainformation>: more meta-information pertaining to the author of a problem, can also contain free-form comments. | ||
| + | |||
| + | Both <status> and <metainformation> will be stored in the database, but stripped from input files for the purposes of running the competition. | ||
| + | |||
| + | The <trs> block is structured as follows: | ||
| + | |||
| + | * <rules>: this block contains all the rules of a TRS, relative rules are separated into a separate child <relrules>; both these blocks can contain multiple <rule> children, consisting of a <lhs>, <rhs> and optional <conditions> block. | ||
| + | * <signature>: this block contains the list of function symbols with their signatures (name, arity, theory and context-sensitive replacement-map). | ||
| + | * <comment>: a free-form comment field about this TRS itself. | ||
| + | *<conditiontype>: for conditional TRS, this block is used to select the type of condition to be applied. | ||
| + | |||
| + | The full structure can be seen in the XML Schema file linked above. | ||
= XSLT Transformation = | = XSLT Transformation = | ||
The stylesheet can be found here: http://dev.aspsimon.org/workspace/projectdownloads/xtc2tpdb.xsl. More information to follow. | The stylesheet can be found here: http://dev.aspsimon.org/workspace/projectdownloads/xtc2tpdb.xsl. More information to follow. | ||
Revision as of 13:08, 13 February 2009
Schema
For now see http://dev.aspsimon.org/xtc.xsd
XML Structure
The XML structure has the following main blocks:
- <trs>: this block contains all the information pertinent to the TRS itself. A more detailed description is below.
- <strategy>: this corresponds to the (STRATEGY ) block in the TPDB format.
- <startterm>: this is an extension for complexity analysis
- <status>: this is a meta-information block which contains information relating to the known termination status of a given problem.
- <metainformation>: more meta-information pertaining to the author of a problem, can also contain free-form comments.
Both <status> and <metainformation> will be stored in the database, but stripped from input files for the purposes of running the competition.
The <trs> block is structured as follows:
- <rules>: this block contains all the rules of a TRS, relative rules are separated into a separate child <relrules>; both these blocks can contain multiple <rule> children, consisting of a <lhs>, <rhs> and optional <conditions> block.
- <signature>: this block contains the list of function symbols with their signatures (name, arity, theory and context-sensitive replacement-map).
- <comment>: a free-form comment field about this TRS itself.
- <conditiontype>: for conditional TRS, this block is used to select the type of condition to be applied.
The full structure can be seen in the XML Schema file linked above.
XSLT Transformation
The stylesheet can be found here: http://dev.aspsimon.org/workspace/projectdownloads/xtc2tpdb.xsl. More information to follow.
