Skip to content

Commit

Permalink
readme
Browse files Browse the repository at this point in the history
  • Loading branch information
@nmacedo
nmacedo committed Sep 27, 2016
2 parents f1f2c71 + bac19db commit 7b0c191
Show file tree
Hide file tree
Showing 12 changed files with 104 additions and 99 deletions.
16 changes: 10 additions & 6 deletions README.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ This repository includes the source code for the Pardinus solver, an extension t
* Target-oriented and weighted-target oriented model finding
* Decomposed parallelized model finding
* Model finding over temporal relational formulas
* Support for unbounded relational model finding
* Support for unbounded relational model finding (planned)

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.

Expand All @@ -22,21 +22,25 @@ Pardinus can be built and run following the instructions from [Kodkod](https://g
- Eduardo Pessoa, 2015 - 2016

## History
### Pardinus (0.3.0) (September 2016) <!--- TRUST Workshop 16 -->
### Pardinus (0.3.0) (September 2016)
<!--- TRUST Workshop 16 -->
- Initial support for temporal model finding
- Support for Electrum Analyzer 0.2
- Support for [Electrum Analyzer 0.2]()

### Pardinus (0.2.0) (April 2016) <!--- ASE16 submission -->
### Pardinus (0.2.0) (April 2016)
<!--- ASE16 submission -->
- Initial support for decomposed model finding
- Support for Syrup (parallel Glucose)

### Pardinus (0.1.1) (October 2014) <!--- FASE15 submission -->
### Pardinus (0.1.1) (October 2014)
<!--- FASE15 submission -->
- 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) <!--- FASE14 submission -->
### Pardinus (0.1.0) (October 2013)
<!--- FASE14 submission -->
- 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)
Expand Down
4 changes: 2 additions & 2 deletions examples/kodkod/examples/pardinus/target/OwnGranpa.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@
import kodkod.instance.*;
import kodkod.engine.*;
import kodkod.engine.Solver.TSolutionIterator;
import kodkod.engine.config.ExtendedOptions;
import kodkod.engine.config.BoundedExtendedOptions;
import kodkod.engine.config.TargetOptions.TMode;
import kodkod.engine.satlab.SATFactory;

Expand Down Expand Up @@ -221,7 +221,7 @@ public static void main(String[] args) throws Exception {
ws.put("String", 1);


ExtendedOptions opt = new ExtendedOptions();
BoundedExtendedOptions opt = new BoundedExtendedOptions();
opt.setSolver(SATFactory.externalPMaxYices("/Users/nmm/Documents/Work/Programming/AlloyExplore/kodextension/lib/yices-1.0.38/bin/yices", "owngrandpa.wcnf", 2000, "-d","-e","-ms","-mw",""+2000));
// opt.setSolver(SATFactory.PMaxSAT4J);
opt.setBitwidth(1);
Expand Down
40 changes: 20 additions & 20 deletions examples/kodkod/examples/pardinus/temporal/DijkstraP.java
View file
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
/*
* Kodkod -- Copyright (c) 2005-present, Emina Torlak
* Pardinus -- Copyright (c) 2014-present, Nuno Macedo
* Pardinus -- Copyright (c) 2013-present, Nuno Macedo, INESC TEC
*
* Permission is hereby granted, free of charge, to any person obtaining a copy
* of this software and associated documentation files (the "Software"), to deal
Expand Down Expand Up @@ -30,7 +30,7 @@
import kodkod.ast.Variable;
import kodkod.engine.Solution;
import kodkod.engine.Solver;
import kodkod.engine.config.ExtendedOptions;
import kodkod.engine.config.BoundedExtendedOptions;
import kodkod.engine.decomp.DModel;
import kodkod.engine.ltl2fol.TemporalFormulaSlicer;
import kodkod.engine.satlab.SATFactory;
Expand Down Expand Up @@ -174,21 +174,21 @@ public Formula isStalled(Expression p) {
public Formula grabMutex(Expression p, Expression m) {
final Formula f1 = isStalled(p).not().and(m.in(p.join(holds)).not());
final Formula isFree = isFree(m);
final Formula f2 = p.join(holds.post()).eq(p.join(holds).union(m));/*
final Formula f2 = p.join(holds.prime()).eq(p.join(holds).union(m));/*
* TEMPORAL
* OP
*/
final Formula f3 = p.join(waits.post()).no();/* TEMPORAL OP */
final Formula f3 = p.join(waits.prime()).no();/* TEMPORAL OP */
final Formula f4 = isFree.implies(f2.and(f3));
final Formula f5 = p.join(holds.post()).eq(p.join(holds));/* TEMPORAL OP */
final Formula f6 = p.join(waits.post()).eq(m);/* TEMPORAL OP */
final Formula f5 = p.join(holds.prime()).eq(p.join(holds));/* TEMPORAL OP */
final Formula f6 = p.join(waits.prime()).eq(m);/* TEMPORAL OP */
final Formula f7 = isFree.not().implies(f5.and(f6));
final Variable otherProc = Variable.unary("otherProc");
final Formula f8 = otherProc.join(holds.post()).eq(otherProc.join(holds));/*
final Formula f8 = otherProc.join(holds.prime()).eq(otherProc.join(holds));/*
* TEMPORAL
* OP
*/
final Formula f9 = otherProc.join(waits.post()).eq(otherProc.join(waits));/*
final Formula f9 = otherProc.join(waits.prime()).eq(otherProc.join(waits));/*
* TEMPORAL
* OP
*/
Expand Down Expand Up @@ -223,32 +223,32 @@ public Formula grabMutex(Expression p, Expression m) {
*/
public Formula releaseMutex(Expression p, Expression m) {
final Formula f1 = isStalled(p).not().and(m.in(p.join(holds)));
final Formula f2 = p.join(holds.post()).eq(p.join(holds).difference(m));/*
final Formula f2 = p.join(holds.prime()).eq(p.join(holds).difference(m));/*
* TEMPORAL
* OP
*/
final Formula f3 = p.join(waits.post()).no();/* TEMPORAL OP */
final Formula f3 = p.join(waits.prime()).no();/* TEMPORAL OP */
final Expression cexpr = m.join((waits).transpose());
final Formula f4 = m.join(holds.post().transpose()).no();/* TEMPORAL OP */
final Formula f5 = m.join(waits.post().transpose()).no();/* TEMPORAL OP */
final Formula f4 = m.join(holds.prime().transpose()).no();/* TEMPORAL OP */
final Formula f5 = m.join(waits.prime().transpose()).no();/* TEMPORAL OP */
final Formula f6 = cexpr.no().implies(f4.and(f5));
final Variable lucky = Variable.unary("lucky");
final Formula f7 = m.join(waits.post().transpose()).eq(m.join(waits.transpose()).difference(lucky));/*
final Formula f7 = m.join(waits.prime().transpose()).eq(m.join(waits.transpose()).difference(lucky));/*
* TEMPORAL
* OP
*/
final Formula f8 = m.join(holds.post().transpose()).eq(lucky);/*
final Formula f8 = m.join(holds.prime().transpose()).eq(lucky);/*
* TEMPORAL
* OP
*/
final Formula f9 = f7.and(f8).forSome(lucky.oneOf(m.join(waits.transpose())));
final Formula f10 = cexpr.some().implies(f9);
final Variable mu = Variable.unary("mu");
final Formula f11 = mu.join(waits.post().transpose()).eq(mu.join(waits.transpose()));/*
final Formula f11 = mu.join(waits.prime().transpose()).eq(mu.join(waits.transpose()));/*
* TEMPORAL
* OP
*/
final Formula f12 = mu.join(holds.post().transpose()).eq(mu.join(holds.transpose()));/*
final Formula f12 = mu.join(holds.prime().transpose()).eq(mu.join(holds.transpose()));/*
* TEMPORAL
* OP
*/
Expand All @@ -275,8 +275,8 @@ public Formula releaseMutex(Expression p, Expression m) {
* </pre>
*/
public Formula grabOrRelease() {
final Formula f1 = holds.post().eq(holds);/* TEMPORAL OP */
final Formula f2 = waits.post().eq(waits);/* TEMPORAL OP */
final Formula f1 = holds.prime().eq(holds);/* TEMPORAL OP */
final Formula f2 = waits.prime().eq(waits);/* TEMPORAL OP */
final Variable p = Variable.unary("p");
final Variable m = Variable.unary("m");
final Decls d = p.oneOf(Process).and(m.oneOf(Mutex));
Expand Down Expand Up @@ -320,7 +320,7 @@ public Formula deadlock() {
*/
public Formula grabbedInOrder() {
final Expression had = Process.join(holds);
final Expression have = Process.join(holds.post());/* TEMPORAL OP */
final Expression have = Process.join(holds.prime());/* TEMPORAL OP */
final Expression grabbed = have.difference(had);
return grabbed.some().implies(grabbed.in(had.join(mord.closure()))).always();/*
* TEMPORAL
Expand Down Expand Up @@ -421,7 +421,7 @@ public int getBitwidth() {
public static void main(String[] args) {
DijkstraP model = new DijkstraP(new String[] { "3", "3", "SAT" });

ExtendedOptions opt = new ExtendedOptions();
BoundedExtendedOptions opt = new BoundedExtendedOptions();
opt.setSolver(SATFactory.Glucose);
opt.setMaxTraceLength(10);
Solver solver = new Solver(opt);
Expand Down
35 changes: 18 additions & 17 deletions examples/kodkod/examples/pardinus/temporal/HotelP.java
View file
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
/*
* Kodkod -- Copyright (c) 2005-present, Emina Torlak
* Pardinus -- Copyright (c) 2014-present, Nuno Macedo
* Pardinus -- Copyright (c) 2013-present, Nuno Macedo, INESC TEC
*
* Permission is hereby granted, free of charge, to any person obtaining a copy
* of this software and associated documentation files (the "Software"), to deal
Expand Down Expand Up @@ -31,7 +31,7 @@
import kodkod.engine.Evaluator;
import kodkod.engine.Solution;
import kodkod.engine.TemporalKodkodSolver;
import kodkod.engine.config.ExtendedOptions;
import kodkod.engine.config.BoundedExtendedOptions;
import kodkod.engine.decomp.DModel;
import kodkod.engine.ltl2fol.TemporalFormulaSlicer;
import kodkod.engine.satlab.SATFactory;
Expand Down Expand Up @@ -238,11 +238,11 @@ private Formula entry(Variable r, Variable k, Variable g) {
Formula x581 = x583.or(x593);

Formula x576 = k.in(g.join(gkeys)); // k in g.keys.t
Formula x609 = (r.join(current.post())).eq(k);/* TEMPORAL OP */// r.current.t'
Formula x609 = (r.join(current.prime())).eq(k);/* TEMPORAL OP */// r.current.t'
// = k

Variable r1 = Variable.unary("r'");
Formula x641 = (r1.join(current)).eq(r1.join(current.post()));/*
Formula x641 = (r1.join(current)).eq(r1.join(current.prime()));/*
* TEMPORAL
* OP
*/
Expand All @@ -253,26 +253,26 @@ private Formula entry(Variable r, Variable k, Variable g) {
// =
// x.current.t'

Formula x614 = gkeys.eq(gkeys.post());/* TEMPORAL OP */// gkeys.t =
Formula x614 = gkeys.eq(gkeys.prime());/* TEMPORAL OP */// gkeys.t =
// gkeys.t'
Formula x629 = (lastkey).eq(lastkey.post());/* TEMPORAL OP */// lastley.t
Formula x629 = (lastkey).eq(lastkey.prime());/* TEMPORAL OP */// lastley.t
// =
// lastkey.t'
Formula x647 = (occupant).eq(occupant.post()); /* TEMPORAL OP */// occupant.t
Formula x647 = (occupant).eq(occupant.prime()); /* TEMPORAL OP */// occupant.t
// =
// occupant.t'
Formula entry = Formula.compose(FormulaOperator.AND, x576, x581, x614, x629, x637, x647, x609);
return entry;
}

private Formula checkin(Variable r, Variable k, Variable g) {
Formula x398 = g.join(gkeys.post()).eq((g.join(gkeys)).union(k)); // g.keys.t'
Formula x398 = g.join(gkeys.prime()).eq((g.join(gkeys)).union(k)); // g.keys.t'
// =
// g.keys.t
// +
// k
Formula x407 = (r.join(occupant)).no(); // no r.occupant.t
Formula x411 = (lastkey.post()).eq((lastkey).override(r.product(k))); // lastkey.t'
Formula x411 = (lastkey.prime()).eq((lastkey).override(r.product(k))); // lastkey.t'
// =
// lastkey.t
// ++
Expand All @@ -284,16 +284,16 @@ private Formula checkin(Variable r, Variable k, Variable g) {
Expression x420 = (((r.join(lastkey)).join(key_next.closure())).intersection(r.join(rkeys))).difference(x428);
Formula x419 = k.eq(x420); // k = (r.lastkey.t.next+ & r.keys) -
// (r.lastkey.t.next+ & r.keys).next+
Formula x439 = (occupant.post()).eq((occupant).union(r.product(g))); // occupant.t'
Formula x439 = (occupant.prime()).eq((occupant).union(r.product(g))); // occupant.t'
// =
// occupant.t
// +
// r
// ->
// g
Formula x447 = (current).eq(current.post()); // current.t = current.t'
Formula x447 = (current).eq(current.prime()); // current.t = current.t'
Variable g1 = Variable.unary("g1");
Formula x461 = (g1.join(gkeys)).eq(g1.join(gkeys.post()));
Formula x461 = (g1.join(gkeys)).eq(g1.join(gkeys.prime()));
Formula x457 = x461.forAll(g1.oneOf(guest.difference(g))); // all g1 :
// Guest - g
// |
Expand All @@ -306,16 +306,16 @@ private Formula checkin(Variable r, Variable k, Variable g) {

private Formula checkout(Variable g) {
Formula x337 = ((occupant).join(g)).some(); // some (occupant.t).g
Formula x343 = occupant.post().eq((occupant).difference(room.product(g))); // occupant.t'
Formula x343 = occupant.prime().eq((occupant).difference(room.product(g))); // occupant.t'
// =
// occupant.t
// -
// room
// ->
// g
Formula x351 = (current).eq(current.post()); // current.t = current.t'
Formula x352 = (gkeys).eq(gkeys.post()); // lastkey.t = lastkey.t'
Formula x353 = (lastkey).eq(lastkey.post()); // gkeys.t = gkeys.t'
Formula x351 = (current).eq(current.prime()); // current.t = current.t'
Formula x352 = (gkeys).eq(gkeys.prime()); // lastkey.t = lastkey.t'
Formula x353 = (lastkey).eq(lastkey.prime()); // gkeys.t = gkeys.t'
Formula checkout = x337.and(x343.and(x351)).and(x352).and(x353);
return checkout;
}
Expand Down Expand Up @@ -390,11 +390,12 @@ public int getBitwidth() {
public static void main(String[] args) {
HotelP model = new HotelP(new String[] { "3", "INTERVENES" });

ExtendedOptions opt = new ExtendedOptions();
BoundedExtendedOptions opt = new BoundedExtendedOptions();
opt.setSolver(SATFactory.Glucose);
opt.setMaxTraceLength(10);
TemporalKodkodSolver solver = new TemporalKodkodSolver(opt);
TemporalBounds tbmpbound = model.bounds();
System.out.println(tbmpbound.toString2());
Solution sol = solver.solveAll(model.finalFormula(), tbmpbound).next();
System.out.println(sol);
if (sol.sat()) {
Expand Down
14 changes: 7 additions & 7 deletions examples/kodkod/examples/pardinus/temporal/RingP.java
View file
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
/*
* Kodkod -- Copyright (c) 2005-present, Emina Torlak
* Pardinus -- Copyright (c) 2014-present, Nuno Macedo
* Pardinus -- Copyright (c) 2013-present, Nuno Macedo, INESC TEC
*
* Permission is hereby granted, free of charge, to any person obtaining a copy
* of this software and associated documentation files (the "Software"), to deal
Expand All @@ -25,7 +25,7 @@
import kodkod.ast.*;
import kodkod.engine.Solution;
import kodkod.engine.Solver;
import kodkod.engine.config.ExtendedOptions;
import kodkod.engine.config.BoundedExtendedOptions;
import kodkod.engine.decomp.DModel;
import kodkod.engine.ltl2fol.TemporalFormulaSlicer;
import kodkod.engine.satlab.SATFactory;
Expand Down Expand Up @@ -146,8 +146,8 @@ public Formula step(Expression p) {
final Expression from = p.join(toSend);
final Expression to = p.join(succ).join(toSend);

final Expression fromPost = p.join(toSend.post());/* TEMPORAL OP */
final Expression toPost = p.join(succ).join(toSend.post());/*
final Expression fromPost = p.join(toSend.prime());/* TEMPORAL OP */
final Expression toPost = p.join(succ).join(toSend.prime());/*
* TEMPORAL
* OP
*/
Expand All @@ -173,7 +173,7 @@ public Formula step(Expression p) {
* <pre>
*/
public Formula skip(Expression p) {
return p.join(toSend).eq(p.join(toSend.post()));
return p.join(toSend).eq(p.join(toSend.prime()));
}/* TEMPORAL OP */

/**
Expand Down Expand Up @@ -227,7 +227,7 @@ public Formula defineElected() {
*/

final Expression comprehension = c.comprehension(p.oneOf(Process));
final Formula f2 = elected.post().eq(comprehension).always();/*
final Formula f2 = elected.prime().eq(comprehension).always();/*
* TEMPORAL
* OP
*/
Expand Down Expand Up @@ -421,7 +421,7 @@ public int getBitwidth() {
public static void main(String[] args) {
RingP model = new RingP(new String[] { "3", "BADLIVENESS", "STATIC" });

ExtendedOptions opt = new ExtendedOptions();
BoundedExtendedOptions opt = new BoundedExtendedOptions();
opt.setSolver(SATFactory.Glucose);
opt.setMaxTraceLength(10);
Solver solver = new Solver(opt);
Expand Down
Loading

0 comments on commit 7b0c191

Please sign in to comment.