From c8dd0bb7e6b1f63d31dba4838443fd5c645812ae Mon Sep 17 00:00:00 2001
From: Simon Thrane <sthranehansen@gmail.com>
Date: Tue, 2 Jan 2024 09:09:51 +0100
Subject: [PATCH] Added mechanism to keep uppaal file for debugging

---
 .../scenarioverifier/api/Verification.scala   | 21 ++++++++-----------
 .../DynamicVerification/PositiveTests.scala   |  3 +--
 2 files changed, 10 insertions(+), 14 deletions(-)

diff --git a/src/main/scala/org/intocps/verification/scenarioverifier/api/Verification.scala b/src/main/scala/org/intocps/verification/scenarioverifier/api/Verification.scala
index 1b07075..fbb2d0c 100644
--- a/src/main/scala/org/intocps/verification/scenarioverifier/api/Verification.scala
+++ b/src/main/scala/org/intocps/verification/scenarioverifier/api/Verification.scala
@@ -44,7 +44,7 @@ object VerificationAPI extends Logging {
    * @return
    *   true if the algorithm is correct, false otherwise
    */
-  def verifyFMI3Algorithm(masterModel: MasterModelFMI3): Boolean = {
+  private def verifyFMI3Algorithm(masterModel: MasterModelFMI3): Boolean = {
     SMTEncoder.verifyAlgorithm(masterModel)
   }
 
@@ -61,13 +61,15 @@ object VerificationAPI extends Logging {
   private def verifyFMI2Algorithm(
       masterModel: MasterModelFMI2,
       uppaalFileType: (String, ModelEncoding, Directory) => File,
-      isOnlineMode: Boolean = false): Boolean = {
+      isOnlineMode: Boolean = false,
+      deleteUppallFile : Boolean = true): Boolean = {
     if (!isOnlineMode) {
       require(VerifyTA.isInstalled, "Uppaal is not installed, please install it and add it to your PATH")
     }
     val uppaalFile = generateUppaalFile(masterModel, uppaalFileType)
     val verificationResult = VerifyTA.verify(uppaalFile, isOnlineMode)
-    FileUtils.deleteQuietly(uppaalFile)
+    if(deleteUppallFile)
+      FileUtils.deleteQuietly(uppaalFile)
     checkVerificationResult(verificationResult)
   }
 
@@ -87,7 +89,8 @@ object VerificationAPI extends Logging {
   def dynamicVerification(
       scenarioModel: FMI2ScenarioModel,
       previous_actions: List[CosimStepInstruction],
-      next_action: CosimStepInstruction): Verdict = {
+      next_action: CosimStepInstruction,
+      deleteUppaalFile : Boolean = true): Verdict = {
     // Does the previous actions contain repeated actions?
     val connectionsSrc = scenarioModel.connections.groupBy(_.srcPort)
     val numberOfActionsInAlgorithm = connectionsSrc
@@ -97,13 +100,6 @@ object VerificationAPI extends Logging {
     val firstAction = Math.max(previous_actions.size - actionsToCheck, 0)
     val filtered_previous_actions = previous_actions.drop(firstAction)
 
-    /*
-    val lastIndexOfFirstAction = if (previous_actions.nonEmpty)
-      previous_actions.lastIndexOf(previous_actions.head)
-    else 0
-    val filtered_previous_actions = previous_actions.drop(lastIndexOfFirstAction)
-     */
-
     val masterModel = MasterModelFMI2(
       "dynamic_verification",
       scenarioModel,
@@ -114,11 +110,12 @@ object VerificationAPI extends Logging {
 
     val cachedResult = lookupInCache(masterModel)
     if (cachedResult.isDefined) {
+      logger.info("Verdict found in cache - skipping verification in Uppaal")
       return Verdict(cachedResult.get, Predef.Set.empty)
     }
 
     val verdict =
-      if (verifyFMI2Algorithm(masterModel, ScenarioGenerator.generateDynamicNoEnabledUppaalFile, isOnlineMode = true)) {
+      if (verifyFMI2Algorithm(masterModel, ScenarioGenerator.generateDynamicNoEnabledUppaalFile, isOnlineMode = true, deleteUppaalFile)) {
         // If the algorithm is correct, we don't need to generate a trace
         Verdict(correct = true, Predef.Set.empty)
       } else {
diff --git a/src/test/scala/DynamicVerification/PositiveTests.scala b/src/test/scala/DynamicVerification/PositiveTests.scala
index 5e0aba2..5d8f012 100644
--- a/src/test/scala/DynamicVerification/PositiveTests.scala
+++ b/src/test/scala/DynamicVerification/PositiveTests.scala
@@ -6,14 +6,13 @@ import org.scalatest.flatspec._
 import org.scalatest.matchers._
 
 class PositiveTests extends AnyFlatSpec with should.Matchers {
-
   def generateAndVerify(resourcesFile: String): Boolean = {
     val conf = getClass.getResourceAsStream(resourcesFile)
     val masterModel = ScenarioLoaderFMI2.load(conf)
     (1 until masterModel.cosimStep.values.head.length).forall(i => {
       val previous_actions = masterModel.cosimStep.values.head.take(i)
       val current_action = masterModel.cosimStep.values.head(i)
-      VerificationAPI.dynamicVerification(masterModel.scenario, previous_actions, current_action).correct
+      VerificationAPI.dynamicVerification(masterModel.scenario, previous_actions, current_action, false).correct
     })
   }