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 5b6ca772817f33531f50d59607574540ebce4d7e..a63a36c6b371297c9b90867b5f6943e49f765d62 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 0000000000000000000000000000000000000000..e6829aa2baf5dd498c43e73edb0d20d552a9fe31 --- /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; + } + } + +}