Updates to the scenario-verifier integration

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

Hide file tree

Showing 6 changed files with 30 additions and 34 deletions.
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 org.intocps.verification.scenarioverifier.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.intocps.verification.scenarioverifier.core.*;
 import org.apache.commons.io.FilenameUtils;
 import org.apache.commons.lang3.tuple.Pair;
 import org.intocps.maestro.Mabl;
@@ -13,12 +13,11 @@
 import org.intocps.maestro.core.messages.IErrorReporter;
 import org.intocps.maestro.framework.fmi2.Fmi2SimulationEnvironment;
 import org.intocps.maestro.framework.fmi2.Fmi2SimulationEnvironmentConfiguration;
-import org.intocps.maestro.plugin.MasterModelMapper;
+import org.intocps.maestro.plugin.*;
 import org.intocps.maestro.template.ScenarioConfiguration;
 import picocli.CommandLine;
 import scala.jdk.javaapi.CollectionConverters;
-import synthesizer.ConfParser.ScenarioConfGenerator;
-import trace_analyzer.TraceAnalyzer;
+import org.intocps.verification.scenarioverifier.traceanalyzer.TraceAnalyzer;
 
 import java.io.*;
 import java.nio.charset.StandardCharsets;
@@ -54,7 +53,7 @@ public Integer call() throws Exception {
             output = Files.createTempDirectory("tmpDir").toFile();
         }
 
-        if (!VerifyTA.checkEnvironment()) {
+        if (!VerifyTA.isInstalled()) {
             System.out.println("Verification environment is not setup correctly");
             return -1;
         }
@@ -63,8 +62,9 @@ public Integer call() throws Exception {
         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();
+        ModelEncoding modelEncoding = new ModelEncoding(masterModel);
         try (FileWriter fileWriter = new FileWriter(uppaalFile)) {
-            fileWriter.write(ScenarioGenerator.generate(new ModelEncoding(masterModel)));
+            fileWriter.write(ScenarioGenerator.generateUppaalEncoding(modelEncoding));
         } catch (Exception e) {
             System.out.println("Unable to write encoded master model to file: " + e);
             return -1;
@@ -76,7 +76,6 @@ public Integer call() throws Exception {
         // from which a visualization can be made.
         if (resultCode == 1) {
             Path videoTraceFolder = output.toPath();
-            ModelEncoding modelEncoding = new ModelEncoding(masterModel);
             try (BufferedReader bufferedReader = new BufferedReader(new FileReader(traceFile))) {
                 TraceAnalyzer.AnalyseScenario(masterModel.name(), CollectionConverters.asScala(bufferedReader.lines().iterator()), modelEncoding,
                         videoTraceFolder.toString());
@@ -120,13 +119,13 @@ public Integer call() throws Exception {
             output = Files.createTempDirectory("tmpDir").toFile();
         }
         File uppaalFile = output.toPath().resolve("uppaal.xml").toFile();
-        if (VerifyTA.checkEnvironment()) {
+        if (VerifyTA.isInstalled()) {
             try (FileWriter fileWriter = new FileWriter(uppaalFile)) {
-                fileWriter.write(ScenarioGenerator.generate(new ModelEncoding(masterModel)));
+                fileWriter.write(ScenarioGenerator.generateUppaalEncoding(new ModelEncoding(masterModel)));
             } catch (Exception e) {
                 System.out.println("Unable to write encoded master model to file: " + e);
             }
-            resultCode = VerifyTA.verify(uppaalFile);
+            resultCode = VerifyTA.verify(uppaalFile, false);
         } else {
             System.out.println("Verification environment is not setup correctly");
             return -1;
@@ -172,7 +171,7 @@ public Integer call() throws Exception {
             return -1;
         }
 
-        String algorithm = ScenarioConfGenerator.generate(masterModel, masterModel.name());
+        String algorithm = masterModel.toConf(0);
         Path algorithmPath = output.toPath().resolve("masterModel.conf");
         Files.write(algorithmPath, algorithm.getBytes(StandardCharsets.UTF_8));
 
@@ -239,7 +238,6 @@ public Integer call() throws Exception {
             }
         }
 
-
         String masterModelAsString;
         Path algorithmPath;
         if (algorithmFile == null) {
@@ -249,7 +247,7 @@ 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());
+                masterModelAsString = masterModel.toConf(0);
 
                 Files.write(algorithmPath, masterModelAsString.getBytes(StandardCharsets.UTF_8));
             } catch (Exception e) {

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,6 +1,6 @@
 package org.intocps.maestro.template;
 
-import core.MasterModel;
+import org.intocps.verification.scenarioverifier.core.MasterModel;
 import org.apache.commons.lang3.tuple.Pair;
 import org.intocps.maestro.core.Framework;
 import org.intocps.maestro.framework.fmi2.Fmi2SimulationEnvironment;

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.intocps.verification.scenarioverifier.core.MasterModel;
 import org.apache.commons.text.StringEscapeUtils;
 import org.intocps.maestro.ast.LexIdentifier;
 import org.intocps.maestro.ast.MableAstFactory;
@@ -18,7 +18,6 @@
 import org.intocps.maestro.plugin.Sigver;
 import org.intocps.maestro.plugin.SigverConfig;
 import scala.jdk.javaapi.CollectionConverters;
-import synthesizer.ConfParser.ScenarioConfGenerator;
 
 import java.util.*;
 import java.util.stream.Collectors;
@@ -124,12 +123,13 @@ public static ASimulationSpecificationCompilationUnit generateTemplate(ScenarioC
 
         // Setup and add scenario verifier config
         SigverConfig expansionConfig = new SigverConfig();
-        expansionConfig.masterModel = ScenarioConfGenerator.generate(masterModel, masterModel.name());
+        expansionConfig.masterModel = masterModel.toConf(0);
         expansionConfig.parameters = configuration.getParameters();
         expansionConfig.relTol = configuration.getExecutionParameters().getConvergenceRelativeTolerance();
         expansionConfig.absTol = configuration.getExecutionParameters().getConvergenceAbsoluteTolerance();
         expansionConfig.convergenceAttempts = configuration.getExecutionParameters().getConvergenceAttempts();
 
+        // TODO Kenneth: Take a look at this
         AConfigStm configStm = new AConfigStm(StringEscapeUtils.escapeJava((new ObjectMapper()).writeValueAsString(expansionConfig)));
         dynamicScope.add(configStm);
 

diff --git a/plugins/sigver/pom.xml b/plugins/sigver/pom.xml
@@ -33,13 +33,11 @@
             <version>${project.version}</version>
             <scope>compile</scope>
         </dependency>
-
- <dependency>
-   <groupId>org.into-cps.verification</groupId>
-    <artifactId>scenario_verifier</artifactId>
-<version>0.2.21-SNAPSHOT</version>
-  </dependency>
-
+        <dependency>
+            <groupId>org.into-cps.verification</groupId>
+            <artifactId>scenario_verifier</artifactId>
+            <version>0.2.21-SNAPSHOT</version>
+        </dependency>
         <dependency>
             <groupId>org.jetbrains.kotlin</groupId>
             <artifactId>kotlin-stdlib-jdk8</artifactId>

diff --git a/plugins/sigver/src/main/java/org/intocps/maestro/plugin/Sigver.java b/plugins/sigver/src/main/java/org/intocps/maestro/plugin/Sigver.java
@@ -1,7 +1,6 @@
 package org.intocps.maestro.plugin;
 
 import com.fasterxml.jackson.databind.ObjectMapper;
-import core.*;
 import org.intocps.maestro.ast.AFunctionDeclaration;
 import org.intocps.maestro.ast.AModuleDeclaration;
 import org.intocps.maestro.ast.MableAstFactory;
@@ -23,8 +22,9 @@
 import org.slf4j.Logger;
 import org.slf4j.LoggerFactory;
 import scala.jdk.javaapi.CollectionConverters;
-import synthesizer.LoopStrategy;
-import synthesizer.SynthesizerSimple;
+import org.intocps.verification.scenarioverifier.core.*;
+import org.intocps.verification.scenarioverifier.synthesizer.LoopStrategy;
+import org.intocps.verification.scenarioverifier.synthesizer.SynthesizerSimple;
 
 import javax.xml.xpath.XPathExpressionException;
 import java.io.ByteArrayInputStream;
@@ -309,8 +309,8 @@ private Map<ComponentVariableFmi2Api, Map.Entry<Fmi2Builder.BoolVariable<PStm>,
 
         // Loop over step instructions and map them to MaBL
         coSimStepInstructions.forEach(instruction -> {
-            if (instruction instanceof core.Set) {
-                mapSetInstruction(((core.Set) instruction).port(), sharedPortVars, fmuInstances, connections);
+            if (instruction instanceof org.intocps.verification.scenarioverifier.core.Set) {
+                mapSetInstruction(((org.intocps.verification.scenarioverifier.core.Set) instruction).port(), sharedPortVars, fmuInstances, connections);
             } else if (instruction instanceof Get) {
                 Map<PortFmi2Api, VariableFmi2Api<Object>> portsWithGets = mapGetInstruction(((Get) instruction).port(), fmuInstances);
                 portsWithGets.forEach((key, value) -> sharedPortVars.stream()

diff --git a/...gver/src/main/kotlin/MasterModelMapper.kt → ...tocps/maestro/plugin/MasterModelMapper.kt b/...gver/src/main/kotlin/MasterModelMapper.kt → ...tocps/maestro/plugin/MasterModelMapper.kt
@@ -1,12 +1,12 @@
 package org.intocps.maestro.plugin
 
-import api.GenerationAPI
-import core.*
 import org.intocps.maestro.core.dto.ExtendedMultiModel
 import org.intocps.maestro.fmi.Fmi2ModelDescription
 import org.intocps.maestro.framework.fmi2.Fmi2SimulationEnvironment
 import org.intocps.maestro.framework.fmi2.Fmi2SimulationEnvironmentConfiguration
 import scala.jdk.javaapi.CollectionConverters
+import org.intocps.verification.scenarioverifier.api.GenerationAPI
+import org.intocps.verification.scenarioverifier.core.*
 
 class MasterModelMapper {
     companion object {
@@ -32,7 +32,7 @@ class MasterModelMapper {
         fun scenarioToMasterModel(scenario: String): MasterModel {
             // Load master model without algorithm
             val masterModel = ScenarioLoader.load(scenario.byteInputStream())
-            return GenerationAPI.generateAlgorithm(masterModel.name(), masterModel.scenario())
+            return GenerationAPI.synthesizeAlgorithm(masterModel.name(), masterModel.scenario())
         }
 
         fun masterModelConnectionsToMultiModelConnections(masterModel: MasterModel): HashMap<String, MutableList<String>> {
@@ -157,7 +157,7 @@ class MasterModelMapper {
             )
 
             // Generate the master model from the scenario
-            return GenerationAPI.generateAlgorithm("generatedFromMultiModel", scenarioModel)
+            return GenerationAPI.synthesizeAlgorithm("generatedFromMultiModel", scenarioModel)
         }
     }
 }