[Termtools] TPDB -- C-Integer Complexity

[aeflores]

The problem with that definition is that the main function does not
receive any parameters so the complexity of the program cannot be defined in terms of the input parameters.
I believe we ran into the same problem last year.

I think we could adopt a similar definition that allows parameters and
collect new examples (points 1 and 2) but I do not think we can use the examples from the termination category
(point 3) for the same reason (maybe some can be adapted).
Best,

Antonio


On 07/31/2017 11:02 AM, Florian Frohn wrote:
> Dear all,
>
> during the preparations for the upcoming TermComp I came across some
> oddities regarding the category "C-Integer Complexity". First of all,
> the TPDB contains just 26 examples for this category, but according to
> the Call for Participation at least 40 examples are required. More
> importantly, they do not conform to the TermComp definition of C-Integer
> programs (http://www.termination-portal.org/wiki/C_Integer_Programs).
> E.g., cBench_bin_search_StepSize2.c uses "nondet" instead of
> "__VERIFIER_nondet_int" for nondeterminism and it uses division, which
> is not allowed by the definition.
>
> Assuming that we agree on the definition from
> http://www.termination-portal.org/wiki/C_Integer_Programs (which was
> discussed when the category "C-Integer Termination" was introduced), I
> propose to
>
> 1. remove all examples that do not conform to the definition,
> 2. collect new examples, and
> 3. use the examples from "C-Integer Termination" as fallback (i.e., if
> less than 40 examples are submitted), even though some of them might be
> uninteresting for complexity analysis.
>
> What do the other participants of this category think?
>
> Best
> Florian
>
>
> PS: Sorry if you received multiple copies of this mail, there were some
> technical issues.
> _______________________________________________
> Termtools mailing list
> Termtools at lists.lri.fr
> http://lists.lri.fr/cgi-bin/mailman/listinfo/termtools