How to use ToString method of Microsoft.Coyote.Runtime.ControlledOperation class

Best Coyote code snippet using Microsoft.Coyote.Runtime.ControlledOperation.ToString

CoyoteRuntime.cs

Source:CoyoteRuntime.cs

...418                    {419                        CleanCurrentExecutionContext();420                    }421                });422                thread.Name = Guid.NewGuid().ToString();423                thread.IsBackground = true;424                // TODO: optimize by reusing threads instead of creating a new thread each time?425                this.ThreadPool.AddOrUpdate(op.Id, thread, (id, oldThread) => thread);426                this.ControlledThreads.AddOrUpdate(thread.Name, op, (threadName, oldOp) => op);427                thread.Start();428            }429        }430        /// <summary>431        /// Schedules the specified delay to be executed asynchronously.432        /// </summary>433#if !DEBUG434        [DebuggerStepThrough]435#endif436        internal Task ScheduleDelay(TimeSpan delay, CancellationToken cancellationToken)437        {438            if (delay.TotalMilliseconds is 0)439            {440                // If the delay is 0, then complete synchronously.441                return Task.CompletedTask;442            }443            // TODO: support cancellations during testing.444            if (this.SchedulingPolicy is SchedulingPolicy.Interleaving)445            {446                uint timeout = (uint)this.GetNextNondeterministicIntegerChoice((int)this.Configuration.TimeoutDelay, null, null);447                if (timeout is 0)448                {449                    // If the delay is 0, then complete synchronously.450                    return Task.CompletedTask;451                }452                // TODO: cache the dummy delay action to optimize memory.453                ControlledOperation op = this.CreateControlledOperation(timeout);454                return this.TaskFactory.StartNew(state =>455                {456                    var delayedOp = state as ControlledOperation;457                    delayedOp.Status = OperationStatus.PausedOnDelay;458                    this.ScheduleNextOperation(delayedOp, SchedulingPointType.Yield);459                },460                op,461                cancellationToken,462                this.TaskFactory.CreationOptions | TaskCreationOptions.DenyChildAttach,463                this.TaskFactory.Scheduler);464            }465            if (!this.TryGetExecutingOperation(out ControlledOperation current))466            {467                // Cannot fuzz the delay of an uncontrolled operation.468                return Task.Delay(delay, cancellationToken);469            }470            // TODO: we need to come up with something better!471            // Fuzz the delay.472            return Task.Delay(TimeSpan.FromMilliseconds(473                this.GetNondeterministicDelay(current, (int)delay.TotalMilliseconds)));474        }475        /// <summary>476        /// Unwraps the specified task.477        /// </summary>478        internal Task UnwrapTask(Task<Task> task)479        {480            var unwrappedTask = task.Unwrap();481            if (this.ControlledTasks.TryGetValue(task, out ControlledOperation op))482            {483                this.ControlledTasks.TryAdd(unwrappedTask, op);484            }485            return unwrappedTask;486        }487        /// <summary>488        /// Unwraps the specified task.489        /// </summary>490        internal Task<TResult> UnwrapTask<TResult>(Task<Task<TResult>> task)491        {492            var unwrappedTask = task.Unwrap();493            if (this.ControlledTasks.TryGetValue(task, out ControlledOperation op))494            {495                this.ControlledTasks.TryAdd(unwrappedTask, op);496            }497            return unwrappedTask;498        }499        /// <summary>500        /// Registers the specified task as a known controlled task.501        /// </summary>502        internal void RegisterKnownControlledTask(Task task)503        {504            if (this.SchedulingPolicy != SchedulingPolicy.None)505            {506                this.ControlledTasks.TryAdd(task, null);507            }508        }509        /// <summary>510        /// Creates a new controlled operation with an optional delay.511        /// </summary>512        internal ControlledOperation CreateControlledOperation(uint delay = 0)513        {514            using (SynchronizedSection.Enter(this.RuntimeLock))515            {516                // Assign the operation group associated with the execution context of the517                // current thread, if such a group exists, else the group of the currently518                // executing operation, if such an operation exists.519                OperationGroup group = OperationGroup.Current ?? ExecutingOperation.Value?.Group;520                // Create a new controlled operation using the next available operation id.521                ulong operationId = this.GetNextOperationId();522                ControlledOperation op = delay > 0 ?523                    new DelayOperation(operationId, $"Delay({operationId})", delay, this) :524                    new ControlledOperation(operationId, $"Op({operationId})", group, this);525                if (operationId > 0 && !this.IsThreadControlled(Thread.CurrentThread))526                {527                    op.IsSourceUncontrolled = true;528                }529                return op;530            }531        }532        /// <summary>533        /// Creates a new user-defined controlled operation from the specified builder.534        /// </summary>535        internal ControlledOperation CreateUserDefinedOperation(IOperationBuilder builder)536        {537            using (SynchronizedSection.Enter(this.RuntimeLock))538            {539                // Create a new controlled operation using the next available operation id.540                ulong operationId = this.GetNextOperationId();541                var op = new UserDefinedOperation(this, builder, operationId);542                if (operationId > 0 && !this.IsThreadControlled(Thread.CurrentThread))543                {544                    op.IsSourceUncontrolled = true;545                }546                return op;547            }548        }549        /// <summary>550        /// Registers the specified newly created controlled operation.551        /// </summary>552        /// <param name="op">The newly created operation to register.</param>553        internal void RegisterNewOperation(ControlledOperation op)554        {555            using (SynchronizedSection.Enter(this.RuntimeLock))556            {557                if (this.ExecutionStatus != ExecutionStatus.Running)558                {559                    return;560                }561#if NETSTANDARD2_0 || NETFRAMEWORK562                if (!this.OperationMap.ContainsKey(op.Id))563                {564                    this.OperationMap.Add(op.Id, op);565                }566#else567                this.OperationMap.TryAdd(op.Id, op);568#endif569                // Assign the operation as a member of its group.570                op.Group.RegisterMember(op);571                if (this.OperationMap.Count is 1)572                {573                    // This is the first operation registered, so schedule it.574                    this.ScheduledOperation = op;575                }576                else577                {578                    // As this is not the first operation getting created, assign an event579                    // handler so that the next scheduling decision cannot be made until580                    // this operation starts executing to avoid race conditions.581                    this.PendingStartOperationMap.Add(op, new ManualResetEventSlim(false));582                }583                IO.Debug.WriteLine("[coyote::debug] Created operation '{0}' of group '{1}' on thread '{2}'.",584                    op.Name, op.Group, Thread.CurrentThread.ManagedThreadId);585            }586        }587        /// <summary>588        /// Starts the execution of the specified controlled operation.589        /// </summary>590        /// <param name="op">The operation to start executing.</param>591        /// <remarks>592        /// This method performs a handshake with <see cref="WaitOperationsStart"/>.593        /// </remarks>594        internal void StartOperation(ControlledOperation op)595        {596            // Configures the execution context of the current thread with data597            // related to the runtime and the operation executed by this thread.598            this.SetCurrentExecutionContext(op);599            using (SynchronizedSection.Enter(this.RuntimeLock))600            {601                IO.Debug.WriteLine("[coyote::debug] Started operation '{0}' of group '{1}' on thread '{2}'.",602                    op.Name, op.Group, Thread.CurrentThread.ManagedThreadId);603                op.Status = OperationStatus.Enabled;604                if (this.SchedulingPolicy is SchedulingPolicy.Interleaving)605                {606                    // If this operation has an associated handler that notifies another awaiting607                    // operation about this operation starting its execution, then set the handler.608                    if (this.PendingStartOperationMap.TryGetValue(op, out ManualResetEventSlim handler))609                    {610                        handler.Set();611                    }612                    // Pause the operation as soon as it starts executing to allow the runtime613                    // to explore a potential interleaving with another executing operation.614                    this.PauseOperation(op);615                }616            }617        }618        /// <summary>619        /// Waits for all recently created operations to start executing.620        /// </summary>621        /// <remarks>622        /// This method performs a handshake with <see cref="StartOperation"/>. It is assumed that this623        /// method is invoked by the same thread executing the operation and that it runs in the scope624        /// of a <see cref="SynchronizedSection"/>.625        /// </remarks>626        private void WaitOperationsStart()627        {628            if (this.SchedulingPolicy is SchedulingPolicy.Interleaving)629            {630                while (this.PendingStartOperationMap.Count > 0)631                {632                    var pendingOp = this.PendingStartOperationMap.First();633                    while (pendingOp.Key.Status is OperationStatus.None && this.ExecutionStatus is ExecutionStatus.Running)634                    {635                        IO.Debug.WriteLine("[coyote::debug] Sleeping thread '{0}' until operation '{1}' of group '{2}' starts.",636                            Thread.CurrentThread.ManagedThreadId, pendingOp.Key.Name, pendingOp.Key.Group);637                        using (SynchronizedSection.Exit(this.RuntimeLock))638                        {639                            try640                            {641                                pendingOp.Value.Wait();642                            }643                            catch (ObjectDisposedException)644                            {645                                // The handler was disposed, so we can ignore this exception.646                            }647                        }648                        IO.Debug.WriteLine("[coyote::debug] Waking up thread '{0}'.", Thread.CurrentThread.ManagedThreadId);649                    }650                    pendingOp.Value.Dispose();651                    this.PendingStartOperationMap.Remove(pendingOp.Key);652                }653            }654        }655        /// <summary>656        /// Pauses the execution of the specified operation.657        /// </summary>658        /// <remarks>659        /// It is assumed that this method is invoked by the same thread executing the operation660        /// and that it runs in the scope of a <see cref="SynchronizedSection"/>.661        /// </remarks>662        private void PauseOperation(ControlledOperation op)663        {664            // Only pause the operation if it is not already completed and it is currently executing on this thread.665            if (op.Status != OperationStatus.Completed && op == ExecutingOperation.Value)666            {667                // Do not allow the operation to wake up, unless its currently scheduled and enabled or the runtime stopped running.668                while (!(op == this.ScheduledOperation && op.Status is OperationStatus.Enabled) && this.ExecutionStatus is ExecutionStatus.Running)669                {670                    IO.Debug.WriteLine("[coyote::debug] Sleeping operation '{0}' of group '{1}' on thread '{2}'.",671                        op.Name, op.Group, Thread.CurrentThread.ManagedThreadId);672                    using (SynchronizedSection.Exit(this.RuntimeLock))673                    {674                        op.WaitSignal();675                    }676                    IO.Debug.WriteLine("[coyote::debug] Waking up operation '{0}' of group '{1}' on thread '{2}'.",677                        op.Name, op.Group, Thread.CurrentThread.ManagedThreadId);678                }679            }680        }681        /// <summary>682        /// Pauses the currently executing operation until the specified condition gets resolved.683        /// </summary>684        internal void PauseOperationUntil(ControlledOperation current, Func<bool> condition, bool isConditionControlled = true, string debugMsg = null)685        {686            using (SynchronizedSection.Enter(this.RuntimeLock))687            {688                if (this.SchedulingPolicy is SchedulingPolicy.Interleaving)689                {690                    // Only proceed if there is an operation executing on the current thread and691                    // the condition is not already resolved.692                    current ??= this.GetExecutingOperation();693                    while (current != null && !condition() && this.ExecutionStatus is ExecutionStatus.Running)694                    {695                        IO.Debug.WriteLine("[coyote::debug] Operation '{0}' of group '{1}' is waiting for {2} on thread '{3}'.",696                            current.Name, current.Group, debugMsg ?? "condition to get resolved", Thread.CurrentThread.ManagedThreadId);697                        // TODO: can we identify when the dependency is uncontrolled?698                        current.PauseWithDependency(condition, isConditionControlled);699                        this.ScheduleNextOperation(current, SchedulingPointType.Pause);700                    }701                }702            }703        }704        /// <summary>705        /// Asynchronously pauses the currently executing operation until the specified condition gets resolved.706        /// </summary>707        internal PausedOperationAwaitable PauseOperationUntilAsync(Func<bool> condition, bool resumeAsynchronously)708        {709            using (SynchronizedSection.Enter(this.RuntimeLock))710            {711                if (this.SchedulingPolicy is SchedulingPolicy.Interleaving &&712                    this.TryGetExecutingOperation(out ControlledOperation current))713                {714                    return new PausedOperationAwaitable(this, current, condition, resumeAsynchronously);715                }716            }717            return new PausedOperationAwaitable(this, null, condition, resumeAsynchronously);718        }719        /// <summary>720        /// Schedules the next enabled operation, which can include the currently executing operation.721        /// </summary>722        /// <param name="current">The currently executing operation, if there is one.</param>723        /// <param name="type">The type of the scheduling point.</param>724        /// <param name="isSuppressible">True if the interleaving can be suppressed, else false.</param>725        /// <param name="isYielding">True if the current operation is yielding, else false.</param>726        /// <remarks>727        /// An enabled operation is one that is not paused nor completed.728        /// </remarks>729        internal void ScheduleNextOperation(ControlledOperation current, SchedulingPointType type, bool isSuppressible = true, bool isYielding = false)730        {731            using (SynchronizedSection.Enter(this.RuntimeLock))732            {733                // Wait for all recently created operations to start executing.734                this.WaitOperationsStart();735                if (this.ExecutionStatus != ExecutionStatus.Running ||736                    this.SchedulingPolicy != SchedulingPolicy.Interleaving)737                {738                    // Cannot schedule the next operation if the scheduler is not attached,739                    // or if the scheduling policy is not systematic.740                    return;741                }742                // Check if the currently executing thread is uncontrolled.743                bool isThreadUncontrolled = false;744                if (current is null && !this.IsThreadControlled(Thread.CurrentThread))745                {746                    if (this.LastPostponedSchedulingPoint is SchedulingPointType.Pause ||747                        this.LastPostponedSchedulingPoint is SchedulingPointType.Complete)748                    {749                        // A scheduling point was postponed due to a potential deadlock, which has750                        // now been resolved, so resume it on this uncontrolled thread.751                        current = this.ScheduledOperation;752                        type = this.LastPostponedSchedulingPoint.Value;753                        IO.Debug.WriteLine("[coyote::debug] Resuming scheduling point '{0}' of operation '{1}' in uncontrolled thread '{2}'.",754                            type, current, Thread.CurrentThread.ManagedThreadId);755                    }756                    else if (type is SchedulingPointType.Create || type is SchedulingPointType.ContinueWith)757                    {758                        // This is a scheduling point that was invoked because a new operation was759                        // created by an uncontrolled thread, so postpone the scheduling point and760                        // resume it on the next available controlled thread.761                        IO.Debug.WriteLine("[coyote::debug] Postponing scheduling point '{0}' in uncontrolled thread '{1}'.",762                            type, Thread.CurrentThread.ManagedThreadId);763                        this.LastPostponedSchedulingPoint = type;764                        return;765                    }766                    isThreadUncontrolled = true;767                }768                // If the current operation was provided as argument to this method, or it is null, then this769                // is a controlled thread, so get the currently executing operation to proceed with scheduling.770                current ??= this.GetExecutingOperation();771                if (current is null)772                {773                    // Cannot proceed without having access to the currently executing operation.774                    return;775                }776                if (current != this.ScheduledOperation)777                {778                    // The currently executing operation is not scheduled, so send it to sleep.779                    this.PauseOperation(current);780                    return;781                }782                if (this.IsSchedulerSuppressed && this.LastPostponedSchedulingPoint is null &&783                    isSuppressible && current.Status is OperationStatus.Enabled)784                {785                    // Suppress the scheduling point.786                    IO.Debug.WriteLine("[coyote::debug] Suppressing scheduling point in operation '{0}'.", current.Name);787                    return;788                }789                this.Assert(!this.IsSpecificationInvoked, "Executing a specification monitor must be atomic.");790                // Checks if the scheduling steps bound has been reached.791                this.CheckIfSchedulingStepsBoundIsReached();792                // Update metadata related to this scheduling point.793                current.LastSchedulingPoint = type;794                this.LastPostponedSchedulingPoint = null;795                if (this.Configuration.IsProgramStateHashingEnabled)796                {797                    // Update the current operation with the hashed program state.798                    current.LastHashedProgramState = this.GetHashedProgramState();799                }800                // Try to enable any operations with resolved dependencies before asking the801                // scheduler to choose the next one to schedule.802                IEnumerable<ControlledOperation> ops = this.OperationMap.Values;803                if (!this.TryEnableOperationsWithResolvedDependencies(current))804                {805                    if (this.IsUncontrolledConcurrencyDetected &&806                        this.Configuration.IsPartiallyControlledConcurrencyAllowed)807                    {808                        // TODO: optimize and make this more fine-grained.809                        // If uncontrolled concurrency is detected, then do not check for deadlocks directly,810                        // but instead leave it to the background deadlock detection timer and postpone the811                        // scheduling point, which might get resolved from an uncontrolled thread.812                        IO.Debug.WriteLine("[coyote::debug] Postponing scheduling point '{0}' of operation '{1}' due to potential deadlock.",813                            type, current);814                        this.LastPostponedSchedulingPoint = type;815                        this.PauseOperation(current);816                        return;817                    }818                    // Check if the execution has deadlocked.819                    this.CheckIfExecutionHasDeadlocked(ops);820                }821                if (this.Configuration.IsLivenessCheckingEnabled && this.Scheduler.IsScheduleFair)822                {823                    // Check if the liveness threshold has been reached if scheduling is fair.824                    this.CheckLivenessThresholdExceeded();825                }826                if (!this.Scheduler.GetNextOperation(ops, current, isYielding, out ControlledOperation next))827                {828                    // The scheduler hit the scheduling steps bound.829                    this.Detach(ExecutionStatus.BoundReached);830                }831                IO.Debug.WriteLine("[coyote::debug] Scheduling operation '{0}' of group '{1}'.", next.Name, next.Group);832                if (current != next)833                {834                    // Pause the currently scheduled operation, and enable the next one.835                    this.ScheduledOperation = next;836                    next.Signal();837                    this.PauseOperation(current);838                }839                else if (isThreadUncontrolled)840                {841                    // If the current operation is the next operation to schedule, and the current thread842                    // is uncontrolled, then we need to signal the current operation to resume execution.843                    next.Signal();844                }845            }846        }847        /// <summary>848        /// Delays the currently executing operation for a non-deterministically chosen amount of time.849        /// </summary>850        /// <remarks>851        /// The delay is chosen non-deterministically by an underlying fuzzing strategy.852        /// If a delay of 0 is chosen, then the operation is not delayed.853        /// </remarks>854        internal void DelayOperation(ControlledOperation current)855        {856            using (SynchronizedSection.Enter(this.RuntimeLock))857            {858                if (this.ExecutionStatus != ExecutionStatus.Running)859                {860                    throw new ThreadInterruptedException();861                }862                if (current != null || this.TryGetExecutingOperation(out current))863                {864                    // Choose the next delay to inject. The value is in milliseconds.865                    int delay = this.GetNondeterministicDelay(current, (int)this.Configuration.MaxFuzzingDelay);866                    IO.Debug.WriteLine("[coyote::debug] Delaying operation '{0}' on thread '{1}' by {2}ms.",867                        current.Name, Thread.CurrentThread.ManagedThreadId, delay);868                    // Only sleep the executing operation if a non-zero delay was chosen.869                    if (delay > 0)870                    {871                        var previousStatus = current.Status;872                        current.Status = OperationStatus.PausedOnDelay;873                        using (SynchronizedSection.Exit(this.RuntimeLock))874                        {875                            Thread.SpinWait(delay);876                        }877                        current.Status = previousStatus;878                    }879                }880            }881        }882        /// <summary>883        /// Completes the specified operation.884        /// </summary>885        internal void CompleteOperation(ControlledOperation op)886        {887            op.ExecuteContinuations();888            using (SynchronizedSection.Enter(this.RuntimeLock))889            {890                IO.Debug.WriteLine("[coyote::debug] Completed operation '{0}' of group '{1}' on thread '{2}'.",891                    op.Name, op.Group, Thread.CurrentThread.ManagedThreadId);892                op.Status = OperationStatus.Completed;893            }894        }895        /// <summary>896        /// Tries to reset the specified controlled operation so that it can start executing again.897        /// This is only allowed if the operation is already completed.898        /// </summary>899        /// <param name="op">The operation to reset.</param>900        internal bool TryResetOperation(ControlledOperation op)901        {902            using (SynchronizedSection.Enter(this.RuntimeLock))903            {904                if (op.Status is OperationStatus.Completed)905                {906                    IO.Debug.WriteLine("[coyote::debug] Resetting operation '{0}' of group '{1}' from thread '{2}'.",907                        op.Name, op.Group, Thread.CurrentThread.ManagedThreadId);908                    op.Status = OperationStatus.None;909                    if (this.SchedulingPolicy is SchedulingPolicy.Interleaving)910                    {911                        // Assign an event handler so that the next scheduling decision cannot be912                        // made until this operation starts executing to avoid race conditions.913                        this.PendingStartOperationMap.Add(op, new ManualResetEventSlim(false));914                    }915                    return true;916                }917            }918            return false;919        }920        /// <summary>921        /// Suppresses scheduling points until <see cref="ResumeScheduling"/> is invoked,922        /// unless a scheduling point must occur naturally.923        /// </summary>924        internal void SuppressScheduling()925        {926            using (SynchronizedSection.Enter(this.RuntimeLock))927            {928                IO.Debug.WriteLine("[coyote::debug] Suppressing scheduling of enabled operations in runtime '{0}'.", this.Id);929                this.IsSchedulerSuppressed = true;930            }931        }932        /// <summary>933        /// Resumes scheduling points that were suppressed by invoking <see cref="SuppressScheduling"/>.934        /// </summary>935        internal void ResumeScheduling()936        {937            using (SynchronizedSection.Enter(this.RuntimeLock))938            {939                IO.Debug.WriteLine("[coyote::debug] Resuming scheduling of enabled operations in runtime '{0}'.", this.Id);940                this.IsSchedulerSuppressed = false;941            }942        }943        /// <summary>944        /// Sets a checkpoint in the currently explored execution trace, that allows replaying all945        /// scheduling decisions until the checkpoint in subsequent iterations.946        /// </summary>947        internal void CheckpointExecutionTrace()948        {949            using (SynchronizedSection.Enter(this.RuntimeLock))950            {951                ExecutionTrace trace = this.Scheduler.CheckpointExecutionTrace();952                IO.Debug.WriteLine("[coyote::debug] Set checkpoint in current execution path with length '{0}' in runtime '{1}'.",953                    trace.Length, this.Id);954            }955        }956        /// <inheritdoc/>957        public bool RandomBoolean() => this.GetNextNondeterministicBooleanChoice(null, null);958        /// <summary>959        /// Returns the next nondeterministic boolean choice.960        /// </summary>961        internal bool GetNextNondeterministicBooleanChoice(string callerName, string callerType)962        {963            using (SynchronizedSection.Enter(this.RuntimeLock))964            {965                bool result;966                if (this.SchedulingPolicy is SchedulingPolicy.Interleaving)967                {968                    // Checks if the current operation is controlled by the runtime.969                    this.GetExecutingOperation();970                    // Checks if the scheduling steps bound has been reached.971                    this.CheckIfSchedulingStepsBoundIsReached();972                    if (this.SchedulingPolicy is SchedulingPolicy.Interleaving &&973                        this.Configuration.IsLivenessCheckingEnabled && this.Scheduler.IsScheduleFair)974                    {975                        // Check if the liveness threshold has been reached if scheduling is fair.976                        this.CheckLivenessThresholdExceeded();977                    }978                    if (this.Configuration.IsProgramStateHashingEnabled)979                    {980                        // Update the current operation with the hashed program state.981                        this.ScheduledOperation.LastHashedProgramState = this.GetHashedProgramState();982                    }983                    if (!this.Scheduler.GetNextBoolean(this.ScheduledOperation, out result))984                    {985                        this.Detach(ExecutionStatus.BoundReached);986                    }987                }988                else989                {990                    result = this.ValueGenerator.Next(2) is 0 ? true : false;991                }992                this.LogWriter.LogRandom(result, callerName, callerType);993                return result;994            }995        }996        /// <inheritdoc/>997        public int RandomInteger(int maxValue) => this.GetNextNondeterministicIntegerChoice(maxValue, null, null);998        /// <summary>999        /// Returns the next nondeterministic integer choice.1000        /// </summary>1001        internal int GetNextNondeterministicIntegerChoice(int maxValue, string callerName, string callerType)1002        {1003            using (SynchronizedSection.Enter(this.RuntimeLock))1004            {1005                int result;1006                if (this.SchedulingPolicy is SchedulingPolicy.Interleaving)1007                {1008                    // Checks if the current operation is controlled by the runtime.1009                    this.GetExecutingOperation();1010                    // Checks if the scheduling steps bound has been reached.1011                    this.CheckIfSchedulingStepsBoundIsReached();1012                    if (this.SchedulingPolicy is SchedulingPolicy.Interleaving &&1013                        this.Configuration.IsLivenessCheckingEnabled && this.Scheduler.IsScheduleFair)1014                    {1015                        // Check if the liveness threshold has been reached if scheduling is fair.1016                        this.CheckLivenessThresholdExceeded();1017                    }1018                    if (this.Configuration.IsProgramStateHashingEnabled)1019                    {1020                        // Update the current operation with the hashed program state.1021                        this.ScheduledOperation.LastHashedProgramState = this.GetHashedProgramState();1022                    }1023                    if (!this.Scheduler.GetNextInteger(this.ScheduledOperation, maxValue, out result))1024                    {1025                        this.Detach(ExecutionStatus.BoundReached);1026                    }1027                }1028                else1029                {1030                    result = this.ValueGenerator.Next(maxValue);1031                }1032                this.LogWriter.LogRandom(result, callerName, callerType);1033                return result;1034            }1035        }1036        /// <summary>1037        /// Returns a controlled nondeterministic delay for the specified operation.1038        /// </summary>1039        private int GetNondeterministicDelay(ControlledOperation op, int maxDelay)1040        {1041            using (SynchronizedSection.Enter(this.RuntimeLock))1042            {1043                // Checks if the scheduling steps bound has been reached.1044                this.CheckIfSchedulingStepsBoundIsReached();1045                // Choose the next delay to inject.1046                if (!this.Scheduler.GetNextDelay(this.OperationMap.Values, op, maxDelay, out int next))1047                {1048                    this.Detach(ExecutionStatus.BoundReached);1049                }1050                return next;1051            }1052        }1053        /// <summary>1054        /// Tries to enable any operations that have their dependencies resolved. It returns1055        /// true if there is at least one operation enabled, else false.1056        /// </summary>1057        /// <remarks>1058        /// It is assumed that this method runs in the scope of a <see cref="SynchronizedSection"/>.1059        /// </remarks>1060        private bool TryEnableOperationsWithResolvedDependencies(ControlledOperation current)1061        {1062            IO.Debug.WriteLine("[coyote::debug] Trying to enable any operation with resolved dependencies in runtime '{0}'.", this.Id);1063            int attempt = 0;1064            int delay = (int)this.Configuration.UncontrolledConcurrencyResolutionDelay;1065            uint maxAttempts = this.Configuration.UncontrolledConcurrencyResolutionAttempts;1066            uint enabledOpsCount = 0;1067            while (true)1068            {1069                // Cache the count of enabled operations from the previous attempt.1070                uint previousEnabledOpsCount = enabledOpsCount;1071                enabledOpsCount = 0;1072                uint statusChanges = 0;1073                bool isRootDependencyUnresolved = false;1074                bool isAnyDependencyUnresolved = false;1075                foreach (var op in this.OperationMap.Values)1076                {1077                    var previousStatus = op.Status;1078                    if (op.IsPaused)1079                    {1080                        this.TryEnableOperation(op);1081                        if (previousStatus == op.Status)1082                        {1083                            IO.Debug.WriteLine("[coyote::debug] Operation '{0}' of group '{1}' has status '{2}'.",1084                                op.Name, op.Group, op.Status);1085                            if (op.IsPaused && op.IsDependencyUncontrolled)1086                            {1087                                if (op.IsRoot)1088                                {1089                                    isRootDependencyUnresolved = true;1090                                }1091                                else1092                                {1093                                    isAnyDependencyUnresolved = true;1094                                }1095                            }1096                        }1097                        else1098                        {1099                            IO.Debug.WriteLine("[coyote::debug] Operation '{0}' of group '{1}' changed status from '{2}' to '{3}'.",1100                                op.Name, op.Group, previousStatus, op.Status);1101                            statusChanges++;1102                        }1103                    }1104                    if (op.Status is OperationStatus.Enabled)1105                    {1106                        enabledOpsCount++;1107                    }1108                }1109                // Heuristics for handling a partially controlled execution.1110                if (this.IsUncontrolledConcurrencyDetected &&1111                    this.Configuration.IsPartiallyControlledConcurrencyAllowed)1112                {1113                    // Compute the delta of enabled operations from the previous attempt.1114                    uint enabledOpsDelta = attempt is 0 ? 0 : enabledOpsCount - previousEnabledOpsCount;1115                    // This value is true if the current operation just completed and has uncontrolled source.1116                    bool isSourceUnresolved = current.Status is OperationStatus.Completed && current.IsSourceUncontrolled;1117                    // We consider the concurrency to be unresolved if there were no new enabled operations1118                    // or status changes in this attempt, and one of the following cases holds:1119                    // - If there are no enabled operations, then the concurrency is unresolved if1120                    //   the current operation was just completed and has uncontrolled source, or1121                    //   if there are any unresolved dependencies.1122                    // - If there are enabled operations, then the concurrency is unresolved if1123                    //   there are any (non-root) unresolved dependencies.1124                    bool isNoEnabledOpsCaseResolved = enabledOpsCount is 0 &&1125                        (isSourceUnresolved || isAnyDependencyUnresolved || isRootDependencyUnresolved);1126                    bool isSomeEnabledOpsCaseResolved = enabledOpsCount > 0 && isAnyDependencyUnresolved;1127                    bool isConcurrencyUnresolved = enabledOpsDelta is 0 && statusChanges is 0 &&1128                        (isNoEnabledOpsCaseResolved || isSomeEnabledOpsCaseResolved);1129                    // Retry if there is unresolved concurrency and attempts left.1130                    if (++attempt < maxAttempts && isConcurrencyUnresolved)1131                    {1132                        // Implement a simple retry logic to try resolve uncontrolled concurrency.1133                        IO.Debug.WriteLine("[coyote::debug] Pausing controlled thread '{0}' to try resolve uncontrolled concurrency.",1134                            Thread.CurrentThread.ManagedThreadId);1135                        using (SynchronizedSection.Exit(this.RuntimeLock))1136                        {1137                            Thread.SpinWait(delay);1138                        }1139                        continue;1140                    }1141                }1142                break;1143            }1144            IO.Debug.WriteLine("[coyote::debug] There are {0} enabled operations in runtime '{1}'.", enabledOpsCount, this.Id);1145            this.MaxConcurrencyDegree = Math.Max(this.MaxConcurrencyDegree, enabledOpsCount);1146            return enabledOpsCount > 0;1147        }1148        /// <summary>1149        /// Tries to enable the specified operation, if its dependencies have been resolved.1150        /// </summary>1151        /// <remarks>1152        /// It is assumed that this method runs in the scope of a <see cref="SynchronizedSection"/>.1153        /// </remarks>1154        private bool TryEnableOperation(ControlledOperation op)1155        {1156            if (op.Status is OperationStatus.PausedOnDelay && op is DelayOperation delayedOp)1157            {1158                if (delayedOp.Delay > 0)1159                {1160                    delayedOp.Delay--;1161                }1162                // The operation is delayed, so it is enabled either if the delay completes1163                // or if no other operation is enabled.1164                if (delayedOp.Delay is 0 ||1165                    !this.OperationMap.Any(kvp => kvp.Value.Status is OperationStatus.Enabled))1166                {1167                    delayedOp.Delay = 0;1168                    delayedOp.Status = OperationStatus.Enabled;1169                    return true;1170                }1171                return false;1172            }1173            // If the operation is paused, then check if its dependency has been resolved.1174            return op.TryEnable();1175        }1176        /// <summary>1177        /// Pauses the scheduled controlled operation until either the uncontrolled task completes,1178        /// it tries to invoke an uncontrolled scheduling point, or the timeout expires.1179        /// </summary>1180        /// <remarks>1181        /// It is assumed that this method runs in the scope of a <see cref="SynchronizedSection"/>.1182        /// </remarks>1183        private void TryPauseAndResolveUncontrolledTask(Task task)1184        {1185            if (this.IsThreadControlled(Thread.CurrentThread))1186            {1187                // A scheduling point from an uncontrolled thread has not been postponed yet, so pause the execution1188                // of the current operation to try give time to the uncontrolled concurrency to be resolved.1189                if (this.LastPostponedSchedulingPoint is null)1190                {1191                    int attempt = 0;1192                    int delay = (int)this.Configuration.UncontrolledConcurrencyResolutionDelay;1193                    uint maxAttempts = this.Configuration.UncontrolledConcurrencyResolutionAttempts;1194                    while (attempt++ < maxAttempts && !task.IsCompleted)1195                    {1196                        IO.Debug.WriteLine("[coyote::debug] Pausing controlled thread '{0}' to try resolve uncontrolled concurrency.",1197                            Thread.CurrentThread.ManagedThreadId);1198                        using (SynchronizedSection.Exit(this.RuntimeLock))1199                        {1200                            Thread.SpinWait(delay);1201                        }1202                        if (this.LastPostponedSchedulingPoint.HasValue)1203                        {1204                            // A scheduling point from an uncontrolled thread has been postponed,1205                            // so stop trying to resolve the uncontrolled concurrency.1206                            break;1207                        }1208                    }1209                }1210                if (this.LastPostponedSchedulingPoint.HasValue)1211                {1212                    IO.Debug.WriteLine("[coyote::debug] Resuming controlled thread '{0}' with uncontrolled concurrency resolved.",1213                        Thread.CurrentThread.ManagedThreadId);1214                    this.ScheduleNextOperation(default, this.LastPostponedSchedulingPoint.Value, isSuppressible: false);1215                }1216            }1217        }1218        /// <summary>1219        /// Returns the currently executing <see cref="ControlledOperation"/>,1220        /// or null if no such operation is executing.1221        /// </summary>1222        internal ControlledOperation GetExecutingOperation()1223        {1224            using (SynchronizedSection.Enter(this.RuntimeLock))1225            {1226                var op = ExecutingOperation.Value;1227                if (op is null)1228                {1229                    this.NotifyUncontrolledCurrentThread();1230                }1231                return op;1232            }1233        }1234        /// <summary>1235        /// Returns the currently executing <see cref="ControlledOperation"/> of the1236        /// specified type, or null if no such operation is executing.1237        /// </summary>1238        internal TControlledOperation GetExecutingOperation<TControlledOperation>()1239            where TControlledOperation : ControlledOperation1240        {1241            using (SynchronizedSection.Enter(this.RuntimeLock))1242            {1243                var op = ExecutingOperation.Value;1244                if (op is null)1245                {1246                    this.NotifyUncontrolledCurrentThread();1247                }1248                return op is TControlledOperation expected ? expected : default;1249            }1250        }1251        /// <summary>1252        /// Tries to return the currently executing <see cref="ControlledOperation"/>,1253        /// or false if no such operation is executing.1254        /// </summary>1255        internal bool TryGetExecutingOperation(out ControlledOperation op)1256        {1257            op = this.GetExecutingOperation();1258            return op != null;1259        }1260        /// <summary>1261        /// Returns the <see cref="ControlledOperation"/> associated with the specified1262        /// operation id, or null if no such operation exists.1263        /// </summary>1264        internal ControlledOperation GetOperationWithId(ulong operationId)1265        {1266            using (SynchronizedSection.Enter(this.RuntimeLock))1267            {1268                this.OperationMap.TryGetValue(operationId, out ControlledOperation op);1269                return op;1270            }1271        }1272        /// <summary>1273        /// Returns the <see cref="ControlledOperation"/> of the specified type that is associated1274        /// with the specified operation id, or null if no such operation exists.1275        /// </summary>1276        internal TControlledOperation GetOperationWithId<TControlledOperation>(ulong operationId)1277            where TControlledOperation : ControlledOperation1278        {1279            using (SynchronizedSection.Enter(this.RuntimeLock))1280            {1281                if (this.OperationMap.TryGetValue(operationId, out ControlledOperation op) &&1282                    op is TControlledOperation expected)1283                {1284                    return expected;1285                }1286            }1287            return default;1288        }1289        /// <summary>1290        /// Returns all registered operations.1291        /// </summary>1292        /// <remarks>1293        /// This operation is thread safe because the systematic testing1294        /// runtime serializes the execution.1295        /// </remarks>1296        private IEnumerable<ControlledOperation> GetRegisteredOperations()1297        {1298            using (SynchronizedSection.Enter(this.RuntimeLock))1299            {1300                return this.OperationMap.Values;1301            }1302        }1303        /// <summary>1304        /// Returns the next available unique operation id.1305        /// </summary>1306        /// <returns>Value representing the next available unique operation id.</returns>1307        internal ulong GetNextOperationId() =>1308            // Atomically increments and safely wraps the value into an unsigned long.1309            (ulong)Interlocked.Increment(ref this.OperationIdCounter) - 1;1310        /// <summary>1311        /// Returns the current hashed state of the execution.1312        /// </summary>1313        /// <remarks>1314        /// The hash is updated in each execution step.1315        /// </remarks>1316        private int GetHashedProgramState()1317        {1318            unchecked1319            {1320                int hash = 19;1321                foreach (var operation in this.GetRegisteredOperations().OrderBy(op => op.Id))1322                {1323                    if (operation is ActorOperation actorOperation)1324                    {1325                        int operationHash = 31 + actorOperation.Actor.GetHashedState(this.SchedulingPolicy);1326                        operationHash = (operationHash * 31) + actorOperation.LastSchedulingPoint.GetHashCode();1327                        hash *= operationHash;1328                    }1329                    else1330                    {1331                        hash *= 31 + operation.LastSchedulingPoint.GetHashCode();1332                    }1333                }1334                foreach (var monitor in this.SpecificationMonitors)1335                {1336                    hash *= 31 + monitor.GetHashedState();1337                }1338                return hash;1339            }1340        }1341        /// <inheritdoc/>1342        public void RegisterMonitor<T>()1343            where T : Specifications.Monitor =>1344            this.TryCreateMonitor(typeof(T));1345        /// <summary>1346        /// Tries to create a new <see cref="Specifications.Monitor"/> of the specified <see cref="Type"/>.1347        /// </summary>1348        private bool TryCreateMonitor(Type type)1349        {1350            if (this.SchedulingPolicy != SchedulingPolicy.None ||1351                this.Configuration.IsMonitoringEnabledInInProduction)1352            {1353                using (SynchronizedSection.Enter(this.RuntimeLock))1354                {1355                    // Only one monitor per type is allowed.1356                    if (!this.SpecificationMonitors.Any(m => m.GetType() == type))1357                    {1358                        var monitor = (Specifications.Monitor)Activator.CreateInstance(type);1359                        monitor.Initialize(this.Configuration, this, this.LogWriter);1360                        monitor.InitializeStateInformation();1361                        this.SpecificationMonitors.Add(monitor);1362                        if (this.SchedulingPolicy is SchedulingPolicy.Interleaving)1363                        {1364                            this.SuppressScheduling();1365                            this.IsSpecificationInvoked = true;1366                            monitor.GotoStartState();1367                            this.IsSpecificationInvoked = false;1368                            this.ResumeScheduling();1369                        }1370                        else1371                        {1372                            monitor.GotoStartState();1373                        }1374                        return true;1375                    }1376                }1377            }1378            return false;1379        }1380        /// <inheritdoc/>1381        public void Monitor<T>(Event e)1382            where T : Specifications.Monitor =>1383            this.InvokeMonitor(typeof(T), e, null, null, null);1384        /// <summary>1385        /// Invokes the specified <see cref="Specifications.Monitor"/> with the specified <see cref="Event"/>.1386        /// </summary>1387        internal void InvokeMonitor(Type type, Event e, string senderName, string senderType, string senderStateName)1388        {1389            if (this.SchedulingPolicy != SchedulingPolicy.None ||1390                this.Configuration.IsMonitoringEnabledInInProduction)1391            {1392                using (SynchronizedSection.Enter(this.RuntimeLock))1393                {1394                    Specifications.Monitor monitor = null;1395                    foreach (var m in this.SpecificationMonitors)1396                    {1397                        if (m.GetType() == type)1398                        {1399                            monitor = m;1400                            break;1401                        }1402                    }1403                    if (monitor != null)1404                    {1405                        this.Assert(e != null, "Cannot invoke monitor '{0}' with a null event.", type.FullName);1406                        if (this.SchedulingPolicy is SchedulingPolicy.Interleaving)1407                        {1408                            this.SuppressScheduling();1409                            this.IsSpecificationInvoked = true;1410                            monitor.MonitorEvent(e, senderName, senderType, senderStateName);1411                            this.IsSpecificationInvoked = false;1412                            this.ResumeScheduling();1413                        }1414                        else1415                        {1416                            monitor.MonitorEvent(e, senderName, senderType, senderStateName);1417                        }1418                    }1419                }1420            }1421        }1422        /// <inheritdoc/>1423        public void Assert(bool predicate)1424        {1425            if (!predicate)1426            {1427                string msg = "Detected an assertion failure.";1428                if (this.SchedulingPolicy is SchedulingPolicy.None)1429                {1430                    throw new AssertionFailureException(msg);1431                }1432                this.NotifyAssertionFailure(msg);1433            }1434        }1435        /// <inheritdoc/>1436        public void Assert(bool predicate, string s, object arg0)1437        {1438            if (!predicate)1439            {1440                var msg = string.Format(CultureInfo.InvariantCulture, s, arg0?.ToString());1441                if (this.SchedulingPolicy is SchedulingPolicy.None)1442                {1443                    throw new AssertionFailureException(msg);1444                }1445                this.NotifyAssertionFailure(msg);1446            }1447        }1448        /// <inheritdoc/>1449        public void Assert(bool predicate, string s, object arg0, object arg1)1450        {1451            if (!predicate)1452            {1453                var msg = string.Format(CultureInfo.InvariantCulture, s, arg0?.ToString(), arg1?.ToString());1454                if (this.SchedulingPolicy is SchedulingPolicy.None)1455                {1456                    throw new AssertionFailureException(msg);1457                }1458                this.NotifyAssertionFailure(msg);1459            }1460        }1461        /// <inheritdoc/>1462        public void Assert(bool predicate, string s, object arg0, object arg1, object arg2)1463        {1464            if (!predicate)1465            {1466                var msg = string.Format(CultureInfo.InvariantCulture, s, arg0?.ToString(), arg1?.ToString(), arg2?.ToString());1467                if (this.SchedulingPolicy is SchedulingPolicy.None)1468                {1469                    throw new AssertionFailureException(msg);1470                }1471                this.NotifyAssertionFailure(msg);1472            }1473        }1474        /// <inheritdoc/>1475        public void Assert(bool predicate, string s, params object[] args)1476        {1477            if (!predicate)1478            {1479                var msg = string.Format(CultureInfo.InvariantCulture, s, args);1480                if (this.SchedulingPolicy is SchedulingPolicy.None)1481                {1482                    throw new AssertionFailureException(msg);1483                }1484                this.NotifyAssertionFailure(msg);1485            }1486        }1487        /// <summary>1488        /// Creates a liveness monitor that checks if the specified task eventually completes execution successfully.1489        /// </summary>1490        internal void MonitorTaskCompletion(Task task)1491        {1492            if (this.SchedulingPolicy is SchedulingPolicy.Interleaving &&1493                task.Status != TaskStatus.RanToCompletion)1494            {1495                var monitor = new TaskLivenessMonitor(task);1496                this.TaskLivenessMonitors.Add(monitor);1497            }1498        }1499        /// <summary>1500        /// Starts running a background monitor that checks for potential deadlocks.1501        /// </summary>1502        private void StartMonitoringDeadlocks() => Task.Factory.StartNew(this.CheckIfExecutionHasDeadlockedAsync,1503            this.CancellationSource.Token, TaskCreationOptions.LongRunning, TaskScheduler.Default);1504        /// <summary>1505        /// Returns true if the specified thread is controlled, else false.1506        /// </summary>1507        private bool IsThreadControlled(Thread thread)1508        {1509            string name = thread?.Name;1510            return name != null && this.ControlledThreads.ContainsKey(name);1511        }1512        /// <summary>1513        /// Returns true if the specified task is uncontrolled, else false.1514        /// </summary>1515        internal bool IsTaskUncontrolled(Task task) =>1516            task != null && !task.IsCompleted && !this.ControlledTasks.ContainsKey(task);1517        /// <summary>1518        /// Checks if the awaited task is uncontrolled.1519        /// </summary>1520        internal bool CheckIfAwaitedTaskIsUncontrolled(Task task)1521        {1522            if (this.IsTaskUncontrolled(task))1523            {1524                this.NotifyUncontrolledTaskWait(task);1525                return true;1526            }1527            return false;1528        }1529        /// <summary>1530        /// Checks if the task returned from the specified method is uncontrolled.1531        /// </summary>1532        internal bool CheckIfReturnedTaskIsUncontrolled(Task task, string methodName)1533        {1534            if (this.IsTaskUncontrolled(task))1535            {1536                this.NotifyUncontrolledTaskReturned(task, methodName);1537                return true;1538            }1539            return false;1540        }1541        /// <summary>1542        /// Checks if the execution has deadlocked. This happens when there are no more enabled operations,1543        /// but there is one or more paused operations that are waiting some resource to complete.1544        /// </summary>1545        private void CheckIfExecutionHasDeadlocked(IEnumerable<ControlledOperation> ops)1546        {1547            if (ops.Any(op => op.Status is OperationStatus.Enabled))1548            {1549                // There are still enabled operations, so the execution is not deadlocked.1550                return;1551            }1552            var pausedOperations = ops.Where(op => op.Status is OperationStatus.Paused).ToList();1553            var pausedOnResources = ops.Where(op => op.Status is OperationStatus.PausedOnResource).ToList();1554            var pausedOnReceiveOperations = ops.Where(op => op.Status is OperationStatus.PausedOnReceive).ToList();1555            var totalCount = pausedOperations.Count + pausedOnResources.Count + pausedOnReceiveOperations.Count;1556            if (totalCount is 0)1557            {1558                // There are no paused operations, so the execution is not deadlocked.1559                return;1560            }1561            // To simplify the error message, remove the root operation, unless it is the only one that is paused.1562            if (totalCount > 1)1563            {1564                pausedOperations.RemoveAll(op => op.IsRoot);1565                pausedOnResources.RemoveAll(op => op.IsRoot);1566                pausedOnReceiveOperations.RemoveAll(op => op.IsRoot);1567            }1568            StringBuilder msg;1569            if (this.IsUncontrolledConcurrencyDetected)1570            {1571                msg = new StringBuilder("Potential deadlock detected.");1572            }1573            else1574            {1575                msg = new StringBuilder("Deadlock detected.");1576            }1577            if (pausedOperations.Count > 0)1578            {1579                for (int idx = 0; idx < pausedOperations.Count; idx++)1580                {1581                    msg.Append(string.Format(CultureInfo.InvariantCulture, " {0}", pausedOperations[idx].Name));1582                    if (idx == pausedOperations.Count - 2)1583                    {1584                        msg.Append(" and");1585                    }1586                    else if (idx < pausedOperations.Count - 1)1587                    {1588                        msg.Append(',');1589                    }1590                }1591                msg.Append(pausedOperations.Count is 1 ? " is " : " are ");1592                msg.Append("paused on a dependency, but no other controlled operations are enabled.");1593            }1594            if (pausedOnResources.Count > 0)1595            {1596                for (int idx = 0; idx < pausedOnResources.Count; idx++)1597                {1598                    msg.Append(string.Format(CultureInfo.InvariantCulture, " {0}", pausedOnResources[idx].Name));1599                    if (idx == pausedOnResources.Count - 2)1600                    {1601                        msg.Append(" and");1602                    }1603                    else if (idx < pausedOnResources.Count - 1)1604                    {1605                        msg.Append(',');1606                    }1607                }1608                msg.Append(pausedOnResources.Count is 1 ? " is " : " are ");1609                msg.Append("waiting to acquire a resource that is already acquired, ");1610                msg.Append("but no other controlled operations are enabled.");1611            }1612            if (pausedOnReceiveOperations.Count > 0)1613            {1614                for (int idx = 0; idx < pausedOnReceiveOperations.Count; idx++)1615                {1616                    msg.Append(string.Format(CultureInfo.InvariantCulture, " {0}", pausedOnReceiveOperations[idx].Name));1617                    if (idx == pausedOnReceiveOperations.Count - 2)1618                    {1619                        msg.Append(" and");1620                    }1621                    else if (idx < pausedOnReceiveOperations.Count - 1)1622                    {1623                        msg.Append(',');1624                    }1625                }1626                msg.Append(pausedOnReceiveOperations.Count is 1 ? " is " : " are ");1627                msg.Append("waiting to receive an event, but no other controlled operations are enabled.");1628            }1629            if (this.IsUncontrolledConcurrencyDetected)1630            {1631                msg.Append(" Due to the presence of uncontrolled concurrency in the test, ");1632                msg.Append("Coyote cannot accurately determine if this is a real deadlock or not.");1633                if (!this.Configuration.ReportPotentialDeadlocksAsBugs)1634                {1635                    this.Logger.WriteLine($"[coyote::test] {msg}");1636                    this.Detach(ExecutionStatus.Deadlocked);1637                }1638                msg.Append(" If you believe that this is not a real deadlock, you can disable reporting ");1639                msg.Append("potential deadlocks as bugs by setting '--skip-potential-deadlocks' or ");1640                msg.Append("'Configuration.WithPotentialDeadlocksReportedAsBugs(false)'.");1641            }1642            this.NotifyAssertionFailure(msg.ToString());1643        }1644        /// <summary>1645        /// Periodically checks if the execution has deadlocked.1646        /// </summary>1647        private async Task CheckIfExecutionHasDeadlockedAsync()1648        {1649            var info = new SchedulingActivityInfo();1650            IO.Debug.WriteLine("[coyote::debug] Started periodic monitoring for potential deadlocks in runtime '{0}'.", this.Id);1651            while (true)1652            {1653                try1654                {1655                    await Task.Delay(TimeSpan.FromMilliseconds(this.Configuration.DeadlockTimeout), this.CancellationSource.Token);1656                    using (SynchronizedSection.Enter(this.RuntimeLock))1657                    {1658                        if (this.ExecutionStatus != ExecutionStatus.Running)1659                        {1660                            break;1661                        }1662                        if (info.OperationCount == this.OperationMap.Count &&1663                            info.StepCount == this.Scheduler.StepCount)1664                        {1665                            string msg = "Potential deadlock detected. The periodic deadlock detection monitor was used, " +1666                                "so Coyote cannot accurately determine if this is a real deadlock or not. If you believe " +1667                                "that this is not a real deadlock, you can try increase the deadlock detection timeout " +1668                                "by setting '--deadlock-timeout N' or 'Configuration.WithDeadlockTimeout(N)'.";1669                            if (this.Configuration.ReportPotentialDeadlocksAsBugs)1670                            {1671                                msg += " Alternatively, you can disable reporting potential deadlocks as bugs by setting " +1672                                "'--skip-potential-deadlocks' or 'Configuration.WithPotentialDeadlocksReportedAsBugs(false)'.";1673                                this.NotifyAssertionFailure(msg);1674                            }1675                            else1676                            {1677                                this.Logger.WriteLine($"[coyote::test] {msg}");1678                                this.Detach(ExecutionStatus.Deadlocked);1679                            }1680                        }1681                        else1682                        {1683                            // Passed check, so continue with the next timeout period.1684                            IO.Debug.WriteLine("[coyote::debug] Passed periodic check for potential deadlocks in runtime '{0}'.", this.Id);1685                            info.OperationCount = this.OperationMap.Count;1686                            info.StepCount = this.Scheduler.StepCount;1687                            if (this.LastPostponedSchedulingPoint is SchedulingPointType.Pause ||1688                                this.LastPostponedSchedulingPoint is SchedulingPointType.Complete)1689                            {1690                                // A scheduling point was postponed due to a potential deadlock, so try to check if it has been resolved.1691                                this.ScheduleNextOperation(default, this.LastPostponedSchedulingPoint.Value, isSuppressible: false);1692                            }1693                        }1694                    }1695                }1696                catch (TaskCanceledException)1697                {1698                    break;1699                }1700            }1701        }1702        /// <summary>1703        /// Checks for liveness errors.1704        /// </summary>1705#if !DEBUG1706        [DebuggerHidden]1707#endif1708        internal void CheckLivenessErrors()1709        {1710            foreach (var monitor in this.TaskLivenessMonitors)1711            {1712                if (!monitor.IsSatisfied)1713                {1714                    string msg = string.Format(CultureInfo.InvariantCulture,1715                        "Found liveness bug at the end of program execution.\nThe stack trace is:\n{0}",1716                        FormatSpecificationMonitorStackTrace(monitor.StackTrace));1717                    this.NotifyAssertionFailure(msg);1718                }1719            }1720            // Checks if there is a specification monitor stuck in a hot state.1721            foreach (var monitor in this.SpecificationMonitors)1722            {1723                if (monitor.IsInHotState(out string stateName))1724                {1725                    string msg = string.Format(CultureInfo.InvariantCulture,1726                        "{0} detected liveness bug in hot state '{1}' at the end of program execution.",1727                        monitor.GetType().FullName, stateName);1728                    this.NotifyAssertionFailure(msg);1729                }1730            }1731        }1732        /// <summary>1733        /// Checks if a liveness monitor exceeded its threshold and, if yes, it reports an error.1734        /// </summary>1735        internal void CheckLivenessThresholdExceeded()1736        {1737            foreach (var monitor in this.TaskLivenessMonitors)1738            {1739                if (monitor.IsLivenessThresholdExceeded(this.Configuration.LivenessTemperatureThreshold))1740                {1741                    string msg = string.Format(CultureInfo.InvariantCulture,1742                        "Found potential liveness bug at the end of program execution.\nThe stack trace is:\n{0}",1743                        FormatSpecificationMonitorStackTrace(monitor.StackTrace));1744                    this.NotifyAssertionFailure(msg);1745                }1746            }1747            foreach (var monitor in this.SpecificationMonitors)1748            {1749                if (monitor.IsLivenessThresholdExceeded(this.Configuration.LivenessTemperatureThreshold))1750                {1751                    string msg = $"{monitor.Name} detected potential liveness bug in hot state '{monitor.CurrentStateName}'.";1752                    this.NotifyAssertionFailure(msg);1753                }1754            }1755        }1756        /// <summary>1757        /// Checks if the scheduling steps bound has been reached. If yes,1758        /// it stops the scheduler and kills all enabled machines.1759        /// </summary>1760        private void CheckIfSchedulingStepsBoundIsReached()1761        {1762            if (this.Scheduler.IsMaxStepsReached)1763            {1764                string message = $"Scheduling steps bound of {this.Scheduler.StepCount} reached.";1765                if (this.Configuration.ConsiderDepthBoundHitAsBug)1766                {1767                    this.NotifyAssertionFailure(message);1768                }1769                else1770                {1771                    IO.Debug.WriteLine($"[coyote::debug] {message}");1772                    this.Detach(ExecutionStatus.BoundReached);1773                }1774            }1775        }1776        /// <summary>1777        /// Notify that an exception was not handled.1778        /// </summary>1779        internal void NotifyUnhandledException(Exception ex, string message)1780        {1781            using (SynchronizedSection.Enter(this.RuntimeLock))1782            {1783                if (this.ExecutionStatus != ExecutionStatus.Running)1784                {1785                    return;1786                }1787                if (this.UnhandledException is null)1788                {1789                    this.UnhandledException = ex;1790                }1791                this.NotifyAssertionFailure(message);1792            }1793        }1794        /// <summary>1795        /// Notify that an assertion has failed.1796        /// </summary>1797#if !DEBUG1798        [DebuggerHidden]1799#endif1800        internal void NotifyAssertionFailure(string text)1801        {1802            using (SynchronizedSection.Enter(this.RuntimeLock))1803            {1804                if (this.ExecutionStatus is ExecutionStatus.Running)1805                {1806                    this.BugReport = text;1807                    this.LogWriter.LogAssertionFailure($"[coyote::error] {text}");1808                    this.RaiseOnFailureEvent(new AssertionFailureException(text));1809                    if (this.Configuration.AttachDebugger)1810                    {1811                        Debugger.Break();1812                    }1813                    this.Detach(ExecutionStatus.BugFound);1814                }1815            }1816        }1817        /// <summary>1818        /// Notify that an uncontrolled invocation was detected.1819        /// </summary>1820        internal void NotifyUncontrolledInvocation(string methodName)1821        {1822            using (SynchronizedSection.Enter(this.RuntimeLock))1823            {1824                if (this.SchedulingPolicy != SchedulingPolicy.None)1825                {1826                    this.UncontrolledInvocations.Add(methodName);1827                }1828                if (this.SchedulingPolicy is SchedulingPolicy.Interleaving)1829                {1830                    string message = $"Invoking '{methodName}' is not intercepted and controlled during " +1831                        "testing, so it can interfere with the ability to reproduce bug traces.";1832                    this.TryHandleUncontrolledConcurrency(message, methodName);1833                }1834            }1835        }1836        /// <summary>1837        /// Notify that the currently executing thread is uncontrolled.1838        /// </summary>1839        private void NotifyUncontrolledCurrentThread()1840        {1841            if (this.SchedulingPolicy is SchedulingPolicy.Interleaving)1842            {1843                // TODO: figure out if there is a way to get more information about the creator of the1844                // uncontrolled thread to ease the user debugging experience.1845                string message = $"Executing thread '{Thread.CurrentThread.ManagedThreadId}' is not intercepted and " +1846                    "controlled during testing, so it can interfere with the ability to reproduce bug traces.";1847                this.TryHandleUncontrolledConcurrency(message);1848            }1849        }1850        /// <summary>1851        /// Notify that an uncontrolled task is being waited.1852        /// </summary>1853        private void NotifyUncontrolledTaskWait(Task task)1854        {1855            using (SynchronizedSection.Enter(this.RuntimeLock))1856            {1857                if (this.SchedulingPolicy is SchedulingPolicy.Interleaving)1858                {1859                    // TODO: figure out if there is a way to get more information about the creator of the1860                    // uncontrolled task to ease the user debugging experience.1861                    string message = $"Waiting task '{task.Id}' that is not intercepted and controlled during " +1862                        "testing, so it can interfere with the ability to reproduce bug traces.";1863                    if (this.TryHandleUncontrolledConcurrency(message) &&1864                        this.UncontrolledTasks.Add(task))1865                    {1866                        this.TryPauseAndResolveUncontrolledTask(task);1867                    }1868                }1869            }1870        }1871        /// <summary>1872        /// Notify that an uncontrolled task was returned.1873        /// </summary>1874        private void NotifyUncontrolledTaskReturned(Task task, string methodName)1875        {1876            using (SynchronizedSection.Enter(this.RuntimeLock))1877            {1878                if (this.SchedulingPolicy != SchedulingPolicy.None)1879                {1880                    this.UncontrolledInvocations.Add(methodName);1881                }1882                if (this.SchedulingPolicy is SchedulingPolicy.Interleaving)1883                {1884                    string message = $"Invoking '{methodName}' returned task '{task.Id}' that is not intercepted and " +1885                        "controlled during testing, so it can interfere with the ability to reproduce bug traces.";1886                    if (this.TryHandleUncontrolledConcurrency(message, methodName) &&1887                        this.UncontrolledTasks.Add(task))1888                    {1889                        this.TryPauseAndResolveUncontrolledTask(task);1890                    }1891                }1892            }1893        }1894        /// <summary>1895        /// Invoked when uncontrolled concurrency is detected. Based on the test configuration, it can try1896        /// handle the uncontrolled concurrency, else it terminates the current test iteration.1897        /// </summary>1898        private bool TryHandleUncontrolledConcurrency(string message, string methodName = default)1899        {1900            if (this.Configuration.IsPartiallyControlledConcurrencyAllowed)1901            {1902                IO.Debug.WriteLine($"[coyote::debug] {message}");1903                this.IsUncontrolledConcurrencyDetected = true;1904                return true;1905            }1906            else if (this.Configuration.IsSystematicFuzzingFallbackEnabled)1907            {1908                IO.Debug.WriteLine($"[coyote::debug] {message}");1909                this.IsUncontrolledConcurrencyDetected = true;1910                this.Detach(ExecutionStatus.ConcurrencyUncontrolled);1911            }1912            else1913            {1914                this.NotifyAssertionFailure(FormatUncontrolledConcurrencyExceptionMessage(message, methodName));1915            }1916            return false;1917        }1918        /// <summary>1919        /// Throws an <see cref="AssertionFailureException"/> exception containing the specified exception.1920        /// </summary>1921        internal void WrapAndThrowException(Exception exception, string s, params object[] args)1922        {1923            string msg = string.Format(CultureInfo.InvariantCulture, s, args);1924            string message = string.Format(CultureInfo.InvariantCulture,1925                "Exception '{0}' was thrown in {1}: {2}\n" +1926                "from location '{3}':\n" +1927                "The stack trace is:\n{4}",1928                exception.GetType(), msg, exception.Message, exception.Source, exception.StackTrace);1929            if (this.SchedulingPolicy is SchedulingPolicy.None)1930            {1931                throw new AssertionFailureException(message, exception);1932            }1933            this.NotifyUnhandledException(exception, message);1934        }1935        /// <summary>1936        /// Formats the message of the uncontrolled concurrency exception.1937        /// </summary>1938        private static string FormatUncontrolledConcurrencyExceptionMessage(string message, string methodName = default)1939        {1940            var mockMessage = methodName is null ? string.Empty : $" either replace or mock '{methodName}', or";1941            return $"{message} As a workaround, you can{mockMessage} use the '--no-repro' command line option " +1942                "(or the 'Configuration.WithNoBugTraceRepro()' method) to ignore this error by disabling bug " +1943                $"trace repro. Learn more at http://aka.ms/coyote-no-repro.\n{new StackTrace()}";1944        }1945        /// <summary>1946        /// Processes an unhandled exception in the specified controlled operation.1947        /// </summary>1948        internal void ProcessUnhandledExceptionInOperation(ControlledOperation op, Exception exception)1949        {1950            // Complete the failed operation. This is required so that the operation1951            // does not throw if it detaches.1952            op.Status = OperationStatus.Completed;1953            if (exception.GetBaseException() is ThreadInterruptedException)1954            {1955                // Ignore this exception, its thrown by the runtime.1956                IO.Debug.WriteLine("[coyote::debug] Controlled thread '{0}' executing operation '{1}' was interrupted.",1957                    Thread.CurrentThread.ManagedThreadId, op.Name);1958            }1959            else1960            {1961                string message;1962                string trace = FormatExceptionStackTrace(exception);1963                if (op is ActorOperation actorOp)1964                {1965                    message = string.Format(CultureInfo.InvariantCulture,1966                        $"Unhandled exception in actor '{actorOp.Name}'. {trace}");1967                }1968                else1969                {1970                    message = $"Unhandled exception. {trace}";1971                }1972                // Report the unhandled exception.1973                this.NotifyUnhandledException(exception, message);1974            }1975        }1976        /// <summary>1977        /// Formats the stack trace of the specified exception.1978        /// </summary>1979        private static string FormatExceptionStackTrace(Exception exception)1980        {1981            string[] lines = exception.ToString().Split(new[] { Environment.NewLine }, StringSplitOptions.None);1982            for (int i = 0; i < lines.Length; i++)1983            {1984                if (lines[i].StartsWith("   at Microsoft.Coyote.Rewriting", StringComparison.Ordinal))1985                {1986                    lines[i] = string.Empty;1987                }1988            }1989            return string.Join(Environment.NewLine, lines.Where(line => !string.IsNullOrEmpty(line)));1990        }1991        /// <summary>1992        /// Formats the specified stack trace of a specification monitor.1993        /// </summary>1994        private static string FormatSpecificationMonitorStackTrace(StackTrace trace)1995        {1996            StringBuilder sb = new StringBuilder();1997            string[] lines = trace.ToString().Split(new[] { Environment.NewLine }, StringSplitOptions.None);1998            foreach (var line in lines)1999            {2000                if ((line.Contains("at Microsoft.Coyote.Specifications") ||2001                    line.Contains("at Microsoft.Coyote.Runtime")) &&2002                    !line.Contains($"at {typeof(Specification).FullName}.{nameof(Specification.Monitor)}"))2003                {2004                    continue;2005                }2006                sb.AppendLine(line);2007            }2008            return sb.ToString();2009        }2010        /// <summary>2011        /// Raises the <see cref="OnFailure"/> event with the specified <see cref="Exception"/>.2012        /// </summary>2013        internal void RaiseOnFailureEvent(Exception exception)2014        {2015            if (this.Configuration.AttachDebugger)2016            {2017                Debugger.Break();2018                this.Configuration.AttachDebugger = false;2019            }2020            this.OnFailure?.Invoke(exception);2021        }2022        /// <summary>...

ControlledOperation.cs

Source:ControlledOperation.cs

...180        public override int GetHashCode() => this.Id.GetHashCode();181        /// <summary>182        /// Returns a string that represents the current operation id.183        /// </summary>184        public override string ToString() => this.Name;185        /// <summary>186        /// Indicates whether the specified <see cref="ControlledOperation"/> is equal187        /// to the current <see cref="ControlledOperation"/>.188        /// </summary>189        public bool Equals(ControlledOperation other) => this.Equals((object)other);190        /// <summary>191        /// Indicates whether the specified <see cref="ControlledOperation"/> is equal192        /// to the current <see cref="ControlledOperation"/>.193        /// </summary>194        bool IEquatable<ControlledOperation>.Equals(ControlledOperation other) => this.Equals(other);195        /// <summary>196        /// Releases any held resources.197        /// </summary>198        public void Dispose()...

TaskServices.cs

Source:TaskServices.cs

...45            {46                if (runtime.SchedulingPolicy is SchedulingPolicy.Interleaving)47                {48                    runtime.PauseOperationUntil(current, () => tasks.All(t => t.IsCompleted), !isAnyTaskUncontrolled,49                        string.Format("all tasks ('{0}') to complete", string.Join("', '", tasks.Select(t => t.Id.ToString()))));50                }51                else if (runtime.SchedulingPolicy is SchedulingPolicy.Fuzzing)52                {53                    runtime.DelayOperation(current);54                }55            }56        }57        /// <summary>58        /// Pauses the current operation until any of the specified tasks completes.59        /// </summary>60        internal static void WaitUntilAnyTaskCompletes(CoyoteRuntime runtime, SystemTask[] tasks)61        {62            bool isAnyTaskUncontrolled = IsAnyTaskUncontrolled(runtime, tasks);63            if (runtime.TryGetExecutingOperation(out ControlledOperation current))64            {65                if (runtime.SchedulingPolicy is SchedulingPolicy.Interleaving)66                {67                    runtime.PauseOperationUntil(current, () => tasks.Any(t => t.IsCompleted), !isAnyTaskUncontrolled,68                        string.Format("any task ('{0}') to complete", string.Join("', '", tasks.Select(t => t.Id.ToString()))));69                }70                else if (runtime.SchedulingPolicy is SchedulingPolicy.Fuzzing)71                {72                    runtime.DelayOperation(current);73                }74            }75        }76        /// <summary>77        /// Checks if any of the specified tasks is uncontrolled.78        /// </summary>79        private static bool IsAnyTaskUncontrolled(CoyoteRuntime runtime, SystemTask[] tasks)80        {81            bool isAnyTaskUncontrolled = false;82            foreach (var task in tasks)...

ToString

Using AI Code Generation

1using System;2using System.Text;3using System.Threading.Tasks;4using Microsoft.Coyote;5using Microsoft.Coyote.Actors;6using Microsoft.Coyote.Specifications;7using Microsoft.Coyote.Tasks;8using Microsoft.Coyote.TestingServices;9using Microsoft.Coyote.TestingServices.Runtime;10using Microsoft.Coyote.TestingServices.SchedulingStrategies;11using Microsoft.Coyote.TestingServices.Tracing.Schedule;12using Microsoft.Coyote.TestingServices.Tracing.Schedule.Custom;13using Microsoft.Coyote.TestingServices.Tracing.Schedule.Custom.CustomScheduleTrace;14using Microsoft.Coyote.TestingServices.Tracing.Schedule.Custom.CustomScheduleTrace.CustomSchedule;15using Microsoft.Coyote.TestingServices.Tracing.Schedule.Custom.CustomScheduleTrace.CustomSchedule.CustomOperation;16using Microsoft.Coyote.TestingServices.Tracing.Schedule.Custom.CustomScheduleTrace.CustomSchedule.CustomOperation.CustomControlledOperation;17using Microsoft.Coyote.TestingServices.Tracing.Schedule.Custom.CustomScheduleTrace.CustomSchedule.CustomOperation.CustomControlledOperation.CustomActorOperation;18using Microsoft.Coyote.TestingServices.Tracing.Schedule.Custom.CustomScheduleTrace.CustomSchedule.CustomOperation.CustomControlledOperation.CustomActorOperation.CustomActor;19using Microsoft.Coyote.TestingServices.Tracing.Schedule.Custom.CustomScheduleTrace.CustomSchedule.CustomOperation.CustomControlledOperation.CustomActorOperation.CustomActor.CustomState;20using Microsoft.Coyote.TestingServices.Tracing.Schedule.Custom.CustomScheduleTrace.CustomSchedule.CustomOperation.CustomControlledOperation.CustomActorOperation.CustomActor.CustomState.CustomEvent;21using Microsoft.Coyote.TestingServices.Tracing.Schedule.Custom.CustomScheduleTrace.CustomSchedule.CustomOperation.CustomControlledOperation.CustomActorOperation.CustomActor.CustomState.CustomEvent.CustomMachineEvent;22using Microsoft.Coyote.TestingServices.Tracing.Schedule.Custom.CustomScheduleTrace.CustomSchedule.CustomOperation.CustomControlledOperation.CustomActorOperation.CustomActor.CustomState.CustomEvent.CustomMachineEvent.CustomMachine;23using Microsoft.Coyote.TestingServices.Tracing.Schedule.Custom.CustomScheduleTrace.CustomSchedule.CustomOperation.CustomControlledOperation.CustomActorOperation.CustomActor.CustomState.CustomEvent.CustomMachineEvent.CustomMachine.CustomState;24using Microsoft.Coyote.TestingServices.Tracing.Schedule.Custom.CustomScheduleTrace.CustomSchedule.CustomOperation.CustomControlledOperation.CustomActorOperation.CustomActor.CustomState.CustomEvent.CustomMachineEvent.CustomMachine.CustomState.CustomEvent;25using Microsoft.Coyote.TestingServices.Tracing.Schedule.Custom.CustomScheduleTrace.CustomSchedule.CustomOperation.CustomControlledOperation.CustomActorOperation.CustomActor.CustomState.CustomEvent.CustomMachineEvent.CustomMachine.CustomState.CustomEvent.CustomMachineEvent;

ToString

Using AI Code Generation

1using System;2using Microsoft.Coyote;3using Microsoft.Coyote.Actors;4using Microsoft.Coyote.Specifications;5using Microsoft.Coyote.Tasks;6using Microsoft.Coyote.Testing;7using Microsoft.Coyote.Testing.Services;8using Microsoft.Coyote.Testing.Systematic;9using Microsoft.Coyote.Testing.Systematic.Strategies;10using Microsoft.Coyote.Testing.Systematic.TestReports;11using Microsoft.Coyote.Testing.Systematic.UnitTesting;12using Microsoft.Coyote.Testing.Systematic.Verification;13using Microsoft.Coyote.Tests.Common.Actors;14using Microsoft.Coyote.Tests.Common.Actors.Counter;15using Microsoft.Coyote.Tests.Common.Actors.EventCaching;16using Microsoft.Coyote.Tests.Common.Actors.EventCaching.Events;17using Microsoft.Coyote.Tests.Common.Actors.EventCaching.Services;18using Microsoft.Coyote.Tests.Common.Actors.EventCaching.Tasks;19using Microsoft.Coyote.Tests.Common.Actors.EventCaching.Tasks.Caching;20using Microsoft.Coyote.Tests.Common.Actors.EventCaching.Tasks.Caching.Events;21using Microsoft.Coyote.Tests.Common.Actors.EventCaching.Tasks.Caching.Services;22using Microsoft.Coyote.Tests.Common.Actors.EventCaching.Tasks.Caching.Tasks;23using Microsoft.Coyote.Tests.Common.Actors.EventCaching.Tasks.Caching.Tasks.Events;24using Microsoft.Coyote.Tests.Common.Actors.EventCaching.Tasks.Caching.Tasks.Services;25using Microsoft.Coyote.Tests.Common.Actors.EventCaching.Tasks.Caching.Tasks.Tasks;26using Microsoft.Coyote.Tests.Common.Actors.EventCaching.Tasks.Caching.Tasks.Tasks.Events;27using Microsoft.Coyote.Tests.Common.Actors.EventCaching.Tasks.Caching.Tasks.Tasks.Services;28using Microsoft.Coyote.Tests.Common.Actors.EventCaching.Tasks.Caching.Tasks.Tasks.Tasks;29using Microsoft.Coyote.Tests.Common.Actors.EventCaching.Tasks.Caching.Tasks.Tasks.Tasks.Events;30using Microsoft.Coyote.Tests.Common.Actors.EventCaching.Tasks.Caching.Tasks.Tasks.Tasks.Services;31using Microsoft.Coyote.Tests.Common.Actors.EventCaching.Tasks.Caching.Tasks.Tasks.Tasks.Tasks;32using Microsoft.Coyote.Tests.Common.Actors.EventCaching.Tasks.Caching.Tasks.Tasks.Tasks.Tasks.Events;33using Microsoft.Coyote.Tests.Common.Actors.EventCaching.Tasks.Caching.Tasks.Tasks.Tasks.Tasks.Services;34using Microsoft.Coyote.Tests.Common.Actors.EventCaching.Tasks.Caching.Tasks.Tasks.Tasks.Tasks.Tasks;

ToString

Using AI Code Generation

1using Microsoft.Coyote.Runtime;2using System;3{4    {5        static void Main(string[] args)6        {7            ControlledOperation op = new ControlledOperation();8            Console.WriteLine(op.ToString());9        }10    }11}

ToString

Using AI Code Generation

1using System;2using System.Collections.Generic;3using System.Linq;4using System.Text;5using System.Threading.Tasks;6{7    {8        static void Main(string[] args)9        {10            var a = new Microsoft.Coyote.Runtime.ControlledOperation();11            Console.WriteLine(a.ToString());12            Console.ReadLine();13        }14    }15}16using System;17using System.Collections.Generic;18using System.Linq;19using System.Text;20using System.Threading.Tasks;21{22    {23        static void Main(string[] args)24        {25            var a = new Microsoft.Coyote.Runtime.ControlledOperation();26            Console.WriteLine(a.ToString());27            Console.ReadLine();28        }29    }30}31using System;32using System.Collections.Generic;33using System.Linq;34using System.Text;35using System.Threading.Tasks;36{37    {38        static void Main(string[] args)39        {40            var a = new Microsoft.Coyote.Runtime.ControlledOperation();41            Console.WriteLine(a.ToString());42            Console.ReadLine();43        }44    }45}46using System;47using System.Collections.Generic;48using System.Linq;49using System.Text;50using System.Threading.Tasks;51{52    {53        static void Main(string[] args)54        {55            var a = new Microsoft.Coyote.Runtime.ControlledOperation();56            Console.WriteLine(a.ToString());57            Console.ReadLine();58        }59    }60}61using System;62using System.Collections.Generic;63using System.Linq;64using System.Text;65using System.Threading.Tasks;66{67    {68        static void Main(string[] args)69        {70            var a = new Microsoft.Coyote.Runtime.ControlledOperation();71            Console.WriteLine(a.ToString());72            Console.ReadLine();73        }74    }75}76using System;77using System.Collections.Generic;78using System.Linq;79using System.Text;

ToString

Using AI Code Generation

1using System;2using Microsoft.Coyote;3using Microsoft.Coyote.Runtime;4using Microsoft.Coyote.Specifications;5{6    {7        static void Main(string[] args)8        {9            ControlledOperation op = new ControlledOperation("Test");10            Console.WriteLine(op.ToString());11        }12    }13}14using System;15using Microsoft.Coyote;16using Microsoft.Coyote.Runtime;17using Microsoft.Coyote.Specifications;18{19    {20        static void Main(string[] args)21        {22            ControlledOperation op = new ControlledOperation("Test", new object[] { 5 });23            Console.WriteLine(op.ToString());24        }25    }26}27Test(5)28using System;29using Microsoft.Coyote;30using Microsoft.Coyote.Runtime;31using Microsoft.Coyote.Specifications;32{33    {34        static void Main(string[] args)35        {36            ControlledOperation op = new ControlledOperation("Test", new object[] { 5, "Hello" });37            Console.WriteLine(op.ToString());38        }39    }40}41Test(5, Hello)42using System;43using Microsoft.Coyote;44using Microsoft.Coyote.Runtime;45using Microsoft.Coyote.Specifications;46{47    {48        static void Main(string[] args)49        {50            ControlledOperation op = new ControlledOperation("Test", new object[] { 5, "Hello", new object[] { 1, 2, 3 } });51            Console.WriteLine(op.ToString());52        }53    }54}55Test(5, Hello, {1, 2, 3})

ToString

Using AI Code Generation

1using System;2using Microsoft.Coyote;3using Microsoft.Coyote.Actors;4using Microsoft.Coyote.Runtime;5{6    {7        public static void Main()8        {9            ControlledOperation op = new ControlledOperation();10            Console.WriteLine(op.ToString());11        }12    }13}14using System;15using Microsoft.Coyote;16using Microsoft.Coyote.Actors;17using Microsoft.Coyote.Runtime;18{19    {20        public static void Main()21        {22            ControlledOperation op = new ControlledOperation();23            Console.WriteLine(op.ToString());24        }25    }26}27using System;28using Microsoft.Coyote;29using Microsoft.Coyote.Actors;30using Microsoft.Coyote.Runtime;31{32    {33        public static void Main()34        {35            ControlledOperation op = new ControlledOperation();36            Console.WriteLine(op.ToString());37        }38    }39}40using System;41using Microsoft.Coyote;42using Microsoft.Coyote.Actors;43using Microsoft.Coyote.Runtime;44{45    {46        public static void Main()47        {48            ControlledOperation op = new ControlledOperation();49            Console.WriteLine(op.ToString());50        }51    }52}53using System;54using Microsoft.Coyote;55using Microsoft.Coyote.Actors;56using Microsoft.Coyote.Runtime;57{58    {59        public static void Main()60        {61            ControlledOperation op = new ControlledOperation();62            Console.WriteLine(op.ToString());63        }64    }65}66using System;67using Microsoft.Coyote;68using Microsoft.Coyote.Actors;69using Microsoft.Coyote.Runtime;70{71    {72        public static void Main()73        {74            ControlledOperation op = new ControlledOperation();75            Console.WriteLine(op.ToString());76        }77    }78}

ToString

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        public static void Main(string[] args)10        {11            ControlledOperation op = new ControlledOperation();12            Console.WriteLine(op.ToString());13        }14    }15}16using System;17using System.Threading.Tasks;18using Microsoft.Coyote;19using Microsoft.Coyote.Actors;20using Microsoft.Coyote.Runtime;21using Microsoft.Coyote.Tasks;22{23    {24        public static void Main(string[] args)25        {26            ControlledOperation op = new ControlledOperation();27            Console.WriteLine(op.ToString());28        }29    }30}31using System;32using System.Threading.Tasks;33using Microsoft.Coyote;34using Microsoft.Coyote.Actors;35using Microsoft.Coyote.Runtime;36using Microsoft.Coyote.Tasks;37{38    {39        public static void Main(string[] args)40        {41            ControlledOperation op = new ControlledOperation();42            Console.WriteLine(op.ToString());43        }44    }45}46using System;47using System.Threading.Tasks;48using Microsoft.Coyote;49using Microsoft.Coyote.Actors;50using Microsoft.Coyote.Runtime;51using Microsoft.Coyote.Tasks;52{53    {54        public static void Main(string[] args)55        {56            ControlledOperation op = new ControlledOperation();57            Console.WriteLine(op.ToString());58        }59    }60}61using System;62using System.Threading.Tasks;63using Microsoft.Coyote;64using Microsoft.Coyote.Actors;65using Microsoft.Coyote.Runtime;66using Microsoft.Coyote.Tasks;67{68    {69        public static void Main(string[] args)70        {71            ControlledOperation op = new ControlledOperation();72            Console.WriteLine(op.ToString());73        }

ToString

Using AI Code Generation

1using System;2using Microsoft.Coyote;3using Microsoft.Coyote.Specifications;4using Microsoft.Coyote.Tasks;5using Microsoft.Coyote.Actors;6using Microsoft.Coyote.Actors.Timers;7{8    {9        public static void Main(string[] args)10        {11            Console.WriteLine(ControlledOperation.Current.ToString());12        }13    }14}15using System;16using Microsoft.Coyote;17using Microsoft.Coyote.Specifications;18using Microsoft.Coyote.Tasks;19using Microsoft.Coyote.Actors;20using Microsoft.Coyote.Actors.Timers;21{22    {23        public static void Main(string[] args)24        {25            Console.WriteLine(ControlledActor.Current.ToString());26        }27    }28}29using System;30using Microsoft.Coyote;31using Microsoft.Coyote.Specifications;32using Microsoft.Coyote.Tasks;33using Microsoft.Coyote.Actors;34using Microsoft.Coyote.Actors.Timers;35{36    {37        public static void Main(string[] args)38        {39            Console.WriteLine(ControlledMachine.Current.ToString());40        }41    }42}43using System;44using Microsoft.Coyote;45using Microsoft.Coyote.Specifications;46using Microsoft.Coyote.Tasks;47using Microsoft.Coyote.Actors;48using Microsoft.Coyote.Actors.Timers;49{50    {51        public static void Main(string[] args)52        {53            Console.WriteLine(ControlledTimer.Current.ToString());54        }55    }56}57using System;58using Microsoft.Coyote;59using Microsoft.Coyote.Specifications;60using Microsoft.Coyote.Tasks;61using Microsoft.Coyote.Actors;62using Microsoft.Coyote.Actors.Timers;63{64    {65        public static void Main(string[] args)66        {67            Console.WriteLine(ControlledTask.Current.ToString());68        }69    }70}

ToString

Using AI Code Generation

1using System;2using Microsoft.Coyote.Runtime;3using Microsoft.Coyote.SystematicTesting;4using Microsoft.Coyote.Tasks;5using System.Threading.Tasks;6{7    {8        static void Main(string[] args)9        {10            var configuration = Configuration.Create();11            configuration.SchedulingIterations = 100;12            configuration.SchedulingStrategy = SchedulingStrategy.Random;13            configuration.TestingEngine = TestingEngine.SystematicTesting;14            configuration.Verbose = 2;15            configuration.EnableCycleDetection = true;16            configuration.EnableDataRaceDetection = true;17            configuration.EnableHotStateDetection = true;18            configuration.EnableOperationInterleavings = true;19            configuration.EnablePhaseParallelism = true;20            configuration.EnableRandomExecution = true;21            configuration.EnableStateGraphTesting = true;22            configuration.EnableTaskParallelism = true;23            configuration.EnableUnfairScheduling = true;

ToString

Using AI Code Generation

1using System;2using Microsoft.Coyote.Runtime;3using Microsoft.Coyote.SystematicTesting;4using Microsoft.Coyote.Tasks;5using System.Threading.Tasks;6{7    {8        public static void Main()9        {10            ControlledOperation op = new ControlledOperation("Test", 1);11            Console.WriteLine(op.ToString());12        }13    }14}15using System;16using Microsoft.Coyote.Runtime;17using Microsoft.Coyote.SystematicTesting;18using Microsoft.Coyote.Tasks;19using System.Threading.Tasks;20{21    {22        public static void Main()23        {24            ControlledOperation op = new ControlledOperation("Test", 1);25            Console.WriteLine("Name: {0}, Id: {1}", op.Name, op.Id);26        }27    }28}

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.