[Termtools] cime3verifier

[Xavier Urbain]

2009/12/16 Martin Johann Korp <Martin.Korp at uibk.ac.at>

> Dear all,
>
> > since TTT2 does not output forward arcs for dependency graph
> > decomposition and cime3verifier needs these forward arcs,
> > I wrote a small .xsl-file that reintroduces forward-edges.
> >
> > So, can either the termination-tool authors post-process their
> > output by
> >
> > xsltproc cpfIntroForwardArcs.xsl $cpf > $newcpf
> >
> > (does aprove output forward arcs??)
> >
> > or can cime3verifier preprocess their input.
>
> to keep things simple and to ensure that the competition can
> start as soon as possible, we volunteer to post-process
> our output as Rene suggested (@Simon: I hope it is still
> possible in this case to submit a new tool!).
>
> Nevertheless, I think there should be some discussion if this
> additional information in the CPF is really necessary.
> From my point of view (the view of a termination tool author)
> the information seems to be superfluous because Rene could fix
> that problem so easily.
>
> All the best,
>  Martin
> _______________________________________________
> Termtools mailing list
> Termtools at lists.lri.fr
> http://lists.lri.fr/mailman/listinfo/termtools
>



There is a format that was defined (open discussion), with rules and ideas
behind those rules, and this format states that those arcs should be given.
The previous output of TTT2 does not follow those ideas.
The information might be superfluous, but that's another problem, and any
discussion about the format is welcome. Lots of information in CPF are
indeed superflous, (we could say: anything but the TRS).

The very simple point here is: a format was given in the competition rules,
and it seems reasonable that competitors fulfil this constraint.

We are glad to see that things seem to be ok now.

Best regards,

The A3PAT group
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.lri.fr/pipermail/termtools/attachments/20091216/cbf1d180/attachment.htm