Dear Model Checking Contest competitors,
This year, the SMV team at University of Geneva will propose a tool
named mcc4mcc (model checker collection for the model checking contest)
in the competition, that acts as a wrapper above the tools you submitted
in 2017.
In order to select one of your tools for each examination/instance,
mcc4mcc uses machine learning techniques on a new feature available this
year in the contest: the
generic properties.
The code of mcc4mcc is open source (MIT license) and available
on GitHub.
A tool paper has also been accepted at the Petri nets conference on this topic,
put as attachment to this email.
In order to create mcc4mcc, we have wrapped all your tools within docker
images, either by compiling the required sources in an
Alpine Linux distribution,
or by copying the binary from your virtual machines.
For each tool, you can look at the Dockerfiles and the prepare script
that are used to build the images. prepare scripts extract required files
from the virtual machines you provided last year.
Currently, all the docker images are stored in a private repository,
but public docker images could be great for your tools.
Feel free to reuse our Dockerfiles to build your own docker images.
We would also be happy to work with you on creating the images, as we propose
in the paper a layout for docker images that could be useful for both your
tools and the contest.
Alas, we had to update some of your scripts, and thus to store them in
the mcc4mcc repository. Most of the time, it is the BenchKit_head.sh
script, that is stored as mcc-head in the repository.
For some tools, we also head to extract some other files.
As we do not own intellectual property on these, we need you to explicitly
accept this. If you want the files to be removed, please ask us as soon
as possible and we will perform the deletion.
The model checking contest rules also require us to get your explicit
approval, even if your tool is free software, to let us use it in the
competition. If you do not want your tool to be used within mcc4mcc,
ask us as soon as possible to remove it. In the other case,
please send us (with copy to the contest organizers) a small sentence of
approval.
The use of other tools to compete in the model checking contest raises a problem concerning the fairness of the results of the competition. The contest commitee is already aware and discussing about this. Our goal is mainly to provide a base tool to the MCC community, and let you reuse and improve it. Thus do not worry about the final score: everything will be made by the organizers to avoid biased results.
Best regards, Alban Linard Semantics Modeling & Verification Team University of Geneva
Note to the developers of smart: we tried to ask a license of smart but did
not obtain an answer, thus smart is currently not included into mcc4mcc.
We would be happy to include it, so feel free to contact us!