-hsc for CTL: libHSC's symbolic checker runs beside its-ctl and the PetriSpot walk on the CTL examinations — HscRunner.runCtl writes (ctl prop<i> f) forms and streams the FORMULA lines, ParallelWalk.startHscCtl publishes them to DoneProperties

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>

Author: yanntm

hsc/fr.lip6.move.hsc.runner/src/fr/lip6/move/hsc/runner/HscRunner.java

@@ -258,6 +258,34 @@ public static Verdicts run(ISparsePetriNet net, List<String> forms, int totalSec
 		}
 	}
 
+	/**
+	 * The CTL formulas at the initial marking, by libHSC's symbolic checker
+	 * (forward form over the saturated reachable set, the inverse relation for
+	 * what the forward form leaves). One (ctl prop&lt;i&gt; formula) form per
+	 * property; hsc-pn runs them in rounds of growing per-property budget under
+	 * totalSeconds, so the cheap ones come first. Verdicts stream to the
+	 * listener as FORMULA lines arrive; a formula the checker leaves open has
+	 * no verdict.
+	 *
+	 * @return one verdict per formula, or null when the binary could not run
+	 */
+	public static Verdicts runCtl(ISparsePetriNet net, List<Expression> formulas, int totalSeconds, Shape shape,
+			boolean force, Listener listener) {
+		if (formulas.isEmpty()) {
+			return new Verdicts(0);
+		}
+		List<String> forms = new ArrayList<>(formulas.size());
+		try {
+			for (int i = 0; i < formulas.size(); i++) {
+				forms.add(SexprPropertyPrinter.ctl("prop" + i, formulas.get(i)));
+			}
+		} catch (UnsupportedOperationException e) {
+			System.out.println("hsc-pn CTL skipped: " + e.getMessage());
+			return null;
+		}
+		return run(net, forms, totalSeconds, shape, force, listener);
+	}
+
 	/** The bundled binary, or the one named by the system property hsc.bin (tests outside OSGi). */
 	private static String binaryPath() throws IOException {
 		String override = System.getProperty("hsc.bin");

pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/Application.java

@@ -50,6 +50,7 @@
 import fr.lip6.move.gal.application.runner.spot.SpotRunner;
 import fr.lip6.move.gal.application.solver.ExclusiveImplicantsComputer;
 import fr.lip6.move.gal.application.solver.GALSolver;
+import fr.lip6.move.gal.application.solver.ParallelWalk;
 import fr.lip6.move.gal.application.solver.ReachabilitySolver;
 import fr.lip6.move.gal.application.solver.UpperBoundsSolver;
 import fr.lip6.move.gal.application.solver.ExclusiveImplicantsComputer.Constraint;
@@ -361,6 +362,7 @@ public Object startNoEx(String[] args) throws Exception {
 				doITS = true;
 			} else if (HSC.equals(args[i])) {
 				doHSC = true;
+				ParallelWalk.HSC_CTL = true;
 			} else if (HSC_BENCH.equals(args[i])) {
 				hscBench = true;
 			} else if (HSC_BENCH_REDUCE.equals(args[i])) {

pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/solver/ParallelWalk.java

@@ -11,6 +11,7 @@
 import fr.lip6.move.gal.structural.StructuralReduction;
 import fr.lip6.move.gal.structural.expr.Expression;
 import fr.lip6.move.petrispot.runner.PetriSpotWalker;
+import fr.lip6.move.hsc.runner.HscRunner;
 
 /**
  * A PetriSpot walk running beside a decision diagram attempt.
@@ -35,6 +36,12 @@ public class ParallelWalk {
 	/** Whether a walk accompanies every decision diagram attempt. */
 	public static final boolean ENABLED = true;
 
+	/**
+	 * Whether libHSC's symbolic CTL checker (hsc-pn) also runs beside a CTL
+	 * attempt, on the same reduced net: set by the -hsc flag.
+	 */
+	public static boolean HSC_CTL = false;
+
 	/** Cores left to the walk. The diagram engine uses one of the four. */
 	private static final int THREADS = 3;
 
@@ -141,9 +148,41 @@ public void formula(int index, String value, String techniques) {
 		}, "petrispot-ctl-beside-dd");
 		thread.setDaemon(true);
 		thread.start();
+		if (HSC_CTL) {
+			startHscCtl(sr, props, formulas, doneProps, seconds);
+		}
 		return new ParallelWalk(thread, cancel);
 	}
 
+	/**
+	 * libHSC's symbolic CTL checker beside a CTL attempt (-hsc): the same
+	 * reduced net and formulas go to hsc-pn, whose verdicts are proofs and
+	 * land in doneProps as they stream. Bounded by seconds like the walk; not
+	 * cancelled with it, the process ends with its budget.
+	 */
+	private static void startHscCtl(StructuralReduction sr, List<Property> props, List<Expression> formulas,
+			DoneProperties doneProps, int seconds) {
+		HscRunner.Listener listener = (index, value, techniques) -> {
+			try {
+				doneProps.put(props.get(index).getName(), "TRUE".equals(value), "DECISION_DIAGRAMS SATURATION HSC");
+			} catch (GlobalPropertySolverException e) {
+				// the verdict decided the whole examination: the printer has said so
+			}
+		};
+		Thread thread = new Thread(() -> {
+			try {
+				HscRunner.Verdicts v = HscRunner.runCtl(sr, formulas, seconds, HscRunner.Shape.LOUVAIN, true, listener);
+				if (v != null && v.solved() > 0) {
+					System.out.println("libHSC CTL check beside the decision diagrams solved " + v.solved() + " properties.");
+				}
+			} catch (RuntimeException e) {
+				System.out.println("libHSC CTL check beside the decision diagrams failed : " + e.getMessage());
+			}
+		}, "hsc-ctl-beside-dd");
+		thread.setDaemon(true);
+		thread.start();
+	}
+
 	/** Stop the walk and wait for its verdicts to be published. */
 	public void stop() {
 		cancel.cancel();