Skip to content

Commit

Permalink
upgrade code to use the new incremental solver
Browse files Browse the repository at this point in the history
  • Loading branch information
@yanntm
yanntm committed May 22, 2024
1 parent 624a794 commit dda5e79
Showing 1 changed file with 56 additions and 47 deletions.
103 changes: 56 additions & 47 deletions ...pplication.pnmcc/src/fr/lip6/move/gal/application/solver/ExclusiveImplicantsComputer.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -11,16 +11,17 @@

import android.util.SparseIntArray;
import fr.lip6.move.gal.application.mcc.MccTranslator;
import fr.lip6.move.gal.mcc.properties.ConcurrentHashDoneProperties;
import fr.lip6.move.gal.mcc.properties.DoneProperties;
import fr.lip6.move.gal.structural.FlowPrinter;
import fr.lip6.move.gal.structural.InvariantCalculator;
import fr.lip6.move.gal.structural.SparsePetriNet;
import fr.lip6.move.gal.structural.expr.AtomicPropRef;
import fr.lip6.move.gal.structural.expr.Expression;
import fr.lip6.move.gal.structural.expr.Op;
import fr.lip6.move.gal.structural.expr.VarRef;
import fr.lip6.move.gal.structural.smt.DeadlockTester;
import fr.lip6.move.gal.structural.smt.ExprTranslator;
import fr.lip6.move.gal.util.IntMatrixCol;
import fr.lip6.move.gal.structural.smt.Problem;
import fr.lip6.move.gal.structural.smt.ProblemSet;
import fr.lip6.move.gal.structural.smt.SMTBasedReachabilitySolver;

public class ExclusiveImplicantsComputer {

Expand Down Expand Up @@ -233,7 +234,7 @@ public Constraint getConstraint() {
}
}

public static void studyImplicants(MccTranslator reader) {
public static List<Constraint> studyImplicants(MccTranslator reader) {

long time = System.currentTimeMillis();
SparsePetriNet spn = reader.getSPN();
Expand All @@ -260,41 +261,38 @@ public static void studyImplicants(MccTranslator reader) {
}
}

if (constraints.size() > 0) {
System.out.println("Proved "+constraints.size()+" constraints trivially:");
if (DEBUG >= 1)
for (Constraint c : constraints) {
System.out.println(c.printConstraint(spn));
}
}

// This invocation prepares and then runs the SMT solver on the problems
// result is for each problem either a "witness" state if problem is
// result is for each problem either "unsolved" if problem is
// SAT/unknown/timeout...,
// or null if the problem is UNSAT.
List<SparseIntArray> verdicts = solveDrainProblems(spn, problems);

for (int id = 0, ide = problems.size(); id < ide; id++) {
DrainProblem dp = problems.get(id);
if (verdicts.get(id) == null) {
// "null" reflects an UNSAT result for this problem.
if (DEBUG >= 1)
System.out.println("Problem " + dp.getConstraint().getType() + " is true.");

constraints.add(dp.getConstraint());
// A="+printPnames(a, spn.getPnames())+ " B=" + printPnames(b, spn.getPnames())
// + " T=" + printPnames(dp.setsT.get(0), spn.getTnames()) );
} else {
// any other reply is a SAT or unknown answer
if (DEBUG >= 1)
System.out.println("Could not prove " + dp.getConstraint().printConstraint(spn));
// or "solved" if the problem is UNSAT.
List<Constraint> solved = solveDrainProblems(spn, problems);

}
}

// Print the constraints we managed to prove
for (Constraint c : constraints) {
System.out.println("Proved that : " + c.printConstraint(spn));
if (solved.size() > 0) {
System.out.println("Proved "+constraints.size()+" constraints with SMT :");
if (DEBUG >= 1)
for (Constraint c : solved) {
System.out.println(c.printConstraint(spn));
}
}

// reader.getSPN().getProperties().clear();
if (DEBUG >= 0)
FlowPrinter.drawNet(reader.getSPN(), reader.getSPN().getName());

System.out.println("In total, drain approach introduced " + constraints.size() + " constraints in "
System.out.println("In total, drain approach introduced " + constraints.size() + " trivial constraints and "+ solved.size() + " constraints requiring SMT in "
+ (System.currentTimeMillis() - time) + " ms.");
constraints.addAll(solved);
return constraints;
}

private static void testInvariants(SparseIntArray a, SparseIntArray b, MccTranslator reader,
Expand Down Expand Up @@ -408,32 +406,43 @@ private static void testInvariants(SparseIntArray a, SparseIntArray b, MccTransl

}

private static List<SparseIntArray> solveDrainProblems(SparsePetriNet spn, List<DrainProblem> problems) {
private static List<Constraint> solveDrainProblems(SparsePetriNet spn, List<DrainProblem> problems) {

int tcsize = problems.size();
if (problems.size() == 0)
return Collections.emptyList();
List<Script> properties = new ArrayList<>();

for (int probid = 0; probid < tcsize; probid++) {
DrainProblem dp = problems.get(probid);
Expression totest = dp.computeDrainProblemCondition(spn);

IExpr smtexpr = totest.accept(new ExprTranslator());
Script property = new Script();
ICommand propAssert = new C_assert(smtexpr);
property.add(propAssert);
properties.add(property);

DoneProperties done = new ConcurrentHashDoneProperties();
ProblemSet ps = new ProblemSet(done);
int i = 0;
for (DrainProblem p : problems) {
Problem pp = new Problem("p"+(i++),true,p.computeDrainProblemCondition(spn));
ps.addProblem(pp);
}

List<Integer> representative = new ArrayList<>();
IntMatrixCol sumMatrix = InvariantCalculator.computeReducedFlow(spn, representative);

List<SparseIntArray> pors = new ArrayList<>();

List<Integer> repr = new ArrayList<>();
int timeout = 30; // in seconds
return DeadlockTester.escalateRealToInt(spn, properties, timeout, false /* no witness needed */, representative,
pors, sumMatrix);
int solved = SMTBasedReachabilitySolver.solveProblems(ps, spn, timeout, false /* don't negate*/, repr);

System.out.println("Solved "+solved+" problems out of "+tcsize + " drain problems.");


List<Constraint> constraints = new ArrayList<>();
for (Problem p : ps.getSolved()) {
int id = Integer.parseInt(p.getName().substring(1));
DrainProblem dp = problems.get(id);
constraints .add(dp.getConstraint());
}

if (DEBUG >= 1) {
for (Problem p : ps.getSolved()) {
int id = Integer.parseInt(p.getName().substring(1));
DrainProblem dp = problems.get(id);
System.out.println("Could not prove " + dp.getConstraint().printConstraint(spn));
}
}

return constraints;
}

private static String printPnames(SparseIntArray a, List<String> pnames) {
Expand Down

0 comments on commit dda5e79

Please sign in to comment.