TempSensorPeriodic_p_tcproc_tempSensor_UnitTestConfiguration_Util.scala

// #Sireum

package tc.TempSensor

// 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 TempSensorPeriodic_p_tcproc_tempSensor_UnitTestConfiguration_Util {

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

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

  type DefaultInitializeProfile = TempSensorPeriodic_p_tcproc_tempSensor_Profile

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

  type DefaultComputeProfile = TempSensorPeriodic_p_tcproc_tempSensor_Profile_P

  def defaultComputeConfig: TempSensorPeriodic_p_tcproc_tempSensor_Compute_UnitTestConfiguration = {
    return (TempSensorPeriodic_p_tcproc_tempSensor_Compute_UnitTestConfiguration (
      verbose = F,
      name = "Default_Compute_Config",
      description = "Default Compute Configuration",
      numTests = 100,
      numTestVectorGenRetries = 100,
      failOnUnsatPreconditions = F,
      profile = TempSensorPeriodic_p_tcproc_tempSensor_Profile_P (
        name = "Compute_Default_Profile",
      ),
      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.toTempSensorTempSensorPeriodic_p_tcproc_tempSensor_PreState_Container_P(json).left
            |    assert (testComputeCBV(testVector) == results)
            |  }""".render))
    )
  }
}

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

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

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

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