From 8d5a07ff4344abfa71ee7993e7ab1f017c7700f6 Mon Sep 17 00:00:00 2001 From: mondokm Date: Tue, 13 Feb 2024 17:00:14 +0100 Subject: [PATCH] Added structural vs symbolic benchmarks --- .../cli/StructuralSymbolicComparison.java | 132 ++++++++++++++++++ 1 file changed, 132 insertions(+) create mode 100644 subprojects/xsts/xsts-cli/src/main/java/hu/bme/mit/theta/xsts/cli/StructuralSymbolicComparison.java diff --git a/subprojects/xsts/xsts-cli/src/main/java/hu/bme/mit/theta/xsts/cli/StructuralSymbolicComparison.java b/subprojects/xsts/xsts-cli/src/main/java/hu/bme/mit/theta/xsts/cli/StructuralSymbolicComparison.java new file mode 100644 index 0000000000..5c3704937a --- /dev/null +++ b/subprojects/xsts/xsts-cli/src/main/java/hu/bme/mit/theta/xsts/cli/StructuralSymbolicComparison.java @@ -0,0 +1,132 @@ +package hu.bme.mit.theta.xsts.cli; + +import com.koloboke.collect.map.hash.HashObjObjMaps; +import hu.bme.mit.delta.collections.RecursiveIntObjCursor; +import hu.bme.mit.delta.java.mdd.*; +import hu.bme.mit.delta.mdd.MddVariableDescriptor; +import hu.bme.mit.theta.analysis.algorithm.symbolic.symbolicnode.SolverPool; +import hu.bme.mit.theta.analysis.algorithm.symbolic.symbolicnode.expression.ExprLatticeDefinition; +import hu.bme.mit.theta.analysis.algorithm.symbolic.symbolicnode.expression.MddExpressionTemplate; +import hu.bme.mit.theta.core.decl.Decl; +import hu.bme.mit.theta.core.type.Expr; +import hu.bme.mit.theta.core.type.booltype.BoolType; +import hu.bme.mit.theta.core.utils.PathUtils; +import hu.bme.mit.theta.core.utils.StmtUtils; +import hu.bme.mit.theta.core.utils.indexings.VarIndexingFactory; +import hu.bme.mit.theta.solver.UnknownSolverStatusException; +import hu.bme.mit.theta.solver.z3.Z3SolverFactory; + +import java.io.BufferedWriter; +import java.io.FileWriter; +import java.util.ArrayList; +import java.util.Collections; +import java.util.List; +import java.util.Map; + +import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Geq; +import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Leq; +import static hu.bme.mit.theta.core.type.booltype.BoolExprs.And; +import static hu.bme.mit.theta.core.type.inttype.IntExprs.Int; +import static hu.bme.mit.theta.xsts.RandomXstsKt.generateXsts; + +public class StructuralSymbolicComparison { + + public static void main(String[] asdsad) throws Exception{ + + final var upperbound = 5; + + var pool = new SolverPool(Z3SolverFactory.getInstance()); + + try(BufferedWriter writer = new BufferedWriter(new FileWriter("build\\measurements.csv", true))){ + for(int i = 0; true; i++) { + try { + var xsts = generateXsts(i); + + final MddGraph transGraph = JavaMddFactory.getDefault().createMddGraph(ExprLatticeDefinition.forExpr()); + final MddGraph structGraph = JavaMddFactory.getDefault().createMddGraph(ExprLatticeDefinition.forExpr()); + + final MddVariableOrder transOrder = JavaMddFactory.getDefault().createMddVariableOrder(transGraph); + final MddVariableOrder structOrder = JavaMddFactory.getDefault().createMddVariableOrder(structGraph); + + final var tranToExprResult = StmtUtils.toExpr(xsts.getTran(), VarIndexingFactory.indexing(0)); + + final List> boundExprs = new ArrayList<>(); + final var shuffledVars = new ArrayList<>(xsts.getVars()); + Collections.shuffle(shuffledVars); + for (var v : shuffledVars) { + transOrder.createOnTop(MddVariableDescriptor.create(v.getConstDecl(tranToExprResult.getIndexing().get(v) == 0 ? 1 : tranToExprResult.getIndexing().get(v)), 0)); + transOrder.createOnTop(MddVariableDescriptor.create(v.getConstDecl(0), 0)); + + structOrder.createOnTop(MddVariableDescriptor.create(v.getName() + "2", 0)); + structOrder.createOnTop(MddVariableDescriptor.create(v.getName(), 0)); + + if (v.getType() instanceof hu.bme.mit.theta.core.type.inttype.IntType) { + boundExprs.add(Geq(v.getConstDecl(0).getRef(), Int(0))); + boundExprs.add(Leq(v.getConstDecl(0).getRef(), Int(upperbound))); + boundExprs.add(Geq(v.getConstDecl(tranToExprResult.getIndexing().get(v) == 0 ? 1 : tranToExprResult.getIndexing().get(v)).getRef(), Int(0))); + boundExprs.add(Leq(v.getConstDecl(tranToExprResult.getIndexing().get(v) == 0 ? 1 : tranToExprResult.getIndexing().get(v)).getRef(), Int(upperbound))); + } + } + + final var transSig = transOrder.getDefaultSetSignature(); + final var structSig = structOrder.getDefaultSetSignature(); + var stmtUnfold = PathUtils.unfold(tranToExprResult.getExprs().stream().findFirst().get(), 0); + stmtUnfold = And(stmtUnfold, And(boundExprs)); + final MddHandle transitionNode = transSig.getTopVariableHandle().checkInNode(MddExpressionTemplate.of(stmtUnfold, o -> (Decl) o, pool)); + + final MddHandle structuralTransitionNode = MddToStructuralTransformer.transform(transitionNode, structSig.getTopVariableHandle()); + + final Long symbolicSize = calculateNonzeroCount(transitionNode); + final Long structuralSize = calculateNonzeroCount(structuralTransitionNode); + System.out.println(transGraph.getUniqueTableSize() + ", " + structGraph.getUniqueTableSize() + ", " + symbolicSize + ", " + structuralSize); + writer.write(transGraph.getUniqueTableSize() + ", " + structGraph.getUniqueTableSize() + ", " + symbolicSize + ", " + structuralSize); + writer.newLine(); + if(i%10 == 0) writer.flush(); + } catch (UnknownSolverStatusException e) { + // TODO this is horrible but needed for now + } + } + } + } + + public static Long calculateNonzeroCount(MddHandle root) { + if (root == null) { + throw new IllegalArgumentException("Root handle cannot be null."); + } else { + int height = root.getVariableHandle().getHeight(); + Map cache = HashObjObjMaps.newMutableMap(); + Long ret = calculateNonzeroCount(root, height, cache, root.cursor()); + return ret; + } + } + + private static Long calculateNonzeroCount(MddHandle node, int level, Map cache, RecursiveIntObjCursor cursor) { + Long cached = (Long)cache.getOrDefault(node, null); + if (cached != null) { + return cached; + } else if (node.isTerminalZero()) { + return 0L; + } else if (node.isTerminal() && !node.isTerminalZero()) { + assert level == 0; + + return 1L; + } else { + long ret = 0L; + + while (cursor.moveNext()){ + try(var valueCursor = cursor.valueCursor()){ + Long res = calculateNonzeroCount(cursor.value(), level - 1, cache, valueCursor); + if (res == null) { + return null; + } + ret += res; + } + } + + Long lRet = ret; + cache.put(node, lRet); + return lRet; + } + } + +}