[Termtools] Call for Complexity Related Problems

[Fabian Emmes]

Dear Georg,

On 23. Jun, 18:51, Georg Moser wrote:
> >What is the rationale for not analyzing innermost systems?
> >In my opinion at least for _i_RC analysis this would be
> >useful.
> >
> Essentially the observation was that we didn't have enough
> information about the content of the additional innermost examples.
> We only knew that some are duplicates (actually no longer that
> many). Hence, we decided to ignore them for the time beeing.
> 
> Actually your tests indeed strengthen this point, as out of 358
> additional examples 128 should be removed according to your
> suggestion.

As the ratio of problems rejected by the tests is about the same for
innermost as for non-innermost examples, I don't agree here.


> I think the main point now is how to proceed. Eliminating these TRS
> from the TPDB is out of the questions. Always using a different
> testbed than TPDB in the competition is also no option. Checking
> against your list is easy to implement, but cumbersome if the TPDB
> grows (which it will).
> 
> What we could do is to incorporate your tests into the selection
> procedure, in a similar way as the test for non-duplicating TRS are
> performed. Would you agree to that?

Yes. I think rejecting trivial examples will lead to better
comparability between the tools.


A completely unrelated thing: The XTC-Format stylesheet contains
information to distinguish (i)DC, (i)RC and termination problems. I
suppose this information was used in the last competition. Since the
TPDB itself contains no complexity problems (only termination problems),
we currently cannot test AProVE on the same files that will be during
the competition. How can I get the complexity problem files?

Best regards,
Fabian
-- 
Fabian Emmes           mailto:emmes at informatik.rwth-aachen.de
LuFG Informatik 2      http://verify.rwth-aachen.de/emmes/
RWTH Aachen            phone: +49 241 80-21241