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/~marche/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
Hello Florian,
- If you participate, can your tool still parse the old format?
The XML format was introduced before the higher-order competition was, so Wanda cannot parse the human-readable variant of the higher-order format. However, I would be in favour of changing the higher-order format used in the competition altogether (although that's a separate discussion), and at that point we might as well go for a human-readable presentation instead. (Wanda /can/ parse the human-readable variant of the first-order format, but is not a competitor in those categories.) Personally, I strongly prefer a format that a human can read and, most importantly, write by hand to quickly test examples, and even if the higher-order format isn't changed I'd gladly sacrifice the time to change Wanda's parser if it meant I could test other tools on a given example without having to jump through hoops to translate it to XML first. I also think it would be a good idea for the termination and confluence competition to do the same. Cynthia. On 08-11-2023 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/~marche/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
Dear Florian, dear all,
(b) go back to the old format [1] (here's [2] an example) ... Contra: There were some issues with the semantics,
also - cf. "Wadler's law of language design", issues with (comment) syntax (? - everything that's invalid, is accepted as comment) for reference, early discussion is here https://verify.rwth-aachen.de/termtools/2003-November/subject.html
(c) a new S-expression based format has been proposed for the confluence competition [3]
Pro: human readable(?)
Pro: the format is used for SMTLIB as well (?)
- If you participate, can your tool still parse the old format?
matchbox - yes. https://hackage.haskell.org/package/tpdb
- Do you recall more details about the reasons for the switch from the old format to the current one?
* avoiding discussion of concrete (surface) syntax, e.g., what is a valid identifier, a comment, etc. * validation of termination proofs needed a (machine-readable) exchange format anyway (cf. https://verify.rwth-aachen.de/termtools/2007-May/000325.html ) but - TRS in CPF syntax (certificates) is not the same as TRS in XTC (benchmarks)? And the name is wrong ... https://verify.rwth-aachen.de/termtools/2009-December/000787.html * XML was all the rage in the 90s - as was JSON was after that, and S-expressions before. - Johannes.
Dear Florian, On 11/8/2023 5:39 PM, Florian Frohn wrote:
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?
MU-TERM can deal with the original TPDB format.
- Do you recall more details about the reasons for the switch from the old format to the current one?
From a programming perspective, utilizing standard formats like XML or JSON to define TRSs is a good idea, given the availability of libraries that facilitate the transformation of these files into data structures (not in Haskell, where we use Parsec, but in Python, for example, there are libraries to do this automatically) and also to interact between different tools. However, from a user standpoint, it is crucial that TRSs can be easy to write. Best, Raúl.
Dear all, concerning the mismatch between CPF and XTC format, I can only say that this is no longer an issue: CPF 3 has just been released and it will no longer support XTC itself, but a cleaned up variant. So competition organisers have to write a converter from their TRS-format to the CPF-input format, which should be an easy task. Such a converter is already available for the new ARI-format, a format that will be used in CoCo starting in 2024. For more information regarding the changes in CPF (in particular for running competitions), cf. http://cl-informatik.uibk.ac.at/isafor/cpf3.html (overview) or http://cl-informatik.uibk.ac.at/isafor/cpf3.tgz (specification + converter) Best, René
Am 13.11.2023 um 09:37 schrieb Raúl Gutiérrez <raguti@upv.es>:
Dear Florian,
On 11/8/2023 5:39 PM, Florian Frohn wrote:
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?
MU-TERM can deal with the original TPDB format.
- Do you recall more details about the reasons for the switch from the old format to the current one?
From a programming perspective, utilizing standard formats like XML or JSON to define TRSs is a good idea, given the availability of libraries that facilitate the transformation of these files into data structures (not in Haskell, where we use Parsec, but in Python, for example, there are libraries to do this automatically) and also to interact between different tools. However, from a user standpoint, it is crucial that TRSs can be easy to write.
Best,
Raúl.
_______________________________________________ Termtools mailing list -- termtools@lists.rwth-aachen.de To unsubscribe send an email to termtools-leave@lists.rwth-aachen.de
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/~marche/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
Dear all, in the meantime, the ARI format has been finalized [1]. I've created GitHub discussions on more concrete proposals how to adapt it for termCOMP. All TRS categories but equational and relative rewriting: https://github.com/orgs/TermCOMP/discussions/83 Equational Rewriting: https://github.com/orgs/TermCOMP/discussions/84 Relative Rewriting: https://github.com/orgs/TermCOMP/discussions/85 Please share your opinions in these discussions. In particular, please let us know if your tool would drop out of the competition due to lack of resources for implementing a parser for the ARI format. Best Florian [1] http://project-coco.uibk.ac.at/ARI/index.php On 11/15/23 10:40, Florian Frohn wrote:
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/~marche/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
Termtools mailing list -- termtools@lists.rwth-aachen.de To unsubscribe send an email to termtools-leave@lists.rwth-aachen.de
Dear all, I'd also like to start a discussion on higher-order categories. The proposal reflects (long) discussions with Cynthia, Frédéric, and Makoto. https://github.com/orgs/TermCOMP/discussions/86 Main points are that there is also a simply typed TRS (STTRS) format, and that HRS category adopts HRS semantics, and restricted to 2nd order. Best, Akihisa On 2024/01/15 18:23, Florian Frohn wrote:
Dear all,
in the meantime, the ARI format has been finalized [1]. I've created GitHub discussions on more concrete proposals how to adapt it for termCOMP.
All TRS categories but equational and relative rewriting:
https://github.com/orgs/TermCOMP/discussions/83
Equational Rewriting:
https://github.com/orgs/TermCOMP/discussions/84
Relative Rewriting:
https://github.com/orgs/TermCOMP/discussions/85
Please share your opinions in these discussions. In particular, please let us know if your tool would drop out of the competition due to lack of resources for implementing a parser for the ARI format.
Best Florian
[1] http://project-coco.uibk.ac.at/ARI/index.php
On 11/15/23 10:40, Florian Frohn wrote:
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/~marche/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
Termtools mailing list -- termtools@lists.rwth-aachen.de To unsubscribe send an email to termtools-leave@lists.rwth-aachen.de
Termtools mailing list -- termtools@lists.rwth-aachen.de To unsubscribe send an email to termtools-leave@lists.rwth-aachen.de
Dear Akihisa, I was under the impression that those discussions were about the /confluence/ competition, not the /termination/ competition? The termination competition has always used plain matching, not modulo matching, and while the argument for HRSs in the confluence case is "most papers on higher-order confluence consider modulo matching" the opposite is true when it comes to termination. I would be very disappointed if HRSs became the de facto standard for higher-order analysis since it would throw away a vast body of work on "HOR union beta", and moreover steer future developments in a direction that makes it much harder to extend results to orders above 2. (Side note: the page somewhat misrepresents Wanda: Wanda's format does /not/ coincide with HRSs in the second-order case, but can represent them -- that does not mean that the power on this subset is the same.) Cynthia. On 16-01-2024 09:09, YAMADA, Akihisa wrote:
Dear all,
I'd also like to start a discussion on higher-order categories. The proposal reflects (long) discussions with Cynthia, Frédéric, and Makoto.
https://github.com/orgs/TermCOMP/discussions/86
Main points are that there is also a simply typed TRS (STTRS) format, and that HRS category adopts HRS semantics, and restricted to 2nd order.
Best, Akihisa
On 2024/01/15 18:23, Florian Frohn wrote:
Dear all,
in the meantime, the ARI format has been finalized [1]. I've created GitHub discussions on more concrete proposals how to adapt it for termCOMP.
All TRS categories but equational and relative rewriting:
https://github.com/orgs/TermCOMP/discussions/83
Equational Rewriting:
https://github.com/orgs/TermCOMP/discussions/84
Relative Rewriting:
https://github.com/orgs/TermCOMP/discussions/85
Please share your opinions in these discussions. In particular, please let us know if your tool would drop out of the competition due to lack of resources for implementing a parser for the ARI format.
Best Florian
[1] http://project-coco.uibk.ac.at/ARI/index.php
On 11/15/23 10:40, Florian Frohn wrote:
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/~marche/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
Termtools mailing list -- termtools@lists.rwth-aachen.de To unsubscribe send an email to termtools-leave@lists.rwth-aachen.de
Termtools mailing list -- termtools@lists.rwth-aachen.de To unsubscribe send an email to termtools-leave@lists.rwth-aachen.de
Termtools mailing list -- termtools@lists.rwth-aachen.de To unsubscribe send an email to termtools-leave@lists.rwth-aachen.de
Dear Cynthia, there shouldn't be any intention towards setting a de-facto standard semantics. It's just that only 2nd-order HRS remain reachable by more than one tool. (If I were to, I'd vote for a formalism that coincides with STTRS on lambda-free fragment, so not HRS. I also observe Isabelle's rewriting is not HRS.) P.S. Will you mind using GitHub? It's far easier to chat than composing E-mails. Best, Akihisa On 2024/01/16 18:10, Cynthia Kop wrote:
Dear Akihisa,
I was under the impression that those discussions were about the /confluence/ competition, not the /termination/ competition?
The termination competition has always used plain matching, not modulo matching, and while the argument for HRSs in the confluence case is "most papers on higher-order confluence consider modulo matching" the opposite is true when it comes to termination. I would be very disappointed if HRSs became the de facto standard for higher-order analysis since it would throw away a vast body of work on "HOR union beta", and moreover steer future developments in a direction that makes it much harder to extend results to orders above 2.
(Side note: the page somewhat misrepresents Wanda: Wanda's format does /not/ coincide with HRSs in the second-order case, but can represent them -- that does not mean that the power on this subset is the same.)
Cynthia.
On 16-01-2024 09:09, YAMADA, Akihisa wrote:
Dear all,
I'd also like to start a discussion on higher-order categories. The proposal reflects (long) discussions with Cynthia, Frédéric, and Makoto.
https://github.com/orgs/TermCOMP/discussions/86
Main points are that there is also a simply typed TRS (STTRS) format, and that HRS category adopts HRS semantics, and restricted to 2nd order.
Best, Akihisa
On 2024/01/15 18:23, Florian Frohn wrote:
Dear all,
in the meantime, the ARI format has been finalized [1]. I've created GitHub discussions on more concrete proposals how to adapt it for termCOMP.
All TRS categories but equational and relative rewriting:
https://github.com/orgs/TermCOMP/discussions/83
Equational Rewriting:
https://github.com/orgs/TermCOMP/discussions/84
Relative Rewriting:
https://github.com/orgs/TermCOMP/discussions/85
Please share your opinions in these discussions. In particular, please let us know if your tool would drop out of the competition due to lack of resources for implementing a parser for the ARI format.
Best Florian
[1] http://project-coco.uibk.ac.at/ARI/index.php
On 11/15/23 10:40, Florian Frohn wrote:
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/~marche/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
Termtools mailing list -- termtools@lists.rwth-aachen.de To unsubscribe send an email to termtools-leave@lists.rwth-aachen.de
Termtools mailing list -- termtools@lists.rwth-aachen.de To unsubscribe send an email to termtools-leave@lists.rwth-aachen.de
Termtools mailing list -- termtools@lists.rwth-aachen.de To unsubscribe send an email to termtools-leave@lists.rwth-aachen.de
_______________________________________________ Termtools mailing list -- termtools@lists.rwth-aachen.de To unsubscribe send an email to termtools-leave@lists.rwth-aachen.de
starexec seems up and running again. what are (names/ids of) the postprocessors (uncertified/certified) that will be used in competition (that we can use for tests)? do we have some nodes assigned for testing? (a recommendation about what nodes to use, and how long will they be available) I forgot details about how provers are run - will they be seeing the input (termination problem) with the correct file extension (.ari)? assuming starexec is stable now - what is the submission deadline? E.g., after this week-end? I am very much not ready ... - Johannes.
Dear Johannes, dear all,
starexec seems up and running again.
As far as I know, just new.q is available, the others are supposed to be back online in the next days.
what are (names/ids of) the postprocessors (uncertified/certified) that will be used in competition (that we can use for tests)?
Since StarExec was offline, I could only test the postprocessors locally so far. I'll start testing them on StarExec today, and I'll let you know when they are ready.
do we have some nodes assigned for testing? (a recommendation about what nodes to use, and how long will they be available)
When all nodes are updated, some of them should be available in termcomp.q. However, if I recall correctly from the previous years, they are only available to "community leaders". So I think the tools should be tested on the publicly available queues. As far as I know, the nodes in termcomp.q (which will be used for the competition) are identical to those in all.q and long.q, but not to those in new.q. I asked Aaron to confirm this. So I think new.q can be used to check if your solver works on StarExec at all. To get (more or less) the same results as in the competition, all.q or long.q should be used instead.
I forgot details about how provers are run - will they be seeing the input (termination problem) with the correct file extension (.ari)?
As far as I remember (and judging from some old configurations that were used last year), the input files are renamed, but the file extension is preserved.
assuming starexec is stable now - what is the submission deadline? E.g., after this week-end? I am very much not ready ...
Since the situation is somewhat chaotic due to the update, lets be pragmatic w.r.t. the deadline: I want to start the first run on Monday, 24th, in the morning, so I'd like to be ready with the setup on Friday, 21st, in the afternoon. So please try to submit until 21st, 10am CEST. If the 21st is approaching and you're running out of time, please get in touch. Best Florian
_______________________________________________ Termtools mailing list -- termtools@lists.rwth-aachen.de To unsubscribe send an email to termtools-leave@lists.rwth-aachen.de
Hi Florian, thanks for doing all the work. Where do you want bug reports? I was uploading a solver, tried starting a job, (in my "space") but got "It seems an error has occurred... (http 400 - bad request) You must specify which benchmarking framework you want to use." This is to be set by the organizer ("community leader")? Or can I do it? Where? - Johannes.
Hi,
Where do you want bug reports?
I guess it's easiest to use the bugtracker of the starexec-master repository: https://github.com/TermCOMP/starexec-master/issues
I was uploading a solver, tried starting a job, (in my "space") but got
"It seems an error has occurred... (http 400 - bad request) You must specify which benchmarking framework you want to use."
This is to be set by the organizer ("community leader")?
I can set a "default" benchmarking framework, which is set to benchexec. However, it seems like benchexec does not work / is not available at the moment. I notified Aaron.
Or can I do it? Where?
When you start a job, click "advanced options", look for the field "benchmarking framework", and choose "runsolver". If I remember correctly, the measurement of the runtime does not work reliably with runsolver in some cases, but it should be okay for a first round of testing. Best Florian
Dear all,
do we have some nodes assigned for testing? (a recommendation about what nodes to use, and how long will they be available) As far as I know, the nodes in termcomp.q (which will be used for the competition) are identical to those in all.q and long.q, but not to those in new.q. I asked Aaron to confirm this.
I got an answer from Aaron: termcomp.q will contain nodes with names nXXX, and those are all identical. According to Aaron, they are "usually found in all.q" (and as far as I remember, also in long.q -- but please double-check). Nodes with names zXX (usually in new.q) are different. Best Florian
participants (8)
-
Cynthia Kop -
Etienne Payet -
Florian Frohn -
Florian Frohn -
Johannes Waldmann -
Raúl Gutiérrez -
Thiemann, René -
YAMADA, Akihisa