From 97c91486d89c265897550433e8abde5639ea8305 Mon Sep 17 00:00:00 2001
From: Yann Thierry-Mieg <Yann.Thierry-Mieg@lip6.fr>
Date: Thu, 2 Mar 2023 16:03:33 +0100
Subject: [PATCH] use the correctly implemented ltlsolve primitive rather than
 mess up

---
 .../solver/ltl/LTLLengthAwareSolver.java      | 38 +------------------
 1 file changed, 2 insertions(+), 36 deletions(-)

diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/solver/ltl/LTLLengthAwareSolver.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/solver/ltl/LTLLengthAwareSolver.java
index fa41334b3a..5924573968 100644
--- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/solver/ltl/LTLLengthAwareSolver.java
+++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/solver/ltl/LTLLengthAwareSolver.java
@@ -83,46 +83,12 @@ public int runSLCLLTLTest(MccTranslator reader, DoneProperties doneProps)
 
 				System.out.println("Found a " + (tgba.isSLInvariant() ? "Lengthening":"Shortening") + " insensitive property : " + propPN.getName());
 
+				
 				// annotate it with Infinite Stutter Accepted Formulas
 				spot.computeInfStutter(tgba);
 
 				// build a new copy of the model
-				SparsePetriNet spn = new SparsePetriNet(reader.getSPN());
-
-				// get rid of other properties
-				spn.getProperties().clear();
-				spn.getProperties().add(propPN.copy());
-
-				// compute supporting variables of the AP in the TGBA
-				BitSet support = new BitSet();
-				List<AtomicProp> aps = tgba.getAPs();
-				for (AtomicProp ap : aps) {
-					PetriNet.addSupport(ap.getExpression(),support);
-				}
-
-				System.out.println("Support contains "+support.cardinality() + " out of " + spn.getPnames().size() + " places. Attempting structural reductions.");
-
-				// run reduction rules in LengthInsensitive mode
-				StructuralReduction sr = new StructuralReduction(spn);
-				sr.setProtected(support);
-				try {
-					ReductionType rt = ReductionType.LI_LTL ;
-					ReachabilitySolver.applyReductions(sr, rt, true, true);
-				} catch (GlobalPropertySolvedException gse) {
-					System.out.println("Unexpected exception when reducing for LTL :" +gse.getMessage());
-					gse.printStackTrace();
-				}
-
-				// rebuild and reinterpret the reduced net
-				// index of places may have changed, formula might be syntactically simpler
-				// recompute fresh tgba with correctly indexed AP referring to the *reduced* model
-				List<Expression> atoms = aps.stream().map(ap -> ap.getExpression()).collect(Collectors.toList());
-				List<Expression> atoms2 = spn.readFrom(sr,atoms);
-				// we can maybe simplify some predicates now : apply some basic tests
-				spn.removeConstantPlaces(atoms2);
-				for (int i =0,ie=atoms.size(); i<ie; i++) {
-					aps.get(i).setExpression(atoms2.get(i));
-				}
+				SparsePetriNet spn = ltlsolve.reduceForProperty(reader.getSPN(), tgba, ReductionType.LI_LTL, propPN);
 
 				// we might have solved the property syntactically thanks to reductions.
 				if (doneProps.containsKey(propPN.getName()))