From 568ba29ecd08e831a752864b4936d21f835214d4 Mon Sep 17 00:00:00 2001 From: Yann Thierry-Mieg Date: Wed, 24 Mar 2021 11:42:24 +0100 Subject: [PATCH 01/13] patch missing future operator in Knowledge exploitation --- .../src/fr/lip6/move/gal/application/LTLPropertySolver.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/LTLPropertySolver.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/LTLPropertySolver.java index 0946532eee..fe09fec2e2 100644 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/LTLPropertySolver.java +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/LTLPropertySolver.java @@ -206,7 +206,7 @@ private TGBA applyKnowledgeBasedReductions(ISparsePetriNet spn, TGBA tgba, boole SpotRunner sr = new SpotRunner(spotPath, workDir, 10); for (Expression factoid : knowledge) { - String ltl = sr.printLTLProperty(factoid); + String ltl = "F(" + sr.printLTLProperty(factoid) + ")"; TGBA prod = sr.computeProduct(tgba, ltl); if (prod.getEdges().get(prod.getInitial()).size() == 0) { // this is just false ! From 4f21f5655e3ad4606d9a586f51dbd73ea5bec24f Mon Sep 17 00:00:00 2001 From: Yann Thierry-Mieg Date: Wed, 24 Mar 2021 11:49:37 +0100 Subject: [PATCH 02/13] reduce trace verbosity (properties encountered -> sparse output) --- .../src/android/util/SparseIntArray.java | 12 ++++++++++- .../move/gal/structural/RandomExplorer.java | 20 +++++++++---------- 2 files changed, 21 insertions(+), 11 deletions(-) diff --git a/fr.lip6.move.gal.structural/src/android/util/SparseIntArray.java b/fr.lip6.move.gal.structural/src/android/util/SparseIntArray.java index 0186f25ae3..d16941e301 100644 --- a/fr.lip6.move.gal.structural/src/android/util/SparseIntArray.java +++ b/fr.lip6.move.gal.structural/src/android/util/SparseIntArray.java @@ -85,7 +85,17 @@ public SparseIntArray(List marks) { } } - public List 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 toList (int size) { List res = new ArrayList (size); int j = 0; for (int i=0; i < size ; i++ ) { diff --git a/fr.lip6.move.gal.structural/src/fr/lip6/move/gal/structural/RandomExplorer.java b/fr.lip6.move.gal.structural/src/fr/lip6/move/gal/structural/RandomExplorer.java index 2eb2a25782..59ae92ab1c 100644 --- a/fr.lip6.move.gal.structural/src/fr/lip6/move/gal/structural/RandomExplorer.java +++ b/fr.lip6.move.gal.structural/src/fr/lip6/move/gal/structural/RandomExplorer.java @@ -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) { @@ -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; } @@ -160,7 +160,7 @@ public int[] runProbabilisticReachabilityDetection (long nbSteps, List 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; } @@ -225,20 +225,20 @@ public int[] runProbabilisticReachabilityDetection (long nbSteps, List 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) { @@ -347,7 +347,7 @@ public int[] runRandomReachabilityDetection (long nbSteps, List 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; } From 6bf51d9ff6b65aa9bb00f9dca6bdcd38b821c27b Mon Sep 17 00:00:00 2001 From: Yann Thierry-Mieg Date: Wed, 24 Mar 2021 14:52:31 +0100 Subject: [PATCH 03/13] refactor code for reuse in OneSafe code --- .../gal/application/UpperBoundsSolver.java | 32 +++++++++---------- 1 file changed, 15 insertions(+), 17 deletions(-) diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/UpperBoundsSolver.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/UpperBoundsSolver.java index da1d8db224..ed04a33a72 100644 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/UpperBoundsSolver.java +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/UpperBoundsSolver.java @@ -10,6 +10,7 @@ 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.ISparsePetriNet; import fr.lip6.move.gal.structural.InvariantCalculator; import fr.lip6.move.gal.structural.NoDeadlockExists; import fr.lip6.move.gal.structural.PropertyType; @@ -24,11 +25,11 @@ public class UpperBoundsSolver { - public static void checkInInitial(MccTranslator reader, DoneProperties doneProps) { - for (fr.lip6.move.gal.structural.Property prop : new ArrayList<>(reader.getSPN().getProperties())) { + public static void checkInInitial(SparsePetriNet spn, DoneProperties doneProps) { + for (fr.lip6.move.gal.structural.Property prop : new ArrayList<>(spn.getProperties())) { if (prop.getBody().getOp() == Op.CONST) { doneProps.put(prop.getName(),prop.getBody().getValue(),"TOPOLOGICAL INITIAL_STATE"); - reader.getSPN().getProperties().remove(prop); + spn.getProperties().remove(prop); } } } @@ -98,12 +99,10 @@ private static void checkStatus(SparsePetriNet spn, List tocheck, Li } - public static void applyReductions(MccTranslator reader, DoneProperties doneProps, String solverPath, boolean isSafe, List initMaxStruct) { + public static void applyReductions(SparsePetriNet spn, DoneProperties doneProps, String solverPath, boolean isSafe, List initMaxStruct) { int iter; int iterations =0; - SparsePetriNet spn = reader.getSPN(); - // need to protect some variables List tocheckIndexes = new ArrayList<>(); List tocheck = new ArrayList<>(spn.getProperties().size()); @@ -137,7 +136,6 @@ public static void applyReductions(MccTranslator reader, DoneProperties doneProp do { iter =0; if (! first) { - spn = reader.getSPN(); tocheck = new ArrayList<>(spn.getProperties().size()); computeToCheck(spn, tocheckIndexes, tocheck, doneProps); } else { @@ -161,7 +159,7 @@ public static void applyReductions(MccTranslator reader, DoneProperties doneProp checkStatus(spn, tocheck, maxStruct, maxSeen, doneProps, "TOPOLOGICAL RANDOM_WALK"); - if (reader.getSPN().getProperties().isEmpty()) + if (spn.getProperties().isEmpty()) break; if (solverPath != null) { @@ -171,7 +169,7 @@ public static void applyReductions(MccTranslator reader, DoneProperties doneProp //interpretVerdict(tocheck, spn, doneProps, new int[tocheck.size()], solverPath, maxSeen, maxStruct); System.out.println("Current structural bounds on expressions (after SMT) : " + maxStruct+ " Max seen :" + maxSeen); - iter += treatVerdicts(reader.getSPN(), doneProps, tocheck, tocheckIndexes, paths, maxSeen, maxStruct); + iter += treatVerdicts(spn, doneProps, tocheck, tocheckIndexes, paths, maxSeen, maxStruct); for (int v = paths.size()-1 ; v >= 0 ; v--) { @@ -250,9 +248,9 @@ public static void applyReductions(MccTranslator reader, DoneProperties doneProp sr.dropTransitions(tfeed , true,"Remove Feeders"); } - if (applyReductions(sr, reader, ReductionType.SAFETY, solverPath, isSafe,false,iterations==0)) { + if (applyReductions(sr, ReductionType.SAFETY, solverPath, isSafe,false,iterations==0)) { iter++; - } else if (iterations>0 && iter==0 /*&& doneSums*/ && applyReductions(sr, reader, ReductionType.SAFETY, solverPath, isSafe,true,false)) { + } else if (iterations>0 && iter==0 /*&& doneSums*/ && applyReductions(sr, ReductionType.SAFETY, solverPath, isSafe,true,false)) { iter++; } int reds= sr.ruleRedundantCompositionsBounds(); @@ -265,22 +263,22 @@ public static void applyReductions(MccTranslator reader, DoneProperties doneProp spn.testInInitial(); spn.removeConstantPlaces(); spn.simplifyLogic(); - checkInInitial(reader, doneProps); + checkInInitial(spn, doneProps); - if (reader.getSPN().getProperties().isEmpty()) { + if (spn.getProperties().isEmpty()) { return; } - if (reader.getSPN().getProperties().removeIf(p -> doneProps.containsKey(p.getName()))) + if (spn.getProperties().removeIf(p -> doneProps.containsKey(p.getName()))) iter++; iterations++; - } while ( (iterations<=1 || iter > 0 || !lastMaxSeen.equals(maxSeen)) && ! reader.getSPN().getProperties().isEmpty()); + } while ( (iterations<=1 || iter > 0 || !lastMaxSeen.equals(maxSeen)) && ! spn.getProperties().isEmpty()); } - private static void approximateStructuralBoundsUsingInvariants(StructuralReduction sr, List tocheck, + public static void approximateStructuralBoundsUsingInvariants(ISparsePetriNet sr, List tocheck, List maxStruct) { { // try to set a max bound on variables using invariants @@ -527,7 +525,7 @@ static int randomCheckReachability(RandomExplorer re, List tocheck, - static boolean applyReductions(StructuralReduction sr, MccTranslator reader, ReductionType rt, String solverPath, boolean isSafe, boolean withSMT, boolean isFirstTime) + static boolean applyReductions(StructuralReduction sr, ReductionType rt, String solverPath, boolean isSafe, boolean withSMT, boolean isFirstTime) { try { boolean cont = false; From 6563e4bdb4d8371dbf9d833487cc7a0d503c39f3 Mon Sep 17 00:00:00 2001 From: Yann Thierry-Mieg Date: Wed, 24 Mar 2021 14:53:27 +0100 Subject: [PATCH 04/13] new strategy for OneSafe : use SMT solver more intelligently instead of one run of the solver per place, one run for all of them. --- .../gal/application/GlobalPropertySolver.java | 32 ++++++++++++++++++- 1 file changed, 31 insertions(+), 1 deletion(-) diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/GlobalPropertySolver.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/GlobalPropertySolver.java index b832535c99..99a4ef692b 100644 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/GlobalPropertySolver.java +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/GlobalPropertySolver.java @@ -1,8 +1,11 @@ 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.Map.Entry; +import java.util.stream.Collectors; import fr.lip6.move.gal.mcc.properties.DoneProperties; import fr.lip6.move.gal.structural.DeadlockFound; @@ -15,6 +18,7 @@ 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; public class GlobalPropertySolver { @@ -156,7 +160,33 @@ public boolean solveProperty(String examination, MccTranslator reader) { if (isSafe) { spn.assumeOneSafe(); } - + + if (ONE_SAFE.equals(examination)) { + List toCheck = new ArrayList<>(spn.getPlaceCount()); + List maxStruct = new ArrayList<>(spn.getPlaceCount()); + List 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); + } + UpperBoundsSolver.approximateStructuralBoundsUsingInvariants(spn, toCheck, maxStruct); + + 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); + } + } + List toCheckID = toCheck.stream().map(e->e.getValue()).collect(Collectors.toList()); + + DeadlockTester.testOneSafeWithSMT(toCheck, spn, doneProps, solverPath, isSafe, 10); + + spn.getProperties().removeIf(p->doneProps.containsKey(p.getName())); + } + // vire les prop triviales, utile ? if (!spn.getProperties().isEmpty()) { try { From c2f0c0f8def2259088df4b26ab4073b1b4a977ea Mon Sep 17 00:00:00 2001 From: Yann Thierry-Mieg Date: Wed, 24 Mar 2021 14:54:00 +0100 Subject: [PATCH 05/13] new API dedicated to OneSafe scenario --- .../gal/structural/smt/DeadlockTester.java | 101 +++++++++++++++++- 1 file changed, 100 insertions(+), 1 deletion(-) diff --git a/smt/fr.lip6.move.gal.gal2smt/src/fr/lip6/move/gal/structural/smt/DeadlockTester.java b/smt/fr.lip6.move.gal.gal2smt/src/fr/lip6/move/gal/structural/smt/DeadlockTester.java index 1e2b5ab28f..7076b79796 100644 --- a/smt/fr.lip6.move.gal.gal2smt/src/fr/lip6/move/gal/structural/smt/DeadlockTester.java +++ b/smt/fr.lip6.move.gal.gal2smt/src/fr/lip6/move/gal/structural/smt/DeadlockTester.java @@ -16,6 +16,7 @@ import org.smtlib.IExpr; import org.smtlib.IExpr.IDeclaration; import org.smtlib.IExpr.IFactory; +import org.smtlib.IExpr.IFcnExpr; import org.smtlib.IResponse; import org.smtlib.ISolver; import org.smtlib.ISort; @@ -33,6 +34,7 @@ import org.smtlib.sexpr.ISexpr.ISeq; import android.util.SparseIntArray; +import fr.lip6.move.gal.mcc.properties.DoneProperties; import fr.lip6.move.gal.structural.ISparsePetriNet; import fr.lip6.move.gal.structural.InvariantCalculator; import fr.lip6.move.gal.structural.StructuralReduction; @@ -1764,9 +1766,106 @@ private static void addInvariant(ISparsePetriNet sr, IFactory efactory, Script s IExpr invarexpr = efactory.fcn(efactory.symbol("="), sumR, sumE); script.add(new C_assert(invarexpr)); } + + public static void testOneSafeWithSMT(List toCheck, ISparsePetriNet sr, DoneProperties doneProps, String solverPath, boolean isSafe, int timeout) { + + List verdicts = new ArrayList<>(); + + List tnames = new ArrayList<>(); + List representative = new ArrayList<>(); + IntMatrixCol sumMatrix = computeReducedFlow(sr, tnames, representative); + Set invar = InvariantCalculator.computePInvariants(sumMatrix, sr.getPnames()); + + boolean solveWithReals = true; + int timeoutQ = 100; + int timeoutT = 100; + + org.smtlib.SMT smt = new SMT(); + IFactory ef = smt.smtConfig.exprFactory; + ISolver solver = initSolver(solverPath, smt,solveWithReals,timeoutQ,timeoutT); + { + // STEP 1 : declare variables, assert net is dead. + long time = System.currentTimeMillis(); + Script varScript = declareVariables(sr.getPnames().size(), "s", isSafe, smt,solveWithReals); + execAndCheckResult(varScript, solver); + String textReply = checkSat(solver); + // are we finished ? + if (textReply.equals("unsat")||textReply.equals("unknown")) { + solver.exit(); + return ; + } + } + + // STEP 2 : declare and assert invariants + long time = System.currentTimeMillis(); + Script invpos = new Script(); + Script invneg = new Script(); + int poscount = declareInvariants(invar,sr,invpos,invneg,smt); + + String textReply = "sat"; + // add the positive only for now + if (!invpos.commands().isEmpty()) { + execAndCheckResult(invpos, solver); + textReply = checkSat(solver, false); + Logger.getLogger("fr.lip6.move.gal").info((solveWithReals ? "[Real]":"[Nat]")+ "Absence check using "+poscount+" positive place invariants in "+ (System.currentTimeMillis()-time) +" ms returned " + textReply); + } + + clearDone(toCheck, doneProps , ef, solver); + if (toCheck.isEmpty()) { + solver.exit(); + return; + } + + + if (textReply.equals("sat") && ! invneg.commands().isEmpty()) { + time = System.currentTimeMillis(); + execAndCheckResult(invneg, solver); + textReply = checkSat(solver, true); + Logger.getLogger("fr.lip6.move.gal").info((solveWithReals ? "[Real]":"[Nat]")+"Absence check using "+poscount+" positive and " + (invar.size() - poscount) +" generalized place invariants in "+ (System.currentTimeMillis()-time) +" ms returned " + textReply); + } + + clearDone(toCheck, doneProps , ef, solver); + + if (toCheck.isEmpty()) { + solver.exit(); + return; + } + + + // STEP 3 : go heavy, use the state equation to refine our solution + time = System.currentTimeMillis(); + Logger.getLogger("fr.lip6.move.gal").info((solveWithReals ? "[Real]":"[Nat]")+"Adding state equation constraints to refine reachable states."); + Script script = declareStateEquation(sumMatrix, sr, smt,solveWithReals, representative, null); + + execAndCheckResult(script, solver); + + clearDone(toCheck, doneProps , ef, solver); + solver.exit(); + return; + } + + + private static void clearDone(List toCheck, DoneProperties doneProps, IFactory ef, ISolver solver) { + for (int i=toCheck.size()-1; i >= 0 ; i-- ) { + int pid = toCheck.get(i).getValue(); + + solver.push(1); + + IFcnExpr test = ef.fcn(ef.symbol(">"), ef.symbol("s"+pid), ef.numeral(1)); + solver.assertExpr(test); + + String res = checkSat(solver); + + if ("unsat".equals(res)) { + toCheck.remove(i); + doneProps.put("place_"+pid, true, "SAT_SMT STRUCTURAL"); + } + solver.pop(1); + } + } public static List findStructuralMaxWithSMT(List tocheck, List maxSeen, - List maxStruct, StructuralReduction sr, String solverPath, boolean isSafe, List representative, + List maxStruct, ISparsePetriNet sr, String solverPath, boolean isSafe, List representative, int timeout, boolean withWitness) { List verdicts = new ArrayList<>(); From eb3c73e77736c8fd5c4dd4f4e1c10384db4fb01b Mon Sep 17 00:00:00 2001 From: Yann Thierry-Mieg Date: Wed, 24 Mar 2021 14:54:34 +0100 Subject: [PATCH 06/13] small refactoring after API changes (pass spn instead of reader) --- .../src/fr/lip6/move/gal/application/Application.java | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/Application.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/Application.java index 179d42cb44..68e2a03d49 100644 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/Application.java +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/Application.java @@ -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); @@ -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."); } From 10a9fe1daf5b8c150faf9fd38e18a3ff7ca047c6 Mon Sep 17 00:00:00 2001 From: Yann Thierry-Mieg Date: Wed, 24 Mar 2021 14:58:33 +0100 Subject: [PATCH 07/13] useless variable --- .../src/fr/lip6/move/gal/application/GlobalPropertySolver.java | 2 -- 1 file changed, 2 deletions(-) diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/GlobalPropertySolver.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/GlobalPropertySolver.java index 99a4ef692b..88b2c23585 100644 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/GlobalPropertySolver.java +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/GlobalPropertySolver.java @@ -180,8 +180,6 @@ public boolean solveProperty(String examination, MccTranslator reader) { toCheck.remove(pid); } } - List toCheckID = toCheck.stream().map(e->e.getValue()).collect(Collectors.toList()); - DeadlockTester.testOneSafeWithSMT(toCheck, spn, doneProps, solverPath, isSafe, 10); spn.getProperties().removeIf(p->doneProps.containsKey(p.getName())); From 7184c95cd8bd150aedfb06c13133511444d48562 Mon Sep 17 00:00:00 2001 From: Yann Thierry-Mieg Date: Wed, 24 Mar 2021 16:18:33 +0100 Subject: [PATCH 08/13] efficiency : avoid recomputing invariants, nicer traces --- .../move/gal/structural/SparsePetriNet.java | 3 +- .../gal/application/GlobalPropertySolver.java | 31 ++++++++++++++++--- .../gal/application/UpperBoundsSolver.java | 28 ++++++++++------- .../gal/structural/smt/DeadlockTester.java | 25 +++++++++------ 4 files changed, 60 insertions(+), 27 deletions(-) diff --git a/fr.lip6.move.gal.structural/src/fr/lip6/move/gal/structural/SparsePetriNet.java b/fr.lip6.move.gal.structural/src/fr/lip6/move/gal/structural/SparsePetriNet.java index 2fc72e74f9..c8b8762c36 100644 --- a/fr.lip6.move.gal.structural/src/fr/lip6/move/gal/structural/SparsePetriNet.java +++ b/fr.lip6.move.gal.structural/src/fr/lip6/move/gal/structural/SparsePetriNet.java @@ -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()) { @@ -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) { diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/GlobalPropertySolver.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/GlobalPropertySolver.java index 88b2c23585..cea63821e5 100644 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/GlobalPropertySolver.java +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/GlobalPropertySolver.java @@ -4,12 +4,15 @@ 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 java.util.stream.Collectors; +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; @@ -19,6 +22,7 @@ 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 { @@ -152,7 +156,9 @@ public boolean solveProperty(String examination, MccTranslator reader) { spn.simplifyLogic(); spn.toPredicates(); - spn.testInInitial(); + if (spn.testInInitial() > 0) { + ReachabilitySolver.checkInInitial(spn, doneProps); + } spn.removeConstantPlaces(); spn.removeRedundantTransitions(false); spn.removeConstantPlaces(); @@ -160,6 +166,8 @@ public boolean solveProperty(String examination, MccTranslator reader) { if (isSafe) { spn.assumeOneSafe(); } + ReachabilitySolver.checkInInitial(spn, doneProps); + if (ONE_SAFE.equals(examination)) { List toCheck = new ArrayList<>(spn.getPlaceCount()); @@ -170,17 +178,30 @@ public boolean solveProperty(String examination, MccTranslator reader) { maxStruct.add(-1); maxSeen.add(1); } - UpperBoundsSolver.approximateStructuralBoundsUsingInvariants(spn, toCheck, maxStruct); + // the invariants themselves + Set 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++; } - } - DeadlockTester.testOneSafeWithSMT(toCheck, spn, doneProps, solverPath, isSafe, 10); + } + 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())); } diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/UpperBoundsSolver.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/UpperBoundsSolver.java index ed04a33a72..d227a1c231 100644 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/UpperBoundsSolver.java +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/UpperBoundsSolver.java @@ -59,8 +59,14 @@ public static List treatSkeleton(MccTranslator reader, DoneProperties d } } - StructuralReduction sr = new StructuralReduction(spn); - approximateStructuralBoundsUsingInvariants(sr, tocheck, maxStruct); + StructuralReduction sr = new StructuralReduction(spn); + Set invar; + { + // effect matrix + IntMatrixCol sumMatrix = IntMatrixCol.sumProd(-1, spn.getFlowPT(), 1, spn.getFlowTP()); + invar = InvariantCalculator.computePInvariants(sumMatrix, spn.getPnames()); + } + approximateStructuralBoundsUsingInvariants(sr, invar, tocheck, maxStruct); checkStatus(spn, tocheck, maxStruct, maxSeen, doneProps, "TOPOLOGICAL CPN_APPROX INITIAL_STATE"); @@ -143,8 +149,14 @@ public static void applyReductions(SparsePetriNet spn, DoneProperties doneProps, } StructuralReduction sr = new StructuralReduction(spn); - - approximateStructuralBoundsUsingInvariants(sr, tocheck, maxStruct); + // the invariants themselves + Set invar ; + { + // effect matrix + IntMatrixCol sumMatrix = IntMatrixCol.sumProd(-1, spn.getFlowPT(), 1, spn.getFlowTP()); + invar = InvariantCalculator.computePInvariants(sumMatrix, spn.getPnames()); + } + approximateStructuralBoundsUsingInvariants(sr, invar, tocheck, maxStruct); checkStatus(spn, tocheck, maxStruct, maxSeen, doneProps, "TOPOLOGICAL INITIAL_STATE"); @@ -278,17 +290,11 @@ public static void applyReductions(SparsePetriNet spn, DoneProperties doneProps, } - public static void approximateStructuralBoundsUsingInvariants(ISparsePetriNet sr, List tocheck, + public static void approximateStructuralBoundsUsingInvariants(ISparsePetriNet sr, Set invar, List tocheck, List maxStruct) { { // try to set a max bound on variables using invariants - // effect matrix - IntMatrixCol sumMatrix = IntMatrixCol.sumProd(-1, sr.getFlowPT(), 1, sr.getFlowTP()); - // the invariants themselves - Set invar = InvariantCalculator.computePInvariants(sumMatrix, sr.getPnames()); - - // structural bounds determined on all variables/places int [] limits = new int [sr.getPnames().size()]; // -1 = no structural bound found diff --git a/smt/fr.lip6.move.gal.gal2smt/src/fr/lip6/move/gal/structural/smt/DeadlockTester.java b/smt/fr.lip6.move.gal.gal2smt/src/fr/lip6/move/gal/structural/smt/DeadlockTester.java index 7076b79796..0be94b09c8 100644 --- a/smt/fr.lip6.move.gal.gal2smt/src/fr/lip6/move/gal/structural/smt/DeadlockTester.java +++ b/smt/fr.lip6.move.gal.gal2smt/src/fr/lip6/move/gal/structural/smt/DeadlockTester.java @@ -1767,14 +1767,12 @@ private static void addInvariant(ISparsePetriNet sr, IFactory efactory, Script s script.add(new C_assert(invarexpr)); } - public static void testOneSafeWithSMT(List toCheck, ISparsePetriNet sr, DoneProperties doneProps, String solverPath, boolean isSafe, int timeout) { + public static void testOneSafeWithSMT(List toCheck, ISparsePetriNet sr, Set invar, DoneProperties doneProps, String solverPath, boolean isSafe, int timeout) { List verdicts = new ArrayList<>(); List tnames = new ArrayList<>(); List representative = new ArrayList<>(); - IntMatrixCol sumMatrix = computeReducedFlow(sr, tnames, representative); - Set invar = InvariantCalculator.computePInvariants(sumMatrix, sr.getPnames()); boolean solveWithReals = true; int timeoutQ = 100; @@ -1807,10 +1805,11 @@ public static void testOneSafeWithSMT(List toCheck, ISparsePetriNet if (!invpos.commands().isEmpty()) { execAndCheckResult(invpos, solver); textReply = checkSat(solver, false); - Logger.getLogger("fr.lip6.move.gal").info((solveWithReals ? "[Real]":"[Nat]")+ "Absence check using "+poscount+" positive place invariants in "+ (System.currentTimeMillis()-time) +" ms returned " + textReply); } - clearDone(toCheck, doneProps , ef, solver); + int d = clearDone(toCheck, doneProps , ef, solver); + Logger.getLogger("fr.lip6.move.gal").info((solveWithReals ? "[Real]":"[Nat]")+ "Absence check using "+poscount+" positive place invariants in "+ (System.currentTimeMillis()-time) +" ms proved " + d + " places are One-Safe."); + if (toCheck.isEmpty()) { solver.exit(); return; @@ -1821,10 +1820,11 @@ public static void testOneSafeWithSMT(List toCheck, ISparsePetriNet time = System.currentTimeMillis(); execAndCheckResult(invneg, solver); textReply = checkSat(solver, true); - Logger.getLogger("fr.lip6.move.gal").info((solveWithReals ? "[Real]":"[Nat]")+"Absence check using "+poscount+" positive and " + (invar.size() - poscount) +" generalized place invariants in "+ (System.currentTimeMillis()-time) +" ms returned " + textReply); + } - clearDone(toCheck, doneProps , ef, solver); + d= clearDone(toCheck, doneProps , ef, solver); + Logger.getLogger("fr.lip6.move.gal").info((solveWithReals ? "[Real]":"[Nat]")+"Absence check using "+poscount+" positive and " + (invar.size() - poscount) +" generalized place invariants in "+ (System.currentTimeMillis()-time) +" ms proved " + d + " places are One-Safe."); if (toCheck.isEmpty()) { solver.exit(); @@ -1834,18 +1834,21 @@ public static void testOneSafeWithSMT(List toCheck, ISparsePetriNet // STEP 3 : go heavy, use the state equation to refine our solution time = System.currentTimeMillis(); - Logger.getLogger("fr.lip6.move.gal").info((solveWithReals ? "[Real]":"[Nat]")+"Adding state equation constraints to refine reachable states."); + IntMatrixCol sumMatrix = computeReducedFlow(sr, tnames, representative); Script script = declareStateEquation(sumMatrix, sr, smt,solveWithReals, representative, null); execAndCheckResult(script, solver); - clearDone(toCheck, doneProps , ef, solver); + d=clearDone(toCheck, doneProps , ef, solver); + Logger.getLogger("fr.lip6.move.gal").info((solveWithReals ? "[Real]":"[Nat]")+" State equation constraints in "+ (System.currentTimeMillis()-time) +" ms proved " + d + " places are One-Safe."); + solver.exit(); return; } - private static void clearDone(List toCheck, DoneProperties doneProps, IFactory ef, ISolver solver) { + private static int clearDone(List toCheck, DoneProperties doneProps, IFactory ef, ISolver solver) { + int done = 0; for (int i=toCheck.size()-1; i >= 0 ; i-- ) { int pid = toCheck.get(i).getValue(); @@ -1858,10 +1861,12 @@ private static void clearDone(List toCheck, DoneProperties doneProps if ("unsat".equals(res)) { toCheck.remove(i); + done++; doneProps.put("place_"+pid, true, "SAT_SMT STRUCTURAL"); } solver.pop(1); } + return done; } public static List findStructuralMaxWithSMT(List tocheck, List maxSeen, From 308c64a6812cab286dced3b3fc1e57aa73cf35e6 Mon Sep 17 00:00:00 2001 From: Yann Thierry-Mieg Date: Wed, 24 Mar 2021 16:19:18 +0100 Subject: [PATCH 09/13] now using initial state as knowledge about the system. --- .../gal/application/LTLPropertySolver.java | 68 +++++++++++++------ 1 file changed, 46 insertions(+), 22 deletions(-) diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/LTLPropertySolver.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/LTLPropertySolver.java index fe09fec2e2..c2debc3e95 100644 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/LTLPropertySolver.java +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/LTLPropertySolver.java @@ -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; @@ -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; @@ -174,7 +176,46 @@ public void runStutteringLTLTest(MccTranslator reader, DoneProperties doneProps, private TGBA applyKnowledgeBasedReductions(ISparsePetriNet spn, TGBA tgba, boolean isSafe) { // cheap knowledge + List 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 ! + 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; + } + } + + return tgba; + + } + + private void addInitialStateKnowledge(List 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 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); @@ -182,40 +223,23 @@ private TGBA applyKnowledgeBasedReductions(ISparsePetriNet spn, TGBA tgba, boole 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 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 = "F(" + 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) { From 6e64cc87ada244ca12a437bad79047acf4ed708f Mon Sep 17 00:00:00 2001 From: Yann Thierry-Mieg Date: Wed, 24 Mar 2021 16:45:37 +0100 Subject: [PATCH 10/13] nicer messages, more adoption likelihood --- .../src/fr/lip6/move/gal/application/LTLPropertySolver.java | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/LTLPropertySolver.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/LTLPropertySolver.java index c2debc3e95..a01dbcf8a6 100644 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/LTLPropertySolver.java +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/LTLPropertySolver.java @@ -193,10 +193,14 @@ private TGBA applyKnowledgeBasedReductions(ISparsePetriNet spn, TGBA tgba, boole 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")) { + } 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; } } From bc6909898bb5a21f04e3c21c9b7c3345cc6b4cdc Mon Sep 17 00:00:00 2001 From: Yann Thierry-Mieg Date: Wed, 24 Mar 2021 17:07:05 +0100 Subject: [PATCH 11/13] missing try/catch --- .../gal/application/GlobalPropertySolver.java | 27 ++++++++++--------- 1 file changed, 15 insertions(+), 12 deletions(-) diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/GlobalPropertySolver.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/GlobalPropertySolver.java index cea63821e5..651f5ba073 100644 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/GlobalPropertySolver.java +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/GlobalPropertySolver.java @@ -154,20 +154,23 @@ public boolean solveProperty(String examination, MccTranslator reader) { if (reader.getHLPN() == null) buildProperties(examination, spn); - spn.simplifyLogic(); - spn.toPredicates(); - if (spn.testInInitial() > 0) { + 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; } - spn.removeConstantPlaces(); - spn.removeRedundantTransitions(false); - spn.removeConstantPlaces(); - spn.simplifyLogic(); - if (isSafe) { - spn.assumeOneSafe(); - } - ReachabilitySolver.checkInInitial(spn, doneProps); - if (ONE_SAFE.equals(examination)) { List toCheck = new ArrayList<>(spn.getPlaceCount()); From 54641fe271f427e6b12d5738015b636e2de07242 Mon Sep 17 00:00:00 2001 From: Yann Thierry-Mieg Date: Wed, 24 Mar 2021 17:08:54 +0100 Subject: [PATCH 12/13] approach is only ok for "normal" PT One-Safe definition. NB: most colored models are dealt with immediately anyway with FALSE answer. --- .../src/fr/lip6/move/gal/application/GlobalPropertySolver.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/GlobalPropertySolver.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/GlobalPropertySolver.java index 651f5ba073..e61d80b0c0 100644 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/GlobalPropertySolver.java +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/GlobalPropertySolver.java @@ -172,7 +172,7 @@ public boolean solveProperty(String examination, MccTranslator reader) { return true; } - if (ONE_SAFE.equals(examination)) { + if (ONE_SAFE.equals(examination) && reader.getHLPN() == null) { List toCheck = new ArrayList<>(spn.getPlaceCount()); List maxStruct = new ArrayList<>(spn.getPlaceCount()); List maxSeen = new ArrayList<>(spn.getPlaceCount()); From 26e3bf28ef9c58d2936ef5c34c53e631a0569297 Mon Sep 17 00:00:00 2001 From: Yann Thierry-Mieg Date: Wed, 24 Mar 2021 17:54:22 +0100 Subject: [PATCH 13/13] Bugfix : test logic inverted --- .../gal/application/GlobalPropertySolver.java | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/GlobalPropertySolver.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/GlobalPropertySolver.java index e61d80b0c0..accddb6065 100644 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/GlobalPropertySolver.java +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/GlobalPropertySolver.java @@ -222,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) {