TempControlPeriodic_p_tcproc_tempControl_UnitTestConfiguration_Util.scala

// #Sireum

package tc.TempControlSoftwareSystem

// Do not edit this file as it will be overwritten if HAMR codegen is rerun

import org.sireum._
import tc.GumboXUtil.GumboXResult
import tc.util.{Container, Profile, UnitTestConfigurationBatch}
import tc.RandomLib
import org.sireum.Random.Impl.Xoshiro256

object TempControlPeriodic_p_tcproc_tempControl_UnitTestConfiguration_Util {

  def freshRandomLib: RandomLib = {
    return RandomLib(Random.Gen64Impl(Xoshiro256.create))
  }

  val tq: String = "\"\"\""

  type DefaultInitializeProfile = TempControlPeriodic_p_tcproc_tempControl_Profile

  def defaultInitializeConfig: TempControlPeriodic_p_tcproc_tempControl_Initialize_UnitTestConfiguration = {
    return (TempControlPeriodic_p_tcproc_tempControl_Initialize_UnitTestConfiguration (
      verbose = F,
      name = "Default_Initialize_Config",
      description = "Default Initialize Configuration",
      numTests = 100,
      numTestVectorGenRetries = 100,
      failOnUnsatPreconditions = F,
      profile = TempControlPeriodic_p_tcproc_tempControl_Profile (
        name = "Initialize_Default_Profile",
      ),
      genReplay = (c: Container, testName: String, r: GumboXResult.Type) => None())
    )
  }

  type DefaultComputeProfile = TempControlPeriodic_p_tcproc_tempControl_Profile_P

  def defaultComputeConfig: TempControlPeriodic_p_tcproc_tempControl_Compute_UnitTestConfiguration = {
    return (TempControlPeriodic_p_tcproc_tempControl_Compute_UnitTestConfiguration (
      verbose = F,
      name = "Default_Compute_Config",
      description = "Default Compute Configuration",
      numTests = 100,
      numTestVectorGenRetries = 100,
      failOnUnsatPreconditions = F,
      profile = TempControlPeriodic_p_tcproc_tempControl_Profile_P (
        name = "Compute_Default_Profile",
        api_currentTemp = freshRandomLib,
        api_fanAck = freshRandomLib,
        api_setPoint = freshRandomLib
      ),
      genReplay = (c: Container, testName: String, r: GumboXResult.Type) => Some(
       st"""Replay Unit Test:
            |  test("Replay: $testName") {
            |    val results = tc.GumboXUtil.GumboXResult.$r
            |    val json = st${tq}${tc.JSON.fromutilContainer(c, T)}${tq}.render
            |    val testVector = tc.JSON.toTempControlSoftwareSystemTempControlPeriodic_p_tcproc_tempControl_PreState_Container_P(json).left
            |    assert (testComputeCBV(testVector) == results)
            |  }""".render))
    )
  }

  type DefaultComputewLProfile = TempControlPeriodic_p_tcproc_tempControl_Profile_PS

  def defaultComputewLConfig: TempControlPeriodic_p_tcproc_tempControl_ComputewL_UnitTestConfiguration = {
    return (TempControlPeriodic_p_tcproc_tempControl_ComputewL_UnitTestConfiguration (
      verbose = F,
      name = "Default_ComputewL_Config",
      description = "Default ComputewL Configuration",
      numTests = 100,
      numTestVectorGenRetries = 100,
      failOnUnsatPreconditions = F,
      profile = TempControlPeriodic_p_tcproc_tempControl_Profile_PS (
        name = "ComputewL_Default_Profile",
        In_latestFanCmd = freshRandomLib,
        api_currentTemp = freshRandomLib,
        api_fanAck = freshRandomLib,
        api_setPoint = freshRandomLib
      ),
      genReplay = (c: Container, testName: String, r: GumboXResult.Type) => Some(
       st"""Replay Unit Test:
            |  test("Replay: $testName") {
            |    val results = tc.GumboXUtil.GumboXResult.$r
            |    val json = st${tq}${tc.JSON.fromutilContainer(c, T)}${tq}.render
            |    val testVector = tc.JSON.toTempControlSoftwareSystemTempControlPeriodic_p_tcproc_tempControl_PreState_Container_PS(json).left
            |    assert (testComputeCBwLV(testVector) == results)
            |  }""".render))
    )
  }
}

@record class TempControlPeriodic_p_tcproc_tempControl_Initialize_UnitTestConfiguration (
  var verbose: B,
  var name: String,
  var description: String,
  var numTests: Z,
  var numTestVectorGenRetries: Z,
  var failOnUnsatPreconditions: B,
  var profile: TempControlPeriodic_p_tcproc_tempControl_Profile_Trait,
  var genReplay: (Container, String, GumboXResult.Type) => Option[String])
  extends UnitTestConfigurationBatch with TempControlPeriodic_p_tcproc_tempControl_GumboX_TestHarness {

  override def test(c: Container): GumboXResult.Type = {
    return testInitialiseCB()
  }
}

@record class TempControlPeriodic_p_tcproc_tempControl_Compute_UnitTestConfiguration (
  var verbose: B,
  var name: String,
  var description: String,
  var numTests: Z,
  var numTestVectorGenRetries: Z,
  var failOnUnsatPreconditions: B,
  var profile: TempControlPeriodic_p_tcproc_tempControl_Profile_P_Trait,
  var genReplay: (Container, String, GumboXResult.Type) => Option[String])
  extends UnitTestConfigurationBatch with TempControlPeriodic_p_tcproc_tempControl_GumboX_TestHarness {

  override def test(c: Container): GumboXResult.Type = {
    return testComputeCBV(c.asInstanceOf[TempControlPeriodic_p_tcproc_tempControl_PreState_Container])
  }
}

@record class TempControlPeriodic_p_tcproc_tempControl_ComputewL_UnitTestConfiguration (
  var verbose: B,
  var name: String,
  var description: String,
  var numTests: Z,
  var numTestVectorGenRetries: Z,
  var failOnUnsatPreconditions: B,
  var profile: TempControlPeriodic_p_tcproc_tempControl_Profile_PS_Trait,
  var genReplay: (Container, String, GumboXResult.Type) => Option[String])
  extends UnitTestConfigurationBatch with TempControlPeriodic_p_tcproc_tempControl_GumboX_TestHarness {

  override def test(c: Container): GumboXResult.Type = {
    return testComputeCBwLV(c.asInstanceOf[TempControlPeriodic_p_tcproc_tempControl_PreState_Container_PS])
  }
}