Skip to content

Commit

Permalink
Remove FromRead from default witness
Browse files Browse the repository at this point in the history 
Signed-off-by: Tianrui Zheng <[email protected]>
  • Loading branch information
Tianrui Zheng committed Dec 5, 2024
1 parent 9bb43d7 commit 8a0518e
Show file tree
Hide file tree
Showing 3 changed files with 4 additions and 21 deletions.
1 change: 0 additions & 1 deletion dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -241,7 +241,6 @@ public static File generateExecutionGraphFile(VerificationTask task, ProverEnvir
// FR edges only give ordering information which is known if the pair is also in PO
// CO edges only give ordering information which is known if the pair is also in PO
return generateGraphvizFile(encodingContext, prover.getModel(), 1, (x, y) -> true,
(x, y) -> !x.getThreadModel().getThread().equals(y.getThreadModel().getThread()),
(x, y) -> !x.getThreadModel().getThread().equals(y.getThreadModel().getThread()),
getOrCreateOutputDirectory() + "/", name,
synContext, witnessType.convertToPng());
Expand Down
4 changes: 2 additions & 2 deletions dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -902,10 +902,10 @@ private static void generateGraphvizFiles(VerificationTask task, ExecutionModelM
String fileNameBase = String.format("%s-%d", programName, iterationCount);
final SyntacticContextAnalysis emptySynContext = getEmptyInstance();
// File with reason edges only
generateGraphvizFile(model, context, smtModel, iterationCount, edgeFilter, edgeFilter, edgeFilter, directoryName, fileNameBase,
generateGraphvizFile(model, context, smtModel, iterationCount, edgeFilter, edgeFilter, directoryName, fileNameBase,
emptySynContext);
// File with all edges
generateGraphvizFile(model, context, smtModel, iterationCount, (x, y) -> true, (x, y) -> true, (x, y) -> true, directoryName,
generateGraphvizFile(model, context, smtModel, iterationCount, (x, y) -> true, (x, y) -> true, directoryName,
fileNameBase + "-full", emptySynContext);
}
}
20 changes: 2 additions & 18 deletions dartagnan/src/main/java/com/dat3m/dartagnan/witness/graphviz/ExecutionGraphVisualizer.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -45,7 +45,6 @@ public class ExecutionGraphVisualizer {
private SyntacticContextAnalysis synContext = getEmptyInstance();
// By default, we do not filter anything
private BiPredicate<EventModel, EventModel> rfFilter = (x, y) -> true;
private BiPredicate<EventModel, EventModel> frFilter = (x, y) -> true;
private BiPredicate<EventModel, EventModel> coFilter = (x, y) -> true;
private final List<MemoryObjectModel> sortedMemoryObjects = new ArrayList<>();
private List<String> relsToShow = List.of(PO, CO, RF);
Expand All @@ -70,11 +69,6 @@ public ExecutionGraphVisualizer setReadFromFilter(BiPredicate<EventModel, EventM
return this;
}

public ExecutionGraphVisualizer setFromReadFilter(BiPredicate<EventModel, EventModel> filter) {
this.frFilter = filter;
return this;
}

public ExecutionGraphVisualizer setCoherenceFilter(BiPredicate<EventModel, EventModel> filter) {
this.coFilter = filter;
return this;
Expand Down Expand Up @@ -147,12 +141,8 @@ private ExecutionGraphVisualizer addRelation(RelationModel rm, String name) {
String attributes = String.format("color=%s", colorMap.getColor(name));
graphviz.setEdgeAttributes(attributes);
String label = String.format("label=\"%s\"", name);
BiPredicate<EventModel, EventModel> filter;
if (rm.getRelation().getDefinition().getClass() == ReadFrom.class) {
filter = rfFilter;
} else if (name.equals("fr")) {
filter = frFilter;
} else { filter = getFilter(name); }
BiPredicate<EventModel, EventModel> filter = rm.getRelation().getDefinition().getClass() == ReadFrom.class ?
rfFilter : getFilter(name);
for (RelationModel.EdgeModel edge : rm.getEdgeModels()) {
EventModel from = edge.getFrom();
EventModel to = edge.getTo();
Expand Down Expand Up @@ -331,7 +321,6 @@ public static File generateGraphvizFile(ExecutionModelNext model,
Model smtModel,
int iterationCount,
BiPredicate<EventModel, EventModel> rfFilter,
BiPredicate<EventModel, EventModel> frFilter,
BiPredicate<EventModel, EventModel> coFilter,
String directoryName,
String fileNameBase,
Expand All @@ -345,7 +334,6 @@ public static File generateGraphvizFile(ExecutionModelNext model,
if (visualizer == null) { visualizer = new ExecutionGraphVisualizer(); }
visualizer.setSyntacticContext(synContext)
.setReadFromFilter(rfFilter)
.setFromReadFilter(frFilter)
.setCoherenceFilter(coFilter)
.generateGraphOfExecutionModel(writer, "Iteration " + iterationCount, model, context, smtModel);

Expand All @@ -365,7 +353,6 @@ public static File generateGraphvizFile(EncodingContext context,
Model smtModel,
int iterationCount,
BiPredicate<EventModel, EventModel> rfFilter,
BiPredicate<EventModel, EventModel> frFilter,
BiPredicate<EventModel, EventModel> coFilter,
String directoryName,
String fileNameBase,
Expand All @@ -379,7 +366,6 @@ public static File generateGraphvizFile(EncodingContext context,
smtModel,
iterationCount,
rfFilter,
frFilter,
coFilter,
directoryName,
fileNameBase,
Expand All @@ -393,7 +379,6 @@ public static void generateGraphvizFile(ExecutionModelNext model,
Model smtModel,
int iterationCount,
BiPredicate<EventModel, EventModel> rfFilter,
BiPredicate<EventModel, EventModel> frFilter,
BiPredicate<EventModel, EventModel> coFilter,
String directoryName,
String fileNameBase,
Expand All @@ -403,7 +388,6 @@ public static void generateGraphvizFile(ExecutionModelNext model,
smtModel,
iterationCount,
rfFilter,
frFilter,
coFilter,
directoryName,
fileNameBase,
Expand Down

0 comments on commit 8a0518e

Please sign in to comment.