partial patch for scenario verifier 0.2.21-SNAPSHOT upgrade

INTO-CPS-Association · Dec 7, 2023 · 8dd024e · 8dd024e
1 parent 5a45009
commit 8dd024e
Show file tree

Hide file tree

Showing 9 changed files with 218 additions and 182 deletions.
diff --git a/frameworks/fmi2/src/main/java/org/intocps/maestro/framework/fmi2/Fmi2FmuValidator.java b/frameworks/fmi2/src/main/java/org/intocps/maestro/framework/fmi2/Fmi2FmuValidator.java
@@ -15,9 +15,9 @@
 public class Fmi2FmuValidator implements IFmuValidator {
     final static Logger logger = LoggerFactory.getLogger(Fmi2FmuValidator.class);
 
-    static {
-        System.setProperty("vdmj.mapping.search_path", "/annotations");
-    }
+//    static {
+//        System.setProperty("vdmj.mapping.search_path", "/annotations");
+//    }
 
     /**
      * returns true if validation could be performed. I.e. true does NOT indicate that no errors were found.

diff --git a/maestro-webapi/src/main/java/org/intocps/maestro/webapi/maestro2/Maestro2Broker.java b/maestro-webapi/src/main/java/org/intocps/maestro/webapi/maestro2/Maestro2Broker.java
@@ -2,8 +2,7 @@
 
 import com.fasterxml.jackson.databind.ObjectMapper;
 import com.spencerwi.either.Either;
-import core.MasterModel;
-import core.ScenarioLoader;
+
 import org.apache.commons.lang3.tuple.Pair;
 import org.intocps.maestro.Mabl;
 import org.intocps.maestro.ast.LexIdentifier;
@@ -30,6 +29,8 @@
 import org.intocps.maestro.webapi.maestro2.dto.SigverSimulateRequestBody;
 import org.intocps.maestro.webapi.maestro2.dto.SimulateRequestBody;
 import org.intocps.maestro.webapi.maestro2.interpreter.WebApiInterpreterFactory;
+import org.intocps.verification.scenarioverifier.core.MasterModel;
+import org.intocps.verification.scenarioverifier.core.ScenarioLoader;
 import org.slf4j.Logger;
 import org.slf4j.LoggerFactory;
 import org.springframework.web.socket.WebSocketSession;

diff --git a/...-webapi/src/main/java/org/intocps/maestro/webapi/maestro2/Maestro2ScenarioController.java b/...-webapi/src/main/java/org/intocps/maestro/webapi/maestro2/Maestro2ScenarioController.java
@@ -1,27 +1,25 @@
 package org.intocps.maestro.webapi.maestro2;
 
-import api.TraceResult;
-import api.VerificationAPI;
-import cli.VerifyTA;
-import core.MasterModel;
-import core.ModelEncoding;
-import core.ScenarioGenerator;
-import core.ScenarioLoader;
+
 import org.intocps.maestro.core.dto.ExtendedMultiModel;
 import org.intocps.maestro.core.messages.ErrorReporter;
 import org.intocps.maestro.plugin.MasterModelMapper;
 import org.intocps.maestro.webapi.dto.ExecutableMasterAndMultiModelTDO;
 import org.intocps.maestro.webapi.dto.VerificationDTO;
 import org.intocps.maestro.webapi.maestro2.dto.SigverSimulateRequestBody;
 import org.intocps.maestro.webapi.util.ZipDirectory;
+import org.intocps.verification.scenarioverifier.api.TraceResult;
+import org.intocps.verification.scenarioverifier.cli.VerifyTA;
+import org.intocps.verification.scenarioverifier.core.MasterModel;
+import org.intocps.verification.scenarioverifier.core.ModelEncoding;
+import org.intocps.verification.scenarioverifier.core.ScenarioLoader;
 import org.springframework.core.io.FileSystemResource;
 import org.springframework.http.HttpStatus;
 import org.springframework.http.MediaType;
 import org.springframework.http.ResponseEntity;
 import org.springframework.http.converter.HttpMessageNotReadableException;
 import org.springframework.stereotype.Component;
 import org.springframework.web.bind.annotation.*;
-import synthesizer.ConfParser.ScenarioConfGenerator;
 
 import javax.servlet.http.HttpServletRequest;
 import javax.servlet.http.HttpServletResponse;

diff --git a/maestro/src/main/java/org/intocps/maestro/cli/SigverCmd.java b/maestro/src/main/java/org/intocps/maestro/cli/SigverCmd.java
@@ -1,10 +1,10 @@
 package org.intocps.maestro.cli;
 
-import cli.VerifyTA;
+
 import com.fasterxml.jackson.core.type.TypeReference;
 import com.fasterxml.jackson.databind.JsonNode;
 import com.fasterxml.jackson.databind.ObjectMapper;
-import core.*;
+
 import org.apache.commons.io.FilenameUtils;
 import org.apache.commons.lang3.tuple.Pair;
 import org.intocps.maestro.Mabl;
@@ -15,10 +15,14 @@
 import org.intocps.maestro.framework.fmi2.Fmi2SimulationEnvironmentConfiguration;
 import org.intocps.maestro.plugin.MasterModelMapper;
 import org.intocps.maestro.template.ScenarioConfiguration;
+import org.intocps.verification.scenarioverifier.core.*;
+import org.intocps.verification.scenarioverifier.synthesizer.*;
+import org.intocps.verification.scenarioverifier.traceanalyzer.*;
+import org.intocps.verification.scenarioverifier.cli.*;
 import picocli.CommandLine;
 import scala.jdk.javaapi.CollectionConverters;
-import synthesizer.ConfParser.ScenarioConfGenerator;
-import trace_analyzer.TraceAnalyzer;
+import scala.reflect.io.Directory;
+
 
 import java.io.*;
 import java.nio.charset.StandardCharsets;
@@ -54,21 +58,24 @@ public Integer call() throws Exception {
             output = Files.createTempDirectory("tmpDir").toFile();
         }
 
-        if (!VerifyTA.checkEnvironment()) {
-            System.out.println("Verification environment is not setup correctly");
-            return -1;
-        }
+//        if (!VerifyTA.checkEnvironment()) {
+//            System.out.println("Verification environment is not setup correctly");
+//            return -1;
+//        }
 
         File tempDir = Files.createTempDirectory("tmpDir").toFile();
         MasterModel masterModel = ScenarioLoader.load(new ByteArrayInputStream(Files.readString(file.toPath()).getBytes()));
         File uppaalFile = Path.of(tempDir.getPath(), "uppaal.xml").toFile();
         File traceFile = Path.of(tempDir.getPath(), "trace.log").toFile();
-        try (FileWriter fileWriter = new FileWriter(uppaalFile)) {
-            fileWriter.write(ScenarioGenerator.generate(new ModelEncoding(masterModel)));
-        } catch (Exception e) {
-            System.out.println("Unable to write encoded master model to file: " + e);
-            return -1;
-        }
+
+        File f=ScenarioGenerator.generateUppaalFile(masterModel.name(),new ModelEncoding(masterModel),new Directory(output));
+        Files.copy(f.toPath(),uppaalFile.toPath());
+//        try (FileWriter fileWriter = new FileWriter(uppaalFile)) {
+//            fileWriter.write(ScenarioGenerator.generate(new ModelEncoding(masterModel)));
+//        } catch (Exception e) {
+//            System.out.println("Unable to write encoded master model to file: " + e);
+//            return -1;
+//        }
         // This verifies the algorithm and writes to the trace file.
         int resultCode = VerifyTA.saveTraceToFile(uppaalFile, traceFile);
 
@@ -120,17 +127,21 @@ public Integer call() throws Exception {
             output = Files.createTempDirectory("tmpDir").toFile();
         }
         File uppaalFile = output.toPath().resolve("uppaal.xml").toFile();
-        if (VerifyTA.checkEnvironment()) {
-            try (FileWriter fileWriter = new FileWriter(uppaalFile)) {
-                fileWriter.write(ScenarioGenerator.generate(new ModelEncoding(masterModel)));
-            } catch (Exception e) {
-                System.out.println("Unable to write encoded master model to file: " + e);
-            }
-            resultCode = VerifyTA.verify(uppaalFile);
-        } else {
-            System.out.println("Verification environment is not setup correctly");
-            return -1;
+        //if (VerifyTA.checkEnvironment())
+        {
+//            try (FileWriter fileWriter = new FileWriter(uppaalFile)) {
+//                fileWriter.write();
+//            } catch (Exception e) {
+//                System.out.println("Unable to write encoded master model to file: " + e);
+//            }
+            uppaalFile=  ScenarioGenerator.generateUppaalFile("uupaal",new ModelEncoding(masterModel),
+                    new Directory(output.getAbsoluteFile()));
+            resultCode = VerifyTA.verify(uppaalFile,false);
         }
+//        else {
+//            System.out.println("Verification environment is not setup correctly");
+//            return -1;
+//        }
 
         System.out.println("Output written to: " + output.getPath());
 
@@ -172,9 +183,10 @@ public Integer call() throws Exception {
             return -1;
         }
 
-        String algorithm = ScenarioConfGenerator.generate(masterModel, masterModel.name());
+       File f= ScenarioGenerator.generateUppaalFile(masterModel.name(),new ModelEncoding(masterModel), new Directory(output)) ;
         Path algorithmPath = output.toPath().resolve("masterModel.conf");
-        Files.write(algorithmPath, algorithm.getBytes(StandardCharsets.UTF_8));
+        Files.copy(f.toPath(),algorithmPath);
+//        Files.write(algorithmPath, algorithm.getBytes(StandardCharsets.UTF_8));
 
         return 0;
     }
@@ -249,9 +261,11 @@ public Integer call() throws Exception {
                 ExtendedMultiModel multiModel = (new ObjectMapper()).readValue(extendedMultiModelFile, ExtendedMultiModel.class);
                 MasterModel masterModel = MasterModelMapper.Companion.multiModelToMasterModel(multiModel, 3);
 
-                masterModelAsString = ScenarioConfGenerator.generate(masterModel, masterModel.name());
+                //FIXME class removed ScenarioConfGenerator
+                throw new RuntimeException("ScenarioConfGenerator removed");
+//                masterModelAsString = ScenarioConfGenerator.generate(masterModel, masterModel.name());
 
-                Files.write(algorithmPath, masterModelAsString.getBytes(StandardCharsets.UTF_8));
+//                Files.write(algorithmPath, masterModelAsString.getBytes(StandardCharsets.UTF_8));
             } catch (Exception e) {
                 System.out.println("Unable to generate masterModel: " + e);
                 return -1;

diff --git a/maestro/src/main/java/org/intocps/maestro/template/ScenarioConfiguration.java b/maestro/src/main/java/org/intocps/maestro/template/ScenarioConfiguration.java
@@ -1,10 +1,11 @@
 package org.intocps.maestro.template;
 
-import core.MasterModel;
+
 import org.apache.commons.lang3.tuple.Pair;
 import org.intocps.maestro.core.Framework;
 import org.intocps.maestro.framework.fmi2.Fmi2SimulationEnvironment;
 import org.intocps.maestro.framework.fmi2.Fmi2SimulationEnvironmentConfiguration;
+import org.intocps.verification.scenarioverifier.core.MasterModel;
 
 import java.util.List;
 import java.util.Map;

diff --git a/maestro/src/main/java/org/intocps/maestro/template/TemplateGeneratorFromScenario.java b/maestro/src/main/java/org/intocps/maestro/template/TemplateGeneratorFromScenario.java
@@ -1,7 +1,7 @@
 package org.intocps.maestro.template;
 
 import com.fasterxml.jackson.databind.ObjectMapper;
-import core.MasterModel;
+
 import org.apache.commons.text.StringEscapeUtils;
 import org.intocps.maestro.ast.LexIdentifier;
 import org.intocps.maestro.ast.MableAstFactory;
@@ -17,9 +17,16 @@
 import org.intocps.maestro.framework.fmi2.api.mabl.variables.FmuVariableFmi2Api;
 import org.intocps.maestro.plugin.Sigver;
 import org.intocps.maestro.plugin.SigverConfig;
+import org.intocps.verification.scenarioverifier.core.MasterModel;
+import org.intocps.verification.scenarioverifier.core.ModelEncoding;
+import org.intocps.verification.scenarioverifier.core.ScenarioGenerator;
 import scala.jdk.javaapi.CollectionConverters;
-import synthesizer.ConfParser.ScenarioConfGenerator;
+import scala.reflect.io.Directory;
+
 
+import java.io.File;
+import java.nio.charset.StandardCharsets;
+import java.nio.file.Files;
 import java.util.*;
 import java.util.stream.Collectors;
 
@@ -124,7 +131,12 @@ public static ASimulationSpecificationCompilationUnit generateTemplate(ScenarioC
 
         // Setup and add scenario verifier config
         SigverConfig expansionConfig = new SigverConfig();
-        expansionConfig.masterModel = ScenarioConfGenerator.generate(masterModel, masterModel.name());
+
+       File f= ScenarioGenerator.generateUppaalFile(masterModel.name(),new ModelEncoding(masterModel),new Directory(new File(System.getProperty(
+               "java.io" +
+                ".tmpdir"))));
+
+        expansionConfig.masterModel = Files.readString(f.toPath(), StandardCharsets.UTF_8);
         expansionConfig.parameters = configuration.getParameters();
         expansionConfig.relTol = configuration.getExecutionParameters().getConvergenceRelativeTolerance();
         expansionConfig.absTol = configuration.getExecutionParameters().getConvergenceAbsoluteTolerance();