Test your AI Agents with the all-new Agent to Agent Testing Platform.Learn More

How to use ReceiveEventAsync method of Microsoft.Coyote.Actors.EventQueue class

Best Coyote code snippet using Microsoft.Coyote.Actors.EventQueue.ReceiveEventAsync

ActorExecutionContext.cs

Source:ActorExecutionContext.cs

...456        internal virtual void LogHandleRaisedEvent(Actor actor, Event e)457        {458        }459        /// <summary>460        /// Logs that the specified actor called <see cref="Actor.ReceiveEventAsync(Type[])"/>461        /// or one of its overloaded methods.462        /// </summary>463        [MethodImpl(MethodImplOptions.AggressiveInlining)]464        internal virtual void LogReceiveCalled(Actor actor)465        {466        }467        /// <summary>468        /// Logs that the specified actor enqueued an event that it was waiting to receive.469        /// </summary>470        internal virtual void LogReceivedEvent(Actor actor, Event e, EventInfo eventInfo)471        {472            if (this.Configuration.IsVerbose)473            {474                string stateName = actor is StateMachine stateMachine ? stateMachine.CurrentStateName : default;475                this.LogWriter.LogReceiveEvent(actor.Id, stateName, e, wasBlocked: true);476            }477        }478        /// <summary>479        /// Logs that the specified actor received an event without waiting because the event480        /// was already in the inbox when the actor invoked the receive statement.481        /// </summary>482        internal virtual void LogReceivedEventWithoutWaiting(Actor actor, Event e, EventInfo eventInfo)483        {484            if (this.Configuration.IsVerbose)485            {486                string stateName = actor is StateMachine stateMachine ? stateMachine.CurrentStateName : default;487                this.LogWriter.LogReceiveEvent(actor.Id, stateName, e, wasBlocked: false);488            }489        }490        /// <summary>491        /// Logs that the specified actor is waiting to receive an event of one of the specified types.492        /// </summary>493        internal virtual void LogWaitEvent(Actor actor, IEnumerable<Type> eventTypes)494        {495            if (this.Configuration.IsVerbose)496            {497                string stateName = actor is StateMachine stateMachine ? stateMachine.CurrentStateName : default;498                var eventWaitTypesArray = eventTypes.ToArray();499                if (eventWaitTypesArray.Length is 1)500                {501                    this.LogWriter.LogWaitEvent(actor.Id, stateName, eventWaitTypesArray[0]);502                }503                else504                {505                    this.LogWriter.LogWaitEvent(actor.Id, stateName, eventWaitTypesArray);506                }507            }508        }509        /// <summary>510        /// Logs that the specified state machine entered a state.511        /// </summary>512        internal virtual void LogEnteredState(StateMachine stateMachine)513        {514            if (this.Configuration.IsVerbose)515            {516                this.LogWriter.LogStateTransition(stateMachine.Id, stateMachine.CurrentStateName, isEntry: true);517            }518        }519        /// <summary>520        /// Logs that the specified state machine exited a state.521        /// </summary>522        internal virtual void LogExitedState(StateMachine stateMachine)523        {524            if (this.Configuration.IsVerbose)525            {526                this.LogWriter.LogStateTransition(stateMachine.Id, stateMachine.CurrentStateName, isEntry: false);527            }528        }529        /// <summary>530        /// Logs that the specified state machine invoked pop.531        /// </summary>532        [MethodImpl(MethodImplOptions.AggressiveInlining)]533        internal virtual void LogPopState(StateMachine stateMachine)534        {535        }536        /// <summary>537        /// Logs that the specified state machine invoked an action.538        /// </summary>539        internal virtual void LogInvokedOnEntryAction(StateMachine stateMachine, MethodInfo action)540        {541            if (this.Configuration.IsVerbose)542            {543                this.LogWriter.LogExecuteAction(stateMachine.Id, stateMachine.CurrentStateName,544                    stateMachine.CurrentStateName, action.Name);545            }546        }547        /// <summary>548        /// Logs that the specified state machine invoked an action.549        /// </summary>550        internal virtual void LogInvokedOnExitAction(StateMachine stateMachine, MethodInfo action)551        {552            if (this.Configuration.IsVerbose)553            {554                this.LogWriter.LogExecuteAction(stateMachine.Id, stateMachine.CurrentStateName,555                    stateMachine.CurrentStateName, action.Name);556            }557        }558        /// <summary>559        /// Builds the coverage graph information, if any. This information is only available560        /// when <see cref="Configuration.ReportActivityCoverage"/> is enabled.561        /// </summary>562        internal CoverageInfo BuildCoverageInfo()563        {564            var result = this.CoverageInfo;565            if (result != null)566            {567                var builder = this.LogWriter.GetLogsOfType<ActorRuntimeLogGraphBuilder>().FirstOrDefault();568                if (builder != null)569                {570                    result.CoverageGraph = builder.SnapshotGraph(this.Configuration.IsDgmlBugGraph);571                }572                var eventCoverage = this.LogWriter.GetLogsOfType<ActorRuntimeLogEventCoverage>().FirstOrDefault();573                if (eventCoverage != null)574                {575                    result.EventInfo = eventCoverage.EventCoverage;576                }577            }578            return result;579        }580        /// <summary>581        /// Returns the current hashed state of the actors.582        /// </summary>583        /// <remarks>584        /// The hash is updated in each execution step.585        /// </remarks>586        internal virtual int GetHashedActorState() => 0;587        /// <summary>588        /// Returns the program counter of the specified actor.589        /// </summary>590        [MethodImpl(MethodImplOptions.AggressiveInlining)]591        internal virtual int GetActorProgramCounter(ActorId actorId) => 0;592        /// <inheritdoc/>593        public void RegisterMonitor<T>()594            where T : Monitor =>595            this.TryCreateMonitor(typeof(T));596        /// <inheritdoc/>597        public void Monitor<T>(Event e)598            where T : Monitor599        {600            // If the event is null then report an error and exit.601            this.Assert(e != null, "Cannot monitor a null event.");602            this.InvokeMonitor(typeof(T), e, null, null, null);603        }604        /// <summary>605        /// Tries to create a new <see cref="Specifications.Monitor"/> of the specified <see cref="Type"/>.606        /// </summary>607        protected bool TryCreateMonitor(Type type) => this.SpecificationEngine.TryCreateMonitor(608            type, this.CoverageInfo, this.LogWriter);609        /// <summary>610        /// Invokes the specified <see cref="Specifications.Monitor"/> with the specified <see cref="Event"/>.611        /// </summary>612        internal void InvokeMonitor(Type type, Event e, string senderName, string senderType, string senderStateName) =>613            this.SpecificationEngine.InvokeMonitor(type, e, senderName, senderType, senderStateName);614        /// <inheritdoc/>615        [MethodImpl(MethodImplOptions.AggressiveInlining)]616        public void Assert(bool predicate) => this.SpecificationEngine.Assert(predicate);617        /// <inheritdoc/>618        [MethodImpl(MethodImplOptions.AggressiveInlining)]619        public void Assert(bool predicate, string s, object arg0) => this.SpecificationEngine.Assert(predicate, s, arg0);620        /// <inheritdoc/>621        [MethodImpl(MethodImplOptions.AggressiveInlining)]622        public void Assert(bool predicate, string s, object arg0, object arg1) => this.SpecificationEngine.Assert(predicate, s, arg0, arg1);623        /// <inheritdoc/>624        [MethodImpl(MethodImplOptions.AggressiveInlining)]625        public void Assert(bool predicate, string s, object arg0, object arg1, object arg2) =>626            this.SpecificationEngine.Assert(predicate, s, arg0, arg1, arg2);627        /// <inheritdoc/>628        [MethodImpl(MethodImplOptions.AggressiveInlining)]629        public void Assert(bool predicate, string s, params object[] args) => this.SpecificationEngine.Assert(predicate, s, args);630        /// <summary>631        /// Asserts that the actor calling an actor method is also the actor that is currently executing.632        /// </summary>633        [MethodImpl(MethodImplOptions.AggressiveInlining)]634        internal virtual void AssertExpectedCallerActor(Actor caller, string calledAPI)635        {636        }637        /// <summary>638        /// Raises the <see cref="OnFailure"/> event with the specified <see cref="Exception"/>.639        /// </summary>640        internal void RaiseOnFailureEvent(Exception exception) => this.Runtime.RaiseOnFailureEvent(exception);641        /// <summary>642        /// Handle the specified dropped <see cref="Event"/>.643        /// </summary>644        internal void HandleDroppedEvent(Event e, ActorId id) => this.OnEventDropped?.Invoke(e, id);645        /// <summary>646        /// Throws an <see cref="AssertionFailureException"/> exception containing the specified exception.647        /// </summary>648#if !DEBUG649        [DebuggerHidden]650#endif651        internal void WrapAndThrowException(Exception exception, string s, params object[] args) =>652            this.SpecificationEngine.WrapAndThrowException(exception, s, args);653        /// <inheritdoc/>654        [Obsolete("Please set the Logger property directory instead of calling this method.")]655        public TextWriter SetLogger(TextWriter logger)656        {657            var result = this.LogWriter.SetLogger(new TextWriterLogger(logger));658            if (result != null)659            {660                return result.TextWriter;661            }662            return null;663        }664        /// <inheritdoc/>665        public void RegisterLog(IActorRuntimeLog log) => this.LogWriter.RegisterLog(log);666        /// <inheritdoc/>667        public void RemoveLog(IActorRuntimeLog log) => this.LogWriter.RemoveLog(log);668        /// <inheritdoc/>669        public void Stop() => this.Scheduler.ForceStop();670        /// <summary>671        /// Disposes runtime resources.672        /// </summary>673        protected virtual void Dispose(bool disposing)674        {675            if (disposing)676            {677                this.ActorMap.Clear();678            }679        }680        /// <inheritdoc/>681        public void Dispose()682        {683            this.Dispose(true);684            GC.SuppressFinalize(this);685        }686        /// <summary>687        /// The mocked execution context of an actor program.688        /// </summary>689        internal sealed class Mock : ActorExecutionContext690        {691            /// <summary>692            /// Map that stores all unique names and their corresponding actor ids.693            /// </summary>694            private readonly ConcurrentDictionary<string, ActorId> NameValueToActorId;695            /// <summary>696            /// Map of program counters used for state-caching to distinguish697            /// scheduling from non-deterministic choices.698            /// </summary>699            private readonly ConcurrentDictionary<ActorId, int> ProgramCounterMap;700            /// <summary>701            /// If true, the actor execution is controlled, else false.702            /// </summary>703            internal override bool IsExecutionControlled => true;704            /// <summary>705            /// Initializes a new instance of the <see cref="Mock"/> class.706            /// </summary>707            internal Mock(Configuration configuration, CoyoteRuntime runtime, OperationScheduler scheduler,708                SpecificationEngine specificationEngine, IRandomValueGenerator valueGenerator, LogWriter logWriter)709                : base(configuration, runtime, scheduler, specificationEngine, valueGenerator, logWriter)710            {711                this.NameValueToActorId = new ConcurrentDictionary<string, ActorId>();712                this.ProgramCounterMap = new ConcurrentDictionary<ActorId, int>();713            }714            /// <inheritdoc/>715            public override ActorId CreateActorIdFromName(Type type, string name)716            {717                // It is important that all actor ids use the monotonically incrementing718                // value as the id during testing, and not the unique name.719                return this.NameValueToActorId.GetOrAdd(name, key => this.CreateActorId(type, key));720            }721            /// <inheritdoc/>722            public override ActorId CreateActor(Type type, Event initialEvent = null, EventGroup eventGroup = null) =>723                this.CreateActor(null, type, null, initialEvent, eventGroup);724            /// <inheritdoc/>725            public override ActorId CreateActor(Type type, string name, Event initialEvent = null, EventGroup eventGroup = null) =>726                this.CreateActor(null, type, name, initialEvent, eventGroup);727            /// <inheritdoc/>728            public override ActorId CreateActor(ActorId id, Type type, Event initialEvent = null, EventGroup eventGroup = null)729            {730                this.Assert(id != null, "Cannot create an actor using a null actor id.");731                return this.CreateActor(id, type, null, initialEvent, eventGroup);732            }733            /// <inheritdoc/>734            public override Task<ActorId> CreateActorAndExecuteAsync(Type type, Event initialEvent = null, EventGroup eventGroup = null) =>735                this.CreateActorAndExecuteAsync(null, type, null, initialEvent, eventGroup);736            /// <inheritdoc/>737            public override Task<ActorId> CreateActorAndExecuteAsync(Type type, string name, Event initialEvent = null, EventGroup eventGroup = null) =>738                this.CreateActorAndExecuteAsync(null, type, name, initialEvent, eventGroup);739            /// <inheritdoc/>740            public override Task<ActorId> CreateActorAndExecuteAsync(ActorId id, Type type, Event initialEvent = null, EventGroup eventGroup = null)741            {742                this.Assert(id != null, "Cannot create an actor using a null actor id.");743                return this.CreateActorAndExecuteAsync(id, type, null, initialEvent, eventGroup);744            }745            /// <summary>746            /// Creates a new actor of the specified <see cref="Type"/> and name, using the specified747            /// unbound actor id, and passes the specified optional <see cref="Event"/>. This event748            /// can only be used to access its payload, and cannot be handled.749            /// </summary>750            internal ActorId CreateActor(ActorId id, Type type, string name, Event initialEvent = null, EventGroup eventGroup = null)751            {752                var creatorOp = this.Scheduler.GetExecutingOperation<ActorOperation>();753                return this.CreateActor(id, type, name, initialEvent, creatorOp?.Actor, eventGroup);754            }755            /// <summary>756            /// Creates a new <see cref="Actor"/> of the specified <see cref="Type"/>.757            /// </summary>758            internal override ActorId CreateActor(ActorId id, Type type, string name, Event initialEvent, Actor creator, EventGroup eventGroup)759            {760                this.AssertExpectedCallerActor(creator, "CreateActor");761                Actor actor = this.CreateActor(id, type, name, creator, eventGroup);762                this.RunActorEventHandler(actor, initialEvent, true, null);763                return actor.Id;764            }765            /// <summary>766            /// Creates a new actor of the specified <see cref="Type"/> and name, using the specified767            /// unbound actor id, and passes the specified optional <see cref="Event"/>. This event768            /// can only be used to access its payload, and cannot be handled. The method returns only769            /// when the actor is initialized and the <see cref="Event"/> (if any) is handled.770            /// </summary>771            internal Task<ActorId> CreateActorAndExecuteAsync(ActorId id, Type type, string name, Event initialEvent = null,772                EventGroup eventGroup = null)773            {774                var creatorOp = this.Scheduler.GetExecutingOperation<ActorOperation>();775                return this.CreateActorAndExecuteAsync(id, type, name, initialEvent, creatorOp?.Actor, eventGroup);776            }777            /// <summary>778            /// Creates a new <see cref="Actor"/> of the specified <see cref="Type"/>. The method779            /// returns only when the actor is initialized and the <see cref="Event"/> (if any)780            /// is handled.781            /// </summary>782            internal override async Task<ActorId> CreateActorAndExecuteAsync(ActorId id, Type type, string name, Event initialEvent,783                Actor creator, EventGroup eventGroup)784            {785                this.AssertExpectedCallerActor(creator, "CreateActorAndExecuteAsync");786                this.Assert(creator != null, "Only an actor can call 'CreateActorAndExecuteAsync': avoid calling " +787                    "it directly from the test method; instead call it through a test driver actor.");788                Actor actor = this.CreateActor(id, type, name, creator, eventGroup);789                this.RunActorEventHandler(actor, initialEvent, true, creator);790                // Wait until the actor reaches quiescence.791                await creator.ReceiveEventAsync(typeof(QuiescentEvent), rev => (rev as QuiescentEvent).ActorId == actor.Id);792                return await Task.FromResult(actor.Id);793            }794            /// <summary>795            /// Creates a new <see cref="Actor"/> of the specified <see cref="Type"/>.796            /// </summary>797            internal override Actor CreateActor(ActorId id, Type type, string name, Actor creator, EventGroup eventGroup)798            {799                this.Assert(type.IsSubclassOf(typeof(Actor)), "Type '{0}' is not an actor.", type.FullName);800                // Using ulong.MaxValue because a Create operation cannot specify801                // the id of its target, because the id does not exist yet.802                this.Scheduler.ScheduleNextOperation(AsyncOperationType.Create);803                this.ResetProgramCounter(creator);804                if (id is null)805                {806                    id = this.CreateActorId(type, name);807                }808                else809                {810                    this.Assert(id.Runtime is null || id.Runtime == this, "Unbound actor id '{0}' was created by another runtime.", id.Value);811                    this.Assert(id.Type == type.FullName, "Cannot bind actor id '{0}' of type '{1}' to an actor of type '{2}'.",812                        id.Value, id.Type, type.FullName);813                    id.Bind(this);814                }815                // If a group was not provided, inherit the current event group from the creator (if any).816                if (eventGroup is null && creator != null)817                {818                    eventGroup = creator.EventGroup;819                }820                Actor actor = ActorFactory.Create(type);821                ActorOperation op = new ActorOperation(id.Value, id.Name, actor, this.Scheduler);822                IEventQueue eventQueue = new MockEventQueue(actor);823                actor.Configure(this, id, op, eventQueue, eventGroup);824                actor.SetupEventHandlers();825                if (this.Configuration.ReportActivityCoverage)826                {827                    actor.ReportActivityCoverage(this.CoverageInfo);828                }829                bool result = this.Scheduler.RegisterOperation(op);830                this.Assert(result, "Actor id '{0}' is used by an existing or previously halted actor.", id.Value);831                if (actor is StateMachine)832                {833                    this.LogWriter.LogCreateStateMachine(id, creator?.Id.Name, creator?.Id.Type);834                }835                else836                {837                    this.LogWriter.LogCreateActor(id, creator?.Id.Name, creator?.Id.Type);838                }839                return actor;840            }841            /// <inheritdoc/>842            public override void SendEvent(ActorId targetId, Event initialEvent, EventGroup eventGroup = default, SendOptions options = null)843            {844                var senderOp = this.Scheduler.GetExecutingOperation<ActorOperation>();845                this.SendEvent(targetId, initialEvent, senderOp?.Actor, eventGroup, options);846            }847            /// <inheritdoc/>848            public override Task<bool> SendEventAndExecuteAsync(ActorId targetId, Event initialEvent,849                EventGroup eventGroup = null, SendOptions options = null)850            {851                var senderOp = this.Scheduler.GetExecutingOperation<ActorOperation>();852                return this.SendEventAndExecuteAsync(targetId, initialEvent, senderOp?.Actor, eventGroup, options);853            }854            /// <summary>855            /// Sends an asynchronous <see cref="Event"/> to an actor.856            /// </summary>857            internal override void SendEvent(ActorId targetId, Event e, Actor sender, EventGroup eventGroup, SendOptions options)858            {859                if (e is null)860                {861                    string message = sender != null ?862                        string.Format("{0} is sending a null event.", sender.Id.ToString()) :863                        "Cannot send a null event.";864                    this.Assert(false, message);865                }866                if (sender != null)867                {868                    this.Assert(targetId != null, "{0} is sending event {1} to a null actor.", sender.Id, e);869                }870                else871                {872                    this.Assert(targetId != null, "Cannot send event {1} to a null actor.", e);873                }874                this.AssertExpectedCallerActor(sender, "SendEvent");875                EnqueueStatus enqueueStatus = this.EnqueueEvent(targetId, e, sender, eventGroup, options, out Actor target);876                if (enqueueStatus is EnqueueStatus.EventHandlerNotRunning)877                {878                    this.RunActorEventHandler(target, null, false, null);879                }880            }881            /// <summary>882            /// Sends an asynchronous <see cref="Event"/> to an actor. Returns immediately if the target was883            /// already running. Otherwise blocks until the target handles the event and reaches quiescense.884            /// </summary>885            internal override async Task<bool> SendEventAndExecuteAsync(ActorId targetId, Event e, Actor sender,886                EventGroup eventGroup, SendOptions options)887            {888                this.Assert(sender is StateMachine, "Only an actor can call 'SendEventAndExecuteAsync': avoid " +889                    "calling it directly from the test method; instead call it through a test driver actor.");890                this.Assert(e != null, "{0} is sending a null event.", sender.Id);891                this.Assert(targetId != null, "{0} is sending event {1} to a null actor.", sender.Id, e);892                this.AssertExpectedCallerActor(sender, "SendEventAndExecuteAsync");893                EnqueueStatus enqueueStatus = this.EnqueueEvent(targetId, e, sender, eventGroup, options, out Actor target);894                if (enqueueStatus is EnqueueStatus.EventHandlerNotRunning)895                {896                    this.RunActorEventHandler(target, null, false, sender as StateMachine);897                    // Wait until the actor reaches quiescence.898                    await (sender as StateMachine).ReceiveEventAsync(typeof(QuiescentEvent), rev => (rev as QuiescentEvent).ActorId == targetId);899                    return true;900                }901                // EnqueueStatus.EventHandlerNotRunning is not returned by EnqueueEvent902                // (even when the actor was previously inactive) when the event e requires903                // no action by the actor (i.e., it implicitly handles the event).904                return enqueueStatus is EnqueueStatus.Dropped || enqueueStatus is EnqueueStatus.NextEventUnavailable;905            }906            /// <summary>907            /// Enqueues an event to the actor with the specified id.908            /// </summary>909            private EnqueueStatus EnqueueEvent(ActorId targetId, Event e, Actor sender, EventGroup eventGroup,910                SendOptions options, out Actor target)911            {912                target = this.Scheduler.GetOperationWithId<ActorOperation>(targetId.Value)?.Actor;913                this.Assert(target != null,914                    "Cannot send event '{0}' to actor id '{1}' that is not bound to an actor instance.",915                    e.GetType().FullName, targetId.Value);916                this.Scheduler.ScheduleNextOperation(AsyncOperationType.Send);917                this.ResetProgramCounter(sender as StateMachine);918                // If no group is provided we default to passing along the group from the sender.919                if (eventGroup is null && sender != null)920                {921                    eventGroup = sender.EventGroup;922                }923                if (target.IsHalted)924                {925                    Guid groupId = eventGroup is null ? Guid.Empty : eventGroup.Id;926                    this.LogWriter.LogSendEvent(targetId, sender?.Id.Name, sender?.Id.Type,927                        (sender as StateMachine)?.CurrentStateName ?? default, e, groupId, isTargetHalted: true);928                    this.Assert(options is null || !options.MustHandle,929                        "A must-handle event '{0}' was sent to {1} which has halted.", e.GetType().FullName, targetId);930                    this.HandleDroppedEvent(e, targetId);931                    return EnqueueStatus.Dropped;932                }933                EnqueueStatus enqueueStatus = this.EnqueueEvent(target, e, sender, eventGroup, options);934                if (enqueueStatus == EnqueueStatus.Dropped)935                {936                    this.HandleDroppedEvent(e, targetId);937                }938                return enqueueStatus;939            }940            /// <summary>941            /// Enqueues an event to the actor with the specified id.942            /// </summary>943            private EnqueueStatus EnqueueEvent(Actor actor, Event e, Actor sender, EventGroup eventGroup, SendOptions options)944            {945                EventOriginInfo originInfo;946                string stateName = null;947                if (sender is StateMachine senderStateMachine)948                {949                    originInfo = new EventOriginInfo(sender.Id, senderStateMachine.GetType().FullName,950                        NameResolver.GetStateNameForLogging(senderStateMachine.CurrentState));951                    stateName = senderStateMachine.CurrentStateName;952                }953                else if (sender is Actor senderActor)954                {955                    originInfo = new EventOriginInfo(sender.Id, senderActor.GetType().FullName, string.Empty);956                }957                else958                {959                    // Message comes from the environment.960                    originInfo = new EventOriginInfo(null, "Env", "Env");961                }962                EventInfo eventInfo = new EventInfo(e, originInfo)963                {964                    MustHandle = options?.MustHandle ?? false,965                    Assert = options?.Assert ?? -1966                };967                Guid opId = eventGroup is null ? Guid.Empty : eventGroup.Id;968                this.LogWriter.LogSendEvent(actor.Id, sender?.Id.Name, sender?.Id.Type, stateName,969                    e, opId, isTargetHalted: false);970                return actor.Enqueue(e, eventGroup, eventInfo);971            }972            /// <summary>973            /// Runs a new asynchronous event handler for the specified actor.974            /// This is a fire and forget invocation.975            /// </summary>976            /// <param name="actor">The actor that executes this event handler.</param>977            /// <param name="initialEvent">Optional event for initializing the actor.</param>978            /// <param name="isFresh">If true, then this is a new actor.</param>979            /// <param name="syncCaller">Caller actor that is blocked for quiscence.</param>980            private void RunActorEventHandler(Actor actor, Event initialEvent, bool isFresh, Actor syncCaller)981            {982                var op = actor.Operation;983                Task task = new Task(async () =>984                {985                    try986                    {987                        // Update the current asynchronous control flow with this runtime instance,988                        // allowing future retrieval in the same asynchronous call stack.989                        CoyoteRuntime.AssignAsyncControlFlowRuntime(this.Runtime);990                        this.Scheduler.StartOperation(op);991                        if (isFresh)992                        {993                            await actor.InitializeAsync(initialEvent);994                        }995                        await actor.RunEventHandlerAsync();996                        if (syncCaller != null)997                        {998                            this.EnqueueEvent(syncCaller, new QuiescentEvent(actor.Id), actor, actor.CurrentEventGroup, null);999                        }1000                        if (!actor.IsHalted)1001                        {1002                            this.ResetProgramCounter(actor);1003                        }1004                        IODebug.WriteLine("<ScheduleDebug> Completed operation {0} on task '{1}'.", actor.Id, Task.CurrentId);1005                        op.OnCompleted();1006                        // The actor is inactive or halted, schedule the next enabled operation.1007                        this.Scheduler.ScheduleNextOperation(AsyncOperationType.Stop);1008                    }1009                    catch (Exception ex)1010                    {1011                        this.ProcessUnhandledExceptionInOperation(op, ex);1012                    }1013                });1014                task.Start();1015                this.Scheduler.WaitOperationStart(op);1016            }1017            /// <summary>1018            /// Creates a new timer that sends a <see cref="TimerElapsedEvent"/> to its owner actor.1019            /// </summary>1020            internal override IActorTimer CreateActorTimer(TimerInfo info, Actor owner)1021            {1022                var id = this.CreateActorId(typeof(MockStateMachineTimer));1023                this.CreateActor(id, typeof(MockStateMachineTimer), new TimerSetupEvent(info, owner, this.Configuration.TimeoutDelay));1024                return this.Scheduler.GetOperationWithId<ActorOperation>(id.Value).Actor as MockStateMachineTimer;1025            }1026            /// <inheritdoc/>1027            public override EventGroup GetCurrentEventGroup(ActorId currentActorId)1028            {1029                var callerOp = this.Scheduler.GetExecutingOperation<ActorOperation>();1030                this.Assert(callerOp != null && currentActorId == callerOp.Actor.Id,1031                    "Trying to access the event group id of {0}, which is not the currently executing actor.",1032                    currentActorId);1033                return callerOp.Actor.CurrentEventGroup;1034            }1035            /// <summary>1036            /// Returns a controlled nondeterministic boolean choice.1037            /// </summary>1038            internal override bool GetNondeterministicBooleanChoice(int maxValue, string callerName, string callerType)1039            {1040                var caller = this.Scheduler.GetExecutingOperation<ActorOperation>()?.Actor;1041                if (caller is Actor callerActor)1042                {1043                    this.IncrementActorProgramCounter(callerActor.Id);1044                }1045                var choice = this.Scheduler.GetNextNondeterministicBooleanChoice(maxValue);1046                this.LogWriter.LogRandom(choice, callerName ?? caller?.Id.Name, callerType ?? caller?.Id.Type);1047                return choice;1048            }1049            /// <summary>1050            /// Returns a controlled nondeterministic integer choice.1051            /// </summary>1052            internal override int GetNondeterministicIntegerChoice(int maxValue, string callerName, string callerType)1053            {1054                var caller = this.Scheduler.GetExecutingOperation<ActorOperation>()?.Actor;1055                if (caller is Actor callerActor)1056                {1057                    this.IncrementActorProgramCounter(callerActor.Id);1058                }1059                var choice = this.Scheduler.GetNextNondeterministicIntegerChoice(maxValue);1060                this.LogWriter.LogRandom(choice, callerName ?? caller?.Id.Name, callerType ?? caller?.Id.Type);1061                return choice;1062            }1063            /// <inheritdoc/>1064            internal override void LogInvokedAction(Actor actor, MethodInfo action, string handlingStateName, string currentStateName) =>1065                this.LogWriter.LogExecuteAction(actor.Id, handlingStateName, currentStateName, action.Name);1066            /// <inheritdoc/>1067            [MethodImpl(MethodImplOptions.AggressiveInlining)]1068            internal override void LogEnqueuedEvent(Actor actor, Event e, EventGroup eventGroup, EventInfo eventInfo) =>1069                this.LogWriter.LogEnqueueEvent(actor.Id, e);1070            /// <inheritdoc/>1071            internal override void LogDequeuedEvent(Actor actor, Event e, EventInfo eventInfo, bool isFreshDequeue)1072            {1073                if (!isFreshDequeue)1074                {1075                    // Skip the scheduling point, as this is the first dequeue of the event handler,1076                    // to avoid unecessery context switches.1077                    this.Scheduler.ScheduleNextOperation(AsyncOperationType.Receive);1078                    this.ResetProgramCounter(actor);1079                }1080                string stateName = actor is StateMachine stateMachine ? stateMachine.CurrentStateName : null;1081                this.LogWriter.LogDequeueEvent(actor.Id, stateName, e);1082            }1083            /// <inheritdoc/>1084            internal override void LogDefaultEventDequeued(Actor actor)1085            {1086                this.Scheduler.ScheduleNextOperation(AsyncOperationType.Receive);1087                this.ResetProgramCounter(actor);1088            }1089            /// <inheritdoc/>1090            [MethodImpl(MethodImplOptions.AggressiveInlining)]1091            internal override void LogDefaultEventHandlerCheck(Actor actor) => this.Scheduler.ScheduleNextOperation();1092            /// <inheritdoc/>1093            internal override void LogRaisedEvent(Actor actor, Event e, EventGroup eventGroup, EventInfo eventInfo)1094            {1095                string stateName = actor is StateMachine stateMachine ? stateMachine.CurrentStateName : null;1096                this.LogWriter.LogRaiseEvent(actor.Id, stateName, e);1097            }1098            /// <inheritdoc/>1099            internal override void LogHandleRaisedEvent(Actor actor, Event e)1100            {1101                string stateName = actor is StateMachine stateMachine ? stateMachine.CurrentStateName : null;1102                this.LogWriter.LogHandleRaisedEvent(actor.Id, stateName, e);1103            }1104            /// <inheritdoc/>1105            [MethodImpl(MethodImplOptions.AggressiveInlining)]1106            internal override void LogReceiveCalled(Actor actor) => this.AssertExpectedCallerActor(actor, "ReceiveEventAsync");1107            /// <inheritdoc/>1108            internal override void LogReceivedEvent(Actor actor, Event e, EventInfo eventInfo)1109            {1110                string stateName = actor is StateMachine stateMachine ? stateMachine.CurrentStateName : null;1111                this.LogWriter.LogReceiveEvent(actor.Id, stateName, e, wasBlocked: true);1112            }1113            /// <inheritdoc/>1114            internal override void LogReceivedEventWithoutWaiting(Actor actor, Event e, EventInfo eventInfo)1115            {1116                string stateName = actor is StateMachine stateMachine ? stateMachine.CurrentStateName : null;1117                this.LogWriter.LogReceiveEvent(actor.Id, stateName, e, wasBlocked: false);1118                this.Scheduler.ScheduleNextOperation(AsyncOperationType.Receive);1119                this.ResetProgramCounter(actor);1120            }...

EventQueue.cs

Source:EventQueue.cs

...169            this.RaisedEvent = (e, eventGroup);170            this.OnRaiseEvent(e, eventGroup, null);171        }172        //// <inheritdoc/>173        public Task<Event> ReceiveEventAsync(Type eventType, Func<Event, bool> predicate = null)174        {175            var eventWaitTypes = new Dictionary<Type, Func<Event, bool>>176            {177                { eventType, predicate }178            };179            return this.ReceiveEventAsync(eventWaitTypes);180        }181        /// <inheritdoc/>182        public Task<Event> ReceiveEventAsync(params Type[] eventTypes)183        {184            var eventWaitTypes = new Dictionary<Type, Func<Event, bool>>();185            foreach (var type in eventTypes)186            {187                eventWaitTypes.Add(type, null);188            }189            return this.ReceiveEventAsync(eventWaitTypes);190        }191        /// <inheritdoc/>192        public Task<Event> ReceiveEventAsync(params Tuple<Type, Func<Event, bool>>[] events)193        {194            var eventWaitTypes = new Dictionary<Type, Func<Event, bool>>();195            foreach (var e in events)196            {197                eventWaitTypes.Add(e.Item1, e.Item2);198            }199            return this.ReceiveEventAsync(eventWaitTypes);200        }201        /// <summary>202        /// Waits for an event to be enqueued based on the conditions defined in the event wait types.203        /// </summary>204        private Task<Event> ReceiveEventAsync(Dictionary<Type, Func<Event, bool>> eventWaitTypes)205        {206            (Event e, EventGroup eventGroup) receivedEvent = default;207            lock (this.Queue)208            {209                var node = this.Queue.First;210                while (node != null)211                {212                    // Dequeue the first event that the caller waits to receive, if there is one in the queue.213                    if (eventWaitTypes.TryGetValue(node.Value.e.GetType(), out Func<Event, bool> predicate) &&214                        (predicate is null || predicate(node.Value.e)))215                    {216                        receivedEvent = node.Value;217                        this.Queue.Remove(node);218                        break;...

ReceiveEventAsync

Using AI Code Generation

1using System;2using System.Collections.Generic;3using System.Linq;4using System.Text;5using System.Threading.Tasks;6using Microsoft.Coyote;7using Microsoft.Coyote.Actors;8using Microsoft.Coyote.Specifications;9using Microsoft.Coyote.Tasks;10using Microsoft.Coyote.Actors.Timers;11using Microsoft.Coyote.Actors.Coverage;12using Microsoft.Coyote.Actors.Logging;13using Microsoft.Coyote.Actors.SharedObjects;14using Microsoft.Coyote.Actors.BugFinding;15using Microsoft.Coyote.Actors.BugFinding.Strategies;16using Microsoft.Coyote.Actors.BugFinding.Coverage;17using Microsoft.Coyote.Actors.BugFinding.Scheduling;18using Microsoft.Coyote.Actors.BugFinding.Programs;19using Microsoft.Coyote.Actors.BugFinding.Programs.Schedule;20using Microsoft.Coyote.Actors.BugFinding.Programs.Schedule.Strategies;21using Microsoft.Coyote.Actors.BugFinding.Programs.Schedule.Strategies.Coverage;22using Microsoft.Coyote.Actors.BugFinding.Programs.Schedule.Strategies.Coverage.Programs;23using Microsoft.Coyote.Actors.BugFinding.Programs.Schedule.Strategies.Coverage.Programs.Strategies;24using Microsoft.Coyote.Actors.BugFinding.Programs.Schedule.Strategies.Coverage.Programs.Strategies.Liveness;25using Microsoft.Coyote.Actors.BugFinding.Programs.Schedule.Strategies.Coverage.Programs.Strategies.Liveness.Strategies;26using Microsoft.Coyote.Actors.BugFinding.Programs.Schedule.Strategies.Coverage.Programs.Strategies.Liveness.Strategies.Coverage;27using Microsoft.Coyote.Actors.BugFinding.Programs.Schedule.Strategies.Coverage.Programs.Strategies.Liveness.Strategies.Coverage.Programs;28using Microsoft.Coyote.Actors.BugFinding.Programs.Schedule.Strategies.Coverage.Programs.Strategies.Liveness.Strategies.Coverage.Programs.Strategies;29using Microsoft.Coyote.Actors.BugFinding.Programs.Schedule.Strategies.Coverage.Programs.Strategies.Liveness.Strategies.Coverage.Programs.Strategies.Liveness;30using Microsoft.Coyote.Actors.BugFinding.Programs.Schedule.Strategies.Coverage.Programs.Strategies.Liveness.Strategies.Coverage.Programs.Strategies.Liveness.Strategies;

ReceiveEventAsync

Using AI Code Generation

1using System;2using System.Threading.Tasks;3using Microsoft.Coyote;4using Microsoft.Coyote.Actors;5using Microsoft.Coyote.Runtime;6using Microsoft.Coyote.Tasks;7{8    {9        private static async Task Main(string[] args)10        {11            RuntimeEnvironment.ConfigureEventLogging = true;12            RuntimeEnvironment.IsExecutionControlled = true;13            RuntimeEnvironment.IsMonitoringEnabled = true;14            RuntimeEnvironment.IsTestingEnabled = true;15            RuntimeEnvironment.IsReplayingEnabled = true;16            Configuration configuration = Configuration.Create().WithNumberOfIterations(100);17            await RunAsync(configuration);18        }19        private static async Task RunAsync(Configuration configuration)20        {21            TaskScheduler scheduler = TaskScheduler.Current;22            Task task = new Task(() => { });23            task.Start(scheduler);24            await task;25            ActorRuntime runtime = await RuntimeFactory.CreateAsync(configuration);26            await runtime.CreateActorAndExecuteAsync(typeof(M));27        }28    }29    {30        private TaskCompletionSource<bool> tcs;31        protected override Task OnInitializeAsync(Event initialEvent)32        {33            this.tcs = new TaskCompletionSource<bool>();34            this.SendEvent(this.Id, new E());35            return Task.CompletedTask;36        }37        protected override async Task OnEventAsync(Event e)38        {39            if (e is E)40            {41                {42                    await this.ReceiveEventAsync(typeof(E));43                }44                catch (Exception ex)45                {46                    this.tcs.TrySetResult(true);47                    throw ex;48                }

ReceiveEventAsync

Using AI Code Generation

1using Microsoft.Coyote.Actors;2using Microsoft.Coyote.Actors.Timers;3using System;4using System.Threading.Tasks;5{6    {7        public static async Task Main(string[] args)8        {9            ActorRuntime.RegisterActor(typeof(Actor1));10            ActorRuntime.RegisterActor(typeof(Actor2));11            ActorRuntime.RegisterActor(typeof(Actor3));12            ActorRuntime.RegisterActor(typeof(Actor4));13            ActorRuntime.RegisterActor(typeof(Actor5));14            ActorRuntime.RegisterActor(typeof(Actor6));15            ActorRuntime.RegisterActor(typeof(Actor7));16            ActorRuntime.RegisterActor(typeof(Actor8));17            ActorRuntime.RegisterActor(typeof(Actor9));18            ActorRuntime.RegisterActor(typeof(Actor10));19            ActorRuntime.RegisterActor(typeof(Actor11));20            ActorRuntime.RegisterActor(typeof(Actor12));21            ActorRuntime.RegisterActor(typeof(Actor13));22            ActorRuntime.RegisterActor(typeof(Actor14));23            ActorRuntime.RegisterActor(typeof(Actor15));24            ActorRuntime.RegisterActor(typeof(Actor16));25            ActorRuntime.RegisterActor(typeof(Actor17));26            ActorRuntime.RegisterActor(typeof(Actor18));27            ActorRuntime.RegisterActor(typeof(Actor19));28            ActorRuntime.RegisterActor(typeof(Actor20));29            ActorRuntime.RegisterActor(typeof(Actor21));30            ActorRuntime.RegisterActor(typeof(Actor22));31            ActorRuntime.RegisterActor(typeof(Actor23));32            ActorRuntime.RegisterActor(typeof(Actor24));33            ActorRuntime.RegisterActor(typeof(Actor25));34            ActorRuntime.RegisterActor(typeof(Actor26));35            ActorRuntime.RegisterActor(typeof(Actor27));36            ActorRuntime.RegisterActor(typeof(Actor28));37            ActorRuntime.RegisterActor(typeof(Actor29));38            ActorRuntime.RegisterActor(typeof(Actor30));39            ActorRuntime.RegisterActor(typeof(Actor31));40            ActorRuntime.RegisterActor(typeof(Actor32));41            ActorRuntime.RegisterActor(typeof(Actor33));42            ActorRuntime.RegisterActor(typeof(Actor34));43            ActorRuntime.RegisterActor(typeof(Actor35));44            ActorRuntime.RegisterActor(typeof(Actor36));45            ActorRuntime.RegisterActor(typeof(Actor37));46            ActorRuntime.RegisterActor(typeof(Actor38));47            ActorRuntime.RegisterActor(typeof(Actor39));48            ActorRuntime.RegisterActor(typeof(Actor40));49            ActorRuntime.RegisterActor(typeof(Actor41));50            ActorRuntime.RegisterActor(typeof(Actor42));51            ActorRuntime.RegisterActor(typeof(Actor43));52            ActorRuntime.RegisterActor(typeof(Actor44));53            ActorRuntime.RegisterActor(typeof(Actor

ReceiveEventAsync

Using AI Code Generation

1using System;2using System.Threading.Tasks;3using Microsoft.Coyote;4using Microsoft.Coyote.Actors;5using Microsoft.Coyote.Actors.Timers;6{7    {8        private TaskCompletionSource<bool> tcs;9        protected override Task OnInitializeAsync(Event initialEvent)10        {11            this.tcs = (TaskCompletionSource<bool>)initialEvent.Payload;12            return Task.CompletedTask;13        }14        protected override Task OnEventAsync(Event e)15        {16            if (e is Halt)17            {18                this.tcs.SetResult(true);19            }20            return Task.CompletedTask;21        }22    }23}24using System;25using System.Threading.Tasks;26using Microsoft.Coyote;27using Microsoft.Coyote.Actors;28using Microsoft.Coyote.Actors.Timers;29{30    {31        private TaskCompletionSource<bool> tcs;32        protected override Task OnInitializeAsync(Event initialEvent)33        {34            this.tcs = (TaskCompletionSource<bool>)initialEvent.Payload;35            return Task.CompletedTask;36        }37        protected override Task OnEventAsync(Event e)38        {39            if (e is Halt)40            {41                this.tcs.SetResult(true);42            }43            else if (e is MyEvent)44            {45                this.SendEvent(this.Id, new Halt());46            }47            return Task.CompletedTask;48        }49    }50}

ReceiveEventAsync

Using AI Code Generation

1{2    using System;3    using System.Threading.Tasks;4    using Microsoft.Coyote;5    using Microsoft.Coyote.Actors;6    {7        static async Task Main(string[] args)8        {9            var queue = new EventQueue();10            var e = new Event();11            queue.Enqueue(e);12            var receivedEvent = await queue.ReceiveEventAsync();13            if (receivedEvent == e)14            {15                Console.WriteLine("Received event is the same as the sent event.");16            }17        }18    }19}20{21    using System;22    using System.Threading.Tasks;23    using Microsoft.Coyote;24    using Microsoft.Coyote.Actors;25    {26        static async Task Main(string[] args)27        {28            var queue = new EventQueue();29            var e = new Event();30            queue.Enqueue(e);31            var receivedEvent = await queue.ReceiveEventAsync(TimeSpan.FromMilliseconds(100));32            if (receivedEvent == e)33            {34                Console.WriteLine("Received event is the same as the sent event.");35            }36        }37    }38}39{40    using System;41    using System.Threading;42    using System.Threading.Tasks;43    using Microsoft.Coyote;44    using Microsoft.Coyote.Actors;45    {46        static async Task Main(string[] args)47        {48            var queue = new EventQueue();49            var e = new Event();

ReceiveEventAsync

Using AI Code Generation

1using System;2using System.Threading.Tasks;3using Microsoft.Coyote.Actors;4using Microsoft.Coyote.Runtime;5using Microsoft.Coyote.Specifications;6using Microsoft.Coyote.Tasks;7using Microsoft.Coyote.Tests.Common;8using Microsoft.Coyote.Tests.Common.Events;9using Microsoft.Coyote.Tests.Common.Actors;10using Microsoft.Coyote.Tests.Common.Actors.Counter;11using Microsoft.Coyote.Tests.Common.Actors.Counter.Events;12using Microsoft.Coyote.Tests.Common.Actors.Counter.Tasks;13using Microsoft.Coyote.Tests.Common.Actors.Counter.Tasks.IncrementCounter;14using Microsoft.Coyote.Tests.Common.Actors.Counter.Tasks.ResetCounter;15using Microsoft.Coyote.Tests.Common.Actors.Counter.Tasks.SetCounter;16using Microsoft.Coyote.Tests.Common.Actors.Counter.Tasks.ReadCounter;17{18    {19        [OnEventDoAction(typeof(TestEvent), nameof(HandleTestEvent))]20        {21            private TaskCompletionSource<bool> tcs;22            protected override Task OnInitializeAsync(Event initialEvent)23            {24                this.tcs = (initialEvent as TestEvent).TaskCompletionSource;25                return Task.CompletedTask;26            }27            private void HandleTestEvent()28            {29                this.CreateActor(typeof(Counter));30                this.CreateActor(typeof(IncrementCounterTask));31                this.CreateActor(typeof(ResetCounterTask));32                this.CreateActor(typeof(SetCounterTask));33                this.CreateActor(typeof(ReadCounterTask));34                this.CreateActor(typeof(WaitForCompletionTask));35            }36            [OnEventDoAction(typeof(CompletionEvent), nameof(HandleCompletionEvent))]37            {38                private int CounterValue;39                private void HandleCompletionEvent()40                {41                    this.Assert(this.CounterValue == 10, "Counter value is not 10.");42                }43                [OnEventDoAction(typeof(IncrementCounterEvent), nameof(HandleIncrementCounterEvent))]44                {45                    private void HandleIncrementCounterEvent()46                    {47                        this.SendEvent((this.ReceivedEvent as IncrementCounterEvent).CounterId, new IncrementEvent());48                    }49                }50                [OnEventDoAction(typeof(ResetCounterEvent), nameof(HandleResetCounterEvent))]51                {52                    private void HandleResetCounterEvent()53                    {54                        this.SendEvent((this.ReceivedEvent

ReceiveEventAsync

Using AI Code Generation

1using System;2using System.Threading.Tasks;3using Microsoft.Coyote.Actors;4using Microsoft.Coyote.Runtime;5{6    {7        static async Task Main(string[] args)8        {9            EventQueue eventQueue = new EventQueue();10            ActorId actor = ActorId.CreateRandom();11            var machine = new MachineId(typeof(ReceivingMachine));12            eventQueue.EnqueueEvent(actor, new e());13            Event e = await eventQueue.ReceiveEventAsync();14            Runtime.SendEvent(machine, e);15        }16    }17    internal class e : Event { }18    {19        [OnEntry(nameof(OnEntryInit))]20        [OnEventDoAction(typeof(e), nameof(ProcessEvent))]21        private class Init : MachineState { }22        private void OnEntryInit() { }23        private void ProcessEvent() { }24    }25}26using System;27using System.Threading.Tasks;28using Microsoft.Coyote.Actors;29using Microsoft.Coyote.Runtime;30{31    {32        static async Task Main(string[] args)33        {34            EventQueue eventQueue = new EventQueue();35            ActorId actor = ActorId.CreateRandom();36            var machine = new MachineId(typeof(ReceivingMachine));37            eventQueue.EnqueueEvent(actor, new e());

Automation Testing Tutorials

Learn to execute automation testing from scratch with LambdaTest Learning Hub. Right from setting up the prerequisites to run your first automation test, to following best practices and diving deeper into advanced test scenarios. LambdaTest Learning Hubs compile a list of step-by-step guides to help you be proficient with different test automation frameworks i.e. Selenium, Cypress, TestNG etc.