KaneAI - World’s First E2E Software Testing Agent.Signup for Private Beta Join TestMu Conference

How to use Dispose method of Microsoft.Coyote.Actors.ActorExecutionContext class

Best Coyote code snippet using Microsoft.Coyote.Actors.ActorExecutionContext.Dispose

CoyoteRuntime.cs

Source:CoyoteRuntime.cs

...1182            {1183                IO.Debug.WriteLine("<Exception> {0} was thrown from operation '{1}'.",1184                    exception.GetType().Name, op.Name);1185            }1186            else if (exception is ObjectDisposedException)1187            {1188                IO.Debug.WriteLine("<Exception> {0} was thrown from operation '{1}' with reason '{2}'.",1189                    exception.GetType().Name, op.Name, ex.Message);1190            }1191            else1192            {1193                message = string.Format(CultureInfo.InvariantCulture, $"Unhandled exception. {exception}");1194            }1195            if (message != null)1196            {1197                // Report the unhandled exception.1198                this.Scheduler.NotifyUnhandledException(exception, message);1199            }1200        }1201        /// <summary>1202        /// Unwraps the specified exception.1203        /// </summary>1204        private static Exception UnwrapException(Exception ex)1205        {1206            Exception exception = ex;1207            while (exception is TargetInvocationException)1208            {1209                exception = exception.InnerException;1210            }1211            if (exception is AggregateException)1212            {1213                exception = exception.InnerException;1214            }1215            return exception;1216        }1217        /// <summary>1218        /// Registers a new specification monitor of the specified <see cref="Type"/>.1219        /// </summary>1220        internal void RegisterMonitor<T>()1221            where T : Monitor => this.DefaultActorExecutionContext.RegisterMonitor<T>();1222        /// <summary>1223        /// Invokes the specified monitor with the specified <see cref="Event"/>.1224        /// </summary>1225        internal void Monitor<T>(Event e)1226            where T : Monitor => this.DefaultActorExecutionContext.Monitor<T>(e);1227        /// <summary>1228        /// Checks if the assertion holds, and if not, throws an <see cref="AssertionFailureException"/> exception.1229        /// </summary>1230        internal void Assert(bool predicate) => this.SpecificationEngine.Assert(predicate);1231        /// <summary>1232        /// Checks if the assertion holds, and if not, throws an <see cref="AssertionFailureException"/> exception.1233        /// </summary>1234        internal void Assert(bool predicate, string s, object arg0) => this.SpecificationEngine.Assert(predicate, s, arg0);1235        /// <summary>1236        /// Checks if the assertion holds, and if not, throws an <see cref="AssertionFailureException"/> exception.1237        /// </summary>1238        internal void Assert(bool predicate, string s, object arg0, object arg1) =>1239            this.SpecificationEngine.Assert(predicate, s, arg0, arg1);1240        /// <summary>1241        /// Checks if the assertion holds, and if not, throws an <see cref="AssertionFailureException"/> exception.1242        /// </summary>1243        internal void Assert(bool predicate, string s, object arg0, object arg1, object arg2) =>1244            this.SpecificationEngine.Assert(predicate, s, arg0, arg1, arg2);1245        /// <summary>1246        /// Checks if the assertion holds, and if not, throws an <see cref="AssertionFailureException"/> exception.1247        /// </summary>1248        internal void Assert(bool predicate, string s, params object[] args) => this.SpecificationEngine.Assert(predicate, s, args);1249        /// <summary>1250        /// Creates a liveness monitor that checks if the specified task eventually completes execution successfully.1251        /// </summary>1252#if !DEBUG1253        [DebuggerStepThrough]1254#endif1255        internal void MonitorTaskCompletion(Task task) => this.SpecificationEngine.MonitorTaskCompletion(task);1256#if !DEBUG1257        [DebuggerStepThrough]1258#endif1259        internal void AssertIsAwaitedTaskControlled(Task task)1260        {1261            if (!task.IsCompleted && !this.TaskMap.ContainsKey(task) &&1262                !this.Configuration.IsPartiallyControlledTestingEnabled)1263            {1264                this.Assert(false, $"Awaiting uncontrolled task with id '{task.Id}' is not allowed: " +1265                    "either mock the method that created the task, or rewrite the method's assembly.");1266            }1267        }1268#if !DEBUG1269        [DebuggerStepThrough]1270#endif1271        internal void AssertIsReturnedTaskControlled(Task task, string methodName)1272        {1273            if (!task.IsCompleted && !this.TaskMap.ContainsKey(task) &&1274                !this.Configuration.IsPartiallyControlledTestingEnabled)1275            {1276                this.Assert(false, $"Method '{methodName}' returned an uncontrolled task with id '{task.Id}', " +1277                    "which is not allowed: either mock the method, or rewrite the method's assembly.");1278            }1279        }1280        /// <summary>1281        /// Returns a controlled nondeterministic boolean choice.1282        /// </summary>1283        internal bool GetNondeterministicBooleanChoice(int maxValue, string callerName, string callerType) =>1284            this.DefaultActorExecutionContext.GetNondeterministicBooleanChoice(maxValue, callerName, callerType);1285        /// <summary>1286        /// Returns a controlled nondeterministic integer choice.1287        /// </summary>1288        internal int GetNondeterministicIntegerChoice(int maxValue, string callerName, string callerType) =>1289            this.DefaultActorExecutionContext.GetNondeterministicIntegerChoice(maxValue, callerName, callerType);1290        /// <summary>1291        /// Returns the next available unique operation id.1292        /// </summary>1293        /// <returns>Value representing the next available unique operation id.</returns>1294        internal ulong GetNextOperationId() =>1295            // Atomically increments and safely wraps the value into an unsigned long.1296            (ulong)Interlocked.Increment(ref this.OperationIdCounter) - 1;1297        /// <summary>1298        /// Gets the <see cref="AsyncOperation"/> that is executing on the current1299        /// synchronization context, or null if no such operation is executing.1300        /// </summary>1301        internal TAsyncOperation GetExecutingOperation<TAsyncOperation>()1302            where TAsyncOperation : AsyncOperation =>1303            this.Scheduler.GetExecutingOperation<TAsyncOperation>();1304        /// <summary>1305        /// Schedules the next controlled asynchronous operation. This method1306        /// is only used during testing.1307        /// </summary>1308        internal void ScheduleNextOperation(AsyncOperationType type = AsyncOperationType.Default, bool isYielding = false, int[] hashArray = null)1309        {1310            var callerOp = this.Scheduler.GetExecutingOperation<AsyncOperation>();1311            if (callerOp != null)1312            {1313                this.Scheduler.ScheduleNextOperation(type, isYielding, hashArray);1314            }1315        }1316        /// <summary>1317        /// Returns the current hashed state of the execution.1318        /// </summary>1319        /// <remarks>1320        /// The hash is updated in each execution step.1321        /// </remarks>1322        [DebuggerStepThrough]1323        internal int GetHashedProgramState()1324        {1325            unchecked1326            {1327                int hash = 19;1328                hash = (hash * 397) + this.DefaultActorExecutionContext.GetHashedActorState();1329                hash = (hash * 397) + this.SpecificationEngine.GetHashedMonitorState();1330                return hash;1331            }1332        }1333        /// <summary>1334        /// Returns the current hashed state of the execution using the specified1335        /// level of abstraction. The hash is updated in each execution step.1336        /// </summary>1337        [DebuggerStepThrough]1338        internal int GetProgramState(string abstractionLevel, int[] hashArray = null)1339        {1340            unchecked1341            {1342                int hash = 14689;1343                if (abstractionLevel is "default" ||1344                    abstractionLevel is "custom")1345                {1346                    foreach (var operation in this.Scheduler.GetRegisteredOperations().OrderBy(op => op.Id))1347                    {1348                        if (operation is ActorOperation actorOperation)1349                        {1350                            int operationHash = 37;1351                            operationHash = (operationHash * 397) + actorOperation.Actor.GetHashedState(abstractionLevel);1352                            operationHash = (operationHash * 397) + actorOperation.Type.GetHashCode();1353                            hash *= operationHash;1354                        }1355                        else if (operation is TaskOperation taskOperation)1356                        {1357                            int operationHash = 37;1358                            operationHash = (operationHash * 397) + taskOperation.Type.GetHashCode();1359                            hash *= operationHash;1360                        }1361                    }1362                    hash = hash + this.SpecificationEngine.GetHashedMonitorState();1363                }1364                else if (abstractionLevel is "inbox-only" ||1365                    abstractionLevel is "custom-only")1366                {1367                    foreach (var operation in this.Scheduler.GetRegisteredOperations().OrderBy(op => op.Id))1368                    {1369                        if (operation is ActorOperation actorOperation)1370                        {1371                            int operationHash = 37;1372                            operationHash = (operationHash * 397) + actorOperation.Actor.GetHashedState(abstractionLevel);1373                            hash *= operationHash;1374                        }1375                    }1376                    hash = hash + this.SpecificationEngine.GetHashedMonitorState();1377                }1378                if (hashArray != null)1379                {1380                    if (abstractionLevel is "default")1381                    {1382                        hash = (hash * 397) + hashArray[0];1383                    }1384                    else if (abstractionLevel is "custom")1385                    {1386                        hash = (hash * 397) + hashArray[1];1387                    }1388                    else if (abstractionLevel is "custom-only")1389                    {1390                        hash = (hash * 397) + hashArray[2];1391                    }1392                }1393                return hash;1394            }1395        }1396        /// <summary>1397        /// Checks if the execution has deadlocked. This happens when there are no more enabled operations,1398        /// but there is one or more blocked operations that are waiting some resource to complete.1399        /// </summary>1400#if !DEBUG1401        [DebuggerHidden]1402#endif1403        internal void CheckIfExecutionHasDeadlocked(IEnumerable<AsyncOperation> ops)1404        {1405            var blockedOnReceiveOperations = ops.Where(op => op.Status is AsyncOperationStatus.BlockedOnReceive).ToList();1406            var blockedOnWaitOperations = ops.Where(op => op.Status is AsyncOperationStatus.BlockedOnWaitAll ||1407                op.Status is AsyncOperationStatus.BlockedOnWaitAny).ToList();1408            var blockedOnResources = ops.Where(op => op.Status is AsyncOperationStatus.BlockedOnResource).ToList();1409            if (blockedOnReceiveOperations.Count is 0 &&1410                blockedOnWaitOperations.Count is 0 &&1411                blockedOnResources.Count is 0)1412            {1413                return;1414            }1415            var msg = new StringBuilder("Deadlock detected.");1416            if (blockedOnReceiveOperations.Count > 0)1417            {1418                for (int idx = 0; idx < blockedOnReceiveOperations.Count; idx++)1419                {1420                    msg.Append(string.Format(CultureInfo.InvariantCulture, " {0}", blockedOnReceiveOperations[idx].Name));1421                    if (idx == blockedOnReceiveOperations.Count - 2)1422                    {1423                        msg.Append(" and");1424                    }1425                    else if (idx < blockedOnReceiveOperations.Count - 1)1426                    {1427                        msg.Append(",");1428                    }1429                }1430                msg.Append(blockedOnReceiveOperations.Count is 1 ? " is " : " are ");1431                msg.Append("waiting to receive an event, but no other controlled tasks are enabled.");1432            }1433            if (blockedOnWaitOperations.Count > 0)1434            {1435                for (int idx = 0; idx < blockedOnWaitOperations.Count; idx++)1436                {1437                    msg.Append(string.Format(CultureInfo.InvariantCulture, " {0}", blockedOnWaitOperations[idx].Name));1438                    if (idx == blockedOnWaitOperations.Count - 2)1439                    {1440                        msg.Append(" and");1441                    }1442                    else if (idx < blockedOnWaitOperations.Count - 1)1443                    {1444                        msg.Append(",");1445                    }1446                }1447                msg.Append(blockedOnWaitOperations.Count is 1 ? " is " : " are ");1448                msg.Append("waiting for a task to complete, but no other controlled tasks are enabled.");1449            }1450            if (blockedOnResources.Count > 0)1451            {1452                for (int idx = 0; idx < blockedOnResources.Count; idx++)1453                {1454                    msg.Append(string.Format(CultureInfo.InvariantCulture, " {0}", blockedOnResources[idx].Name));1455                    if (idx == blockedOnResources.Count - 2)1456                    {1457                        msg.Append(" and");1458                    }1459                    else if (idx < blockedOnResources.Count - 1)1460                    {1461                        msg.Append(",");1462                    }1463                }1464                msg.Append(blockedOnResources.Count is 1 ? " is " : " are ");1465                msg.Append("waiting to acquire a resource that is already acquired, ");1466                msg.Append("but no other controlled tasks are enabled.");1467            }1468            this.NotifyAssertionFailure(msg.ToString());1469        }1470        /// <summary>1471        /// Checks for liveness errors.1472        /// </summary>1473#if !DEBUG1474        [DebuggerHidden]1475#endif1476        internal void CheckLivenessErrors()1477        {1478            if (this.Scheduler.HasFullyExploredSchedule)1479            {1480                this.SpecificationEngine.CheckLivenessErrors();1481            }1482        }1483        /// <summary>1484        /// Notify that an assertion has failed.1485        /// </summary>1486#if !DEBUG1487        [DebuggerHidden]1488#endif1489        internal void NotifyAssertionFailure(string text, bool killTasks = true, bool cancelExecution = true) =>1490            this.Scheduler.NotifyAssertionFailure(text, killTasks, cancelExecution);1491        /// <summary>1492        /// Reports the specified thrown exception.1493        /// </summary>1494        private void ReportThrownException(Exception exception)1495        {1496            if (!(exception is ExecutionCanceledException || exception is TaskCanceledException ||1497                exception is OperationCanceledException))1498            {1499                string message = string.Format(CultureInfo.InvariantCulture,1500                    $"Exception '{exception.GetType()}' was thrown in task '{Task.CurrentId}', " +1501                    $"'{exception.Source}':\n" +1502                    $"   {exception.Message}\n" +1503                    $"The stack trace is:\n{exception.StackTrace}");1504                this.Logger.WriteLine(LogSeverity.Warning, $"<ExceptionLog> {message}");1505            }1506        }1507        /// <summary>1508        /// Raises the <see cref="OnFailure"/> event with the specified <see cref="Exception"/>.1509        /// </summary>1510        internal void RaiseOnFailureEvent(Exception exception)1511        {1512            if (this.IsControlled &&1513                (exception is ExecutionCanceledException ||1514                (exception is ActionExceptionFilterException ae && ae.InnerException is ExecutionCanceledException)))1515            {1516                // Internal exception used during testing.1517                return;1518            }1519            if (this.Configuration.AttachDebugger)1520            {1521                Debugger.Break();1522                this.Configuration.AttachDebugger = false;1523            }1524            this.OnFailure?.Invoke(exception);1525        }1526        /// <summary>1527        /// Assigns the specified runtime as the default for the current asynchronous control flow.1528        /// </summary>1529        internal static void AssignAsyncControlFlowRuntime(CoyoteRuntime runtime) => AsyncLocalInstance.Value = runtime;1530        /// <summary>1531        /// Waits until all actors have finished execution.1532        /// </summary>1533        [DebuggerStepThrough]1534        internal Task WaitAsync() => this.Scheduler.WaitAsync();1535        /// <summary>1536        /// Disposes runtime resources.1537        /// </summary>1538        private void Dispose(bool disposing)1539        {1540            if (disposing)1541            {1542                this.OperationIdCounter = 0;1543                this.DefaultActorExecutionContext.Dispose();1544                this.SpecificationEngine.Dispose();1545                if (this.IsControlled)1546                {1547                    // Note: this makes it possible to run a Controlled unit test followed by a production1548                    // unit test, whereas before that would throw "Uncontrolled Task" exceptions.1549                    // This does not solve mixing unit test type in parallel.1550                    Interlocked.Decrement(ref ExecutionControlledUseCount);1551                }1552                AssignAsyncControlFlowRuntime(null);1553            }1554        }1555        /// <summary>1556        /// Disposes runtime resources.1557        /// </summary>1558        public void Dispose()1559        {1560            this.Dispose(true);1561            GC.SuppressFinalize(this);1562        }1563    }1564}...

ActorExecutionContext.cs

Source:ActorExecutionContext.cs

...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            }1121            /// <inheritdoc/>1122            internal override void LogWaitEvent(Actor actor, IEnumerable<Type> eventTypes)1123            {1124                string stateName = actor is StateMachine stateMachine ? stateMachine.CurrentStateName : null;1125                var eventWaitTypesArray = eventTypes.ToArray();1126                if (eventWaitTypesArray.Length is 1)1127                {1128                    this.LogWriter.LogWaitEvent(actor.Id, stateName, eventWaitTypesArray[0]);1129                }1130                else1131                {1132                    this.LogWriter.LogWaitEvent(actor.Id, stateName, eventWaitTypesArray);1133                }1134                this.Scheduler.ScheduleNextOperation(AsyncOperationType.Join);1135                this.ResetProgramCounter(actor);1136            }1137            /// <inheritdoc/>1138            internal override void LogEnteredState(StateMachine stateMachine)1139            {1140                string stateName = stateMachine.CurrentStateName;1141                this.LogWriter.LogStateTransition(stateMachine.Id, stateName, isEntry: true);1142            }1143            /// <inheritdoc/>1144            internal override void LogExitedState(StateMachine stateMachine)1145            {1146                this.LogWriter.LogStateTransition(stateMachine.Id, stateMachine.CurrentStateName, isEntry: false);1147            }1148            /// <inheritdoc/>1149            internal override void LogPopState(StateMachine stateMachine)1150            {1151                this.AssertExpectedCallerActor(stateMachine, "Pop");1152                this.LogWriter.LogPopState(stateMachine.Id, default, stateMachine.CurrentStateName);1153            }1154            /// <inheritdoc/>1155            internal override void LogInvokedOnEntryAction(StateMachine stateMachine, MethodInfo action)1156            {1157                string stateName = stateMachine.CurrentStateName;1158                this.LogWriter.LogExecuteAction(stateMachine.Id, stateName, stateName, action.Name);1159            }1160            /// <inheritdoc/>1161            internal override void LogInvokedOnExitAction(StateMachine stateMachine, MethodInfo action)1162            {1163                string stateName = stateMachine.CurrentStateName;1164                this.LogWriter.LogExecuteAction(stateMachine.Id, stateName, stateName, action.Name);1165            }1166            /// <summary>1167            /// Returns the current hashed state of the actors.1168            /// </summary>1169            /// <remarks>1170            /// The hash is updated in each execution step.1171            /// </remarks>1172            internal override int GetHashedActorState()1173            {1174                unchecked1175                {1176                    int hash = 19;1177                    foreach (var operation in this.Scheduler.GetRegisteredOperations().OrderBy(op => op.Id))1178                    {1179                        if (operation is ActorOperation actorOperation)1180                        {1181                            hash *= 31 + actorOperation.Actor.GetHashedState();1182                        }1183                    }1184                    return hash;1185                }1186            }1187            /// <inheritdoc/>1188            [MethodImpl(MethodImplOptions.AggressiveInlining)]1189            internal override int GetActorProgramCounter(ActorId actorId) =>1190                this.ProgramCounterMap.GetOrAdd(actorId, 0);1191            /// <summary>1192            /// Increments the program counter of the specified actor.1193            /// </summary>1194            [MethodImpl(MethodImplOptions.AggressiveInlining)]1195            private void IncrementActorProgramCounter(ActorId actorId) =>1196                this.ProgramCounterMap.AddOrUpdate(actorId, 1, (id, value) => value + 1);1197            /// <summary>1198            /// Resets the program counter of the specified actor.1199            /// </summary>1200            private void ResetProgramCounter(Actor actor)1201            {1202                if (actor != null)1203                {1204                    this.ProgramCounterMap.AddOrUpdate(actor.Id, 0, (id, value) => 0);1205                }1206            }1207            /// <inheritdoc/>1208#if !DEBUG1209            [DebuggerHidden]1210#endif1211            internal override void AssertExpectedCallerActor(Actor caller, string calledAPI)1212            {1213                if (caller is null)1214                {1215                    return;1216                }1217                var op = this.Scheduler.GetExecutingOperation<ActorOperation>();1218                if (op is null)1219                {1220                    return;1221                }1222                this.Assert(op.Actor.Equals(caller), "{0} invoked {1} on behalf of {2}.",1223                    op.Actor.Id, calledAPI, caller.Id);1224            }1225            /// <summary>1226            /// Processes an unhandled exception in the specified asynchronous operation.1227            /// </summary>1228            private void ProcessUnhandledExceptionInOperation(AsyncOperation op, Exception ex)1229            {1230                string message = null;1231                Exception exception = UnwrapException(ex);1232                if (exception is ExecutionCanceledException || exception is TaskSchedulerException)1233                {1234                    IODebug.WriteLine("<Exception> {0} was thrown from operation '{1}'.",1235                        exception.GetType().Name, op.Name);1236                }1237                else if (exception is ObjectDisposedException)1238                {1239                    IODebug.WriteLine("<Exception> {0} was thrown from operation '{1}' with reason '{2}'.",1240                        exception.GetType().Name, op.Name, ex.Message);1241                }1242                else if (op is ActorOperation actorOp)1243                {1244                    message = string.Format(CultureInfo.InvariantCulture,1245                        $"Unhandled exception. {exception.GetType()} was thrown in actor {actorOp.Name}, " +1246                        $"'{exception.Source}':\n" +1247                        $"   {exception.Message}\n" +1248                        $"The stack trace is:\n{exception.StackTrace}");1249                }1250                else1251                {1252                    message = string.Format(CultureInfo.InvariantCulture, $"Unhandled exception. {exception}");1253                }1254                if (message != null)1255                {1256                    // Report the unhandled exception.1257                    this.Scheduler.NotifyUnhandledException(exception, message);1258                }1259            }1260            /// <summary>1261            /// Unwraps the specified exception.1262            /// </summary>1263            private static Exception UnwrapException(Exception ex)1264            {1265                Exception exception = ex;1266                while (exception is TargetInvocationException)1267                {1268                    exception = exception.InnerException;1269                }1270                if (exception is AggregateException)1271                {1272                    exception = exception.InnerException;1273                }1274                return exception;1275            }1276            /// <inheritdoc/>1277            protected override void Dispose(bool disposing)1278            {1279                if (disposing)1280                {1281                    this.NameValueToActorId.Clear();1282                    this.ProgramCounterMap.Clear();1283                }1284                base.Dispose(disposing);1285            }1286        }1287    }1288}...

Dispose

Using AI Code Generation

1using System;2using Microsoft.Coyote;3using Microsoft.Coyote.Actors;4using Microsoft.Coyote.Actors.Timers;5using Microsoft.Coyote.SystematicTesting;6using Microsoft.Coyote.Tasks;7using Microsoft.Coyote.SystematicTesting.Tasks;8using Microsoft.Coyote.SystematicTesting.Timers;9using Microsoft.Coyote.SystematicTesting.Actors;10using Microsoft.Coyote.SystematicTesting.Runtime;11using System.Threading.Tasks;12using System.Diagnostics;13using System.Threading;14using System.Collections.Generic;15using System.Collections.Concurrent;16using Microsoft.Coyote.SystematicTesting.Threading;17using System.Linq;18using System.IO;19using System.Text;20using Microsoft.Coyote.SystematicTesting.Exceptions;21{22    {23        public static void Main(string[] args)24        {25            var configuration = Configuration.Create();26            configuration.EnableCycleDetection = true;27            configuration.EnableDataRaceDetection = true;28            configuration.EnableDeadlockDetection = true;29            configuration.EnableLivelockDetection = true;30            configuration.EnableOperationInterleavings = true;31            configuration.EnablePhaseInterleavings = true;32            configuration.EnableRandomExecution = true;33            configuration.EnableStategraphTesting = true;34            configuration.EnableTaskInterleavings = true;35            configuration.EnableUnfairScheduling = true;36            configuration.EnableUnfairSchedulingWithFairnessBound = true;37            configuration.EnableUnfairSchedulingWithFairnessBound = true;38            configuration.FairnessBound = 2;39            configuration.MaxFairSchedulingSteps = 2;40            configuration.MaxUnfairSchedulingSteps = 2;41            configuration.MaxSteps = 2;

Dispose

Using AI Code Generation

1using System;2using System.Threading.Tasks;3using Microsoft.Coyote;4using Microsoft.Coyote.Actors;5using Microsoft.Coyote.Testing;6using Microsoft.Coyote.TestingServices;7using Microsoft.Coyote.TestingServices.SchedulingStrategies;8using Microsoft.Coyote.TestingServices.Tracing.Schedule;9using Microsoft.Coyote.TestingServices.Tracing.ScheduleExploration;10{11    static void Main(string[] args)12    {13        var configuration = Configuration.Create().WithTestingIterations(1000);14        configuration.SchedulingStrategy = new RandomStrategy();15        configuration.SchedulingIterations = 1000;16        configuration.SchedulingSeed = 0;17        configuration.Verbose = 1;18        configuration.LivenessTemperatureThreshold = 1;19        configuration.UserOutputFilePath = "output.txt";20        configuration.LogWriter = new LogWriter();21        configuration.SchedulingTraceFilePath = "trace.xml";22        configuration.SchedulingStrategy = new RandomStrategy();23        configuration.SchedulingIterations = 1000;24        configuration.SchedulingSeed = 0;25        configuration.Verbose = 1;26        configuration.LivenessTemperatureThreshold = 1;27        configuration.UserOutputFilePath = "output.txt";28        configuration.LogWriter = new LogWriter();29        configuration.SchedulingTraceFilePath = "trace.xml";30        configuration.SchedulingStrategy = new RandomStrategy();31        configuration.SchedulingIterations = 1000;32        configuration.SchedulingSeed = 0;33        configuration.Verbose = 1;34        configuration.LivenessTemperatureThreshold = 1;35        configuration.UserOutputFilePath = "output.txt";36        configuration.LogWriter = new LogWriter();37        configuration.SchedulingTraceFilePath = "trace.xml";38        configuration.SchedulingStrategy = new RandomStrategy();39        configuration.SchedulingIterations = 1000;40        configuration.SchedulingSeed = 0;41        configuration.Verbose = 1;42        configuration.LivenessTemperatureThreshold = 1;43        configuration.UserOutputFilePath = "output.txt";44        configuration.LogWriter = new LogWriter();45        configuration.SchedulingTraceFilePath = "trace.xml";46        configuration.SchedulingStrategy = new RandomStrategy();47        configuration.SchedulingIterations = 1000;48        configuration.SchedulingSeed = 0;49        configuration.Verbose = 1;50        configuration.LivenessTemperatureThreshold = 1;51        configuration.UserOutputFilePath = "output.txt";52        configuration.LogWriter = new LogWriter();53        configuration.SchedulingTraceFilePath = "trace.xml";

Dispose

Using AI Code Generation

1using System;2using Microsoft.Coyote.Actors;3using Microsoft.Coyote.Runtime;4using Microsoft.Coyote.SystematicTesting;5using Microsoft.Coyote.Tasks;6using Microsoft.Coyote.Scheduling;7using System.Threading.Tasks;8{9    {10        public int Value;11        public Event1(int value)12        {13            Value = value;14        }15    }16    {17        public int Value;18        public Event2(int value)19        {20            Value = value;21        }22    }23    {24        protected override async Task OnInitializeAsync(Event initialEvent)25        {26            int value = 0;27            if (initialEvent is Event1)28            {29                value = ((Event1)initialEvent).Value;30            }31            else if (initialEvent is Event2)32            {33                value = ((Event2)initialEvent).Value;34            }35            await this.SendEvent(this.Id, new Event1(value + 1));36            await this.SendEvent(this.Id, new Event2(value + 2));37        }38    }39    {40        public static void Main(string[] args)41        {42            var configuration = Configuration.Create().WithTestingIterations(1);43            using (var runtime = RuntimeFactory.Create(configuration))44            {45                runtime.RegisterActor(typeof(Actor1));46                var actorTask = Task.Run(async () =>47                {48                    var actorId = await runtime.CreateActorAsync(typeof(Actor1), new Event1(0));49                    await runtime.DisposeAsync(actorId);50                });51                runtime.Run();

Dispose

Using AI Code Generation

1using Microsoft.Coyote;2using Microsoft.Coyote.Actors;3using Microsoft.Coyote.Actors.Timers;4using Microsoft.Coyote.Specifications;5using Microsoft.Coyote.Tasks;6using System;7using System.Collections.Generic;8using System.Linq;9using System.Text;10using System.Threading.Tasks;11{12    {13        static void Main(string[] args)14        {15            var runtime = RuntimeFactory.Create();16            runtime.CreateActor(typeof(HelloWorld));17            runtime.Dispose();18        }19    }20    {21        protected override async Task OnInitializeAsync(Event initialEvent)22        {23            await this.SendEvent(this.Id, new E());24            await this.ReceiveEventAsync(typeof(E));25        }26    }27    class E : Event { }28}29using Microsoft.Coyote;30using Microsoft.Coyote.Actors;31using Microsoft.Coyote.Actors.Timers;32using Microsoft.Coyote.Specifications;33using Microsoft.Coyote.Tasks;34using System;35using System.Collections.Generic;36using System.Linq;37using System.Text;38using System.Threading.Tasks;39{40    {41        static void Main(string[] args)42        {43            var runtime = RuntimeFactory.Create();44            runtime.CreateActor(typeof(HelloWorld));45            runtime.Dispose();46        }47    }48    {49        protected override async Task OnInitializeAsync(Event initialEvent)50        {51            await this.SendEvent(this.Id, new E());52            await this.ReceiveEventAsync(typeof(E));53        }54    }55    class E : Event { }56}57using Microsoft.Coyote;58using Microsoft.Coyote.Actors;59using Microsoft.Coyote.Actors.Timers;60using Microsoft.Coyote.Specifications;61using Microsoft.Coyote.Tasks;62using System;63using System.Collections.Generic;64using System.Linq;65using System.Text;66using System.Threading.Tasks;67{68    {69        static void Main(string[] args)70        {71            var runtime = RuntimeFactory.Create();72            runtime.CreateActor(typeof(HelloWorld));73            runtime.Dispose();74        }75    }

Dispose

Using AI Code Generation

1using Microsoft.Coyote.Actors;2using System;3using System.Collections.Generic;4using System.Threading.Tasks;5{6    {7        static void Main(string[] args)8        {9            using (var runtime = RuntimeFactory.Create())10            {11                var actor = runtime.CreateActor(typeof(MyActor));12                runtime.SendEvent(actor, new MyEvent());13            }14        }15    }16    class MyEvent : Event { }17    {18        protected override async Task OnInitializeAsync(Event initialEvent)19        {20            await this.ReceiveEventAsync<MyEvent>();21            Console.WriteLine("Received event!");22        }23    }24}25using Microsoft.Coyote.Actors;26using System;27using System.Collections.Generic;28using System.Threading.Tasks;29{30    {31        static void Main(string[] args)32        {33            using (var runtime = RuntimeFactory.Create())34            {35                var actor = runtime.CreateActor(typeof(MyActor));36                runtime.SendEvent(actor, new MyEvent());37            }38        }39    }40    class MyEvent : Event { }41    {42        protected override async Task OnInitializeAsync(Event initialEvent)43        {44            await this.ReceiveEventAsync<MyEvent>();45            Console.WriteLine("Received event!");46        }47    }48}49using Microsoft.Coyote.Actors;50using System;51using System.Collections.Generic;52using System.Threading.Tasks;53{54    {55        static void Main(string[] args)56        {57            using (var runtime = RuntimeFactory.Create())58            {59                var actor = runtime.CreateActor(typeof(MyActor));60                runtime.SendEvent(actor, new MyEvent());61            }62        }63    }64    class MyEvent : Event { }65    {66        protected override async Task OnInitializeAsync(Event initialEvent)67        {

Dispose

Using AI Code Generation

1using System;2using System.Threading.Tasks;3using Microsoft.Coyote;4{5    {6        static void Main(string[] args)7        {8            Console.WriteLine("Hello World!");9            using (var runtime = RuntimeFactory.Create())10            {11                var proxy = runtime.CreateActor(typeof(MyActor));12                var task = proxy.SendEventAsync(new MyEvent());13                task.Wait();14            }15        }16    }17    class MyEvent : Event { }18    {19        protected override Task OnInitializeAsync(Event initialEvent)20        {21            Console.WriteLine("Actor initialized.");22            return Task.CompletedTask;23        }24        protected override Task OnEventAsync(Event e)25        {26            if (e is MyEvent)27            {28                Console.WriteLine("Received MyEvent.");29            }30            return Task.CompletedTask;31        }32    }33}34using System;35using System.Threading.Tasks;36using Microsoft.Coyote;37{38    {39        static void Main(string[] args)40        {41            Console.WriteLine("Hello World!");42            using (var runtime = RuntimeFactory.Create())43            {44                var proxy = runtime.CreateActor(typeof(MyActor));45                var task = proxy.SendEventAsync(new MyEvent());46                task.Wait();47            }48        }49    }50    class MyEvent : Event { }51    {52        protected override Task OnInitializeAsync(Event initialEvent)53        {54            Console.WriteLine("Actor initialized.");55            return Task.CompletedTask;56        }57        protected override Task OnEventAsync(Event e)58        {59            if (e is MyEvent)60            {61                Console.WriteLine("Received MyEvent.");62            }63            return Task.CompletedTask;64        }65    }66}67using System;68using System.Threading.Tasks;69using Microsoft.Coyote;

Dispose

Using AI Code Generation

1using Microsoft.Coyote.Actors;2using System;3using System.Threading.Tasks;4using Microsoft.Coyote;5{6    {7        static void Main(string[] args)8        {9            ActorRuntime runtime = new ActorRuntime();10            runtime.CreateActor(typeof(MyFirstActor));11            Console.ReadLine();12            runtime.Dispose();13        }14    }15    {16        protected override Task OnInitializeAsync(Event initialEvent)17        {18            Console.WriteLine("MyFirstActor initialized");19            return Task.CompletedTask;20        }21    }22}

Dispose

Using AI Code Generation

1using Microsoft.Coyote.Actors;2using System;3{4    {5        static void Main(string[] args)6        {7            using (ActorExecutionContext runtime = ActorExecutionContext.Create())8            {9            }10        }11    }12}

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.