From 6446353b119ff231b9d634e25dba5a4c493dbd1d Mon Sep 17 00:00:00 2001 From: Simon Thrane Date: Mon, 11 Dec 2023 08:27:05 +0100 Subject: [PATCH] Updated references to Scenario-Verifier --- .../webapi/maestro2/Maestro2Broker.java | 4 +- .../maestro2/Maestro2ScenarioController.java | 43 +++++++++---------- .../maestro2/dto/VerificationResult.java | 21 +++++++++ 3 files changed, 43 insertions(+), 25 deletions(-) create mode 100644 maestro-webapi/src/main/java/org/intocps/maestro/webapi/maestro2/dto/VerificationResult.java 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..d86d1aa26 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,17 +1,16 @@ package org.intocps.maestro.webapi.maestro2; - -import api.TraceResult; -import api.VerificationAPI; -import cli.VerifyTA; -import core.MasterModel; -import core.ModelEncoding; -import core.ScenarioGenerator; -import core.ScenarioLoader; +import org.intocps.verification.scenarioverifier.core.MasterModel; +import org.intocps.verification.scenarioverifier.core.ScenarioLoader; +import org.intocps.verification.scenarioverifier.core.ModelEncoding; +import org.intocps.verification.scenarioverifier.core.ScenarioGenerator; +import org.intocps.verification.scenarioverifier.api.TraceResult; +import org.intocps.verification.scenarioverifier.api.VerificationAPI; +import org.intocps.verification.scenarioverifier.cli.VerifyTA; import org.intocps.maestro.core.dto.ExtendedMultiModel; import org.intocps.maestro.core.messages.ErrorReporter; import org.intocps.maestro.plugin.MasterModelMapper; import org.intocps.maestro.webapi.dto.ExecutableMasterAndMultiModelTDO; -import org.intocps.maestro.webapi.dto.VerificationDTO; +import org.intocps.maestro.webapi.dto.VerificationResult; import org.intocps.maestro.webapi.maestro2.dto.SigverSimulateRequestBody; import org.intocps.maestro.webapi.util.ZipDirectory; import org.springframework.core.io.FileSystemResource; @@ -21,7 +20,6 @@ import org.springframework.http.converter.HttpMessageNotReadableException; import org.springframework.stereotype.Component; import org.springframework.web.bind.annotation.*; -import synthesizer.ConfParser.ScenarioConfGenerator; import javax.servlet.http.HttpServletRequest; import javax.servlet.http.HttpServletResponse; @@ -45,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,17 +51,17 @@ 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. @@ -75,25 +73,25 @@ public VerificationDTO verifyAlgorithm(@RequestBody String masterModelAsString) try (Writer writer = new BufferedWriter(new OutputStreamWriter(new FileOutputStream(tempFile), StandardCharsets.UTF_8))) { writer.write(encodedModel); } - int verificationCode = VerifyTA.verify(tempFile); + int verificationCode = VerifyTA.verify(tempFile, false); tempFile.delete(); switch (verificationCode) { case 0: - return new VerificationDTO(true, encodedModel, ""); + return new VerificationResult(true, encodedModel, ""); case 1: - return new VerificationDTO(false, encodedModel, "Model is not valid. Generate the trace and use it to correct the algorithm."); + return new VerificationResult(false, encodedModel, "Model is not valid. Generate the trace and use it to correct the algorithm."); case 2: - return new VerificationDTO(false, encodedModel, + return new VerificationResult(false, encodedModel, "The verification in Uppaal failed most likely due to a syntax error in the " + "UPPAAL model."); default: - return new VerificationDTO(false, encodedModel, ""); + return new VerificationResult(false, encodedModel, ""); } } @RequestMapping(value = "/visualizeTrace", method = RequestMethod.POST, consumes = MediaType.TEXT_PLAIN_VALUE, produces = "video/mp4") public FileSystemResource visualizeTrace(@RequestBody String masterModelAsString) throws Exception { MasterModel masterModel = ScenarioLoader.load(new ByteArrayInputStream(masterModelAsString.getBytes())); - TraceResult traceResult = VerificationAPI.generateTraceFromMasterModel(masterModel); + TraceResult traceResult = VerificationAPI.generateTraceVideo(masterModel); if (!traceResult.isGenerated()) { throw new Exception("Unable to generate trace results - the algorithm is probably successfully verified"); @@ -130,8 +128,7 @@ public void executeAlgorithm(@RequestBody ExecutableMasterAndMultiModelTDO execu Maestro2Broker broker = new Maestro2Broker(zipDir, reporter, () -> false); SigverSimulateRequestBody requestBody = new SigverSimulateRequestBody(executableModel.getExecutionParameters().getStartTime(), - executableModel.getExecutionParameters().getEndTime(), Map.of(), false, 0d, - ScenarioConfGenerator.generate(masterModel, masterModel.name())); + executableModel.getExecutionParameters().getEndTime(), Map.of(), false, 0d, masterModel.toConf(0)); broker.buildAndRunMasterModel(null, null, executableModel.getMultiModel(), requestBody, new File(zipDir, "outputs.csv")); 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; + } +}