From 36a08227645bc0677a4466c6238e8300e81538bb Mon Sep 17 00:00:00 2001 From: Levente Bajczi Date: Fri, 10 Nov 2023 22:19:57 +0100 Subject: [PATCH] Added debugger support --- subprojects/common/analysis/build.gradle.kts | 1 + .../bme/mit/theta/analysis/algorithm/ARG.java | 4 + .../algorithm/debug/ARGWebDebugger.java | 137 ++++++++++++++++++ 3 files changed, 142 insertions(+) create mode 100644 subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/debug/ARGWebDebugger.java diff --git a/subprojects/common/analysis/build.gradle.kts b/subprojects/common/analysis/build.gradle.kts index dae61a15a5..d73ed4f787 100644 --- a/subprojects/common/analysis/build.gradle.kts +++ b/subprojects/common/analysis/build.gradle.kts @@ -24,4 +24,5 @@ dependencies { implementation(project(":theta-solver")) implementation(project(":theta-graph-solver")) testImplementation(project(":theta-solver-z3")) + implementation("com.corundumstudio.socketio:netty-socketio:2.0.6") } diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/ARG.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/ARG.java index 85313ef0f2..e653bfb397 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/ARG.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/ARG.java @@ -18,6 +18,7 @@ import hu.bme.mit.theta.analysis.Action; import hu.bme.mit.theta.analysis.PartialOrd; import hu.bme.mit.theta.analysis.State; +import hu.bme.mit.theta.analysis.algorithm.debug.ARGWebDebugger; import hu.bme.mit.theta.common.container.Containers; import java.util.Collection; @@ -109,6 +110,7 @@ public ArgNode createInitNode(final S initState, final boolean target) { checkNotNull(initState); final ArgNode initNode = createNode(initState, 0, target); initNodes.add(initNode); + ARGWebDebugger.create(initNode); return initNode; } @@ -134,6 +136,7 @@ private ArgEdge createEdge(final ArgNode source, final A action, fin final ArgEdge edge = new ArgEdge<>(source, action, target); source.outEdges.add(edge); target.inEdge = Optional.of(edge); + ARGWebDebugger.add(source, action, target); return edge; } @@ -147,6 +150,7 @@ public void prune(final ArgNode node) { final ArgEdge edge = node.getInEdge().get(); final ArgNode parent = edge.getSource(); parent.outEdges.remove(edge); + ARGWebDebugger.remove(edge); parent.expanded = false; } else { assert initNodes.contains(node); diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/debug/ARGWebDebugger.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/debug/ARGWebDebugger.java new file mode 100644 index 0000000000..f43f913c23 --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/debug/ARGWebDebugger.java @@ -0,0 +1,137 @@ +/* + * Copyright 2023 Budapest University of Technology and Economics + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ + +package hu.bme.mit.theta.analysis.algorithm.debug; + +import com.corundumstudio.socketio.Configuration; +import com.corundumstudio.socketio.SocketIOServer; +import hu.bme.mit.theta.analysis.Action; +import hu.bme.mit.theta.analysis.State; +import hu.bme.mit.theta.analysis.algorithm.ArgEdge; +import hu.bme.mit.theta.analysis.algorithm.ArgNode; + +import java.util.LinkedList; +import java.util.List; + + +/** + * Use http://leventebajczi.com/theta-debugger/ to connect to Theta and see the ARG being built. + * Modify the *debug* field below to true in order to enable the debugger. + */ + +public final class ARGWebDebugger { + private static final boolean debug = false; + private static final Integer PORT = 8080; + + private static SocketIOServer server; + private static final Object lock = new Object(); + private static volatile boolean received; + private static volatile boolean waiting; + + + private static final List replayLog = new LinkedList<>(); + + + private ARGWebDebugger() { + } + + private static void startServer() { + if (!debug) return; + Configuration config = new Configuration(); + config.setPort(PORT); + + config.setOrigin("http://localhost:3000"); + + server = new SocketIOServer(config); + server.addEventListener("continue", String.class, (client, data, ackSender) -> { + received = true; + synchronized (lock) { + lock.notifyAll(); + } + }); + server.addConnectListener(client -> { + for (String s : replayLog) { + System.err.println("Replaying " + s); + client.sendEvent("message", s); + } + if (waiting) client.sendEvent("message", "{\"method\": \"wait\"}"); + }); + server.start(); + waitUntil(); + } + + private static void send(String data, boolean log) { + if (server == null) startServer(); + if (log) replayLog.add(data); + server.getAllClients().forEach(client -> client.sendEvent("message", data)); + } + + private static void waitUntil() { + if (server == null) startServer(); + send("{\"method\": \"wait\"}", false); + synchronized (lock) { + while (!received) { + waiting = true; + try { + lock.wait(1000); + } catch (InterruptedException e) { + e.printStackTrace(); + } + } + received = false; // Reset for the next wait + waiting = false; + } + } + + private static String nodeToString(ArgNode node, A action) { + return "{\"name\": \"Node " + node.getId() + "\"," + + " \"attributes\": {" + + (action == null ? "" : "\"action\": \"" + action.toString().replaceAll("[\\n\\r\\t\"]", " ") + "\",") + + "\"state\": \"" + node.getState().toString().replaceAll("[\\n\\r\\t\"]", " ") + "\"" + "," + + "\"target\": \"" + node.isTarget() + "\"" + "}," + + " \"tooltip\": {" + + (action == null ? "" : "\"action\": \"" + action.toString().replaceAll("[\\n\\r\\t\"]", " ") + "\",") + + "\"state\": \"" + node.getState().toString().replaceAll("[\\n\\r\\t\"]", " ") + "\"" + "}," + + " \"id\": " + node.getId() + "}"; + } + + public static void create(ArgNode initNode) { + if (!debug) { + return; + } + replayLog.clear(); + send("{\"method\": \"create\", \"node\": " + nodeToString(initNode, null) + "}", true); + waitUntil(); + } + + public static void add(ArgNode parent, + A action, + ArgNode child) { + if (!debug) { + return; + } + send("{\"method\": \"add\", \"parent\": " + parent.getId() + ", \"child\": " + nodeToString(child, action) + "}", true); + waitUntil(); + } + + public static void remove(ArgEdge edge) { + if (!debug) { + return; + } + send("{\"method\": \"delete\", \"parent\": " + edge.getSource().getId() + ", \"child\": " + edge.getTarget().getId() + "}", true); + waitUntil(); + } +}