Skip to content

Commit

Permalink
Merge pull request #7 from lip6/master
Browse files Browse the repository at this point in the history 
merging with last update concerning smt solver onesafe
  • Loading branch information
@bnslmn
bnslmn authored Mar 24, 2021
2 parents 53b77ef + 26e3bf2 commit 52bb31e
Show file tree
Hide file tree
Showing 8 changed files with 283 additions and 84 deletions.
12 changes: 11 additions & 1 deletion fr.lip6.move.gal.structural/src/android/util/SparseIntArray.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -85,7 +85,17 @@ public SparseIntArray(List<Integer> marks) {
}
}

public List<Integer> toList (int size) {
public SparseIntArray(int[] marks) {
// compute and set correct capacity
this ( (int) Arrays.stream(marks).filter(e -> e != 0).count());
for (int i = 0, e = marks.length ; i < e ; i++) {
int v = marks[i];
if (v != 0) {
append(i, v);
}
}
}
public List<Integer> toList (int size) {
List<Integer> res = new ArrayList<Integer> (size);
int j = 0;
for (int i=0; i < size ; i++ ) {
Expand Down
20 changes: 10 additions & 10 deletions fr.lip6.move.gal.structural/src/fr/lip6/move/gal/structural/RandomExplorer.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -58,7 +58,7 @@ public int[] runGuidedReachabilityDetection (long nbSteps, SparseIntArray parikh
for (; i < nbSteps ; i++) {
long dur = System.currentTimeMillis() - time + 1;
if (dur > 1000 * timeout) {
System.out.println("Interrupted Parikh walk after "+ i + " steps, including "+nbresets+ " resets, run timeout after "+ dur +" ms. (steps per millisecond="+ (i/dur) +" )"+ " properties seen :" + Arrays.toString(verdicts) +(DEBUG >=1 ? (" reached state " + state):"") );
System.out.println("Interrupted Parikh walk after "+ i + " steps, including "+nbresets+ " resets, run timeout after "+ dur +" ms. (steps per millisecond="+ (i/dur) +" )"+ " properties seen :" + new SparseIntArray(verdicts) +(DEBUG >=1 ? (" reached state " + state):"") );
return verdicts;
}
if (!max) {
Expand Down Expand Up @@ -122,7 +122,7 @@ public int[] runGuidedReachabilityDetection (long nbSteps, SparseIntArray parikh
}

long dur = System.currentTimeMillis() - time + 1;
System.out.println("Incomplete Parikh walk after "+ i + " steps, including "+nbresets+ " resets, run finished after "+ dur +" ms. (steps per millisecond="+ (i/dur) +" )"+ " properties seen :" + Arrays.toString(verdicts) + " could not realise parikh vector " + (DEBUG >=1 ? parikhori : "")+ (DEBUG >=1 ? (" reached state " + state):"") );
System.out.println("Incomplete Parikh walk after "+ i + " steps, including "+nbresets+ " resets, run finished after "+ dur +" ms. (steps per millisecond="+ (i/dur) +" )"+ " properties seen :" + new SparseIntArray(verdicts) + " could not realise parikh vector " + (DEBUG >=1 ? parikhori : "")+ (DEBUG >=1 ? (" reached state " + state):"") );
return verdicts;
}

Expand Down Expand Up @@ -160,7 +160,7 @@ public int[] runProbabilisticReachabilityDetection (long nbSteps, List<Expressio

long dur = System.currentTimeMillis() - time + 1;
if (dur > 1000 * timeout) {
System.out.println("Interrupted probabilistic random walk after "+ i + " steps, run timeout after "+ dur +" ms. (steps per millisecond="+ (i/dur) +" )"+ " properties seen :" + Arrays.toString(verdicts) +(DEBUG >=1 ? (" reached state " + state):"") );
System.out.println("Interrupted probabilistic random walk after "+ i + " steps, run timeout after "+ dur +" ms. (steps per millisecond="+ (i/dur) +" )"+ " properties seen :" + new SparseIntArray(verdicts) +(DEBUG >=1 ? (" reached state " + state):"") );
break;
}

Expand Down Expand Up @@ -225,20 +225,20 @@ public int[] runProbabilisticReachabilityDetection (long nbSteps, List<Expressio
if (todo.isEmpty()) {
wex.wasExhaustive = true;
if (! exhaustive) {
System.out.println("Probably explored full state space saw : "+ seen + " states, properties seen :" + Arrays.toString(verdicts) );
System.out.println("Probably explored full state space saw : "+ seen + " states, properties seen :" + new SparseIntArray(verdicts) );
} else {
System.out.println("Explored full state space saw : "+ seen + " states, properties seen :" + Arrays.toString(verdicts) );
System.out.println("Explored full state space saw : "+ seen + " states, properties seen :" + new SparseIntArray(verdicts) );
}
}
long dur = System.currentTimeMillis() - time + 1;
if (! exhaustive) {
System.out.println("Probabilistic random walk after "+ i + " steps, saw "+seen+" distinct states, run finished after "+ dur +" ms. (steps per millisecond="+ (i/dur) +" )"+ " properties seen :" + Arrays.toString(verdicts) );
System.out.println("Probabilistic random walk after "+ i + " steps, saw "+seen+" distinct states, run finished after "+ dur +" ms. (steps per millisecond="+ (i/dur) +" )"+ " properties seen :" + new SparseIntArray(verdicts) );
} else {
System.out.println("Exhaustive walk after "+ i + " steps, saw "+seen+" distinct states, run finished after "+ dur +" ms. (steps per millisecond="+ (i/dur) +" )"+ " properties seen :" + Arrays.toString(verdicts) );
System.out.println("Exhaustive walk after "+ i + " steps, saw "+seen+" distinct states, run finished after "+ dur +" ms. (steps per millisecond="+ (i/dur) +" )"+ " properties seen :" + new SparseIntArray(verdicts) );
}
} catch (OutOfMemoryError e) {
long dur = System.currentTimeMillis() - time + 1;
System.out.println("Probabilistic random walk exhausted memory after "+ i + " steps, saw "+seen+" distinct states, run finished after "+ dur +" ms. (steps per millisecond="+ (i/dur) +" )"+ " properties seen :" + Arrays.toString(verdicts) );
System.out.println("Probabilistic random walk exhausted memory after "+ i + " steps, saw "+seen+" distinct states, run finished after "+ dur +" ms. (steps per millisecond="+ (i/dur) +" )"+ " properties seen :" + new SparseIntArray(verdicts) );
}
return verdicts;
}
Expand Down Expand Up @@ -272,7 +272,7 @@ public int[] runRandomReachabilityDetection (long nbSteps, List<Expression> expr
for (; i < nbSteps ; i++) {
long dur = System.currentTimeMillis() - time + 1;
if (dur > 1000 * timeout) {
System.out.println("Interrupted "+(bestFirst>=0?"Best-First ":"")+"random walk after "+ i + " steps, including "+nbresets+ " resets, run timeout after "+ dur +" ms. (steps per millisecond="+ (i/dur) +" )"+ " properties seen :" + Arrays.toString(verdicts) +(DEBUG >=1 ? (" reached state " + state):"") );
System.out.println("Interrupted "+(bestFirst>=0?"Best-First ":"")+"random walk after "+ i + " steps, including "+nbresets+ " resets, run timeout after "+ dur +" ms. (steps per millisecond="+ (i/dur) +" )"+ " properties seen :" + new SparseIntArray(verdicts) +(DEBUG >=1 ? (" reached state " + state):"") );
return verdicts;
}
if (!max) {
Expand Down Expand Up @@ -347,7 +347,7 @@ public int[] runRandomReachabilityDetection (long nbSteps, List<Expression> expr
}
}
long dur = System.currentTimeMillis() - time + 1;
System.out.println("Incomplete "+(bestFirst>=0?"Best-First ":"")+"random walk after "+ i + " steps, including "+nbresets+ " resets, run finished after "+ dur +" ms. (steps per millisecond="+ (i/dur) +" )"+ " properties seen :" + Arrays.toString(verdicts) +(DEBUG >=1 ? (" reached state " + state):"") );
System.out.println("Incomplete "+(bestFirst>=0?"Best-First ":"")+"random walk after "+ i + " steps, including "+nbresets+ " resets, run finished after "+ dur +" ms. (steps per millisecond="+ (i/dur) +" )"+ " properties seen :" + new SparseIntArray(verdicts) +(DEBUG >=1 ? (" reached state " + state):"") );

return verdicts;
}
Expand Down
3 changes: 2 additions & 1 deletion fr.lip6.move.gal.structural/src/fr/lip6/move/gal/structural/SparsePetriNet.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -186,7 +186,7 @@ private Expression replacePredicates(Expression expr) {
return expr;
}

public void testInInitial () {
public int testInInitial () {
SparseIntArray spinit = new SparseIntArray(marks);
int proved = 0;
for (Property prop : getProperties()) {
Expand All @@ -206,6 +206,7 @@ public void testInInitial () {
if (proved > 0) {
Logger.getLogger("fr.lip6.move.gal").info("Initial state test concluded for "+proved+ " properties.");
}
return proved;
}

private Expression simplifyConstants(Expression expr, int[] perm) {
Expand Down
8 changes: 4 additions & 4 deletions pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/Application.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -365,9 +365,9 @@ public Object startNoEx(IApplicationContext context) throws Exception {
ReachabilitySolver.checkInInitial(reader.getSPN(), doneProps);
reader.getSPN().getProperties().removeIf(p -> doneProps.containsKey(p.getName()));

UpperBoundsSolver.checkInInitial(reader, doneProps);
UpperBoundsSolver.checkInInitial(reader.getSPN(), doneProps);

UpperBoundsSolver.applyReductions(reader, doneProps, solverPath, isSafe, skelBounds);
UpperBoundsSolver.applyReductions(reader.getSPN(), doneProps, solverPath, isSafe, skelBounds);

reader.getSPN().getProperties().removeIf(p -> doneProps.containsKey(p.getName()));
// checkInInitial(reader.getSpec(), doneProps, isSafe);
Expand All @@ -384,8 +384,8 @@ public Object startNoEx(IApplicationContext context) throws Exception {
System.out.println("Starting property specific reduction for " + p.getName());
r2.getSPN().getProperties().clear();
r2.getSPN().getProperties().add(p);
UpperBoundsSolver.checkInInitial(r2, doneProps);
UpperBoundsSolver.applyReductions(r2, doneProps, solverPath, isSafe, null);
UpperBoundsSolver.checkInInitial(r2.getSPN(), doneProps);
UpperBoundsSolver.applyReductions(r2.getSPN(), doneProps, solverPath, isSafe, null);
System.out.println("Ending property specific reduction for " + p.getName() + " in "
+ (System.currentTimeMillis() - time) + " ms.");
}
Expand Down
88 changes: 70 additions & 18 deletions ...ip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/GlobalPropertySolver.java
View file
Original file line number Diff line number Diff line change
@@ -1,12 +1,18 @@
package fr.lip6.move.gal.application;

import java.util.ArrayList;
import java.util.Arrays;
import java.util.Collections;
import java.util.List;
import java.util.Set;
import java.util.logging.Logger;
import java.util.Map.Entry;

import android.util.SparseIntArray;
import fr.lip6.move.gal.mcc.properties.DoneProperties;
import fr.lip6.move.gal.structural.DeadlockFound;
import fr.lip6.move.gal.structural.HLPlace;
import fr.lip6.move.gal.structural.InvariantCalculator;
import fr.lip6.move.gal.structural.NoDeadlockExists;
import fr.lip6.move.gal.structural.PetriNet;
import fr.lip6.move.gal.structural.Property;
Expand All @@ -15,6 +21,8 @@
import fr.lip6.move.gal.structural.SparsePetriNet;
import fr.lip6.move.gal.structural.expr.Expression;
import fr.lip6.move.gal.structural.expr.Op;
import fr.lip6.move.gal.structural.smt.DeadlockTester;
import fr.lip6.move.gal.util.IntMatrixCol;

public class GlobalPropertySolver {

Expand Down Expand Up @@ -146,17 +154,61 @@ public boolean solveProperty(String examination, MccTranslator reader) {
if (reader.getHLPN() == null)
buildProperties(examination, spn);

spn.simplifyLogic();
spn.toPredicates();
spn.testInInitial();
spn.removeConstantPlaces();
spn.removeRedundantTransitions(false);
spn.removeConstantPlaces();
spn.simplifyLogic();
if (isSafe) {
spn.assumeOneSafe();
try {
spn.simplifyLogic();
spn.toPredicates();
if (spn.testInInitial() > 0) {
ReachabilitySolver.checkInInitial(spn, doneProps);
}
spn.removeConstantPlaces();
spn.removeRedundantTransitions(false);
spn.removeConstantPlaces();
spn.simplifyLogic();
if (isSafe) {
spn.assumeOneSafe();
}
ReachabilitySolver.checkInInitial(spn, doneProps);
} catch (GlobalPropertySolverException e) {
return true;
}


if (ONE_SAFE.equals(examination) && reader.getHLPN() == null) {
List<Expression> toCheck = new ArrayList<>(spn.getPlaceCount());
List<Integer> maxStruct = new ArrayList<>(spn.getPlaceCount());
List<Integer> maxSeen = new ArrayList<>(spn.getPlaceCount());
for (int pid=0,e=spn.getPlaceCount() ; pid < e ; pid++) {
toCheck.add(Expression.var(pid));
maxStruct.add(-1);
maxSeen.add(1);
}
// the invariants themselves
Set<SparseIntArray> invar ;
{
// effect matrix
IntMatrixCol sumMatrix = IntMatrixCol.sumProd(-1, spn.getFlowPT(), 1, spn.getFlowTP());
invar = InvariantCalculator.computePInvariants(sumMatrix, spn.getPnames());
}

long time = System.currentTimeMillis();
UpperBoundsSolver.approximateStructuralBoundsUsingInvariants(spn, invar, toCheck, maxStruct);

int d=0;
for (int pid=spn.getPlaceCount()-1 ; pid >= 0 ; pid--) {
if (maxStruct.get(pid) == 1) {
doneProps.put("place_"+pid, true, "STRUCTURAL INVARIANTS");
maxStruct.remove(pid);
maxSeen.remove(pid);
toCheck.remove(pid);
d++;
}
}
Logger.getLogger("fr.lip6.move.gal").info("Rough structural analysis with invriants proved " + d + " places are one safe in " + (System.currentTimeMillis() - time) + " ms.");

DeadlockTester.testOneSafeWithSMT(toCheck, spn, invar, doneProps, solverPath, isSafe, 10);

spn.getProperties().removeIf(p->doneProps.containsKey(p.getName()));
}

// vire les prop triviales, utile ?
if (!spn.getProperties().isEmpty()) {
try {
Expand All @@ -170,21 +222,21 @@ public boolean solveProperty(String examination, MccTranslator reader) {
}
}

spn.getProperties().removeIf(p -> ! doneProps.containsKey(p.getName()));
spn.getProperties().removeIf(p -> doneProps.containsKey(p.getName()));

if (!spn.getProperties().isEmpty()) {
System.out.println("Unable to solve all queries for examination "+examination + ". Remains :"+ spn.getProperties().size() + " assertions to prove.");
return false;
} else {
System.out.println("Able to resolve query "+examination+ " after proving " + doneProps.size() + " properties.");
}
boolean success = isSuccess(doneProps, examination);
if (success)
System.out.println("FORMULA " + examination + " TRUE TECHNIQUES " + doneProps.computeTechniques());
else
System.out.println("FORMULA " + examination + " FALSE TECHNIQUES " + doneProps.computeTechniques());
boolean success = isSuccess(doneProps, examination);
if (success)
System.out.println("FORMULA " + examination + " TRUE TECHNIQUES " + doneProps.computeTechniques());
else
System.out.println("FORMULA " + examination + " FALSE TECHNIQUES " + doneProps.computeTechniques());

return true;
return true;
}
}

private void buildProperties(String examination, PetriNet spn) {
Expand Down
72 changes: 50 additions & 22 deletions ...r.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/LTLPropertySolver.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,7 @@
import java.util.Set;
import java.util.concurrent.TimeoutException;

import android.util.SparseIntArray;
import fr.lip6.ltl.tgba.AcceptedRunFoundException;
import fr.lip6.ltl.tgba.EmptyProductException;
import fr.lip6.ltl.tgba.LTLException;
Expand All @@ -19,6 +20,7 @@
import fr.lip6.move.gal.structural.SparsePetriNet;
import fr.lip6.move.gal.structural.StructuralReduction;
import fr.lip6.move.gal.structural.StructuralReduction.ReductionType;
import fr.lip6.move.gal.structural.expr.AtomicProp;
import fr.lip6.move.gal.structural.expr.Expression;
import fr.lip6.move.gal.structural.expr.Op;
import fr.lip6.move.gal.structural.smt.DeadlockTester;
Expand Down Expand Up @@ -174,48 +176,74 @@ public void runStutteringLTLTest(MccTranslator reader, DoneProperties doneProps,
private TGBA applyKnowledgeBasedReductions(ISparsePetriNet spn, TGBA tgba, boolean isSafe) {

// cheap knowledge
List<Expression> knowledge = new ArrayList<>();

addConvergenceKnowledge(knowledge, spn, tgba, isSafe);

addInitialStateKnowledge(knowledge, spn, tgba);

System.out.println("Knowledge obtained : " + knowledge);

// try to reduce the tgba using this knowledge
SpotRunner sr = new SpotRunner(spotPath, workDir, 10);


for (Expression factoid : knowledge) {
String ltl = sr.printLTLProperty(factoid);
TGBA prod = sr.computeProduct(tgba, ltl);
if (prod.getEdges().get(prod.getInitial()).size() == 0) {
// this is just false !
System.out.println("Property proved to be true thanks to knowledge :" + factoid);
return prod;
} else if (prod.getProperties().contains("stutter-invariant") && ! tgba.getProperties().contains("stutter-invariant")) {
System.out.println("Adopting stutter invariant property thanks to knowledge :" + factoid);
tgba = prod;
} else if (prod.getAPs().size() < tgba.getAPs().size()) {
System.out.println("Adopting property with smaller alphabet thanks to knowledge :" + factoid);
tgba = prod;
}
}

return tgba;

}

private void addInitialStateKnowledge(List<Expression> knowledge, ISparsePetriNet spn, TGBA tgba) {
SparseIntArray init = new SparseIntArray(spn.getMarks());
for (AtomicProp ap : tgba.getAPs()) {
if (ap.getExpression().eval(init) == 1) {
knowledge.add(Expression.apRef(ap));
} else {
knowledge.add(Expression.not(Expression.apRef(ap)));
}
}
}

private void addConvergenceKnowledge(List<Expression> knowledge, ISparsePetriNet spn, TGBA tgba, boolean isSafe) {
// we are SCC free hence structurally we will meet a deadlock in all traces
// hence we must be accepted in one of these states, and they are by definition stuttering
boolean allPathsAreDead = testAFDead (spn);

if (allPathsAreDead) {
System.out.println("Detected that all paths lead to deadlock. Applying this knowledge to assert that all AP eventually converge : F ( (Ga|G!a) & (Gb|G!b)...)");

boolean [] results = DeadlockTester.testAPInDeadlocksWithSMT(spn, tgba.getAPs(), solverPath, isSafe);

List<Expression> knowledge = new ArrayList<>();
boolean [] results = DeadlockTester.testAPInDeadlocksWithSMT(spn, tgba.getAPs(), solverPath, isSafe);

// build expressions : G p | G !p
// for each ap "p", but remove bad values eliminated through SMT
for (int i=0,ie=tgba.getAPs().size() ; i < ie ; i++) {
boolean posExist = results[i];
boolean negExist = results[i+1];
knowledge.add(Expression.op(Op.OR,
knowledge.add(
Expression.op(Op.F,
Expression.op(Op.OR,
posExist ? Expression.op(Op.G, Expression.apRef(tgba.getAPs().get(i)), null): Expression.constant(false),
negExist ? Expression.op(Op.G, Expression.not(Expression.apRef(tgba.getAPs().get(i))),null): Expression.constant(false)));
negExist ? Expression.op(Op.G, Expression.not(Expression.apRef(tgba.getAPs().get(i))),null): Expression.constant(false)),null));
if (!posExist && ! negExist) {
System.out.println("Strange error detected, AP can be neither true nor false in deadlock.");
}
}

System.out.println("Knowledge obtained : " + knowledge);


// try to reduce the tgba using this knowledge
SpotRunner sr = new SpotRunner(spotPath, workDir, 10);

for (Expression factoid : knowledge) {
String ltl = sr.printLTLProperty(factoid);
TGBA prod = sr.computeProduct(tgba, ltl);
if (prod.getEdges().get(prod.getInitial()).size() == 0) {
// this is just false !
return prod;
}
}
}
return tgba;

}

private boolean testAFDead(ISparsePetriNet spn) {
Expand Down
Loading

0 comments on commit 52bb31e

Please sign in to comment.