From 4f98cc4ddad83b11f93d6593eb286db6d24bda00 Mon Sep 17 00:00:00 2001
From: Fabian Vu <Fabian.Vu@hhu.de>
Date: Thu, 20 Jun 2024 15:39:30 +0200
Subject: [PATCH] Implement reflections to access functions
---
.../de/hhu/stups/java/modelchecker/Main.java | 2 +
.../stups/java/modelchecker/Modelchecker.java | 114 ++++++++++++++++++
2 files changed, 116 insertions(+)
create mode 100644 JavaModelChecker/src/main/java/de/hhu/stups/java/modelchecker/Modelchecker.java
diff --git a/JavaModelChecker/src/main/java/de/hhu/stups/java/modelchecker/Main.java b/JavaModelChecker/src/main/java/de/hhu/stups/java/modelchecker/Main.java
index 5b6ca77..a63a36c 100644
--- a/JavaModelChecker/src/main/java/de/hhu/stups/java/modelchecker/Main.java
+++ b/JavaModelChecker/src/main/java/de/hhu/stups/java/modelchecker/Main.java
@@ -1,5 +1,7 @@
package de.hhu.stups.java.modelchecker;
+import java.io.IOException;
+
public class Main {
public static void main(String[] args) throws IOException {
diff --git a/JavaModelChecker/src/main/java/de/hhu/stups/java/modelchecker/Modelchecker.java b/JavaModelChecker/src/main/java/de/hhu/stups/java/modelchecker/Modelchecker.java
new file mode 100644
index 0000000..e6829aa
--- /dev/null
+++ b/JavaModelChecker/src/main/java/de/hhu/stups/java/modelchecker/Modelchecker.java
@@ -0,0 +1,114 @@
+package de.hhu.stups.java.modelchecker;
+
+import de.hhu.stups.btypes.BTuple;
+import de.hhu.stups.java.modelchecker.json.ModelCheckingInfo;
+import de.hhu.stups.java.modelchecker.json.OperationFunctionInfo;
+
+import java.io.File;
+import java.lang.reflect.Constructor;
+import java.lang.reflect.Method;
+import java.net.URL;
+import java.net.URLClassLoader;
+import java.util.HashMap;
+import java.util.List;
+import java.util.Map;
+
+public class Modelchecker {
+
+ private final ModelCheckingInfo modelCheckingInfo;
+
+ private Object machine;
+
+ private final Map<String, Method> methods;
+
+ public Modelchecker(final ModelCheckingInfo modelCheckingInfo) {
+ this.modelCheckingInfo = modelCheckingInfo;
+ this.methods = new HashMap<>();
+ setupAccess();
+ }
+
+ private void setupAccess() {
+ String machineName = modelCheckingInfo.getMachineName();
+ try {
+ File directory = new File("");
+
+ // Convert File to a URL
+ URL url = directory.toURI().toURL();
+ URL[] urls = new URL[]{url};
+
+ // Create a new class loader with the directory
+ ClassLoader cl = new URLClassLoader(urls);
+
+ Class<?> myClass = cl.loadClass(machineName);
+ Class<?>[] types = {};
+ Constructor<?> constructor = myClass.getConstructor(types);
+ Object[] parameters = {};
+
+ this.machine = constructor.newInstance(parameters);
+
+ for(OperationFunctionInfo opInfo : modelCheckingInfo.getOperationFunctions()) {
+ String opName = opInfo.getOpName();
+ List<String> parameterTypes = opInfo.getParameterTypes();
+ Method method;
+ if(opInfo.getParameterTypes().isEmpty()) {
+ method = machine.getClass().getMethod(opName);
+ } else {
+ Class<?>[] methodParameterTypes = new Class<?>[parameterTypes.size()];
+ for(int i = 0; i < parameterTypes.size(); i++) {
+ try {
+ methodParameterTypes[i] = cl.loadClass(parameterTypes.get(i));
+ } catch (ClassNotFoundException e) {
+ e.printStackTrace();
+ }
+ }
+ method = machine.getClass().getMethod(opName, methodParameterTypes);
+ }
+ method.setAccessible(true);
+ methods.put(opName, method);
+ }
+
+ for(String functionInfo : modelCheckingInfo.getTransitionEvaluationFunctions().values()) {
+ Method method = machine.getClass().getMethod(functionInfo);
+ method.setAccessible(true);
+ methods.put(functionInfo, method);
+ }
+
+ for(String var : modelCheckingInfo.getVariables()) {
+ Method method = machine.getClass().getMethod(var);
+ method.setAccessible(true);
+ methods.put(var, method);
+ }
+
+ Method copyMethod = machine.getClass().getMethod("_copy");
+ copyMethod.setAccessible(true);
+ methods.put("_copy", copyMethod);
+
+ Method checkInvMethod = machine.getClass().getMethod("_check_inv");
+ checkInvMethod.setAccessible(true);
+ methods.put("_check_inv", checkInvMethod);
+
+ } catch (Exception e) {
+ e.printStackTrace();
+ }
+ }
+
+ private Object[] tupleToList(BTuple<?, ?> tuple, int length) {
+ if(length == 2) {
+ Object[] res = new Object[length];
+ res[0] = tuple.projection1();
+ res[1] = tuple.projection2();
+ return res;
+ } else {
+ Object[] res = new Object[length];
+ BTuple<?, ?> currentTuple = tuple;
+ for(int i = 0; i < length - 2; i++) {
+ res[i] = currentTuple.projection1();
+ currentTuple = (BTuple<?, ?>) tuple.projection2();
+ }
+ res[length - 2] = currentTuple.projection1();
+ res[length - 1] = currentTuple.projection2();
+ return res;
+ }
+ }
+
+}
--
GitLab