add how to run

how_to_run.md

@@ -0,0 +1,32 @@
+# Workflow
+
+1. Optional: modify the AADL model and then rerun codegen
+
+    * [isolette/aadl/bin/run-hamr.cmd](isolette/aadl/bin/run-hamr.cmd)
+
+    The model is in [isolette/aadl/aadl/packages](isolette/aadl/aadl/packages)
+
+1. Modify system testing containers
+
+    The following are relative to [isolette/hamr/slang/src/main/util/isolette/system_tests](isolette/hamr/slang/src/main/util/isolette/system_tests)
+
+    * [monitor1/Monitor_Subsystem_Containers.scala](isolette/hamr/slang/src/main/util/isolette/system_tests/monitor1/Monitor_Subsystem_Containers.scala)
+
+    * [rst/Regulate_Subsystem_Containers.scala](isolette/hamr/slang/src/main/util/isolette/system_tests/rst/Regulate_Subsystem_Containers.scala)
+
+1. Rerun system testing artifact generator
+
+    The following is relative to [isolette/hamr/slang](isolette/hamr/slang)
+
+    * [bin/generate-system-test-artifacts.sc](isolette/hamr/slang/bin/generate-system-test-artifacts.sc)
+
+
+1. Update system testing schemas
+
+    The following are relative to [isolette/hamr/slang/src/test/system/isolette/system_tests](isolette/hamr/slang/src/test/system/isolette/system_tests)
+
+    * [monitor1/Monitor_Subsystem_Test_wSlangCheck.scala](isolette/hamr/slang/src/test/system/isolette/system_tests/monitor1/Monitor_Subsystem_Test_wSlangCheck.scala)
+
+    * [rst/Regulate_Subsystem_Test_wSlangCheck.scala](isolette/hamr/slang/src/test/system/isolette/system_tests/rst/Regulate_Subsystem_Test_wSlangCheck.scala)
+
+

isolette/hamr/slang/src/test/system/isolette/system_tests/monitor1/Example_Monitor_Subsystem_Inputs_Container_DSC_Test_Harness.scala

@@ -0,0 +1,85 @@
+package isolette.system_tests.monitor1
+
+import org.sireum._
+import isolette._
+import isolette.system_tests.monitor1.Monitor_Subsystem_Inputs_Container_SlangCheck.SystemTestConfiguration
+
+// Do not edit this file as it will be overwritten if SystemTestArtifactGen is rerun
+
+object Example_Monitor_Subsystem_Inputs_Container_DSC_Test_Harness extends App {
+
+  // main generates the Jenkins build parameters string and the JSON serialized testRow information
+  override def main(args: ISZ[String]): Z = {
+    // Regenerate the json files and emit their locations to the console. The
+    // exampleJenkinsScript.cmd will use these to get the test configurations keys
+    Example_Monitor_Subsystem_Inputs_Container_Test_wSlangCheck.genJsons(T)
+
+    return 0
+  }
+}
+
+class Example_Monitor_Subsystem_Inputs_Container_DSC_Test_Harness
+  extends Example_Monitor_Subsystem_Inputs_Container_Test_wSlangCheck
+  with Monitor_Subsystem_Inputs_Container_DSC_Test_Harness {
+
+  override def next(): isolette.system_tests.monitor1.Monitor_Subsystem_Inputs_Container = {
+    return getConfig().profile.next()
+  }
+
+  override def test(o: isolette.system_tests.monitor1.Monitor_Subsystem_Inputs_Container): B = {
+    val config = getConfig()
+
+    if (verbose) {
+      println(genTestName(config))
+    }
+
+    disableLogsAndGuis()
+
+    super.beforeEach()
+
+    if (!config.filter.function(o)) {
+
+      if (verbose) {
+        println(s"  Didn't pass pre state check ${o}")
+      }
+
+      DSC_RecordUnsatPre.report(toCompactJson(o))
+
+      return T
+    } else {
+
+      val result = config.schema.function(o, config.property.function)
+
+      this.afterEach()
+
+      if (verbose) {
+        println(s"  ${result}")
+      }
+      return result
+    }
+  }
+
+  def getConfig(): SystemTestConfiguration = {
+    Os.prop("DSC_TEST_CONFIGURATION_NAME") match {
+      case Some(v) => return ops.ISZOps(configurations).filter(p => p.name == v)(0)
+      case _ =>
+        Os.env("DSC_TEST_CONFIGURATION_NAME") match {
+          case Some(v) => return ops.ISZOps(configurations).filter(p => p.name == v)(0)
+          case _ =>
+        }
+    }
+    halt("DSC_TEST_CONFIGURATION_NAME not defined")
+  }
+
+  override def string: String = toString
+
+  override def $clonable: Boolean = F
+
+  override def $clonable_=(b: Boolean): org.sireum.$internal.MutableMarker = this
+
+  override def $owned: Boolean = F
+
+  override def $owned_=(b: Boolean): org.sireum.$internal.MutableMarker = this
+
+  override def $clone: org.sireum.$internal.MutableMarker = this
+}

isolette/hamr/slang/src/test/system/isolette/system_tests/monitor1/Example_Monitor_Subsystem_Inputs_Container_Test_wSlangCheck.scala

@@ -0,0 +1,248 @@
+package isolette.system_tests.monitor1
+
+import org.sireum._
+import art.scheduling.static._
+import art.Art
+import isolette._
+import isolette.system_tests.monitor1.Monitor_Subsystem_Inputs_Container_SlangCheck._
+import Example_Monitor_Subsystem_Inputs_Container_Test_wSlangCheck._
+import isolette.system_tests.monitor1.Monitor_Subsystem_Inputs_Container_Profile
+import isolette.system_tests.monitor1.Monitor_Subsystem_Inputs_Container_Profile._
+
+import scala.language.implicitConversions
+
+// Do not edit this file as it will be overwritten if SystemTestArtifactGen is rerun
+
+class Example_Monitor_Subsystem_Inputs_Container_Test_wSlangCheck
+  extends Monitor_Subsystem_Inputs_Container_SlangCheck {
+
+  //================================================================
+  //  S c h e d u l a r     and    S t e p p e r     Configuration
+  //================================================================
+
+  // note: this is overriding SystemTestSuite's 'def scheduler: Scheduler'
+  //       abstract method
+  //var scheduler: StaticScheduler = Schedulers.getStaticSchedulerH(MNone())
+  var scheduler: StaticScheduler = Schedulers.getStaticScheduler(
+    Schedulers.defaultStaticSchedule,
+    Schedulers.defaultDomainToBridgeIdMap,
+    Schedulers.threadNickNames,
+    ISZCommandProvider(ISZ()))
+
+  def compute(isz: ISZ[Command]): Unit = {
+    scheduler = scheduler(commandProvider = ISZCommandProvider(isz :+ Stop()))
+
+    Art.computePhase(scheduler)
+  }
+
+  override def beforeEach(): Unit = {
+
+    // uncomment the following to disable the various guis and to suppress the log streams
+    //disableLogsAndGuis()
+
+    super.beforeEach()
+  }
+
+  //===========================================================
+  //  S l a n g   C h e c k    Infrastructure
+  //===========================================================
+
+  val maxTests = 100
+  var verbose: B = T
+
+  val configurations: ISZ[SystemTestConfiguration] = ISZ(
+    SystemTestConfiguration(
+      name = "test-name", // must be unique and does not contain spaces
+      description = "Test description",
+      schema = exampleSchema _,
+      profile = getDefaultProfile,
+      filter = examplePreStateContainerFilter _,
+      property = exampleProperty _,
+      componentsOfInterest = ISZ(),
+      numTests = maxTests
+    )
+  )
+
+  for (config <- configurations) {
+    run(config)
+  }
+
+  def run(config: SystemTestConfiguration): Unit = {
+
+    def next: Option[Monitor_Subsystem_Inputs_Container] = {
+      try {
+        return Some(config.profile.next())
+      } catch {
+        case e: AssertionError => // SlangCheck was unable to satisfy a datatype's filter
+          return None()
+      }
+    }
+
+    for (i <- 0 until config.numTests) {
+      val testName = s"${genTestName(config)}_$i"
+      this.registerTest(testName) {
+        var retry: B = T
+        var j: Z = 0
+
+        while (j < config.profile.numTestVectorGenRetries && retry) {
+          if (verbose && j > 0) {
+            println(s"Retry $j:")
+          }
+
+          next match {
+            case Some(container) =>
+              if (!config.filter.function(container)) {
+                // retry
+              } else {
+                assert(config.schema.function(container, config.property.function))
+                retry = F
+              }
+            case _ =>
+          }
+          j = j + 1
+        }
+      }
+    }
+  }
+
+  def exampleSchema(input_container: Any, property_function: Any): B = {
+    return T
+  }
+
+  def exampleProperty(input_container: Any, output_container: Any): B = {
+    return T
+  }
+
+  // a pre-state container filter could prove useful/necessary in order to
+  // ensure that the values in the container will satisfy the assume/requires clause
+  // of a component in the system that will receive those values
+  def examplePreStateContainerFilter(container: Monitor_Subsystem_Inputs_Container): B = {
+    // e.g. return container.low < container.high
+    return T
+  }
+
+  def genTestName(config: SystemTestConfiguration): String = {
+    return s"${config.name}: ${config.schema.name}: ${config.property.name}: ${config.profile.name}"
+  }
+
+  def genTestNameJson(config: SystemTestConfiguration): String = {
+    @strictpure def p(str: String): ST = Json.Printer.printString(str)
+    return st"""{"name" : ${p(config.name)}, "description" : ${p(config.description)}, "schema": ${p(config.schema.name)}, "property" : ${p(config.property.name)}, "profile" : ${p(config.profile.name)}}"""".render
+  }
+
+  override def beforeAll(): Unit = {
+    val s = Set.empty[String] ++ (for(c <- configurations) yield c.name)
+    assert (s.size == configurations.size, "Configuration names must be unique")
+    assert (ops.ISZOps(s.elements).forall(p => !ops.StringOps(p).contains(" ")), "Configuration names cannot contain spaces")
+
+    propStatus = Map.empty
+    super.beforeAll()
+  }
+
+  val failOnTriviallyTrueProps: B = T
+
+  override def afterAll(): Unit = {
+    var msgs: ISZ[String] = ISZ()
+    for (p <- propStatus.entries if p._2.triggerT_desiredT == 0) {
+      // propStatus has three fields
+      //   # of F -> X
+      //   # of T -> F  --> the test case would have failed for T -> F so this should be 0
+      //   # of T -> T  --> may need to increase # of tests if this is always 0
+      msgs = msgs :+ s"Property ${p._1} was trivially true ${p._2.triggerF} times, desired failed ${p._2.triggerT_desiredF} times, and desired was never satisfied"
+    }
+    if (msgs.nonEmpty) {
+      if (failOnTriviallyTrueProps) {
+        assert(F, st"${(msgs, "\n")}".render)
+      } else {
+        cprint(T, st"${(msgs, "\n")}".render)
+      }
+    }
+    super.afterAll()
+  }
+
+  def bookKeep(triggerCond: B, desiredCond: B): Unit = {
+    val propName = Thread.currentThread().getStackTrace()(2).getMethodName
+    val prop = propStatus.getOrElse(propName, PropStatus(0,0,0))
+    propStatus = propStatus + propName ~> prop.copy(
+      triggerF = prop.triggerF + (if (!triggerCond) 1 else 0),
+      triggerT_desiredF = prop.triggerT_desiredF + (if (triggerCond && !desiredCond) 1 else 0),
+      triggerT_desiredT = prop.triggerT_desiredT + (if (triggerCond && desiredCond) 1 else 0)
+    )
+  }
+
+  implicit def toNameProvider1[X](eta: X => B)(implicit line: sourcecode.Line): NameProvider1 = {
+    val l = ops.StringOps(lines(line.value - 1))
+    return NameProvider1(l.substring(l.lastIndexOf('=') + 2, l.lastIndexOf('_') - 1), eta)
+  }
+
+  implicit def toNameProvider2[X, Y](eta: (X, Y) => B)(implicit line: sourcecode.Line): NameProvider2 = {
+    val l = ops.StringOps(lines(line.value - 1))
+    return NameProvider2(l.substring(l.lastIndexOf('=') + 2, l.lastIndexOf('_') - 1), eta)
+  }
+
+  implicit def oneToGen[X](eta: (X) => B): Any => B = eta.asInstanceOf[Any => B]
+
+  implicit def twoToGen[X, Y](eta: (X, Y) => B): (Any, Any) => B = eta.asInstanceOf[(Any, Any) => B]
+}
+
+object Example_Monitor_Subsystem_Inputs_Container_Test_wSlangCheck {
+
+  case class PropStatus (val triggerF: Z,
+                         val triggerT_desiredF: Z,
+                         val triggerT_desiredT: Z)
+
+  var propStatus: Map[String, PropStatus] = Map.empty
+
+  val lines: ISZ[String] = {
+    val ll: String = Os.env("ABS_JAR_LOC") match {
+      case Some(l) =>
+        // must be running from the jar file so need to unpack it to get the source files
+        val tempDir = Os.tempDir()
+        proc"unzip $l -d $tempDir".runCheck()
+        val name = ops.ISZOps(ops.StringOps(ops.StringOps(getClass.getName).replaceAllLiterally("$", "")).split(c => c == C('.')))
+        val ret = ((tempDir /+ name.dropRight(1)) / s"${name.last}.scala").read
+        tempDir.removeAll()
+        ret
+      case _ => Os.path(implicitly[sourcecode.File].value).read
+    }
+    ops.StringOps(ops.StringOps(ll).replaceAllLiterally("\n", " \n")).split(c => c == C('\n'))
+  }
+
+  @strictpure def p(str: String): ST = Json.Printer.printString(str)
+
+  val dummy = genJsons(F)   // doing this a var decl so that the actions are invoked when the JVM loads the object
+
+  def genJsons(echo: B): B = {
+    if (Os.env("JENKINS_HOME").isEmpty) { // don't generate these when CI
+      // emit test configs as JSON
+      val inst = new Example_Monitor_Subsystem_Inputs_Container_Test_wSlangCheck()
+      val entries = for (entry <- inst.configurations) yield inst.genTestNameJson(entry)
+      val thisFile = Os.path(implicitly[sourcecode.File].value)
+      val outFile = thisFile.up / s"${thisFile.name}.json"
+      outFile.writeOver(st"${(entries, "\n")}".render)
+
+      // emit schedule as JSON
+      val nickNames: ISZ[ST] = for (e <- inst.scheduler.threadNickNames.entries) yield
+        st"${e._1}:${Arch.ad.components(e._2).name}"
+      val nickNamesS = st"${(nickNames, ",")}".render
+      val revMap = Map.empty[Art.BridgeId, String] ++ (for(e <- inst.scheduler.threadNickNames.entries) yield e._2 ~> e._1)
+      val sched: ISZ[ST] = for (e <- inst.scheduler.domainToBridgeIdMap) yield
+        st"""${revMap.get(e).get}"""
+      val schedS = st"${(sched, ",")}".render
+      val schedFile = thisFile.up / s"${thisFile.name}_schedule.json"
+      schedFile.writeOver(
+        st"""{
+            |  "nickNames": ${p(nickNamesS)},
+            |  "scheduleProvider": ${p(inst.scheduler.getClass.getName)},
+            |  "schedule": ${p(schedS)}
+            |}""".render)
+
+      if (echo) {
+        println(outFile)
+        println(schedFile)
+      }
+    }
+
+    F
+  }
+}