Skip to content

Commit 1ce069d

Browse files
yanntmyanntm
committed
small changes to enable better debugging of LTSmin calls
1 parent 05048bc commit 1ce069d

9 files changed

Lines changed: 83 additions & 115 deletions

File tree

‎fr.lip6.move.gal.structural/src/fr/lip6/move/gal/structural/expr/CExpressionPrinter.java‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@
22

33
import java.io.PrintWriter;
44

5-
public class CExpressionPrinter implements ExprVisitor<Void> {
5+
public class CExpressionPrinter implements ExprVisitor<Void>, AutoCloseable {
66

77
private String prefix;
88
protected PrintWriter pw;

‎pins/fr.lip6.move.gal.gal2pins/src/fr/lip6/move/gal/gal2pins/Gal2PinsTransformerNext.java‎

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -798,7 +798,8 @@ public Boolean caseLTLGlobally(LTLGlobally object) {
798798
private List<AtomicProp> atoms = new ArrayList<>();
799799
private Map<BooleanExpression, AtomicProp> atomMap = new HashMap<BooleanExpression, AtomicProp>();
800800
private boolean isSafe;
801-
public void transform (Specification spec, String cwd, boolean withPorMatrix, boolean isSafe) {
801+
802+
public void transform (Specification spec, String cwd, boolean withPorMatrix, boolean isSafe, List<File> todel) {
802803
this.isSafe = isSafe;
803804
// if ( spec.getMain() instanceof GALTypeDeclaration ) {
804805
// Logger.getLogger("fr.lip6.move.gal").fine("detecting pure GAL");
@@ -863,6 +864,9 @@ public void transform (Specification spec, String cwd, boolean withPorMatrix, bo
863864

864865
buildHeader(cwd + "/model.h");
865866

867+
todel.add(new File(cwd + "/model.c"));
868+
todel.add(new File(cwd + "/model.h"));
869+
866870
Logger.getLogger("fr.lip6.move.gal").info("Built C files in "+ (System.currentTimeMillis()- time ) + "ms conformant to PINS in folder :"+cwd);
867871
} catch (IOException e) {
868872
// TODO Auto-generated catch block

‎pins/fr.lip6.move.gal.gal2pins/src/fr/lip6/move/gal/gal2pins/Test.java‎

Lines changed: 14 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,11 @@
11
package fr.lip6.move.gal.gal2pins;
22

33

4+
import java.io.File;
5+
import java.io.IOException;
6+
import java.util.ArrayList;
7+
import java.util.List;
8+
49
import fr.lip6.move.gal.Specification;
510
import fr.lip6.move.gal.gal2smt.Gal2SMTFrontEnd;
611
import fr.lip6.move.gal.gal2smt.Solver;
@@ -20,6 +25,14 @@ public static void main(String[] args) {
2025

2126
Gal2SMTFrontEnd gsf = new Gal2SMTFrontEnd(Solver.Z3, 300000);
2227
g2p.setSmtConfig(gsf);
23-
g2p.transform(spec, "tests/", true, false);
28+
List<File> produced = new ArrayList<>();
29+
g2p.transform(spec, "tests/", true, false, produced);
30+
for (File f : produced) {
31+
try {
32+
System.out.println("Produced file: " + f.getCanonicalPath());
33+
} catch (IOException e) {
34+
e.printStackTrace();
35+
}
36+
}
2437
}
2538
}

‎pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/runner/ltsmin/LTSminPNMLRunner.java‎

Lines changed: 13 additions & 81 deletions
Original file line numberDiff line numberDiff line change
@@ -8,24 +8,13 @@
88
import java.util.ArrayList;
99
import java.util.List;
1010
import java.util.concurrent.TimeoutException;
11-
import java.util.stream.Collectors;
1211

1312
import fr.lip6.ltl.tgba.TGBA;
14-
import fr.lip6.move.gal.LTLProp;
15-
import fr.lip6.move.gal.Property;
16-
import fr.lip6.move.gal.ReachableProp;
1713
import fr.lip6.move.gal.application.runner.AbstractRunner;
1814
import fr.lip6.move.gal.application.runner.Ender;
19-
import fr.lip6.move.gal.application.runner.IRunner;
20-
import fr.lip6.move.gal.gal2pins.Gal2PinsTransformerNext;
21-
import fr.lip6.move.gal.gal2smt.Gal2SMTFrontEnd;
22-
import fr.lip6.move.gal.gal2smt.Solver;
2315
import fr.lip6.move.gal.ltsmin.BinaryToolsPlugin;
2416
import fr.lip6.move.gal.ltsmin.BinaryToolsPlugin.Tool;
2517
import fr.lip6.move.gal.mcc.properties.DoneProperties;
26-
import fr.lip6.move.gal.mcc.properties.MCCExporter;
27-
import fr.lip6.move.gal.mcc.properties.PropertyPrinter;
28-
import fr.lip6.move.gal.pn2pins.PetriNet2PinsTransformer;
2918
import fr.lip6.move.gal.process.CommandLine;
3019
import fr.lip6.move.gal.process.Runner;
3120
import fr.lip6.move.gal.structural.PropertyType;
@@ -65,26 +54,21 @@ public void solve(Ender ender) {
6554

6655
@Override
6756
public void run() {
57+
List<File> todel = new ArrayList<>();
6858
try {
6959
System.out.println("Building PNML and property files in : \n" + new File(workFolder + "/"));
7060

7161
// step 1 : build PNML
72-
File pnmlpathff = Files.createTempFile("model", ".pnml").toFile();
73-
pnmlpathff.deleteOnExit();
62+
File pnmlpathff = Files.createTempFile("model", ".pnml").toFile();
63+
todel.add(pnmlpathff);
7464
pnmlPath = pnmlpathff.getCanonicalPath();
7565
StructuralToPNML.transform(spn, pnmlPath);
7666

7767
// step 2 : export properties
78-
if (tgba != null) {
79-
80-
} else {
81-
82-
}
83-
8468
if (tgba == null) {
85-
checkProperties(timeout,doneProps);
69+
checkProperties(timeout,doneProps, todel);
8670
} else {
87-
checkProperty(tgba.getName(), stateBasedHOA, timeout, false, PropertyType.LTL);
71+
checkProperty(tgba.getName(), stateBasedHOA, timeout, false, PropertyType.LTL, todel);
8872
}
8973

9074
/*
@@ -119,10 +103,14 @@ public void run() {
119103
} catch (RuntimeException e) {
120104
System.out.println("WARNING : LTS min runner thread failed on error :" + e);
121105
e.printStackTrace();
106+
} finally {
107+
if (DEBUG == 0)
108+
for (File f : todel)
109+
f.delete();
122110
}
123111
}
124112

125-
public void checkProperties(long time, DoneProperties doneProps)
113+
public void checkProperties(long time, DoneProperties doneProps, List<File> todel)
126114
throws IOException, InterruptedException {
127115
boolean negateResult;
128116

@@ -133,7 +121,6 @@ public void checkProperties(long time, DoneProperties doneProps)
133121
String pbody = null;
134122
if (prop.getType() == PropertyType.LTL) {
135123
ByteArrayOutputStream baos = new ByteArrayOutputStream();
136-
PrintWriter pw = new PrintWriter(baos);
137124
{
138125
CExpressionPrinter printer = new CExpressionPrinter(new PrintWriter(baos), "src");
139126
prop.getBody().accept(printer);
@@ -148,7 +135,7 @@ public void checkProperties(long time, DoneProperties doneProps)
148135
negateResult = false;
149136
}
150137

151-
checkProperty(prop.getName(),pbody,time,negateResult, prop.getType());
138+
checkProperty(prop.getName(),pbody,time,negateResult, prop.getType(), todel);
152139
}
153140
}
154141

@@ -159,7 +146,7 @@ public void checkProperties(long time, DoneProperties doneProps)
159146
runnerThread.start();
160147
}
161148

162-
private void checkProperty(String pname, String pbody, long timeout, boolean negateResult, PropertyType propertyType) throws IOException, InterruptedException {
149+
private void checkProperty(String pname, String pbody, long timeout, boolean negateResult, PropertyType propertyType, List<File> todel) throws IOException, InterruptedException {
163150
if (doneProps.containsKey(pname)) {
164151
return;
165152
}
@@ -203,7 +190,7 @@ private void checkProperty(String pname, String pbody, long timeout, boolean neg
203190

204191
try {
205192
File outputff = Files.createTempFile("ltsrun", ".out").toFile();
206-
outputff.deleteOnExit();
193+
todel.add(outputff);
207194
long time = System.currentTimeMillis();
208195
System.out.println("Running LTSmin : " + ltsmin);
209196
int status = Runner.runTool(timeout, ltsmin, outputff, true);
@@ -264,61 +251,6 @@ private boolean isStutterInvariant(String pbody) {
264251
return pbody==null || pbody.contains(".hoa") || ! pbody.contains("X");
265252
}
266253

267-
private void compilePINS(int timeout) throws IOException, TimeoutException, InterruptedException {
268-
// compile
269-
long time = System.currentTimeMillis();
270-
CommandLine clgcc = new CommandLine();
271-
clgcc.setWorkingDir(workFolder);
272-
clgcc.addArg(BinaryToolsPlugin.getProgramURI(Tool.limit_time).getPath().toString());
273-
clgcc.addArg(Long.toString(timeout));
274-
clgcc.addArg("gcc");
275-
clgcc.addArg("-c");
276-
clgcc.addArg("-I" + BinaryToolsPlugin.getIncludeFolderURI().getPath().toString());
277-
clgcc.addArg("-I.");
278-
clgcc.addArg("-std=c99");
279-
clgcc.addArg("-fPIC");
280-
// try no opt to limit timeout
281-
clgcc.addArg("-O0");
282-
// clgcc.addArg("-O2");
283-
clgcc.addArg("model.c");
284-
285-
System.out.println("Running compilation step : " + clgcc);
286-
File outputff = Files.createTempFile("gccrun", ".out").toFile();
287-
outputff.deleteOnExit();
288-
new File(workFolder+"/model.o").deleteOnExit();
289-
int status = Runner.runTool(timeout, clgcc, outputff, true);
290-
if (status != 0) {
291-
Files.lines(outputff.toPath()).forEach(l -> System.err.println(l));
292-
throw new RuntimeException("Could not compile executable ." + clgcc);
293-
}
294-
System.out.println("Compilation finished in "+ (System.currentTimeMillis() -time) +" ms.");
295-
System.out.flush();
296-
}
297-
298-
private void linkPINS(long timeLimit) throws IOException, TimeoutException, InterruptedException {
299-
// link
300-
long time = System.currentTimeMillis();
301-
CommandLine clgcc = new CommandLine();
302-
File cwd = workFolder;
303-
clgcc.setWorkingDir(cwd);
304-
clgcc.addArg("gcc");
305-
clgcc.addArg("-shared");
306-
clgcc.addArg("-o");
307-
clgcc.addArg("gal.so");
308-
clgcc.addArg("model.o");
309-
System.out.println("Running link step : " + clgcc);
310-
File outputff = Files.createTempFile("linkrun", ".out").toFile();
311-
outputff.deleteOnExit();
312-
new File(workFolder+"/gal.so").deleteOnExit();
313-
int status = Runner.runTool(timeout, clgcc, outputff, true);
314-
if (status != 0) {
315-
Files.lines(outputff.toPath()).forEach(l -> System.err.println(l));
316-
throw new RuntimeException("Could not link executable ." + clgcc);
317-
}
318-
System.out.println("Link finished in "+ (System.currentTimeMillis() -time) +" ms.");
319-
System.out.flush();
320-
}
321-
322254
public void setNet(SparsePetriNet spn) {
323255
this.spn = spn;
324256
}

‎pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/runner/ltsmin/LTSminRunner.java‎

Lines changed: 25 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -64,6 +64,7 @@ public void solve(Ender ender) {
6464

6565
@Override
6666
public void run() {
67+
List<File> todel = new ArrayList<>();
6768
try {
6869
System.out.println("Built C files in : \n" + new File(workFolder + "/"));
6970

@@ -75,20 +76,20 @@ public void run() {
7576
final Gal2SMTFrontEnd gsf = new Gal2SMTFrontEnd(Solver.Z3, timeout);
7677
g2p.setSmtConfig(gsf);
7778
g2p.initSolver();
78-
g2p.transform(spec, workFolder.getCanonicalPath(), doPOR, isSafe);
79+
g2p.transform(spec, workFolder.getCanonicalPath(), doPOR, isSafe, todel);
7980

8081
} else {
8182
p2p = new PetriNet2PinsTransformer();
8283
if (tgba != null) {
83-
p2p.transform(spn, workFolder.getCanonicalPath(), doPOR, false, tgba.getAPs());
84+
p2p.transform(spn, workFolder.getCanonicalPath(), doPOR, false, tgba.getAPs(), todel);
8485
} else {
85-
p2p.transform(spn, workFolder.getCanonicalPath(), doPOR, false, null);
86+
p2p.transform(spn, workFolder.getCanonicalPath(), doPOR, false, null, todel);
8687
}
8788

8889
}
8990
try {
90-
compilePINS((int)Math.max(2, timeout/5));
91-
linkPINS(Math.max(1, timeout/5));
91+
compilePINS((int)Math.max(2, timeout/5), todel);
92+
linkPINS(Math.max(1, timeout/5), todel);
9293
} catch (TimeoutException to) {
9394
throw new RuntimeException("Compilation or link of executable timed out." + to);
9495
}
@@ -111,14 +112,14 @@ public void run() {
111112
todo.removeAll(doneProps.keySet());
112113

113114
if (tgba == null) {
114-
checkProperties(g2p, p2p, timeout,doneProps);
115+
checkProperties(g2p, p2p, timeout,doneProps, todel);
115116
} else {
116-
checkProperty(tgba.getName(), stateBasedHOA, timeout, false, PropertyType.LTL);
117+
checkProperty(tgba.getName(), stateBasedHOA, timeout, false, PropertyType.LTL, todel);
117118
}
118119
todo.removeAll(doneProps.keySet());
119120
if (! todo.isEmpty() && shouldRetry) {
120121
System.out.println("Retrying LTSmin with larger timeout "+(8*timeout)+ " s");
121-
checkProperties(g2p, p2p, 8 * timeout, doneProps);
122+
checkProperties(g2p, p2p, 8 * timeout, doneProps, todel);
122123
}
123124
todo.removeAll(doneProps.keySet());
124125
if ( todo.isEmpty()) {
@@ -131,10 +132,16 @@ public void run() {
131132
} catch (RuntimeException e) {
132133
System.out.println("WARNING : LTS min runner thread failed on error :" + e);
133134
e.printStackTrace();
135+
} finally {
136+
if (DEBUG == 0) {
137+
for (File f : todel) {
138+
if (f.exists()) f.delete();
139+
}
140+
}
134141
}
135142
}
136143

137-
public void checkProperties(Gal2PinsTransformerNext g2p, PetriNet2PinsTransformer p2p, long time, DoneProperties doneProps)
144+
public void checkProperties(Gal2PinsTransformerNext g2p, PetriNet2PinsTransformer p2p, long time, DoneProperties doneProps, List<File> todel)
138145
throws IOException, InterruptedException {
139146
boolean negateResult;
140147
if (spn == null) {
@@ -155,7 +162,7 @@ public void checkProperties(Gal2PinsTransformerNext g2p, PetriNet2PinsTransforme
155162
ptype = PropertyType.INVARIANT;
156163
}
157164

158-
checkProperty(prop.getName(),pbody,time,negateResult, ptype);
165+
checkProperty(prop.getName(),pbody,time,negateResult, ptype, todel);
159166
}
160167

161168
} else {
@@ -173,7 +180,7 @@ public void checkProperties(Gal2PinsTransformerNext g2p, PetriNet2PinsTransforme
173180
negateResult = false;
174181
}
175182

176-
checkProperty(prop.getName(),pbody,time/spn.getProperties().size(),negateResult, prop.getType());
183+
checkProperty(prop.getName(),pbody,time/spn.getProperties().size(),negateResult, prop.getType(), todel);
177184
}
178185
}
179186
}
@@ -184,7 +191,7 @@ public void checkProperties(Gal2PinsTransformerNext g2p, PetriNet2PinsTransforme
184191
runnerThread.start();
185192
}
186193

187-
private void checkProperty(String pname, String pbody, long timeout, boolean negateResult, PropertyType propertyType) throws IOException, InterruptedException {
194+
private void checkProperty(String pname, String pbody, long timeout, boolean negateResult, PropertyType propertyType, List<File> todel) throws IOException, InterruptedException {
188195
if (doneProps.containsKey(pname)) {
189196
return;
190197
}
@@ -228,7 +235,7 @@ private void checkProperty(String pname, String pbody, long timeout, boolean neg
228235

229236
try {
230237
File outputff = Files.createTempFile("ltsrun", ".out").toFile();
231-
outputff.deleteOnExit();
238+
todel.add(outputff);
232239
long time = System.currentTimeMillis();
233240
System.out.println("Running LTSmin : " + ltsmin);
234241
int status = Runner.runTool(timeout, ltsmin, outputff, true);
@@ -276,6 +283,7 @@ private void checkProperty(String pname, String pbody, long timeout, boolean neg
276283
}
277284
}
278285
}
286+
if (DEBUG >= 1) System.out.println("Property " + pname + " result: " + result);
279287
String ress = (result + "").toUpperCase();
280288
doneProps.put(pname,"TRUE".equals(ress),(withPOR ? "PARTIAL_ORDER ":"") + "EXPLICIT LTSMIN SAT_SMT");
281289
System.out.flush();
@@ -289,7 +297,7 @@ private boolean isStutterInvariant(String pbody) {
289297
return pbody==null || pbody.contains(".hoa") || ! pbody.contains("X");
290298
}
291299

292-
private void compilePINS(int timeout) throws IOException, TimeoutException, InterruptedException {
300+
private void compilePINS(int timeout, List<File> todel) throws IOException, TimeoutException, InterruptedException {
293301
// compile
294302
long time = System.currentTimeMillis();
295303
CommandLine clgcc = new CommandLine();
@@ -309,8 +317,7 @@ private void compilePINS(int timeout) throws IOException, TimeoutException, Inte
309317

310318
System.out.println("Running compilation step : " + clgcc);
311319
File outputff = Files.createTempFile("gccrun", ".out").toFile();
312-
outputff.deleteOnExit();
313-
new File(workFolder+"/model.o").deleteOnExit();
320+
todel.add(outputff);
314321
int status = Runner.runTool(timeout, clgcc, outputff, true);
315322
if (status != 0) {
316323
Files.lines(outputff.toPath()).forEach(l -> System.err.println(l));
@@ -320,7 +327,7 @@ private void compilePINS(int timeout) throws IOException, TimeoutException, Inte
320327
System.out.flush();
321328
}
322329

323-
private void linkPINS(long timeLimit) throws IOException, TimeoutException, InterruptedException {
330+
private void linkPINS(long timeLimit, List<File> todel) throws IOException, TimeoutException, InterruptedException {
324331
// link
325332
long time = System.currentTimeMillis();
326333
CommandLine clgcc = new CommandLine();
@@ -333,8 +340,7 @@ private void linkPINS(long timeLimit) throws IOException, TimeoutException, Inte
333340
clgcc.addArg("model.o");
334341
System.out.println("Running link step : " + clgcc);
335342
File outputff = Files.createTempFile("linkrun", ".out").toFile();
336-
outputff.deleteOnExit();
337-
new File(workFolder+"/gal.so").deleteOnExit();
343+
todel.add(outputff);
338344
int status = Runner.runTool(timeout, clgcc, outputff, true);
339345
if (status != 0) {
340346
Files.lines(outputff.toPath()).forEach(l -> System.err.println(l));

0 commit comments

Comments
 (0)