Updated scenarioLoading

INTO-CPS-Association · Dec 20, 2023 · 6ccdbfd · 6ccdbfd
1 parent 143c14b
commit 6ccdbfd
Show file tree

Hide file tree

Showing 9 changed files with 231 additions and 321 deletions.
diff --git a/src/main/scala/org/intocps/verification/scenarioverifier/cli/Z3/Z3ModelParser.scala b/src/main/scala/org/intocps/verification/scenarioverifier/cli/Z3/Z3ModelParser.scala
@@ -4,8 +4,8 @@ import org.intocps.verification.scenarioverifier
 import org.intocps.verification.scenarioverifier.core.masterModel._
 import org.intocps.verification.scenarioverifier.core.CosimStepInstruction
 import org.intocps.verification.scenarioverifier.core.DefaultStepSize
+import org.intocps.verification.scenarioverifier.core.EventInstruction
 import org.intocps.verification.scenarioverifier.core.FMI3
-import org.intocps.verification.scenarioverifier.core.FMI3.EventInstruction
 import org.intocps.verification.scenarioverifier.core.FMI3.Get
 import org.intocps.verification.scenarioverifier.core.FMI3.GetClock
 import org.intocps.verification.scenarioverifier.core.FMI3.SetClock
@@ -26,16 +26,21 @@ object Z3ModelParser {
     actions.sortBy(_._2).map(_._1)
   }
 
+  private def parsePortRef(action: String): PortRef = {
+    val fmuName = action.split("-").head
+    val portName = action.split("-").last
+    PortRef(fmuName, portName)
+  }
+
   private def parseZ3InitAlgorithm(algorithm: String, masterModel: MasterModelFMI3): List[InitializationInstruction] = {
     val actions = filterActions(algorithm)
     val instructions = actions.map(action => {
-      val fmuName = action.split("-").head
-      val portName = action.split("-").last
-      val fmuModel = masterModel.scenario.fmus(fmuName)
-      if (fmuModel.inputs.contains(portName))
-        InitSet(PortRef(fmuName, portName))
-      else if (fmuModel.outputs.contains(portName))
-        InitGet(PortRef(fmuName, portName))
+      val portRef = parsePortRef(action)
+      val fmuModel = masterModel.scenario.fmus(portRef.fmu)
+      if (fmuModel.inputs.contains(portRef.port))
+        InitSet(portRef)
+      else if (fmuModel.outputs.contains(portRef.port))
+        InitGet(portRef)
       else
         throw new Exception(s"The action $action is not a valid action in the given context")
     })
@@ -65,17 +70,16 @@ object Z3ModelParser {
   private def parseZ3EventAlgorithm(algorithm: String, masterModel: MasterModelFMI3): List[EventInstruction] = {
     val actions = filterActions(algorithm)
     val instructions = actions.map(action => {
-      val fmuName = action.split("-").head
-      val portName = action.split("-").last
-      val fmuModel = masterModel.scenario.fmus(fmuName)
-      if (fmuModel.inputs.contains(portName))
-        FMI3.Set(PortRef(fmuName, portName))
-      else if (fmuModel.outputs.contains(portName))
-        Get(PortRef(fmuName, portName))
-      else if (fmuModel.inputClocks.contains(portName))
-        SetClock(PortRef(fmuName, portName))
-      else if (fmuModel.outputClocks.contains(portName))
-        GetClock(PortRef(fmuName, portName))
+      var portRef = parsePortRef(action)
+      val fmuModel = masterModel.scenario.fmus(portRef.fmu)
+      if (fmuModel.inputs.contains(portRef.port))
+        FMI3.Set(portRef)
+      else if (fmuModel.outputs.contains(portRef.port))
+        Get(portRef)
+      else if (fmuModel.inputClocks.contains(portRef.port))
+        SetClock(portRef)
+      else if (fmuModel.outputClocks.contains(portRef.port))
+        GetClock(portRef)
       else
         throw new Exception(s"The action $action is not a valid action in the given context")
     })

diff --git a/...in/scala/org/intocps/verification/scenarioverifier/core/FMI3/SimulationInstructions.scala b/...in/scala/org/intocps/verification/scenarioverifier/core/FMI3/SimulationInstructions.scala
@@ -1,50 +1,37 @@
 package org.intocps.verification.scenarioverifier.core.FMI3
 
-import org.intocps.verification.scenarioverifier.core.masterModel.SMTLibElement
+import org.intocps.verification.scenarioverifier.core.EventInstruction
 import org.intocps.verification.scenarioverifier.core.InitializationInstruction
+import org.intocps.verification.scenarioverifier.core.PortAction
 import org.intocps.verification.scenarioverifier.core.PortRef
-import org.intocps.verification.scenarioverifier.core.SimulationInstruction
 
-final case class GetShift(port: PortRef) extends InitializationInstruction {
-  override def fmu: String = port.fmu
+final case class GetShift(port: PortRef) extends InitializationInstruction with PortAction {
+  override def action: String = "get-shift"
 
-  override def toUppaal: String = s"{$fmu, getShift, ${fmuPortName(port)}, noStep, noFMU, final, noLoop}"
-
-  override def toConf(indentationLevel: Int): String = s"${indentBy(indentationLevel)}{get-shift: ${generatePort(port)}}"
+  override def UPPAALaction: String = "getShift"
 
   override def toSMTLib: String = s"${fmu}_${port.port}_shift"
 }
 
-final case class GetInterval(port: PortRef) extends InitializationInstruction {
-  override def fmu: String = port.fmu
+final case class GetInterval(port: PortRef) extends InitializationInstruction with PortAction {
 
-  override def toUppaal: String = s"{$fmu, getInterval, ${fmuPortName(port)}, noStep, noFMU, final, noLoop}"
+  override def action: String = "get-interval"
 
-  override def toConf(indentationLevel: Int): String = s"${indentBy(indentationLevel)}{get-interval: ${generatePort(port)}}"
+  override def UPPAALaction: String = "getInterval"
 
   override def toSMTLib: String = s"${fmu}_${port.port}_shift"
 }
 
-sealed abstract class EventInstruction extends SimulationInstruction with SMTLibElement
-
-final case class Set(port: PortRef) extends EventInstruction {
-  override def fmu: String = port.fmu
-
-  override def toUppaal: String = s"{$fmu, set, ${fmuPortName(port)}, noStep, noFMU, final, noLoop}"
-
-  override def toConf(indentationLevel: Int): String = s"${indentBy(indentationLevel)}{set: ${generatePort(port)}}"
+final case class Set(port: PortRef) extends PortAction {
+  override def action: String = "set"
 
-  override def toSMTLib: String = s"${fmu}_${port.port}"
+  override def UPPAALaction: String = "set"
 }
 
-final case class Get(port: PortRef) extends EventInstruction {
-  override def fmu: String = port.fmu
+final case class Get(port: PortRef) extends PortAction {
+  override def action: String = "get"
 
-  override def toUppaal: String = s"{$fmu, get, ${fmuPortName(port)}, noStep, noFMU, final, noLoop}"
-
-  override def toConf(indentationLevel: Int): String = s"${indentBy(indentationLevel)}{get: ${generatePort(port)}}"
-
-  override def toSMTLib: String = s"${fmu}_${port.port}"
+  override def UPPAALaction: String = "get"
 }
 
 final case class StepE(fmu: String) extends EventInstruction {
@@ -56,35 +43,21 @@ final case class StepE(fmu: String) extends EventInstruction {
   override def toSMTLib: String = s"${fmu}_stepE"
 }
 
-final case class GetClock(port: PortRef) extends EventInstruction {
-  override def toUppaal: String =
-    s"{$fmu, getClock, ${fmuPortName(port)}, noStep, noFMU, final, noLoop}"
-
-  override def toConf(indentationLevel: Int): String = s"${indentBy(indentationLevel)}{get-clock: ${generatePort(port)}}"
-
-  override def fmu: String = port.fmu
+final case class GetClock(port: PortRef) extends PortAction {
+  override def action: String = "get-clock"
 
-  override def toSMTLib: String = s"${fmu}_${port.port}"
+  override def UPPAALaction: String = "getClock"
 }
 
-final case class SetClock(port: PortRef) extends EventInstruction {
-  override def toUppaal: String =
-    s"{$fmu, setClock, ${fmuPortName(port)}, noStep, noFMU, final, noLoop}"
-
-  override def toConf(indentationLevel: Int): String = s"${indentBy(indentationLevel)}{set-clock: ${generatePort(port)}}"
+final case class SetClock(port: PortRef) extends PortAction {
+  override def action: String = "set-clock"
 
-  override def fmu: String = port.fmu
-
-  override def toSMTLib: String = s"${fmu}_${port.port}"
+  override def UPPAALaction: String = "setClock"
 }
 
-final case class NextClock(port: PortRef) extends EventInstruction with SMTLibElement {
-  override def toUppaal: String =
-    s"{$fmu, nextClock, ${fmuPortName(port)}, noStep, noFMU, final, noLoop}"
-
-  override def toConf(indentationLevel: Int): String = s"${indentBy(indentationLevel)}{next: ${generatePort(port)}}"
+final case class NextClock(port: PortRef) extends PortAction {
+  override def action: String = "next"
 
-  override def fmu: String = port.fmu
+  override def UPPAALaction: String = "nextClock"
 
-  override def toSMTLib: String = s"${fmu}_${port.port}"
 }