diff --git a/.gitignore b/.gitignore index 292ba7375..fba01e0fa 100644 --- a/.gitignore +++ b/.gitignore @@ -114,4 +114,12 @@ __pycache__/ *$py.class /external_tester/venv/ -*.ci-friendly-pom.xml \ No newline at end of file +*.ci-friendly-pom.xml +.metals/metals.mv.db +.bloop/ast-test.json +.bloop/ast.json +.bloop/bloop.settings.json +.bloop/core-test.json +.bloop/core.json +.bloop/root-test.json +.bloop/root.json diff --git a/external_tester/maestro_cli_test.py b/external_tester/maestro_cli_test.py index 285b38b87..a52cdf889 100644 --- a/external_tester/maestro_cli_test.py +++ b/external_tester/maestro_cli_test.py @@ -116,7 +116,7 @@ def cliGenerateAlgorithmFromMultiModel(): with open(multiModelPath, "w+") as jsonFile: json.dump(multiModel, jsonFile) - + cmd = "java -jar {0} sigver generate-algorithm {1} -output {2}".format(path, multiModelPath, temporary) func = lambda: print("Succesfully generated algorithm from multi model") if(os.path.exists(os.path.join(temporary, "algorithm.conf"))) else lambda: (Exception("Algorithm was not returned")) testutils.testCliCommandWithFunc(cmd, func) @@ -188,10 +188,10 @@ def cliExecuteAlgorithmFromMasterModel(): SCR_path = "scenario_controller_resources" print("Testing CLI of: " + path) -cliRaw() -cliSpecGen() -cliExpansion() -cliExportCpp(args.includeSlowTests) +# cliRaw() +# cliSpecGen() +# cliExpansion() +# cliExportCpp(args.includeSlowTests) cliGenerateAlgorithmFromScenario() cliGenerateAlgorithmFromMultiModel() cliExecuteAlgorithmFromExtendedMultiModel() diff --git a/external_tester/scenario_controller_resources/generate_from_multi_model/expectedMasterModel.txt b/external_tester/scenario_controller_resources/generate_from_multi_model/expectedMasterModel.txt index 7567b8ee3..69ad529ed 100644 --- a/external_tester/scenario_controller_resources/generate_from_multi_model/expectedMasterModel.txt +++ b/external_tester/scenario_controller_resources/generate_from_multi_model/expectedMasterModel.txt @@ -1 +1 @@ -name = generatedFromMultiModel\nscenario = {\nfmus = {\nFMU_roller = { \n can-reject-step = true,\n inputs = {\nvalve = {reactivity=delayed}},\n outputs = {\nlevel = {dependencies-init=[valve], dependencies=[valve]}}\n }\nController_cont = { \n can-reject-step = true,\n inputs = {\nlevel = {reactivity=delayed}},\n outputs = {\n}\n }}\nconnections = [\n"FMU_roller.level" -> "Controller_cont.level"]\n}\ninitialization = [\n\n{set: "FMU_roller.valve"}\n\n{get: "FMU_roller.level"}\n\n{set: "Controller_cont.level"}\n\n\n]\ncosim-step = {conf1 = [{save-state: Controller_cont}\n\n{save-state: FMU_roller}\n\n{loop: { \n until-step-accept: [Controller_cont,FMU_roller] \n iterate: [{step: Controller_cont }\n\n{step: FMU_roller }\n] \n if-retry-needed: [{restore-state: Controller_cont}\n\n{restore-state: FMU_roller}\n]} \n }\n\n{set: "FMU_roller.valve"}\n\n{get: "FMU_roller.level"}\n\n{set: "Controller_cont.level"}\n]\n} \ No newline at end of file +name = generatedFromMultiModel\nscenario = {\n \n fmus = {\n FMU_roller = \n {\n can-reject-step = true,\n inputs = {\n \n },\n outputs = {\n level = {dependencies-init=[], dependencies=[]}\n }\n }\nController_cont = \n {\n can-reject-step = true,\n inputs = {\n level = {reactivity=delayed}\n },\n outputs = {\n \n }\n }\n }\n connections = [ \"FMU_roller.level\" -> \"Controller_cont.level\"]\n\n}\ninitialization = [ {get: \"FMU_roller.level\"}\n {set: \"Controller_cont.level\"}]\ncosim-step = { conf1 =\n [ {save-state: Controller_cont}\n {save-state: FMU_roller}\n {\n loop: {\n until-step-accept: [Controller_cont,FMU_roller]\n iterate: [ {step: Controller_cont }\n {step: FMU_roller }]\n if-retry-needed: [ {restore-state: Controller_cont}, {restore-state: FMU_roller}]\n }\n }\n \n {get: \"FMU_roller.level\"}\n {set: \"Controller_cont.level\"}]\n }\n \ No newline at end of file diff --git a/external_tester/scenario_controller_resources/generate_from_multi_model/multimodel.json b/external_tester/scenario_controller_resources/generate_from_multi_model/multimodel.json index a3bc5a761..b0ce2a07a 100644 --- a/external_tester/scenario_controller_resources/generate_from_multi_model/multimodel.json +++ b/external_tester/scenario_controller_resources/generate_from_multi_model/multimodel.json @@ -12,7 +12,6 @@ "sigver": { "reactivity": { "{Controller}.cont.level": "Delayed" - }, - "verification": false + } } } \ No newline at end of file diff --git a/external_tester/scenario_controller_resources/generate_from_scenario/expectedResult.txt b/external_tester/scenario_controller_resources/generate_from_scenario/expectedResult.txt index 7b4c6fdd2..58be9bff1 100644 --- a/external_tester/scenario_controller_resources/generate_from_scenario/expectedResult.txt +++ b/external_tester/scenario_controller_resources/generate_from_scenario/expectedResult.txt @@ -1,114 +1,106 @@ name = Example master that has a loop within a loop scenario = { -fmus = { -msd3 = { - can-reject-step = true, - inputs = { -z = {reactivity=delayed}}, - outputs = { -G = {dependencies-init=[z], dependencies=[z]}} - } -msd2 = { - can-reject-step = true, - inputs = { -v1 = {reactivity=reactive} -x1 = {reactivity=delayed} -G = {reactivity=reactive}}, - outputs = { -fk = {dependencies-init=[x1,v1], dependencies=[x1,v1]} -z = {dependencies-init=[], dependencies=[]}} - } -msd1 = { - can-reject-step = true, - inputs = { -fk = {reactivity=reactive}}, - outputs = { -x1 = {dependencies-init=[], dependencies=[]} -v1 = {dependencies-init=[], dependencies=[]}} - }} -connections = [ -"msd1.x1" -> "msd2.x1" -"msd1.v1" -> "msd2.v1" -"msd2.fk" -> "msd1.fk" -"msd2.z" -> "msd3.z" -"msd3.G" -> "msd2.G"] + fmus = { + msd3 = + { + can-reject-step = true, + inputs = { + z = {reactivity=delayed} + }, + outputs = { + G = {dependencies-init=[z], dependencies=[z]} + } + } + msd2 = + { + can-reject-step = true, + inputs = { + v1 = {reactivity=reactive} + x1 = {reactivity=delayed} + G = {reactivity=reactive} + }, + outputs = { + fk = {dependencies-init=[x1,v1], dependencies=[x1,v1]} + z = {dependencies-init=[], dependencies=[]} + } + } + msd1 = + { + can-reject-step = true, + inputs = { + fk = {reactivity=reactive} + }, + outputs = { + x1 = {dependencies-init=[], dependencies=[]} + v1 = {dependencies-init=[], dependencies=[]} + } + } + } + connections = [ + "msd1.x1" -> "msd2.x1", + "msd1.v1" -> "msd2.v1", + "msd2.fk" -> "msd1.fk", + "msd2.z" -> "msd3.z", + "msd3.G" -> "msd2.G" + ] } -initialization = [ - - -{get: "msd1.x1"} - -{set: "msd2.x1"} - -{get: "msd2.z"} - -{set: "msd3.z"} - -{get: "msd1.v1"} - -{set: "msd2.v1"} - -{get: "msd2.fk"} - -{set: "msd1.fk"} - -{get: "msd3.G"} - -{set: "msd2.G"} - - - -] -cosim-step = {conf1 = [{save-state: msd2} - -{save-state: msd1} - -{save-state: msd3} - -{loop: { - until-step-accept: [msd2,msd1,msd3] - iterate: [{loop: { - until-converged: ["msd3.G","msd2.fk","msd2.z","msd1.x1","msd1.v1"] - iterate: [{set: "msd2.G"} - -{step: msd3 } - -{set: "msd3.z"} - -{get-tentative: "msd3.G"} - -{set: "msd1.fk"} - -{step: msd1 } - -{get-tentative: "msd1.v1"} - -{get-tentative: "msd1.x1"} - -{set: "msd2.v1"} - -{step: msd2 } - -{set: "msd2.x1"} - -{get-tentative: "msd2.fk"} - -{get-tentative: "msd2.z"} -] - if-retry-needed: [{restore-state: msd3} - -{restore-state: msd2} - -{restore-state: msd1} -]} - } -] - if-retry-needed: [{restore-state: msd2} - -{restore-state: msd1} - -{restore-state: msd3} -]} - } -] +initialization = [ + {get: "msd2.z"} + {set: "msd3.z"} + {get: "msd3.G"} + {set: "msd2.G"} + {get: "msd1.v1"} + {set: "msd2.v1"} + {get: "msd1.x1"} + {set: "msd2.x1"} + {get: "msd2.fk"} + {set: "msd1.fk"} + ] +cosim-step = +{ + conf1 = + [ + {save-state: msd2} + {save-state: msd1} + {save-state: msd3} + { + loop: { + until-step-accept: [msd2,msd1,msd3] + iterate: [ + { + loop: { + until-converged: ["msd3.G","msd2.fk","msd2.z","msd1.x1","msd1.v1"] + iterate: [ + {step: msd3 } + {set: "msd2.G"} + {set: "msd1.fk"} + {step: msd1 } + {get-tentative: "msd1.v1"} + {set: "msd2.v1"} + {step: msd2 } + {get-tentative: "msd1.x1"} + {set-tentative: "msd2.x1"} + {get-tentative: "msd2.fk"} + {get-tentative: "msd2.z"} + {set-tentative: "msd3.z"} + {get-tentative: "msd3.G"} + ] + if-retry-needed: + [ + {restore-state: msd3}, + {restore-state: msd2}, + {restore-state: msd1} + ] + } + } + ] + if-retry-needed: + [ + {restore-state: msd2}, + {restore-state: msd1}, + {restore-state: msd3} + ] + } + } + ] } \ No newline at end of file diff --git a/external_tester/testutils.py b/external_tester/testutils.py index e5e700d0b..4bd85c4c2 100644 --- a/external_tester/testutils.py +++ b/external_tester/testutils.py @@ -12,6 +12,7 @@ import subprocess from threading import Thread import time +import string TempDirectoryData = namedtuple('TempDirectoryData', 'dirPath initializationPath resultPath mablSpecPath') @@ -69,6 +70,19 @@ def compareCSV(expected, actual): else: print(f"ERROR: {expected} doest not exist!") return False + +def comparText(file1, file2): + expectedFile = open(file1, 'r') + actualFile = open(file2, 'r') + remove = str.maketrans('', '', string.whitespace) + expectedLines = expectedFile.readlines() + actualLines = actualFile.readlines() + expectedLines = "".join(expectedLines).translate(remove) + actualLines = "".join(actualLines).translate(remove) + expectedFile.close() + actualFile.close() + + return expectedLines == actualLines def compare(strPrefix, expected, actual): if os.path.exists(expected): @@ -76,8 +90,13 @@ def compare(strPrefix, expected, actual): compareResult = filecmp.cmp(expected, actual) if not compareResult: - print("ERROR: {}: Files {} and {} do not match".format(strPrefix, expected, actual)) - return False + compareRes = comparText(expected, actual) + if not compareRes: + print("ERROR: {}: Files {} and {} do not match".format(strPrefix, expected, actual)) + return False + else: + print("%s: Files match" % strPrefix) + return True else: print("%s: Files match" % strPrefix) return True diff --git a/external_tester/webapi_test.py b/external_tester/webapi_test.py index 8828ac196..33b473c04 100644 --- a/external_tester/webapi_test.py +++ b/external_tester/webapi_test.py @@ -174,6 +174,8 @@ def testScenarioController(basicUrl): f.write(response.text) if(not testutils.compare("Generate from scenario", expectedResult, actualResult)): + print("ERROR: actual and expected algorithm do not match") + print("Actual:" + response.text) raise Exception("Expected algorithm does not match the actual algorithm.") #Test generate algorithm from multi model diff --git a/frameworks/fmi2/pom.xml b/frameworks/fmi2/pom.xml index 0de05d5e3..5a9447e9b 100644 --- a/frameworks/fmi2/pom.xml +++ b/frameworks/fmi2/pom.xml @@ -21,7 +21,7 @@ org.into-cps.vdmcheck.fmi2 vdmcheck2 - 1.1.1 + 1.1.3-SNAPSHOT junit diff --git a/maestro-webapi/pom.xml b/maestro-webapi/pom.xml index a80939f69..7806c9978 100644 --- a/maestro-webapi/pom.xml +++ b/maestro-webapi/pom.xml @@ -23,8 +23,8 @@ 3.11 - INTO-CPS-Association - scenario_verifier_2.13 + org.into-cps.verification + scenario_verifier org.junit.jupiter 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..1675866c4 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,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; 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..1196d42b0 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,18 +1,17 @@ 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.maestro2.dto.SigverSimulateRequestBody; +import org.intocps.maestro.webapi.maestro2.dto.VerificationResult; import org.intocps.maestro.webapi.util.ZipDirectory; import org.springframework.core.io.FileSystemResource; import org.springframework.http.HttpStatus; @@ -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,7 +43,7 @@ public ResponseEntity 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, @@ -53,47 +51,47 @@ public String generateAlgorithmFromScenario(@RequestBody String scenario) { 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. MasterModel masterModel = ScenarioLoader.load(new ByteArrayInputStream(masterModelAsString.getBytes())); ModelEncoding encoding = new ModelEncoding(masterModel); - String encodedModel = ScenarioGenerator.generate(encoding); + String encodedModel = ScenarioGenerator.generateUppaalEncoding(encoding); File tempFile = Files.createTempFile(null, ".xml").toFile(); 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")); diff --git a/maestro-webapi/src/main/java/org/intocps/maestro/webapi/maestro2/dto/VerificationResult.java b/maestro-webapi/src/main/java/org/intocps/maestro/webapi/maestro2/dto/VerificationResult.java new file mode 100644 index 000000000..08914c4ca --- /dev/null +++ b/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; + } +} diff --git a/maestro/pom.xml b/maestro/pom.xml index 4420b4ad4..4d79190db 100644 --- a/maestro/pom.xml +++ b/maestro/pom.xml @@ -27,8 +27,9 @@ - INTO-CPS-Association - scenario_verifier_2.13 + org.into-cps.verification + scenario_verifier + org.junit.jupiter 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..a6944f019 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; @@ -160,19 +159,23 @@ class GenerateAlgorithmCmd implements Callable { @Override public Integer call() throws Exception { + System.out.println("Generating algorithm from scenario or multi-model"); Path filePath = file.toPath(); MasterModel masterModel; if (FilenameUtils.getExtension(filePath.toString()).equals("conf")) { + System.out.println("Generating algorithm from scenario"); String scenario = Files.readString(filePath); masterModel = MasterModelMapper.Companion.scenarioToMasterModel(scenario); } else if (FilenameUtils.getExtension(filePath.toString()).equals("json")) { + System.out.println("Generating algorithm from multi-model"); ExtendedMultiModel multiModel = (new ObjectMapper()).readValue(file, ExtendedMultiModel.class); masterModel = MasterModelMapper.Companion.multiModelToMasterModel(multiModel, 3); } else { + System.out.println("Unable to generate algorithm from file: " + filePath.toString() + " - file extension must be .conf or .json"); 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 +242,6 @@ public Integer call() throws Exception { } } - String masterModelAsString; Path algorithmPath; if (algorithmFile == null) { @@ -249,7 +251,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/maestro/src/test/java/org/intocps/maestro/TemplateGeneratorFromScenarioTest.java b/maestro/src/test/java/org/intocps/maestro/TemplateGeneratorFromScenarioTest.java index 73275f693..4e67b987f 100644 --- a/maestro/src/test/java/org/intocps/maestro/TemplateGeneratorFromScenarioTest.java +++ b/maestro/src/test/java/org/intocps/maestro/TemplateGeneratorFromScenarioTest.java @@ -3,8 +3,8 @@ 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.intocps.verification.scenarioverifier.core.MasterModel; +import org.intocps.verification.scenarioverifier.core.ScenarioLoader; import org.apache.commons.io.IOUtils; import org.apache.commons.lang3.tuple.Pair; import org.intocps.maestro.ast.display.PrettyPrinter; @@ -34,95 +34,92 @@ 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")); - } -} +// 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")); +// } +// } \ No newline at end of file diff --git a/maestro/src/test/resources/jacobian_step_builder/legacy_discard/config.json b/maestro/src/test/resources/jacobian_step_builder/legacy_discard/config.json index aac78e83c..f0b287a8e 100644 --- a/maestro/src/test/resources/jacobian_step_builder/legacy_discard/config.json +++ b/maestro/src/test/resources/jacobian_step_builder/legacy_discard/config.json @@ -1,7 +1,6 @@ { "parameters": { }, - "verifyAgainstProlog": false, "stabilisation": false, "fixedPointIteration": 5, "absoluteTolerance": 0.0, diff --git a/maestro/src/test/resources/jacobian_step_builder/legacy_fixed_step/config.json b/maestro/src/test/resources/jacobian_step_builder/legacy_fixed_step/config.json index f23b7b538..7d492be5d 100644 --- a/maestro/src/test/resources/jacobian_step_builder/legacy_fixed_step/config.json +++ b/maestro/src/test/resources/jacobian_step_builder/legacy_fixed_step/config.json @@ -3,7 +3,6 @@ "{ctrl}.ctrlInstance.maxLevel":2, "{ctrl}.ctrlInstance.minLevel":1 }, - "verifyAgainstProlog": false, "stabilisation": false, "fixedPointIteration": 5, "absoluteTolerance": 0.3, diff --git a/maestro/src/test/resources/jacobian_step_builder/legacy_invalid_varstep/config.json b/maestro/src/test/resources/jacobian_step_builder/legacy_invalid_varstep/config.json index c56d13ae5..eadda169f 100644 --- a/maestro/src/test/resources/jacobian_step_builder/legacy_invalid_varstep/config.json +++ b/maestro/src/test/resources/jacobian_step_builder/legacy_invalid_varstep/config.json @@ -5,7 +5,6 @@ "{pump}.pump.tLength":0.05, "{pump}.pump.h":0.5 }, - "verifyAgainstProlog": false, "stabilisation": false, "fixedPointIteration": 5, "absoluteTolerance": 0.0, diff --git a/maestro/src/test/resources/jacobian_step_builder/legacy_rollback/config.json b/maestro/src/test/resources/jacobian_step_builder/legacy_rollback/config.json index c56d13ae5..eadda169f 100644 --- a/maestro/src/test/resources/jacobian_step_builder/legacy_rollback/config.json +++ b/maestro/src/test/resources/jacobian_step_builder/legacy_rollback/config.json @@ -5,7 +5,6 @@ "{pump}.pump.tLength":0.05, "{pump}.pump.h":0.5 }, - "verifyAgainstProlog": false, "stabilisation": false, "fixedPointIteration": 5, "absoluteTolerance": 0.0, diff --git a/maestro/src/test/resources/jacobian_step_builder/legacy_unstable/config.json b/maestro/src/test/resources/jacobian_step_builder/legacy_unstable/config.json index 99b505840..ed107e072 100644 --- a/maestro/src/test/resources/jacobian_step_builder/legacy_unstable/config.json +++ b/maestro/src/test/resources/jacobian_step_builder/legacy_unstable/config.json @@ -13,7 +13,6 @@ "{m1}.mi1.d1": 1, "{m1}.mi1.c1": 1 }, - "verifyAgainstProlog": false, "stabilisation": false, "fixedPointIteration": 5, "absoluteTolerance": 0.0, diff --git a/maestro/src/test/resources/jacobian_step_builder/slow_down_to_real_time/config.json b/maestro/src/test/resources/jacobian_step_builder/slow_down_to_real_time/config.json index d6e820c61..5f77051d5 100644 --- a/maestro/src/test/resources/jacobian_step_builder/slow_down_to_real_time/config.json +++ b/maestro/src/test/resources/jacobian_step_builder/slow_down_to_real_time/config.json @@ -3,7 +3,6 @@ "{ctrl}.ctrlInstance.maxlevel": 2, "{ctrl}.ctrlInstance.minlevel": 1 }, - "verifyAgainstProlog": false, "stabilisation": false, "fixedPointIteration": 5, "absoluteTolerance": 0.1, diff --git a/maestro/src/test/resources/jacobian_step_builder/stabilization/config.json b/maestro/src/test/resources/jacobian_step_builder/stabilization/config.json index 99b505840..ed107e072 100644 --- a/maestro/src/test/resources/jacobian_step_builder/stabilization/config.json +++ b/maestro/src/test/resources/jacobian_step_builder/stabilization/config.json @@ -13,7 +13,6 @@ "{m1}.mi1.d1": 1, "{m1}.mi1.c1": 1 }, - "verifyAgainstProlog": false, "stabilisation": false, "fixedPointIteration": 5, "absoluteTolerance": 0.0, diff --git a/maestro/src/test/resources/jacobian_step_builder/variable_step_WT/config.json b/maestro/src/test/resources/jacobian_step_builder/variable_step_WT/config.json index d6e820c61..5f77051d5 100644 --- a/maestro/src/test/resources/jacobian_step_builder/variable_step_WT/config.json +++ b/maestro/src/test/resources/jacobian_step_builder/variable_step_WT/config.json @@ -3,7 +3,6 @@ "{ctrl}.ctrlInstance.maxlevel": 2, "{ctrl}.ctrlInstance.minlevel": 1 }, - "verifyAgainstProlog": false, "stabilisation": false, "fixedPointIteration": 5, "absoluteTolerance": 0.1, diff --git a/maestro/src/test/resources/specifications/full/initialize_fixedstep_singleWaterTank/config.json b/maestro/src/test/resources/specifications/full/initialize_fixedstep_singleWaterTank/config.json index 3561abfd1..8efcd28f3 100644 --- a/maestro/src/test/resources/specifications/full/initialize_fixedstep_singleWaterTank/config.json +++ b/maestro/src/test/resources/specifications/full/initialize_fixedstep_singleWaterTank/config.json @@ -3,7 +3,6 @@ "{crtl}.crtlInstance.maxlevel": 2, "{crtl}.crtlInstance.minlevel": 1 }, - "verifyAgainstProlog": false, "stabilisation": false, "fixedPointIteration": 5, "absoluteTolerance": 0.1, diff --git a/maestro/src/test/resources/specifications/full/initialize_fixedstep_unfold_loop/config.json b/maestro/src/test/resources/specifications/full/initialize_fixedstep_unfold_loop/config.json index 66417e830..6d445da16 100644 --- a/maestro/src/test/resources/specifications/full/initialize_fixedstep_unfold_loop/config.json +++ b/maestro/src/test/resources/specifications/full/initialize_fixedstep_unfold_loop/config.json @@ -13,7 +13,6 @@ "{m1}.i1.d1": 1, "{m1}.i1.c1": 1 }, - "verifyAgainstProlog": true, "stabilisation": true, "fixedPointIteration": 5, "absoluteTolerance": 0.1, diff --git a/maestro/src/test/resources/specifications/full/initialize_fixedstep_unfold_noloop/config.json b/maestro/src/test/resources/specifications/full/initialize_fixedstep_unfold_noloop/config.json index 700762437..3ef738a19 100644 --- a/maestro/src/test/resources/specifications/full/initialize_fixedstep_unfold_noloop/config.json +++ b/maestro/src/test/resources/specifications/full/initialize_fixedstep_unfold_noloop/config.json @@ -13,7 +13,6 @@ "{m1}.i1.d1": 1, "{m1}.i1.c1": 1 }, - "verifyAgainstProlog": true, "stabilisation": true, "fixedPointIteration": 5, "absoluteTolerance": 0.1, diff --git a/maestro/src/test/resources/specifications/full/initialize_jacobianstepbuilder_unfold_loop/config.json b/maestro/src/test/resources/specifications/full/initialize_jacobianstepbuilder_unfold_loop/config.json index d6e820c61..5f77051d5 100644 --- a/maestro/src/test/resources/specifications/full/initialize_jacobianstepbuilder_unfold_loop/config.json +++ b/maestro/src/test/resources/specifications/full/initialize_jacobianstepbuilder_unfold_loop/config.json @@ -3,7 +3,6 @@ "{ctrl}.ctrlInstance.maxlevel": 2, "{ctrl}.ctrlInstance.minlevel": 1 }, - "verifyAgainstProlog": false, "stabilisation": false, "fixedPointIteration": 5, "absoluteTolerance": 0.1, diff --git a/maestro/src/test/resources/specifications/full/initialize_singleWaterTank/config.json b/maestro/src/test/resources/specifications/full/initialize_singleWaterTank/config.json index bbbc12157..2e921ea82 100644 --- a/maestro/src/test/resources/specifications/full/initialize_singleWaterTank/config.json +++ b/maestro/src/test/resources/specifications/full/initialize_singleWaterTank/config.json @@ -3,7 +3,6 @@ "{x1}.crtlInstance.maxlevel": 2, "{crtl}.crtlInstance.minlevel": 1 }, - "verifyAgainstProlog": true, "stabilisation": true, "fixedPointIteration": 5, "absoluteTolerance": 0.1, diff --git a/maestro/src/test/resources/specifications/full/initialize_threetanks/config.json b/maestro/src/test/resources/specifications/full/initialize_threetanks/config.json index 2d1e5d251..6ced088a9 100644 --- a/maestro/src/test/resources/specifications/full/initialize_threetanks/config.json +++ b/maestro/src/test/resources/specifications/full/initialize_threetanks/config.json @@ -3,7 +3,6 @@ "{controller}.controller.wt3_max": 1.7, "{controller}.controller.wt3_min": 1.3 }, - "verifyAgainstProlog": true, "stabilisation": true, "fixedPointIteration": 5, "absoluteTolerance": 0.1, diff --git a/maestro/src/test/resources/specifications/online/.stabilityMassSpringDamper/config.json b/maestro/src/test/resources/specifications/online/.stabilityMassSpringDamper/config.json index 6fcc5b01a..c62b63a3b 100644 --- a/maestro/src/test/resources/specifications/online/.stabilityMassSpringDamper/config.json +++ b/maestro/src/test/resources/specifications/online/.stabilityMassSpringDamper/config.json @@ -18,8 +18,7 @@ "{m1}.i1.m1": 1, "{m1}.i1.d1": 1, "{m1}.i1.c1": 1 - }, - "verifyAgainstProlog": true + } } } ] \ No newline at end of file diff --git a/maestro/src/test/resources/specifications/online/build_varstep_ZC_single/config.json b/maestro/src/test/resources/specifications/online/build_varstep_ZC_single/config.json index 65fc2e612..5c91bb48c 100644 --- a/maestro/src/test/resources/specifications/online/build_varstep_ZC_single/config.json +++ b/maestro/src/test/resources/specifications/online/build_varstep_ZC_single/config.json @@ -10,8 +10,7 @@ "{pump}.pump.tBegin": 4, "{pump}.pump.tLength": 2, "{pump}.pump.h": -5 - }, - "verifyAgainstProlog": false + } } } ] \ No newline at end of file diff --git a/maestro/src/test/resources/specifications/online/initialize_fixedstep_unfold/config.json b/maestro/src/test/resources/specifications/online/initialize_fixedstep_unfold/config.json index 05e9945c4..519c5b4ad 100644 --- a/maestro/src/test/resources/specifications/online/initialize_fixedstep_unfold/config.json +++ b/maestro/src/test/resources/specifications/online/initialize_fixedstep_unfold/config.json @@ -9,7 +9,6 @@ "{crtl}.crtlInstance.maxlevel": 2, "{crtl}.crtlInstance.minlevel": 1 }, - "verifyAgainstProlog": true, "stabilisation" : false, "fixedPointIteration" : 5, "absoluteTolerance" : 0.1, diff --git a/maestro/src/test/resources/specifications/online/rollback/config.json b/maestro/src/test/resources/specifications/online/rollback/config.json index 88f87a232..40330bda2 100644 --- a/maestro/src/test/resources/specifications/online/rollback/config.json +++ b/maestro/src/test/resources/specifications/online/rollback/config.json @@ -9,7 +9,6 @@ "{crtl}.crtlInstance.maxlevel": 2, "{crtl}.crtlInstance.minlevel": 1 }, - "verifyAgainstProlog": true, "stabilisation": false, "fixedPointIteration": 5, "absoluteTolerance": 0.1, diff --git a/plugins/initializer/src/main/kotlin/Initializer.kt b/plugins/initializer/src/main/kotlin/Initializer.kt index 06ed4f8c9..1c073df77 100644 --- a/plugins/initializer/src/main/kotlin/Initializer.kt +++ b/plugins/initializer/src/main/kotlin/Initializer.kt @@ -28,7 +28,6 @@ import org.intocps.maestro.framework.fmi2.api.mabl.variables.* import org.intocps.maestro.plugin.* import org.intocps.maestro.plugin.IMaestroExpansionPlugin.EmptyRuntimeConfig import org.intocps.maestro.plugin.initializer.instructions.* -import org.intocps.maestro.plugin.verificationsuite.prologverifier.InitializationPrologQuery import org.slf4j.Logger import org.slf4j.LoggerFactory import java.io.IOException @@ -94,7 +93,6 @@ class Initializer : BasicMaestroExpansionPlugin { private val portsAlreadySet = HashMap>() private val topologicalPlugin: TopologicalPlugin - private val initializationPrologQuery: InitializationPrologQuery var config: InitializationConfig? = null var modelParameters: List? = null var envParameters: List? = null @@ -106,13 +104,11 @@ class Initializer : BasicMaestroExpansionPlugin { var maxConvergeAttempts: Fmi2Builder.IntVariable? = null constructor() { - initializationPrologQuery = InitializationPrologQuery() topologicalPlugin = TopologicalPlugin() } - constructor(topologicalPlugin: TopologicalPlugin, initializationPrologQuery: InitializationPrologQuery) { + constructor(topologicalPlugin: TopologicalPlugin) { this.topologicalPlugin = topologicalPlugin - this.initializationPrologQuery = initializationPrologQuery } override fun getName(): String { @@ -264,11 +260,6 @@ class Initializer : BasicMaestroExpansionPlugin { //Find the right order to instantiate dependentPorts and make sure where doesn't exist any cycles in the connections val instantiationOrder = topologicalPlugin.findInstantiationOrderStrongComponents(connections, filterTargets) - //Verification against prolog should only be done if it turned on and there is no loops - if (this.config!!.verifyAgainstProlog && instantiationOrder.all { i -> i.size == 1 }) - initializationPrologQuery.initializationOrderIsValid(instantiationOrder.flatten(), connections) - - //Set variables for all components in IniPhase setComponentsVariables(fmuInstances, PhasePredicates.iniPhase(), builder) @@ -394,10 +385,6 @@ class Initializer : BasicMaestroExpansionPlugin { // //Find the right order to instantiate dependentPorts and make sure where doesn't exist any cycles in the connections // val instantiationOrder = topologicalPlugin.findInstantiationOrderStrongComponents(connections) // -// //Verification against prolog should only be done if it turned on and there is no loops -// if (this.config!!.verifyAgainstProlog && instantiationOrder.all { i -> i.size == 1 }) -// initializationPrologQuery.initializationOrderIsValid(instantiationOrder.flatten(), connections) -// // // //Set variables for all components in IniPhase // setComponentsVariables(fmuInstances, PhasePredicates.iniPhase(), builder) @@ -676,7 +663,6 @@ class Initializer : BasicMaestroExpansionPlugin { } val parameters = root["parameters"] val envParameters = root["environmentParameters"] - val verify = root["verifyAgainstProlog"] val stabilisation = root["stabilisation"] val fixedPointIteration = root["fixedPointIteration"] val absoluteTolerance = root["absoluteTolerance"] @@ -686,7 +672,6 @@ class Initializer : BasicMaestroExpansionPlugin { conf = InitializationConfig( if (parameters is NullNode) null else parameters, if (envParameters is NullNode) null else envParameters, - verify, stabilisation, fixedPointIteration, absoluteTolerance, @@ -720,7 +705,6 @@ class Initializer : BasicMaestroExpansionPlugin { class InitializationConfig( parameters: JsonNode?, envParameters: JsonNode?, - verify: JsonNode?, stabilisation: JsonNode?, fixedPointIteration: JsonNode?, absoluteTolerance: JsonNode?, @@ -729,12 +713,10 @@ class Initializer : BasicMaestroExpansionPlugin { var stabilisation = false val modelParameters: List? val envParameters: List? - var verifyAgainstProlog = false var maxIterations = 0 var absoluteTolerance = 0.0 var relativeTolerance = 0.0 - init { val mapper = ObjectMapper() val convertParameters: Map? = @@ -756,7 +738,6 @@ class Initializer : BasicMaestroExpansionPlugin { List::class.java ) as List - verifyAgainstProlog = verify?.asBoolean(false) ?: false this.stabilisation = stabilisation?.asBoolean(false) ?: false maxIterations = fixedPointIteration?.asInt(5) ?: 5 if (absoluteTolerance == null) { diff --git a/plugins/initializer/src/test/java/InitializerTest.java b/plugins/initializer/src/test/java/InitializerTest.java index b157a7676..a54beb4e3 100644 --- a/plugins/initializer/src/test/java/InitializerTest.java +++ b/plugins/initializer/src/test/java/InitializerTest.java @@ -9,8 +9,6 @@ import org.intocps.maestro.plugin.IPluginConfiguration; import org.intocps.maestro.plugin.initializer.Initializer; import org.intocps.maestro.plugin.initializer.TopologicalPlugin; -import org.intocps.maestro.plugin.verificationsuite.prologverifier.InitializationPrologQuery; -import org.intocps.maestro.plugin.verificationsuite.prologverifier.PrologGenerator; import org.junit.jupiter.api.Assertions; import org.junit.jupiter.api.Test; import scala.Console; @@ -33,9 +31,7 @@ public class InitializerTest { public void parseConfig() throws IOException { InputStream pluginConfiguration = minimalConfiguration; var topologicalPlugin = new TopologicalPlugin(); - var prologGenerator = new PrologGenerator(); - var initializationPrologQuery = new InitializationPrologQuery(prologGenerator); - IMaestroExpansionPlugin plugin = new Initializer(topologicalPlugin, initializationPrologQuery); + IMaestroExpansionPlugin plugin = new Initializer(topologicalPlugin); plugin.parseConfig(minimalConfiguration); } @@ -43,9 +39,7 @@ public void parseConfig() throws IOException { public void unfoldCallsSpecGen() throws Exception { InputStream pluginConfiguration = minimalConfiguration; var topologicalPlugin = new TopologicalPlugin(); - var prologGenerator = new PrologGenerator(); - var initializationPrologQuery = new InitializationPrologQuery(prologGenerator); - IMaestroExpansionPlugin plugin = new Initializer(topologicalPlugin, initializationPrologQuery); + IMaestroExpansionPlugin plugin = new Initializer(topologicalPlugin); AFunctionDeclaration funcDecl = plugin.getDeclaredImportUnit().getModule().getFunctions().iterator().next(); IPluginConfiguration parsedPluginConfiguration = plugin.parseConfig(pluginConfiguration); diff --git a/plugins/initializer/src/test/resources/InitializePluginTest/config.json b/plugins/initializer/src/test/resources/InitializePluginTest/config.json index 4ff409178..befe202dc 100644 --- a/plugins/initializer/src/test/resources/InitializePluginTest/config.json +++ b/plugins/initializer/src/test/resources/InitializePluginTest/config.json @@ -3,8 +3,7 @@ "parameters": { "{crtl}.crtlInstance.maxlevel": 2, "{crtl}.crtlInstance.minlevel": 1 - }, - "verifyAgainstProlog": true + } } } diff --git a/plugins/sigver/pom.xml b/plugins/sigver/pom.xml index b57144b12..2c0ed8760 100644 --- a/plugins/sigver/pom.xml +++ b/plugins/sigver/pom.xml @@ -34,8 +34,9 @@ compile - INTO-CPS-Association - scenario_verifier_2.13 + org.into-cps.verification + scenario_verifier + 0.2.21-SNAPSHOT org.jetbrains.kotlin @@ -118,4 +119,4 @@ - \ No newline at end of file + 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..eebd944da 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; @@ -106,7 +106,6 @@ public RuntimeConfigAddition expandWithRuntimeAddition(AFunctionDeclarati // GENERATE MaBL try { - MasterModel masterModel = ScenarioLoader.load(new ByteArrayInputStream(configuration.masterModel.getBytes())); ScenarioModel scenarioModel = masterModel.scenario(); adaptiveModel = scenarioModel.config(); @@ -309,8 +308,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 diff --git a/plugins/verificationsuite/lib/jiprolog-4.1.6.1.jar b/plugins/verificationsuite/lib/jiprolog-4.1.6.1.jar new file mode 100644 index 000000000..f9430bf10 Binary files /dev/null and b/plugins/verificationsuite/lib/jiprolog-4.1.6.1.jar differ diff --git a/plugins/verificationsuite/pom.xml b/plugins/verificationsuite/pom.xml index 4f8bf9a38..bdb74eaf2 100644 --- a/plugins/verificationsuite/pom.xml +++ b/plugins/verificationsuite/pom.xml @@ -20,11 +20,6 @@ ${project.version} compile - - com.ugos - JIProlog - 4.1.6.1 - guru.nidi graphviz-java @@ -41,4 +36,6 @@ junit-jupiter + + diff --git a/plugins/verificationsuite/src/main/java/org/intocps/maestro/plugin/verificationsuite/prologverifier/InitializationPrologQuery.java b/plugins/verificationsuite/src/main/java/org/intocps/maestro/plugin/verificationsuite/prologverifier/InitializationPrologQuery.java deleted file mode 100644 index 6618742c4..000000000 --- a/plugins/verificationsuite/src/main/java/org/intocps/maestro/plugin/verificationsuite/prologverifier/InitializationPrologQuery.java +++ /dev/null @@ -1,77 +0,0 @@ -package org.intocps.maestro.plugin.verificationsuite.prologverifier; - -import com.ugos.jiprolog.engine.*; -import org.intocps.maestro.framework.fmi2.Fmi2SimulationEnvironment; -import org.slf4j.Logger; -import org.slf4j.LoggerFactory; - -import java.nio.file.Path; -import java.nio.file.Paths; -import java.util.List; -import java.util.Set; -import java.util.stream.Collectors; - -public class InitializationPrologQuery { - final static Logger logger = LoggerFactory.getLogger(InitializationPrologQuery.class); - private final PrologGenerator prologGenerator; - - public InitializationPrologQuery(PrologGenerator prologGenerator) { - this.prologGenerator = prologGenerator; - } - - public InitializationPrologQuery() { - this.prologGenerator = new PrologGenerator(); - } - - public boolean initializationOrderIsValid(List instantiationOrder, - Set relations) { - // New instance of prolog engine - JIPEngine jip = new JIPEngine(); - JIPTerm queryTerm = null; - Boolean isCorrectInitializationOrder = false; - // files are searched in the search path - Path path = getPathToProlog(); - // parse query - try { - // consult file - jip.consultFile(path + "/initialization.pl"); - - var init = prologGenerator.createInitOperationOrder(instantiationOrder); - var connections = prologGenerator.createConnections( - relations.stream().filter(o -> o.getOrigin() == Fmi2SimulationEnvironment.Relation.InternalOrExternal.External) - .collect(Collectors.toList())); - var fmus = prologGenerator.createFMUs(relations); - - queryTerm = jip.getTermParser().parseTerm(String.format("?- isInitSchedule(%s,%s, %s).", init, fmus, connections)); - - //queryTerm = jip.getTermParser().parseTerm("?- father(X, Y)."); - } catch (JIPSyntaxErrorException ex) { - ex.printStackTrace(); - } - - // open Query - JIPQuery jipQuery = jip.openSynchronousQuery(queryTerm); - - try { - //If the solution is false the result will be null - isCorrectInitializationOrder = (jipQuery.nextSolution() != null); - } catch (JIPRuntimeException ex) { - logger.error("No solution", ex); - } - - jip.reset(); - - return isCorrectInitializationOrder; - } - - private Path getPathToProlog() { - var currentPath = Paths.get("").toAbsolutePath().getParent().normalize().toString(); - var pluginString = "plugins"; - if (currentPath.contains("plugins")) { - pluginString = ""; - } - return Paths.get(currentPath, pluginString, "verificationsuite", "src", "main", "resources", "prologCode"); - } - -} - diff --git a/plugins/verificationsuite/src/main/java/org/intocps/maestro/plugin/verificationsuite/prologverifier/PrologGenerator.java b/plugins/verificationsuite/src/main/java/org/intocps/maestro/plugin/verificationsuite/prologverifier/PrologGenerator.java deleted file mode 100644 index f59a2f6df..000000000 --- a/plugins/verificationsuite/src/main/java/org/intocps/maestro/plugin/verificationsuite/prologverifier/PrologGenerator.java +++ /dev/null @@ -1,111 +0,0 @@ -package org.intocps.maestro.plugin.verificationsuite.prologverifier; - -import org.intocps.maestro.ast.LexIdentifier; -import org.intocps.maestro.fmi.Fmi2ModelDescription; -import org.intocps.maestro.framework.fmi2.Fmi2SimulationEnvironment; -import org.intocps.maestro.plugin.ExpandException; - -import java.util.Collection; -import java.util.List; -import java.util.Set; -import java.util.stream.Collectors; - -public class PrologGenerator { - public String createInitOperationOrder(List instantiationOrder) { - StringBuilder initOrder = new StringBuilder(); - instantiationOrder.forEach(o -> { - try { - initOrder.append(String.format("%s(%s, %s),", getMethod(o), o.scalarVariable.getInstance().getText().toLowerCase(), - o.scalarVariable.getScalarVariable().getName().toLowerCase())); - } catch (ExpandException e) { - e.printStackTrace(); - } - }); - - return fixListFormat(initOrder).toString(); - } - - public String createFMUs(Set relations) { - StringBuilder fmuString = new StringBuilder(); - var fmuList = relations.stream().map(o -> o.getSource().scalarVariable.getInstance()).collect(Collectors.toSet()); - fmuList.forEach(fmu -> { - fmuString.append(String.format("fmu(%s, %s, %s),", fmu.getText().toLowerCase(), getInPorts(relations, fmu), getOutPorts(relations, fmu))); - }); - - return fixListFormat(fmuString).toString(); - } - - public String createConnections(List relations) { - StringBuilder connections = new StringBuilder(); - relations.forEach(relation -> { - relation.getTargets().values().forEach(target -> { - connections.append(String.format("connect(%s,%s, %s, %s),", relation.getSource().scalarVariable.getInstance().getText().toLowerCase(), - relation.getSource().scalarVariable.getScalarVariable().getName().toLowerCase(), - target.scalarVariable.getInstance().getText().toLowerCase(), - target.scalarVariable.getScalarVariable().getName().toLowerCase())); - }); - }); - return fixListFormat(connections).toString(); - } - - private StringBuilder fixListFormat(StringBuilder stringBuilder) { - if (stringBuilder.length() > 0) { - stringBuilder.setLength(stringBuilder.length() - 1); - } - stringBuilder.insert(0, "["); - stringBuilder.append("]"); - return stringBuilder; - } - - private String getInPorts(Set relations, LexIdentifier fmu) { - StringBuilder inPorts = new StringBuilder(); - var inputPorts = relations.stream().map(p -> p.getTargets().values()).collect(Collectors.toList()).stream().flatMap(Collection::stream) - .collect(Collectors.toSet()).stream().filter(o -> o.scalarVariable.getInstance().getText().equals(fmu.getText())) - .collect(Collectors.toSet()); - - inputPorts.forEach(port -> { - inPorts.append(String.format("port(%s, delayed),", port.scalarVariable.getScalarVariable().getName().toLowerCase())); - }); - - return fixListFormat(inPorts).toString(); - } - - private String getOutPorts(Set relations, LexIdentifier fmu) { - StringBuilder outPorts = new StringBuilder(); - var externalRelations = relations.stream().filter(o -> o.getOrigin() == Fmi2SimulationEnvironment.Relation.InternalOrExternal.External) - .collect(Collectors.toSet()); - var internalRelations = relations.stream().filter(o -> o.getOrigin() == Fmi2SimulationEnvironment.Relation.InternalOrExternal.Internal) - .collect(Collectors.toSet()); - var outputPorts = externalRelations.stream().filter(p -> p.getSource().scalarVariable.getInstance() == fmu).collect(Collectors.toSet()); - - outputPorts.forEach(port -> { - outPorts.append(String.format("port(%s, %s),", port.getSource().scalarVariable.getScalarVariable().getName().toLowerCase(), - getInternalDependencies(port.getSource(), internalRelations))); - }); - - return fixListFormat(outPorts).toString(); - } - - private String getInternalDependencies(Fmi2SimulationEnvironment.Variable source, Set internalRelations) { - var sources = - internalRelations.stream().filter(rel -> rel.getSource() == source).map(o -> o.getTargets().values()).collect(Collectors.toSet()) - .stream().flatMap(Collection::stream).collect(Collectors.toSet()); - - StringBuilder internalConnections = new StringBuilder(); - sources.forEach(s -> { - internalConnections.append(String.format("%s,", s.scalarVariable.getScalarVariable().getName().toLowerCase())); - }); - - return fixListFormat(internalConnections).toString(); - } - - private String getMethod(Fmi2SimulationEnvironment.Variable variable) throws ExpandException { - if (variable.scalarVariable.getScalarVariable().causality == Fmi2ModelDescription.Causality.Output) { - return "getOut"; - } else if (variable.scalarVariable.getScalarVariable().causality == Fmi2ModelDescription.Causality.Input) { - return "setIn"; - } else { - throw new ExpandException("Unknown causality of port"); - } - } -} diff --git a/plugins/verificationsuite/src/test/java/PrologVerifierTest.java b/plugins/verificationsuite/src/test/java/PrologVerifierTest.java deleted file mode 100644 index 76dcd16c5..000000000 --- a/plugins/verificationsuite/src/test/java/PrologVerifierTest.java +++ /dev/null @@ -1,81 +0,0 @@ -import org.intocps.maestro.ast.LexIdentifier; -import org.intocps.maestro.core.messages.IErrorReporter; -import org.intocps.maestro.fmi.Fmi2ModelDescription; -import org.intocps.maestro.framework.fmi2.Fmi2SimulationEnvironment; -import org.intocps.maestro.framework.fmi2.RelationVariable; -import org.intocps.maestro.plugin.verificationsuite.prologverifier.InitializationPrologQuery; -import org.junit.jupiter.api.Test; - -import java.io.InputStream; -import java.util.Arrays; -import java.util.HashSet; -import java.util.stream.Collectors; - -public class PrologVerifierTest { - InputStream envWaterTankJson = this.getClass().getResourceAsStream("PrologVerifierTest/env.json"); - InputStream envThreeTankJson = this.getClass().getResourceAsStream("PrologVerifierTest/threetank_env.json"); - - /* - @Test - public void VerifyInitializationOrderWatertankTest() throws Exception { - var prologVerifier = new InitializationPrologQuery(); - var unitRelationship = new UnitRelationship(envWaterTankJson); - var components = Arrays.asList("crtlInstance", "wtInstance"); - var relations = new HashSet(); - components.forEach(c -> relations.addAll(unitRelationship.getRelations(new LexIdentifier(c, null)))); - var initializationOrder = relations.stream().filter() - var result = prologVerifier.initializationOrderIsValid(); - assert(result); - }*/ - - @Test - public void verifyInitializationOrderNotValidWatertankTest() throws Exception { - var prologVerifier = new InitializationPrologQuery(); - var unitRelationship = Fmi2SimulationEnvironment.of(envWaterTankJson, new IErrorReporter.SilentReporter()); - var components = Arrays.asList("crtlInstance", "wtInstance"); - var relations = new HashSet(); - components.forEach(c -> relations.addAll(unitRelationship.getRelations(new LexIdentifier(c, null)))); - var initializationOrder = relations.stream().map(Fmi2SimulationEnvironment.Relation::getSource).distinct().collect(Collectors.toList()); - var result = prologVerifier.initializationOrderIsValid(initializationOrder, relations); - assert (!result); - } - - /* - @Test - public void VerifyInitializationOrderProlog() throws Exception { - var prologVerifier = new InitializationPrologQuery(); - var unitRelationship = new UnitRelationship(envThreeTankJson); - var relations = new ArrayList(); - - var variable1 = createVariable("Ctrl", "Sig", unitRelationship); - var variable2 = createVariable("Ctrl", "Input", unitRelationship); - var variable3 = createVariable("CE", "Level", unitRelationship); - var variable4 = createVariable("Tank", "Level", unitRelationship); - - HashMap target1 = new HashMap<>(); - target1.put(new LexIdentifier(variable1.scalarVariable.instance.getText(), null), variable1); - HashMap target2 = new HashMap<>(); - target2.put(new LexIdentifier(variable2.scalarVariable.instance.getText(), null), variable2); - HashMap target3 = new HashMap<>(); - target3.put(new LexIdentifier(variable3.scalarVariable.instance.getText(), null), variable3); - HashMap target4 = new HashMap<>(); - target4.put(new LexIdentifier(variable4.scalarVariable.instance.getText(), null), variable4); - relations.add(new UnitRelationship.Relation.RelationBuilder(variable1, target2).build()); - relations.add(new UnitRelationship.Relation.RelationBuilder(variable2, target3).build()); - relations.add(new UnitRelationship.Relation.RelationBuilder(variable3, target4).build()); - - var result = - prologVerifier.initializationOrderIsValid(relations.stream().map(UnitRelationship.Relation::getSource).collect(Collectors.toList()), new HashSet<>(relations)); - - assert(result); - } -*/ - - private Fmi2SimulationEnvironment.Variable createVariable(String fmuName, String variableName, Fmi2SimulationEnvironment unitRelationship) { - var scalarVar = new Fmi2ModelDescription.ScalarVariable(); - scalarVar.name = variableName; - return new Fmi2SimulationEnvironment.Variable(new RelationVariable(scalarVar, new LexIdentifier(fmuName, null))); - } - -} - diff --git a/plugins/verificationsuite/src/test/resources/PrologVerifierTest/config.json b/plugins/verificationsuite/src/test/resources/PrologVerifierTest/config.json index 4ff409178..befe202dc 100644 --- a/plugins/verificationsuite/src/test/resources/PrologVerifierTest/config.json +++ b/plugins/verificationsuite/src/test/resources/PrologVerifierTest/config.json @@ -3,8 +3,7 @@ "parameters": { "{crtl}.crtlInstance.maxlevel": 2, "{crtl}.crtlInstance.minlevel": 1 - }, - "verifyAgainstProlog": true + } } } diff --git a/pom.xml b/pom.xml index 35402200c..46db6e9ff 100644 --- a/pom.xml +++ b/pom.xml @@ -37,21 +37,21 @@ - - maestro2-third-party - maestro2-third-party - https://overture.au.dk/artifactory/maestro2-third-party - - - overture.au.dk - overture.au.dk-releases - https://overture.au.dk/artifactory/into-cps - - - vdmj - overture.au.dk-vdmj - https://overture.au.dk/artifactory/vdmj - + + + + + + + + + + + + + + + @@ -367,9 +367,9 @@ - INTO-CPS-Association - scenario_verifier_2.13 - 0.2.6 + org.into-cps.verification + scenario_verifier + 0.2.21-SNAPSHOT @@ -746,30 +746,30 @@ - - maestro2-third-party - maestro2-third-party - https://overture.au.dk/artifactory/maestro2-third-party - - interval:30 - - - - overture.au.dk - overture.au.dk-releases - https://overture.au.dk/artifactory/into-cps - - interval:30 - - - - vdmj - overture.au.dk-vdmj - https://overture.au.dk/artifactory/vdmj - - interval:30 - - + + + + + + + + + + + + + + + + + + + + + + + +