From c7abbbcc0ffa8aa075d45de1ebb106434d56ac3d Mon Sep 17 00:00:00 2001 From: Yann Thierry-Mieg Date: Wed, 24 Feb 2021 13:42:37 +0100 Subject: [PATCH 01/43] refactor : extract some methods to clarify main procedures --- .../gal/application/ReachabilitySolver.java | 168 ++++++++++-------- 1 file changed, 96 insertions(+), 72 deletions(-) diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/ReachabilitySolver.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/ReachabilitySolver.java index cdcfffea56..3a21063e11 100644 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/ReachabilitySolver.java +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/ReachabilitySolver.java @@ -310,89 +310,34 @@ static boolean applyReductions(StructuralReduction sr, MccTranslator reader, Red int reduced = 0; + // The big one ! apply our set of reduction rules, customized by ReductionType, until convergence. reduced += sr.reduce(rt); total+=reduced; cont = false; + + // Quick test for deadlocks, no more transitions. if (rt == ReductionType.DEADLOCKS && sr.getTnames().isEmpty()) { throw new DeadlockFound(); } + // Coming mostly from colored models with an arc + from a colored place + // when the net is color safe (unfolded version is 1 safe) all bindings with + // x=y become unfeasible. Removing them makes the net much simpler, no more arc weights !=1, less transitions... if (isFirstTime && it==0) { - boolean hasGT1ArcValues = false; - for (int t=0,te=sr.getTnames().size() ; t < te && !hasGT1ArcValues; t++) { - SparseIntArray col = sr.getFlowPT().getColumn(t); - for (int i=0,ie=col.size(); i < ie ; i++) { - if (col.valueAt(i)>1) { - hasGT1ArcValues = true; - break; - } - } - } - - if (hasGT1ArcValues) { - List tokill = DeadlockTester.testDeadTransitionWithSMT(sr, solverPath, isSafe); - if (! tokill.isEmpty()) { - System.out.println("Found "+tokill.size()+ " dead transitions using SMT." ); - } - sr.dropTransitions(tokill,"Dead Transitions using SMT only with invariants"); - if (!tokill.isEmpty()) { - System.out.println("Dead transitions reduction (with SMT) triggered by suspicious arc values removed "+tokill.size()+" transitions :"+ tokill); - cont = true; - total++; - } + boolean hasReduced = arcValuesTriggerSMTDeadTransitions(sr, solverPath, isSafe); + if (hasReduced) { + cont=true; + total++; } } + + // implicit and dead transitions test using SMT + // We pass iteration counter and reduced counter to delay more costly versions with state equation. if (withSMT && solverPath != null) { - boolean useStateEq = false; - if (reduced > 0 || it ==0) { - long t = System.currentTimeMillis(); - // go for more reductions ? - - List implicitPlaces = DeadlockTester.testImplicitWithSMT(sr, solverPath, isSafe, false); - if (!implicitPlaces.isEmpty()) { - sr.dropPlaces(implicitPlaces,false,"Implicit Places With SMT (invariants only)"); - sr.ruleReduceTrans(rt); - cont = true; - total++; - } else if (sr.getPnames().size() <= 10000 && sr.getTnames().size() < 10000){ - // limit to 20 k variables for SMT solver with parikh constraints - useStateEq = true; - // with state equation can we solve more ? - implicitPlaces = DeadlockTester.testImplicitWithSMT(sr, solverPath, isSafe, true); - if (!implicitPlaces.isEmpty()) { - sr.dropPlaces(implicitPlaces,false,"Implicit Places With SMT (with state equation)"); - sr.ruleReduceTrans(rt); - reduced += implicitPlaces.size(); - cont = true; - total++; - } - } - System.out.println("Implicit Place search using SMT "+ (useStateEq?"with State Equation":"only with invariants") +" took "+ (System.currentTimeMillis() -t) +" ms to find "+implicitPlaces.size()+ " implicit places."); - } - - if (reduced == 0 || it==0) { - List tokill = DeadlockTester.testImplicitTransitionWithSMT(sr, solverPath); - if (! tokill.isEmpty()) { - System.out.println("Found "+tokill.size()+ " redundant transitions using SMT." ); - } - sr.dropTransitions(tokill,"Redundant Transitions using SMT "+ (useStateEq?"with State Equation":"only with invariants") ); - if (!tokill.isEmpty()) { - System.out.println("Redundant transitions reduction (with SMT) removed "+tokill.size()+" transitions :"+ tokill); - cont = true; - total++; - } - } - if (reduced == 0 || it==0) { - List tokill = DeadlockTester.testDeadTransitionWithSMT(sr, solverPath, isSafe); - if (! tokill.isEmpty()) { - System.out.println("Found "+tokill.size()+ " dead transitions using SMT." ); - } - sr.dropTransitions(tokill,"Dead Transitions using SMT only with invariants"); - if (!tokill.isEmpty()) { - System.out.println("Dead transitions reduction (with SMT) removed "+tokill.size()+" transitions :"+ tokill); - cont = true; - total++; - } + boolean hasReduced = applySMTBasedReductionRules(sr, rt, it, solverPath, isSafe, reduced); + if (hasReduced) { + cont = true; + total++; } } if (!cont && rt == ReductionType.SAFETY && withSMT) { @@ -404,4 +349,83 @@ static boolean applyReductions(StructuralReduction sr, MccTranslator reader, Red return total > 0; } + private static boolean applySMTBasedReductionRules(StructuralReduction sr, ReductionType rt, int iteration, + String solverPath, boolean isSafe, int reduced) throws NoDeadlockExists { + boolean hasReduced = false; + boolean useStateEq = false; + if (reduced > 0 || iteration ==0) { + long t = System.currentTimeMillis(); + // go for more reductions ? + + List implicitPlaces = DeadlockTester.testImplicitWithSMT(sr, solverPath, isSafe, false); + if (!implicitPlaces.isEmpty()) { + sr.dropPlaces(implicitPlaces,false,"Implicit Places With SMT (invariants only)"); + sr.ruleReduceTrans(rt); + hasReduced = true; + } else if (sr.getPnames().size() <= 10000 && sr.getTnames().size() < 10000){ + // limit to 20 k variables for SMT solver with parikh constraints + useStateEq = true; + // with state equation can we solve more ? + implicitPlaces = DeadlockTester.testImplicitWithSMT(sr, solverPath, isSafe, true); + if (!implicitPlaces.isEmpty()) { + sr.dropPlaces(implicitPlaces,false,"Implicit Places With SMT (with state equation)"); + sr.ruleReduceTrans(rt); + reduced += implicitPlaces.size(); + hasReduced = true; + } + } + System.out.println("Implicit Place search using SMT "+ (useStateEq?"with State Equation":"only with invariants") +" took "+ (System.currentTimeMillis() -t) +" ms to find "+implicitPlaces.size()+ " implicit places."); + } + + if (reduced == 0 || iteration==0) { + List tokill = DeadlockTester.testImplicitTransitionWithSMT(sr, solverPath); + if (! tokill.isEmpty()) { + System.out.println("Found "+tokill.size()+ " redundant transitions using SMT." ); + } + sr.dropTransitions(tokill,"Redundant Transitions using SMT "+ (useStateEq?"with State Equation":"only with invariants") ); + if (!tokill.isEmpty()) { + System.out.println("Redundant transitions reduction (with SMT) removed "+tokill.size()+" transitions :"+ tokill); + hasReduced = true; + } + } + if (reduced == 0 || iteration==0) { + List tokill = DeadlockTester.testDeadTransitionWithSMT(sr, solverPath, isSafe); + if (! tokill.isEmpty()) { + System.out.println("Found "+tokill.size()+ " dead transitions using SMT." ); + } + sr.dropTransitions(tokill,"Dead Transitions using SMT only with invariants"); + if (!tokill.isEmpty()) { + System.out.println("Dead transitions reduction (with SMT) removed "+tokill.size()+" transitions :"+ tokill); + hasReduced = true; + } + } + return hasReduced; + } + + private static boolean arcValuesTriggerSMTDeadTransitions(StructuralReduction sr, String solverPath, boolean isSafe) { + boolean hasGT1ArcValues = false; + for (int t=0,te=sr.getTnames().size() ; t < te && !hasGT1ArcValues; t++) { + SparseIntArray col = sr.getFlowPT().getColumn(t); + for (int i=0,ie=col.size(); i < ie ; i++) { + if (col.valueAt(i)>1) { + hasGT1ArcValues = true; + break; + } + } + } + + if (hasGT1ArcValues) { + List tokill = DeadlockTester.testDeadTransitionWithSMT(sr, solverPath, isSafe); + if (! tokill.isEmpty()) { + System.out.println("Found "+tokill.size()+ " dead transitions using SMT." ); + } + sr.dropTransitions(tokill,"Dead Transitions using SMT only with invariants"); + if (!tokill.isEmpty()) { + System.out.println("Dead transitions reduction (with SMT) triggered by suspicious arc values removed "+tokill.size()+" transitions :"+ tokill); + return true; + } + } + return false; + } + } From c01853d64b1b8cd8e14a256774af680596540061 Mon Sep 17 00:00:00 2001 From: Yann Thierry-Mieg Date: Wed, 24 Feb 2021 13:43:14 +0100 Subject: [PATCH 02/43] extract method to deal with Bliss experimental test --- .../move/gal/application/Application.java | 84 +++++++++++-------- 1 file changed, 48 insertions(+), 36 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 2b809884f5..1956f47c50 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 @@ -437,42 +437,9 @@ public Object startNoEx(IApplicationContext context) throws Exception { if (blisspath != null) { - List>> generators = null; - BlissRunner br = new BlissRunner(blisspath,pwd,100); - generators = br.run(sr); - System.out.println("Obtained generators : " + generators); - List>> gen = br.computeMatrixForm(generators); - if (! gen.isEmpty()) { - StructuralReduction sr2 = sr.clone(); - // attempt fusion - - for (Set> set : gen) { - if (set.size() >= 2) { - Iterator> ite = set.iterator(); - List base = ite.next(); - while (ite.hasNext()) { - sr2.fusePlaces(base,ite.next()); - } - } - } - boolean conti = true; - try { sr2.reduce(ReductionType.DEADLOCKS) ; } - catch (DeadlockFound df) { - conti = false; - } - catch (NoDeadlockExists ne) { - System.out.println( "FORMULA " + reader.getSpec().getProperties().get(0).getName() + " FALSE TECHNIQUES TOPOLOGICAL SAT_SMT STRUCTURAL_REDUCTION SYMMETRIES"); - return null; - } - if (conti) { - List repr = new ArrayList<>(); - SparseIntArray parikh = DeadlockTester.testDeadlocksWithSMT(sr2,solverPath, isSafe,repr); - if (parikh == null) { - System.out.println( "FORMULA " + reader.getSpec().getProperties().get(0).getName() + " FALSE TECHNIQUES TOPOLOGICAL SAT_SMT STRUCTURAL_REDUCTION SYMMETRIES"); - return null; - } - } - System.out.println("Symmetry overapproximation was not able to conclude."); + boolean hasConcluded = runBlissSymmetryAnalysis(reader, sr, isSafe, blisspath, pwd, solverPath); + if (hasConcluded) { + return null; } } @@ -725,6 +692,51 @@ public Object startNoEx(IApplicationContext context) throws Exception { return IApplication.EXIT_OK; } + private boolean runBlissSymmetryAnalysis(MccTranslator reader, StructuralReduction sr, boolean isSafe, + String blisspath, String pwd, String solverPath) throws TimeoutException { + boolean hasConcluded = false; + List>> generators = null; + BlissRunner br = new BlissRunner(blisspath,pwd,100); + generators = br.run(sr); + System.out.println("Obtained generators : " + generators); + List>> gen = br.computeMatrixForm(generators); + if (! gen.isEmpty()) { + StructuralReduction sr2 = sr.clone(); + // attempt fusion + + for (Set> set : gen) { + if (set.size() >= 2) { + Iterator> ite = set.iterator(); + List base = ite.next(); + while (ite.hasNext()) { + sr2.fusePlaces(base,ite.next()); + } + } + } + boolean conti = true; + try { sr2.reduce(ReductionType.DEADLOCKS) ; } + catch (DeadlockFound df) { + conti = false; + } + catch (NoDeadlockExists ne) { + System.out.println( "FORMULA " + reader.getSpec().getProperties().get(0).getName() + " FALSE TECHNIQUES TOPOLOGICAL SAT_SMT STRUCTURAL_REDUCTION SYMMETRIES"); + hasConcluded=true; + conti = false; + } + if (conti) { + List repr = new ArrayList<>(); + SparseIntArray parikh = DeadlockTester.testDeadlocksWithSMT(sr2,solverPath, isSafe,repr); + if (parikh == null) { + System.out.println( "FORMULA " + reader.getSpec().getProperties().get(0).getName() + " FALSE TECHNIQUES TOPOLOGICAL SAT_SMT STRUCTURAL_REDUCTION SYMMETRIES"); + hasConcluded = true; + } + } + if (!hasConcluded) + System.out.println("Symmetry overapproximation was not able to conclude."); + } + return hasConcluded; + } + private void tryRebuildPNML(String pwd, String examination, boolean rebuildPNML, MccTranslator reader, Map doneProps) throws IOException { if (rebuildPNML) { From b7ac73b6ffa6ada61f2bb8cb9d9d9f2f674c06b8 Mon Sep 17 00:00:00 2001 From: Yann Thierry-Mieg Date: Wed, 24 Feb 2021 15:11:07 +0100 Subject: [PATCH 03/43] Use DoneProperties instead of Map This object may now serve as an observer/notifu=ication strategy to the computation progress, with some code triggered when we add a new result. Previously code would Sysout the result and separately add to the Map. Allows to better control what we do with the results. Opens the road to more reuse of the code base outside of producing MCC compliant traces. Hopefully this huge commit is not breaking anything, but it sure is intrusive. Otoh it simplifies the code (a single place now with the keyword "FORMULA"...) and may avoid some bugs (doneProps and sysout not in accord like we detected in a recent patch). --- .../ConcurrentHashDoneProperties.java | 41 +++++++++++++ .../gal/mcc/properties/DoneProperties.java | 22 +++++++ .../gal/mcc/properties/PropertiesToPNML.java | 5 +- .../move/gal/application/AbstractRunner.java | 6 +- .../move/gal/application/Application.java | 59 +++++++------------ .../move/gal/application/AtomicReducerSR.java | 5 +- .../gal/application/GlobalPropertySolver.java | 51 +++------------- .../fr/lip6/move/gal/application/IRunner.java | 4 +- .../lip6/move/gal/application/ITSRunner.java | 32 +++------- .../move/gal/application/LTSminRunner.java | 4 +- .../application/MccDonePropertyPrinter.java | 20 +++++++ .../move/gal/application/MccTranslator.java | 3 +- .../gal/application/ReachabilitySolver.java | 43 +++++--------- .../lip6/move/gal/application/SMTRunner.java | 11 ++-- .../move/gal/application/SpotLTLRunner.java | 5 +- .../move/gal/gal2smt/Gal2SMTFrontEnd.java | 19 +++--- 16 files changed, 166 insertions(+), 164 deletions(-) create mode 100644 fr.lip6.move.gal.structural/src/fr/lip6/move/gal/mcc/properties/ConcurrentHashDoneProperties.java create mode 100644 fr.lip6.move.gal.structural/src/fr/lip6/move/gal/mcc/properties/DoneProperties.java create mode 100644 pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/MccDonePropertyPrinter.java diff --git a/fr.lip6.move.gal.structural/src/fr/lip6/move/gal/mcc/properties/ConcurrentHashDoneProperties.java b/fr.lip6.move.gal.structural/src/fr/lip6/move/gal/mcc/properties/ConcurrentHashDoneProperties.java new file mode 100644 index 0000000000..6eba978d2f --- /dev/null +++ b/fr.lip6.move.gal.structural/src/fr/lip6/move/gal/mcc/properties/ConcurrentHashDoneProperties.java @@ -0,0 +1,41 @@ +package fr.lip6.move.gal.mcc.properties; + +import java.util.Map; +import java.util.Map.Entry; +import java.util.Set; +import java.util.concurrent.ConcurrentHashMap; + +public class ConcurrentHashDoneProperties implements DoneProperties { + private Map map = new ConcurrentHashMap<>(); + + @Override + public boolean containsKey(Object arg0) { + return map.containsKey(arg0); + } + + @Override + public Set> entrySet() { + return map.entrySet(); + } + + @Override + public Boolean put(String prop, Boolean value, String techniques) { + return map.put(prop, value); + } + + @Override + public Boolean put(String prop, Integer value, String techniques) { + return map.put(prop, true); + } + + @Override + public Set keySet() { + return map.keySet(); + } + + @Override + public int size() { + return map.size(); + } + +} diff --git a/fr.lip6.move.gal.structural/src/fr/lip6/move/gal/mcc/properties/DoneProperties.java b/fr.lip6.move.gal.structural/src/fr/lip6/move/gal/mcc/properties/DoneProperties.java new file mode 100644 index 0000000000..15a8f59964 --- /dev/null +++ b/fr.lip6.move.gal.structural/src/fr/lip6/move/gal/mcc/properties/DoneProperties.java @@ -0,0 +1,22 @@ +package fr.lip6.move.gal.mcc.properties; + +import java.util.Map.Entry; +import java.util.Set; + +public interface DoneProperties { + + int size(); + + // A boolean result + Boolean put(String prop, Boolean value, String techniques); + // A numeric result + Boolean put(String prop, Integer value, String techniques); + + + Set> entrySet(); + + boolean containsKey(Object arg0); + + Set keySet(); + +} diff --git a/fr.lip6.move.gal.structural/src/fr/lip6/move/gal/mcc/properties/PropertiesToPNML.java b/fr.lip6.move.gal.structural/src/fr/lip6/move/gal/mcc/properties/PropertiesToPNML.java index 155a95474d..4e842947fe 100644 --- a/fr.lip6.move.gal.structural/src/fr/lip6/move/gal/mcc/properties/PropertiesToPNML.java +++ b/fr.lip6.move.gal.structural/src/fr/lip6/move/gal/mcc/properties/PropertiesToPNML.java @@ -37,7 +37,7 @@ private static Logger getLog() { * @return true if we had to introduce a special "one" place to represent constants. * @throws IOException */ - public static boolean transform(SparsePetriNet spn, String path, Map doneProps) throws IOException { + public static boolean transform(SparsePetriNet spn, String path, DoneProperties doneProps) throws IOException { long time = System.currentTimeMillis(); PrintWriter pw = new PrintWriter(new File(path)); pw.append("\n"); @@ -45,8 +45,7 @@ public static boolean transform(SparsePetriNet spn, String path, Map\n"); boolean usesConstants = false; for (Property prop : spn.getProperties()) { - Boolean res = doneProps.get(prop.getName()); - if (res == null) { + if (! doneProps.containsKey(prop.getName())) { pw.append(" \n" + " "+ prop.getName() +"\n" + " Automatically generated\n" + diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/AbstractRunner.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/AbstractRunner.java index 7c81ca7b44..2a87233936 100644 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/AbstractRunner.java +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/AbstractRunner.java @@ -1,14 +1,14 @@ package fr.lip6.move.gal.application; import java.io.IOException; -import java.util.Map; import fr.lip6.move.gal.Specification; +import fr.lip6.move.gal.mcc.properties.DoneProperties; public abstract class AbstractRunner implements IRunner { protected Specification spec; - protected Map doneProps; + protected DoneProperties doneProps; protected Thread runnerThread; public AbstractRunner() { super(); @@ -29,7 +29,7 @@ public void join() throws InterruptedException { } @Override - public void configure(Specification z3Spec, Map doneProps) throws IOException { + public void configure(Specification z3Spec, DoneProperties doneProps) throws IOException { this.spec = z3Spec ; this.doneProps = doneProps; } 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 1956f47c50..7d0e6e453b 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 @@ -56,6 +56,7 @@ import fr.lip6.move.gal.logic.Properties; import fr.lip6.move.gal.logic.saxparse.PropertyParser; import fr.lip6.move.gal.logic.togal.ToGalTransformer; +import fr.lip6.move.gal.mcc.properties.DoneProperties; import fr.lip6.move.gal.mcc.properties.PropertiesToPNML; import fr.lip6.move.gal.semantics.IDeterministicNextBuilder; import fr.lip6.move.gal.semantics.INextBuilder; @@ -289,7 +290,7 @@ public Object startNoEx(IApplicationContext context) throws Exception { } // initialize a shared container to detect help detect termination in portfolio case - Map doneProps = new ConcurrentHashMap<>(); + DoneProperties doneProps = new MccDonePropertyPrinter(); // reader now has a spec and maybe a ITS decomposition // no properties yet. @@ -588,11 +589,9 @@ public Object startNoEx(IApplicationContext context) throws Exception { if (parikh == null) { Property prop = specnocol.getProperties().get(v); if (prop.getBody() instanceof ReachableProp) { - System.out.println("FORMULA "+prop.getName() + " FALSE TECHNIQUES COLOR_ABSTRACTION STRUCTURAL_REDUCTION TOPOLOGICAL SAT_SMT"); - doneProps.put(prop.getName(),false); + doneProps.put(prop.getName(),false, "COLOR_ABSTRACTION STRUCTURAL_REDUCTION TOPOLOGICAL SAT_SMT"); } else { - System.out.println("FORMULA "+prop.getName() + " TRUE TECHNIQUES COLOR_ABSTRACTION STRUCTURAL_REDUCTION TOPOLOGICAL SAT_SMT"); - doneProps.put(prop.getName(),true); + doneProps.put(prop.getName(),true, "COLOR_ABSTRACTION STRUCTURAL_REDUCTION TOPOLOGICAL SAT_SMT"); } iter++; } @@ -738,7 +737,7 @@ private boolean runBlissSymmetryAnalysis(MccTranslator reader, StructuralReducti } private void tryRebuildPNML(String pwd, String examination, boolean rebuildPNML, MccTranslator reader, - Map doneProps) throws IOException { + DoneProperties doneProps) throws IOException { if (rebuildPNML) { String outform = pwd + "/" + examination + ".sr.xml"; boolean usesConstants = PropertiesToPNML.transform(reader.getSPN(), outform, doneProps); @@ -770,7 +769,7 @@ public int rebuildSpecification(MccTranslator reader, StructuralReduction sr) { return done; } - private void regeneratePNML (MccTranslator reader, Map doneProps, String solverPath, boolean isSafe) { + private void regeneratePNML (MccTranslator reader, DoneProperties doneProps, String solverPath, boolean isSafe) { reader.flattenSpec(false); System.out.println("Initial size " + ((GALTypeDeclaration) reader.getSpec().getTypes().get(0)).getVariables().size()); for (Entry prop : doneProps.entrySet()) { @@ -812,7 +811,7 @@ private List translateProperties(List props, IDeterministi } private MccTranslator runMultiITS(String pwd, String examination, String gspnpath, String orderHeur, boolean doITS, - boolean onlyGal, boolean doHierarchy, boolean useManyOrder, MccTranslator reader, Map doneProps, boolean useLouvain, long timeout) + boolean onlyGal, boolean doHierarchy, boolean useManyOrder, MccTranslator reader, DoneProperties doneProps, boolean useLouvain, long timeout) throws IOException, InterruptedException { MccTranslator reader2 = null; long elapsed = (startTime - System.currentTimeMillis()) / 1000; @@ -949,19 +948,12 @@ private String computeOrderWithGreatSPN(String pwd, String gspnpath, String orde return orderff; } - - - - - - - /** * Structural analysis and reduction : test in initial state. * @param specWithProps spec which will be modified : trivial properties will be removed * @param doneProps */ - private int checkInInitial(Specification specWithProps, Map doneProps, boolean isSafe) { + private int checkInInitial(Specification specWithProps, DoneProperties doneProps, boolean isSafe) { List props = new ArrayList(specWithProps.getProperties()); int done = 0; // iterate down so indexes are consistent @@ -1009,72 +1001,61 @@ private int checkInInitial(Specification specWithProps, Map don LogicProp prop = propp.getBody(); Simplifier.simplifyAllExpressions(prop); + String tech = "TOPOLOGICAL INITIAL_STATE"; boolean solved = false; - boolean verdict = false; // output verdict if (prop instanceof ReachableProp || prop instanceof InvariantProp) { if (((SafetyProp) prop).getPredicate() instanceof True) { // positive forms : EF True , AG True <=>True - System.out.println("FORMULA "+propp.getName() + " TRUE TECHNIQUES TOPOLOGICAL INITIAL_STATE"); + doneProps.put(propp.getName(), true, tech); solved = true; - verdict = true; } else if (((SafetyProp) prop).getPredicate() instanceof False) { // positive forms : EF False , AG False <=> False - System.out.println("FORMULA "+propp.getName() + " FALSE TECHNIQUES TOPOLOGICAL INITIAL_STATE"); + doneProps.put(propp.getName(), false, tech); solved = true; - verdict = false; } } else if (prop instanceof NeverProp) { if (((SafetyProp) prop).getPredicate() instanceof True) { // negative form : ! EF P = AG ! P, so ! EF True <=> False - System.out.println("FORMULA "+propp.getName() + " FALSE TECHNIQUES TOPOLOGICAL INITIAL_STATE"); + doneProps.put(propp.getName(), false, tech); solved = true; - verdict = false; } else if (((SafetyProp) prop).getPredicate() instanceof False) { // negative form : ! EF P = AG ! P, so ! EF False <=> True - System.out.println("FORMULA "+propp.getName() + " TRUE TECHNIQUES TOPOLOGICAL INITIAL_STATE"); + doneProps.put(propp.getName(), true, tech); solved = true; - verdict = true; } } else if (prop instanceof LTLProp) { LTLProp ltl = (LTLProp) prop; if (ltl.getPredicate() instanceof True) { // positive forms : EF True , AG True <=>True - System.out.println("FORMULA "+propp.getName() + " TRUE TECHNIQUES TOPOLOGICAL INITIAL_STATE"); + doneProps.put(propp.getName(), true, tech); solved = true; - verdict = true; } else if (ltl.getPredicate() instanceof False) { // positive forms : EF False , AG False <=> False - System.out.println("FORMULA "+propp.getName() + " FALSE TECHNIQUES TOPOLOGICAL INITIAL_STATE"); + doneProps.put(propp.getName(), false, tech); solved = true; - verdict = false; } } else if (prop instanceof CTLProp) { CTLProp ltl = (CTLProp) prop; if (ltl.getPredicate() instanceof True) { // positive forms : EF True , AG True <=>True - System.out.println("FORMULA "+propp.getName() + " TRUE TECHNIQUES TOPOLOGICAL INITIAL_STATE"); + doneProps.put(propp.getName(), true, tech); solved = true; - verdict = true; } else if (ltl.getPredicate() instanceof False) { // positive forms : EF False , AG False <=> False - System.out.println("FORMULA "+propp.getName() + " FALSE TECHNIQUES TOPOLOGICAL INITIAL_STATE"); + doneProps.put(propp.getName(), false, tech); solved = true; - verdict = false; } } else if (prop instanceof BoundsProp) { BoundsProp bp = (BoundsProp) prop; if (bp.getTarget() instanceof Constant) { - System.out.println("FORMULA "+propp.getName() + " " + ((Constant) bp.getTarget()).getValue() +" TECHNIQUES TOPOLOGICAL INITIAL_STATE"); + doneProps.put(propp.getName(),((Constant) bp.getTarget()).getValue(),tech); solved = true; - verdict = true; - } - + } } - if (solved) { - doneProps.put(propp.getName(),verdict); + if (solved) { // discard property specWithProps.getProperties().remove(i); done++; diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/AtomicReducerSR.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/AtomicReducerSR.java index 4881b20139..e9219a49a4 100644 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/AtomicReducerSR.java +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/AtomicReducerSR.java @@ -13,6 +13,7 @@ import android.util.SparseIntArray; import fr.lip6.move.gal.gal2smt.DeadlockTester; +import fr.lip6.move.gal.mcc.properties.DoneProperties; import fr.lip6.move.gal.structural.Property; import fr.lip6.move.gal.structural.RandomExplorer; import fr.lip6.move.gal.structural.SparsePetriNet; @@ -25,7 +26,7 @@ public class AtomicReducerSR { private static final int DEBUG = 0; - public int strongReductions(String solverPath, MccTranslator reader, boolean isSafe, Map doneProps) { + public int strongReductions(String solverPath, MccTranslator reader, boolean isSafe, DoneProperties doneProps) { int solved = checkAtomicPropositions(reader.getSPN(), doneProps, isSafe,solverPath, true); solved += checkAtomicPropositions(reader.getSPN(), doneProps, isSafe,solverPath, false); reader.getSPN().simplifyLogic(); @@ -68,7 +69,7 @@ private boolean isPureBool(Expression expr) { * @param solverPath * @param comparisonAtoms if true look only at comparisons only as atoms (single predicate), otherwise sub boolean formulas are considered atoms (CTL, LTL) */ - private int checkAtomicPropositions(SparsePetriNet spec, Map doneProps, boolean isSafe, String solverPath, boolean comparisonAtoms) { + private int checkAtomicPropositions(SparsePetriNet spec, DoneProperties doneProps, boolean isSafe, String solverPath, boolean comparisonAtoms) { if (solverPath == null) { return 0; 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 4c9761507c..50a9d6d55e 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,10 +1,8 @@ package fr.lip6.move.gal.application; import java.util.Collections; -import java.util.Map; -import java.util.Map.Entry; -import java.util.concurrent.ConcurrentHashMap; +import fr.lip6.move.gal.mcc.properties.DoneProperties; import fr.lip6.move.gal.structural.DeadlockFound; import fr.lip6.move.gal.structural.NoDeadlockExists; import fr.lip6.move.gal.structural.Property; @@ -24,7 +22,7 @@ public GlobalPropertySolver(String solverPath) { public boolean solveProperty(String examination, MccTranslator reader) { // initialize a shared container to detect help detect termination in portfolio case - Map doneProps = new ConcurrentHashMap<>(); + DoneProperties doneProps = new MccDonePropertyPrinter(); boolean isSafe = false; // load "known" stuff about the model @@ -36,35 +34,13 @@ public boolean solveProperty(String examination, MccTranslator reader) { // build properties SparsePetriNet spn = reader.getSPN(); -// for (int tid=0; tid < spn.getTransitionCount() ; tid++) { -// Expression prop = Expression.nop(Op.ENABLED, Collections.singletonList(Expression.trans(tid))); -// Expression ag = Expression.op(Op.AG, prop, null); -// Property p = new Property(ag ,PropertyType.INVARIANT,"enabled"+tid); -// spn.getProperties().add(p ); -// } -// System.out.println(spn); -// -// -// Expression stable = Expression.op(Op.EQ, Expression.var(0), Expression.constant(spn.getMarks().get(0))); -// - for(int pid = 0; pid < spn.getPlaceCount(); pid++) { - Expression pInfOne = Expression.op(Op.LEQ, Expression.var(pid), Expression.constant(1)); - // unary op ignore right - Expression ag = Expression.op(Op.AG, pInfOne, null); - Property oneSafeProperty = new Property(ag ,PropertyType.INVARIANT,"place_"+pid); - spn.getProperties().add(oneSafeProperty); + for (int tid=0; tid < spn.getTransitionCount() ; tid++) { + Expression prop = Expression.nop(Op.ENABLED, Collections.singletonList(Expression.trans(tid))); + Property p = new Property(prop ,PropertyType.INVARIANT,"enabled"+tid); + spn.getProperties().add(p ); } + System.out.println(spn); - spn.simplifyLogic(); - spn.toPredicates(); - spn.testInInitial(); - spn.removeConstantPlaces(); - spn.removeRedundantTransitions(false); - spn.removeConstantPlaces(); - spn.simplifyLogic(); - if (isSafe) { - spn.assumeOneSafe(); - } // vire les prop triviales, utile ? ReachabilitySolver.checkInInitial(reader, doneProps); @@ -76,17 +52,8 @@ public boolean solveProperty(String examination, MccTranslator reader) { } catch (DeadlockFound e) { e.printStackTrace(); } - } - boolean isOneSafe = true; - for(Entry e : doneProps.entrySet()) { - if(e.getValue() == true) { - System.out.println("FORMULA ONESAFE FALSE"); - isOneSafe = false; - System.out.println("Property is false " + e.getKey()); - break; - } - } - if(isOneSafe) System.out.println("FORMULA ONESAFE TRUE"); + } + return false; } diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/IRunner.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/IRunner.java index 0d086587f6..d059938b37 100644 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/IRunner.java +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/IRunner.java @@ -1,9 +1,9 @@ package fr.lip6.move.gal.application; import java.io.IOException; -import java.util.Map; import fr.lip6.move.gal.Specification; +import fr.lip6.move.gal.mcc.properties.DoneProperties; public interface IRunner { @@ -11,7 +11,7 @@ public interface IRunner { void join() throws InterruptedException; - void configure(Specification z3Spec, Map doneProps) throws IOException; + void configure(Specification z3Spec, DoneProperties doneProps) throws IOException; void solve(Ender application); diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/ITSRunner.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/ITSRunner.java index 99745ecbe0..65a566a30b 100644 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/ITSRunner.java +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/ITSRunner.java @@ -21,6 +21,7 @@ import fr.lip6.move.gal.Reference; import fr.lip6.move.gal.Specification; import fr.lip6.move.gal.itstools.CommandLineBuilder; +import fr.lip6.move.gal.mcc.properties.DoneProperties; import fr.lip6.move.gal.itstools.BinaryToolsPlugin.Tool; import fr.lip6.move.gal.process.CommandLine; import fr.lip6.move.gal.process.Runner; @@ -55,7 +56,7 @@ public ITSRunner(String examination, MccTranslator reader, boolean doITS, boolea @Override - public void configure(Specification spec, Map doneProps) throws IOException { + public void configure(Specification spec, DoneProperties doneProps) throws IOException { super.configure(spec, doneProps); if (examination.equals("StateSpace")) { String outpath = outputGalFile(); @@ -154,12 +155,12 @@ class ITSInterpreter implements Runnable { private String examination; private boolean withStructure; private MccTranslator reader; - private Map seen; + private DoneProperties seen; private Set todoProps; private Ender ender; - public ITSInterpreter(String examination, boolean withStructure, MccTranslator reader, Map doneProps, Set todoProps, Ender ender) { + public ITSInterpreter(String examination, boolean withStructure, MccTranslator reader, DoneProperties doneProps, Set todoProps, Ender ender) { this.examination = examination; this.withStructure = withStructure; this.reader = reader; @@ -212,13 +213,7 @@ public void run() { Property dead = reader.getSpec().getProperties().get(0); String pname = dead.getName(); double nbdead = Double.parseDouble(line.split("\\s+")[2]); - String res ; - if (nbdead == 0) - res = "FALSE"; - else - res = "TRUE"; - System.out.println( "FORMULA " + pname + " " +res + " TECHNIQUES DECISION_DIAGRAMS TOPOLOGICAL " + (withStructure?"USE_NUPN":"") ); - seen.put(pname,nbdead != 0); + seen.put(pname,nbdead != 0,"DECISION_DIAGRAMS TOPOLOGICAL " + (withStructure?"USE_NUPN":"")); } } if ( line.matches("Bounds property.*")) { @@ -247,8 +242,7 @@ public void run() { it.prune(); } } - seen.put(pname,true); - System.out.println( "FORMULA " + pname + " " + (bound+toadd) + " TECHNIQUES DECISION_DIAGRAMS TOPOLOGICAL " + (withStructure?"USE_NUPN":"") ); + seen.put(pname,(bound+toadd),"DECISION_DIAGRAMS TOPOLOGICAL "+ (withStructure?"USE_NUPN":"")); } } if ( examination.startsWith("CTL")) { @@ -256,14 +250,8 @@ public void run() { String [] tab = line.split(","); int formindex = Integer.parseInt(tab[0].split(" ")[1]); int verdict = Integer.parseInt(tab[1]); - String res ; - if (verdict == 0) - res = "FALSE"; - else - res = "TRUE"; String pname = reader.getSpec().getProperties().get(formindex).getName(); - System.out.println( "FORMULA " + pname + " " +res + " TECHNIQUES DECISION_DIAGRAMS TOPOLOGICAL " + (withStructure?"USE_NUPN":"") ); - seen.put(pname,verdict != 0); + seen.put(pname,verdict != 0,"DECISION_DIAGRAMS TOPOLOGICAL "+ (withStructure?"USE_NUPN":"")); } } if ( examination.startsWith("LTL")) { @@ -272,8 +260,7 @@ public void run() { int formindex = Integer.parseInt(tab[1]); String res = tab[3]; String pname = reader.getSpec().getProperties().get(formindex).getName(); - System.out.println( "FORMULA " + pname + " " +res + " TECHNIQUES DECISION_DIAGRAMS TOPOLOGICAL " + (withStructure?"USE_NUPN":"") ); - seen.put(pname, "TRUE".equals(res)); + seen.put(pname, "TRUE".equals(res),"DECISION_DIAGRAMS TOPOLOGICAL "+ (withStructure?"USE_NUPN":"")); } } @@ -296,8 +283,7 @@ public void run() { } pname = pname.replaceAll("\\s", ""); if (!seen.containsKey(pname)) { - System.out.println("FORMULA "+pname+ " "+ res + " TECHNIQUES DECISION_DIAGRAMS TOPOLOGICAL COLLATERAL_PROCESSING " + (withStructure?"USE_NUPN":"")); - seen.put(pname,"TRUE".equals(res)); + seen.put(pname,"TRUE".equals(res),"DECISION_DIAGRAMS TOPOLOGICAL COLLATERAL_PROCESSING " + (withStructure?"USE_NUPN":"")); } } } diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/LTSminRunner.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/LTSminRunner.java index 147a758c3e..8dc832d116 100644 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/LTSminRunner.java +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/LTSminRunner.java @@ -263,9 +263,7 @@ private void checkProperty(String pname, String pbody, long timeout, boolean neg } } String ress = (result + "").toUpperCase(); - System.out.println("FORMULA " + pname + " " + ress - + " TECHNIQUES " + (withPOR ? "PARTIAL_ORDER ":"") + "EXPLICIT LTSMIN SAT_SMT"); - doneProps.put(pname,"TRUE".equals(ress)); + doneProps.put(pname,"TRUE".equals(ress),(withPOR ? "PARTIAL_ORDER ":"") + "EXPLICIT LTSMIN SAT_SMT"); System.out.flush(); } catch (TimeoutException to) { System.out.println("WARNING : LTSmin timed out (>"+timeout+" s) on command " + ltsmin); diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/MccDonePropertyPrinter.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/MccDonePropertyPrinter.java new file mode 100644 index 0000000000..0f8c585df9 --- /dev/null +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/MccDonePropertyPrinter.java @@ -0,0 +1,20 @@ +package fr.lip6.move.gal.application; + +import fr.lip6.move.gal.mcc.properties.ConcurrentHashDoneProperties; + +public class MccDonePropertyPrinter extends ConcurrentHashDoneProperties { + + + @Override + public Boolean put(String prop, Boolean value, String techniques) { + System.out.println("FORMULA "+prop+(value?" TRUE":" FALSE")+ " TECHNIQUES "+techniques); + return super.put(prop, value, techniques); + } + + + @Override + public Boolean put(String prop, Integer value, String techniques) { + System.out.println("FORMULA "+prop+" "+value+ " TECHNIQUES "+techniques); + return super.put(prop, value, techniques); + } +} diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/MccTranslator.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/MccTranslator.java index 7f0bdf9d7a..d8d29d2618 100644 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/MccTranslator.java +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/MccTranslator.java @@ -66,6 +66,7 @@ import fr.lip6.move.gal.LTLProp; import fr.lip6.move.gal.LTLUntil; import fr.lip6.move.gal.louvain.GraphBuilder; +import fr.lip6.move.gal.mcc.properties.DoneProperties; import fr.lip6.move.gal.order.CompositeGalOrder; import fr.lip6.move.gal.order.IOrder; import fr.lip6.move.gal.order.IOrderVisitor; @@ -703,7 +704,7 @@ private int collectChildren(IntExpression expr, Set vars) throws BadSumE } - public void rebuildSpecification(Map doneProps) { + public void rebuildSpecification(DoneProperties doneProps) { Specification reduced = getSPN().rebuildSpecification(); for (fr.lip6.move.gal.structural.Property prop : spn.getProperties()) { if (! doneProps.containsKey(prop.getName())) diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/ReachabilitySolver.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/ReachabilitySolver.java index 3a21063e11..04e0a3d825 100644 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/ReachabilitySolver.java +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/ReachabilitySolver.java @@ -3,15 +3,13 @@ import java.util.ArrayList; import java.util.BitSet; import java.util.List; -import java.util.Map; import android.util.SparseIntArray; import fr.lip6.move.gal.gal2smt.DeadlockTester; +import fr.lip6.move.gal.mcc.properties.DoneProperties; import fr.lip6.move.gal.structural.DeadlockFound; import fr.lip6.move.gal.structural.NoDeadlockExists; -import fr.lip6.move.gal.structural.Property; import fr.lip6.move.gal.structural.RandomExplorer; -import fr.lip6.move.gal.structural.RandomExplorer.WasExhaustive; import fr.lip6.move.gal.structural.SparsePetriNet; import fr.lip6.move.gal.structural.StructuralReduction; import fr.lip6.move.gal.structural.StructuralReduction.ReductionType; @@ -21,21 +19,16 @@ public class ReachabilitySolver { - public static void checkInInitial(MccTranslator reader, Map doneProps) { + public static void checkInInitial(MccTranslator reader, DoneProperties doneProps) { for (fr.lip6.move.gal.structural.Property prop : new ArrayList<>(reader.getSPN().getProperties())) { if (prop.getBody().getOp() == Op.BOOLCONST) { - if (prop.getBody().getValue() == 1) { - System.out.println("FORMULA "+prop.getName() + " TRUE TECHNIQUES TOPOLOGICAL INITIAL_STATE"); - } else { - System.out.println("FORMULA "+prop.getName() + " FALSE TECHNIQUES TOPOLOGICAL INITIAL_STATE"); - } - doneProps.put(prop.getName(),prop.getBody().getValue()==1); + doneProps.put(prop.getName(),prop.getBody().getValue()==1,"TOPOLOGICAL INITIAL_STATE"); reader.getSPN().getProperties().remove(prop); } } } - public static void applyReductions(MccTranslator reader, Map doneProps, String solverPath, boolean isSafe) + public static void applyReductions(MccTranslator reader, DoneProperties doneProps, String solverPath, boolean isSafe) throws NoDeadlockExists, DeadlockFound { int iter; int iterations =0; @@ -204,12 +197,12 @@ public static void computeToCheck(SparsePetriNet spn, List tocheckIndex for (int j=0; j < spn.getProperties().size(); j++) { tocheckIndexes.add(j);} } - static int treatVerdicts(SparsePetriNet sparsePetriNet, Map doneProps, List tocheck, + static int treatVerdicts(SparsePetriNet sparsePetriNet, DoneProperties doneProps, List tocheck, List tocheckIndexes, List paths) { return treatVerdicts(sparsePetriNet, doneProps, tocheck, tocheckIndexes, paths, ""); } - static int treatVerdicts(SparsePetriNet spn, Map doneProps, List tocheck, + static int treatVerdicts(SparsePetriNet spn, DoneProperties doneProps, List tocheck, List tocheckIndexes, List paths, String technique) { int iter = 0; for (int v = paths.size()-1 ; v >= 0 ; v--) { @@ -217,12 +210,10 @@ static int treatVerdicts(SparsePetriNet spn, Map doneProps, Lis if (parikh == null) { fr.lip6.move.gal.structural.Property prop = spn.getProperties().get(tocheckIndexes.get(v)); if (prop.getBody().getOp() == Op.EF) { - System.out.println("FORMULA "+prop.getName() + " FALSE TECHNIQUES STRUCTURAL_REDUCTION TOPOLOGICAL SAT_SMT " + technique); - doneProps.put(prop.getName(),false); + doneProps.put(prop.getName(),false,"STRUCTURAL_REDUCTION TOPOLOGICAL SAT_SMT "+technique); } else { // AG - System.out.println("FORMULA "+prop.getName() + " TRUE TECHNIQUES STRUCTURAL_REDUCTION TOPOLOGICAL SAT_SMT " + technique); - doneProps.put(prop.getName(),true); + doneProps.put(prop.getName(),true,"STRUCTURAL_REDUCTION TOPOLOGICAL SAT_SMT "+technique); } tocheck.remove(v); @@ -236,7 +227,7 @@ static int treatVerdicts(SparsePetriNet spn, Map doneProps, Lis } static int randomCheckReachability(RandomExplorer re, List tocheck, SparsePetriNet spn, - Map doneProps, int steps) { + DoneProperties doneProps, int steps) { int[] verdicts = re.runRandomReachabilityDetection(steps,tocheck,30,-1); int seen = interpretVerdict(tocheck, spn, doneProps, verdicts,"RANDOM"); for (int i=0 ; i < tocheck.size() ; i++) { @@ -260,23 +251,21 @@ static int randomCheckReachability(RandomExplorer re, List tocheck, return seen; } - private static int interpretVerdict(List tocheck, SparsePetriNet spn, Map doneProps, + private static int interpretVerdict(List tocheck, SparsePetriNet spn, DoneProperties doneProps, int[] verdicts, String walkType) { return interpretVerdict(tocheck, spn, doneProps, verdicts, walkType, false); } - private static int interpretVerdict(List tocheck, SparsePetriNet spn, Map doneProps, + private static int interpretVerdict(List tocheck, SparsePetriNet spn, DoneProperties doneProps, int[] verdicts, String walkType, boolean andNeg) { int seen = 0; for (int v = verdicts.length-1 ; v >= 0 ; v--) { if (verdicts[v] != 0) { fr.lip6.move.gal.structural.Property prop = spn.getProperties().get(v); if (prop.getBody().getOp() == Op.EF) { - System.out.println("FORMULA "+prop.getName() + " TRUE TECHNIQUES TOPOLOGICAL "+walkType+"_WALK"); - doneProps.put(prop.getName(),true); + doneProps.put(prop.getName(),true,"TOPOLOGICAL "+walkType+"_WALK"); } else { - System.out.println("FORMULA "+prop.getName() + " FALSE TECHNIQUES TOPOLOGICAL "+walkType+"_WALK"); - doneProps.put(prop.getName(),false); + doneProps.put(prop.getName(),false,"TOPOLOGICAL "+walkType+"_WALK"); } tocheck.remove(v); spn.getProperties().remove(v); @@ -284,11 +273,9 @@ private static int interpretVerdict(List tocheck, SparsePetriNet spn } else if (andNeg) { fr.lip6.move.gal.structural.Property prop = spn.getProperties().get(v); if (prop.getBody().getOp() == Op.EF) { - System.out.println("FORMULA "+prop.getName() + " FALSE TECHNIQUES TOPOLOGICAL "+walkType+"_WALK"); - doneProps.put(prop.getName(),false); + doneProps.put(prop.getName(),false,"TOPOLOGICAL "+walkType+"_WALK"); } else { - System.out.println("FORMULA "+prop.getName() + " TRUE TECHNIQUES TOPOLOGICAL "+walkType+"_WALK"); - doneProps.put(prop.getName(),true); + doneProps.put(prop.getName(),true,"TOPOLOGICAL "+walkType+"_WALK"); } tocheck.remove(v); spn.getProperties().remove(v); diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/SMTRunner.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/SMTRunner.java index 529004d870..c03b1e3dfe 100644 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/SMTRunner.java +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/SMTRunner.java @@ -9,6 +9,7 @@ import fr.lip6.move.gal.gal2smt.ISMTObserver; import fr.lip6.move.gal.gal2smt.Result; import fr.lip6.move.gal.gal2smt.Solver; +import fr.lip6.move.gal.mcc.properties.DoneProperties; public class SMTRunner extends AbstractRunner implements IRunner { @@ -32,7 +33,7 @@ private Logger getLog() { } public Thread runSMT(final String pwd, final String solverPath, final Solver solver, final Specification z3Spec, - final Ender ender, Map doneProps) { + final Ender ender, DoneProperties doneProps) { runnerThread = new Thread(new Runnable() { int nbsolve = 0; @@ -44,8 +45,8 @@ public void run() { @Override public synchronized void notifyResult(Property prop, Result res, String desc) { if (res == Result.TRUE || res == Result.FALSE) { - System.out.println( - "FORMULA " + prop.getName() + " " + res + " " + "TECHNIQUES SAT_SMT " + desc); +// System.out.println( +// "FORMULA " + prop.getName() + " " + res + " " + "TECHNIQUES SAT_SMT " + desc); nbsolve++; } else { // a ambiguous verdict @@ -88,8 +89,8 @@ public void run() { @Override public synchronized void notifyResult(Property prop, Result res, String desc) { if (res == Result.TRUE || res == Result.FALSE) { - System.out.println( - "FORMULA " + prop.getName() + " " + res + " " + "TECHNIQUES SAT_SMT " + desc); +// System.out.println( +// "FORMULA " + prop.getName() + " " + res + " " + "TECHNIQUES SAT_SMT " + desc); nbsolve++; } else { // a ambiguous verdict diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/SpotLTLRunner.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/SpotLTLRunner.java index 1dab83c063..b75559b6ea 100644 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/SpotLTLRunner.java +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/SpotLTLRunner.java @@ -269,10 +269,7 @@ private void checkProperty(String pname, String pbody, long timeout, boolean neg } } } - String ress = (result + "").toUpperCase(); - System.out.println("FORMULA " + pname + " " + ress - + " TECHNIQUES " + (withPOR ? "PARTIAL_ORDER ":"") + "EXPLICIT SpotMC SAT_SMT"); - doneProps.put(pname,"TRUE".equals(ress)); + doneProps.put(pname,result,(withPOR ? "PARTIAL_ORDER ":"") + "EXPLICIT SpotMC SAT_SMT"); System.out.flush(); } catch (TimeoutException to) { System.out.println("WARNING : SpotMC timed out (>"+timeout+" s) on command " + SpotMC); diff --git a/smt/fr.lip6.move.gal.gal2smt/src/fr/lip6/move/gal/gal2smt/Gal2SMTFrontEnd.java b/smt/fr.lip6.move.gal.gal2smt/src/fr/lip6/move/gal/gal2smt/Gal2SMTFrontEnd.java index 575258c839..931c8e570f 100644 --- a/smt/fr.lip6.move.gal.gal2smt/src/fr/lip6/move/gal/gal2smt/Gal2SMTFrontEnd.java +++ b/smt/fr.lip6.move.gal.gal2smt/src/fr/lip6/move/gal/gal2smt/Gal2SMTFrontEnd.java @@ -25,6 +25,7 @@ import fr.lip6.move.gal.gal2smt.bmc.NextBMCSolver; import fr.lip6.move.gal.gal2smt.smt.IBMCSolver; import fr.lip6.move.gal.instantiate.GALRewriter; +import fr.lip6.move.gal.mcc.properties.DoneProperties; import fr.lip6.move.gal.semantics.IDeterministicNextBuilder; import fr.lip6.move.gal.semantics.INextBuilder; @@ -71,7 +72,7 @@ public NecessaryEnablingsolver buildNecessaryEnablingSolver (boolean isSafe) { return nes; } - public Map checkProperties (final Specification spec, String folder, Map doneProps, boolean isSafe) throws Exception { + public Map checkProperties (final Specification spec, String folder, DoneProperties doneProps, boolean isSafe) throws Exception { GALRewriter.flatten(spec, true); // getLog().info("Translation to SMT took " + ( System.currentTimeMillis() - timestamp ) + " ms"); @@ -114,7 +115,7 @@ public Map checkProperties (final Specification spec, String fol } notifyObservers(prop, res, "TAUTOLOGY"); result.put(prop.getName(), res); - doneProps.put(prop.getName(), res==Result.TRUE); + doneProps.put(prop.getName(), res==Result.TRUE,"SAT_SMT TAUTOLOGY"); taut.add(prop); continue; } else if (sp.getPredicate() instanceof False) { @@ -126,7 +127,7 @@ public Map checkProperties (final Specification spec, String fol } notifyObservers(prop, res, "TAUTOLOGY"); result.put(prop.getName(), res); - doneProps.put(prop.getName(), res==Result.TRUE); + doneProps.put(prop.getName(), res==Result.TRUE, "SAT_SMT TAUTOLOGY"); taut.add(prop); continue; } @@ -146,7 +147,7 @@ public Map checkProperties (final Specification spec, String fol } notifyObservers(prop, res, "TAUTOLOGY"); result.put(prop.getName(), res); - doneProps.put(prop.getName(),res==Result.TRUE); + doneProps.put(prop.getName(),res==Result.TRUE, "SAT_SMT TAUTOLOGY"); taut.add(prop); } @@ -187,7 +188,7 @@ public void run() { return result; } - private void cleanTodo(List todo, Map doneProps) { + private void cleanTodo(List todo, DoneProperties doneProps) { todo.removeIf( p -> doneProps.containsKey(p.getName())); } @@ -275,7 +276,7 @@ private void cleanTodo(List todo, Map doneProps) { // return result; // } - private void runKInduction(Configuration smtConfig, List todo, int i, Map result, IDeterministicNextBuilder spec, Map doneProps, boolean isSafe) { + private void runKInduction(Configuration smtConfig, List todo, int i, Map result, IDeterministicNextBuilder spec, DoneProperties doneProps, boolean isSafe) { if (todo.isEmpty()) { return ; } long timestamp = System.currentTimeMillis(); KInductionSolver kind = new KInductionSolver(smtConfig, engine, true, isSafe); @@ -324,7 +325,7 @@ private void runKInduction(Configuration smtConfig, List todo, int i, } // we disproved for all n ! getLog().info(" Induction result is UNSAT, successfully proved induction at step "+ depth +" for " + prop.getName()); - doneProps.put(prop.getName(),res==Result.TRUE); + doneProps.put(prop.getName(),res==Result.TRUE,"SAT_SMT K_INDUCTION("+depth+")"); } notifyObservers(prop, res, "K_INDUCTION("+depth+")"); result.put(prop.getName(), res); @@ -353,7 +354,7 @@ private void runKInduction(Configuration smtConfig, List todo, int i, } - private void runBMC(IBMCSolver bmc, List todo, int maxd, Map result, Map doneProps, Map expectedLength) throws RuntimeException { + private void runBMC(IBMCSolver bmc, List todo, int maxd, Map result, DoneProperties doneProps, Map expectedLength) throws RuntimeException { try { // 300 secs timeout for full loop @@ -390,7 +391,7 @@ private void runBMC(IBMCSolver bmc, List todo, int maxd, Map Date: Wed, 24 Feb 2021 15:22:39 +0100 Subject: [PATCH 04/43] more Map->DoneProperties to update --- .../src/fr/lip6/move/gal/gal2java/TestBMC.java | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/pins/fr.lip6.move.gal.gal2pins/src/fr/lip6/move/gal/gal2java/TestBMC.java b/pins/fr.lip6.move.gal.gal2pins/src/fr/lip6/move/gal/gal2java/TestBMC.java index 3e7d96529e..a111687825 100644 --- a/pins/fr.lip6.move.gal.gal2pins/src/fr/lip6/move/gal/gal2java/TestBMC.java +++ b/pins/fr.lip6.move.gal.gal2pins/src/fr/lip6/move/gal/gal2java/TestBMC.java @@ -6,6 +6,7 @@ import fr.lip6.move.gal.gal2smt.Gal2SMTFrontEnd; import fr.lip6.move.gal.gal2smt.Result; import fr.lip6.move.gal.gal2smt.Solver; +import fr.lip6.move.gal.mcc.properties.ConcurrentHashDoneProperties; import fr.lip6.move.serialization.SerializationUtil; public class TestBMC { @@ -40,7 +41,7 @@ public static void main(String[] args) { }); try { - smt.checkProperties(spec, "/data/ythierry/workspaces/neon/fr.lip6.move.gal.gal2pins/tests/work", new ConcurrentHashMap<>(), false); + smt.checkProperties(spec, "/data/ythierry/workspaces/neon/fr.lip6.move.gal.gal2pins/tests/work", new ConcurrentHashDoneProperties(), false); } catch (Exception e) { // TODO Auto-generated catch block e.printStackTrace(); From 59540f0994b393ebf26c3175a9a30e94ae4201fe Mon Sep 17 00:00:00 2001 From: Yann Thierry-Mieg Date: Wed, 24 Feb 2021 15:35:27 +0100 Subject: [PATCH 05/43] semi unused code that still needs to be updated to new DoneProps API --- ltsmin/fr.lip6.move.gal.ltsmin/META-INF/MANIFEST.MF | 3 ++- .../fr/lip6/move/gal/ltsmin/orders/LTSMinOrderRunner.java | 4 +++- .../src/fr/lip6/move/gal/ltsmin/orders/LTSminRunner.java | 5 +---- 3 files changed, 6 insertions(+), 6 deletions(-) diff --git a/ltsmin/fr.lip6.move.gal.ltsmin/META-INF/MANIFEST.MF b/ltsmin/fr.lip6.move.gal.ltsmin/META-INF/MANIFEST.MF index baf15e2498..5d1f50ea6e 100644 --- a/ltsmin/fr.lip6.move.gal.ltsmin/META-INF/MANIFEST.MF +++ b/ltsmin/fr.lip6.move.gal.ltsmin/META-INF/MANIFEST.MF @@ -12,5 +12,6 @@ Require-Bundle: fr.lip6.move.gal;bundle-version="1.0.0", fr.lip6.move.gal.itstools.binaries, org.eclipse.core.runtime;bundle-version="3.13.0", lip6.smtlib.plugin.SMTPlugin, - fr.lip6.move.gal.logic + fr.lip6.move.gal.logic, + fr.lip6.move.gal.structural Export-Package: fr.lip6.move.gal.ltsmin.orders diff --git a/ltsmin/fr.lip6.move.gal.ltsmin/src/fr/lip6/move/gal/ltsmin/orders/LTSMinOrderRunner.java b/ltsmin/fr.lip6.move.gal.ltsmin/src/fr/lip6/move/gal/ltsmin/orders/LTSMinOrderRunner.java index 864e5bdc6b..8b4341b0a6 100644 --- a/ltsmin/fr.lip6.move.gal.ltsmin/src/fr/lip6/move/gal/ltsmin/orders/LTSMinOrderRunner.java +++ b/ltsmin/fr.lip6.move.gal.ltsmin/src/fr/lip6/move/gal/ltsmin/orders/LTSMinOrderRunner.java @@ -17,13 +17,15 @@ import fr.lip6.move.gal.Specification; import fr.lip6.move.gal.application.Ender; import fr.lip6.move.gal.gal2smt.Solver; +import fr.lip6.move.gal.mcc.properties.ConcurrentHashDoneProperties; +import fr.lip6.move.gal.mcc.properties.DoneProperties; import fr.lip6.move.gal.semantics.INextBuilder; public class LTSMinOrderRunner { private LTSminRunner runner; - private Map doneProps = new HashMap<>(); + private DoneProperties doneProps = new ConcurrentHashDoneProperties(); public List buildOrder (Specification spec) { INextBuilder inb = INextBuilder.build(spec); diff --git a/ltsmin/fr.lip6.move.gal.ltsmin/src/fr/lip6/move/gal/ltsmin/orders/LTSminRunner.java b/ltsmin/fr.lip6.move.gal.ltsmin/src/fr/lip6/move/gal/ltsmin/orders/LTSminRunner.java index aee0739451..81359da870 100644 --- a/ltsmin/fr.lip6.move.gal.ltsmin/src/fr/lip6/move/gal/ltsmin/orders/LTSminRunner.java +++ b/ltsmin/fr.lip6.move.gal.ltsmin/src/fr/lip6/move/gal/ltsmin/orders/LTSminRunner.java @@ -229,10 +229,7 @@ private void checkProperty(Property prop, Gal2PinsTransformerNext g2p, long time } } } - String ress = (result + "").toUpperCase(); - System.out.println("FORMULA " + prop.getName() + " " + ress - + " TECHNIQUES PARTIAL_ORDER EXPLICIT LTSMIN SAT_SMT"); - doneProps.put(prop.getName(),result); + doneProps.put(prop.getName(),result,"PARTIAL_ORDER EXPLICIT LTSMIN SAT_SMT"); } private void compilePINS(long timeout) throws IOException, TimeoutException, InterruptedException { From ef09eb1c626acd68be3d178d36353563eb8a1013 Mon Sep 17 00:00:00 2001 From: Yann Thierry-Mieg Date: Thu, 25 Feb 2021 16:23:03 +0100 Subject: [PATCH 06/43] small additional case for simplified bounds properties --- .../src/fr/lip6/move/gal/application/ReachabilitySolver.java | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/ReachabilitySolver.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/ReachabilitySolver.java index 04e0a3d825..b3f58f5adf 100644 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/ReachabilitySolver.java +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/ReachabilitySolver.java @@ -9,6 +9,7 @@ import fr.lip6.move.gal.mcc.properties.DoneProperties; import fr.lip6.move.gal.structural.DeadlockFound; import fr.lip6.move.gal.structural.NoDeadlockExists; +import fr.lip6.move.gal.structural.PropertyType; import fr.lip6.move.gal.structural.RandomExplorer; import fr.lip6.move.gal.structural.SparsePetriNet; import fr.lip6.move.gal.structural.StructuralReduction; @@ -24,6 +25,9 @@ public static void checkInInitial(MccTranslator reader, DoneProperties doneProps if (prop.getBody().getOp() == Op.BOOLCONST) { doneProps.put(prop.getName(),prop.getBody().getValue()==1,"TOPOLOGICAL INITIAL_STATE"); reader.getSPN().getProperties().remove(prop); + } else if (prop.getType() == PropertyType.BOUNDS && prop.getBody().getOp()== Op.CONST) { + doneProps.put(prop.getName(),prop.getBody().getValue(),"TOPOLOGICAL INITIAL_STATE"); + reader.getSPN().getProperties().remove(prop); } } } From ecb616d582a1c02d6d7de5485f7bba20f31b102b Mon Sep 17 00:00:00 2001 From: Yann Thierry-Mieg Date: Thu, 25 Feb 2021 16:24:21 +0100 Subject: [PATCH 07/43] A first try at a dedicated UpperBounds SMT/RandomWalk procedure A lot of copy-pasta in this commit, and incomplete procedures. --- .../gal/application/UpperBoundsSolver.java | 411 ++++++++++++++++++ .../lip6/move/gal/gal2smt/DeadlockTester.java | 55 +++ 2 files changed, 466 insertions(+) create mode 100644 pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/UpperBoundsSolver.java 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 new file mode 100644 index 0000000000..3bc7fc9595 --- /dev/null +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/UpperBoundsSolver.java @@ -0,0 +1,411 @@ +package fr.lip6.move.gal.application; + +import java.util.ArrayList; +import java.util.BitSet; +import java.util.List; + +import android.util.SparseIntArray; +import fr.lip6.move.gal.gal2smt.DeadlockTester; +import fr.lip6.move.gal.mcc.properties.DoneProperties; +import fr.lip6.move.gal.structural.DeadlockFound; +import fr.lip6.move.gal.structural.NoDeadlockExists; +import fr.lip6.move.gal.structural.PropertyType; +import fr.lip6.move.gal.structural.RandomExplorer; +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.BinOp; +import fr.lip6.move.gal.structural.expr.Expression; +import fr.lip6.move.gal.structural.expr.Op; + +public class UpperBoundsSolver { + + public static void checkInInitial(MccTranslator reader, DoneProperties doneProps) { + for (fr.lip6.move.gal.structural.Property prop : new ArrayList<>(reader.getSPN().getProperties())) { + if (prop.getBody().getOp() == Op.BOOLCONST) { + doneProps.put(prop.getName(),prop.getBody().getValue()==1,"TOPOLOGICAL INITIAL_STATE"); + reader.getSPN().getProperties().remove(prop); + } + } + } + + public static void applyReductions(MccTranslator reader, DoneProperties doneProps, String solverPath, boolean isSafe) { + int iter; + int iterations =0; + boolean doneAtoms = false; + boolean doneSums = false; + do { + iter =0; + SparsePetriNet spn = reader.getSPN(); + + StructuralReduction sr = new StructuralReduction(spn); + + // need to protect some variables + List tocheckIndexes = new ArrayList<>(); + List tocheck = new ArrayList<>(spn.getProperties().size()); + computeToCheck(spn, tocheckIndexes, tocheck); + + List maxStruct = new ArrayList<>(tocheckIndexes.size()); + List maxSeen = new ArrayList<>(tocheckIndexes.size()); + { + SparseIntArray m0 = new SparseIntArray(sr.getMarks()); + for (Expression tc:tocheck) { + maxSeen.add(tc.eval(m0)); + maxStruct.add(-1); + } + } + + RandomExplorer re = new RandomExplorer(sr); + int steps = 1000000; // 1 million + if (iterations == 0 && iter==0) { + steps = 10000; // be more moderate on first run : 100k + } + if (randomCheckReachability(re, tocheck, spn, doneProps,steps,maxSeen,maxStruct) >0) + iter++; + + if (reader.getSPN().getProperties().isEmpty()) + break; + + if (solverPath != null) { + List repr = new ArrayList<>(); + List paths = DeadlockTester.findStructuralMaxWithSMT(tocheck, maxSeen, maxStruct, sr, solverPath, isSafe, repr, iterations==0 ? 5:45,true); + + //interpretVerdict(tocheck, spn, doneProps, new int[tocheck.size()], solverPath, maxSeen, maxStruct); + + iter += treatVerdicts(reader.getSPN(), doneProps, tocheck, tocheckIndexes, paths, maxSeen, maxStruct); + + for (int v = paths.size()-1 ; v >= 0 ; v--) { + SparseIntArray parikh = paths.get(v); + if (parikh != null) { + // we have a candidate, try a Parikh satisfaction run. + int sz = 0; + for (int i=0 ; i < parikh.size() ; i++) { + sz += parikh.valueAt(i); + } + if (sz != 0) { + if (Application.DEBUG >= 1) { + System.out.println("SMT solver thinks a reachable witness state is likely to occur in "+sz +" steps."); + SparseIntArray init = new SparseIntArray(); + for (int i=0 ; i < parikh.size() ; i++) { + System.out.print(sr.getTnames().get(parikh.keyAt(i))+"="+ parikh.valueAt(i)+", "); + init = SparseIntArray.sumProd(1, init, - parikh.valueAt(i), sr.getFlowPT().getColumn(parikh.keyAt(i))); + init = SparseIntArray.sumProd(1, init, + parikh.valueAt(i), sr.getFlowTP().getColumn(parikh.keyAt(i))); + } + System.out.println(); + { + System.out.println("This Parikh overall has effect " + init); + SparseIntArray is = new SparseIntArray(sr.getMarks()); + System.out.println("Initial state is " + is); + System.out.println("Reached state is " + SparseIntArray.sumProd(1, is, 1, init)); + } + } + // StringBuilder sb = new StringBuilder(); + // for (int i=0 ; i < parikh.size() ; i++) { + // sb.append(sr.getTnames().get(parikh.keyAt(i))+"="+ parikh.valueAt(i)+", "); + // } + // sb.append(SerializationUtil.getText(reader.getSpec().getProperties().get(v).getBody(),false)); + // //sb.append(tocheck.get(v)); + // Set toHL = new HashSet<>(); + // for (int i=0;i doneProps.containsKey(p.getName()))) + iter++; + + } + + if (spn.getProperties().removeIf(p -> doneProps.containsKey(p.getName()))) + iter++; + if (spn.getProperties().isEmpty()) + break; + + + BitSet support = spn.computeSupport(); + System.out.println("Support contains "+support.cardinality() + " out of " + sr.getPnames().size() + " places. Attempting structural reductions."); + + sr.setProtected(support); + if (applyReductions(sr, reader, ReductionType.SAFETY, solverPath, isSafe,false,iterations==0)) { + iter++; + } else if (iterations>0 && iter==0 /*&& doneSums*/ && applyReductions(sr, reader, ReductionType.SAFETY, solverPath, isSafe,true,false)) { + iter++; + } + // FlowPrinter.drawNet(sr, "Final Model", 1000); + spn.readFrom(sr); + spn.testInInitial(); + spn.removeConstantPlaces(); + spn.simplifyLogic(); + checkInInitial(reader, doneProps); + + if (reader.getSPN().getProperties().isEmpty()) { + return; + } + + if (iter == 0 && !doneAtoms) { + // SerializationUtil.systemToFile(reader.getSpec(), "/tmp/before.gal"); + if (new AtomicReducerSR().strongReductions(solverPath, reader, isSafe, doneProps) > 0) { + checkInInitial(reader, doneProps); + iter++; + } + doneAtoms = true; + // reader.rewriteSums(); + // SerializationUtil.systemToFile(reader.getSpec(), "/tmp/after.gal"); + } + if (reader.getSPN().getProperties().removeIf(p -> doneProps.containsKey(p.getName()))) + iter++; + + + + iterations++; + } while ( (iterations<=1 || iter > 0) && ! reader.getSPN().getProperties().isEmpty()); + + } + + public static void computeToCheck(SparsePetriNet spn, List tocheckIndexes, List tocheck) { + int j=0; + for (fr.lip6.move.gal.structural.Property p : spn.getProperties()) { + if (p.getType() == PropertyType.BOUNDS) { + tocheck.add(p.getBody()); + tocheckIndexes.add(j); + } + j++; + } + } + + static int treatVerdicts(SparsePetriNet sparsePetriNet, DoneProperties doneProps, List tocheck, + List tocheckIndexes, List paths, List maxSeen, List maxStruct) { + return treatVerdicts(sparsePetriNet, doneProps, tocheck, tocheckIndexes, paths, "",maxSeen,maxStruct); + } + + static int treatVerdicts(SparsePetriNet spn, DoneProperties doneProps, List tocheck, + List tocheckIndexes, List paths, String technique, List maxSeen, List maxStruct) { + int seen = 0; + for (int v = paths.size()-1 ; v >= 0 ; v--) { + if (maxSeen.get(v)==maxStruct.get(v)) { + fr.lip6.move.gal.structural.Property prop = spn.getProperties().get(v); + doneProps.put(prop.getName(),maxSeen.get(v),"TOPOLOGICAL SAT_SMT RANDOM_WALK"); + tocheck.remove(v); + spn.getProperties().remove(v); + maxSeen.remove(v); + maxStruct.remove(v); + seen++; + } + } + return seen; + +// int iter = 0; +// for (int v = paths.size()-1 ; v >= 0 ; v--) { +// SparseIntArray parikh = paths.get(v); +// if (parikh == null) { +// fr.lip6.move.gal.structural.Property prop = spn.getProperties().get(tocheckIndexes.get(v)); +// if (prop.getBody().getOp() == Op.EF) { +// doneProps.put(prop.getName(),false,"STRUCTURAL_REDUCTION TOPOLOGICAL SAT_SMT "+technique); +// } else { +// // AG +// doneProps.put(prop.getName(),true,"STRUCTURAL_REDUCTION TOPOLOGICAL SAT_SMT "+technique); +// } +// +// tocheck.remove(v); +// tocheckIndexes.remove(v); +// iter++; +// } +// } +// if (spn.getProperties().removeIf(p -> doneProps.containsKey(p.getName()))) +// iter++; +// return iter; + } + + static int randomCheckReachability(RandomExplorer re, List tocheck, SparsePetriNet spn, + DoneProperties doneProps, int steps, List maxSeen, List maxStruct) { + int[] verdicts = re.runRandomReachabilityDetection(steps,tocheck,30,-1,true); + + int seen = interpretVerdict(tocheck, spn, doneProps, verdicts,"RANDOM",maxSeen,maxStruct); +// for (int i=0 ; i < tocheck.size() ; i++) { +// verdicts = re.runRandomReachabilityDetection(steps,tocheck,5,i,true); +// for (int j =0; j <= i ; j++) { +// if (verdicts[j] != 0) +// i--; +// } +// seen += interpretVerdict(tocheck, spn, doneProps, verdicts,"BESTFIRST",maxSeen,maxStruct); +// } + + + +// if (seen == 0) { +// RandomExplorer.WasExhaustive wex = new RandomExplorer.WasExhaustive(); +// verdicts = re.runProbabilisticReachabilityDetection(steps*1000,tocheck,30,-1,false,wex); +// seen += interpretVerdict(tocheck, spn, doneProps, verdicts,"PROBABILISTIC"); +// if (wex.wasExhaustive) { +// wex = new RandomExplorer.WasExhaustive(); +// verdicts = re.runProbabilisticReachabilityDetection(steps*1000,tocheck,30,-1,true,wex); +// seen += interpretVerdict(tocheck, spn, doneProps, verdicts,"EXHAUSTIVE",wex.wasExhaustive); +// } +// } + return seen; + } + + private static int interpretVerdict(List tocheck, SparsePetriNet spn, DoneProperties doneProps, + int[] verdicts, String walkType, List maxSeen, List maxStruct) { + int seen = 0; + for (int v = verdicts.length-1 ; v >= 0 ; v--) { + int cur = verdicts[v]; + maxSeen.set(v,Math.max(maxSeen.get(v), cur)); + if (maxSeen.get(v)==maxStruct.get(v)) { + fr.lip6.move.gal.structural.Property prop = spn.getProperties().get(v); + doneProps.put(prop.getName(),maxSeen.get(v),"TOPOLOGICAL "+walkType+"_WALK"); + tocheck.remove(v); + spn.getProperties().remove(v); + maxSeen.remove(v); + maxStruct.remove(v); + seen++; + } + } + return seen; + } + + static boolean applyReductions(StructuralReduction sr, MccTranslator reader, ReductionType rt, String solverPath, boolean isSafe, boolean withSMT, boolean isFirstTime) + { + try { + boolean cont = false; + int it =0; + int initp = sr.getPnames().size(); + int initt = sr.getTnames().size(); + int total = 0; + do { + System.out.println("Starting structural reductions, iteration "+ it + " : " + sr.getPnames().size() +"/" +initp+ " places, " + sr.getTnames().size()+"/"+initt + " transitions."); + + int reduced = 0; + + // The big one ! apply our set of reduction rules, customized by ReductionType, until convergence. + reduced += sr.reduce(rt); + total+=reduced; + cont = false; + + // Quick test for deadlocks, no more transitions. + if (rt == ReductionType.DEADLOCKS && sr.getTnames().isEmpty()) { + throw new DeadlockFound(); + } + + // Coming mostly from colored models with an arc + from a colored place + // when the net is color safe (unfolded version is 1 safe) all bindings with + // x=y become unfeasible. Removing them makes the net much simpler, no more arc weights !=1, less transitions... + if (isFirstTime && it==0) { + boolean hasReduced = arcValuesTriggerSMTDeadTransitions(sr, solverPath, isSafe); + if (hasReduced) { + cont=true; + total++; + } + } + + // implicit and dead transitions test using SMT + // We pass iteration counter and reduced counter to delay more costly versions with state equation. + if (withSMT && solverPath != null) { + boolean hasReduced = applySMTBasedReductionRules(sr, rt, it, solverPath, isSafe, reduced); + if (hasReduced) { + cont = true; + total++; + } + } + if (!cont && rt == ReductionType.SAFETY && withSMT) { + cont = sr.ruleFreeAgglo(true) > 0; + } + it++; + } while (cont); + System.out.println("Finished structural reductions, in "+ it + " iterations. Remains : " + sr.getPnames().size() +"/" +initp+ " places, " + sr.getTnames().size()+"/"+initt + " transitions."); + return total > 0; + } catch (DeadlockFound|NoDeadlockExists e) { + e.printStackTrace(); + return false; + } + } + + private static boolean applySMTBasedReductionRules(StructuralReduction sr, ReductionType rt, int iteration, + String solverPath, boolean isSafe, int reduced) throws NoDeadlockExists { + boolean hasReduced = false; + boolean useStateEq = false; + if (reduced > 0 || iteration ==0) { + long t = System.currentTimeMillis(); + // go for more reductions ? + + List implicitPlaces = DeadlockTester.testImplicitWithSMT(sr, solverPath, isSafe, false); + if (!implicitPlaces.isEmpty()) { + sr.dropPlaces(implicitPlaces,false,"Implicit Places With SMT (invariants only)"); + sr.ruleReduceTrans(rt); + hasReduced = true; + } else if (sr.getPnames().size() <= 10000 && sr.getTnames().size() < 10000){ + // limit to 20 k variables for SMT solver with parikh constraints + useStateEq = true; + // with state equation can we solve more ? + implicitPlaces = DeadlockTester.testImplicitWithSMT(sr, solverPath, isSafe, true); + if (!implicitPlaces.isEmpty()) { + sr.dropPlaces(implicitPlaces,false,"Implicit Places With SMT (with state equation)"); + sr.ruleReduceTrans(rt); + reduced += implicitPlaces.size(); + hasReduced = true; + } + } + System.out.println("Implicit Place search using SMT "+ (useStateEq?"with State Equation":"only with invariants") +" took "+ (System.currentTimeMillis() -t) +" ms to find "+implicitPlaces.size()+ " implicit places."); + } + + if (reduced == 0 || iteration==0) { + List tokill = DeadlockTester.testImplicitTransitionWithSMT(sr, solverPath); + if (! tokill.isEmpty()) { + System.out.println("Found "+tokill.size()+ " redundant transitions using SMT." ); + } + sr.dropTransitions(tokill,"Redundant Transitions using SMT "+ (useStateEq?"with State Equation":"only with invariants") ); + if (!tokill.isEmpty()) { + System.out.println("Redundant transitions reduction (with SMT) removed "+tokill.size()+" transitions :"+ tokill); + hasReduced = true; + } + } + if (reduced == 0 || iteration==0) { + List tokill = DeadlockTester.testDeadTransitionWithSMT(sr, solverPath, isSafe); + if (! tokill.isEmpty()) { + System.out.println("Found "+tokill.size()+ " dead transitions using SMT." ); + } + sr.dropTransitions(tokill,"Dead Transitions using SMT only with invariants"); + if (!tokill.isEmpty()) { + System.out.println("Dead transitions reduction (with SMT) removed "+tokill.size()+" transitions :"+ tokill); + hasReduced = true; + } + } + return hasReduced; + } + + private static boolean arcValuesTriggerSMTDeadTransitions(StructuralReduction sr, String solverPath, boolean isSafe) { + boolean hasGT1ArcValues = false; + for (int t=0,te=sr.getTnames().size() ; t < te && !hasGT1ArcValues; t++) { + SparseIntArray col = sr.getFlowPT().getColumn(t); + for (int i=0,ie=col.size(); i < ie ; i++) { + if (col.valueAt(i)>1) { + hasGT1ArcValues = true; + break; + } + } + } + + if (hasGT1ArcValues) { + List tokill = DeadlockTester.testDeadTransitionWithSMT(sr, solverPath, isSafe); + if (! tokill.isEmpty()) { + System.out.println("Found "+tokill.size()+ " dead transitions using SMT." ); + } + sr.dropTransitions(tokill,"Dead Transitions using SMT only with invariants"); + if (!tokill.isEmpty()) { + System.out.println("Dead transitions reduction (with SMT) triggered by suspicious arc values removed "+tokill.size()+" transitions :"+ tokill); + return true; + } + } + return false; + } + +} diff --git a/smt/fr.lip6.move.gal.gal2smt/src/fr/lip6/move/gal/gal2smt/DeadlockTester.java b/smt/fr.lip6.move.gal.gal2smt/src/fr/lip6/move/gal/gal2smt/DeadlockTester.java index 2ac6961f15..b2e6246474 100644 --- a/smt/fr.lip6.move.gal.gal2smt/src/fr/lip6/move/gal/gal2smt/DeadlockTester.java +++ b/smt/fr.lip6.move.gal.gal2smt/src/fr/lip6/move/gal/gal2smt/DeadlockTester.java @@ -38,6 +38,7 @@ import fr.lip6.move.gal.structural.InvariantCalculator; import fr.lip6.move.gal.structural.StructuralReduction; import fr.lip6.move.gal.structural.expr.Expression; +import fr.lip6.move.gal.structural.expr.Op; import fr.lip6.move.gal.util.MatrixCol; public class DeadlockTester { @@ -1871,4 +1872,58 @@ private static void addInvariant(StructuralReduction sr, IFactory efactory, Scri script.add(new C_assert(invarexpr)); } + public static List findStructuralMaxWithSMT(List tocheck, List maxSeen, + List maxStruct, StructuralReduction sr, String solverPath, boolean isSafe, List representative, + int timeout, boolean withWitness) { + List verdicts = new ArrayList<>(); + + List tnames = new ArrayList<>(); + MatrixCol sumMatrix = computeReducedFlow(sr, tnames, representative); + + Set invar = InvariantCalculator.computePInvariants(sumMatrix, sr.getPnames()); + //InvariantCalculator.printInvariant(invar, sr.getPnames(), sr.getMarks()); + Set invarT = computeTinvariants(sr, sumMatrix, tnames); + + ReadFeedCache rfc = new ReadFeedCache(); + for (int i=0, e=tocheck.size() ; i < e ; i++) { + try { + SparseIntArray parikh = null; + if (withWitness) + parikh = new SparseIntArray(); + boolean solveWithReals = true; + IExpr smtexpr = Expression.op(Op.GT, tocheck.get(i), Expression.constant(maxSeen.get(i))).accept(new ExprTranslator()); + Script property = new Script(); + property.add(new C_assert(smtexpr)); + String reply = verifyPossible(sr, property, solverPath, isSafe, sumMatrix, tnames, invar, invarT, solveWithReals, parikh, representative,rfc, 3000, timeout); + if ("real".equals(reply)) { + reply = verifyPossible(sr, property, solverPath, isSafe, sumMatrix, tnames, invar, invarT, false, parikh, representative,rfc, 3000, timeout); + } + + if (! "unsat".equals(reply)) { + if (withWitness) + verdicts.add(parikh); + else + verdicts.add(new SparseIntArray()); + + + if (DEBUG>=2 && invarT != null) { + for (SparseIntArray invt: invarT) { + if (SparseIntArray.greaterOrEqual(parikh, invt)) { + System.out.println("reducible !"); + } + } + } + } else { + verdicts.add(null); + maxStruct.set(i, maxSeen.get(i)); + } + } catch (RuntimeException re) { + Logger.getLogger("fr.lip6.move.gal").warning("SMT solver failed with error :" + re + " while checking expression at index " + i); + verdicts.add(new SparseIntArray()); + } + } + + return verdicts ; + } + } From a01d1485ca02ab0fb1d922a94cf1c17bffd4bfd9 Mon Sep 17 00:00:00 2001 From: Yann Thierry-Mieg Date: Thu, 25 Feb 2021 16:24:42 +0100 Subject: [PATCH 08/43] using our new UpperBoundsSolver and related algorithms --- .../lip6/move/gal/application/Application.java | 16 ++++++++++++++-- 1 file changed, 14 insertions(+), 2 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 7d0e6e453b..dbe43d62e7 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 @@ -356,10 +356,22 @@ public Object startNoEx(IApplicationContext context) throws Exception { } checkInInitial(reader.getSpec(), doneProps, isSafe); if (examination.equals("UpperBounds")) { - ReachabilitySolver.applyReductions(reader, doneProps, solverPath, isSafe); - checkInInitial(reader.getSpec(), doneProps, isSafe); + + UpperBoundsSolver.checkInInitial(reader, doneProps); + + UpperBoundsSolver.applyReductions(reader, doneProps, solverPath, isSafe); + + + // checkInInitial(reader.getSpec(), doneProps, isSafe); + + if (doneProps.keySet().containsAll(reader.getSPN().getProperties().stream().map(p->p.getName()).collect(Collectors.toList()))) { + System.out.println("All properties solved without resorting to model-checking."); + return null; + } + } + tryRebuildPNML(pwd, examination, rebuildPNML, reader, doneProps); reader = runMultiITS(pwd, examination, gspnpath, orderHeur, doITS, onlyGal, doHierarchy, useManyOrder, From 13052e0fdaf36c2eda3efe4ca824160bf7bc610b Mon Sep 17 00:00:00 2001 From: Yann Thierry-Mieg Date: Fri, 26 Feb 2021 13:07:25 +0100 Subject: [PATCH 09/43] allow Parikh walk to work for Bounds --- .../lip6/move/gal/structural/RandomExplorer.java | 14 +++++++++----- 1 file changed, 9 insertions(+), 5 deletions(-) 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 941ff1a08b..de20e2900c 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 @@ -123,7 +123,7 @@ public void updateEnabled (SparseIntArray state, int [] enabled, int tfired) { } } } - public int[] runGuidedReachabilityDetection (long nbSteps, SparseIntArray parikhori, List exprs, List repr, int timeout) { + public int[] runGuidedReachabilityDetection (long nbSteps, SparseIntArray parikhori, List exprs, List repr, int timeout, boolean max) { ThreadLocalRandom rand = ThreadLocalRandom.current(); Map> repSet = computeMap(repr); @@ -155,11 +155,15 @@ public int[] runGuidedReachabilityDetection (long nbSteps, SparseIntArray parikh 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):"") ); return verdicts; } - - if (! updateVerdicts(exprs, state, verdicts)) { - System.out.println("Finished Parikh walk after "+ i + " steps, including "+nbresets+ " resets, run visited all " +exprs.size()+ " properties in "+ dur +" ms. (steps per millisecond="+ (i/dur) +" )"+ (DEBUG >=1 ? (" reached state " + state):"") ); - return verdicts; + if (!max) { + if (! updateVerdicts(exprs, state, verdicts)) { + System.out.println("Finished Parikh walk after "+ i + " steps, including "+nbresets+ " resets, run visited all " +exprs.size()+ " properties in "+ dur +" ms. (steps per millisecond="+ (i/dur) +" )"+ (DEBUG >=1 ? (" reached state " + state):"") ); + return verdicts; + } + } else { + updateMaxVerdicts(exprs, state, verdicts); } + if (list[0] == 0){ //System.out.println("Dead end with self loop(s) found at step " + i); nbresets ++; From 35b9206fd313b695701ef330a535d5568f69b6dc Mon Sep 17 00:00:00 2001 From: Yann Thierry-Mieg Date: Fri, 26 Feb 2021 13:07:51 +0100 Subject: [PATCH 10/43] not max/bounds, normal traversal in Reachability --- .../src/fr/lip6/move/gal/application/ReachabilitySolver.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/ReachabilitySolver.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/ReachabilitySolver.java index b3f58f5adf..d8ea5aca5a 100644 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/ReachabilitySolver.java +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/ReachabilitySolver.java @@ -103,7 +103,7 @@ public static void applyReductions(MccTranslator reader, DoneProperties doneProp // } // } // FlowPrinter.drawNet(sr, "Parikh Test :" + sb.toString(),toHL,Collections.emptySet()); - int[] verdicts = re.runGuidedReachabilityDetection(100*sz, parikh, tocheck,repr,30); + int[] verdicts = re.runGuidedReachabilityDetection(100*sz, parikh, tocheck,repr,30,false); interpretVerdict(tocheck, spn, doneProps, verdicts, "PARIKH"); if (tocheck.isEmpty()) { break; From f37c3768b410d8554877d124b8d2cb7732748e8c Mon Sep 17 00:00:00 2001 From: Yann Thierry-Mieg Date: Fri, 26 Feb 2021 13:08:25 +0100 Subject: [PATCH 11/43] Better algorithm, now using Parikh guided walk --- .../gal/application/UpperBoundsSolver.java | 51 +++++++++++-------- 1 file changed, 30 insertions(+), 21 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 3bc7fc9595..2e7d3b729c 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 @@ -34,26 +34,31 @@ public static void applyReductions(MccTranslator reader, DoneProperties doneProp int iterations =0; boolean doneAtoms = false; boolean doneSums = false; + + SparsePetriNet spn = reader.getSPN(); + + // need to protect some variables + List tocheckIndexes = new ArrayList<>(); + List tocheck = new ArrayList<>(spn.getProperties().size()); + computeToCheck(spn, tocheckIndexes, tocheck, doneProps); + + List maxStruct = new ArrayList<>(tocheckIndexes.size()); + List maxSeen = new ArrayList<>(tocheckIndexes.size()); + { + SparseIntArray m0 = new SparseIntArray(spn.getMarks()); + for (Expression tc:tocheck) { + maxSeen.add(tc.eval(m0)); + maxStruct.add(-1); + } + } do { iter =0; - SparsePetriNet spn = reader.getSPN(); - - StructuralReduction sr = new StructuralReduction(spn); - - // need to protect some variables - List tocheckIndexes = new ArrayList<>(); - List tocheck = new ArrayList<>(spn.getProperties().size()); - computeToCheck(spn, tocheckIndexes, tocheck); - - List maxStruct = new ArrayList<>(tocheckIndexes.size()); - List maxSeen = new ArrayList<>(tocheckIndexes.size()); - { - SparseIntArray m0 = new SparseIntArray(sr.getMarks()); - for (Expression tc:tocheck) { - maxSeen.add(tc.eval(m0)); - maxStruct.add(-1); - } + if (iterations != 0) { + spn = reader.getSPN(); + tocheck = new ArrayList<>(spn.getProperties().size()); + computeToCheck(spn, tocheckIndexes, tocheck, doneProps); } + StructuralReduction sr = new StructuralReduction(spn); RandomExplorer re = new RandomExplorer(sr); int steps = 1000000; // 1 million @@ -112,8 +117,11 @@ public static void applyReductions(MccTranslator reader, DoneProperties doneProp // } // } // FlowPrinter.drawNet(sr, "Parikh Test :" + sb.toString(),toHL,Collections.emptySet()); - int[] verdicts = re.runGuidedReachabilityDetection(100*sz, parikh, tocheck,repr,30); - interpretVerdict(tocheck, spn, doneProps, verdicts, "PARIKH",maxSeen,maxStruct); + int[] verdicts = re.runGuidedReachabilityDetection(100*sz, parikh, tocheck,repr,30,true); + int seen = interpretVerdict(tocheck, spn, doneProps, verdicts,"PARIKH",maxSeen,maxStruct); + iter += treatVerdicts(reader.getSPN(), doneProps, tocheck, tocheckIndexes, paths, maxSeen, maxStruct); + + //interpretVerdict(tocheck, spn, doneProps, verdicts, "PARIKH",maxSeen,maxStruct); if (tocheck.isEmpty()) { break; } @@ -171,10 +179,10 @@ public static void applyReductions(MccTranslator reader, DoneProperties doneProp } - public static void computeToCheck(SparsePetriNet spn, List tocheckIndexes, List tocheck) { + public static void computeToCheck(SparsePetriNet spn, List tocheckIndexes, List tocheck, DoneProperties doneProps) { int j=0; for (fr.lip6.move.gal.structural.Property p : spn.getProperties()) { - if (p.getType() == PropertyType.BOUNDS) { + if (! doneProps.containsKey(p.getName()) && p.getType() == PropertyType.BOUNDS) { tocheck.add(p.getBody()); tocheckIndexes.add(j); } @@ -198,6 +206,7 @@ static int treatVerdicts(SparsePetriNet spn, DoneProperties doneProps, List Date: Fri, 26 Feb 2021 14:41:47 +0100 Subject: [PATCH 12/43] make sure we clean done properties --- .../src/fr/lip6/move/gal/application/Application.java | 1 + 1 file changed, 1 insertion(+) 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 dbe43d62e7..74c4922bda 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 @@ -356,6 +356,7 @@ public Object startNoEx(IApplicationContext context) throws Exception { } checkInInitial(reader.getSpec(), doneProps, isSafe); if (examination.equals("UpperBounds")) { + reader.getSPN().getProperties().removeIf(p -> doneProps.containsKey(p.getName())); UpperBoundsSolver.checkInInitial(reader, doneProps); From b88cf8bce70ea015526529e415993ebddc0109c7 Mon Sep 17 00:00:00 2001 From: Yann Thierry-Mieg Date: Fri, 26 Feb 2021 17:41:43 +0100 Subject: [PATCH 13/43] a ICommand to access non SMT standard compliant optimize --- .../src/org/smtlib/command/C_minmax.java | 77 +++++++++++++++++++ 1 file changed, 77 insertions(+) create mode 100644 smt/lip6.smtlib.SMT/src/org/smtlib/command/C_minmax.java diff --git a/smt/lip6.smtlib.SMT/src/org/smtlib/command/C_minmax.java b/smt/lip6.smtlib.SMT/src/org/smtlib/command/C_minmax.java new file mode 100644 index 0000000000..e3df6d7be0 --- /dev/null +++ b/smt/lip6.smtlib.SMT/src/org/smtlib/command/C_minmax.java @@ -0,0 +1,77 @@ +/* + * This file is part of the SMT project. + * Copyright 2010 David R. Cok + * Created August 2010 + */ +package org.smtlib.command; + +import java.io.IOException; + +import org.smtlib.IExpr; +import org.smtlib.IParser.ParserException; +import org.smtlib.IResponse; +import org.smtlib.ISolver; +import org.smtlib.IVisitor; +import org.smtlib.impl.Command; +import org.smtlib.sexpr.Parser; +import org.smtlib.sexpr.Printer; + +/** Implements the assert command */ +public class C_minmax extends Command { + + private boolean isMax; + + /** Constructs a command object given the expression to assert */ + public C_minmax(IExpr expr, boolean isMax) { + formula = expr; + this.isMax = isMax; + } + + /** Returns the asserted formula */ + public IExpr expr() { + return formula; + } + + /** The command name */ + public static final String minCommandName = "minimize"; + public static final String maxCommandName = "maximize"; + + /** The command name */ + public String commandName() { + if (isMax) return maxCommandName; + else return minCommandName; + } + + /** The formula to assert */ + protected IExpr formula; + + /** Writes out the command in S-expression syntax using the given printer */ + public void write(Printer p) throws IOException, IVisitor.VisitorException { + p.writer().append("(" + commandName() + " "); + formula.accept(p); + p.writer().append(")"); + } + + /** Parses the arguments of the command, producing a new command instance */ + static public /*@Nullable*/ C_minmax parse(Parser p) throws IOException, ParserException { + IExpr expr = p.parseExpr(); + if (expr == null) return null; + return new C_minmax(expr, false); + } + + @Override + public IResponse execute(ISolver solver) { + if (isMax) { + return solver.maximize(formula); + } else { + return solver.minimize(formula); + } + } + + @Override + public T accept(IVisitor v) throws IVisitor.VisitorException { + return v.visit(this); + } + + +} From 46d4587a67a144af4bf0ee94d0f6dda611bd39f3 Mon Sep 17 00:00:00 2001 From: Yann Thierry-Mieg Date: Fri, 26 Feb 2021 17:49:03 +0100 Subject: [PATCH 14/43] iterate until max seen does not increase in a full iteration --- .../fr/lip6/move/gal/application/UpperBoundsSolver.java | 9 +++++++-- 1 file changed, 7 insertions(+), 2 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 2e7d3b729c..dadd456fdf 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 @@ -51,6 +51,8 @@ public static void applyReductions(MccTranslator reader, DoneProperties doneProp maxStruct.add(-1); } } + List lastMaxSeen = null; + do { iter =0; if (iterations != 0) { @@ -60,6 +62,8 @@ public static void applyReductions(MccTranslator reader, DoneProperties doneProp } StructuralReduction sr = new StructuralReduction(spn); + + lastMaxSeen = new ArrayList<>(maxSeen); RandomExplorer re = new RandomExplorer(sr); int steps = 1000000; // 1 million if (iterations == 0 && iter==0) { @@ -127,7 +131,8 @@ public static void applyReductions(MccTranslator reader, DoneProperties doneProp } } } - } + } + if (spn.getProperties().removeIf(p -> doneProps.containsKey(p.getName()))) iter++; @@ -175,7 +180,7 @@ public static void applyReductions(MccTranslator reader, DoneProperties doneProp iterations++; - } while ( (iterations<=1 || iter > 0) && ! reader.getSPN().getProperties().isEmpty()); + } while ( (iterations<=1 || iter > 0 || !lastMaxSeen.equals(maxSeen)) && ! reader.getSPN().getProperties().isEmpty()); } From bcced47812c3b9c7e85e1212e292549408d37e23 Mon Sep 17 00:00:00 2001 From: Yann Thierry-Mieg Date: Fri, 26 Feb 2021 17:49:53 +0100 Subject: [PATCH 15/43] Edit "maximize" syntax. Worrisome that it is not the same as minimize. --- smt/lip6.smtlib.SMT/src/org/smtlib/solvers/Solver_z3_4_3.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/smt/lip6.smtlib.SMT/src/org/smtlib/solvers/Solver_z3_4_3.java b/smt/lip6.smtlib.SMT/src/org/smtlib/solvers/Solver_z3_4_3.java index 6ee103a077..a16be8979d 100755 --- a/smt/lip6.smtlib.SMT/src/org/smtlib/solvers/Solver_z3_4_3.java +++ b/smt/lip6.smtlib.SMT/src/org/smtlib/solvers/Solver_z3_4_3.java @@ -661,7 +661,7 @@ public IResponse minimize(IExpr e) { @Override public IResponse maximize(IExpr e) { try { - String r = solverProcess.sendAndListen("(maximize ("+translate(e)+"))\n"); + String r = solverProcess.sendAndListen("(maximize "+translate(e)+")\n"); IResponse response = parseResponse(r); return response; } catch (IOException | VisitorException ex) { From 4d504fa3cdd3e07fec0ef9ea5dc85ed0def59fe5 Mon Sep 17 00:00:00 2001 From: Yann Thierry-Mieg Date: Fri, 26 Feb 2021 17:52:48 +0100 Subject: [PATCH 16/43] Bounds queries now ask for maximizing the solution Also test check-sat after first constraint assertion ; some bounds can be solved already by one-safe constraint. --- .../lip6/move/gal/gal2smt/DeadlockTester.java | 44 +++++++++++++------ 1 file changed, 30 insertions(+), 14 deletions(-) diff --git a/smt/fr.lip6.move.gal.gal2smt/src/fr/lip6/move/gal/gal2smt/DeadlockTester.java b/smt/fr.lip6.move.gal.gal2smt/src/fr/lip6/move/gal/gal2smt/DeadlockTester.java index b2e6246474..7efa107e08 100644 --- a/smt/fr.lip6.move.gal.gal2smt/src/fr/lip6/move/gal/gal2smt/DeadlockTester.java +++ b/smt/fr.lip6.move.gal.gal2smt/src/fr/lip6/move/gal/gal2smt/DeadlockTester.java @@ -29,6 +29,7 @@ import org.smtlib.command.C_declare_fun; import org.smtlib.command.C_declare_sort; import org.smtlib.command.C_define_fun; +import org.smtlib.command.C_minmax; import org.smtlib.ext.C_get_model; import org.smtlib.impl.Script; import org.smtlib.sexpr.ISexpr; @@ -136,9 +137,9 @@ public static List testUnreachableWithSMT(List toche IExpr smtexpr = tocheck.get(i).accept(new ExprTranslator()); Script property = new Script(); property.add(new C_assert(smtexpr)); - String reply = verifyPossible(sr, property, solverPath, isSafe, sumMatrix, tnames, invar, invarT, solveWithReals, parikh, representative,rfc, 3000, timeout); + String reply = verifyPossible(sr, property, solverPath, isSafe, sumMatrix, tnames, invar, invarT, solveWithReals, parikh, representative,rfc, 3000, timeout, null); if ("real".equals(reply)) { - reply = verifyPossible(sr, property, solverPath, isSafe, sumMatrix, tnames, invar, invarT, false, parikh, representative,rfc, 3000, timeout); + reply = verifyPossible(sr, property, solverPath, isSafe, sumMatrix, tnames, invar, invarT, false, parikh, representative,rfc, 3000, timeout, null); } if (! "unsat".equals(reply)) { @@ -182,12 +183,12 @@ Script getScript(StructuralReduction sr, MatrixCol sumMatrix, List repr private static String areDeadlocksPossible(StructuralReduction sr, String solverPath, boolean isSafe, MatrixCol sumMatrix, List tnames, Set invar, Set invarT, boolean solveWithReals, SparseIntArray parikh, List representative) { Script scriptAssertDead = assertNetIsDead(sr); - return verifyPossible(sr, scriptAssertDead, solverPath, isSafe, sumMatrix, tnames, invar, invarT, solveWithReals, parikh, representative, new ReadFeedCache(), 3000, 300); + return verifyPossible(sr, scriptAssertDead, solverPath, isSafe, sumMatrix, tnames, invar, invarT, solveWithReals, parikh, representative, new ReadFeedCache(), 3000, 300, null); } static Configuration smtConf = new SMT().smtConfig; private static String verifyPossible(StructuralReduction sr, Script tocheck, String solverPath, boolean isSafe, - MatrixCol sumMatrix, List tnames, Set invar, Set invarT, boolean solveWithReals, SparseIntArray parikh, List representative, ReadFeedCache readFeedCache, int timeoutQ, int timeoutT) { + MatrixCol sumMatrix, List tnames, Set invar, Set invarT, boolean solveWithReals, SparseIntArray parikh, List representative, ReadFeedCache readFeedCache, int timeoutQ, int timeoutT, ICommand minmax) { long time; lastState = null; lastParikh = null; @@ -200,6 +201,12 @@ private static String verifyPossible(StructuralReduction sr, Script tocheck, Str execAndCheckResult(varScript, solver); // add the script's constraints execAndCheckResult(tocheck, solver); + String textReply = checkSat(solver); + // are we finished ? + if (textReply.equals("unsat")||textReply.equals("unknown")) { + solver.exit(); + return textReply; + } } // STEP 2 : declare and assert invariants @@ -252,16 +259,22 @@ private static String verifyPossible(StructuralReduction sr, Script tocheck, Str } if (textReply.equals("sat") && parikh != null) { if (true && sumMatrix.getColumnCount() < 3000) { - System.out.println("Attempting to minimize the solution found."); long ttime = System.currentTimeMillis(); - List tosum = new ArrayList<>(sumMatrix.getColumnCount()); - IFactory ef = smt.smtConfig.exprFactory; - for (int trindex=0; trindex < sumMatrix.getColumnCount(); trindex++) { - IExpr ss = ef.symbol("t"+trindex); - tosum.add(ss); + if (minmax == null) { + System.out.println("Attempting to minimize the solution found."); + List tosum = new ArrayList<>(sumMatrix.getColumnCount()); + IFactory ef = smt.smtConfig.exprFactory; + for (int trindex=0; trindex < sumMatrix.getColumnCount(); trindex++) { + IExpr ss = ef.symbol("t"+trindex); + tosum.add(ss); + } + solver.minimize(ef.fcn(ef.symbol("+"), tosum)); + } else { + IResponse r = minmax.execute(solver); + if (r.isError()) { + System.err.println("Maximisation of solution failed !"); + } } - solver.minimize(ef.fcn(ef.symbol("+"), tosum)); - textReply = checkSat(solver, false); System.out.println("Minimization took " + (System.currentTimeMillis() - ttime) + " ms."); } @@ -1894,9 +1907,11 @@ public static List findStructuralMaxWithSMT(List toc IExpr smtexpr = Expression.op(Op.GT, tocheck.get(i), Expression.constant(maxSeen.get(i))).accept(new ExprTranslator()); Script property = new Script(); property.add(new C_assert(smtexpr)); - String reply = verifyPossible(sr, property, solverPath, isSafe, sumMatrix, tnames, invar, invarT, solveWithReals, parikh, representative,rfc, 3000, timeout); + // Add a requirement on solver to please max the value of the expression + ICommand minmax = new C_minmax(tocheck.get(i).accept(new ExprTranslator()),true); + String reply = verifyPossible(sr, property, solverPath, isSafe, sumMatrix, tnames, invar, invarT, solveWithReals, parikh, representative,rfc, 3000, timeout,minmax); if ("real".equals(reply)) { - reply = verifyPossible(sr, property, solverPath, isSafe, sumMatrix, tnames, invar, invarT, false, parikh, representative,rfc, 3000, timeout); + reply = verifyPossible(sr, property, solverPath, isSafe, sumMatrix, tnames, invar, invarT, false, parikh, representative,rfc, 3000, timeout, minmax); } if (! "unsat".equals(reply)) { @@ -1919,6 +1934,7 @@ public static List findStructuralMaxWithSMT(List toc } } catch (RuntimeException re) { Logger.getLogger("fr.lip6.move.gal").warning("SMT solver failed with error :" + re + " while checking expression at index " + i); + re.printStackTrace(); verdicts.add(new SparseIntArray()); } } From 87e99581bcd2618b1b4b2c6d03be5d8e89d44518 Mon Sep 17 00:00:00 2001 From: Yann Thierry-Mieg Date: Sat, 27 Feb 2021 17:41:54 +0100 Subject: [PATCH 17/43] this test should be obsolete now --- .../lip6/move/gal/application/MccTranslator.java | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/MccTranslator.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/MccTranslator.java index d8d29d2618..977d769ad8 100644 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/MccTranslator.java +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/MccTranslator.java @@ -185,13 +185,13 @@ public boolean applyOrder(Support supp) { if (rewriteConstantSums()) { Simplifier.simplifyProperties(spec); } - if ( ! spec.getProperties().isEmpty() && - spec.getProperties().stream() - .map(Property::getBody) - .filter(p -> p instanceof BoolProp).map(p -> (BoolProp) p) - .map(BoolProp::getPredicate).allMatch(p -> p instanceof True || p instanceof False)) { - return true; - } +// if ( ! spec.getProperties().isEmpty() && +// spec.getProperties().stream() +// .map(Property::getBody) +// .filter(p -> p instanceof BoolProp).map(p -> (BoolProp) p) +// .map(BoolProp::getPredicate).allMatch(p -> p instanceof True || p instanceof False)) { +// return true; +// } if (done) { simplifiedVars.addAll(GALRewriter.flatten(spec, withSeparation)); } From 747807f1ce62df9668f88b8f342f6474f65eac55 Mon Sep 17 00:00:00 2001 From: Yann Thierry-Mieg Date: Sat, 27 Feb 2021 17:42:31 +0100 Subject: [PATCH 18/43] make sure we use the reduced model in UpperBounds examination --- .../src/fr/lip6/move/gal/application/Application.java | 1 + 1 file changed, 1 insertion(+) 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 74c4922bda..82a73168b6 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 @@ -369,6 +369,7 @@ public Object startNoEx(IApplicationContext context) throws Exception { System.out.println("All properties solved without resorting to model-checking."); return null; } + reader.rebuildSpecification(doneProps); } From 0c21b11b08dd24ad62e54cd32e46b45764e85cfe Mon Sep 17 00:00:00 2001 From: Yann Thierry-Mieg Date: Sat, 27 Feb 2021 18:45:56 +0100 Subject: [PATCH 19/43] make sure we also copy the spn --- .../src/fr/lip6/move/gal/application/MccTranslator.java | 1 + 1 file changed, 1 insertion(+) diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/MccTranslator.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/MccTranslator.java index 977d769ad8..f0d668feb6 100644 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/MccTranslator.java +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/MccTranslator.java @@ -483,6 +483,7 @@ public MccTranslator copy() { copy.simplifiedVars = new Support(simplifiedVars); copy.spec = EcoreUtil.copy(spec); copy.useLouvain = useLouvain; + copy.spn = new SparsePetriNet(spn); return copy ; } From 92bf38bc5e9ff9a3db2ac11325cb829ecf6b0ae3 Mon Sep 17 00:00:00 2001 From: Yann Thierry-Mieg Date: Sat, 27 Feb 2021 18:46:33 +0100 Subject: [PATCH 20/43] deal with Best-first logic for Bounds exploration --- .../src/fr/lip6/move/gal/structural/RandomExplorer.java | 8 ++++---- .../src/fr/lip6/move/gal/structural/expr/NaryOp.java | 5 +++++ .../src/fr/lip6/move/gal/structural/expr/VarRef.java | 3 +++ 3 files changed, 12 insertions(+), 4 deletions(-) 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 de20e2900c..f4d792789e 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 @@ -411,18 +411,18 @@ public int[] runRandomReachabilityDetection (long nbSteps, List expr } } else { // heuristically follow a successor with "Best-first search" - int minDist = Integer.MAX_VALUE; + int minDist = max ? 0 :Integer.MAX_VALUE; List mini = new ArrayList<>(); List bestSucc = new ArrayList<>(); for (int ti = 1 ; ti-1 < list[0] && i < nbSteps; ti++) { SparseIntArray succ = fire(list[ti],state); - int distance = exprs.get(bestFirst).evalDistance(succ, false); - if (distance < minDist) { + int distance = exprs.get(bestFirst).evalDistance(succ, false); + if ( (!max && distance < minDist) || (max && distance > minDist)) { mini.clear(); bestSucc.clear(); minDist = distance; } - if (distance <= minDist) { + if ((!max && distance <= minDist) || (max && distance >= minDist)) { mini.add(list[ti]); bestSucc.add(succ); } diff --git a/fr.lip6.move.gal.structural/src/fr/lip6/move/gal/structural/expr/NaryOp.java b/fr.lip6.move.gal.structural/src/fr/lip6/move/gal/structural/expr/NaryOp.java index 794dd1a4ba..acade2b09d 100644 --- a/fr.lip6.move.gal.structural/src/fr/lip6/move/gal/structural/expr/NaryOp.java +++ b/fr.lip6.move.gal.structural/src/fr/lip6/move/gal/structural/expr/NaryOp.java @@ -85,6 +85,11 @@ public int evalDistance(SparseIntArray state, boolean isNeg) { } return min; } + case ADD: + { + //BOUNDS only + return eval(state); + } default: } } else { diff --git a/fr.lip6.move.gal.structural/src/fr/lip6/move/gal/structural/expr/VarRef.java b/fr.lip6.move.gal.structural/src/fr/lip6/move/gal/structural/expr/VarRef.java index 22ffa7780e..49c813af68 100644 --- a/fr.lip6.move.gal.structural/src/fr/lip6/move/gal/structural/expr/VarRef.java +++ b/fr.lip6.move.gal.structural/src/fr/lip6/move/gal/structural/expr/VarRef.java @@ -31,6 +31,9 @@ public String toString() { @Override public int evalDistance(SparseIntArray state, boolean isNeg) { + if (!isNeg) { + return eval(state); + } throw new UnsupportedOperationException(); } From 2536acaed644a0e87ac7fcdda3a2efc7fcb19832 Mon Sep 17 00:00:00 2001 From: Yann Thierry-Mieg Date: Sat, 27 Feb 2021 18:49:35 +0100 Subject: [PATCH 21/43] add a struct bound for safe nets, rule to kill feeders, BestFirst So 3 patches in one commit * Safe nets => we place an a priori structural bound of 1 on single place references. Hastens conclusions a bit in first iteration. * Rule : single place bound query, place is one safe, kill transitions feeding from it. * Use the now working Best-first strategy for each bound. --- .../gal/application/UpperBoundsSolver.java | 29 +++++++++++++------ 1 file changed, 20 insertions(+), 9 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 dadd456fdf..5fafedc887 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 @@ -48,7 +48,11 @@ public static void applyReductions(MccTranslator reader, DoneProperties doneProp SparseIntArray m0 = new SparseIntArray(spn.getMarks()); for (Expression tc:tocheck) { maxSeen.add(tc.eval(m0)); - maxStruct.add(-1); + if (isSafe && tc.getOp() == Op.PLACEREF) { + maxStruct.add(1); + } else { + maxStruct.add(-1); + } } } List lastMaxSeen = null; @@ -148,6 +152,16 @@ public static void applyReductions(MccTranslator reader, DoneProperties doneProp System.out.println("Support contains "+support.cardinality() + " out of " + sr.getPnames().size() + " places. Attempting structural reductions."); sr.setProtected(support); + + if (isSafe && tocheck.size() == 1 && support.cardinality()==1) { + int pid = support.nextSetBit(0); + List tfeed = new ArrayList<>(sr.getFlowPT().getColumn(pid).size()); + for (int tid : sr.getFlowPT().getColumn(pid).copyKeys()) { + tfeed.add(tid); + } + sr.dropTransitions(tfeed , true,"Remove Feeders"); + } + if (applyReductions(sr, reader, ReductionType.SAFETY, solverPath, isSafe,false,iterations==0)) { iter++; } else if (iterations>0 && iter==0 /*&& doneSums*/ && applyReductions(sr, reader, ReductionType.SAFETY, solverPath, isSafe,true,false)) { @@ -244,14 +258,11 @@ static int randomCheckReachability(RandomExplorer re, List tocheck, int[] verdicts = re.runRandomReachabilityDetection(steps,tocheck,30,-1,true); int seen = interpretVerdict(tocheck, spn, doneProps, verdicts,"RANDOM",maxSeen,maxStruct); -// for (int i=0 ; i < tocheck.size() ; i++) { -// verdicts = re.runRandomReachabilityDetection(steps,tocheck,5,i,true); -// for (int j =0; j <= i ; j++) { -// if (verdicts[j] != 0) -// i--; -// } -// seen += interpretVerdict(tocheck, spn, doneProps, verdicts,"BESTFIRST",maxSeen,maxStruct); -// } + for (int i=0 ; i < tocheck.size() ; i++) { + verdicts = re.runRandomReachabilityDetection(steps,tocheck,5,i,true); + + seen += interpretVerdict(tocheck, spn, doneProps, verdicts,"BESTFIRST",maxSeen,maxStruct); + } From 4d5f738ef45cff400e486bdb8a72c05f8b372bfd Mon Sep 17 00:00:00 2001 From: Yann Thierry-Mieg Date: Sat, 27 Feb 2021 18:51:09 +0100 Subject: [PATCH 22/43] WIP : add property specific reduction for bounds. --- .../fr/lip6/move/gal/application/Application.java | 15 ++++++++++++++- 1 file changed, 14 insertions(+), 1 deletion(-) 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 82a73168b6..dd1019197e 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 @@ -362,12 +362,25 @@ public Object startNoEx(IApplicationContext context) throws Exception { UpperBoundsSolver.applyReductions(reader, doneProps, solverPath, isSafe); - + reader.getSPN().getProperties().removeIf(p -> doneProps.containsKey(p.getName())); // checkInInitial(reader.getSpec(), doneProps, isSafe); if (doneProps.keySet().containsAll(reader.getSPN().getProperties().stream().map(p->p.getName()).collect(Collectors.toList()))) { System.out.println("All properties solved without resorting to model-checking."); return null; + } else { + for (int pid = 0 ; pid < reader.getSPN().getProperties().size() ; pid++) { + long time = System.currentTimeMillis(); + MccTranslator r2 = reader.copy(); + fr.lip6.move.gal.structural.Property p = r2.getSPN().getProperties().get(pid); + 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); + System.out.println("Ending property specific reduction for "+p.getName()+" in "+ (time -System.currentTimeMillis())+" ms."); + } + reader.getSPN().getProperties().removeIf(p -> doneProps.containsKey(p.getName())); } reader.rebuildSpecification(doneProps); From c47d8bcbcfba8d3ecdcdc9317607e7de68e9b75f Mon Sep 17 00:00:00 2001 From: Yann Thierry-Mieg Date: Sun, 28 Feb 2021 17:29:43 +0100 Subject: [PATCH 23/43] typo neg sign --- .../src/fr/lip6/move/gal/application/Application.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/Application.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/Application.java index dd1019197e..b3b4a8f0e7 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 @@ -378,7 +378,7 @@ public Object startNoEx(IApplicationContext context) throws Exception { r2.getSPN().getProperties().add(p); UpperBoundsSolver.checkInInitial(r2, doneProps); UpperBoundsSolver.applyReductions(r2, doneProps, solverPath, isSafe); - System.out.println("Ending property specific reduction for "+p.getName()+" in "+ (time -System.currentTimeMillis())+" ms."); + System.out.println("Ending property specific reduction for "+p.getName()+" in "+ (System.currentTimeMillis()-time)+" ms."); } reader.getSPN().getProperties().removeIf(p -> doneProps.containsKey(p.getName())); } From b4401dcec8f61e465290cbf8fb0ed5b4822d190a Mon Sep 17 00:00:00 2001 From: Yann Thierry-Mieg Date: Sun, 28 Feb 2021 17:32:01 +0100 Subject: [PATCH 24/43] Patch feeder rule, drop AtomicSR * we need tFlowPT not flowPT => (transpose) * simpler logic condition on main loop * atomicSR should not help on bounds --- .../gal/application/UpperBoundsSolver.java | 28 ++++++++----------- 1 file changed, 11 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 5fafedc887..02f3e12a7a 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 @@ -57,12 +57,15 @@ public static void applyReductions(MccTranslator reader, DoneProperties doneProp } List lastMaxSeen = null; + boolean first = true; do { iter =0; - if (iterations != 0) { + if (! first) { spn = reader.getSPN(); tocheck = new ArrayList<>(spn.getProperties().size()); computeToCheck(spn, tocheckIndexes, tocheck, doneProps); + } else { + first = false; } StructuralReduction sr = new StructuralReduction(spn); @@ -156,10 +159,12 @@ public static void applyReductions(MccTranslator reader, DoneProperties doneProp if (isSafe && tocheck.size() == 1 && support.cardinality()==1) { int pid = support.nextSetBit(0); List tfeed = new ArrayList<>(sr.getFlowPT().getColumn(pid).size()); - for (int tid : sr.getFlowPT().getColumn(pid).copyKeys()) { - tfeed.add(tid); - } - sr.dropTransitions(tfeed , true,"Remove Feeders"); + SparseIntArray fpt = sr.getFlowPT().transpose().getColumn(pid); + for (int i = fpt.size() - 1 ; i >= 0 ; i--) { + tfeed.add(fpt.keyAt(i)); + } + if (!tfeed.isEmpty()) + sr.dropTransitions(tfeed , true,"Remove Feeders"); } if (applyReductions(sr, reader, ReductionType.SAFETY, solverPath, isSafe,false,iterations==0)) { @@ -177,20 +182,9 @@ public static void applyReductions(MccTranslator reader, DoneProperties doneProp if (reader.getSPN().getProperties().isEmpty()) { return; } - - if (iter == 0 && !doneAtoms) { - // SerializationUtil.systemToFile(reader.getSpec(), "/tmp/before.gal"); - if (new AtomicReducerSR().strongReductions(solverPath, reader, isSafe, doneProps) > 0) { - checkInInitial(reader, doneProps); - iter++; - } - doneAtoms = true; - // reader.rewriteSums(); - // SerializationUtil.systemToFile(reader.getSpec(), "/tmp/after.gal"); - } + if (reader.getSPN().getProperties().removeIf(p -> doneProps.containsKey(p.getName()))) iter++; - iterations++; From a760113d5a72bc149f3c983c5a5220fcd66a410a Mon Sep 17 00:00:00 2001 From: Yann Thierry-Mieg Date: Sun, 28 Feb 2021 17:32:51 +0100 Subject: [PATCH 25/43] document an idea on relaxing "future fusion" rule --- .../src/fr/lip6/move/gal/structural/StructuralReduction.java | 3 +++ 1 file changed, 3 insertions(+) diff --git a/fr.lip6.move.gal.structural/src/fr/lip6/move/gal/structural/StructuralReduction.java b/fr.lip6.move.gal.structural/src/fr/lip6/move/gal/structural/StructuralReduction.java index cf66e08d27..2df6bec845 100644 --- a/fr.lip6.move.gal.structural/src/fr/lip6/move/gal/structural/StructuralReduction.java +++ b/fr.lip6.move.gal.structural/src/fr/lip6/move/gal/structural/StructuralReduction.java @@ -1831,6 +1831,9 @@ private int ruleFusePlaceByFuture() { for (int tj = 0; tj < pjouts.size() ; tj++) { int indtj = pjouts.keyAt(tj); + + // TODO : possibly this test could be removed, if the "equal up to perm" criterion matches, + // in the result we must now take two tokens from the fused place however. if (indti == indtj) { break; } From 9bcef94b975cd4ea4fd741cc3ff8476bc7a06720 Mon Sep 17 00:00:00 2001 From: Yann Thierry-Mieg Date: Sun, 28 Feb 2021 18:37:54 +0100 Subject: [PATCH 26/43] upperbounds and CTL now are just different cases --- .../fr/lip6/move/gal/application/Application.java | 12 +++++++----- 1 file changed, 7 insertions(+), 5 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 b3b4a8f0e7..c72a66e623 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 @@ -341,12 +341,14 @@ public Object startNoEx(IApplicationContext context) throws Exception { // are we going for CTL ? only ITSRunner answers this. if (examination.startsWith("CTL") || examination.equals("UpperBounds")) { - new AtomicReducerSR().strongReductions(solverPath, reader, isSafe, doneProps); - reader.getSPN().simplifyLogic(); - reader.rebuildSpecification(doneProps); + if (examination.startsWith("CTL")) { - + new AtomicReducerSR().strongReductions(solverPath, reader, isSafe, doneProps); + reader.getSPN().simplifyLogic(); + reader.rebuildSpecification(doneProps); + checkInInitial(reader.getSpec(), doneProps, isSafe); reader.flattenSpec(false); + checkInInitial(reader.getSpec(), doneProps, isSafe); // new AtomicReducer().strongReductions(solverPath, reader, isSafe, doneProps); // Simplifier.simplify(reader.getSpec()); @@ -354,8 +356,8 @@ public Object startNoEx(IApplicationContext context) throws Exception { // TODO: make CTL syntax match the normal predicate syntax in ITS tools //reader.removeAdditionProperties(); } - checkInInitial(reader.getSpec(), doneProps, isSafe); if (examination.equals("UpperBounds")) { + reader.getSPN().simplifyLogic(); reader.getSPN().getProperties().removeIf(p -> doneProps.containsKey(p.getName())); UpperBoundsSolver.checkInInitial(reader, doneProps); From 73ae1ad4d5daa5a5cc5f3e1e8145d4bd1c818e02 Mon Sep 17 00:00:00 2001 From: Yann Thierry-Mieg Date: Sun, 28 Feb 2021 18:38:59 +0100 Subject: [PATCH 27/43] a new rule usable in the context of Bounds study. --- .../gal/structural/StructuralReduction.java | 53 +++++++++++++++++++ .../gal/application/UpperBoundsSolver.java | 5 ++ 2 files changed, 58 insertions(+) diff --git a/fr.lip6.move.gal.structural/src/fr/lip6/move/gal/structural/StructuralReduction.java b/fr.lip6.move.gal.structural/src/fr/lip6/move/gal/structural/StructuralReduction.java index 2df6bec845..6ed2ebfc7c 100644 --- a/fr.lip6.move.gal.structural/src/fr/lip6/move/gal/structural/StructuralReduction.java +++ b/fr.lip6.move.gal.structural/src/fr/lip6/move/gal/structural/StructuralReduction.java @@ -230,6 +230,59 @@ public int reduce (ReductionType rt) throws NoDeadlockExists, DeadlockFound { } + public int ruleRedundantCompositionsBounds() { + if (tnames.size() > 20000) { + // quadratic |T| => 10^8 hurts too much + return 0; + } + Set todel = new HashSet<>(); + // map effect to list of transition indexes having this effect + Map> effects = new HashMap<>(); + for (int tid=0, e=tnames.size() ; tid < e ; tid++) { + final int t =tid; + // we want positive effects + SparseIntArray effect = SparseIntArray.sumProd(-1, flowPT.getColumn(tid),1,flowTP.getColumn(tid)); + SparseIntArray posEffect = new SparseIntArray(); + for (int i=0,ie=effect.size(); i < ie ; i++) { + int v = effect.valueAt(i); + if (v > 0) { + posEffect.append(effect.keyAt(i), v); + } + } + effects.compute(posEffect, (k,v) -> { + if (v==null) { + v = new ArrayList<>(); + v.add(t); + } else { + for (int to : v) { + if (SparseIntArray.greaterOrEqual(flowPT.getColumn(t), flowPT.getColumn(to))) { + todel.add(t); + Set tset = new HashSet<>(); + tset.add(t); + tset.add(to); + FlowPrinter.drawNet(this,"Discarding transition "+tnames.get(t)+ " with rule Dominated (bounds)", new HashSet<>(), tset ); + } else if (SparseIntArray.greaterOrEqual(flowPT.getColumn(to), flowPT.getColumn(t))) { + todel.add(to); + Set tset = new HashSet<>(); + tset.add(t); + tset.add(to); + FlowPrinter.drawNet(this,"Discarding transition "+tnames.get(to)+ " with rule Dominated (bounds)", new HashSet<>(), tset ); + } + } + v.add(t); + v.removeAll(todel); + } + return v; + }); + } + if (! todel.isEmpty()) { + dropTransitions(new ArrayList<>(todel),"Dominated transitions (bounds rule)."); + System.out.println("Dominated transitions for bounds rules discarded "+todel.size()+ " transitions"); + } + return todel.size(); + } + + /** * Detects and destroys transitions t such that exists t1,t2 such that * t1 fireable => t1.t2 is fireable for any state 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 02f3e12a7a..4c67fbc0e9 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 @@ -172,6 +172,11 @@ public static void applyReductions(MccTranslator reader, DoneProperties doneProp } else if (iterations>0 && iter==0 /*&& doneSums*/ && applyReductions(sr, reader, ReductionType.SAFETY, solverPath, isSafe,true,false)) { iter++; } + int reds= sr.ruleRedundantCompositionsBounds(); + if (reds > 0) { + iter++; + } + // FlowPrinter.drawNet(sr, "Final Model", 1000); spn.readFrom(sr); spn.testInInitial(); From ee76ec8534781b500f7808c71c61c6f8d67da3c4 Mon Sep 17 00:00:00 2001 From: Yann Thierry-Mieg Date: Mon, 1 Mar 2021 15:59:44 +0100 Subject: [PATCH 28/43] prefer "".equals(str) to str.equals("") --- .../src/fr/lip6/move/gal/application/Application.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/Application.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/Application.java index c72a66e623..13f40c21e3 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 @@ -269,7 +269,7 @@ public Object startNoEx(IApplicationContext context) throws Exception { } - if (examination.equals("StableMarking")) { + if ("StableMarking".equals(examination)) { GlobalPropertySolver gps = new GlobalPropertySolver(solverPath); boolean b = gps.solveProperty(examination, reader); From cccee3d651280a2b820570d9d6e8b5dd2942f447 Mon Sep 17 00:00:00 2001 From: Yann Thierry-Mieg Date: Mon, 1 Mar 2021 16:02:15 +0100 Subject: [PATCH 29/43] use invariants "manually", we are better than SMT solver at this Delegating these computations to the solver means it might timeout, so especially for hard/large models, this makes a big difference. TODO : we recompute invariants twice now in the loop, once for SMT and once here, we should store them instead. TODO : refactor it to separate function --- .../gal/application/UpperBoundsSolver.java | 164 +++++++++++++++++- 1 file changed, 159 insertions(+), 5 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 4c67fbc0e9..ac40909582 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 @@ -1,22 +1,26 @@ package fr.lip6.move.gal.application; import java.util.ArrayList; +import java.util.Arrays; import java.util.BitSet; import java.util.List; +import java.util.Set; + import android.util.SparseIntArray; import fr.lip6.move.gal.gal2smt.DeadlockTester; import fr.lip6.move.gal.mcc.properties.DoneProperties; import fr.lip6.move.gal.structural.DeadlockFound; +import fr.lip6.move.gal.structural.InvariantCalculator; import fr.lip6.move.gal.structural.NoDeadlockExists; import fr.lip6.move.gal.structural.PropertyType; import fr.lip6.move.gal.structural.RandomExplorer; 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.BinOp; import fr.lip6.move.gal.structural.expr.Expression; import fr.lip6.move.gal.structural.expr.Op; +import fr.lip6.move.gal.util.MatrixCol; public class UpperBoundsSolver { @@ -70,6 +74,156 @@ public static void applyReductions(MccTranslator reader, DoneProperties doneProp StructuralReduction sr = new StructuralReduction(spn); + { + // try to set a max bound on variables using invariants + + // effect matrix + MatrixCol sumMatrix = MatrixCol.sumProd(-1, spn.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 + Arrays.fill(limits, -1); + // split invariants in positive semi-flows and generalized flows (with neg coeffs) + List posinv = new ArrayList(); + List geninv = new ArrayList(); + + // do the split + for (SparseIntArray invariant : invar) { + boolean hasNeg = false; + for (int i=0; i < invariant.size() ; i++) { + if (invariant.valueAt(i) < 0) { + hasNeg = true; + break; + } + } + if (! hasNeg) { + posinv.add(invariant); + } else { + geninv.add(invariant); + } + } + + // start with positive semi flows + for (SparseIntArray invariant : posinv) { + + // ok so we have an invariant : a0 * p0 + a1 * p1 ...= K + // at best all variables are zero except one, in that case pi = K / ai (rounded down) + // e.g. 2*p0 + p1 = 4 => p0 <= 2 ; p1 <= 4 + // e.g. 2*p0 + p1 = 5 => p0 <= 2 ; p1 <= 5 + + // compute K + int sum = 0; + for (int i = 0 ; i < invariant.size() ; i++) { + int v = invariant.keyAt(i); + int val = invariant.valueAt(i); + sum += sr.getMarks().get(v) * val; + } + // iterate elements and set bound + for (int i = 0 ; i < invariant.size() ; i++) { + int v = invariant.keyAt(i); + int val = invariant.valueAt(i); + int bound = sum / val ; + limits[v] = Math.min(limits[v]==-1?Integer.MAX_VALUE:limits[v], bound); + } + } + + // now use these bounds to have a (pessimistic) opinion on generalized flows + for (SparseIntArray invariant : posinv) { + + // ok so we have an invariant : a0 * p0 - a1 * p1 + ...= K + // Now if all negative coefficient elements are actually bounded, we can conservatively use this bound + // e.g. p0 - p1 = K knowing that p1 <= K1 => p0 - K1 <= K => p0 <= K + K1 + // in other words, move all negative elements to the right, update K pessimistically + // Similarly, if the positive elements are all bounded we can deduce + // p0 - p1 = K knowing that p0 <= K0 => p0 - K = p1 => p1 <= K0 - K + + // true if + boolean boundPosExists = true; + boolean boundNegExists = true; + + // compute K and whether we have bounds on one term + int tsum = 0; + int pbound = 0; + int nbound = 0; + for (int i = 0 ; i < invariant.size() ; i++) { + int v = invariant.keyAt(i); + int val = invariant.valueAt(i); + tsum += sr.getMarks().get(v) * val; + if (val < 0 && limits[v]==-1) { + boundNegExists = false; + } else if (val > 0 && limits[v]==-1) { + boundPosExists = false; + } else if (val < 0) { + nbound -= val * limits[v]; + } else if (val > 0) { + pbound += val * limits[v]; + } + } + + // apply any bounds found + if (boundPosExists || boundNegExists) { + // p0 - p1 = K knowing that p0 <= K0 => p0 - K = p1 => p1 <= K0 - K + int psum = pbound - tsum; + // e.g. p0 - p1 = K knowing that p1 <= K1 => p0 - K1 <= K => p0 <= K + K1 + int nsum = nbound + tsum ; + + // iterate elements and set bound + for (int i = 0 ; i < invariant.size() ; i++) { + int v = invariant.keyAt(i); + int val = invariant.valueAt(i); + if (val < 0 && boundPosExists) { + int bound = -nsum / val ; + limits[v] = Math.min(limits[v]==-1?Integer.MAX_VALUE:limits[v], bound); + } else if (val > 0 && boundNegExists){ + int bound = psum / val ; + limits[v] = Math.min(limits[v]==-1?Integer.MAX_VALUE:limits[v], bound); + } + } + } + } + System.out.println("Managed to find structural bounds :" + Arrays.toString(limits)); + System.out.println("Current structural bounds on expressions : " + maxStruct); + + for (int propid = 0 ; propid < tocheck.size() ; propid++) { + Expression tc = tocheck.get(propid); + if (tc.getOp() == Op.PLACEREF) { + if (limits[tc.getValue()]!=-1) { + maxStruct.set(propid, Math.min(maxStruct.get(propid)==-1?Integer.MAX_VALUE:maxStruct.get(propid), limits[tc.getValue()])); + } + } else if (tc.getOp() == Op.ADD){ + int bound = 0; + boolean hasBound = true; + // check all children have a bound + for (int ci=0, cie =tc.nbChildren() ; ci < cie ; ci++) { + Expression child = tc.childAt(ci); + if (child.getOp() == Op.PLACEREF) { + if (limits[child.getValue()] == -1) { + hasBound = false; + break; + } else { + bound += limits[child.getValue()]; + } + } else if (child.getOp() == Op.CONST) { + bound += child.getValue(); + } else { + System.out.println("Strange operator met in bounds query."); + } + } + if (hasBound) { + maxStruct.set(propid, Math.min(maxStruct.get(propid)==-1?Integer.MAX_VALUE:maxStruct.get(propid), bound)); + } + } + } + System.out.println("Current structural bounds on expressions : " + maxStruct); + } + + + + lastMaxSeen = new ArrayList<>(maxSeen); RandomExplorer re = new RandomExplorer(sr); int steps = 1000000; // 1 million @@ -206,8 +360,8 @@ public static void computeToCheck(SparsePetriNet spn, List tocheckIndex } j++; } - } - + } + static int treatVerdicts(SparsePetriNet sparsePetriNet, DoneProperties doneProps, List tocheck, List tocheckIndexes, List paths, List maxSeen, List maxStruct) { return treatVerdicts(sparsePetriNet, doneProps, tocheck, tocheckIndexes, paths, "",maxSeen,maxStruct); @@ -217,7 +371,7 @@ static int treatVerdicts(SparsePetriNet spn, DoneProperties doneProps, List tocheckIndexes, List paths, String technique, List maxSeen, List maxStruct) { int seen = 0; for (int v = paths.size()-1 ; v >= 0 ; v--) { - if (maxSeen.get(v)==maxStruct.get(v)) { + if (maxSeen.get(v).equals(maxStruct.get(v))) { fr.lip6.move.gal.structural.Property prop = spn.getProperties().get(v); doneProps.put(prop.getName(),maxSeen.get(v),"TOPOLOGICAL SAT_SMT RANDOM_WALK"); tocheck.remove(v); @@ -284,7 +438,7 @@ private static int interpretVerdict(List tocheck, SparsePetriNet spn for (int v = verdicts.length-1 ; v >= 0 ; v--) { int cur = verdicts[v]; maxSeen.set(v,Math.max(maxSeen.get(v), cur)); - if (maxSeen.get(v)==maxStruct.get(v)) { + if (maxSeen.get(v).equals(maxStruct.get(v))) { fr.lip6.move.gal.structural.Property prop = spn.getProperties().get(v); doneProps.put(prop.getName(),maxSeen.get(v),"TOPOLOGICAL "+walkType+"_WALK"); tocheck.remove(v); From 4902025ef2be22f6842e89d7a35466ac8f4972a6 Mon Sep 17 00:00:00 2001 From: Yann Thierry-Mieg Date: Mon, 1 Mar 2021 17:50:38 +0100 Subject: [PATCH 30/43] Constant might occur in bounds due to simplifications --- .../src/fr/lip6/move/gal/structural/expr/Constant.java | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/fr.lip6.move.gal.structural/src/fr/lip6/move/gal/structural/expr/Constant.java b/fr.lip6.move.gal.structural/src/fr/lip6/move/gal/structural/expr/Constant.java index 053d773d2b..0000c6390a 100644 --- a/fr.lip6.move.gal.structural/src/fr/lip6/move/gal/structural/expr/Constant.java +++ b/fr.lip6.move.gal.structural/src/fr/lip6/move/gal/structural/expr/Constant.java @@ -26,6 +26,10 @@ public String toString() { @Override public int evalDistance(SparseIntArray state, boolean isNeg) { + if (!isNeg) { + // should be a bounds query + return value; + } throw new UnsupportedOperationException(); } From 0221ae26122852835f1c9ac6aec9ad32c061b61c Mon Sep 17 00:00:00 2001 From: Yann Thierry-Mieg Date: Mon, 1 Mar 2021 17:51:31 +0100 Subject: [PATCH 31/43] Still WIP : refining structural bounds --- .../gal/application/UpperBoundsSolver.java | 161 +++++++++--------- 1 file changed, 85 insertions(+), 76 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 ac40909582..558c311867 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 @@ -107,6 +107,7 @@ public static void applyReductions(MccTranslator reader, DoneProperties doneProp } } + // start with positive semi flows for (SparseIntArray invariant : posinv) { @@ -131,94 +132,102 @@ public static void applyReductions(MccTranslator reader, DoneProperties doneProp } } + System.out.println("(Positive flows) Managed to find structural bounds :" + Arrays.toString(limits)); + System.out.println("Current structural bounds on expressions : " + maxStruct); + // now use these bounds to have a (pessimistic) opinion on generalized flows - for (SparseIntArray invariant : posinv) { + for (int repeat=0; repeat < 2 ; repeat++) { + for (SparseIntArray invariant : geninv) { - // ok so we have an invariant : a0 * p0 - a1 * p1 + ...= K - // Now if all negative coefficient elements are actually bounded, we can conservatively use this bound - // e.g. p0 - p1 = K knowing that p1 <= K1 => p0 - K1 <= K => p0 <= K + K1 - // in other words, move all negative elements to the right, update K pessimistically - // Similarly, if the positive elements are all bounded we can deduce - // p0 - p1 = K knowing that p0 <= K0 => p0 - K = p1 => p1 <= K0 - K - - // true if - boolean boundPosExists = true; - boolean boundNegExists = true; - - // compute K and whether we have bounds on one term - int tsum = 0; - int pbound = 0; - int nbound = 0; - for (int i = 0 ; i < invariant.size() ; i++) { - int v = invariant.keyAt(i); - int val = invariant.valueAt(i); - tsum += sr.getMarks().get(v) * val; - if (val < 0 && limits[v]==-1) { - boundNegExists = false; - } else if (val > 0 && limits[v]==-1) { - boundPosExists = false; - } else if (val < 0) { - nbound -= val * limits[v]; - } else if (val > 0) { - pbound += val * limits[v]; - } - } - - // apply any bounds found - if (boundPosExists || boundNegExists) { - // p0 - p1 = K knowing that p0 <= K0 => p0 - K = p1 => p1 <= K0 - K - int psum = pbound - tsum; + // ok so we have an invariant : a0 * p0 - a1 * p1 + ...= K + // Now if all negative coefficient elements are actually bounded, we can conservatively use this bound // e.g. p0 - p1 = K knowing that p1 <= K1 => p0 - K1 <= K => p0 <= K + K1 - int nsum = nbound + tsum ; - - // iterate elements and set bound + // in other words, move all negative elements to the right, update K pessimistically + // Similarly, if the positive elements are all bounded we can deduce + // p0 - p1 = K knowing that p0 <= K0 => p0 - K = p1 => p1 <= K0 - K + + // true if + boolean boundPosExists = true; + boolean boundNegExists = true; + + // compute K and whether we have bounds on one term + int tsum = 0; + int pbound = 0; + int nbound = 0; for (int i = 0 ; i < invariant.size() ; i++) { int v = invariant.keyAt(i); int val = invariant.valueAt(i); - if (val < 0 && boundPosExists) { - int bound = -nsum / val ; - limits[v] = Math.min(limits[v]==-1?Integer.MAX_VALUE:limits[v], bound); - } else if (val > 0 && boundNegExists){ - int bound = psum / val ; - limits[v] = Math.min(limits[v]==-1?Integer.MAX_VALUE:limits[v], bound); + tsum += sr.getMarks().get(v) * val; + if (val < 0 && limits[v]==-1) { + boundNegExists = false; + } else if (val > 0 && limits[v]==-1) { + boundPosExists = false; + } else if (val < 0) { + nbound -= val * limits[v]; + } else if (val > 0) { + pbound += val * limits[v]; } - } - } - } - System.out.println("Managed to find structural bounds :" + Arrays.toString(limits)); - System.out.println("Current structural bounds on expressions : " + maxStruct); - - for (int propid = 0 ; propid < tocheck.size() ; propid++) { - Expression tc = tocheck.get(propid); - if (tc.getOp() == Op.PLACEREF) { - if (limits[tc.getValue()]!=-1) { - maxStruct.set(propid, Math.min(maxStruct.get(propid)==-1?Integer.MAX_VALUE:maxStruct.get(propid), limits[tc.getValue()])); } - } else if (tc.getOp() == Op.ADD){ - int bound = 0; - boolean hasBound = true; - // check all children have a bound - for (int ci=0, cie =tc.nbChildren() ; ci < cie ; ci++) { - Expression child = tc.childAt(ci); - if (child.getOp() == Op.PLACEREF) { - if (limits[child.getValue()] == -1) { - hasBound = false; - break; + + // apply any bounds found + if (boundPosExists || boundNegExists) { + // p0 - p1 = K knowing that p0 <= K0 => p0 - K = p1 => p1 <= K0 - K + int psum = pbound - tsum; + // e.g. p0 - p1 = K knowing that p1 <= K1 => p0 - K1 <= K => p0 <= K + K1 + int nsum = nbound + tsum ; + + // iterate elements and set bound + for (int i = 0 ; i < invariant.size() ; i++) { + int v = invariant.keyAt(i); + int val = invariant.valueAt(i); + if (val < 0 && boundPosExists) { + int bound = -psum / val ; + limits[v] = Math.min(limits[v]==-1?Integer.MAX_VALUE:limits[v], bound); + } else if (val > 0 && boundNegExists){ + int bound = nsum / val ; + limits[v] = Math.min(limits[v]==-1?Integer.MAX_VALUE:limits[v], bound); + } + } + } + } + System.out.println("Repeat="+repeat+" : Managed to find structural bounds :" + Arrays.toString(limits)); + System.out.println("Current structural bounds on expressions : " + maxStruct); + + for (int propid = 0 ; propid < tocheck.size() ; propid++) { + Expression tc = tocheck.get(propid); + if (tc.getOp() == Op.PLACEREF) { + if (limits[tc.getValue()]!=-1) { + maxStruct.set(propid, Math.min(maxStruct.get(propid)==-1?Integer.MAX_VALUE:maxStruct.get(propid), limits[tc.getValue()])); + } + } else if (tc.getOp() == Op.CONST){ + // trivial ! + maxStruct.set(propid, tc.getValue()); + } else if (tc.getOp() == Op.ADD){ + int bound = 0; + boolean hasBound = true; + // check all children have a bound + for (int ci=0, cie =tc.nbChildren() ; ci < cie ; ci++) { + Expression child = tc.childAt(ci); + if (child.getOp() == Op.PLACEREF) { + if (limits[child.getValue()] == -1) { + hasBound = false; + break; + } else { + bound += limits[child.getValue()]; + } + } else if (child.getOp() == Op.CONST) { + bound += child.getValue(); } else { - bound += limits[child.getValue()]; + System.out.println("Strange operator met in bounds query."); } - } else if (child.getOp() == Op.CONST) { - bound += child.getValue(); - } else { - System.out.println("Strange operator met in bounds query."); } - } - if (hasBound) { - maxStruct.set(propid, Math.min(maxStruct.get(propid)==-1?Integer.MAX_VALUE:maxStruct.get(propid), bound)); - } - } + if (hasBound) { + maxStruct.set(propid, Math.min(maxStruct.get(propid)==-1?Integer.MAX_VALUE:maxStruct.get(propid), bound)); + } + } + } + System.out.println("Current structural bounds on expressions : " + maxStruct); } - System.out.println("Current structural bounds on expressions : " + maxStruct); } From d96b336eef797a0de2d5894813e51530489b9883 Mon Sep 17 00:00:00 2001 From: Yann Thierry-Mieg Date: Mon, 1 Mar 2021 17:57:52 +0100 Subject: [PATCH 32/43] simplify constant bounds (duh !) --- .../lip6/move/gal/application/UpperBoundsSolver.java | 11 +++++++---- 1 file changed, 7 insertions(+), 4 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 558c311867..372dac9284 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 @@ -26,8 +26,8 @@ public class UpperBoundsSolver { public static void checkInInitial(MccTranslator reader, DoneProperties doneProps) { for (fr.lip6.move.gal.structural.Property prop : new ArrayList<>(reader.getSPN().getProperties())) { - if (prop.getBody().getOp() == Op.BOOLCONST) { - doneProps.put(prop.getName(),prop.getBody().getValue()==1,"TOPOLOGICAL INITIAL_STATE"); + if (prop.getBody().getOp() == Op.CONST) { + doneProps.put(prop.getName(),prop.getBody().getValue(),"TOPOLOGICAL INITIAL_STATE"); reader.getSPN().getProperties().remove(prop); } } @@ -41,6 +41,8 @@ public static void applyReductions(MccTranslator reader, DoneProperties doneProp SparsePetriNet spn = reader.getSPN(); + + // need to protect some variables List tocheckIndexes = new ArrayList<>(); List tocheck = new ArrayList<>(spn.getProperties().size()); @@ -250,9 +252,11 @@ public static void applyReductions(MccTranslator reader, DoneProperties doneProp List paths = DeadlockTester.findStructuralMaxWithSMT(tocheck, maxSeen, maxStruct, sr, solverPath, isSafe, repr, iterations==0 ? 5:45,true); //interpretVerdict(tocheck, spn, doneProps, new int[tocheck.size()], solverPath, maxSeen, maxStruct); - + System.out.println("Current structural bounds on expressions (after SMT) : " + maxStruct); + iter += treatVerdicts(reader.getSPN(), doneProps, tocheck, tocheckIndexes, paths, maxSeen, maxStruct); + for (int v = paths.size()-1 ; v >= 0 ; v--) { SparseIntArray parikh = paths.get(v); if (parikh != null) { @@ -302,7 +306,6 @@ public static void applyReductions(MccTranslator reader, DoneProperties doneProp } } } - if (spn.getProperties().removeIf(p -> doneProps.containsKey(p.getName()))) iter++; From cc2db1afb7c362b143dac14251f746510f7ba644 Mon Sep 17 00:00:00 2001 From: Yann Thierry-Mieg Date: Mon, 1 Mar 2021 18:25:11 +0100 Subject: [PATCH 33/43] patch bug in Parikh interpretation --- .../gal/application/UpperBoundsSolver.java | 65 +++++++------------ 1 file changed, 24 insertions(+), 41 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 372dac9284..e793317510 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 @@ -296,8 +296,8 @@ public static void applyReductions(MccTranslator reader, DoneProperties doneProp // } // FlowPrinter.drawNet(sr, "Parikh Test :" + sb.toString(),toHL,Collections.emptySet()); int[] verdicts = re.runGuidedReachabilityDetection(100*sz, parikh, tocheck,repr,30,true); - int seen = interpretVerdict(tocheck, spn, doneProps, verdicts,"PARIKH",maxSeen,maxStruct); - iter += treatVerdicts(reader.getSPN(), doneProps, tocheck, tocheckIndexes, paths, maxSeen, maxStruct); + iter += interpretVerdict(tocheck, spn, doneProps, verdicts,"PARIKH",maxSeen,maxStruct); + //iter += treatVerdicts(reader.getSPN(), doneProps, tocheck, tocheckIndexes, paths, maxSeen, maxStruct); //interpretVerdict(tocheck, spn, doneProps, verdicts, "PARIKH",maxSeen,maxStruct); if (tocheck.isEmpty()) { @@ -395,29 +395,29 @@ static int treatVerdicts(SparsePetriNet spn, DoneProperties doneProps, List= 0 ; v--) { -// SparseIntArray parikh = paths.get(v); -// if (parikh == null) { -// fr.lip6.move.gal.structural.Property prop = spn.getProperties().get(tocheckIndexes.get(v)); -// if (prop.getBody().getOp() == Op.EF) { -// doneProps.put(prop.getName(),false,"STRUCTURAL_REDUCTION TOPOLOGICAL SAT_SMT "+technique); -// } else { -// // AG -// doneProps.put(prop.getName(),true,"STRUCTURAL_REDUCTION TOPOLOGICAL SAT_SMT "+technique); -// } -// -// tocheck.remove(v); -// tocheckIndexes.remove(v); -// iter++; -// } -// } -// if (spn.getProperties().removeIf(p -> doneProps.containsKey(p.getName()))) -// iter++; -// return iter; + } + private static int interpretVerdict(List tocheck, SparsePetriNet spn, DoneProperties doneProps, + int[] verdicts, String walkType, List maxSeen, List maxStruct) { + int seen = 0; + for (int v = verdicts.length-1 ; v >= 0 ; v--) { + int cur = verdicts[v]; + maxSeen.set(v,Math.max(maxSeen.get(v), cur)); + if (maxSeen.get(v).equals(maxStruct.get(v))) { + fr.lip6.move.gal.structural.Property prop = spn.getProperties().get(v); + doneProps.put(prop.getName(),maxSeen.get(v),"TOPOLOGICAL "+walkType+"_WALK"); + tocheck.remove(v); + spn.getProperties().remove(v); + maxSeen.remove(v); + maxStruct.remove(v); + seen++; + } + } + return seen; + } + + static int randomCheckReachability(RandomExplorer re, List tocheck, SparsePetriNet spn, DoneProperties doneProps, int steps, List maxSeen, List maxStruct) { int[] verdicts = re.runRandomReachabilityDetection(steps,tocheck,30,-1,true); @@ -444,24 +444,7 @@ static int randomCheckReachability(RandomExplorer re, List tocheck, return seen; } - private static int interpretVerdict(List tocheck, SparsePetriNet spn, DoneProperties doneProps, - int[] verdicts, String walkType, List maxSeen, List maxStruct) { - int seen = 0; - for (int v = verdicts.length-1 ; v >= 0 ; v--) { - int cur = verdicts[v]; - maxSeen.set(v,Math.max(maxSeen.get(v), cur)); - if (maxSeen.get(v).equals(maxStruct.get(v))) { - fr.lip6.move.gal.structural.Property prop = spn.getProperties().get(v); - doneProps.put(prop.getName(),maxSeen.get(v),"TOPOLOGICAL "+walkType+"_WALK"); - tocheck.remove(v); - spn.getProperties().remove(v); - maxSeen.remove(v); - maxStruct.remove(v); - seen++; - } - } - return seen; - } + static boolean applyReductions(StructuralReduction sr, MccTranslator reader, ReductionType rt, String solverPath, boolean isSafe, boolean withSMT, boolean isFirstTime) { From 510bff77b1400e1371ba0c4638cd0f7d9fadd3a7 Mon Sep 17 00:00:00 2001 From: Yann Thierry-Mieg Date: Tue, 2 Mar 2021 17:01:58 +0100 Subject: [PATCH 34/43] using a skeleton first if possible in UpperBounds --- .../move/gal/application/Application.java | 21 ++++++++++++++----- 1 file changed, 16 insertions(+), 5 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 13f40c21e3..b9d542ef35 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 @@ -270,7 +270,7 @@ public Object startNoEx(IApplicationContext context) throws Exception { if ("StableMarking".equals(examination)) { - + reader.createSPN(); GlobalPropertySolver gps = new GlobalPropertySolver(solverPath); boolean b = gps.solveProperty(examination, reader); @@ -338,11 +338,11 @@ public Object startNoEx(IApplicationContext context) throws Exception { reader.loadProperties(); - // are we going for CTL ? only ITSRunner answers this. if (examination.startsWith("CTL") || examination.equals("UpperBounds")) { if (examination.startsWith("CTL")) { + reader.createSPN(); new AtomicReducerSR().strongReductions(solverPath, reader, isSafe, doneProps); reader.getSPN().simplifyLogic(); reader.rebuildSpecification(doneProps); @@ -357,12 +357,20 @@ public Object startNoEx(IApplicationContext context) throws Exception { //reader.removeAdditionProperties(); } if (examination.equals("UpperBounds")) { + List skelBounds = null; + if (reader.getHLPN() != null) { + skelBounds = UpperBoundsSolver.treatSkeleton(reader,doneProps, solverPath); + + reader.getHLPN().getProperties().removeIf(p->doneProps.containsKey(p.getName())); + } + + reader.createSPN(); reader.getSPN().simplifyLogic(); reader.getSPN().getProperties().removeIf(p -> doneProps.containsKey(p.getName())); UpperBoundsSolver.checkInInitial(reader, doneProps); - UpperBoundsSolver.applyReductions(reader, doneProps, solverPath, isSafe); + UpperBoundsSolver.applyReductions(reader, doneProps, solverPath, isSafe, skelBounds); reader.getSPN().getProperties().removeIf(p -> doneProps.containsKey(p.getName())); // checkInInitial(reader.getSpec(), doneProps, isSafe); @@ -379,7 +387,7 @@ public Object startNoEx(IApplicationContext context) throws Exception { r2.getSPN().getProperties().clear(); r2.getSPN().getProperties().add(p); UpperBoundsSolver.checkInInitial(r2, doneProps); - UpperBoundsSolver.applyReductions(r2, doneProps, solverPath, isSafe); + UpperBoundsSolver.applyReductions(r2, doneProps, solverPath, isSafe,null); System.out.println("Ending property specific reduction for "+p.getName()+" in "+ (System.currentTimeMillis()-time)+" ms."); } reader.getSPN().getProperties().removeIf(p -> doneProps.containsKey(p.getName())); @@ -401,6 +409,7 @@ public Object startNoEx(IApplicationContext context) throws Exception { if (examination.startsWith("LTL") || examination.equals("ReachabilityDeadlock")|| examination.equals("GlobalProperties")) { if (examination.startsWith("LTL")) { + reader.createSPN(); if (spotPath != null) { SpotRunner sr = new SpotRunner(spotPath, pwd, 10); sr.runLTLSimplifications(reader.getSPN()); @@ -426,6 +435,8 @@ public Object startNoEx(IApplicationContext context) throws Exception { long debut = System.currentTimeMillis(); + reader.createSPN(); + // remove parameters // reader.flattenSpec(false); // Specification spec = reader.getSpec(); @@ -583,7 +594,7 @@ public Object startNoEx(IApplicationContext context) throws Exception { if (examination.equals("ReachabilityFireability") || examination.equals("ReachabilityCardinality") ) { if (true) { - + reader.createSPN(); ReachabilitySolver.checkInInitial(reader, doneProps); if (!reader.getSPN().getProperties().isEmpty()) ReachabilitySolver.applyReductions(reader, doneProps, solverPath, isSafe); From 6f44a48857da50f4d5ce231185a46c8e6a32bb2b Mon Sep 17 00:00:00 2001 From: Yann Thierry-Mieg Date: Tue, 2 Mar 2021 17:04:04 +0100 Subject: [PATCH 35/43] using a skeleton first if possible in UpperBounds + diverse refactoring to reuse some code in both scenarios --- .../gal/application/UpperBoundsSolver.java | 406 +++++++++++------- 1 file changed, 242 insertions(+), 164 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 e793317510..f1903e4d16 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 @@ -32,16 +32,77 @@ public static void checkInInitial(MccTranslator reader, DoneProperties doneProps } } } + + public static List treatSkeleton(MccTranslator reader, DoneProperties doneProps, String solverPath) { + SparsePetriNet spn = reader.getHLPN().skeleton(); + spn.simplifyLogic(); + spn.toPredicates(); + spn.testInInitial(); + spn.removeConstantPlaces(); + spn.removeRedundantTransitions(false); + spn.removeConstantPlaces(); + spn.simplifyLogic(); + + + // need to protect some variables + List tocheckIndexes = new ArrayList<>(); + List tocheck = new ArrayList<>(spn.getProperties().size()); + computeToCheck(spn, tocheckIndexes, tocheck, doneProps); + List maxStruct = new ArrayList<>(tocheckIndexes.size()); + List maxSeen = new ArrayList<>(tocheckIndexes.size()); + { + SparseIntArray m0 = new SparseIntArray(spn.getMarks()); + for (Expression tc:tocheck) { + maxSeen.add(tc.eval(m0)); + maxStruct.add(-1); + } + } + + StructuralReduction sr = new StructuralReduction(spn); + approximateStructuralBoundsUsingInvariants(sr, tocheck, maxStruct); + + checkStatus(spn, tocheck, maxStruct, maxSeen, doneProps, "TOPOLOGICAL CPN_APPROX INITIAL_STATE"); + + { + List paths = new ArrayList<>(tocheck.size()); + for (int i=0; i < tocheck.size(); i++) { + paths.add(null); + } + treatVerdicts(reader.getSPN(), doneProps, tocheck, tocheckIndexes, paths , maxSeen, maxStruct); + } + + if (solverPath != null) { + List repr = new ArrayList<>(); + List paths = DeadlockTester.findStructuralMaxWithSMT(tocheck, maxSeen, maxStruct, sr, solverPath, false, repr, 5,true); + + //interpretVerdict(tocheck, spn, doneProps, new int[tocheck.size()], solverPath, maxSeen, maxStruct); + System.out.println("Current structural bounds on expressions (after SMT) : " + maxStruct); + + checkStatus(spn, tocheck, maxStruct, maxSeen, doneProps, "TOPOLOGICAL SAT_SMT CPN_APPROX INITIAL_STATE"); + } + return maxStruct; + } + + private static void checkStatus(SparsePetriNet spn, List tocheck, List maxStruct, + List maxSeen, DoneProperties doneProps, String tech) { + for (int v = tocheck.size()-1 ; v >= 0 ; v--) { + if (maxSeen.get(v).equals(maxStruct.get(v))) { + fr.lip6.move.gal.structural.Property prop = spn.getProperties().get(v); + doneProps.put(prop.getName(),maxSeen.get(v),tech); + tocheck.remove(v); + spn.getProperties().remove(v); + maxSeen.remove(v); + maxStruct.remove(v); + } + } + } + - public static void applyReductions(MccTranslator reader, DoneProperties doneProps, String solverPath, boolean isSafe) { + public static void applyReductions(MccTranslator reader, DoneProperties doneProps, String solverPath, boolean isSafe, List initMaxStruct) { int iter; int iterations =0; - boolean doneAtoms = false; - boolean doneSums = false; SparsePetriNet spn = reader.getSPN(); - - // need to protect some variables List tocheckIndexes = new ArrayList<>(); @@ -61,6 +122,15 @@ public static void applyReductions(MccTranslator reader, DoneProperties doneProp } } } + if (initMaxStruct != null) { + for (int i=0; i < maxStruct.size() ; i++) { + maxStruct.set(i, Math.min(maxStruct.get(i)==-1?Integer.MAX_VALUE:maxStruct.get(i), + initMaxStruct.get(i)==-1?Integer.MAX_VALUE:initMaxStruct.get(i))); + } + } + + checkStatus(spn, tocheck, maxStruct, maxSeen, doneProps, "TOPOLOGICAL INITIAL_STATE"); + List lastMaxSeen = null; boolean first = true; @@ -76,163 +146,8 @@ public static void applyReductions(MccTranslator reader, DoneProperties doneProp StructuralReduction sr = new StructuralReduction(spn); - { - // try to set a max bound on variables using invariants - - // effect matrix - MatrixCol sumMatrix = MatrixCol.sumProd(-1, spn.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 - Arrays.fill(limits, -1); - // split invariants in positive semi-flows and generalized flows (with neg coeffs) - List posinv = new ArrayList(); - List geninv = new ArrayList(); - - // do the split - for (SparseIntArray invariant : invar) { - boolean hasNeg = false; - for (int i=0; i < invariant.size() ; i++) { - if (invariant.valueAt(i) < 0) { - hasNeg = true; - break; - } - } - if (! hasNeg) { - posinv.add(invariant); - } else { - geninv.add(invariant); - } - } - - - // start with positive semi flows - for (SparseIntArray invariant : posinv) { - - // ok so we have an invariant : a0 * p0 + a1 * p1 ...= K - // at best all variables are zero except one, in that case pi = K / ai (rounded down) - // e.g. 2*p0 + p1 = 4 => p0 <= 2 ; p1 <= 4 - // e.g. 2*p0 + p1 = 5 => p0 <= 2 ; p1 <= 5 - - // compute K - int sum = 0; - for (int i = 0 ; i < invariant.size() ; i++) { - int v = invariant.keyAt(i); - int val = invariant.valueAt(i); - sum += sr.getMarks().get(v) * val; - } - // iterate elements and set bound - for (int i = 0 ; i < invariant.size() ; i++) { - int v = invariant.keyAt(i); - int val = invariant.valueAt(i); - int bound = sum / val ; - limits[v] = Math.min(limits[v]==-1?Integer.MAX_VALUE:limits[v], bound); - } - } - - System.out.println("(Positive flows) Managed to find structural bounds :" + Arrays.toString(limits)); - System.out.println("Current structural bounds on expressions : " + maxStruct); - - // now use these bounds to have a (pessimistic) opinion on generalized flows - for (int repeat=0; repeat < 2 ; repeat++) { - for (SparseIntArray invariant : geninv) { - - // ok so we have an invariant : a0 * p0 - a1 * p1 + ...= K - // Now if all negative coefficient elements are actually bounded, we can conservatively use this bound - // e.g. p0 - p1 = K knowing that p1 <= K1 => p0 - K1 <= K => p0 <= K + K1 - // in other words, move all negative elements to the right, update K pessimistically - // Similarly, if the positive elements are all bounded we can deduce - // p0 - p1 = K knowing that p0 <= K0 => p0 - K = p1 => p1 <= K0 - K - - // true if - boolean boundPosExists = true; - boolean boundNegExists = true; - - // compute K and whether we have bounds on one term - int tsum = 0; - int pbound = 0; - int nbound = 0; - for (int i = 0 ; i < invariant.size() ; i++) { - int v = invariant.keyAt(i); - int val = invariant.valueAt(i); - tsum += sr.getMarks().get(v) * val; - if (val < 0 && limits[v]==-1) { - boundNegExists = false; - } else if (val > 0 && limits[v]==-1) { - boundPosExists = false; - } else if (val < 0) { - nbound -= val * limits[v]; - } else if (val > 0) { - pbound += val * limits[v]; - } - } - - // apply any bounds found - if (boundPosExists || boundNegExists) { - // p0 - p1 = K knowing that p0 <= K0 => p0 - K = p1 => p1 <= K0 - K - int psum = pbound - tsum; - // e.g. p0 - p1 = K knowing that p1 <= K1 => p0 - K1 <= K => p0 <= K + K1 - int nsum = nbound + tsum ; - - // iterate elements and set bound - for (int i = 0 ; i < invariant.size() ; i++) { - int v = invariant.keyAt(i); - int val = invariant.valueAt(i); - if (val < 0 && boundPosExists) { - int bound = -psum / val ; - limits[v] = Math.min(limits[v]==-1?Integer.MAX_VALUE:limits[v], bound); - } else if (val > 0 && boundNegExists){ - int bound = nsum / val ; - limits[v] = Math.min(limits[v]==-1?Integer.MAX_VALUE:limits[v], bound); - } - } - } - } - System.out.println("Repeat="+repeat+" : Managed to find structural bounds :" + Arrays.toString(limits)); - System.out.println("Current structural bounds on expressions : " + maxStruct); - - for (int propid = 0 ; propid < tocheck.size() ; propid++) { - Expression tc = tocheck.get(propid); - if (tc.getOp() == Op.PLACEREF) { - if (limits[tc.getValue()]!=-1) { - maxStruct.set(propid, Math.min(maxStruct.get(propid)==-1?Integer.MAX_VALUE:maxStruct.get(propid), limits[tc.getValue()])); - } - } else if (tc.getOp() == Op.CONST){ - // trivial ! - maxStruct.set(propid, tc.getValue()); - } else if (tc.getOp() == Op.ADD){ - int bound = 0; - boolean hasBound = true; - // check all children have a bound - for (int ci=0, cie =tc.nbChildren() ; ci < cie ; ci++) { - Expression child = tc.childAt(ci); - if (child.getOp() == Op.PLACEREF) { - if (limits[child.getValue()] == -1) { - hasBound = false; - break; - } else { - bound += limits[child.getValue()]; - } - } else if (child.getOp() == Op.CONST) { - bound += child.getValue(); - } else { - System.out.println("Strange operator met in bounds query."); - } - } - if (hasBound) { - maxStruct.set(propid, Math.min(maxStruct.get(propid)==-1?Integer.MAX_VALUE:maxStruct.get(propid), bound)); - } - } - } - System.out.println("Current structural bounds on expressions : " + maxStruct); - } - } - - + approximateStructuralBoundsUsingInvariants(sr, tocheck, maxStruct); + checkStatus(spn, tocheck, maxStruct, maxSeen, doneProps, "TOPOLOGICAL INITIAL_STATE"); lastMaxSeen = new ArrayList<>(maxSeen); @@ -243,7 +158,9 @@ public static void applyReductions(MccTranslator reader, DoneProperties doneProp } if (randomCheckReachability(re, tocheck, spn, doneProps,steps,maxSeen,maxStruct) >0) iter++; - + + checkStatus(spn, tocheck, maxStruct, maxSeen, doneProps, "TOPOLOGICAL RANDOM_WALK"); + if (reader.getSPN().getProperties().isEmpty()) break; @@ -252,7 +169,7 @@ public static void applyReductions(MccTranslator reader, DoneProperties doneProp List paths = DeadlockTester.findStructuralMaxWithSMT(tocheck, maxSeen, maxStruct, sr, solverPath, isSafe, repr, iterations==0 ? 5:45,true); //interpretVerdict(tocheck, spn, doneProps, new int[tocheck.size()], solverPath, maxSeen, maxStruct); - System.out.println("Current structural bounds on expressions (after SMT) : " + 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); @@ -363,6 +280,165 @@ public static void applyReductions(MccTranslator reader, DoneProperties doneProp } + private static void approximateStructuralBoundsUsingInvariants(StructuralReduction sr, List tocheck, + List maxStruct) { + { + // try to set a max bound on variables using invariants + + // effect matrix + MatrixCol sumMatrix = MatrixCol.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 + Arrays.fill(limits, -1); + // split invariants in positive semi-flows and generalized flows (with neg coeffs) + List posinv = new ArrayList(); + List geninv = new ArrayList(); + + // do the split + for (SparseIntArray invariant : invar) { + boolean hasNeg = false; + for (int i=0; i < invariant.size() ; i++) { + if (invariant.valueAt(i) < 0) { + hasNeg = true; + break; + } + } + if (! hasNeg) { + posinv.add(invariant); + } else { + geninv.add(invariant); + } + } + + + // start with positive semi flows + for (SparseIntArray invariant : posinv) { + + // ok so we have an invariant : a0 * p0 + a1 * p1 ...= K + // at best all variables are zero except one, in that case pi = K / ai (rounded down) + // e.g. 2*p0 + p1 = 4 => p0 <= 2 ; p1 <= 4 + // e.g. 2*p0 + p1 = 5 => p0 <= 2 ; p1 <= 5 + + // compute K + int sum = 0; + for (int i = 0 ; i < invariant.size() ; i++) { + int v = invariant.keyAt(i); + int val = invariant.valueAt(i); + sum += sr.getMarks().get(v) * val; + } + // iterate elements and set bound + for (int i = 0 ; i < invariant.size() ; i++) { + int v = invariant.keyAt(i); + int val = invariant.valueAt(i); + int bound = sum / val ; + limits[v] = Math.min(limits[v]==-1?Integer.MAX_VALUE:limits[v], bound); + } + } + + System.out.println("(Positive flows) Managed to find structural bounds :" + Arrays.toString(limits)); + System.out.println("Current structural bounds on expressions : " + maxStruct); + + // now use these bounds to have a (pessimistic) opinion on generalized flows + for (int repeat=0; repeat < 2 ; repeat++) { + for (SparseIntArray invariant : geninv) { + + // ok so we have an invariant : a0 * p0 - a1 * p1 + ...= K + // Now if all negative coefficient elements are actually bounded, we can conservatively use this bound + // e.g. p0 - p1 = K knowing that p1 <= K1 => p0 - K1 <= K => p0 <= K + K1 + // in other words, move all negative elements to the right, update K pessimistically + // Similarly, if the positive elements are all bounded we can deduce + // p0 - p1 = K knowing that p0 <= K0 => p0 - K = p1 => p1 <= K0 - K + + // true if + boolean boundPosExists = true; + boolean boundNegExists = true; + + // compute K and whether we have bounds on one term + int tsum = 0; + int pbound = 0; + int nbound = 0; + for (int i = 0 ; i < invariant.size() ; i++) { + int v = invariant.keyAt(i); + int val = invariant.valueAt(i); + tsum += sr.getMarks().get(v) * val; + if (val < 0 && limits[v]==-1) { + boundNegExists = false; + } else if (val > 0 && limits[v]==-1) { + boundPosExists = false; + } else if (val < 0) { + nbound -= val * limits[v]; + } else if (val > 0) { + pbound += val * limits[v]; + } + } + + // apply any bounds found + if (boundPosExists || boundNegExists) { + // p0 - p1 = K knowing that p0 <= K0 => p0 - K = p1 => p1 <= K0 - K + int psum = pbound - tsum; + // e.g. p0 - p1 = K knowing that p1 <= K1 => p0 - K1 <= K => p0 <= K + K1 + int nsum = nbound + tsum ; + + // iterate elements and set bound + for (int i = 0 ; i < invariant.size() ; i++) { + int v = invariant.keyAt(i); + int val = invariant.valueAt(i); + if (val < 0 && boundPosExists) { + int bound = -psum / val ; + limits[v] = Math.min(limits[v]==-1?Integer.MAX_VALUE:limits[v], bound); + } else if (val > 0 && boundNegExists){ + int bound = nsum / val ; + limits[v] = Math.min(limits[v]==-1?Integer.MAX_VALUE:limits[v], bound); + } + } + } + } + System.out.println("Repeat="+repeat+" : Managed to find structural bounds :" + Arrays.toString(limits)); + System.out.println("Current structural bounds on expressions : " + maxStruct ); + + for (int propid = 0 ; propid < tocheck.size() ; propid++) { + Expression tc = tocheck.get(propid); + if (tc.getOp() == Op.PLACEREF) { + if (limits[tc.getValue()]!=-1) { + maxStruct.set(propid, Math.min(maxStruct.get(propid)==-1?Integer.MAX_VALUE:maxStruct.get(propid), limits[tc.getValue()])); + } + } else if (tc.getOp() == Op.CONST){ + // trivial ! + maxStruct.set(propid, tc.getValue()); + } else if (tc.getOp() == Op.ADD){ + int bound = 0; + boolean hasBound = true; + // check all children have a bound + for (int ci=0, cie =tc.nbChildren() ; ci < cie ; ci++) { + Expression child = tc.childAt(ci); + if (child.getOp() == Op.PLACEREF) { + if (limits[child.getValue()] == -1) { + hasBound = false; + break; + } else { + bound += limits[child.getValue()]; + } + } else if (child.getOp() == Op.CONST) { + bound += child.getValue(); + } else { + System.out.println("Strange operator met in bounds query."); + } + } + if (hasBound) { + maxStruct.set(propid, Math.min(maxStruct.get(propid)==-1?Integer.MAX_VALUE:maxStruct.get(propid), bound)); + } + } + } + System.out.println("Current structural bounds on expressions : " + maxStruct); + } + } + } + public static void computeToCheck(SparsePetriNet spn, List tocheckIndexes, List tocheck, DoneProperties doneProps) { int j=0; for (fr.lip6.move.gal.structural.Property p : spn.getProperties()) { @@ -581,4 +657,6 @@ private static boolean arcValuesTriggerSMTDeadTransitions(StructuralReduction sr return false; } + + } From 3ec9f7981dbe16fa9b7991b241ddb8a7a54023b9 Mon Sep 17 00:00:00 2001 From: Yann Thierry-Mieg Date: Tue, 2 Mar 2021 17:04:30 +0100 Subject: [PATCH 36/43] create two steps to work with HLPN first if we we can --- .../move/gal/application/MccTranslator.java | 40 +++++++++---------- 1 file changed, 20 insertions(+), 20 deletions(-) diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/MccTranslator.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/MccTranslator.java index f0d668feb6..3e96466601 100644 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/MccTranslator.java +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/MccTranslator.java @@ -323,33 +323,33 @@ public void loadProperties() throws IOException { if (hlpn != null) { parsed = fr.lip6.move.gal.mcc.properties.PropertyParser.fileToProperties(propff , hlpn, getPropertyType()); hlpn.simplifyLogic(); - spn = hlpn.unfold(); } else { parsed = fr.lip6.move.gal.mcc.properties.PropertyParser.fileToProperties(propff , spn, getPropertyType()); } - if (DEBUG >= 1) System.out.println("initial properties :" + spn.getProperties()); - spn.simplifyLogic(); - spn.toPredicates(); - spn.testInInitial(); - spn.removeConstantPlaces(); - spn.removeRedundantTransitions(false); - spn.removeConstantPlaces(); - spn.simplifyLogic(); - if (isSafeNet) { - spn.assumeOneSafe(); - } - if (DEBUG >= 1) System.out.println("after syntactic reduction properties :" +spn.getProperties()); - -// Properties props = PropertyParser.fileToProperties(propff , spec); -// spec = ToGalTransformer.toGal(props); -// if (isSafeNet) { -// rewriteVariableComparisons(spec); -// } -// PropertySimplifier.pushNegation(spec); System.out.println("Parsed " +parsed +" properties from file "+propff+" in "+ (System.currentTimeMillis() - time) + " ms."); } } + + public void createSPN() { + if (hlpn != null) { + hlpn.simplifyLogic(); + spn = hlpn.unfold(); + } + if (DEBUG >= 1) System.out.println("initial properties :" + spn.getProperties()); + spn.simplifyLogic(); + spn.toPredicates(); + spn.testInInitial(); + spn.removeConstantPlaces(); + spn.removeRedundantTransitions(false); + spn.removeConstantPlaces(); + spn.simplifyLogic(); + if (isSafeNet) { + spn.assumeOneSafe(); + } + if (DEBUG >= 1) System.out.println("after syntactic reduction properties :" +spn.getProperties()); + } + private PropertyType getPropertyType() { if ("ReachabilityFireability".equals(examination) || "ReachabilityCardinality".equals(examination)) { return PropertyType.INVARIANT; From 29a88dfe88c156f606ca52e26328cb45ced50e50 Mon Sep 17 00:00:00 2001 From: Yann Thierry-Mieg Date: Tue, 2 Mar 2021 17:10:46 +0100 Subject: [PATCH 37/43] a method to build a skeleton --- .../move/gal/structural/SparseHLPetriNet.java | 110 ++++++++++++++++++ 1 file changed, 110 insertions(+) diff --git a/fr.lip6.move.gal.structural/src/fr/lip6/move/gal/structural/SparseHLPetriNet.java b/fr.lip6.move.gal.structural/src/fr/lip6/move/gal/structural/SparseHLPetriNet.java index c060ec5abe..4ec7d3931d 100644 --- a/fr.lip6.move.gal.structural/src/fr/lip6/move/gal/structural/SparseHLPetriNet.java +++ b/fr.lip6.move.gal.structural/src/fr/lip6/move/gal/structural/SparseHLPetriNet.java @@ -2,6 +2,8 @@ import java.util.ArrayDeque; import java.util.ArrayList; +import java.util.Arrays; +import java.util.HashSet; import java.util.List; import java.util.Queue; import java.util.logging.Logger; @@ -86,6 +88,57 @@ public String toString() { } + public SparsePetriNet skeleton () { + long time = System.currentTimeMillis(); + SparsePetriNet spn = new SparsePetriNet(); + spn.setName(getName() +"_skel"); + + // generate places with appropriate indexes + for (HLPlace p : places) { + spn.addPlace(p.getName(), Arrays.stream(p.getInitial()).sum()); + } + for (HLTrans t : transitions) { + spn.addTransition(t.name); + + SparseIntArray pt = computeCardinality(t.pre); + for (int i=0,ie=pt.size();i(), new HashSet<>()); + return spn; + } + + + + private SparseIntArray computeCardinality(List> arcs) { + SparseIntArray pt = new SparseIntArray(); + for (Pair arc : arcs) { + Expression place = arc.getFirst(); + if (place.getOp() == Op.HLPLACEREF) { + ArrayVarRef aref = (ArrayVarRef) place; + int pind = aref.base; + int val = pt.get(pind) + arc.getSecond(); + pt.put(pind, val); + } + } + return pt; + } + + public SparsePetriNet unfold () { long time = System.currentTimeMillis(); SparsePetriNet spn = new SparsePetriNet(); @@ -245,6 +298,63 @@ private Void remapParameter(Expression expr, Param tokeep, Param todel) { return null; } + private Expression bindSkeletonColors(Expression expr) { + if (expr == null) { + return expr; + } else if (expr instanceof BinOp) { + BinOp bin = (BinOp) expr; + Expression l = bindSkeletonColors(bin.left); + Expression r = bindSkeletonColors(bin.right); + if (l == bin.left && r == bin.right) { + return expr; + } + return Expression.op(bin.op, l, r); + } else if (expr instanceof NaryOp) { + NaryOp nop = (NaryOp) expr; + List resc = new ArrayList<>(); + if (expr.getOp() == Op.CARD || expr.getOp() == Op.BOUND) { + for (Expression child : nop.getChildren()) { + if (child.getOp() == Op.PLACEREF) { + if (places.get(child.getValue()).isConstant()) { + int sum = 0; + for (int v : places.get(child.getValue()).getInitial()) { + sum +=v; + } + resc.add(Expression.constant(sum)); + } else { + resc.add(Expression.var(child.getValue())); + } + } + } + return Expression.nop(nop.getOp(), resc); + } else if (expr.getOp() == Op.ENABLED) { + for (Expression child : nop.getChildren()) { + if (child.getOp() == Op.TRANSREF) { + resc.add(Expression.trans(child.getValue())); + } + } + return Expression.nop(nop.getOp(), resc); + } else { + boolean changed = false; + for (Expression child : nop.getChildren()) { + Expression nc = bindSkeletonColors(child); + resc.add(nc); + if (nc != child) { + changed = true; + } + } + if (!changed) { + return expr; + } + return Expression.nop(nop.getOp(), resc); + } + } else if (expr instanceof ArrayVarRef) { + ArrayVarRef aref = (ArrayVarRef) expr; + return Expression.var( aref.base ); + } + return expr; + } + private Expression bindColors(Expression expr, List> en) { if (expr == null) { return expr; From 22bd407bde77a7606480eb6fcfe6898498fc76ee Mon Sep 17 00:00:00 2001 From: Yann Thierry-Mieg Date: Tue, 2 Mar 2021 17:13:11 +0100 Subject: [PATCH 38/43] reduce verbosity, invariant based bounds are tested and work. --- .../move/gal/application/UpperBoundsSolver.java | 17 +++++++++++------ 1 file changed, 11 insertions(+), 6 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 f1903e4d16..b575e0cc21 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 @@ -340,8 +340,10 @@ private static void approximateStructuralBoundsUsingInvariants(StructuralReducti } } - System.out.println("(Positive flows) Managed to find structural bounds :" + Arrays.toString(limits)); - System.out.println("Current structural bounds on expressions : " + maxStruct); + if (Application.DEBUG >= 2) { + System.out.println("(Positive flows) Managed to find structural bounds :" + Arrays.toString(limits)); + System.out.println("Current structural bounds on expressions : " + maxStruct); + } // now use these bounds to have a (pessimistic) opinion on generalized flows for (int repeat=0; repeat < 2 ; repeat++) { @@ -398,9 +400,10 @@ private static void approximateStructuralBoundsUsingInvariants(StructuralReducti } } } - System.out.println("Repeat="+repeat+" : Managed to find structural bounds :" + Arrays.toString(limits)); - System.out.println("Current structural bounds on expressions : " + maxStruct ); - + if (Application.DEBUG >= 2) { + System.out.println("Repeat="+repeat+" : Managed to find structural bounds :" + Arrays.toString(limits)); + System.out.println("Current structural bounds on expressions : " + maxStruct ); + } for (int propid = 0 ; propid < tocheck.size() ; propid++) { Expression tc = tocheck.get(propid); if (tc.getOp() == Op.PLACEREF) { @@ -434,7 +437,9 @@ private static void approximateStructuralBoundsUsingInvariants(StructuralReducti } } } - System.out.println("Current structural bounds on expressions : " + maxStruct); + if (Application.DEBUG >= 1) { + System.out.println("Current structural bounds on expressions : " + maxStruct); + } } } } From b47b295cbc768c3931628367a5c6b131148a02f6 Mon Sep 17 00:00:00 2001 From: Yann Thierry-Mieg Date: Wed, 3 Mar 2021 14:19:06 +0100 Subject: [PATCH 39/43] slight API changes to enable reuse in skeleton scenarios --- .../move/gal/structural/StructuralReduction.java | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/fr.lip6.move.gal.structural/src/fr/lip6/move/gal/structural/StructuralReduction.java b/fr.lip6.move.gal.structural/src/fr/lip6/move/gal/structural/StructuralReduction.java index 6ed2ebfc7c..0915ff13df 100644 --- a/fr.lip6.move.gal.structural/src/fr/lip6/move/gal/structural/StructuralReduction.java +++ b/fr.lip6.move.gal.structural/src/fr/lip6/move/gal/structural/StructuralReduction.java @@ -115,7 +115,7 @@ public int reduce (ReductionType rt) throws NoDeadlockExists, DeadlockFound { if (findFreeSCC()) total++; - if (findSCCSuffixes(rt)) + if (findSCCSuffixes(rt) != null) total++; int deltatpos = 0; do { @@ -128,7 +128,7 @@ public int reduce (ReductionType rt) throws NoDeadlockExists, DeadlockFound { // } totaliter += ruleReduceTrans(rt); - totaliter += findSCCSuffixes(rt) ? 1:0; + totaliter += findSCCSuffixes(rt) != null ? 1:0; int implicit = ruleImplicitPlace(); totaliter +=implicit; @@ -187,7 +187,7 @@ public int reduce (ReductionType rt) throws NoDeadlockExists, DeadlockFound { totaliter += findFreeSCC() ? 1 :0; } if (totaliter == 0) { - totaliter += findSCCSuffixes(rt) ? 1 :0; + totaliter += findSCCSuffixes(rt) != null ? 1 :0; } totaliter += ruleReducePlaces(rt,true,false); if (totaliter == 0 && rt == ReductionType.SAFETY) { @@ -2128,7 +2128,7 @@ private boolean isStronglyQuasiPersistent(int hid, MatrixCol tflowPT, ReductionT } - private boolean findSCCSuffixes(ReductionType rt) throws DeadlockFound { + public Set findSCCSuffixes(ReductionType rt) throws DeadlockFound { long time = System.currentTimeMillis(); // extract all transitions to a PxP matrix MatrixCol graph = buildGraph(rt, -1); @@ -2150,10 +2150,10 @@ private boolean findSCCSuffixes(ReductionType rt) throws DeadlockFound { if (safeNodes.size() < nbP) { int nbedges = graph.getColumns().stream().mapToInt(col -> col.size()).sum(); System.out.println("Graph (complete) has "+nbedges+ " edges and " + nbP + " vertex of which " + safeNodes.size() + " are kept as prefixes of interest. Removing "+ (nbP - safeNodes.size()) + " places using SCC suffix rule." + (System.currentTimeMillis()- time) + " ms"); - return true; + return safeNodes; } - return false; + return null; } From c205b4ea139efa86b9df1d590ffde54b5cf24fb0 Mon Sep 17 00:00:00 2001 From: Yann Thierry-Mieg Date: Wed, 3 Mar 2021 14:20:17 +0100 Subject: [PATCH 40/43] new API to clear some HL places and related transitions To reduce the HL net *before* unfolding, using info extracted on the skeleton. --- .../move/gal/structural/SparseHLPetriNet.java | 52 ++++++++++++++++++- 1 file changed, 50 insertions(+), 2 deletions(-) diff --git a/fr.lip6.move.gal.structural/src/fr/lip6/move/gal/structural/SparseHLPetriNet.java b/fr.lip6.move.gal.structural/src/fr/lip6/move/gal/structural/SparseHLPetriNet.java index 4ec7d3931d..e991ef27fd 100644 --- a/fr.lip6.move.gal.structural/src/fr/lip6/move/gal/structural/SparseHLPetriNet.java +++ b/fr.lip6.move.gal.structural/src/fr/lip6/move/gal/structural/SparseHLPetriNet.java @@ -6,6 +6,7 @@ import java.util.HashSet; import java.util.List; import java.util.Queue; +import java.util.Set; import java.util.logging.Logger; import android.util.SparseIntArray; @@ -83,8 +84,8 @@ public int getPlaceIndex(String name) { @Override public String toString() { - return "SparseHLPetriNet [places=" + places + ", transitions=" + transitions + ", getName()=" + getName() - + ", getProperties()=" + getProperties() + "]"; + return "SparseHLPetriNet [places=" + places + ",\n transitions=" + transitions + ",\n getName()=" + getName() + + ",\n getProperties()=" + getProperties() + "]"; } @@ -536,6 +537,53 @@ private int transformHLtoPT(HLTrans bt, SparsePetriNet spn) { } return tind; } + + public void dropAllExcept(Set safeNodes) { + + int [] perm = new int [places.size()]; + for (int i = 0, ind =0 ; i < places.size() ; i++) { + if (safeNodes.contains(i)) { + perm[i]=ind++; + } else { + perm[i]=-1; + } + } + + int trem=0,prem=0; + for (int tid = transitions.size()-1 ; tid >= 0 ; tid -- ) { + for (Pair arc : transitions.get(tid).pre) { + int pid = ((ArrayVarRef) arc.getFirst()).base; + if (!safeNodes.contains(pid)) { + transitions.remove(tid); + trem++; + break; + } else { + ((ArrayVarRef) arc.getFirst()).base = perm[pid]; + } + } + } + for (int tid = transitions.size()-1 ; tid >= 0 ; tid -- ) { + for (Pair arc : transitions.get(tid).post) { + int pid = ((ArrayVarRef) arc.getFirst()).base; + ((ArrayVarRef) arc.getFirst()).base = perm[pid]; + } + transitions.get(tid).post.removeIf(arc -> ((ArrayVarRef) arc.getFirst()).base == -1); + } + for (int pid = places.size()-1 ; pid >= 0 ; pid -- ) { + if (! safeNodes.contains(pid)) { + places.remove(pid); + prem++; + } + } + + placeCount = 0; + for (int pid = 0, pide=places.size() ; pid < pide ; pid ++ ) { + places.get(pid).startIndex = placeCount; + placeCount += places.get(pid).getInitial().length; + } + + System.out.println("Prefix of Interest using HLPN skeleton for deadlock discarded "+prem+" places and "+trem + " transitions."); + } } From c178e1a9c452c36dde57db93ac0f9e2419b0c27c Mon Sep 17 00:00:00 2001 From: Yann Thierry-Mieg Date: Wed, 3 Mar 2021 14:22:42 +0100 Subject: [PATCH 41/43] New algorithm : use skeleton to find unavoidable deadlocks ! Indeed, while existence of a deadlock in skeleton is not meaningful, if *all* paths lead to a deadlock in the skeleton, this is also necessarily the case in the Colored net. --- .../move/gal/application/Application.java | 40 +++++++++++++++++++ 1 file changed, 40 insertions(+) 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 b9d542ef35..b37d8b880f 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 @@ -65,6 +65,7 @@ import fr.lip6.move.gal.structural.InvariantCalculator; import fr.lip6.move.gal.structural.NoDeadlockExists; import fr.lip6.move.gal.structural.RandomExplorer; +import fr.lip6.move.gal.structural.SparseHLPetriNet; import fr.lip6.move.gal.structural.SparsePetriNet; import fr.lip6.move.gal.structural.StructuralReduction; import fr.lip6.move.gal.structural.StructuralReduction.ReductionType; @@ -435,6 +436,45 @@ public Object startNoEx(IApplicationContext context) throws Exception { long debut = System.currentTimeMillis(); + if (reader.getHLPN() != null) { + SparsePetriNet spn = reader.getHLPN().skeleton(); + spn.toPredicates(); + spn.testInInitial(); + + // this might break the consistency between hlpn and skeleton place indexes, let's avoid it. + spn.removeConstantPlaces(); + // spn.removeRedundantTransitions(false); + // spn.removeConstantPlaces(); + spn.simplifyLogic(); + + StructuralReduction sr = new StructuralReduction(spn); + try { + Set before = new HashSet<>(sr.getPnames()); + Set safeNodes = sr.findSCCSuffixes(ReductionType.DEADLOCKS); + + if (safeNodes != null) { + Set torem = new HashSet<>(before); + torem.removeAll(sr.getPnames()); + + Set hlSafeNodes = new HashSet<>(); + SparseHLPetriNet hlpn = reader.getHLPN(); + for (int pid = 0 ; pid < hlpn.getPlaces().size() ; pid++) { + if (!torem.contains(hlpn.getPlaces().get(pid).getName())) { + hlSafeNodes.add(pid); + } + } + hlpn.dropAllExcept(hlSafeNodes ); + // System.out.println(hlpn); + } + + + } catch (DeadlockFound e) { + System.out.println( "FORMULA " + reader.getHLPN().getProperties().get(0).getName() + " TRUE TECHNIQUES CPN_APPROX TOPOLOGICAL STRUCTURAL_REDUCTION"); + return null; + } + + } + reader.createSPN(); // remove parameters From c0f23360f4f04109dafa5e3b480daac699768682 Mon Sep 17 00:00:00 2001 From: Yann Thierry-Mieg Date: Wed, 3 Mar 2021 14:24:56 +0100 Subject: [PATCH 42/43] HL places now store their sort name --- .../src/fr/lip6/move/gal/structural/HLPlace.java | 7 ++++++- .../src/fr/lip6/move/gal/structural/SparseHLPetriNet.java | 4 ++-- 2 files changed, 8 insertions(+), 3 deletions(-) diff --git a/fr.lip6.move.gal.structural/src/fr/lip6/move/gal/structural/HLPlace.java b/fr.lip6.move.gal.structural/src/fr/lip6/move/gal/structural/HLPlace.java index beb0273292..8714025a57 100644 --- a/fr.lip6.move.gal.structural/src/fr/lip6/move/gal/structural/HLPlace.java +++ b/fr.lip6.move.gal.structural/src/fr/lip6/move/gal/structural/HLPlace.java @@ -7,10 +7,12 @@ public class HLPlace { int startIndex; private int [] initial; private boolean isConstant = false; - public HLPlace(String name, int start, int [] initial) { + private String sort; + public HLPlace(String name, int start, int [] initial, String sname) { this.name = name; this.startIndex = start; this.initial = initial; + this.sort = sname; } public String getName() { return name; @@ -28,4 +30,7 @@ public boolean isConstant() { public int[] getInitial() { return initial; } + public String getSort() { + return sort; + } } \ No newline at end of file diff --git a/fr.lip6.move.gal.structural/src/fr/lip6/move/gal/structural/SparseHLPetriNet.java b/fr.lip6.move.gal.structural/src/fr/lip6/move/gal/structural/SparseHLPetriNet.java index e991ef27fd..9c48c61a75 100644 --- a/fr.lip6.move.gal.structural/src/fr/lip6/move/gal/structural/SparseHLPetriNet.java +++ b/fr.lip6.move.gal.structural/src/fr/lip6/move/gal/structural/SparseHLPetriNet.java @@ -31,9 +31,9 @@ public int addTransition (String tname, List params, Expression guard) { return transitions.size()-1; } - public int addPlace (String pname, int [] init) { + public int addPlace (String pname, int [] init, String sname) { int index = placeCount; - places.add(new HLPlace(pname, index, init)); + places.add(new HLPlace(pname, index, init, sname)); placeCount += init.length; return places.size()-1; } From 7f5e02534c37ce057cd6f309386a4c405132f3ed Mon Sep 17 00:00:00 2001 From: Yann Thierry-Mieg Date: Wed, 3 Mar 2021 14:54:20 +0100 Subject: [PATCH 43/43] Avoid building order before it is needed The order object has complexity related to unfolded net, we want to avoid building that as much as is possible. This version avoids building it until we want to run SDD on the decomposed GAL, if ever. --- .../move/gal/structural/SparseHLPetriNet.java | 44 ++++++++++++++++ .../move/gal/application/Application.java | 3 ++ .../move/gal/application/MccTranslator.java | 5 +- .../move/gal/pnml/togal/HLSRTransformer.java | 52 +++++-------------- 4 files changed, 64 insertions(+), 40 deletions(-) diff --git a/fr.lip6.move.gal.structural/src/fr/lip6/move/gal/structural/SparseHLPetriNet.java b/fr.lip6.move.gal.structural/src/fr/lip6/move/gal/structural/SparseHLPetriNet.java index 9c48c61a75..fabf1ec5d9 100644 --- a/fr.lip6.move.gal.structural/src/fr/lip6/move/gal/structural/SparseHLPetriNet.java +++ b/fr.lip6.move.gal.structural/src/fr/lip6/move/gal/structural/SparseHLPetriNet.java @@ -3,13 +3,19 @@ import java.util.ArrayDeque; import java.util.ArrayList; import java.util.Arrays; +import java.util.HashMap; import java.util.HashSet; import java.util.List; +import java.util.Map; import java.util.Queue; import java.util.Set; +import java.util.Map.Entry; import java.util.logging.Logger; import android.util.SparseIntArray; +import fr.lip6.move.gal.order.CompositeGalOrder; +import fr.lip6.move.gal.order.IOrder; +import fr.lip6.move.gal.order.VarOrder; import fr.lip6.move.gal.structural.expr.ArrayVarRef; import fr.lip6.move.gal.structural.expr.BinOp; import fr.lip6.move.gal.structural.expr.Expression; @@ -585,6 +591,44 @@ public void dropAllExcept(Set safeNodes) { System.out.println("Prefix of Interest using HLPN skeleton for deadlock discarded "+prem+" places and "+trem + " transitions."); } + + public IOrder computeOrder () { + Map> placeSort = new HashMap<>(); + for (HLPlace p : places) { + placeSort.computeIfAbsent(p.getSort(), v -> new ArrayList<>()).add(p); + } + List orders = new ArrayList<>(); + for (Entry> ps : placeSort.entrySet()) { + List places = ps.getValue(); + if (! places.isEmpty()) + { + //Sort psort = places.get(0).getType().getStructure(); + int sz = places.get(0).getInitial().length; + + if (sz > 1) { + + for (int i=0 ; i < sz ; i++) { + List supp = new ArrayList<>(); + for (HLPlace p : places) { + supp.add( p.getName() +"_" + i); + } + orders.add(new VarOrder(supp, ps.getKey()+i)); + } + } else { + // dot case mostly + for (HLPlace p : places) { + List supp = new ArrayList<>(); + String pname = p.getName(); + supp.add(pname+"_0"); + orders.add(new VarOrder(supp, pname)); + } + } + } + } + IOrder order = new CompositeGalOrder(orders, "main"); + return order; + } + } class HLTrans { 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 b37d8b880f..1f442c20c5 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 @@ -930,6 +930,9 @@ private MccTranslator runMultiITS(String pwd, String examination, String gspnpat if (useManyOrder) reader = reader2.copy(); reader.getSpec().getProperties().removeIf(p->doneProps.containsKey(p.getName())); + if (reader.getHLPN() != null) { + reader.setOrder(reader.getHLPN().computeOrder()); + } reader.flattenSpec(true); if (doITS || onlyGal) { diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/MccTranslator.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/MccTranslator.java index 3e96466601..9425c601a5 100644 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/MccTranslator.java +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/MccTranslator.java @@ -75,6 +75,7 @@ import fr.lip6.move.gal.semantics.IDeterministicNextBuilder; import fr.lip6.move.gal.semantics.INextBuilder; import fr.lip6.move.gal.semantics.NextSupportAnalyzer; +import fr.lip6.move.gal.structural.FlowPrinter; import fr.lip6.move.gal.structural.PropertyType; import fr.lip6.move.gal.structural.SparseHLPetriNet; import fr.lip6.move.gal.structural.SparsePetriNet; @@ -326,7 +327,7 @@ public void loadProperties() throws IOException { } else { parsed = fr.lip6.move.gal.mcc.properties.PropertyParser.fileToProperties(propff , spn, getPropertyType()); } - System.out.println("Parsed " +parsed +" properties from file "+propff+" in "+ (System.currentTimeMillis() - time) + " ms."); + System.out.println("Parsed " +parsed +" properties from file "+propff+" in "+ (System.currentTimeMillis() - time) + " ms."); } } @@ -335,6 +336,7 @@ public void createSPN() { if (hlpn != null) { hlpn.simplifyLogic(); spn = hlpn.unfold(); + FlowPrinter.drawNet(new StructuralReduction(spn), "Unfolded"); } if (DEBUG >= 1) System.out.println("initial properties :" + spn.getProperties()); spn.simplifyLogic(); @@ -484,6 +486,7 @@ public MccTranslator copy() { copy.spec = EcoreUtil.copy(spec); copy.useLouvain = useLouvain; copy.spn = new SparsePetriNet(spn); + copy.hlpn = this.hlpn; return copy ; } diff --git a/pnml/fr.lip6.move.gal.pnml.togal/src/fr/lip6/move/gal/pnml/togal/HLSRTransformer.java b/pnml/fr.lip6.move.gal.pnml.togal/src/fr/lip6/move/gal/pnml/togal/HLSRTransformer.java index 3036bbea8f..5a9a3c9842 100644 --- a/pnml/fr.lip6.move.gal.pnml.togal/src/fr/lip6/move/gal/pnml/togal/HLSRTransformer.java +++ b/pnml/fr.lip6.move.gal.pnml.togal/src/fr/lip6/move/gal/pnml/togal/HLSRTransformer.java @@ -12,9 +12,7 @@ import org.eclipse.emf.common.util.TreeIterator; import org.eclipse.emf.ecore.EObject; -import fr.lip6.move.gal.order.CompositeGalOrder; import fr.lip6.move.gal.order.IOrder; -import fr.lip6.move.gal.order.VarOrder; import fr.lip6.move.gal.pnml.togal.utils.EqualityHelperUpToPerm; import fr.lip6.move.gal.pnml.togal.utils.HLUtils; import fr.lip6.move.gal.pnml.togal.utils.Utils; @@ -72,6 +70,8 @@ public class HLSRTransformer { + private static final int DEBUG = 0; + private static Logger getLog() { return Logger.getLogger("fr.lip6.move.gal"); } @@ -95,8 +95,8 @@ public SparseHLPetriNet transform(PetriNet pn) { private void handlePage(Page page, SparseHLPetriNet res) { long time = System.currentTimeMillis(); - Map> placeSort = new HashMap<>(); Map placeMap = new HashMap<>(); + Map> placeSort = new HashMap<>(); for (PnObject n : page.getObjects()) { if (n instanceof Place) { Place p = (Place) n; @@ -106,50 +106,24 @@ private void handlePage(Page page, SparseHLPetriNet res) { placeSort.computeIfAbsent(sname, v -> new ArrayList<>()).add(p); int[] value = interpretMarking(p.getHlinitialMarking(),psort); - int index = res.addPlace(Utils.normalizeName(p.getId()), value); + int index = res.addPlace(Utils.normalizeName(p.getId()), value, Utils.normalizeName(sname)); placeMap.put(p, index); } } - StringBuilder sb = new StringBuilder(); - for (Entry> r : placeSort.entrySet()) { - sb.append(r.getKey() +"->"); - for (Place p : r.getValue()) { - sb.append(p.getId() +","); - } - sb.append("\n"); - } - getLog().info("sort/places :\n" +sb.toString()); - List orders = new ArrayList(); - for (Entry> ps : placeSort.entrySet()) { - List places = ps.getValue(); - if (! places.isEmpty()) - { - Sort psort = places.get(0).getType().getStructure(); - int sz = computeSortCardinality(psort); - - if (sz > 1) { - - for (int i=0 ; i < sz ; i++) { - List supp = new ArrayList<>(); - for (Place p : places) { - supp.add( res.getPlaces().get(placeMap.get(p)).getName() +"_" + i); - } - orders.add(new VarOrder(supp, Utils.normalizeName(ps.getKey()+i))); - } - } else { - // dot case mostly - for (Place p : places) { - List supp = new ArrayList<>(); - String pname = res.getPlaces().get(placeMap.get(p)).getName(); - supp.add(pname+"_0"); - orders.add(new VarOrder(supp, pname)); - } + if (DEBUG >= 1) { + StringBuilder sb = new StringBuilder(); + for (Entry> r : placeSort.entrySet()) { + sb.append(r.getKey() +"->"); + for (Place p : r.getValue()) { + sb.append(p.getId() +","); } + sb.append("\n"); } + getLog().info("sort/places :\n" +sb.toString()); } - order = new CompositeGalOrder(orders, "main"); + Set constPlaces = new HashSet<>(); for (int i=0; i < res.getPlaces().size() ; i++) { constPlaces.add(i);