Dear all,
thank you very much for your input! Let me try to summarize what we got so far:
1. Some benefits of a human-readable format have been pointed out.
2. Using an "established" format (that is also used at other competitions, e.g., SMT-LIB or the CoCo-format) would be nice.
3. Using a standardized format like XML has benefits as well, e.g., there's no need to discuss concrete syntax and one can use existing libraries.
Regarding the old TPDB format, some tools cannot parse it anymore, and it had a few quirks that were heavily discussed in the past [1].
In any case, a conversion to CeTA's new input format will be necessary. For the CoCo-format, a suitable converter is already available.
If there are other points that should be taken into account, please share them!
Best Florian
[1] https://verify.rwth-aachen.de/termtools/2003-November/subject.html
On 11/8/23 17:39, Florian Frohn wrote:
Dear all,
at the last WST, there were some discussions about the input format for TRSs. My takeaway was that not everyone is happy with the current XML format. So we (the TermComp SC) recently started to discuss whether the format should be changed. As far as I can see, there are three obvious options:
(a) keep the current format
Pro: no work Contra: not human readable
(b) go back to the old format [1] (here's [2] an example)
Pro: - human readable - the same format is used for other categories (e.g., Complexity of ITSs and Termination of Integer TRSs) - some tools can still parse it
Contra: There were some issues with the semantics, in particular if there were several VAR sections. However, from my understanding, these issues can be resolved by forbidding more than one VAR section.
(c) a new S-expression based format has been proposed for the confluence competition [3]
Pro: human readable(?) Contra: no tool can parse it yet
So if you compete, or are interested in, the TRS categories at TermComp, please let us know what you think. I'm also particularly interested in the following questions:
- If you participate, can your tool still parse the old format?
- Do you recall more details about the reasons for the switch from the
old format to the current one?
A related (but mostly independent) question is whether we should separate the properties to be analyzed (full vs innermost rewriting, termination vs complexity etc.) from the actual TRS. That could avoid a lot of redundancy in the TPDB. If you have an opinion on that, please share it.
Thanks, Florian
[1] https://www.lri.fr/%7Emarche/tpdb/format.html [2] https://aprove.informatik.rwth-aachen.de/interface/v-AProVE2023/trs_wst [3] http://cl-informatik.uibk.ac.at/iwc/2023/proceedings.pdf, page 32 _______________________________________________ Termtools mailing list -- termtools@lists.rwth-aachen.de To unsubscribe send an email to termtools-leave@lists.rwth-aachen.de