Added JNI support for alloy

se-buw · Jul 25, 2024 · fd86236 · fd86236
1 parent 8e3cc34
commit fd86236
Show file tree

Hide file tree

Showing 3 changed files with 33 additions and 4 deletions.
diff --git a/alloy-api/Dockerfile b/alloy-api/Dockerfile
@@ -2,10 +2,12 @@ FROM openjdk:17-jdk-alpine
 
 WORKDIR /app
 COPY . /app
+
+RUN apk add --no-cache libstdc++
 RUN sed -i -e 's/\r$//' gradlew
 RUN chmod +x gradlew
-RUN ./gradlew clean build
+RUN ./gradlew clean build -x test 
 RUN mv build/libs/fmp.alloy.api-0.0.1.jar app.jar
 EXPOSE 8080
 
-ENTRYPOINT ["java","-jar","app.jar"]
+ENTRYPOINT ["java","-Djava.library.path=lib/", "-jar","app.jar"]
diff --git a/alloy-api/lib/libminisat.so b/alloy-api/lib/libminisat.so
diff --git a/alloy-api/src/main/java/de/buw/fmp/alloy/api/AlloyInstanceController.java b/alloy-api/src/main/java/de/buw/fmp/alloy/api/AlloyInstanceController.java
@@ -34,6 +34,13 @@ public class AlloyInstanceController {
 
     static Map<String, StoredSolution> instances = new LinkedHashMap<>();
 
+    public static A4Options getOptions() {
+        A4Options opt = new A4Options();
+        String osName = System.getProperty("os.name").toLowerCase();
+        opt.solver = osName.contains("linux") ? A4Options.SatSolver.MiniSatJNI : A4Options.SatSolver.SAT4J;
+        return opt;
+      }
+
     @PostMapping("/instance/{cmd}")
     public String getInstance(@RequestBody InstanceRequest instanceRequest, @PathVariable int cmd) throws IOException {
         String code = instanceRequest.getCode();
@@ -54,9 +61,18 @@ public String getInstance(@RequestBody InstanceRequest instanceRequest, @PathVar
             runCommand = new Command(Pos.UNKNOWN, ExprConstant.TRUE, "FMPlayDefault", false, 4, 4, 4, -1, -1, -1, null, null, ExprConstant.TRUE, null);
         };
 
-        A4Options options = new A4Options();
+        A4Options options = getOptions();
         // get the first instance of the Alloy file
-        A4Solution instance = TranslateAlloyToKodkod.execute_command(A4Reporter.NOP, module.getAllSigs(), runCommand, options);
+        A4Solution instance;
+        try {
+            instance = TranslateAlloyToKodkod.execute_command(A4Reporter.NOP, module.getAllSigs(), runCommand, options);            
+        } catch (Exception e) {
+            // return error message as JSON with http status code 400
+            JSONObject obj = new JSONObject();
+            obj.put("error", e.toString());
+            obj.put("status", HttpStatus.BAD_REQUEST.value());
+            return obj.toString();
+        }
 
         String specId = null;
         if (!instance.satisfiable()) {
@@ -82,6 +98,8 @@ public String getInstance(@RequestBody InstanceRequest instanceRequest, @PathVar
         if (specId != null) {
             xmlJSONObj.append("specId", specId);
         }
+        String tabularInstance = instance.format();
+        xmlJSONObj.append("tabularInstance", tabularInstance);
         String jsonPrettyPrintString = xmlJSONObj.toString(4);
 
         return jsonPrettyPrintString;
@@ -100,6 +118,13 @@ private boolean hasDefaultCommand(CompModule module) {
     @PostMapping("/nextInstance")
     public String getNextInstance(@RequestBody String specId) throws IOException {
         StoredSolution storedSolution = instances.get(specId);
+        if (storedSolution == null) {
+            JSONObject obj = new JSONObject();
+            obj.put("error", "No instance found, possibly cleaned up in the meantime");
+            obj.put("status", HttpStatus.BAD_REQUEST.value());
+            return obj.toString();
+        }
+
         A4Solution instance = storedSolution.getSolution();
 
         instance = instance.next();
@@ -119,6 +144,8 @@ public String getNextInstance(@RequestBody String specId) throws IOException {
         JSONObject xmlJSONObj = XML.toJSONObject(instanceContent);
 
         xmlJSONObj.append("specId", specId);
+        String tabularInstance = instance.format();
+        xmlJSONObj.append("tabularInstance", tabularInstance);
         String jsonPrettyPrintString = xmlJSONObj.toString(4);
 
         return jsonPrettyPrintString;