Replaying schedule file programmatically?

[ankushdesai]

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?

[pdeligia]

Hey @ankushdesai, we will put out a new version soon that will include an API that allows you to do this. It will look like this:

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

The following API:

ITestingEngine engine = TestingEngineFactory.CreateReplayEngine(configuration, (Action<IActorRuntime>)function.start);

is replaced by:

TestingEngine engine = TestingEngine.Create(configuration, (Action<IActorRuntime>)function.start);

That is already available. What is missing is:

configuration.WithReplayStrategy("AfterNewUpdate.schedule");

[ankushdesai]

Thanks @pdeligia, looking forward to it!

[pdeligia]

@ankushdesai v1.0.4 is out, so this should work now, but let me know if it doesn't!

[ankushdesai]

Thanks a lot @pdeligia, will try it out and get back to you.

[ankushdesai]

I am able to use this feature now, thanks for all the help!
@pdeligia

[ankushdesai]

@pdeligia There seems to be some problem with the usage of the new API.

configuration.WithReplayStrategy("xx.schedule");
TestingEngine engine = TestingEngine.Create(configuration, (Action<IActorRuntime>)function.start);

It throws the following exception when passed any string as input:

Unhandled exception. System.FormatException: Input string was not in a correct format.
   at System.Number.ThrowOverflowOrFormatException(ParsingStatus status, TypeCode type)
   at Microsoft.Coyote.SystematicTesting.ScheduleTrace..ctor(String[] traceDump)
   at Microsoft.Coyote.SystematicTesting.TestingEngine..ctor(Configuration configuration, TestMethodInfo testMethodInfo)
   at Microsoft.Coyote.SystematicTesting.TestingEngine..ctor(Configuration configuration, Delegate test)
   at Microsoft.Coyote.SystematicTesting.TestingEngine.Create(Configuration configuration, Action`1 test)

Can you please help?

[pdeligia]

@ankushdesai actually you need to pass the contents of the file to this API, rather than the file itself :) Sorry if this was confusing! We plan to write some documentation page on how to use the programmatic test API and will clarify there.

You could do something like:

File.WriteAllText("xx.schedule", reproducableTrace);
configuration.WithReplayStrategy(reproducableTrace);

But there is another way, that works if in the same test you already run the non-replay testing engine! You could do something like:

// Test to find a bug.
Configuration testConfiguration = Configuration.Create(); // assign more options
TestingEngine testingEngine = TestingEngine.Create(testConfiguration, (Action<IActorRuntime>)function.start);
engine.Run();
string bug = testingEngine.TestReport.BugReports.FirstOrDefault();
if (testingEngine.TestReport.NumOfFoundBugs > 0)
{
  Configuration replayConfiguration = Configuration.Create().WithReplayStrategy(testingEngine.ReproducableTrace);
  TestingEngine replayEngine = TestingEngine.Create(replayConfiguration, (Action<IActorRuntime>)function.start);
  replayEngine.Run();
}

Basically, in the next version, we will expose two currently internal APIs (only set during testing, not replay):

string TestingEngine.ReadableTrace;
string TestingEngine.ReproducableTrace;

The first gives you the contents of the human readable trace (which are normally dump inside the schedule .txt file), and the second gives you the contents of the .schedule file. So you can then do all these stuff programmatically (and even write them in your own custom locations/files). This is just optional btw, you can still read the file content of the schedule and pass it to the method as I described in the start of this post :)

Hope this helps!

[ankushdesai]

@pdeligia You rock! Thanks for the quick help. The above thing works.