Skip to content

Commit 5d606bb

Browse files
yanntmyanntm
committed
testing the new modes in the benchmark.
1 parent 659edae commit 5d606bb

1 file changed

Lines changed: 91 additions & 80 deletions

File tree

‎pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/ltl/stats/KnowledgeStatsCalculator.java‎

Lines changed: 91 additions & 80 deletions
Original file line numberDiff line numberDiff line change
@@ -42,42 +42,42 @@ public void calculateStats(String inputFolder, String outputFolder) {
4242

4343
File outputFile = outputDir.resolve("formulaStats.csv").toFile();
4444
try (PrintStream out = new PrintStream(new BufferedOutputStream(new FileOutputStream(outputFile)))) {
45-
synchronized (out) {
46-
out.println(AutomatonStats.buildHeaderLine());
47-
}
48-
49-
// Traverse the input directory
50-
try (DirectoryStream<Path> directoryStream = Files.newDirectoryStream(inputPath)) {
51-
List<Path> paths = new ArrayList<>();
52-
for (Path path : directoryStream) {
53-
if (Files.isDirectory(path)) {
54-
paths.add(path);
55-
}
56-
}
57-
58-
paths.parallelStream().unordered().forEach(path -> {
59-
try {
60-
findAndProcessFiles(path, out, "LTLFireability");
61-
} catch (Exception e) {
62-
System.err.println("Error processing: " + path.toString() + " - " + e.getMessage());
63-
}
64-
});
65-
paths.parallelStream().unordered().forEach(path -> {
66-
try {
67-
findAndProcessFiles(path, out, "LTLCardinality");
68-
} catch (Exception e) {
69-
System.err.println("Error processing: " + path.toString() + " - " + e.getMessage());
70-
}
71-
});
72-
73-
} catch (IOException e) {
74-
System.err.println("Error reading input directory: " + e.getMessage());
75-
}
76-
synchronized (out) {
77-
out.flush();
78-
}
45+
synchronized (out) {
46+
out.println(AutomatonStats.buildHeaderLine());
47+
}
48+
49+
// Traverse the input directory
50+
try (DirectoryStream<Path> directoryStream = Files.newDirectoryStream(inputPath)) {
51+
List<Path> paths = new ArrayList<>();
52+
for (Path path : directoryStream) {
53+
if (Files.isDirectory(path)) {
54+
paths.add(path);
55+
}
56+
}
57+
58+
paths.parallelStream().unordered().forEach(path -> {
59+
try {
60+
findAndProcessFiles(path, out, "LTLFireability");
61+
} catch (Exception e) {
62+
System.err.println("Error processing: " + path.toString() + " - " + e.getMessage());
63+
}
64+
});
65+
paths.parallelStream().unordered().forEach(path -> {
66+
try {
67+
findAndProcessFiles(path, out, "LTLCardinality");
68+
} catch (Exception e) {
69+
System.err.println("Error processing: " + path.toString() + " - " + e.getMessage());
70+
}
71+
});
72+
73+
} catch (IOException e) {
74+
System.err.println("Error reading input directory: " + e.getMessage());
75+
}
76+
synchronized (out) {
77+
out.flush();
78+
}
7979
} catch (FileNotFoundException e) {
80-
System.err.println("Error opening output file: " + e.getMessage());
80+
System.err.println("Error opening output file: " + e.getMessage());
8181
}
8282
System.out.println("In total out of "+nbFolder+" found knowledge information in "+ nbTreated + " cases.");
8383

@@ -110,9 +110,9 @@ private void findAndProcessFiles(Path benchmarkDir, PrintStream out, String form
110110
// System.out.println("Working on "+dir+" for " + formulaType);
111111
calculateBenchmarkStats(formulasFile, knowledgeFile, falseKnowledgeFile, out);
112112
nbTreated.incrementAndGet();
113-
synchronized (out) {
114-
out.flush();
115-
}
113+
synchronized (out) {
114+
out.flush();
115+
}
116116
} else {
117117
System.err.println("Incomplete set of files in folder: " + benchmarkDir.toString());
118118
}
@@ -134,8 +134,8 @@ private void calculateBenchmarkStats(File formulasFile, File knowledgeFile, File
134134

135135
private void generateMinMax(File formulasFile, File knowledgeFile, File falseKnowledgeFile, String model, String exam, PrintStream out, boolean negateFormula) {
136136
try {
137-
// if (! model.equals("CloudOpsManagement-PT-00080by00040"))
138-
// return;
137+
// if (! model.equals("CloudOpsManagement-PT-00080by00040"))
138+
// return;
139139

140140
List<String> rawFormulas = Files.readAllLines(formulasFile.toPath());
141141
List<String> knowledgeFormulas = Files.readAllLines(knowledgeFile.toPath());
@@ -145,7 +145,7 @@ private void generateMinMax(File formulasFile, File knowledgeFile, File falseKno
145145
List<Set<String>> knowledgeSupports = new ArrayList<>();
146146
List<Set<String>> falseKnowledgeSupports = new ArrayList<>();
147147

148-
148+
149149
// Compute support sets once and store
150150
for (String formula : rawFormulas) {
151151
rawSupports.add(support(formula));
@@ -156,7 +156,7 @@ private void generateMinMax(File formulasFile, File knowledgeFile, File falseKno
156156
for (String formula : falseKnowledgeFormulas) {
157157
falseKnowledgeSupports.add(support(formula));
158158
}
159-
159+
160160
SpotRunner sr = new SpotRunner(10);
161161

162162
if (negateFormula) {
@@ -171,13 +171,13 @@ private void generateMinMax(File formulasFile, File knowledgeFile, File falseKno
171171
Set<String> rawSupport = rawSupports.get(lineNumber);
172172

173173
String formulaName = model + "-" + exam + "-" + String.format("%02d", lineNumber);
174-
175-
174+
175+
176176
// the assertions we keep
177177
ArrayList<String> selectedKnowledge = new ArrayList<>();
178178
// the support of these assertions
179179
Set<String> extendedSupport = new HashSet<>(rawSupport);
180-
180+
181181
// First pass to retain facts whose alphabet intersects formula
182182
selectKnowledge(knowledgeFormulas, knowledgeSupports, rawSupport, selectedKnowledge, extendedSupport);
183183
// make unique, but preserve order
@@ -186,29 +186,29 @@ private void generateMinMax(File formulasFile, File knowledgeFile, File falseKno
186186
ArrayList<String> selectedFalseKnowledge = new ArrayList<>();
187187
selectKnowledge(falseKnowledgeFormulas, falseKnowledgeSupports, rawSupport, selectedFalseKnowledge, extendedSupport);
188188
selectedFalseKnowledge = new ArrayList<>(new LinkedHashSet<>(selectedFalseKnowledge));
189-
189+
190190
String andknowledge = String.join(" && ", selectedKnowledge);
191191
if (selectedKnowledge.isEmpty()) {
192192
System.out.println("No knowledge for formula " + formulaName + " (negative facts :"+selectedFalseKnowledge.size()+ ")");
193-
193+
194194
andknowledge = "1";
195195
}
196196
if (selectedKnowledge.isEmpty() && selectedFalseKnowledge.isEmpty()) {
197197
System.out.println("No knowledge for formula " + formulaName + " (negative facts :"+selectedFalseKnowledge.size()+ ")");
198198
continue;
199199
}
200-
200+
201201
TGBA rawTGBA = buildAndPrintAutomatonStats("raw", rawFormula, formulaName, out, sr,0);
202-
202+
203203
boolean withMinMax = true;
204-
204+
205205
if (withMinMax) {
206206
// NB : no existential quantification
207207
buildAndPrintAutomatonStats("min", "(" + rawFormula + ")&&" + andknowledge, formulaName, out, sr,selectedKnowledge.size());
208208

209209
buildAndPrintAutomatonStats("max", "(" + rawFormula + ")||!(" + andknowledge + ")", formulaName, out, sr,selectedKnowledge.size());
210210
}
211-
211+
212212
Set<String> toQuantify = new HashSet<>(extendedSupport);
213213
toQuantify.removeAll(rawSupport);
214214
//andknowledge = "(G((p16||!p32)))";
@@ -226,44 +226,49 @@ private void generateMinMax(File formulasFile, File knowledgeFile, File falseKno
226226
}
227227
String maxqeform = "(" + rawFormula + ")||!(" + quantifiedKnowledge + ")";
228228
TGBA maxqe = buildAndPrintAutomatonStats("maxqe", maxqeform, formulaName, out, sr,selectedKnowledge.size());
229-
229+
230230
/* negative knowledge */
231231
/* K- is false ; so !K- contains a run of S.*/
232232
/* This run must also be part of K+, since K+ wraps S. Using this fact lets us use a smaller language for inclusion test. */
233233
/* So, consider !K- AND K+ : it must contain a system run.*/
234234
/* So if it is included in !phi, !phi contains a system run, that is a counterexample to phi. */
235-
235+
236236
/* To avoid complementations and full inclusions, we leverage a "satisfiable" LTL test */
237237
/* !K- AND K+ AND phi unsatisfiable => (!K- AND K+) included in !phi since (!K- AND K+) cannot be empty.*/
238238
/* hence we have a counterexample to phi if : !K- AND K+ AND phi is UNSAT*/
239-
if (! selectedFalseKnowledge.isEmpty()) {
239+
if (! selectedFalseKnowledge.isEmpty() && ! minqe.isEmptyLanguage()) {
240240
long time = System.currentTimeMillis();
241241

242242
// Build our formula for (K+ AND phi)
243243
String kplusandphi = "(" + rawFormula + ")&&(" + quantifiedKnowledge + ")";
244-
244+
245+
//System.out.println("Testing formula " + formulaName + " : " + rawFormula);
246+
//System.out.println("With positive knowledge : " + quantifiedKnowledge);
247+
248+
249+
245250
boolean hasCounterExample = false;
246-
251+
247252
for (String fk : selectedFalseKnowledge) {
248253
String totest = "!(" + fk + ")&&(" + kplusandphi + ")";
249-
if (!sr.isSatisfiable(totest)) { // new helper (see next message)
250-
System.out.println("Negative knowledge disproves " + formulaName +
251-
" using false fact: " + fk);
252-
hasCounterExample = true;
253-
break;
254-
}
254+
if (!sr.isSatisfiable(totest)) {
255+
System.out.println("Negative knowledge disproves " + formulaName +
256+
" using false fact: " + fk);
257+
hasCounterExample = true;
258+
break;
259+
}
255260
}
256-
261+
257262
TGBA tgba = null;
258263
if (hasCounterExample) {
259264
tgba = TGBA.makeTrue();
260265
}
261266
AutomatonStats rawStats = AutomatonStatsCalculator.computeStats(tgba, formulaName, "negative",time,selectedFalseKnowledge.size());
262-
synchronized (out) { out.println(rawStats.toString()); }
267+
synchronized (out) { out.println(rawStats.toString()); }
263268
}
264-
269+
265270
}
266-
271+
267272
// incremental
268273
applyGivenThat(formulaName, rawTGBA, selectedKnowledge, out, sr,"");
269274
// global
@@ -298,13 +303,13 @@ public void selectKnowledge(List<String> knowledgeFormulas, List<Set<String>> kn
298303
if (toadd[i])
299304
selectedKnowledge.add("(" + knowledgeFormulas.get(i) + ")");
300305
}
301-
302-
306+
307+
303308
// second pass, keep if it intersects formulas we kept in first pass : touches extendedSupport
304309
// currently disabled
305310
boolean secondPass = false;
306311
if (secondPass) {
307-
312+
308313
boolean[] toadd2 = new boolean[knowledgeFormulas.size()];
309314
Set<String> finalSupport = new HashSet<>(extendedSupport);
310315
for (int i = 0; i < knowledgeFormulas.size(); ++i) {
@@ -320,7 +325,7 @@ public void selectKnowledge(List<String> knowledgeFormulas, List<Set<String>> kn
320325
if (toadd2[i])
321326
selectedKnowledge.add("(" + knowledgeFormulas.get(i) + ")");
322327
}
323-
328+
324329
// update alphabet for "--remove-ap" invocations
325330
extendedSupport = finalSupport;
326331
}
@@ -358,9 +363,15 @@ public TGBA buildAndPrintAutomatonStats(String type, String formula, String form
358363

359364
public void applyGivenThat(String formulaName, TGBA rawTGBA, ArrayList<String> selectedKnowledge,
360365
PrintStream out, SpotRunner sr, String prefix) {
361-
366+
362367
boolean compositions = true;
363368
boolean doubleCompositions = false;
369+
370+
{
371+
TGBA autoSmall = computeStats(formulaName, rawTGBA, GivenStrategy.AUTO_SMALL, selectedKnowledge, out, sr, prefix+ GivenStrategy.AUTO_SMALL);
372+
TGBA autoSI = computeStats(formulaName, rawTGBA, GivenStrategy.AUTO_SI, selectedKnowledge, out, sr, prefix+ GivenStrategy.AUTO_SI);
373+
374+
}
364375

365376
TGBA minato = computeStats(formulaName, rawTGBA, GivenStrategy.MINATO, selectedKnowledge, out, sr, prefix+ GivenStrategy.MINATO);
366377
// minato/minato
@@ -374,7 +385,7 @@ public void applyGivenThat(String formulaName, TGBA rawTGBA, ArrayList<String> s
374385
}
375386
}
376387
}
377-
388+
378389
TGBA relax = computeStats(formulaName, rawTGBA, GivenStrategy.STUTTER_RELAX, selectedKnowledge, out, sr, prefix+ GivenStrategy.STUTTER_RELAX);
379390
if (compositions && relax != null) {
380391
TGBA relaxmin = computeStats(formulaName, relax, GivenStrategy.MINATO, selectedKnowledge, out, sr, prefix+ GivenStrategy.STUTTER_RELAX+ GivenStrategy.MINATO);
@@ -385,20 +396,20 @@ public void applyGivenThat(String formulaName, TGBA rawTGBA, ArrayList<String> s
385396
}
386397
}
387398
}
388-
399+
389400
computeStats(formulaName, rawTGBA, GivenStrategy.STUTTER_RESTRICT, selectedKnowledge, out, sr, prefix+ GivenStrategy.STUTTER_RESTRICT);
390-
391-
// TGBA all =computeStats(formulaName, rawTGBA, GivenStrategy.ALL, selectedKnowledge, out, sr, prefix+ GivenStrategy.ALL);
392-
//
393-
// if (compositions && all != null) {
394-
// TGBA allall =computeStats(formulaName, all, GivenStrategy.ALL, selectedKnowledge, out, sr, prefix+ GivenStrategy.ALL+ GivenStrategy.ALL);
395-
// }
401+
402+
// TGBA all =computeStats(formulaName, rawTGBA, GivenStrategy.ALL, selectedKnowledge, out, sr, prefix+ GivenStrategy.ALL);
403+
//
404+
// if (compositions && all != null) {
405+
// TGBA allall =computeStats(formulaName, all, GivenStrategy.ALL, selectedKnowledge, out, sr, prefix+ GivenStrategy.ALL+ GivenStrategy.ALL);
406+
// }
396407

397408
}
398409

399410
public TGBA computeStats(String formulaName, TGBA rawTGBA, GivenStrategy strat, ArrayList<String> selectedKnowledge,
400411
PrintStream out, SpotRunner sr, String prefix) {
401-
412+
402413
long time = System.currentTimeMillis();
403414
TGBA tgbaRes = sr.givenThat(rawTGBA, selectedKnowledge, strat);
404415
AutomatonStats stats = AutomatonStatsCalculator.computeStats(tgbaRes, formulaName, prefix,time,selectedKnowledge.size());

0 commit comments

Comments
 (0)