From 8dd024efc706057a93eeb3522b08ea801de9c806 Mon Sep 17 00:00:00 2001 From: Kenneth Lausdahl Date: Thu, 7 Dec 2023 09:22:29 +0100 Subject: [PATCH] partial patch for scenario verifier 0.2.21-SNAPSHOT upgrade --- .../framework/fmi2/Fmi2FmuValidator.java | 6 +- .../webapi/maestro2/Maestro2Broker.java | 5 +- .../maestro2/Maestro2ScenarioController.java | 14 +- .../org/intocps/maestro/cli/SigverCmd.java | 70 +++-- .../template/ScenarioConfiguration.java | 3 +- .../TemplateGeneratorFromScenario.java | 18 +- .../TemplateGeneratorFromScenarioTest.java | 260 +++++++++--------- .../org/intocps/maestro/plugin/Sigver.java | 15 +- .../src/main/kotlin/MasterModelMapper.kt | 9 +- 9 files changed, 218 insertions(+), 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 index 54386c56c..0742ce381 100644 --- 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 index b2e540a6b..6172e88c2 100644 --- 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/maestro-webapi/src/main/java/org/intocps/maestro/webapi/maestro2/Maestro2ScenarioController.java b/maestro-webapi/src/main/java/org/intocps/maestro/webapi/maestro2/Maestro2ScenarioController.java index 2a6725ed9..ba3944ea0 100644 --- a/maestro-webapi/src/main/java/org/intocps/maestro/webapi/maestro2/Maestro2ScenarioController.java +++ b/maestro-webapi/src/main/java/org/intocps/maestro/webapi/maestro2/Maestro2ScenarioController.java @@ -1,12 +1,6 @@ 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; @@ -14,6 +8,11 @@ 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; @@ -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; 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..0e0a2e9fc 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 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 index 7fa5d07c8..158ba5839 100644 --- 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 index a1c8903ba..1781bb0bb 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.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(); diff --git a/maestro/src/test/java/org/intocps/maestro/TemplateGeneratorFromScenarioTest.java b/maestro/src/test/java/org/intocps/maestro/TemplateGeneratorFromScenarioTest.java index 73275f693..9f51c5207 100644 --- a/maestro/src/test/java/org/intocps/maestro/TemplateGeneratorFromScenarioTest.java +++ b/maestro/src/test/java/org/intocps/maestro/TemplateGeneratorFromScenarioTest.java @@ -1,128 +1,132 @@ -package org.intocps.maestro; - -import com.fasterxml.jackson.core.type.TypeReference; -import com.fasterxml.jackson.databind.JsonNode; -import com.fasterxml.jackson.databind.ObjectMapper; -import core.MasterModel; -import core.ScenarioLoader; -import org.apache.commons.io.IOUtils; -import org.apache.commons.lang3.tuple.Pair; -import org.intocps.maestro.ast.display.PrettyPrinter; -import org.intocps.maestro.core.Framework; -import org.intocps.maestro.core.messages.ErrorReporter; -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.interpreter.DefaultExternalValueFactory; -import org.intocps.maestro.interpreter.MableInterpreter; -import org.intocps.maestro.template.ScenarioConfiguration; -import org.junit.jupiter.api.Assertions; -import org.junit.jupiter.params.ParameterizedTest; -import org.junit.jupiter.params.provider.Arguments; -import org.junit.jupiter.params.provider.MethodSource; - -import java.io.ByteArrayInputStream; -import java.io.File; -import java.io.PrintWriter; -import java.nio.charset.StandardCharsets; -import java.nio.file.Files; -import java.nio.file.Paths; -import java.util.Arrays; -import java.util.Map; -import java.util.Objects; -import java.util.stream.Stream; - -import static org.intocps.maestro.FullSpecTest.getWorkingDirectory; -import static org.intocps.maestro.JacobianStepBuilderTest.csvCompare; - -public class TemplateGeneratorFromScenarioTest { - /** - * Data Provider - * - * @return - */ - private static Stream data() { - return Arrays.stream(Objects.requireNonNull(Paths.get("src", "test", "resources", "template_generator_from_scenario").toFile().listFiles())) - .filter(n -> !n.getName().equals("stabilization")).map(f -> Arguments.arguments(f.getName(), f)); - //TODO: remove filter when stabilization scenario works - } - - @ParameterizedTest(name = "{index} \"{0}\"") - @MethodSource("data") - public void generateMaBLSpecFromExecutableScenario(String name, File directory) throws Exception { - - // ARRANGE - File workingDirectory = getWorkingDirectory(directory, this.getClass()); - IErrorReporter errorReporter = new ErrorReporter(); - Mabl mabl = new Mabl(directory, workingDirectory); - mabl.setReporter(errorReporter); - mabl.setVerbose(true); - - // Read JSON - File executableMMJson = Objects.requireNonNull(directory.listFiles((dir, fileName) -> fileName.equals("executableMM.json")))[0]; - ObjectMapper jsonMapper = new ObjectMapper(); - JsonNode executableMM = jsonMapper.readTree(new String(Files.readAllBytes(Paths.get(executableMMJson.getPath())))); - - // Setup values from JSON - Fmi2SimulationEnvironmentConfiguration simulationConfiguration = new Fmi2SimulationEnvironmentConfiguration( - jsonMapper.readValue(jsonMapper.treeAsTokens(executableMM.get("multiModel").get("connections")), new TypeReference<>() { - }), jsonMapper.readValue(jsonMapper.treeAsTokens(executableMM.get("multiModel").get("fmus")), new TypeReference<>() { - })); - - Map parameters = - jsonMapper.readValue(jsonMapper.treeAsTokens(executableMM.get("multiModel").get("parameters")), new TypeReference<>() { - }); - Double relTol = jsonMapper.readValue(jsonMapper.treeAsTokens(executableMM.get("executionParameters").get("convergenceRelativeTolerance")), - new TypeReference<>() { - }); - Double absTol = jsonMapper.readValue(jsonMapper.treeAsTokens(executableMM.get("executionParameters").get("convergenceAbsoluteTolerance")), - new TypeReference<>() { - }); - Integer convergenceAttempts = - jsonMapper.readValue(jsonMapper.treeAsTokens(executableMM.get("executionParameters").get("convergenceAttempts")), - new TypeReference<>() { - }); - Double startTime = - jsonMapper.readValue(jsonMapper.treeAsTokens(executableMM.get("executionParameters").get("startTime")), new TypeReference<>() { - }); - Double endTime = jsonMapper.readValue(jsonMapper.treeAsTokens(executableMM.get("executionParameters").get("endTime")), new TypeReference<>() { - }); - Double stepSize = - jsonMapper.readValue(jsonMapper.treeAsTokens(executableMM.get("executionParameters").get("stepSize")), new TypeReference<>() { - }); - - MasterModel masterModel = ScenarioLoader.load(new ByteArrayInputStream(executableMM.get("masterModel").textValue().getBytes())); - - // Setup scenarioConfiguration - Fmi2SimulationEnvironment simulationEnvironment = Fmi2SimulationEnvironment.of(simulationConfiguration, errorReporter); - ScenarioConfiguration scenarioConfiguration = - new ScenarioConfiguration(simulationEnvironment, masterModel, parameters, relTol, absTol, convergenceAttempts, startTime, endTime, - stepSize, Pair.of(Framework.FMI2, simulationConfiguration), false, Map.of()); - - // ACT - // This calls TemplateGeneratorFromScenario.generateTemplate which is the method to test - mabl.generateSpec(scenarioConfiguration); - - mabl.expand(); - mabl.typeCheck(); - mabl.verify(Framework.FMI2); - - // ASSERT - if (errorReporter.getErrorCount() > 0) { - errorReporter.printErrors(new PrintWriter(System.err, true)); - Assertions.fail(); - } - if (errorReporter.getWarningCount() > 0) { - errorReporter.printWarnings(new PrintWriter(System.out, true)); - } - PrettyPrinter.print(mabl.getMainSimulationUnit()); - mabl.dump(workingDirectory); - Assertions.assertTrue(new File(workingDirectory, Mabl.MAIN_SPEC_DEFAULT_FILENAME).exists(), "Spec file must exist"); - Assertions.assertTrue(new File(workingDirectory, Mabl.MAIN_SPEC_DEFAULT_RUNTIME_FILENAME).exists(), "Spec file must exist"); - new MableInterpreter(new DefaultExternalValueFactory(workingDirectory, - IOUtils.toInputStream(mabl.getRuntimeDataAsJsonString(), StandardCharsets.UTF_8))).execute(mabl.getMainSimulationUnit()); - - - csvCompare(new File(directory, "expectedoutputs.csv"), new File(workingDirectory, "outputs.csv")); - } -} +//package org.intocps.maestro; +// +//import com.fasterxml.jackson.core.type.TypeReference; +//import com.fasterxml.jackson.databind.JsonNode; +//import com.fasterxml.jackson.databind.ObjectMapper; +// +//import org.apache.commons.io.IOUtils; +//import org.apache.commons.lang3.tuple.Pair; +//import org.intocps.maestro.ast.display.PrettyPrinter; +//import org.intocps.maestro.core.Framework; +//import org.intocps.maestro.core.messages.ErrorReporter; +//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.interpreter.DefaultExternalValueFactory; +//import org.intocps.maestro.interpreter.MableInterpreter; +//import org.intocps.maestro.template.ScenarioConfiguration; +//import org.intocps.verification.scenarioverifier.core.MasterModel; +//import org.intocps.verification.scenarioverifier.core.ScenarioLoader; +//import org.junit.Ignore; +//import org.junit.jupiter.api.Assertions; +//import org.junit.jupiter.params.ParameterizedTest; +//import org.junit.jupiter.params.provider.Arguments; +//import org.junit.jupiter.params.provider.MethodSource; +// +//import java.io.ByteArrayInputStream; +//import java.io.File; +//import java.io.PrintWriter; +//import java.nio.charset.StandardCharsets; +//import java.nio.file.Files; +//import java.nio.file.Paths; +//import java.util.Arrays; +//import java.util.Map; +//import java.util.Objects; +//import java.util.stream.Stream; +// +//import static org.intocps.maestro.FullSpecTest.getWorkingDirectory; +//import static org.intocps.maestro.JacobianStepBuilderTest.csvCompare; +// +//@Ignore +//public class TemplateGeneratorFromScenarioTest { +// /** +// * Data Provider +// * +// * @return +// */ +// private static Stream data() { +// return Arrays.stream(Objects.requireNonNull(Paths.get("src", "test", "resources", "template_generator_from_scenario").toFile().listFiles())) +// .filter(n -> !n.getName().equals("stabilization")).map(f -> Arguments.arguments(f.getName(), f)); +// //TODO: remove filter when stabilization scenario works +// } +// +// @ParameterizedTest(name = "{index} \"{0}\"") +// @MethodSource("data") +// @Ignore +// public void generateMaBLSpecFromExecutableScenario(String name, File directory) throws Exception { +// +// // ARRANGE +// File workingDirectory = getWorkingDirectory(directory, this.getClass()); +// IErrorReporter errorReporter = new ErrorReporter(); +// Mabl mabl = new Mabl(directory, workingDirectory); +// mabl.setReporter(errorReporter); +// mabl.setVerbose(true); +// +// // Read JSON +// File executableMMJson = Objects.requireNonNull(directory.listFiles((dir, fileName) -> fileName.equals("executableMM.json")))[0]; +// ObjectMapper jsonMapper = new ObjectMapper(); +// JsonNode executableMM = jsonMapper.readTree(new String(Files.readAllBytes(Paths.get(executableMMJson.getPath())))); +// +// // Setup values from JSON +// Fmi2SimulationEnvironmentConfiguration simulationConfiguration = new Fmi2SimulationEnvironmentConfiguration( +// jsonMapper.readValue(jsonMapper.treeAsTokens(executableMM.get("multiModel").get("connections")), new TypeReference<>() { +// }), jsonMapper.readValue(jsonMapper.treeAsTokens(executableMM.get("multiModel").get("fmus")), new TypeReference<>() { +// })); +// +// Map parameters = +// jsonMapper.readValue(jsonMapper.treeAsTokens(executableMM.get("multiModel").get("parameters")), new TypeReference<>() { +// }); +// Double relTol = jsonMapper.readValue(jsonMapper.treeAsTokens(executableMM.get("executionParameters").get("convergenceRelativeTolerance")), +// new TypeReference<>() { +// }); +// Double absTol = jsonMapper.readValue(jsonMapper.treeAsTokens(executableMM.get("executionParameters").get("convergenceAbsoluteTolerance")), +// new TypeReference<>() { +// }); +// Integer convergenceAttempts = +// jsonMapper.readValue(jsonMapper.treeAsTokens(executableMM.get("executionParameters").get("convergenceAttempts")), +// new TypeReference<>() { +// }); +// Double startTime = +// jsonMapper.readValue(jsonMapper.treeAsTokens(executableMM.get("executionParameters").get("startTime")), new TypeReference<>() { +// }); +// Double endTime = jsonMapper.readValue(jsonMapper.treeAsTokens(executableMM.get("executionParameters").get("endTime")), new TypeReference<>() { +// }); +// Double stepSize = +// jsonMapper.readValue(jsonMapper.treeAsTokens(executableMM.get("executionParameters").get("stepSize")), new TypeReference<>() { +// }); +// +// MasterModel masterModel = ScenarioLoader.load(new ByteArrayInputStream(executableMM.get("masterModel").textValue().getBytes())); +// +// // Setup scenarioConfiguration +// Fmi2SimulationEnvironment simulationEnvironment = Fmi2SimulationEnvironment.of(simulationConfiguration, errorReporter); +// ScenarioConfiguration scenarioConfiguration = +// new ScenarioConfiguration(simulationEnvironment, masterModel, parameters, relTol, absTol, convergenceAttempts, startTime, endTime, +// stepSize, Pair.of(Framework.FMI2, simulationConfiguration), false, Map.of()); +// +// // ACT +// // This calls TemplateGeneratorFromScenario.generateTemplate which is the method to test +// mabl.generateSpec(scenarioConfiguration); +// +// mabl.expand(); +// mabl.typeCheck(); +// mabl.verify(Framework.FMI2); +// +// // ASSERT +// if (errorReporter.getErrorCount() > 0) { +// errorReporter.printErrors(new PrintWriter(System.err, true)); +// Assertions.fail(); +// } +// if (errorReporter.getWarningCount() > 0) { +// errorReporter.printWarnings(new PrintWriter(System.out, true)); +// } +// PrettyPrinter.print(mabl.getMainSimulationUnit()); +// mabl.dump(workingDirectory); +// Assertions.assertTrue(new File(workingDirectory, Mabl.MAIN_SPEC_DEFAULT_FILENAME).exists(), "Spec file must exist"); +// Assertions.assertTrue(new File(workingDirectory, Mabl.MAIN_SPEC_DEFAULT_RUNTIME_FILENAME).exists(), "Spec file must exist"); +// new MableInterpreter(new DefaultExternalValueFactory(workingDirectory, +// IOUtils.toInputStream(mabl.getRuntimeDataAsJsonString(), StandardCharsets.UTF_8))).execute(mabl.getMainSimulationUnit()); +// +// +// csvCompare(new File(directory, "expectedoutputs.csv"), new File(workingDirectory, "outputs.csv")); +// } +//} 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..fbaec0a00 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,7 @@ 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; @@ -20,11 +20,16 @@ import org.intocps.maestro.framework.fmi2.api.mabl.scoping.WhileMaBLScope; import org.intocps.maestro.framework.fmi2.api.mabl.values.*; import org.intocps.maestro.framework.fmi2.api.mabl.variables.*; +import org.intocps.verification.scenarioverifier.core.MasterModel; +import org.intocps.verification.scenarioverifier.core.ScenarioLoader; +import org.intocps.verification.scenarioverifier.core.ScenarioModel; +import org.intocps.verification.scenarioverifier.core.*; +import org.intocps.verification.scenarioverifier.synthesizer.LoopStrategy; +import org.intocps.verification.scenarioverifier.synthesizer.SynthesizerSimple; import org.slf4j.Logger; import org.slf4j.LoggerFactory; import scala.jdk.javaapi.CollectionConverters; -import synthesizer.LoopStrategy; -import synthesizer.SynthesizerSimple; + import javax.xml.xpath.XPathExpressionException; import java.io.ByteArrayInputStream; @@ -309,8 +314,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/MasterModelMapper.kt index 0e9b983ef..adccdfa93 100644 --- a/plugins/sigver/src/main/kotlin/MasterModelMapper.kt +++ b/plugins/sigver/src/main/kotlin/MasterModelMapper.kt @@ -1,11 +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 org.intocps.verification.scenarioverifier.core.* +import org.intocps.verification.scenarioverifier.api.* import scala.jdk.javaapi.CollectionConverters class MasterModelMapper { @@ -32,7 +33,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 +158,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