How do we the following in latest version of Coyote:

 // For replaying a bug and single stepping
Configuration configuration = Configuration.Create();
configuration.WithVerbosityEnabled(true);
// update the path to the schedule file.
configuration.ScheduleFile = "AfterNewUpdate.schedule";
ITestingEngine engine = TestingEngineFactory.CreateReplayEngine(configuration, (Action<IActorRuntime>)function.start);
engine.Run();
string bug = engine.TestReport.BugReports.FirstOrDefault();
if (bug != null)
{
   Console.WriteLine(bug);
}

coyote replay with -break command doesn't work on all platforms and the above thing is very useful. Can you please re-enable it?

E.g. if someone forgot to make the method static. Eventually we should support non-static methods too.

We should support rewriting and testing the following:

Task task = new Task(...);
task.Start();

Including nested tasks (e.g. Task).

I wonder if it was considered to add a rewrite step as a MSBuild target in the NuGet package. This way calling the tool coyote rewrite wouldn't be needed as that would be done automatically once the assembly is generated.

Could possibly be done if a specific property is provided like /p:CoyoteRewrite=true or be an opt-out when Configuration=Debug.

Using System.Tasks the CallOnStart() function (in below example) is called 3 times, where as using Coyote.Tasks it's being called 9 times.

Example:

    private class Observer
    {
        public string Name;
        public int Stage;

        public Observer(int stage, string str)
        {
            this.Stage = stage;
            this.Name = str;
        }
    }

    internal static int Count = 0;

    [Fact(Timeout = 5000)]
    public void TestWhenAll()
    {
        this.Test(async () =>
        {
        List<Observer> list = new List<Observer>();
        for (int i = 0; i < 3; i++)
        {
            list.Add(new Observer(1, "Task"));
        }

        foreach (IGrouping<int, Observer> group1 in list
            .GroupBy(oo => oo.Stage)
            .OrderBy(group => group.Key))
        {
                await Task.WhenAll(group1.Select(oo => CallOnStart()));
        }
            Specification.Assert(Count == 3, "Value is '{0}' instead of 3.", Count);

            await Task.Delay(1);
        },
        configuration: GetConfiguration().WithTestingIterations(100));
    }

    internal static Task CallOnStart()
    {
        Count = Count + 1;
        return Task.CompletedTask;
    }

There are two methods to "control" randomness: RandomBoolean and RandomInteger.
How to control Guid and Double values?

I was wondering why is the OnEntryAttribute sealed?

I see InitializeState() function looks for OnEntryAttribute (or its derived classes, as signified by "true" argument in the source) to locate the entry action, which to me indicates there was some initial thought on making it un-sealed.

This is very useful in scenarios where we want to write abstractions around the Coyote StateMachine class - for example, I am trying to write one where I allow maintaining state of the machine in a persistent store, and overriding OnEntryArribute not only makes my job easier (as I can define my custom OnEntry function which handles checkpointing of state) but also hides the nitty gitty implementation complexity of how my abstraction is implemented from the user.

Alternative ways to accomplish this are possible but the above approach seems most seamless to end users for me, so was wondering if it is possible to enable this.

From discussion with @lovettchris. We should set up something like this so that when a PR is committed to main it automatically deploys that to gh-pages branch:

https://github.com/mhausenblas/mkdocs-deploy-gh-pages

If i follow the steps using the Developer Command Prompt for VS2019 (tried both preview and not)
(In this article https://microsoft.github.io/coyote/learn/tools/coverage)

powershell -f build.ps1

then

coyote test ./bin/netcoreapp3.1/Monitors.exe -i 10 --coverage

i get the following output

i then spot the troubleshooting

Exception thrown: ‘System.BadImageFormatException’ in System.Private.CoreLib.dll
This could happen on a .NET Core build if you are referencing a *.exe instead of the *.dll assembly for testing.
This is on a Windows 2019 server (1809)

So i change it to use the dll instead.

next troubleshooting says.

Error: Could not find dependent assembly …
You may need to add --instrument or --instrument-list option to specify the location of that additional assembly.

I'm not sure what i am supposed to pass. This is literally running the steps after cloning the repo. Do i need other tools on my machine other than Visual Studio 2019 Professional?

We should provide a dotnet test adaptor to natively run Coyote tests from command line via dotnet test.

Assertion error: "Cannot wait for zero tasks to complete."
The below example throws assertion error when ran using coyote tasks. But, using System tasks it executes.

Using system task Task.WhenAll(tasks); with tasks.count == 0, the program executes successfully. The tasks.count not mandatory be greater than 0.

Example:

    [Fact(Timeout = 5000)]
    public void Test1()
    {
        this.Test(async () =>
        {
            Random r = new Random();
            var tasks = new List<Task>();
            if (r.Next(2) == 1)
            {
                tasks.Add(Task.Delay(100));
            }
            await Task.WhenAll(tasks);
        },
        configuration: GetConfiguration().WithTestingIterations(1));
    }

We should integrate Udit's work in this #165.

Is there a suggested way to persist actors?
I have long running state machines and the application might restart multiple times before they complete.
Are there guidelines for this scenario?

Right now concurrency fuzzing does not provide replay. This is general is tricky due to real timing involved. We can still though keep track of chosen delays and attempt to replay.

It could round-robin between random, fairpct, etc. Should probably be the default.

On both Firefox and Edge, the left side menu is misplaced, sometimes to the point of either not appearing on the screen at all or being mostly unusable. Depending on the screen resolution and the content of the side menu, the menu position moves up and down.

This issue makes part of the documentation undiscoverable/unreachable for visitors if like me there are unlucky enough to hit the wrong browser/resolution combination.

Please see the screenshots below.

As a side note: on the last screenshot, notice the UI dark pattern to nudge users to accept all cookies, in particular the lack of a "Decline all" button to complement the "Accept all" button. It gets even worse if you click the "Manage cookies" button. This kind of pattern is understandable (although ethically questionable) on website depending on third-party tracking to monetize, but it is rather puzzling to see that on a Microsoft funded software project documentation page. I'd be grateful if you provide this feedback to whomever can influence that decision.

The first example in the documentation here https://microsoft.github.io/coyote/learn/tools/unit-testing
passes. It doesn't seem to be picking up the Specification.Assert(False) as an fail?

<Project Sdk="Microsoft.NET.Sdk">
  <PropertyGroup>
    <TargetFramework>netcoreapp3.1</TargetFramework>
  </PropertyGroup>
  <ItemGroup>
    <PackageReference Include="Microsoft.Coyote" Version="1.0.12" />
    <PackageReference Include="Microsoft.Coyote.Test" Version="1.0.12" />
    <PackageReference Include="xunit" Version="2.4.1" />
    <PackageReference Include="xunit.runner.console" Version="2.4.1">
      <PrivateAssets>all</PrivateAssets>
      <IncludeAssets>runtime; build; native; contentfiles; analyzers; buildtransitive</IncludeAssets>
    </PackageReference>
    <PackageReference Include="xunit.runner.visualstudio" Version="2.4.2">
      <PrivateAssets>all</PrivateAssets>
      <IncludeAssets>runtime; build; native; contentfiles; analyzers; buildtransitive</IncludeAssets>
    </PackageReference>
  </ItemGroup>
</Project>

using Microsoft.Coyote.Specifications;
using Microsoft.Coyote.Tasks;
using Microsoft.Coyote.Runtime;
using Microsoft.Coyote;

using Microsoft.Coyote.SystematicTesting;
using Xunit;
using Xunit.Abstractions;

namespace TimboCoyote
{
    public class FirstTest
    {
        ITestOutputHelper Output;

        public Test(ITestOutputHelper output)
        {
            this.Output = output;
        }


        [Fact(Timeout = 5000)]
        public void RunCoyoteTest()
        {
            var config = Configuration.Create();
            TestingEngine engine = TestingEngine.Create(config, CoyoteTestMethod);
            engine.Run();
            var report = engine.TestReport;
            Output.WriteLine("Coyote found {0} bug.", report.NumOfFoundBugs);
        }

        private async Task CoyoteTestMethod()
        {
            // This is running as a Coyote test.
            await Task.Delay(10);
            Specification.Assert(false, "This test failed!");
        }
    }
}

did i use the incorrect using statements?

When running coyote on a sample I am getting the following error:

System.NullReferenceException
  HResult=0x80004003
  Message=Object reference not set to an instance of an object.
  Source=System.Private.CoreLib
  StackTrace:
   at System.Text.StringBuilder.Append(String value) in E:\A\_work\482\s\src\mscorlib\shared\System\Text\StringBuilder.cs:line 666
   at System.Text.StringBuilder.AppendLine(String value) in E:\A\_work\482\s\src\mscorlib\shared\System\Text\StringBuilder.cs:line 836
   at Microsoft.Coyote.IO.InMemoryLogger.WriteLine(String value)
   at Microsoft.Coyote.Runtime.LogWriter.LogAssertionFailure(String error)
   at Microsoft.Coyote.TestingServices.Scheduling.OperationScheduler.NotifyAssertionFailure(String text, Boolean killTasks, Boolean cancelExecution)
   at Microsoft.Coyote.TestingServices.Runtime.SystematicTestingRuntime.ProcessUnhandledExceptionInOperation(AsyncOperation op, Exception ex)
   at Microsoft.Coyote.TestingServices.Runtime.SystematicTestingRuntime.<>c__DisplayClass29_0.<<RunActorEventHandler>b__0>d.MoveNext()
   at System.Runtime.ExceptionServices.ExceptionDispatchInfo.Throw() in E:\A\_work\482\s\src\mscorlib\src\System\Runtime\ExceptionServices\ExceptionDispatchInfo.cs:line 132
   at System.Threading.ExecutionContext.RunInternal(ExecutionContext executionContext, ContextCallback callback, Object state) in E:\A\_work\482\s\src\mscorlib\shared\System\Threading\ExecutionContext.cs:line 167
   at System.Runtime.ExceptionServices.ExceptionDispatchInfo.Throw() in E:\A\_work\482\s\src\mscorlib\src\System\Runtime\ExceptionServices\ExceptionDispatchInfo.cs:line 132
   at System.Threading.ThreadPoolWorkQueue.Dispatch() in E:\A\_work\482\s\src\mscorlib\src\System\Threading\ThreadPool.cs:line 588

[Updated the error message] This seems like an internal exception which must be handled correctly?

ValueTasks are an important TPL type and although one can replace their usage with Task in their own code, many common 3rd party and system libraries use them. Most notably is the Microsoft.AspNetCore.Mvc.Testing library depends on HttpClient which uses ValueTask. Another example is Autofac's DisposeAsync.

This is a known limitation, just wanted to create an issue to put it on the roadmap.

I was wondering how do you generally recommend sending messages between state machines that are running across different machines?

In addition, in our scenario, the state machines are run as asynchronous operations in response to a user request, and they are released from the CPU contention as they enter a waiting state. Periodically, they may be rehydrated to see if any progress can be made.

In this case, is the recommendation to keep polling the other system/state-machine for task completion? or serialize all events to a state machine to some storage which it can monitor?

1. the animating state machine diagrams don't work
2. after visiting a long tutorial, like the robot tutorial, every page after that has huge long blank space to the page footer until you hit refresh on the top page (which resets the inner iframe I guess).
3. Sometimes a finger swipe to scroll becomes super sensitive and scrolls way too fast.
4. When you select a link from the footer like "Getting Started" from a long tutorial, it does not scroll back to the top of the page, so you see no change, it should scroll to the top so you can see the actual Getting Started content.

The following strange but simple program results into an "Common Language Runtime detected an invalid program" error after coyote rewrite. We should look into this and fix it (might be able to minimize more).

[Test]
public static async Task TestRaces()
{
  Thread.Sleep(10);
  await Task.Run(async () =>
  {
    await Task.CompletedTask;
  });
}

Looks like it's because you moved some folders but not change the links.

Hi Coyote team!

I'm playing around with the Coyote toolset with the HelloWorldTasks example. I want to try the coyote replay tool. I'm trying the following:

1- Run coyote test ./obj/Release/netcoreapp3.1/osx-x64/HelloWorldTasks.dll --iterations 100 to generate the faulty trace
2- Run coyote replay ./obj/Release/netcoreapp3.1/osx-x64/HelloWorldTasks.dll ./obj/Release/netcoreapp3.1/osx-x64/Output/HelloWorldTasks.dll/CoyoteOutput/HelloWorldTasks_0_1.schedule --break to replay the program with that trace
3- Expect that the coyote runtime will wait for a debugger to attach until it starts reproducing it. Not sure of this, that's my assumption of how it sould work

Any advice on how to use it? (I'm working with MacOS if it help in some way)

Coyote used to support explicit Microsoft.Coyote.Task task types before we introduced rewriting. We have deprecated them, and not advertise them in the documentation, but the types are still available in Microsoft.Coyote.dll because of backwards compatibility with an internal team that still uses them. Although we should switch them over to rewriting and completely remove these types, today someone can by mistake explicitly do using Microsoft.Coyote.Task, which then coupled with rewriting it can result into corrupted IL.

We can add a pass in rewriting that if it detects such explicit use of Microsoft.Coyote.Task it then complains to the user with an error, so that they can fix it.

ICoyoteRuntime.Stop() does not tell the actors about this event, it would be nice is we had a way to cause OnHaltAsync to be invoked on all actors, without having to explicitly send HaltEvent to each of them - outside code may not even know all the ActorId's to do this, whereas the Runtime does. Perhaps we need a new async method like this:

    Task HaltAsync();

And the ActorRuntime can implement this by calling OnHaltAsync on all actors that are not already halted.

That are marked with [Test] unless -m TEST_NAME is used. This is helpful when testing projects consisting of multiple Coyote tests via the command line tool.

call "C:\Program Files (x86)\Microsoft Visual Studio\2019\Enterprise\VC\Auxiliary\Build\vcvars64.bat"

Would be nice if we can fix that because I need to use x64 for all my c++ projects, so would be nice if coyote also was friendly to this environment...

Hi,

According to the page https://microsoft.github.io/coyote/learn/core/liveness-checking#effective-liveness-checking about liveness checking. It says "any terminated execution of the program must not have a monitor in a hot state". What will happen if the program terminates in a hot state?

In my code, I created a monitor with both hot and cold states. And I saw sometimes the program terminates without entering a cold state. The test.TestReport.NumOfFoundBugs is always 0 even the program ends in a hot state. I tried to set the LivenessTemperatureThreshold but it seems just for temperature larger than 0.

Does this cold state check need to be enabled explicitly?

Thanks

Rewrite this method then run coyote rewrite, then run the program you will see a runtime error:

(ell) d:\Temp\CoyoteTest>dotnet D:\Temp\CoyoteTest\CoyoteTest\bin\Debug\net5.0\CoyoteTest.dll
Hello World!
Unhandled exception. System.MissingMethodException: Method not found: 'System.Runtime.CompilerServices.TaskAwaiter`1<!0> UncontrolledTaskAwaiter`1.GetAwaiter()'.
   at CoyoteTest.Program.<>c.<<TestDetectedUncontrolledGenericAwaiter>b__1_0>d.MoveNext()
   at System.Runtime.CompilerServices.AsyncMethodBuilderCore.Start[TStateMachine](TStateMachine& stateMachine)
   at CoyoteTest.Program.<>c.<TestDetectedUncontrolledGenericAwaiter>b__1_0()
   at CoyoteTest.Program.Test(Func`1 test, Configuration configuration) in D:\Temp\CoyoteTest\CoyoteTest\Program.cs:line 33
   at CoyoteTest.Program.TestDetectedUncontrolledGenericAwaiter() in D:\Temp\CoyoteTest\CoyoteTest\Program.cs:line 23
   at CoyoteTest.Program.Main(String[] args) in D:\Temp\CoyoteTest\CoyoteTest\Program.cs:line 16

using Microsoft.Coyote.SystematicTesting;
using Microsoft.Coyote;
using System;
using System.Threading;
using System.Threading.Tasks;
using System.Runtime.CompilerServices;

namespace CoyoteTest
{
    class Program
    {
        static void Main(string[] args)
        {
            Console.WriteLine("Hello World!");
            Program p = new Program();
            p.TestDetectedUncontrolledGenericAwaiter();
            Console.WriteLine("Test complete!");
        }

        [Test]
        public void TestDetectedUncontrolledGenericAwaiter()
        {
            this.Test(async () =>
            {
                await new UncontrolledTaskAwaiter<int>();
            },
            configuration: this.GetConfiguration().WithTestingIterations(100));
        }


        protected void Test(Func<Task> test, Configuration configuration = null)
        {
            test();
        }

        protected Configuration GetConfiguration()
        {
            return Configuration.Create();
        }
        public class UncontrolledTaskAwaiter<T>
        {
            public TaskAwaiter<T> GetAwaiter() => Task.FromResult<T>(default).GetAwaiter();
        }
    }
}

Exception output:

System.NullReferenceException
Object reference not set to an instance of an object.
   at Microsoft.Coyote.Tasks.TaskAwaiter`1.get_IsCompleted()
   at CoyoteRepro.Tests.CoyoteUnitTest.Coyote_Should_Not_Throw_NRE() in /Users/mitch528/repos/CoyoteRepro/CoyoteRepro/CoyoteRepro.Tests/CoyoteUnitTest.cs:line 42
   at Xunit.Sdk.TestInvoker`1.<>c__DisplayClass48_1.<<InvokeTestMethodAsync>b__1>d.MoveNext() in C:\Dev\xunit\xunit\src\xunit.execution\Sdk\Frameworks\Runners\TestInvoker.cs:line 264
--- End of stack trace from previous location ---
   at Xunit.Sdk.ExecutionTimer.AggregateAsync(Func`1 asyncAction) in C:\Dev\xunit\xunit\src\xunit.execution\Sdk\Frameworks\ExecutionTimer.cs:line 48
   at Xunit.Sdk.ExceptionAggregator.RunAsync(Func`1 code) in C:\Dev\xunit\xunit\src\xunit.core\Sdk\ExceptionAggregator.cs:line 90

Repro: https://github.com/Mitch528/CoyoteRepro

Expected:

Both tests should succeed

Actual:

Test awaiting Task<TResponse> succeeds, but test awaiting AsyncUnaryCall<TResponse> fails (code).

I'm interested in wanting to use State machines in Orleans.
Because Orleans itself supports Actor, how do you put them together?

I'm a beginner who's interested in State machines and wants help.

Thank you so much

Is there a way to generate the graph from the unit tests?

Last thing people wanna do is switch over all their Tasks, only to find 1 year later that Microsoft Research is trying something new, different, and incompatible with prior products :D

If the answers are "yes" and "hella good support", it should be declared as such in the Readme.

I'm attempting to use Coyote to check for bugs in a library of mine, but some of my code is using System.Threading.SemaphoreSlim, which currently isn't supported.
It seems that there is a compatible implementation already available here:
https://github.com/microsoft/coyote/blob/main/Source/Core/Tasks/Locks/Semaphore.cs
My code seems to work normally when I manually rewrite it to use this implementation.

Could a rewrite rule be added to directly support code which uses SemaphoreSlim, or is there a detail I've missed?

I like to integrate Coyote with ASP.NET Core REST API we have. I was reading Synchronous execution of actors in docs and is it so that I have to create an actor that is created just for calling into actor system?
If I would use CreateActorAndExecuteAsync and send message in its OnEntry method should call Halt() at end of that method if I'm gonna use that actor for sending a single message from REST API?

It would be create I there was example/sample how to integrate something similar to ASP.NET Core API to Coyote actor system. Just having having example how to send single message into actor system and receive value synchronously that could be used without blocking from ASP.NET Core controller would be enough.

When I run the following command:
$ dotnet /Users/ankushpd/.nuget/packages/microsoft.coyote/1.0.0-rc9/lib/netcoreapp2.2/CoyoteCoverageReportMerger.dll Manager.sci

I get

Error: No input files provided

The file does exist at this path.

I am using a mac machine.

I am trying to using Coyote with .Net Core 3.1 which our project uses. However, after I rewrite the assembly the test assembly cannot use it any more.

Severity Code Description Project File Line Suppression State
Error CS1705 Assembly 'Foo.AzureClient' with identity 'Foo.AzureClient, Version=1.0.0.0, Culture=neutral, PublicKeyToken=null' uses 'System.Runtime, Version=5.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a' which has a higher version than referenced assembly 'System.Runtime' with identity 'System.Runtime, Version=4.2.2.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a' azureclient.tests

I did the rewrite using the following steps

1. dotnet tool install --global Microsoft.Coyote.CLI
2. .csproj Postbuild command "coyote rewrite $(TargetPath)"

This is using 1.2.7

Hello
I like your product, congrat!
I have a question: which tool did you use to build the animated state machine demo? https://microsoft.github.io/coyote/learn/programming-models/actors/state-machine-demo

We should integrate work from @Izikiel here and build on top of it.

Hello,
I watched the On .NET show coyote videos, great work on those. You should definitely add a link to those on documentation pages.

I had a look at the bounded buffer sample and played around with some code of my own using the Task model. I tried out the --graph option, but noticed nothing is output (only some skeleton styling). I noticed this mentioned on the gitter, that the graph option is more geared to the actor model. It would be really great if you could provide the additional logging code that was used in the video to generate the chart, would you be able to add that part to the sample code? @lovettchris

I notice the readme was removed from the bounded buffer example, why was it removed? I'm guessing it was supposed to be moved to the documentation site but that step was forgotten?

Right now, during SCT, each asynchronous task continuation (at an await point that is not complete) gets assigned its own priority for PCT. Instead, we should experiment with an optimization that figures out when these continuations can be "chained" together (without missing interleavings), and maintain the priority of a prior task continuation in the "chain" to optimize PCT exploration (similar to how its done today with actors and state machines).

We should support running ilverify (a .NET IL verification tool) as part of our rewriting test suite, to catch rewriting bugs early and increase our confidence in rewriting correctness.

Is the source code for the application/test used for the state machine demo available? I'm curious how the invariant that there should be at most one Leader at a time is communicated to the test.

Previous versions used to support --coverage activity on dotnet core.

Can we please re-enable it?

After running coyote rewrite on a .dll which is used by non-Microsoft.Coyote.SystematicTesting.Test unit tests (nunit tests which call into TestingEngine), the subsuquent running of dotnet test throws a Missing System.Runtime 5.0.0.0 etc. exception.

Looking into the rewritten dll with ildasm shows that Coyote added a reference to System.Runtime 5.0.0.0 in addition to System.Runtime 4.2.0.0, while the original dll only references System.Runtime 4.2.0.0.

I created a sample project to portray the issue.

I see that there is a change in behavior of the coyote commandline option -m in the latest release.
If we do not provide the -m option it prints:

Starting TestingProcessScheduler in process 8745
Error: Failed to get test method '' from assembly 'Manager, Version=1.0.0.0, Culture=neutral, PublicKeyToken=null'

In the older versions, it used to print out all the methods as potential options.
If this behavior has changed then shouldn't -m be made a compulsory parameter?

Currently Microsoft has at least:
Service Fabric Actors
Dapr
Coyote
Orleans
...

So, in order to understand what coyote is and what it is best for we need at least some understanding about:

• the reason, it's been created
• how it is different from others
• what are scenarios to use coyote and what are scenarios to consider other frameworks
• what's scenarios Azure team used it in and why they have chosen coyote instead of Service Fabric,
  please NOTE that in the past Microsoft advertised Service Fabric as a service that is used internally by Azure a lot

PS
See here https://twitter.com/RogerAlsing/status/1246504499784581124

Is it possible to use the Actors alone, without the rest of the framework?

Are the Actors extracted from another Microsoft project, and if so which one.

Currently, invoking Microsoft.Coyote.Runtime.SchedulingPoint.Interleave bypasses the --no-repro command, which can result into uncontrolled task errors. We should make sure that this method plays along well with fuzzing mode.