From 2ab8e2d24d3d4e6070f62124c9e17ef155af3198 Mon Sep 17 00:00:00 2001 From: Simon Thrane Date: Fri, 8 Dec 2023 14:55:52 +0100 Subject: [PATCH] Updates to the scenario-verifier integration --- .../org/intocps/maestro/cli/SigverCmd.java | 26 +++++++++---------- .../template/ScenarioConfiguration.java | 2 +- .../TemplateGeneratorFromScenario.java | 6 ++--- plugins/sigver/pom.xml | 12 ++++----- .../org/intocps/maestro/plugin/Sigver.java | 10 +++---- .../maestro/plugin}/MasterModelMapper.kt | 8 +++--- 6 files changed, 30 insertions(+), 34 deletions(-) rename plugins/sigver/src/main/kotlin/{ => org/intocps/maestro/plugin}/MasterModelMapper.kt (96%) diff --git a/maestro/src/main/java/org/intocps/maestro/cli/SigverCmd.java b/maestro/src/main/java/org/intocps/maestro/cli/SigverCmd.java index d29af9d18..290bbbad5 100644 --- 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 index 7fa5d07c8..ebbbc796a 100644 --- 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 index a1c8903ba..d5660804e 100644 --- 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 index 6234818be..2c0ed8760 100644 --- a/plugins/sigver/pom.xml +++ b/plugins/sigver/pom.xml @@ -33,13 +33,11 @@ ${project.version} compile - - - org.into-cps.verification - scenario_verifier -0.2.21-SNAPSHOT - - + + org.into-cps.verification + scenario_verifier + 0.2.21-SNAPSHOT + org.jetbrains.kotlin kotlin-stdlib-jdk8 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 index d6e5b955c..1c5d68b6d 100644 --- 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, // 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> portsWithGets = mapGetInstruction(((Get) instruction).port(), fmuInstances); portsWithGets.forEach((key, value) -> sharedPortVars.stream() diff --git a/plugins/sigver/src/main/kotlin/MasterModelMapper.kt b/plugins/sigver/src/main/kotlin/org/intocps/maestro/plugin/MasterModelMapper.kt similarity index 96% rename from plugins/sigver/src/main/kotlin/MasterModelMapper.kt rename to plugins/sigver/src/main/kotlin/org/intocps/maestro/plugin/MasterModelMapper.kt index 0e9b983ef..31d813db5 100644 --- a/plugins/sigver/src/main/kotlin/MasterModelMapper.kt +++ b/plugins/sigver/src/main/kotlin/org/intocps/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> { @@ -157,7 +157,7 @@ class MasterModelMapper { ) // Generate the master model from the scenario - return GenerationAPI.generateAlgorithm("generatedFromMultiModel", scenarioModel) + return GenerationAPI.synthesizeAlgorithm("generatedFromMultiModel", scenarioModel) } } } \ No newline at end of file