Harness.hs

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE OverloadedLabels #-}
-- @generated by keiro-dsl 0.8.0.0 (language keiro-dsl 4) from aggregate Surge; do not edit.
module SkelProcess.Generated.MyService.Surge.Harness (harnessAssertions) where

import SkelProcess.Generated.MyService.Surge.Domain
import SkelProcess.Generated.MyService.Surge.Codec (encodeSurgeEvent, parseSurgeEvent, surgeCodec)
import SkelProcess.Generated.MyService.Surge.Transducer (surgeTransducer)
import Keiki.Core (applyEventsEither, defaultValidationOptions, step, validateTransducer)
import Keiro.Codec (eventType)
import SkelProcess.Generated.MyService.Nominals (HospitalId, parseHospitalId)

-- | (label, passed). A driver runs these and exits non-zero on any False,
-- naming the failing assertion. Filling a hole wrongly turns a specific
-- entry False; the scaffold cannot.
harnessAssertions :: [(String, Bool)]
harnessAssertions =
  [ ("validateTransducer is empty", null (validateTransducer defaultValidationOptions surgeTransducer))
  , ("clock-free: spec samples no wall clock", True)
  , ("golden round-trip: SurgeThresholdNoted", roundTrips sampleEventSurgeThresholdNoted)
  , ("golden round-trip: SurgeTimerMarked", roundTrips sampleEventSurgeTimerMarked)
  , ("accepts NoteSurgeThreshold from SurgeIdle", acceptNoteSurgeThreshold)
  , ("accepts MarkSurgeTimerFired from SurgeIdle", acceptMarkSurgeTimerFired)
  ]
  ++ forwardReplayNoteSurgeThreshold
  ++ forwardReplayMarkSurgeTimerFired

roundTrips :: SurgeEvent -> Bool
roundTrips e = parseSurgeEvent (eventType surgeCodec e) (encodeSurgeEvent e) == Right e

sampleEventSurgeThresholdNoted :: SurgeEvent
sampleEventSurgeThresholdNoted = (SurgeThresholdNoted (SurgeThresholdNotedData (case parseHospitalId "hosp_01h455vb4pex5vsknk084sn02q" of Right parsed -> parsed; Left _ -> error "generated valid ID sample failed to parse") 0 0 "sample-timerId"))

sampleEventSurgeTimerMarked :: SurgeEvent
sampleEventSurgeTimerMarked = (SurgeTimerMarked (SurgeTimerMarkedData (case parseHospitalId "hosp_01h455vb4pex5vsknk084sn02q" of Right parsed -> parsed; Left _ -> error "generated valid ID sample failed to parse") "sample-timerId"))

acceptNoteSurgeThreshold :: Bool
acceptNoteSurgeThreshold =
  case step surgeTransducer (SurgeIdle, initialSurgeRegs) ((NoteSurgeThreshold (NoteSurgeThresholdData (case parseHospitalId "hosp_01h455vb4pex5vsknk084sn02q" of Right parsed -> parsed; Left _ -> error "generated valid ID sample failed to parse") 0 0 "sample-timerId"))) of
    Just (v, _, _) -> v == SurgeIdle
    Nothing -> False

acceptMarkSurgeTimerFired :: Bool
acceptMarkSurgeTimerFired =
  case step surgeTransducer (SurgeIdle, initialSurgeRegs) ((MarkSurgeTimerFired (MarkSurgeTimerFiredData (case parseHospitalId "hosp_01h455vb4pex5vsknk084sn02q" of Right parsed -> parsed; Left _ -> error "generated valid ID sample failed to parse") "sample-timerId"))) of
    Just (v, _, _) -> v == SurgeFired
    Nothing -> False

-- forward/replay equality (plan 147): cross the persisted codec boundary,
-- replay the emitted chain, and compare the final vertex and every register.
forwardReplayNoteSurgeThreshold :: [(String, Bool)]
forwardReplayNoteSurgeThreshold =
  case step surgeTransducer (SurgeIdle, initialSurgeRegs) ((NoteSurgeThreshold (NoteSurgeThresholdData (case parseHospitalId "hosp_01h455vb4pex5vsknk084sn02q" of Right parsed -> parsed; Left _ -> error "generated valid ID sample failed to parse") 0 0 "sample-timerId"))) of
    Nothing -> [(prefix <> "forward step accepted", False)]
    Just (forwardVertex, _forwardRegs, emitted) ->
      case mapM (\event -> parseSurgeEvent (eventType surgeCodec event) (encodeSurgeEvent event)) emitted of
        Left _ -> [(prefix <> "emitted chain decodes", False)]
        Right decodedEvents ->
          case applyEventsEither surgeTransducer (SurgeIdle, initialSurgeRegs) decodedEvents of
            Left _ -> [(prefix <> "replay succeeds", False)]
            Right (replayVertex, _replayRegs) ->
              [ (prefix <> "final vertex", replayVertex == forwardVertex)
              ]
  where
    prefix = "forward/replay equality: NoteSurgeThreshold from SurgeIdle -- "

-- forward/replay equality (plan 147): cross the persisted codec boundary,
-- replay the emitted chain, and compare the final vertex and every register.
forwardReplayMarkSurgeTimerFired :: [(String, Bool)]
forwardReplayMarkSurgeTimerFired =
  case step surgeTransducer (SurgeIdle, initialSurgeRegs) ((MarkSurgeTimerFired (MarkSurgeTimerFiredData (case parseHospitalId "hosp_01h455vb4pex5vsknk084sn02q" of Right parsed -> parsed; Left _ -> error "generated valid ID sample failed to parse") "sample-timerId"))) of
    Nothing -> [(prefix <> "forward step accepted", False)]
    Just (forwardVertex, _forwardRegs, emitted) ->
      case mapM (\event -> parseSurgeEvent (eventType surgeCodec event) (encodeSurgeEvent event)) emitted of
        Left _ -> [(prefix <> "emitted chain decodes", False)]
        Right decodedEvents ->
          case applyEventsEither surgeTransducer (SurgeIdle, initialSurgeRegs) decodedEvents of
            Left _ -> [(prefix <> "replay succeeds", False)]
            Right (replayVertex, _replayRegs) ->
              [ (prefix <> "final vertex", replayVertex == forwardVertex)
              ]
  where
    prefix = "forward/replay equality: MarkSurgeTimerFired from SurgeIdle -- "