CoCoWeb - A Convenient Web Interface for Confluence Tools
Julian Nagele Aart Middeldorp


Batch-Based Activity Recognition from Egocentric Photo-Streams
    [
    
==============================================================




We present a useful web interface for tools that participate in the annual
confluence competition.




§ INTRODUCTION


In recent years several tools have been developed to automatically prove
confluence and related properties of a variety of rewrite formats.
These tools compete annually in the confluence competition <cit.>
http://coco.nue.riec.tohoku.ac.jp/(CoCo).
[<http://coco.nue.riec.tohoku.ac.jp>]
Most of the tools can be downloaded, installed, and run on one's local
machine, but this can be a painful process.
[StarExec provides a VM Image with their environment,
which can helpful in case a local setup is essential.]
Few confluence tools—we are
aware of  <cit.>,  <cit.>, and
 <cit.>—provide a convenient web interface to painlessly
test the status of a system that is provided by the user.

Inspired by the latest web interface of  <cit.>,
in this note we present , a web interface
that provides a single entry point to all tools that participate in CoCo.
 is available at


<http://cl-informatik.uibk.ac.at/software/cocoweb>


The typical use of  will be to test whether a given
confluence problem is known to be confluent or not. This is useful when
preparing or reviewing an article, preparing or correcting exams about
term rewriting, and when contemplating to submit a challenging problem
to the confluence problems
(http://cops.uibk.ac.at/Cops)
[<http://cops.uibk.ac.at>]
database. In particular,
 is useful is when looking for
(killer) examples to illustrate a new technique. For instance, in
<cit.> a rewrite system is presented that can be shown to be
confluent with the technique introduced in that paper. The authors write
“Note that we have tried to show confluence [ …] by confluence checker
and , and both of them failed.” Despite having an easy to use
web interface, was not tried.  could also be
useful for the CoCo steering committee when integrating newly submitted
problems into Cops.

The tools run on the same hardware, which is compatible with a single
node of StarExec <cit.> that is used for CoCo, allowing for a proper
comparison of tools.

In the next section we present the web interface of 
by means of a number of screenshots. Implementation details are
presented in Section <ref> and in
Section <ref> we list some possibilities for
extending the functionality of  in the future.



§ WEB INTERFACE



Figure <ref> shows a screenshot of the entry page of
. Problems can be entered in three
different ways:
[label=(*)]

  * using the text box,

  * uploading a file,

  * entering the number of a system in Cops.


The tools that should be executed can be selected from the tools panel
on the left.

Tools are grouped into categories, similar to the grouping
in CoCo except that we merged the certified categories with the
corresponding uncertified categories. Multiple tools can be selected.
This is illustrated in Figure <ref>.
Here we selected the CoCo 2016
and 2015 versions of and the CoCo 2015 version of , and
Cop 500 is chosen is input problem.

The screenshot in Figure <ref> shows the output of 
after clicking the submit button. The output of the selected tools is
presented in separate tabs. The colors of these tabs reveal
useful information: Green means that the tool answered yes,
red (not shown) means that the tool answered no, and a maybe answer or
a timeout is shown in blue. By clicking on a tab, the color is made
lighter and the output of the tool is presented. The final line of the
output is timing information provided by .


The final screenshot (in Figure <ref>) is concerned with the example
in <cit.> that we referred to in the introduction.




§ IMPLEMENTATION



Most of  is built using PHP. User input in forms, i.e.,
rewrite systems and tool selections, is sent using the HTTP POST method.
The dynamic parts of the website, namely folding and unfolding in the tool
selection menu and the tabs used for viewing tool output are implemented
using JavaScript.

To layout the tool selection menu we made extensive use of CSS3 selectors.
For instance, the buttons to select tools are implemented as checkboxes
with labels that are styled according to whether the checkbox is ticked or
not:

Drawing the edges of the tree menu is also done using CSS, relying mainly
on its  selector.

The content of the tool menu, i.e., years, the grouping by categories, and
the actual tools, is generated automatically from a directory tree that
has the structure of the menu in .
There small configuration files reside that specify how the tools are
to be run, in case they are selected. Two environment variables are set in
such a file, for example the one for the 2012 version of reads
as follows:

The variable  specifies the directory that contains the
tool binary, while  gives the tool invocation, which in
turn refers to , the timeout, and , the input
rewrite system. Using such configuration files tools are run using the
following script, whose first and second argument are the configuration
of the tool and input rewrite system respectively:

The script uses three different timeouts:  is the timeout
passed to the tool itself if supported, while after  and
 the signals  and  are sent
to the tool in case it did not terminate on its own volition. When
multiple tools are selected,  runs them sequentially, in
order to avoid interference.



§ POSSIBLE EXTENSIONS



We conclude this note with some ideas for future extensions of
the functionality of .


  * By analyzing the format of the input problem, it is often possible to
determine the category to which the problem belongs. This information can
then be used to restrict tool selection accordingly.

  * Adding support for other competition categories like ground confluence
and unique normal forms is an obvious extension. This, however, limits
the possibilities to restrict tool selection mentioned in the previous
item.

  * Selected tools are executed sequentially and so if many tools are
selected, the 60 seconds time limit per tool may result in an
unacceptably slow response. In that case a timer option is a welcome
feature.


plain


