Skip to content

Commit

Permalink
use more general exceptions + catch them
Browse files Browse the repository at this point in the history
  • Loading branch information
@yanntm
yanntm committed Apr 16, 2021
1 parent 3a7f3a1 commit 8c2af0d
Show file tree
Hide file tree
Showing 3 changed files with 105 additions and 98 deletions.
5 changes: 2 additions & 3 deletions pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/Application.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -46,9 +46,8 @@
import fr.lip6.move.gal.mcc.properties.PropertiesToPNML;
import fr.lip6.move.gal.semantics.IDeterministicNextBuilder;
import fr.lip6.move.gal.semantics.INextBuilder;
import fr.lip6.move.gal.structural.DeadlockFound;
import fr.lip6.move.gal.structural.GlobalPropertySolvedException;
import fr.lip6.move.gal.structural.InvariantCalculator;
import fr.lip6.move.gal.structural.NoDeadlockExists;
import fr.lip6.move.gal.structural.SparsePetriNet;
import fr.lip6.move.gal.structural.StructuralReduction;
import fr.lip6.move.gal.structural.expr.Expression;
Expand Down Expand Up @@ -694,7 +693,7 @@ private void regeneratePNML(MccTranslator reader, DoneProperties doneProps, Stri
System.out.println("For property " + prop.getName() + " final size "
+ ((GALTypeDeclaration) copy.getSpec().getTypes().get(0)).getVariables().size());
}
} catch (NoDeadlockExists | DeadlockFound e) {
} catch (GlobalPropertySolvedException e) {
e.printStackTrace();
}
}
Expand Down
180 changes: 91 additions & 89 deletions ...ip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/GlobalPropertySolver.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -15,10 +15,10 @@
import fr.lip6.move.gal.mcc.properties.DoneProperties;
import fr.lip6.move.gal.structural.DeadlockFound;
import fr.lip6.move.gal.structural.FlowPrinter;
import fr.lip6.move.gal.structural.GlobalPropertySolvedException;
import fr.lip6.move.gal.structural.HLPlace;
import fr.lip6.move.gal.structural.ISparsePetriNet;
import fr.lip6.move.gal.structural.InvariantCalculator;
import fr.lip6.move.gal.structural.NoDeadlockExists;
import fr.lip6.move.gal.structural.PetriNet;
import fr.lip6.move.gal.structural.Property;
import fr.lip6.move.gal.structural.PropertyType;
Expand Down Expand Up @@ -117,7 +117,7 @@ private boolean[] computeDominatedTransitions(PetriNet pn) {
if (pn instanceof ISparsePetriNet) {
ISparsePetriNet spn = (ISparsePetriNet) pn;
IntMatrixCol tflowPT = spn.getFlowPT().transpose();

for (int pid = 0, pide = spn.getPlaceCount(); pid < pide; pid++) {
SparseIntArray tpt = tflowPT.getColumn(pid);
List<Integer> consumers = Arrays.stream(tpt.copyKeys()).boxed().collect(Collectors.toList());
Expand Down Expand Up @@ -164,7 +164,7 @@ public Optional<Boolean> solveProperty(String examination, MccTranslator reader)
DoneProperties doneProps = new GlobalDonePropertyPrinter(examination, true);
return preSolveLiveness(examination, reader, doneProps);
}

public Optional<Boolean> preSolveLiveness(String examination, MccTranslator reader, DoneProperties doneProps) {

if (LIVENESS.equals(examination)) {
Expand Down Expand Up @@ -195,15 +195,15 @@ public Optional<Boolean> preSolveLiveness(String examination, MccTranslator read
}
}


{
// call for liveness exhaustive evaluation (using definiton)
if (reader.getHLPN() != null)
buildLivenessProperty(reader.getHLPN());
else
buildLivenessProperty(reader.getSPN());
}

reader.createSPN(false, false);
{
if (!isCol && !executeSCCLivenessTest(reader.getSPN(),null)) {
Expand Down Expand Up @@ -237,7 +237,7 @@ public Optional<Boolean> preSolveLiveness(String examination, MccTranslator read
MccTranslator readercopy = reader.copy();
readercopy.getSPN().getProperties().clear();
Optional<Boolean> qlResult = solveProperty(QUASI_LIVENESS, readercopy, new GlobalDonePropertyPrinter(QUASI_LIVENESS, false));

if (qlResult.isPresent() && ! qlResult.get()) {
System.out.println("FORMULA " + examination + " FALSE TECHNIQUES QUASILIVENESS_TEST");
return Optional.of(false);
Expand Down Expand Up @@ -309,63 +309,63 @@ public boolean executeSCCLivenessTest(SparsePetriNet spn, List<List<Integer>> en
}

private Optional<Boolean> solveProperty(String examination, MccTranslator reader, DoneProperties doneProps) {

if (!LIVENESS.equals(examination)) {
if (reader.getHLPN() != null) {

buildProperties(examination, reader.getHLPN());

if (ONE_SAFE.equals(examination)) {
for (HLPlace place : reader.getHLPN().getPlaces()) {
int[] initial = place.getInitial();
int sum = Arrays.stream(initial).sum();
if (sum > 1) {
System.out.println(
"FORMULA " + examination + " FALSE TECHNIQUES STRUCTURAL INITIAL_STATE CPN_APPROX");
return Optional.of(false);
try {
if (!LIVENESS.equals(examination)) {
if (reader.getHLPN() != null) {

buildProperties(examination, reader.getHLPN());

if (ONE_SAFE.equals(examination)) {
for (HLPlace place : reader.getHLPN().getPlaces()) {
int[] initial = place.getInitial();
int sum = Arrays.stream(initial).sum();
if (sum > 1) {
System.out.println(
"FORMULA " + examination + " FALSE TECHNIQUES STRUCTURAL INITIAL_STATE CPN_APPROX");
return Optional.of(false);
}
}
}
}

}
}

boolean isSafe = false;
// load "known" stuff about the model
if (reader.isSafeNet()) {
// NUPN implies one safe
if (examination.equals(ONE_SAFE)) {
System.out.println("FORMULA " + examination + " TRUE TECHNIQUES STRUCTURAL");
return Optional.of(true);
boolean isSafe = false;
// load "known" stuff about the model
if (reader.isSafeNet()) {
// NUPN implies one safe
if (examination.equals(ONE_SAFE)) {
System.out.println("FORMULA " + examination + " TRUE TECHNIQUES STRUCTURAL");
return Optional.of(true);
}
isSafe = true;
}
if (QUASI_LIVENESS.equals(examination) || STABLE_MARKING.equals(examination)|| LIVENESS.equals(examination)) {
reader.createSPN(false, false);
} else {
reader.createSPN();
}
isSafe = true;
}
if (QUASI_LIVENESS.equals(examination) || STABLE_MARKING.equals(examination)|| LIVENESS.equals(examination)) {
reader.createSPN(false, false);
} else {
reader.createSPN();
// switching examination
if (reader.getHLPN() == null) {
reader.getSPN().getProperties().clear();
if (examination.equals(LIVENESS) || examination.equals(QUASI_LIVENESS)) {
StructuralReduction sr = new StructuralReduction(reader.getSPN());
try {
ReachabilitySolver.applyReductions(sr, ReductionType.LIVENESS, solverPath, reader.isSafeNet(), true, true);
//sr.reduce(ReductionType.LIVENESS);
} catch (DeadlockFound e) {
doneProps.put(examination, false, "STRUCTURAL_REDUCTION");
return Optional.of(false);
} catch (GlobalPropertySolvedException e) {
e.printStackTrace();
}
reader.getSPN().readFrom(sr);
}
buildProperties(examination, reader.getSPN());
}
}
// switching examination
if (reader.getHLPN() == null) {
reader.getSPN().getProperties().clear();
if (examination.equals(LIVENESS) || examination.equals(QUASI_LIVENESS)) {
StructuralReduction sr = new StructuralReduction(reader.getSPN());
try {
ReachabilitySolver.applyReductions(sr, ReductionType.LIVENESS, solverPath, reader.isSafeNet(), true, true);
//sr.reduce(ReductionType.LIVENESS);
} catch (DeadlockFound e) {
doneProps.put(examination, false, "STRUCTURAL_REDUCTION");
return Optional.of(false);
} catch (NoDeadlockExists e) {
e.printStackTrace();
}
reader.getSPN().readFrom(sr);
}
buildProperties(examination, reader.getSPN());
}

SparsePetriNet spn = reader.getSPN();
try {
SparsePetriNet spn = reader.getSPN();

spn.simplifyLogic();
spn.toPredicates();
if (spn.testInInitial() > 0) {
Expand Down Expand Up @@ -393,41 +393,43 @@ private Optional<Boolean> solveProperty(String examination, MccTranslator reader

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

} catch (GlobalPropertySolverException e) {
return Optional.of(e.verdict);
}

if (! spn.getProperties().isEmpty()) {
if (LIVENESS.equals(examination)) {
verifyWithCTL(reader, doneProps, "CTLFireability");
} else {
verifyWithCTL(reader, doneProps, "ReachabilityFireability");


if (! spn.getProperties().isEmpty()) {
if (LIVENESS.equals(examination)) {
verifyWithCTL(reader, doneProps, "CTLFireability");
} else {
verifyWithCTL(reader, doneProps, "ReachabilityFireability");
}
}
}

if (doneProps.containsKey(examination)) {
return Optional.of(doneProps.getValue(examination));
}

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

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

GlobalDonePropertyPrinter gdpp = (GlobalDonePropertyPrinter) doneProps;
if (gdpp.shouldTrace()) {
if (success)
System.out.println("FORMULA " + examination + " TRUE TECHNIQUES " + gdpp.computeTechniques());
else
System.out.println("FORMULA " + examination + " FALSE TECHNIQUES " + gdpp.computeTechniques());
if (doneProps.containsKey(examination)) {
return Optional.of(doneProps.getValue(examination));
}
return Optional.of(success);

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

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

GlobalDonePropertyPrinter gdpp = (GlobalDonePropertyPrinter) doneProps;
if (gdpp.shouldTrace()) {
if (success)
System.out.println("FORMULA " + examination + " TRUE TECHNIQUES " + gdpp.computeTechniques());
else
System.out.println("FORMULA " + examination + " FALSE TECHNIQUES " + gdpp.computeTechniques());
}
return Optional.of(success);
}

} catch (GlobalPropertySolverException e) {
return Optional.of(e.verdict);
}
}

Expand Down Expand Up @@ -478,7 +480,7 @@ private void verifyWithCTL(MccTranslator reader, DoneProperties doneProps, Strin

// timeout 1000 secs ?
int timeout = 1000;

try {
// decompose + simplify as needed
IRunner itsRunner = new ITSRunner(examinationForITS, reader, true, false, reader.getFolder(), timeout,
Expand All @@ -502,7 +504,7 @@ private void applyReachabilitySolver(MccTranslator reader, DoneProperties donePr
try {
ReachabilitySolver.checkInInitial(reader.getSPN(), doneProps);
ReachabilitySolver.applyReductions(reader, doneProps, solverPath, isSafe);
} catch (NoDeadlockExists | DeadlockFound e) {
} catch (GlobalPropertySolvedException e) {
e.printStackTrace();
}
}
Expand Down
18 changes: 12 additions & 6 deletions ....lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/ReachabilitySolver.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@
import android.util.SparseIntArray;
import fr.lip6.move.gal.mcc.properties.DoneProperties;
import fr.lip6.move.gal.structural.DeadlockFound;
import fr.lip6.move.gal.structural.NoDeadlockExists;
import fr.lip6.move.gal.structural.GlobalPropertySolvedException;
import fr.lip6.move.gal.structural.PetriNet;
import fr.lip6.move.gal.structural.PropertyType;
import fr.lip6.move.gal.structural.RandomExplorer;
Expand Down Expand Up @@ -37,7 +37,7 @@ public static int checkInInitial(PetriNet pn, DoneProperties doneProps) {
}

public static void applyReductions(MccTranslator reader, DoneProperties doneProps, String solverPath, boolean isSafe)
throws NoDeadlockExists, DeadlockFound {
throws GlobalPropertySolvedException {
int iter;
int iterations =0;
boolean doneAtoms = false;
Expand Down Expand Up @@ -312,7 +312,7 @@ private static int interpretVerdict(List<Expression> tocheck, SparsePetriNet spn
}

public static boolean applyReductions(StructuralReduction sr, ReductionType rt, String solverPath, boolean isSafe, boolean withSMT, boolean isFirstTime)
throws NoDeadlockExists, DeadlockFound {
throws GlobalPropertySolvedException {
boolean cont = false;
int it =0;
int initp = sr.getPnames().size();
Expand All @@ -337,7 +337,7 @@ public static boolean applyReductions(StructuralReduction sr, ReductionType rt,
// 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);
boolean hasReduced = arcValuesTriggerSMTDeadTransitions(sr, solverPath, isSafe,rt);
if (hasReduced) {
cont=true;
total++;
Expand All @@ -363,7 +363,7 @@ public static boolean applyReductions(StructuralReduction sr, ReductionType rt,
}

private static boolean applySMTBasedReductionRules(StructuralReduction sr, ReductionType rt, int iteration,
String solverPath, boolean isSafe, int reduced) throws NoDeadlockExists {
String solverPath, boolean isSafe, int reduced) throws GlobalPropertySolvedException {
boolean hasReduced = false;
boolean useStateEq = false;
if (reduced > 0 || iteration ==0) {
Expand Down Expand Up @@ -406,6 +406,9 @@ private static boolean applySMTBasedReductionRules(StructuralReduction sr, Reduc
if (! tokill.isEmpty()) {
System.out.println("Found "+tokill.size()+ " dead transitions using SMT." );
}
if (rt == ReductionType.LIVENESS) {
throw new DeadlockFound();
}
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);
Expand All @@ -415,7 +418,7 @@ private static boolean applySMTBasedReductionRules(StructuralReduction sr, Reduc
return hasReduced;
}

private static boolean arcValuesTriggerSMTDeadTransitions(StructuralReduction sr, String solverPath, boolean isSafe) {
private static boolean arcValuesTriggerSMTDeadTransitions(StructuralReduction sr, String solverPath, boolean isSafe, ReductionType rt) throws DeadlockFound {
boolean hasGT1ArcValues = false;
for (int t=0,te=sr.getTnames().size() ; t < te && !hasGT1ArcValues; t++) {
SparseIntArray col = sr.getFlowPT().getColumn(t);
Expand All @@ -435,6 +438,9 @@ private static boolean arcValuesTriggerSMTDeadTransitions(StructuralReduction sr
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);
if (rt == ReductionType.LIVENESS) {
throw new DeadlockFound();
}
return true;
}
}
Expand Down

0 comments on commit 8c2af0d

Please sign in to comment.