Skip to content

Commit

Permalink
Website: The model repository is now a benchmark set.
Browse files Browse the repository at this point in the history
  • Loading branch information
@ahartmanns
ahartmanns committed Nov 16, 2018
1 parent 123f936 commit 84c9d80
Show file tree
Hide file tree
Showing 6 changed files with 38 additions and 38 deletions.
30 changes: 15 additions & 15 deletions benchmarks/contributing.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,20 +2,20 @@
<html>
<head>
<meta charset="UTF-8">
<title>QComp - Quantitative Formal Models Repository - qcomp.org</title>
<title>QComp - Quantitative Verification Benchmark Set - qcomp.org</title>
<link rel="stylesheet" type="text/css" href="../style.css">
<script type="text/javascript" src="../script.js"></script>
</head>
<body onload="init()">

<h1>Quantitative Formal Model Repository</h1>
<h1>Quantitative Verification Benchmark Set</h1>
<div class="belowh1">
<a href="index.html">⮌</a> &nbsp;|&nbsp; <a href="#info">Contributor Information</a> &nbsp;|&nbsp; <a href="#addmodels">Adding Models</a> &nbsp;|&nbsp; <a href="#updatemodels">Updating Models</a> &nbsp;|&nbsp; <a href="#addresults">Adding Results</a>
</div>

<h2 id="info">Information for Contributors</h2>
<p>
We welcome contributions that extend the <a href="index.html">Quantitative Formal Model Repository</a> by <a href="#addmodels">adding new models</a>, <a href="#updatemodels">updating existing models</a>, and <a href="#addresults">adding new experimental results</a>.
We welcome contributions that extend the <a href="index.html">Quantitative Verification Benchmark Set</a> by <a href="#addmodels">adding new models</a>, <a href="#updatemodels">updating existing models</a>, and <a href="#addresults">adding new experimental results</a>.
Before you submit, please carefully read and follow the general instructions as well as those specific for your type of contribution below.
If you have questions about contributing, contact <script type="text/javascript">WriteMailLink('n.etnewtu@snnamtrah.a:otliaml', 'nnamtraH dnrAs');</script>.
</p>
Expand All @@ -26,20 +26,20 @@ <h3>How to submit</h3>
Submissions via email will be committed to our <a href="https://github.com/ahartmanns/qcomp">Git repository</a> in your name; please mention your full name and the email address of your GitHub account in your email.
For pull requests, we require all commits to be in your full name.
Every submission should only contain a single contribution, e.g. one new model, or an update to one existing model.
<!-- The repository does not require any server-side infrastructure to run.
<!-- The benchmark set does not require any server-side infrastructure to run.
Please test your contribution before submitting by cloning our Git repository and applying your changes to it.-->
</p>

<h3>Licensing</h3>
<p>
All data contributed to the repository will be redistributed under the terms of the open-access <a href="http://creativecommons.org/licenses/by/4.0/">CC-BY 4.0</a> license.
All data contributed to the benchmark set will be redistributed under the terms of the open-access <a href="http://creativecommons.org/licenses/by/4.0/">CC-BY 4.0</a> license.
Before submitting, make sure that you have the right to make your contribution publically available under this license and include a statement to this effect in your email.
If you submit via pull request, send an email (from the email address associated with your GitHub account) with such a statement to <script type="text/javascript">WriteMailLink('n.etnewtu@snnamtrah.a:otliaml', 'nnamtraH dnrAs');</script> before creating the pull request.
</p>

<h2 id="addmodels">Adding New Models</h2>
<p>
We welcome contributions of new models that extend the repository.
We welcome contributions of new models that extend the benchmark set.
Every model must be
</p>
<ul class="text continue">
Expand All @@ -50,7 +50,7 @@ <h2 id="addmodels">Adding New Models</h2>
available in the <a href="http://www.jani-spec.org/">JANI</a> model format in addition to its original modelling formalism (see our <a href="conversions.html">list of existing JANI converters</a>);
</li>
<li>
tested to work with one tool given the JANI translation and at least one parameter configuration, where the test is documented as an experimental result in the repository; and be
tested to work with one tool given the JANI translation and at least one parameter configuration, where the test is documented as an experimental result in the benchmark set; and be
</li>
<li>
maintained, i.e. the submitter must be willing and available to answer questions about the model and review update submissions, for a reasonable amount of years after the submission.
Expand All @@ -69,31 +69,31 @@ <h2 id="addmodels">Adding New Models</h2>
Has it been developed to solve a challenging industrial problem?
</li>
<li>
Is the type of model – its modelling formalism or the kind of system it represents – underrepresented in the repository?
Is the type of model – its modelling formalism or the kind of system it represents – underrepresented in the benchmark set?
</li>
<li>
Is it challenging to analyse due to its size, other structural aspects, or the properties to check?
</li>
</ul>
<p class="continue">
Very briefly state this reasoning in the <tt>notes</tt> or <tt>challenge</tt> attribute of the model metadata.
Once you have established that you have the right to release the model under the terms of the <a href="http://creativecommons.org/licenses/by/4.0/">CC-BY 4.0</a> license (see above), that it satisfies the above requirements, and that it is interesting, please do the following steps to contribute it to the repository:
Once you have established that you have the right to release the model under the terms of the <a href="http://creativecommons.org/licenses/by/4.0/">CC-BY 4.0</a> license (see above), that it satisfies the above requirements, and that it is interesting, please do the following steps to contribute it to the benchmark set:
</p>
<ol class="text continue">
<li>
Clone the <a href="https://github.com/ahartmanns/qcomp">Git repository</a>.
</li>
<li>
Choose a <tt>short</tt> name for your model.
Follow the short name patterns established by the existing models in the repository.
Follow the short name patterns established by the existing models in the benchmark set.
</li>
<li>
In the folder corresponding to the mathematical semantics of your model (e.g. <tt>benchmarks/ma</tt> for Markov automata, etc.), create a new subfolder with the exact <tt>short</tt> name for your model.
</li>
<li>
Place the original model file and its JANI translation into that subfolder.
Use the "short" name of the model for the file names of all model files (original and JANI) wherever possible.
If a file contains hardcoded parameters, use the short name of the model, followed by a dot (<tt>.</tt>), followed by the hardcoded parameter values separated by dashes (<tt>-</tt>) in the order in which they appear on the repository's website, followed by the file extension.
If a file contains hardcoded parameters, use the short name of the model, followed by a dot (<tt>.</tt>), followed by the hardcoded parameter values separated by dashes (<tt>-</tt>) in the order in which they appear on the benchmark set's website, followed by the file extension.
</li>
<li>
In the same subfolder, create a file <tt>index.json</tt> containing the metadata for your model.
Expand All @@ -106,8 +106,8 @@ <h2 id="addmodels">Adding New Models</h2>
Use title capitalisation for the model's <tt>name</tt>.
</li>
<li>
Whenever possible, use a citable document for the <tt>source</tt> (i.e. link to a DOI in a format recognised by the repository's website).
This link will be labelled "first presented in", and users of the repository are asked to cite this document when using the model.
Whenever possible, use a citable document for the <tt>source</tt> (i.e. link to a DOI in a format recognised by the benchmark set's website).
This link will be labelled "first presented in", and users of the benchmark set are asked to cite this document when using the model.
</li>
<li>
All <tt>references</tt> must be referred to in the <tt>description</tt> (use <tt>[1]</tt> to refer to the first reference, <tt>[2]</tt> for the second, etc.; use <tt>[0]</tt> to refer to the <tt>source</tt>).
Expand Down Expand Up @@ -142,7 +142,7 @@ <h2 id="addmodels">Adding New Models</h2>

<h2 id="updatemodels">Updating Existing Models</h2>
<p>
Existing models within the repository may be updated to correct modelling errors, add parameters, or add properties.
Existing models within the benchmark set may be updated to correct modelling errors, add parameters, or add properties.
An update should make the least amount of changes necessary to achieve its goal.
These are the recommended steps to submit an update of an existing model:
</p>
Expand Down Expand Up @@ -180,7 +180,7 @@ <h2 id="addresults">Adding New Results</h2>
Add the <tt>.json</tt> files and tool output logs describing your results to the <tt>results</tt> subfolder of the corresponding model.
The names of the files should be the name of the tool followed by a dot (<tt>.</tt>),
followed by the tool variant used and a dot (if any),
followed by all parameter values separated by dashes (<tt>-</tt>) in the order in which they appear on the repository's website and a dot,
followed by all parameter values separated by dashes (<tt>-</tt>) in the order in which they appear on the benchmark set's website and a dot,
followed by the date (in <tt>YYYY-MM-DD</tt> format) of the results and a dot,
followed by the file extension.
For example: <tt>Storm.exact.3-4-3.2018-10-03.json</tt>.
Expand Down
6 changes: 3 additions & 3 deletions benchmarks/conversions.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,20 +2,20 @@
<html>
<head>
<meta charset="UTF-8">
<title>QComp - Quantitative Formal Models Repository - qcomp.org</title>
<title>QComp - Quantitative Verification Benchmark Set - qcomp.org</title>
<link rel="stylesheet" type="text/css" href="../style.css">
<script type="text/javascript" src="../script.js"></script>
</head>
<body onload="init()">

<h1>Quantitative Formal Model Repository</h1>
<h1>Quantitative Verification Benchmark Set</h1>
<div class="belowh1">
<a href="index.html">⮌</a> &nbsp;|&nbsp; <a href="#otherstojani">Other Models to JANI</a> &nbsp;|&nbsp; <a href="#janitojani">JANI to JANI</a>
</div>

<h2 id="otherstojani">Conversion of Models to JANI</h2>
<p>
All models in the <a href="index.html">Quantitative Formal Model Repository</a> need to be available in the <a href="http://www.jani-spec.org/">JANI</a> model format.
All models in the <a href="index.html">Quantitative Verification Benchmark Set</a> need to be available in the <a href="http://www.jani-spec.org/">JANI</a> model format.
The following conversions from other modelling formalisms are available in tools:
</p>
<ul class="text continue">
Expand Down
8 changes: 4 additions & 4 deletions benchmarks/index.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@
<html>
<head>
<meta charset="UTF-8">
<title>QComp - Quantitative Formal Models Repository - qcomp.org</title>
<title>QComp - Quantitative Verification Benchmark Set - qcomp.org</title>
<link rel="stylesheet" type="text/css" href="../style.css">
<script type="text/javascript" src="../libraries/knockout.js"></script>
<script type="text/javascript" src="../script.js"></script>
Expand All @@ -11,17 +11,17 @@
</head>
<body onload="init()">

<h1>Quantitative Formal Model Repository</h1>
<h1>Quantitative Verification Benchmark Set</h1>
<div class="belowh1">
<a href="../index.html">⮌</a> &nbsp;|&nbsp; License: <a href="http://creativecommons.org/licenses/by/4.0/">CC-BY 4.0</a> &nbsp;|&nbsp; <a href="contributing.html">Contributing</a> &nbsp;|&nbsp;&thinsp; <a href="conversions.html">JANI Converters</a>
</div>
<p>
The models and results in this repository on <a href="../index.html">qcomp.org</a> are provided as a benchmark set under the terms of the
The models and results in this benchmark set on <a href="../index.html">qcomp.org</a> are provided under the terms of the
<a href="http://creativecommons.org/licenses/by/4.0/">CC-BY 4.0</a> license.
Please cite the publication linked as "first presented in" for each model.
To contribute a new model, update an existing model, or add new results for an existing model, please consider our
<a href="contributing.html">information for contributors</a>.
For general questions or comments concerning the model repository, contact
For general questions or comments concerning the benchmark set, contact
<script type="text/javascript">WriteMailLink('n.etnewtu@snnamtrah.a:otliaml', 'nnamtraH dnrAs');</script>.
If you have questions concerning a specific model, please contact the submitter listed for that model.
</p>
Expand Down
8 changes: 4 additions & 4 deletions benchmarks/results.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@
<html>
<head>
<meta charset="UTF-8">
<title>QComp - Quantitative Formal Models Repository - qcomp.org</title>
<title>QComp - Quantitative Verification Benchmark Set - qcomp.org</title>
<link rel="stylesheet" type="text/css" href="../libraries/taucharts.css">
<link rel="stylesheet" type="text/css" href="../style.css">
<script type="text/javascript" src="../libraries/knockout.js"></script>
Expand All @@ -14,17 +14,17 @@
</head>
<body onload="init()">

<h1>Quantitative Formal Model Results Browser</h1>
<h1>Quantitative Verification Benchmark Results</h1>
<div class="belowh1">
<a href="index.html">⮌</a> &nbsp;|&nbsp; License: <a href="http://creativecommons.org/licenses/by/4.0/">CC-BY 4.0</a> &nbsp;|&nbsp; <a href="contributing.html">Contributing</a> &nbsp;|&nbsp;&thinsp; <a href="conversions.html">JANI Converters</a>
</div>
<p>
The models and results in this repository on <a href="../index.html">qcomp.org</a> are provided as a benchmark set under the terms of the
The models and results in this benchmark set on <a href="../index.html">qcomp.org</a> are provided under the terms of the
<a href="http://creativecommons.org/licenses/by/4.0/">CC-BY 4.0</a> license.
Please cite the publication linked as "first presented in" for each model.
To contribute a new model, update an existing model, or add new results for an existing model, please consider our
<a href="contributing.html">information for contributors</a>.
For general questions or comments concerning the model repository, contact
For general questions or comments concerning the benchmark set, contact
<script type="text/javascript">WriteMailLink('n.etnewtu@snnamtrah.a:otliaml', 'nnamtraH dnrAs');</script>.
If you have questions concerning a specific model, please contact the submitter listed for that model.
</p>
Expand Down
10 changes: 5 additions & 5 deletions competition/2019/index.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,7 @@ <h1>QComp 2019</h1>
<p>
The <b>2019 Comparison of Tools for the Analysis of Quantitative Formal Models</b> (<a href="../../index.html">QComp</a> 2019) is part of the <a href="https://tacas.info/toolympics.php">TACAS 2019 Toolympics</a>.
It is the first <b>friendly competition</b> among verification and analysis tools for quantitative formal models.
Based on a curated subset of benchmarks from the <a href="../../benchmarks/index.html">Quantitative Formal Model Repository</a>, QComp will compare the performance, versatility and usability of the participating tools.
Based on a curated subset of benchmarks from the <a href="../../benchmarks/index.html">Quantitative Verification Benchmark Set</a>, QComp will compare the performance, versatility and usability of the participating tools.
</p>


Expand Down Expand Up @@ -65,7 +65,7 @@ <h2 id="timeline">Timeline</h2>
<p>
We ask benchmark contributions as well as tool participation to be announced to the organisers by October 20.
This is to ensure that all benchmarks are properly tested and annotated with metadata in time by the submission deadline on October 27.
Between October 27 and November 24, the organisers and participants will select a subset of the models and properties in the <a href="../../benchmarks/index.html">repository</a> for use in the performance comparison and discuss the reference results.
Between October 27 and November 24, the organisers and participants will select a subset of the models and properties in the <a href="../../benchmarks/index.html">benchmark set</a> for use in the performance comparison and discuss the reference results.
Participants submit their tool description by December 15, which will then be edited by the organisers for inclusion in the competition report.
We currently expect the <a href="https://tacas.info/toolympics.php">Toolympics</a> deadline for a first complete version of the competition report to be around January 10, 2019.
The purpose of the re-evaluation phase in January 2019 is to allow participants to fix bugs in their tools that were not discovered in their own testing prior to the original tool submission.
Expand Down Expand Up @@ -187,7 +187,7 @@ <h2 id="evaluation">Evaluation Procedure</h2>
<p>
QComp 2019 is a flexible and friendly event.
As a <i>comparison</i>, not a competition, there is no global scoring or ranking of tools.
Instead, we collect data and publish comparison tables and diagrams about the <b>performance</b> of the participating tools on a curated selection of models from the <a href="../../benchmarks/index.html">Quantitative Formal Model Repository</a>.
Instead, we collect data and publish comparison tables and diagrams about the <b>performance</b> of the participating tools on a curated selection of models from the <a href="../../benchmarks/index.html">Quantitative Verification Benchmark Set</a>.
We analyse and highlight every tool's strengths and tradeoffs.
Equally prominently, based on input and feedback from the participants, we describe and compare the tools in terms of <b>versatility</b> and <b>usability</b>.
The entire performance evaluation and report-writing process will be performed in close collaboration with the participants to quickly include feedback and resolve any setup errors or misunderstandings early.
Expand All @@ -203,7 +203,7 @@ <h3>Performance Evaluation</h3>
Participants provide a tool package, installation instructions, and command lines/scripts to run the selected benchmarks and deliver the tool's results in a simple common format.
We plan to evaluate all tools once with the command lines provided by the participants, and once with default parameters for comparison.
For every benchmark, participants briefly explain the tool settings used, why they were chosen for the particular benchmark, and what the capabilities of their tool are (e.g. which properties of the benchmark are supported and what kind of guarantee is attached to the results provided by the tool).
We expect tools to provide results with a relative error of ± 10e-4.
We expect tools to provide results with a relative error of ± 1e-3.
Statistical tools (e.g. simulators) should provide results outside of this error bound with a probability of at most 5 %.
The competition report will not contain a performance ranking, but will provide tables, diagrams, and a discussion reporting on the runtimes achieved by the tools.
We will not directly evaluate memory usage, but note that the amount of RAM available in the central server is not high.
Expand Down Expand Up @@ -233,7 +233,7 @@ <h3>Versatility and Usability</h3>

<h3>Features of the Future</h3>
<p>
As the first iteration of a quantitative analysis competition, QComp 2019 is intentionally limited to a small set of mathematical formalisms (from Markov chains to probabilistic timed automata) and properties (probabilistic reachability and expected rewards only).
As the first iteration of a quantitative analysis competition, QComp 2019 is intentionally limited to a small set of mathematical formalisms (from Markov chains to probabilistic timed automata) and properties (probabilistic reachability, expected rewards and steady-state queries only).
However, as part of the QComp 2019 evaluation, we also hope to identify advanced and upcoming areas of interest in quantitative modelling and analysis that may be of interest for the next edition of QComp.
</p>

Expand Down
Loading

0 comments on commit 84c9d80

Please sign in to comment.