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