filter formulas based on examination

lip6 · Jul 4, 2024 · ed8570b · ed8570b
1 parent dd4af97
commit ed8570b
Showing 1 changed file with 18 additions and 0 deletions.
diff --git a/mist/fr.lip6.converter/src/main/java/fr/lip6/converter/ConverterMain.java b/mist/fr.lip6.converter/src/main/java/fr/lip6/converter/ConverterMain.java
@@ -18,13 +18,15 @@
 import fr.lip6.move.gal.mcc.properties.MCCExporter;
 import fr.lip6.move.gal.structural.FlowPrinter;
 import fr.lip6.move.gal.structural.Property;
+import fr.lip6.move.gal.structural.PropertyType;
 import fr.lip6.move.gal.structural.SparsePetriNet;
 import fr.lip6.move.gal.structural.pnml.PTNetReader;
 
 public class ConverterMain {
 
 	private static final String CONVERT_FLAG = "-convert";
 	private static final String FORMULA_FLAG = "-formula";
+	private static final String EXAMINATION_FLAG = "-examination";
 	private static final String OUT_FOLDER = "-o";
 	private static final String DOT_OUT = "-dot";
 	private static final String SELT_FLAG = "-selt";
@@ -41,12 +43,15 @@ public static void main(String[] args) {
 		boolean doDotOutput=false;
 		boolean isFormula = false;
 		int firstSelt = -1;
+		String exam = null;
 		for (int i=0; i < args.length ; i++) {
 			if (CONVERT_FLAG.equals(args[i])) {
 				ff = args[++i];
 			} else if (FORMULA_FLAG.equals(args[i])) {
 				ff = args[++i];
 				isFormula = true;
+			} else if (EXAMINATION_FLAG.equals(args[i])) {
+				exam = args[++i];
 			} else if (OUT_FOLDER.equals(args[i])) {
 				folder = args[++i];
 			} else if (DOT_OUT.equals(args[i])) {
@@ -80,6 +85,19 @@ public static void main(String[] args) {
 				Map<String, Integer> vars = new HashMap<>();
 				List<Property> props = pi.parseFile(ff, vars);
 				System.out.println("Parsed properties :" + props);
+				if (exam != null) {
+					if (exam.startsWith("UpperBounds")) {
+						props.removeIf(p -> p.getType() != PropertyType.BOUNDS);
+					} else if (exam.startsWith("Reachability")) {
+						props.removeIf(p -> p.getType() != PropertyType.INVARIANT);
+					} else if (exam.startsWith("CTL")) {
+						props.removeIf(p -> p.getType() != PropertyType.CTL);
+					} else if (exam.startsWith("LTL")) {
+						props.removeIf(p -> p.getType() != PropertyType.LTL);
+					} else {
+						System.err.println("Unknown examination type "+exam + " not filtering formulas.");
+					}
+				}
 				PropertiesToPNML.transform(props, vars, folder + "/properties.xml");
 			} catch (IOException e) {
 				e.printStackTrace();