Dear all,
the testing for the competition categories is over. Some tools still
have problems regarding their performance (rejects in certified
categories or severe regressions compared to last year), but from a
technical point of view, all tools (*) are working.
If your tool has rejects or significant regressions, then you've been
notified. I'll continue to accept updates, but I won't run any more
tests. So if you update your tool, please make sure that the updated
version works on StarExec.
Moreover, the links to the proofs in the demo categories are working again.
Best
Florian
(*) AutoNon still has a few issues, but that's a 'historical' tool that
was just registered for reference. I'll take care of updating it.
Dear all,
the registration for termCOMP is over. Some teams worked really hard to
fix issues caused by the StarExec update, resulting in some last minute
registrations. Thanks for that!
If you missed the deadline, but intended to participate, please get in
touch.
Best
Florian
Dear all,
I was just informed that the benchmarking framework that we used in the
past (BenchExec) is no longer available on StarExec. Hence, we'll have
to work with "runsolver" instead. If I remember correctly, we used
runsolver at some point, but then we switched to BenchExec due to issues
with the measurement of the runtime. If you remember any details / your
tool was affected by these problems, please let me know.
Best
Florian
Dear all,
can I express in CPF (for Ceta-2)
that I want to apply "flat context closure" to a subset of rules only?
specifically, I want this for rules with empty lhs or rhs,
as it seems to increase the power of matrix interpretations.
(as shown by Aprove in TC 23).
I am looking at
http://cl2-informatik.uibk.ac.at/rewriting/mercurial.cgi/IsaFoR/file/825022…
but the example seems to close all rules.
I guess I can indeed context-close all rules uniformly,
and use the same interpretation, to remove the same rules.
But perhaps I want other methods that refer to the original rules.
Well it's a bit late anyway.
- J.
Dear all,
just to clarify, we expect the tools to output *CPF2 proofs* in the
certified categories (just like last year). If your tool already
supports the new CPF3 format and you planned to make use of that at
termCOMP, please let me know.
Best
Florian
Dear all,
for uncertified categories that use the new ARI format, you can start
testing with the following post-processor:
plain.ari.24.1 (784)
I tested it successfully on 1(!) example, so it might still have some
issues.
Best
Florian
Dear all,
here is the information that I have about the current StarExec
configuration:
root@starexec2:~# uname -r
5.15.0-112-generic
oot@starexec2:~# dpkg -l libc6-dev:amd64 python3
Desired=Unknown/Install/Remove/Purge/Hold
|
Status=Not/Inst/Conf-files/Unpacked/halF-conf/Half-inst/trig-aWait/Trig-pend
|/ Err?=(none)/Reinst-required (Status,Err: uppercase=bad)
||/ Name Version Architecture Description
+++-===============-===============-============-=========================================================================
ii libc6-dev:amd64 2.35-0ubuntu3.8 amd64 GNU C Library:
Development Libraries and Header Files
ii python3 3.10.6-1~22.04 amd64 interactive high-level
object-oriented language (default python3 version)
Note that the information here
https://www.starexec.org/starexec/public/machine-specs.txt
is outdated!
Best
Florian
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
