Hi Florian - on https://termination-portal.org/wiki/Termination_Competition_2025_technical_d... you write "following two commands will be executed in your container: solver --name solver --timeout=$timeout --category=$category $benchmark" * what do you recommend for --name? (how many lines, words, characters) (e.g., can/should it contain precise version information?) * I can just ignore timeout? (and expect it to be 60 seconds?) * how many cores can I expect to use? RAM? * what are the possible values for $category? (they are names of top-level directories in TPDB? e.g., SRS_Standard, SRS_Relative ? Could you provide empty files in https://github.com/TermCOMP/registration ?) * How do I know whether it's certified or not? * $benchmark : will it have a specific extension (.ari)? - Johannes.
Dear Johannes,
* what do you recommend for --name? (how many lines, words, characters) (e.g., can/should it contain precise version information?)
That's up to you. I think including version information would be useful. I'll probably use something like "LoAT v0.2.0" or "LoAT $SHORT_GIT_SHA" for my tool.
* I can just ignore timeout? (and expect it to be 60 seconds?)
Yes, you can do that.
* how many cores can I expect to use? RAM?
4 Cores, 20.345 MiB RAM.
* what are the possible values for $category? (they are names of top-level directories in TPDB?
Yes, for most categories, it'll just be the name of the top-level directory. We just have to think about an alternative for categories that do not have their own benchmark set (e.g., parallel rewriting).
e.g., SRS_Standard, SRS_Relative ? Could you provide empty files in https://github.com/TermCOMP/registration ?)
Please just create the missing files before creating a pull request.
* How do I know whether it's certified or not?
Good question. I didn't test with certification yet. I guess an additional argument '--cert' would do. Could you provide a (containerized) solver with support for certification (via '--cert')? Then I can start testing with certification and figure out the details.
* $benchmark : will it have a specific extension (.ari)?
Yes, .ari for all TRS/SRS/Transition System categories. Best Florian
Hi again,
* what do you recommend for --name? (how many lines, words, characters) (e.g., can/should it contain precise version information?)
I forgot to say something regarding the number of lines / words. The name is shown in the header of the table with the results, so it should be reasonably short (and just one line). Best Florian
Hi Florian, thanks for clarifications.
additional argument '--cert' would do.
perhaps --cert=$format ? (cpf/ceta, cetera) for future-proofing
Could you provide a (containerized) solver with support for certification (via '--cert')?
Yes we are currently working on this. We have containerized matchbox (*) it just needs some minimal testing and then publishing.
--name ... reasonably short (and just one line)
yes, so, not a full commit hash? I guess you will have to automatically trim the name anyway, for uniform display. To how many characters? Best regards, Johannes. (*) maybe this is helpful for others: here is our Dockerfile, it shows how to build an Haskell executable, and a C library https://git.imn.htwk-leipzig.de/waldmann/pure-matchbox/-/blob/eikmanns-%2312...
Hi Johannes,
additional argument '--cert' would do.
perhaps --cert=$format ? (cpf/ceta, cetera) for future-proofing
Will cetera use a different format than ceta? We use a uniform input format for solvers, so I guess it would be nice to have a uniform input format for certifiers as well (if possible)?
--name ... reasonably short (and just one line)
yes, so, not a full commit hash? I guess you will have to automatically trim the name anyway, for uniform display. To how many characters?
As far as I can see, the longest name last year was matchbox-2024-06-19 (19 characters). So let's say 20 characters max (unless using a longer name is important to someone -- in this case, please let me know). Best Florian
Will cetera use a different format than ceta?
right now, yes. See example below. That's part laziness - I just write "deriving (Read, Show)", and part design - I do like this format, it is less verbose, and more readable, than CPF. Well, this only matters for small certificates. Regardless of size - a Haskell data declaration is a much nicer specification than an XML schema (more concise, easier to machine-check). I think.
We use a uniform input format for solvers, so I guess it would be nice to have a uniform input format for certifiers as well (if possible)?
yes that is also a nice goal. I'm not too sure about running matchbox+cetera in termcomp now. It would just be a demonstration. If it's too much work for you, then we postpone. Another complication (for termcomp - for me, it's a simplification) is that I have Haskell syntax for SRS as well (see example) and letters must be natural numbers. Let's do "--cert" (meaning CPF/Ceta) for now (as you suggested) and discuss choice of formats/verifiers later (at WST). There _were_ several options for verification in the past. Then XML won? Cf. https://termination-portal.org/wiki/WScT08 (2008) - Johannes Certificate { system = [ Rule { lhs = [0,0,1,1], rhs = [1,1,1,0,0,0] } ] , reason = MatrixInterpretation { minterpretation = MatrixInterpretation { dim = 5 , int = [ (0, [[1,0,0,1,0] ,[0,0,0,2,0] ,[0,0,0,1,0] ,[0,0,1,0,0] ,[0,0,0,0,1]]) , (1, [[1,0,0,0,0] ,[0,0,1,2,1] ,[0,1,0,0,0] ,[0,0,0,0,0] ,[0,0,0,0,1]]) ] } , remove = [ Rule { lhs = [0,0,1,1], rhs = [1,1,1,0,0,0] } ] , sub = Certificate { system = [] , reason = Empty } } }
participants (2)
-
Florian Frohn -
Johannes Waldmann