From bac19db31f021db0ea58cc39985f40003b20a8f7 Mon Sep 17 00:00:00 2001 From: Nuno Macedo Date: Fri, 23 Sep 2016 18:31:55 +0100 Subject: [PATCH] Update README.md --- README.md | 49 ++++++++++++++++++++++++++++++++++++++++++------- 1 file changed, 42 insertions(+), 7 deletions(-) diff --git a/README.md b/README.md index b5e667e5..81af9856 100644 --- a/README.md +++ b/README.md @@ -1,12 +1,47 @@ -# Pardinus +Pardinus +======= -Pardinus - Kodkod's (slightly bulkier) Iberian cousin +Pardinus is Kodkod's (slightly bulkier) Iberian cousin This repository includes the source code for the Pardinus solver, an extension to the [Kodkod](http://alloy.mit.edu/kodkod/index.html) solver for relational logic. It extends Kodkod with the following functionalities: -* Target-oriented and weighted-target oriented model finding (@tmguimaraes, @nmacedo, @alcinocunha); -* Decomposed parallelized model finding (@EduardoPessoa, @nmacedo, @alcinocunha); -* Model finding over temporal relational formulas (@EduardoPessoa, @nmacedo, @alcinocunha); -* Support for unbounded relational model finding (planned). +* Target-oriented and weighted-target oriented model finding +* Decomposed parallelized model finding +* Model finding over temporal relational formulas +* Support for unbounded relational model finding (planned) -Pardinus is open-source and available under the [MIT license](LICENSE), as is Kodkod. However, the implementation relies on third-party SAT solvers ([SAT4J](http://www.sat4j.org), [MiniSat](http://minisat.se), [Glucose](http://www.labri.fr/perso/lsimon/glucose/), and [(P)Lingeling](http://fmv.jku.at/lingeling/)), some of which are released under stricter licenses. Please see the solver licenses for details. +Pardinus is developed at the High-Assurance Software Laboratory ([HASLab](http://haslab.di.uminho.pt)), from INESC TEC and University of Minho, and is led by Alcino Cunha and Nuno Macedo. It is used as a back-end for [Electrum Analyzer](), an extension to the Alloy Analyzer. + +Pardinus is open-source and available under the [MIT license](LICENSE), as is Kodkod. However, the implementation relies on third-party solvers ([SAT4J](http://www.sat4j.org), [MiniSat](http://minisat.se), [Glucose/Syrup](http://www.labri.fr/perso/lsimon/glucose/), [(P)Lingeling](http://fmv.jku.at/lingeling/), and [Yices](http://yices.csl.sri.com)), some of which are released under stricter licenses (see the various LICENSE files in the distribution for details) + +Pardinus can be built and run following the instructions from [Kodkod](https://github.com/emina/kodkod/blob/master/README.md#building-and-installing-kodkod). + +## Collaborators +- Alcino Cunha, 2013 - present +- Nuno Macedo, 2013 - present +- Tiago Guimarães, 2013 - 2014 +- Eduardo Pessoa, 2015 - 2016 + +## History +### Pardinus (0.3.0) (September 2016) + +- Initial support for temporal model finding +- Support for [Electrum Analyzer 0.2]() + +### Pardinus (0.2.0) (April 2016) + +- Initial support for decomposed model finding +- Support for Syrup (parallel Glucose) + +### Pardinus (0.1.1) (October 2014) + +- Support for weighted target-oriented model finding +- Merged Alloy Analyzer's Kodkod 2.0 tweaks into Kodkod 2.1 +- Supported scenario exploration operations from [extended Alloy Analyzer](toalloy.jar) +- Described in the FASE 15 [paper](http://dx.doi.org/10.1007/978-3-662-46675-9_20) + +### Pardinus (0.1.0) (October 2013) + +- Initial support for target-oriented model finding +- Extended support to Max-SAT SAT4J and Yices +- Described in the FASE 14 [paper](http://dx.doi.org/10.1007/978-3-642-54804-8_2)