Transducer.hs

{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE OverloadedRecordDot #-}
{-# LANGUAGE QualifiedDo #-}
-- @generated by keiro-dsl 0.9.0.0 (language keiro-dsl 4) from aggregate Surge; do not edit.
module SkelProcess.Generated.MyService.Surge.Transducer
  ( surgeTransducer
  , surgeFoldFingerprint
  , BehaviorOwnership (..)
  , surgePredicateVerifications
  ) where

import SkelProcess.Generated.MyService.Surge.Domain
import Data.Text (Text)
import Keiki.Builder qualified as B
import Keiki.Core (HsPred, SymTransducer)
import Keiki.Core qualified as K
import Keiki.Symbolic qualified as S

surgeTransducer
  :: SymTransducer
       (HsPred SurgeRegs SurgeCommand)
       SurgeRegs
       SurgeVertex
       SurgeCommand
       SurgeEvent
surgeTransducer =
  B.buildTransducer SurgeIdle initialSurgeRegs isTerminal do
    B.from SurgeIdle do
      B.onCmd inCtorNoteSurgeThreshold $ \d -> B.do
        B.emit wireSurgeThresholdNoted (SurgeThresholdNotedTermFields
          { hospitalId = d.hospitalId
          , availableIcuBeds = d.availableIcuBeds
          , redDemand = d.redDemand
          , timerId = d.timerId
          })
        B.goto SurgeIdle
      B.onCmd inCtorMarkSurgeTimerFired $ \d -> B.do
        B.emit wireSurgeTimerMarked (SurgeTimerMarkedTermFields
          { hospitalId = d.hospitalId
          , timerId = d.timerId
          })
        B.goto SurgeFired
 where
  isTerminal = \case
    SurgeFired -> True
    _ -> False

surgeFoldFingerprint :: Text
surgeFoldFingerprint = "d84ee3eac65a407f23e4a4443cafab93"

data BehaviorOwnership = GeneratedOwned | HoleOwned
  deriving stock (Eq, Show)

-- Every checked transition predicate is audited through Keiki's conservative
-- symbolic verifier. Opaque Hole terms remain explicitly unverified.
surgePredicateVerifications :: IO [(Text, BehaviorOwnership, S.PredicateVerification)]
surgePredicateVerifications = sequence
  [ verifyTransition "transition1IdleNoteSurgeThreshold" GeneratedOwned SurgeIdle 0
  , verifyTransition "transition2IdleMarkSurgeTimerFired" GeneratedOwned SurgeIdle 1
  ]
 where
  verifyTransition label owner source edgeIndex =
    case drop edgeIndex (K.edgesOut surgeTransducer source) of
      K.Edge predicate _ _ _ _ : _ -> (\result -> (label, owner, result)) <$> S.verifyPredicate predicate
      [] -> pure (label, owner, S.UnverifiedSolverFailure "generated transition edge missing")