Updated references to Scenario-Verifier

maestro-webapi/src/main/java/org/intocps/maestro/webapi/maestro2/Maestro2Broker.java

@@ -2,8 +2,8 @@
 
 import com.fasterxml.jackson.databind.ObjectMapper;
 import com.spencerwi.either.Either;
-import core.MasterModel;
-import core.ScenarioLoader;
+import org.intocps.verification.scenarioverifier.core.MasterModel;
+import org.intocps.verification.scenarioverifier.core.ScenarioLoader;
 import org.apache.commons.lang3.tuple.Pair;
 import org.intocps.maestro.Mabl;
 import org.intocps.maestro.ast.LexIdentifier;

maestro-webapi/src/main/java/org/intocps/maestro/webapi/maestro2/Maestro2ScenarioController.java

@@ -1,17 +1,16 @@
 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.verification.scenarioverifier.core.MasterModel;
+import org.intocps.verification.scenarioverifier.core.ScenarioLoader;
+import org.intocps.verification.scenarioverifier.core.ModelEncoding;
+import org.intocps.verification.scenarioverifier.core.ScenarioGenerator;
+import org.intocps.verification.scenarioverifier.api.TraceResult;
+import org.intocps.verification.scenarioverifier.api.VerificationAPI;
+import org.intocps.verification.scenarioverifier.cli.VerifyTA;
 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.dto.VerificationResult;
 import org.intocps.maestro.webapi.maestro2.dto.SigverSimulateRequestBody;
 import org.intocps.maestro.webapi.util.ZipDirectory;
 import org.springframework.core.io.FileSystemResource;
@@ -21,7 +20,6 @@
 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;
@@ -45,25 +43,25 @@ public ResponseEntity<String> handleJsonParseException(HttpMessageNotReadableExc
             produces = MediaType.TEXT_PLAIN_VALUE)
     public String generateAlgorithmFromScenario(@RequestBody String scenario) {
         MasterModel masterModel = MasterModelMapper.Companion.scenarioToMasterModel(scenario);
-        return ScenarioConfGenerator.generate(masterModel, masterModel.name());
+        return masterModel.toConf(0);
     }
 
     @RequestMapping(value = "/generateAlgorithmFromMultiModel", method = RequestMethod.POST, consumes = MediaType.APPLICATION_JSON_VALUE,
             produces = MediaType.TEXT_PLAIN_VALUE)
     public String generateAlgorithmFromMultiModel(@RequestBody ExtendedMultiModel multiModel) {
         // MaxPossibleStepSize is related to verification in Uppaal.
         MasterModel masterModel = MasterModelMapper.Companion.multiModelToMasterModel(multiModel, 3);
-        return ScenarioConfGenerator.generate(masterModel, masterModel.name());
+        return masterModel.toConf(0);
     }
 
     @RequestMapping(value = "/verifyAlgorithm", method = RequestMethod.POST, consumes = MediaType.TEXT_PLAIN_VALUE,
             produces = MediaType.APPLICATION_JSON_VALUE)
-    public VerificationDTO verifyAlgorithm(@RequestBody String masterModelAsString) throws IOException {
+    public VerificationResult verifyAlgorithm(@RequestBody String masterModelAsString) throws IOException {
         // Check that UPPAAL is available
         try {
-            VerificationAPI.checkUppaalVersion();
+            VerifyTA.isInstalled();
         } catch (Exception e) {
-            return new VerificationDTO(false, "", "UPPAAL v.4.1 is not in PATH - please install it and try again!");
+            return new VerificationResult(false, "", "UPPAAL v.4.1 is not in PATH - please install it and try again!");
         }
 
         // Load the master model, verify the algorithm and return success and any error message.
@@ -75,25 +73,25 @@ public VerificationDTO verifyAlgorithm(@RequestBody String masterModelAsString)
         try (Writer writer = new BufferedWriter(new OutputStreamWriter(new FileOutputStream(tempFile), StandardCharsets.UTF_8))) {
             writer.write(encodedModel);
         }
-        int verificationCode = VerifyTA.verify(tempFile);
+        int verificationCode = VerifyTA.verify(tempFile, false);
         tempFile.delete();
         switch (verificationCode) {
             case 0:
-                return new VerificationDTO(true, encodedModel, "");
+                return new VerificationResult(true, encodedModel, "");
             case 1:
-                return new VerificationDTO(false, encodedModel, "Model is not valid. Generate the trace and use it to correct the algorithm.");
+                return new VerificationResult(false, encodedModel, "Model is not valid. Generate the trace and use it to correct the algorithm.");
             case 2:
-                return new VerificationDTO(false, encodedModel,
+                return new VerificationResult(false, encodedModel,
                         "The verification in Uppaal failed most likely due to a syntax error in the " + "UPPAAL model.");
             default:
-                return new VerificationDTO(false, encodedModel, "");
+                return new VerificationResult(false, encodedModel, "");
         }
     }
 
     @RequestMapping(value = "/visualizeTrace", method = RequestMethod.POST, consumes = MediaType.TEXT_PLAIN_VALUE, produces = "video/mp4")
     public FileSystemResource visualizeTrace(@RequestBody String masterModelAsString) throws Exception {
         MasterModel masterModel = ScenarioLoader.load(new ByteArrayInputStream(masterModelAsString.getBytes()));
-        TraceResult traceResult = VerificationAPI.generateTraceFromMasterModel(masterModel);
+        TraceResult traceResult = VerificationAPI.generateTraceVideo(masterModel);
 
         if (!traceResult.isGenerated()) {
             throw new Exception("Unable to generate trace results - the algorithm is probably successfully verified");
@@ -130,8 +128,7 @@ public void executeAlgorithm(@RequestBody ExecutableMasterAndMultiModelTDO execu
             Maestro2Broker broker = new Maestro2Broker(zipDir, reporter, () -> false);
 
             SigverSimulateRequestBody requestBody = new SigverSimulateRequestBody(executableModel.getExecutionParameters().getStartTime(),
-                    executableModel.getExecutionParameters().getEndTime(), Map.of(), false, 0d,
-                    ScenarioConfGenerator.generate(masterModel, masterModel.name()));
+                    executableModel.getExecutionParameters().getEndTime(), Map.of(), false, 0d, masterModel.toConf(0));
 
             broker.buildAndRunMasterModel(null, null, executableModel.getMultiModel(), requestBody, new File(zipDir, "outputs.csv"));
 

maestro-webapi/src/main/java/org/intocps/maestro/webapi/maestro2/dto/VerificationResult.java

@@ -0,0 +1,21 @@
+package org.intocps.maestro.webapi.maestro2.dto;
+
+import com.fasterxml.jackson.annotation.JsonProperty;
+
+public class VerificationResult {
+    @JsonProperty("correct")
+    public Boolean correct;
+    @JsonProperty("masterModel")
+    public String masterModel;
+    @JsonProperty("errorMessage")
+    public String errorMessage;
+
+    public VerificationResult() {
+    }
+
+    public VerificationResult(Boolean correct, String masterModel, String errorMessage) {
+        this.correct = correct;
+        this.masterModel = masterModel;
+        this.errorMessage = errorMessage;
+    }
+}