packages feed

keiro-dsl-0.17.0.0: test/conformance-process-timers/Generated/ProcessTimers/Incident/Transducer.hs

{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE QualifiedDo #-}
-- @generated by keiro-dsl 0.17.0.0 (language keiro-dsl 6) from aggregate Incident; do not edit.
module Generated.ProcessTimers.Incident.Transducer
  ( incidentTransducer
  , incidentFoldFingerprint
  , BehaviorOwnership (..)
  , incidentPredicateVerifications
  ) where

import Generated.ProcessTimers.Incident.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

incidentTransducer
  :: SymTransducer
       (HsPred IncidentRegs IncidentCommand)
       IncidentRegs
       IncidentVertex
       IncidentCommand
       IncidentEvent
incidentTransducer =
  B.buildTransducer IncidentOpen initialIncidentRegs isTerminal do
    B.from IncidentOpen do
      B.onCmd inCtorEscalateIncident $ \d -> B.do
        B.emit wireIncidentEscalated (IncidentEscalatedTermFields
          { incidentId = d.incidentId
          })
        B.goto IncidentEscalatedState
      B.onCmd inCtorRemindIncident $ \d -> B.do
        B.emit wireIncidentReminded (IncidentRemindedTermFields
          { incidentId = d.incidentId
          })
        B.goto IncidentOpen
 where
  isTerminal = \case

    _ -> False

incidentFoldFingerprint :: Text
incidentFoldFingerprint = "02e08b4a7c1ca3151b93124ec044b785"

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.
incidentPredicateVerifications :: IO [(Text, BehaviorOwnership, S.PredicateVerification)]
incidentPredicateVerifications = sequence
  [ verifyTransition "transition1OpenEscalateIncident" GeneratedOwned IncidentOpen 0
  , verifyTransition "transition2OpenRemindIncident" GeneratedOwned IncidentOpen 1
  ]
 where
  verifyTransition label owner source edgeIndex =
    case drop edgeIndex (K.edgesOut incidentTransducer source) of
      K.Edge predicate _ _ _ _ : _ -> (\result -> (label, owner, result)) <$> S.verifyPredicate predicate
      [] -> pure (label, owner, S.UnverifiedSolverFailure "generated transition edge missing")