From 7278d32089422476cd28e634b377195d359d31e1 Mon Sep 17 00:00:00 2001 From: Yann Thierry-Mieg Date: Wed, 5 Jun 2024 13:52:51 +0200 Subject: [PATCH] code supporting the DD vs SMT analysis --- .../src/smtanalysis/DDrunner.java | 102 ++++++++++++++++++ .../src/smtanalysis/SMTAnalyzer.java | 61 +++++++++++ 2 files changed, 163 insertions(+) create mode 100644 pnmcc/fr.lip6.move.gal.application.pnmcc/src/smtanalysis/DDrunner.java create mode 100644 pnmcc/fr.lip6.move.gal.application.pnmcc/src/smtanalysis/SMTAnalyzer.java diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/smtanalysis/DDrunner.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/smtanalysis/DDrunner.java new file mode 100644 index 0000000000..9e3f70c8ac --- /dev/null +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/smtanalysis/DDrunner.java @@ -0,0 +1,102 @@ +package smtanalysis; + +import java.io.BufferedReader; +import java.io.File; +import java.io.IOException; +import java.nio.file.Files; +import java.util.concurrent.TimeUnit; +import java.util.concurrent.TimeoutException; + +import fr.lip6.move.gal.application.mcc.MccTranslator; +import fr.lip6.move.gal.itstools.BinaryToolsPlugin.Tool; +import fr.lip6.move.gal.mcc.properties.ConcurrentHashDoneProperties; +import fr.lip6.move.gal.itstools.CommandLineBuilder; +import fr.lip6.move.gal.process.CommandLine; +import fr.lip6.move.gal.process.Runner; +import fr.lip6.move.serialization.SerializationUtil; + +public class DDrunner { + + private static final int DEBUG = 1; + private MccTranslator reader; + private String workFolder; + private long timeout; + private CommandLine cl; + private String smtFile; + + public DDrunner(MccTranslator reader, String workFolder, long timeout) { + this.reader = reader; + this.workFolder = workFolder; + this.timeout = timeout; + } + + public String outputGalFile() throws IOException { + File file = Files.createTempFile("ddtosmt", ".gal").toFile(); + if (DEBUG == 0) + file.deleteOnExit(); + String outpath = file.getCanonicalPath(); + SerializationUtil.systemToFile(reader.getSpec(), outpath, false); + return outpath; + } + + public String getSmtFile() { + return smtFile; + } + + public void run() throws IOException { + buildCommandLine(); + + ProcessBuilder pb = new ProcessBuilder(cl.getArgs()); + pb.directory(cl.getWorkingDir()); + pb.redirectErrorStream(true); + + System.out.println("Invoking ITS tools like this :" + cl); + try { + final Process process = pb.start(); + + Thread runnerThread = new Thread(() -> { + try { + int status = Runner.waitForOrTimeout(timeout, TimeUnit.SECONDS, cl, process); + if (status != 0) { + System.err.println("ITS-tools command line returned an error code " + status); + } else { + try (BufferedReader in = process.inputReader()) { + while (in.ready()) { + String line = in.readLine(); + System.out.println(line); + } + } catch (IOException e) { + System.out.println("Error reading output of ITS tools." + e); + } + } + } catch (InterruptedException e) { + System.out.println("ITS tools runne²r thread asked to quit. Dying gracefully."); + return; + } catch (TimeoutException e) { + System.out.println("Detected timeout of ITS tools."); + return; + } + }); + runnerThread.start(); + + } catch (IOException e) { + System.out.println("Failure when invoking ITS tools." + e); + return; + } + } + + public void buildCommandLine() throws IOException { + CommandLineBuilder clb = new CommandLineBuilder(Tool.reach); + reader.createSPN(true, true); + reader.rebuildSpecification(new ConcurrentHashDoneProperties()); + String modelff = outputGalFile(); + clb.setModelFile(modelff); + clb.setModelType("CGAL"); + cl = clb.getCommandLine(); + cl.addArg("-exportsmt"); + smtFile = new File(workFolder, "model.smt2").getCanonicalPath(); + cl.addArg(smtFile); + cl.setWorkingDir(new File(workFolder)); + } + +} diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/smtanalysis/SMTAnalyzer.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/smtanalysis/SMTAnalyzer.java new file mode 100644 index 0000000000..ca9f463503 --- /dev/null +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/smtanalysis/SMTAnalyzer.java @@ -0,0 +1,61 @@ +package smtanalysis; + +import java.io.IOException; +import java.util.ArrayList; +import java.util.List; + +import org.smtlib.SMT; + +import android.util.SparseBoolArray; +import fr.lip6.move.gal.application.mcc.MccTranslator; +import fr.lip6.move.gal.mcc.properties.ConcurrentHashDoneProperties; +import fr.lip6.move.gal.mcc.properties.DoneProperties; +import fr.lip6.move.gal.structural.SparsePetriNet; +import fr.lip6.move.gal.structural.smt.Problem; +import fr.lip6.move.gal.structural.smt.ProblemSet; +import fr.lip6.move.gal.structural.smt.SMTBasedReachabilitySolver; +import fr.lip6.move.gal.structural.smt.VarSet; + +public class SMTAnalyzer { + + public void analyze(MccTranslator reader, String workFolder) { + // step 0 : unfold, rename net places to indexed form + SparsePetriNet spn = reader.getSPN(); + toIndexedNames(spn); + + // step 1 : invoke DD based tool (120 secs timeout) + DDrunner runner = new DDrunner(reader, workFolder, 120); + try { + runner.run(); + } catch (IOException e) { + e.printStackTrace(); + } + String smtFile = runner.getSmtFile(); + + VarSet support = new VarSet(); + SparseBoolArray sball = new SparseBoolArray(spn.getPlaceCount(), true); + support.addVars("s", sball ); + Problem p = new Problem("complete",smtFile, SMT.instance.smtConfig.exprFactory.symbol("unreachable"), support); + + DoneProperties done = new ConcurrentHashDoneProperties(); + ProblemSet problems = new ProblemSet(done); + problems.addProblem(p); + + List repr = new ArrayList<>(); + SMTBasedReachabilitySolver.solveProblems(problems, spn, 300, true, repr); + + System.out.println(problems); + } + + private void toIndexedNames(SparsePetriNet spn) { + List names = spn.getPnames(); + for (int index =0; index < names.size() ; index++) { + names.set(index, "s"+index); + } + names = spn.getTnames(); + for (int index =0; index < names.size() ; index++) { + names.set(index, "t"+index); + } + } + +}