Harness.hs

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE OverloadedLabels #-}
-- @generated by keiro-dsl; do not edit. Regenerated from the .keiro spec.
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.MyService.Surge.Holes (surgeTransducer)
import Keiki.Core (applyEventsEither, defaultValidationOptions, step, validateTransducer)
import Keiro.Codec (eventType)
import SkelProcess.Generated.MyService.Nominals (HospitalId (..))

{- | (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 (HospitalId "sample") 0 0 "sample-timerId"))

sampleEventSurgeTimerMarked :: SurgeEvent
sampleEventSurgeTimerMarked = (SurgeTimerMarked (SurgeTimerMarkedData (HospitalId "sample") "sample-timerId"))

acceptNoteSurgeThreshold :: Bool
acceptNoteSurgeThreshold =
  case step surgeTransducer (SurgeIdle, initialSurgeRegs) ((NoteSurgeThreshold (NoteSurgeThresholdData (HospitalId "sample") 0 0 "sample-timerId"))) of
    Just (v, _, _) -> v == SurgeIdle
    Nothing -> False

acceptMarkSurgeTimerFired :: Bool
acceptMarkSurgeTimerFired =
  case step surgeTransducer (SurgeIdle, initialSurgeRegs) ((MarkSurgeTimerFired (MarkSurgeTimerFiredData (HospitalId "sample") "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 (HospitalId "sample") 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 (HospitalId "sample") "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 -- "