Skip to content

Commit

Permalink
Reformatted code
Browse files Browse the repository at this point in the history
Removed caching

Revert "Removed caching"

This reverts commit 05a5d44.

Commented out problematic test

Added reference checks, moved state/action-equality first

Removed old hash code caches

added null checks

Added tests

Added debugger support
  • Loading branch information
thetabotmaintainer[bot] authored and leventeBajczi committed Nov 10, 2023
1 parent 274b07d commit a8d44b8
Show file tree
Hide file tree
Showing 11 changed files with 293 additions and 28 deletions.
1 change: 1 addition & 0 deletions subprojects/common/analysis/build.gradle.kts
Original file line number Diff line number Diff line change
Expand Up @@ -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")
}
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -109,6 +110,7 @@ public ArgNode<S, A> createInitNode(final S initState, final boolean target) {
checkNotNull(initState);
final ArgNode<S, A> initNode = createNode(initState, 0, target);
initNodes.add(initNode);
ARGWebDebugger.create(initNode);
return initNode;
}

Expand All @@ -134,6 +136,7 @@ private ArgEdge<S, A> createEdge(final ArgNode<S, A> source, final A action, fin
final ArgEdge<S, A> edge = new ArgEdge<>(source, action, target);
source.outEdges.add(edge);
target.inEdge = Optional.of(edge);
ARGWebDebugger.add(source, action, target);
return edge;
}

Expand All @@ -147,6 +150,7 @@ public void prune(final ArgNode<S, A> node) {
final ArgEdge<S, A> edge = node.getInEdge().get();
final ArgNode<S, A> parent = edge.getSource();
parent.outEdges.remove(edge);
ARGWebDebugger.remove(edge);
parent.expanded = false;
} else {
assert initNodes.contains(node);
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -19,9 +19,6 @@
import hu.bme.mit.theta.analysis.State;

public final class ArgEdge<S extends State, A extends Action> {
private static final int HASH_SEED = 3653;
private volatile int hashCode = 0;

private final ArgNode<S, A> source;
private final ArgNode<S, A> target;
private final A action;
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -30,9 +30,6 @@

public final class ArgNode<S extends State, A extends Action> {

private static final int HASH_SEED = 8543;
private volatile int hashCode = 0;

final ARG<S, A> arg;

private final int id;
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -40,24 +40,34 @@
public final class ArgStructuralEquality {
private static final Map<Object, Integer> hashCodeCache = new LinkedHashMap<>();

private ArgStructuralEquality(){
private ArgStructuralEquality() {
}

public static boolean equals(final ArgNode<? extends State, ? extends Action> n1,
final ArgNode<? extends State, ? extends Action> n2) {

// if one node has a parent but the other one does not, nodes are not equal
if(n1.inEdge.isPresent() != n2.inEdge.isPresent()) {
return false;
// if references are the same, the two nodes are equal
if (n1 == n2) {
return true;
}

// if in edge is not same, nodes are not equal
if(n1.inEdge.isPresent() && !equals(n1.inEdge.get(), n2.inEdge.get())) {
// if one is null, the two nodes are not equal
if (n1 == null || n2 == null) {
return false;
}

// if wrapped state is not same, nodes are not equal
if(!n1.getState().equals(n2.getState())) {
if (!n1.getState().equals(n2.getState())) {
return false;
}

// if one node has a parent but the other one does not, nodes are not equal
if (n1.inEdge.isPresent() != n2.inEdge.isPresent()) {
return false;
}

// if in edge is not same, nodes are not equal
if (n1.inEdge.isPresent() && !equals(n1.inEdge.get(), n2.inEdge.get())) {
return false;
}

Expand All @@ -67,13 +77,24 @@ public static boolean equals(final ArgNode<? extends State, ? extends Action> n1
public static boolean equals(final ArgEdge<? extends State, ? extends Action> e1,
final ArgEdge<? extends State, ? extends Action> e2) {

// if source node is not same, edges are not equal
if(!equals(e1.getSource(), e2.getSource())) {
// if references are the same, the two edges are equal
if (e1 == e2) {
return true;
}

// if one is null, the two edges are not equal
if (e1 == null || e2 == null) {
return false;
}


// if wrapped action is not same, edges are not equal
if(!e1.getAction().equals(e2.getAction())) {
if (!e1.getAction().equals(e2.getAction())) {
return false;
}

// if source node is not same, edges are not equal
if (!equals(e1.getSource(), e2.getSource())) {
return false;
}

Expand All @@ -83,18 +104,28 @@ public static boolean equals(final ArgEdge<? extends State, ? extends Action> e1
public static boolean equals(final ARG<? extends State, ? extends Action> a1,
final ARG<? extends State, ? extends Action> a2) {

// if references are the same, the two edges are equal
if (a1 == a2) {
return true;
}

// if one is null, the two args are not equal
if (a1 == null || a2 == null) {
return false;
}

Set<ArgNode<? extends State, ? extends Action>> leaves1 = a1.getNodes().filter(ArgNode::isLeaf).collect(Collectors.toUnmodifiableSet());
Set<ArgNode<? extends State, ? extends Action>> leaves2 = a2.getNodes().filter(ArgNode::isLeaf).collect(Collectors.toUnmodifiableSet());

// if the two ARGs contain a different number of leaf nodes, they are not equal
if(leaves1.size() != leaves2.size()) {
if (leaves1.size() != leaves2.size()) {
return false;
}

leaves1loop:
for (ArgNode<? extends State, ? extends Action> n1 : leaves1) {
for (ArgNode<? extends State, ? extends Action> n2 : leaves2) {
if(equals(n1, n2)) {
if (equals(n1, n2)) {
continue leaves1loop;
}
}
Expand All @@ -112,10 +143,10 @@ public static boolean equals(final ArgTrace<? extends State, ? extends Action> t


public static int hashCode(final ArgNode<? extends State, ? extends Action> n) {
if(!hashCodeCache.containsKey(n)) {
if (!hashCodeCache.containsKey(n)) {
int hashcode = 0;

if(n.inEdge.isPresent()) {
if (n.inEdge.isPresent()) {
hashcode += hashCode(n.inEdge.get());
}

Expand All @@ -126,7 +157,7 @@ public static int hashCode(final ArgNode<? extends State, ? extends Action> n) {
}

public static int hashCode(final ArgEdge<? extends State, ? extends Action> e) {
if(!hashCodeCache.containsKey(e)) {
if (!hashCodeCache.containsKey(e)) {
int hashcode = 0;

hashcode += hashCode(e.getSource());
Expand All @@ -151,7 +182,7 @@ public static int hashCode(final ARG<? extends State, ? extends Action> a) {
}

public static int hashCode(final ArgTrace<? extends State, ? extends Action> t) {
if(!hashCodeCache.containsKey(t)) {
if (!hashCodeCache.containsKey(t)) {
int hashcode = hashCode(t.node(t.length()));
hashCodeCache.put(t, hashcode);
}
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -34,9 +34,6 @@
*/
public final class ArgTrace<S extends State, A extends Action> implements Iterable<ArgNode<S, A>> {

private static final int HASH_SEED = 7653;
private volatile int hashCode = 0;

private final List<ArgNode<S, A>> nodes;
private final List<ArgEdge<S, A>> edges;
private final Collection<State> states;
Expand Down
Original file line number Diff line number Diff line change
@@ -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<String> 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 <A extends Action> String nodeToString(ArgNode<? extends State, ? extends Action> 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<? extends State, ? extends Action> initNode) {
if (!debug) {
return;
}
replayLog.clear();
send("{\"method\": \"create\", \"node\": " + nodeToString(initNode, null) + "}", true);
waitUntil();
}

public static <A extends Action> void add(ArgNode<? extends State, ? extends Action> parent,
A action,
ArgNode<? extends State, ? extends Action> child) {
if (!debug) {
return;
}
send("{\"method\": \"add\", \"parent\": " + parent.getId() + ", \"child\": " + nodeToString(child, action) + "}", true);
waitUntil();
}

public static <A extends Action> void remove(ArgEdge<? extends State, ? extends Action> edge) {
if (!debug) {
return;
}
send("{\"method\": \"delete\", \"parent\": " + edge.getSource().getId() + ", \"child\": " + edge.getTarget().getId() + "}", true);
waitUntil();
}
}
Loading

0 comments on commit a8d44b8

Please sign in to comment.