Pardinus is Kodkod's (slightly bulkier) Iberian cousin.

This repository includes the source code for the Pardinus solver, an extension to the Kodkod solver for relational logic. It extends Kodkod with the following functionalities:

• Target-oriented and weighted-target oriented model finding
• Model finding over (past and future) LTL relational formulas
• Symbolic bound declarations
• Decomposed parallelized model finding
• Unbounded relational model finding

Pardinus is developed at the High-Assurance Software Laboratory (HASLab), 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, which is itself an extension to the Alloy Analyzer.

Pardinus is open-source and available under the MIT license, as is Kodkod. However, the implementation relies on third-party solvers (SAT4J, MiniSat, Glucose/Syrup, (P)Lingeling, Yices, and Electrod), some of which are released under stricter licenses (see the various LICENSE files in the distribution for details).

Pardinus inherits Kodkod's building and running instructions.

Kodkod uses the Waf build system, which requires Python 2.5 or later. You will also need Java 8 and a C/C++ compiler, and your JAVA_HOME environment variable needs to point to the JDK 8 home directory.

• Set the JAVA_HOME variable. For example, on OS X:

  $ export JAVA_HOME=`/usr/libexec/java_home`

• Clone the Pardinus repository:

  $ git clone https://github.com/haslab/Pardinus.git
$ cd Pardinus

• Download Waf 1.8.12 and make it executable:

  $ wget --no-check-certificate https://waf.io/waf-1.8.12
$ chmod u+x waf-1.8.12
$ alias waf=$PWD/waf-1.8.12

• Build the native libraries, pardinus.jar, and examples.jar and install them into the pardinus/lib directory:

  $ waf configure --prefix=. --libdir=lib build install

• Nuno Macedo, HASLab, INESC TEC & Universidade do Minho, Portugal, 2013 - present
• Alcino Cunha, HASLab, INESC TEC & Universidade do Minho, Portugal, 2013 - present
• Eduardo Pessoa, HASLab, INESC TEC & Universidade do Minho, Portugal, 2015 - 2016
• Tiago Guimarães, HASLab, INESC TEC & Universidade do Minho, Portugal, 2013 - 2014

• Support for unbounded model finding in SMV through Electrod
• Support for Electrum Analyzer 1.0

• Support for symbolic bound declaration
• Described in the ATVA 17 paper

• Initial support for (past and future) temporal model finding
• Support for Electrum Analyzer 0.2

• Initial support for decomposed model finding
• Support for Syrup (parallel Glucose)

• 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
• Described in the FASE 15 paper

• Initial support for target-oriented model finding
• Extended support to Max-SAT SAT4J and Yices
• Described in the FASE 14 paper