module arch.node.engines.verification;

import prelude open;
import arch.node.types.engine open;

import arch.node.engines.verification_config open public;
import arch.node.engines.verification_messages open public;
import arch.node.engines.verification_environment open public;
import arch.node.engines.verification_behaviour open public;

import arch.node.types.anoma as Anoma open;

open verification_config_example;
open verification_environment_example;

VerificationEngine : Type :=
  Engine
    VerificationCfg
    VerificationLocalState
    VerificationMailboxState
    VerificationTimerHandle
    VerificationActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

exampleVerificationEngine : VerificationEngine :=
  mkEngine@{
    cfg := verificationCfg;
    env := verificationEnv;
    behaviour := verificationBehaviour;
  };