microsoft
/
coyote
зеркало из
1
0
Форкнуть 0
Код Задачи Пакеты Проекты Релизы Вики Активность

graphing

This commit is contained in:
Pantazis Deligiannis 2022-12-14 03:29:36 +08:00
Родитель b6d3a83c74
Коммит 45c7450bf6
19 изменённых файлов: 619 добавлений и 425 удалений
Показать статистику Скачать Patch файл Скачать Diff файл Показать все файлы Свернуть все файлы

10
Source/Actors/Runtime/ActorExecutionContext.cs
Просмотреть файл

@ -992,11 +992,6 @@ namespace Microsoft.Coyote.Actors
{
this.Assert(type.IsSubclassOf(typeof(Actor)), "Type '{0}' is not an actor.", type.FullName);
// Using ulong.MaxValue because a Create operation cannot specify
// the id of its target, because the id does not exist yet.
this.Runtime.ScheduleNextOperation(creator?.Operation, SchedulingPointType.Create);
this.ResetProgramCounter(creator);
if (id is null)
{
id = this.CreateActorId(type, name);
@ -1049,6 +1044,9 @@ namespace Microsoft.Coyote.Actors
this.LogManager.LogCreateActor(id, creator?.Id.Name, creator?.Id.Type);
}
this.Runtime.ScheduleNextOperation(creator?.Operation, SchedulingPointType.Create, op);
this.ResetProgramCounter(creator);
return actor;
}
@ -1138,7 +1136,7 @@ namespace Microsoft.Coyote.Actors
"Cannot send event '{0}' to actor id '{1}' that is not bound to an actor instance.",
e.GetType().FullName, targetId.Value);
this.Runtime.ScheduleNextOperation(sender?.Operation, SchedulingPointType.Send);
this.Runtime.ScheduleNextOperation(sender?.Operation, SchedulingPointType.Send, target.Operation);
this.ResetProgramCounter(sender as StateMachine);
// If no group is provided we default to passing along the group from the sender.

2
Source/Actors/Runtime/ActorOperation.cs
Просмотреть файл

@ -19,7 +19,7 @@ namespace Microsoft.Coyote.Actors
/// Initializes a new instance of the <see cref="ActorOperation"/> class.
/// </summary>
internal ActorOperation(ulong operationId, string name, Actor actor, CoyoteRuntime runtime)
: base(operationId, name, null, runtime)
: base(operationId, name, actor.GetType().FullName, null, runtime)
{
this.Actor = actor;
}

15
Source/Core/Configuration.cs
Просмотреть файл

@ -292,12 +292,18 @@ namespace Microsoft.Coyote
internal bool IsCoverageInfoSerialized;
/// <summary>
/// If true, requests a DGML graph of the iteration that contains a bug, if a bug is found.
/// If true, requests a visual graph of the iteration that contains a bug, if a bug is found.
/// This is different from a coverage activity graph, as it will also show actor instances.
/// </summary>
[DataMember]
internal bool IsTraceVisualizationEnabled;
/// <summary>
/// If true, visual traces are produced in the DGML format, else in the DOT format.
/// </summary>
[DataMember]
internal bool IsDgmlFormatEnabled;
/// <summary>
/// Produce an XML formatted runtime log file.
/// </summary>
@ -361,6 +367,7 @@ namespace Microsoft.Coyote
this.IsScheduleCoverageReported = false;
this.IsCoverageInfoSerialized = false;
this.IsTraceVisualizationEnabled = false;
this.IsDgmlFormatEnabled = false;
this.IsXmlLogEnabled = false;
string optout = Environment.GetEnvironmentVariable("COYOTE_CLI_TELEMETRY_OPTOUT");
@ -833,13 +840,15 @@ namespace Microsoft.Coyote
/// <summary>
/// Updates the configuration with trace visualization enabled or disabled.
/// If enabled, the testing engine can produce a DGML graph representing
/// If enabled, the testing engine can produce a visual graph representing
/// an execution leading up to a bug.
/// </summary>
/// <param name="isEnabled">If true, then enables trace visualization.</param>
public Configuration WithTraceVisualizationEnabled(bool isEnabled = true)
/// <param name="useDgmlFormat">If true, then uses DGML format, else DOT.</param>
public Configuration WithTraceVisualizationEnabled(bool isEnabled = true, bool useDgmlFormat = false)
{
this.IsTraceVisualizationEnabled = isEnabled;
this.IsDgmlFormatEnabled = useDgmlFormat;
return this;
}

46
Source/Core/Coverage/CoverageGraph.cs
Просмотреть файл

@ -4,6 +4,7 @@
using System;
using System.Collections.Generic;
using System.IO;
using System.Linq;
using System.Runtime.Serialization;
using System.Text;
using System.Xml.Linq;
@ -156,11 +157,54 @@ namespace Microsoft.Coyote.Coverage
return index;
}
internal void SaveDgml(string graphFilePath, bool includeDefaultStyles)
internal void Save(string graphFilePath, bool includeDefaultStyles, bool useDgmlFormat = false)
{
using StreamWriter writer = new StreamWriter(graphFilePath, false, Encoding.UTF8);
if (useDgmlFormat)
{
this.WriteDgml(writer, includeDefaultStyles);
}
else
{
this.WriteDot(writer, includeDefaultStyles);
}
}
/// <summary>
/// Serializes the <see cref="CoverageGraph"/> to DOT format.
/// </summary>
public void WriteDot(TextWriter writer, bool includeDefaultStyles)
{
writer.WriteLine("digraph CoyoteGraph {");
if (includeDefaultStyles)
{
writer.WriteLine(
@" start[shape=Mdiamond];
end[shape=Msquare];");
}
if (this.InternalNodes != null && this.InternalLinks != null)
{
List<string> nodes = new List<string>(this.InternalNodes.Keys);
nodes.Sort(StringComparer.Ordinal);
foreach (var nodeId in nodes)
{
Node node = this.InternalNodes[nodeId];
List<string> links = new List<string>(this.InternalLinks.Where(
link => link.Value.Source?.Id == node.Id).Select(link => link.Key));
links.Sort(StringComparer.Ordinal);
foreach (var linkId in links)
{
Link link = this.InternalLinks[linkId];
writer.WriteLine(" \"{0}\" -> \"{1}\";", link.Source.Id, link.Target.Id);
}
}
}
writer.WriteLine("}");
}
/// <summary>
/// Serializes the <see cref="CoverageGraph"/> to DGML format.

4
Source/Core/Coverage/CoverageReporter.cs
Просмотреть файл

@ -37,12 +37,12 @@ namespace Microsoft.Coyote.Coverage
/// <summary>
/// Emits the visualization graph, if it is available.
/// </summary>
public bool TryEmitVisualizationGraph(string graphFile)
public bool TryEmitVisualizationGraph(string graphFile, bool useDgmlFormat = false)
{
bool isAvailable = this.CoverageInfo.CoverageGraph?.IsAvailable() ?? false;
if (isAvailable)
{
this.CoverageInfo.CoverageGraph.SaveDgml(graphFile, true);
this.CoverageInfo.CoverageGraph.Save(graphFile, true, useDgmlFormat);
}
return isAvailable;

65
Source/Core/Runtime/CoyoteRuntime.cs
Просмотреть файл

@ -20,7 +20,7 @@ using SpecMonitor = Microsoft.Coyote.Specifications.Monitor;
namespace Microsoft.Coyote.Runtime
{
/// <summary>
/// Runtime for controlling, scheduling and executing asynchronous operations.
/// Runtime for controlling, scheduling and executing operations.
/// </summary>
/// <remarks>
/// Invoking scheduling methods is thread-safe.
@ -115,9 +115,9 @@ namespace Microsoft.Coyote.Runtime
private readonly ConcurrentDictionary<ulong, Thread> ThreadPool;
/// <summary>
/// Map from unique operation ids to asynchronous operations.
/// Map from unique operation ids to controlled operations.
/// </summary>
private readonly Dictionary<ulong, ControlledOperation> OperationMap;
internal readonly Dictionary<ulong, ControlledOperation> OperationMap;
/// <summary>
/// Map from newly created operations that have not started executing yet
@ -218,7 +218,7 @@ namespace Microsoft.Coyote.Runtime
private readonly object RuntimeLock;
/// <summary>
/// Produces tokens for canceling asynchronous operations when the runtime detaches.
/// Produces tokens for canceling controlled operations when the runtime detaches.
/// </summary>
private readonly CancellationTokenSource CancellationSource;
@ -364,7 +364,7 @@ namespace Microsoft.Coyote.Runtime
Thread.CurrentThread.ManagedThreadId, this.Scheduler.GetStrategyName());
this.Assert(testMethod != null, "Unable to execute a null test method.");
ControlledOperation op = this.CreateControlledOperation();
ControlledOperation op = this.CreateControlledOperation(description: string.IsNullOrEmpty(testName) ? "test" : testName);
this.ScheduleOperation(op, () =>
{
Task task = Task.CompletedTask;
@ -430,14 +430,15 @@ namespace Microsoft.Coyote.Runtime
}
else
{
op = this.CreateControlledOperation();
string callerInfo = GetCallerInfoFromStackTrace(new StackTrace());
op = this.CreateControlledOperation(description: callerInfo);
}
// Register this task as a known controlled task.
this.ControlledTasks.TryAdd(task, op);
this.ScheduleOperation(op, () => this.ControlledTaskScheduler.ExecuteTask(task));
this.ScheduleNextOperation(default, SchedulingPointType.Create);
this.ScheduleNextOperation(default, SchedulingPointType.Create, op);
}
/// <summary>
@ -447,7 +448,7 @@ namespace Microsoft.Coyote.Runtime
{
ControlledOperation op = this.CreateControlledOperation(group: ExecutingOperation?.Group);
this.ScheduleOperation(op, continuation, preCondition, postCondition);
this.ScheduleNextOperation(default, SchedulingPointType.ContinueWith);
this.ScheduleNextOperation(default, SchedulingPointType.ContinueWith, op);
}
/// <summary>
@ -543,7 +544,7 @@ namespace Microsoft.Coyote.Runtime
{
var delayedOp = state as ControlledOperation;
delayedOp.Status = OperationStatus.PausedOnDelay;
this.ScheduleNextOperation(delayedOp, SchedulingPointType.Yield);
this.ScheduleNextOperation(delayedOp, SchedulingPointType.Delay);
},
op,
cancellationToken,
@ -616,15 +617,16 @@ namespace Microsoft.Coyote.Runtime
/// <summary>
/// Creates a new controlled operation with the specified group and an optional delay.
/// </summary>
internal ControlledOperation CreateControlledOperation(OperationGroup group = null, uint delay = 0)
internal ControlledOperation CreateControlledOperation(string description = null, OperationGroup group = null, uint delay = 0)
{
using (SynchronizedSection.Enter(this.RuntimeLock))
{
// Create a new controlled operation using the next available operation id.
Console.WriteLine($"Creating controlled operation: {new System.Diagnostics.StackTrace()}");
ulong operationId = this.GetNextOperationId();
ControlledOperation op = delay > 0 ?
new DelayOperation(operationId, $"Delay({operationId})", delay, group, this) :
new ControlledOperation(operationId, $"Op({operationId})", group, this);
new ControlledOperation(operationId, $"Op({operationId})", description, group, this);
if (operationId > 0 && !this.IsThreadControlled(Thread.CurrentThread))
{
op.IsSourceUncontrolled = true;
@ -842,6 +844,7 @@ namespace Microsoft.Coyote.Runtime
/// </summary>
/// <param name="current">The currently executing operation, if there is one.</param>
/// <param name="type">The type of the scheduling point.</param>
/// <param name="target">The target operation, if there is one.</param>
/// <param name="isSuppressible">True if the interleaving can be suppressed, else false.</param>
/// <param name="isYielding">True if the current operation is yielding, else false.</param>
/// <returns>True if an operation other than the current was scheduled, else false.</returns>
@ -849,7 +852,7 @@ namespace Microsoft.Coyote.Runtime
/// An enabled operation is one that is not paused nor completed.
/// </remarks>
internal bool ScheduleNextOperation(ControlledOperation current, SchedulingPointType type,
bool isSuppressible = true, bool isYielding = false)
ControlledOperation target = null, bool isSuppressible = true, bool isYielding = false)
{
using (SynchronizedSection.Enter(this.RuntimeLock))
{
@ -965,7 +968,7 @@ namespace Microsoft.Coyote.Runtime
this.CoverageInfo.DeclareSchedulingPoint(type.ToString(), new StackTrace().ToString());
}
if (!this.Scheduler.GetNextOperation(ops, current, isYielding, out ControlledOperation next))
if (!this.Scheduler.GetNextOperation(ops, current, target ?? current, isYielding, out ControlledOperation next))
{
// The scheduler hit the scheduling steps bound.
this.Detach(ExecutionStatus.BoundReached);
@ -2453,6 +2456,42 @@ namespace Microsoft.Coyote.Runtime
return sb.ToString();
}
/// <summary>
/// Returns the caller info from the specified stack trace.
/// </summary>
private static string GetCallerInfoFromStackTrace(StackTrace trace)
{
#if NET || NETCOREAPP3_1
string[] lines = trace.ToString().Split(Environment.NewLine, StringSplitOptions.None);
#else
string[] lines = trace.ToString().Split(new[] { Environment.NewLine }, StringSplitOptions.None);
#endif
string info = string.Empty;
for (int i = 0; i < lines.Length; i++)
{
if (!lines[i].StartsWith(" at System", StringComparison.Ordinal) &&
!lines[i].StartsWith(" at Microsoft.Coyote", StringComparison.Ordinal))
{
// Get the method name with the parameters from the trace line.
int index = lines[i].IndexOf("at ", StringComparison.Ordinal);
if (index >= 0)
{
index += 3;
int endIndex = lines[i].IndexOf("(", index, StringComparison.Ordinal);
if (endIndex >= 0)
{
info = lines[i].Substring(index, endIndex - index);
}
}
break;
}
}
return info;
}
/// <summary>
/// Raises the <see cref="OnFailure"/> event with the specified <see cref="Exception"/>.
/// </summary>

244
Source/Core/Runtime/ExecutionTrace.cs
Просмотреть файл

@ -49,29 +49,29 @@ namespace Microsoft.Coyote.Runtime
internal static ExecutionTrace Create() => new ExecutionTrace();
/// <summary>
/// Adds a scheduling choice.
/// Adds a scheduling decision.
/// </summary>
internal void AddSchedulingChoice(ulong scheduledOperationId, SchedulingPointType sp)
internal void AddSchedulingDecision(ulong current, SchedulingPointType sp, ulong target, ulong next)
{
var scheduleStep = Step.CreateSchedulingChoice(this.Length, scheduledOperationId, sp);
var scheduleStep = new SchedulingStep(this.Length, current, sp, target, next);
this.Push(scheduleStep);
}
/// <summary>
/// Adds a nondeterministic boolean choice.
/// Adds a nondeterministic boolean decision.
/// </summary>
internal void AddNondeterministicBooleanChoice(bool choice, SchedulingPointType sp)
internal void AddNondeterministicBooleanDecision(ulong current, bool value)
{
var scheduleStep = Step.CreateNondeterministicBooleanChoice(this.Length, choice, sp);
var scheduleStep = new BooleanChoiceStep(this.Length, current, value);
this.Push(scheduleStep);
}
/// <summary>
/// Adds a nondeterministic integer choice.
/// Adds a nondeterministic integer decision.
/// </summary>
internal void AddNondeterministicIntegerChoice(int choice, SchedulingPointType sp)
internal void AddNondeterministicIntegerDecision(ulong current, int value)
{
var scheduleStep = Step.CreateNondeterministicIntegerChoice(this.Length, choice, sp);
var scheduleStep = new IntegerChoiceStep(this.Length, current, value);
this.Push(scheduleStep);
}
@ -143,17 +143,18 @@ namespace Microsoft.Coyote.Runtime
{
foreach (var step in trace.Steps)
{
if (step.Kind is DecisionKind.SchedulingChoice)
if (step is SchedulingStep schedulingStep)
{
this.AddSchedulingChoice(step.ScheduledOperationId, step.SchedulingPoint);
this.AddSchedulingDecision(schedulingStep.Current, schedulingStep.SchedulingPoint,
schedulingStep.Target, schedulingStep.Value);
}
else if (step.Kind is DecisionKind.NondeterministicChoice && step.BooleanChoice.HasValue)
else if (step is BooleanChoiceStep boolChoiceStep)
{
this.AddNondeterministicBooleanChoice(step.BooleanChoice.Value, step.SchedulingPoint);
this.AddNondeterministicBooleanDecision(boolChoiceStep.Current, boolChoiceStep.Value);
}
else if (step.Kind is DecisionKind.NondeterministicChoice && step.IntegerChoice.HasValue)
else if (step is IntegerChoiceStep intChoiceStep)
{
this.AddNondeterministicIntegerChoice(step.IntegerChoice.Value, step.SchedulingPoint);
this.AddNondeterministicIntegerDecision(intChoiceStep.Current, intChoiceStep.Value);
}
}
@ -185,17 +186,18 @@ namespace Microsoft.Coyote.Runtime
while (appendIndex < trace.Length)
{
Step step = trace[appendIndex];
if (step.Kind is DecisionKind.SchedulingChoice)
if (step is SchedulingStep schedulingStep)
{
this.AddSchedulingChoice(step.ScheduledOperationId, step.SchedulingPoint);
this.AddSchedulingDecision(schedulingStep.Current, schedulingStep.SchedulingPoint,
schedulingStep.Target, schedulingStep.Value);
}
else if (step.Kind is DecisionKind.NondeterministicChoice && step.BooleanChoice.HasValue)
else if (step is BooleanChoiceStep boolChoiceStep)
{
this.AddNondeterministicBooleanChoice(step.BooleanChoice.Value, step.SchedulingPoint);
this.AddNondeterministicBooleanDecision(boolChoiceStep.Current, boolChoiceStep.Value);
}
else if (step.Kind is DecisionKind.NondeterministicChoice && step.IntegerChoice.HasValue)
else if (step is IntegerChoiceStep intChoiceStep)
{
this.AddNondeterministicIntegerChoice(step.IntegerChoice.Value, step.SchedulingPoint);
this.AddNondeterministicIntegerDecision(intChoiceStep.Current, intChoiceStep.Value);
}
appendIndex++;
@ -209,19 +211,10 @@ namespace Microsoft.Coyote.Runtime
/// </summary>
internal void Clear() => this.Steps.Clear();
/// <summary>
/// The kind of decision taken during an execution step.
/// </summary>
internal enum DecisionKind
{
SchedulingChoice = 0,
NondeterministicChoice
}
/// <summary>
/// Contains metadata related to a single execution step.
/// </summary>
internal sealed class Step : IEquatable<Step>, IComparable<Step>
internal abstract class Step : IEquatable<Step>, IComparable<Step>
{
/// <summary>
/// The unique index of this execution step.
@ -229,32 +222,9 @@ namespace Microsoft.Coyote.Runtime
internal int Index;
/// <summary>
/// The kind of controlled decision taken in this execution step.
/// The id of the currently executing operation.
/// </summary>
internal DecisionKind Kind { get; private set; }
/// <summary>
/// The type of scheduling point encountered in this execution step.
/// </summary>
internal SchedulingPointType SchedulingPoint { get; private set; }
/// <summary>
/// The id of the scheduled operation. Only relevant if this is
/// a regular execution step.
/// </summary>
internal ulong ScheduledOperationId;
/// <summary>
/// The non-deterministic boolean choice value. Only relevant if
/// this is a choice execution step.
/// </summary>
internal bool? BooleanChoice;
/// <summary>
/// The non-deterministic integer choice value. Only relevant if
/// this is a choice execution step.
/// </summary>
internal int? IntegerChoice;
internal ulong Current;
/// <summary>
/// The previous execution step.
@ -267,52 +237,14 @@ namespace Microsoft.Coyote.Runtime
internal Step Next;
/// <summary>
/// Creates an execution step.
/// Initializes a new instance of the <see cref="Step"/> class.
/// </summary>
internal static Step CreateSchedulingChoice(int index, ulong scheduledOperationId, SchedulingPointType sp)
protected Step(int index, ulong current)
{
var scheduleStep = new Step();
scheduleStep.Index = index;
scheduleStep.Kind = DecisionKind.SchedulingChoice;
scheduleStep.SchedulingPoint = sp;
scheduleStep.ScheduledOperationId = scheduledOperationId;
scheduleStep.BooleanChoice = null;
scheduleStep.IntegerChoice = null;
scheduleStep.Previous = null;
scheduleStep.Next = null;
return scheduleStep;
}
/// <summary>
/// Creates a nondeterministic boolean choice execution step.
/// </summary>
internal static Step CreateNondeterministicBooleanChoice(int index, bool choice, SchedulingPointType sp)
{
var scheduleStep = new Step();
scheduleStep.Index = index;
scheduleStep.Kind = DecisionKind.NondeterministicChoice;
scheduleStep.SchedulingPoint = sp;
scheduleStep.BooleanChoice = choice;
scheduleStep.IntegerChoice = null;
scheduleStep.Previous = null;
scheduleStep.Next = null;
return scheduleStep;
}
/// <summary>
/// Creates a nondeterministic integer choice execution step.
/// </summary>
internal static Step CreateNondeterministicIntegerChoice(int index, int choice, SchedulingPointType sp)
{
var scheduleStep = new Step();
scheduleStep.Index = index;
scheduleStep.Kind = DecisionKind.NondeterministicChoice;
scheduleStep.SchedulingPoint = sp;
scheduleStep.BooleanChoice = null;
scheduleStep.IntegerChoice = choice;
scheduleStep.Previous = null;
scheduleStep.Next = null;
return scheduleStep;
this.Index = index;
this.Current = current;
this.Previous = null;
this.Next = null;
}
/// <summary>
@ -324,13 +256,7 @@ namespace Microsoft.Coyote.Runtime
/// Indicates whether the specified <see cref="Step"/> is equal
/// to the current <see cref="Step"/>.
/// </summary>
internal bool Equals(Step other) => other != null ?
this.Index == other.Index && this.Kind == other.Kind &&
this.SchedulingPoint == other.SchedulingPoint &&
this.ScheduledOperationId == other.ScheduledOperationId &&
this.BooleanChoice == other.BooleanChoice &&
this.IntegerChoice == other.IntegerChoice :
false;
internal abstract bool Equals(Step other);
/// <summary>
/// Determines whether the specified object is equal to the current object.
@ -349,5 +275,109 @@ namespace Microsoft.Coyote.Runtime
/// </summary>
int IComparable<Step>.CompareTo(Step other) => this.Index - other.Index;
}
/// <summary>
/// Contains metadata related to a single scheduling step.
/// </summary>
internal sealed class SchedulingStep : Step
{
/// <summary>
/// The type of scheduling point encountered in this execution step.
/// </summary>
internal SchedulingPointType SchedulingPoint { get; private set; }
/// <summary>
/// The id of the target operation.
/// </summary>
internal ulong Target;
/// <summary>
/// The non-deterministic scheduling choice value.
/// </summary>
internal ulong Value;
/// <summary>
/// Initializes a new instance of the <see cref="SchedulingStep"/> class.
/// </summary>
internal SchedulingStep(int index, ulong current, SchedulingPointType sp, ulong target, ulong next)
: base(index, current)
{
this.SchedulingPoint = sp;
this.Target = target;
this.Value = next;
}
/// <summary>
/// Indicates whether the specified <see cref="Step"/> is equal
/// to the current <see cref="Step"/>.
/// </summary>
internal override bool Equals(Step other) => other is SchedulingStep step ?
this.Index == step.Index &&
this.Current == step.Current &&
this.SchedulingPoint == step.SchedulingPoint &&
this.Target == step.Target &&
this.Value == step.Value :
false;
}
/// <summary>
/// Contains metadata related to a single boolean choice step.
/// </summary>
internal sealed class BooleanChoiceStep : Step
{
/// <summary>
/// The non-deterministic boolean choice value.
/// </summary>
internal bool Value;
/// <summary>
/// Initializes a new instance of the <see cref="BooleanChoiceStep"/> class.
/// </summary>
internal BooleanChoiceStep(int index, ulong current, bool value)
: base(index, current)
{
this.Value = value;
}
/// <summary>
/// Indicates whether the specified <see cref="Step"/> is equal
/// to the current <see cref="Step"/>.
/// </summary>
internal override bool Equals(Step other) => other is BooleanChoiceStep step ?
this.Index == step.Index &&
this.Current == step.Current &&
this.Value == step.Value :
false;
}
/// <summary>
/// Contains metadata related to a single integer choice step.
/// </summary>
internal sealed class IntegerChoiceStep : Step
{
/// <summary>
/// The non-deterministic integer choice value.
/// </summary>
internal int Value;
/// <summary>
/// Initializes a new instance of the <see cref="IntegerChoiceStep"/> class.
/// </summary>
internal IntegerChoiceStep(int index, ulong current, int value)
: base(index, current)
{
this.Value = value;
}
/// <summary>
/// Indicates whether the specified <see cref="Step"/> is equal
/// to the current <see cref="Step"/>.
/// </summary>
internal override bool Equals(Step other) => other is IntegerChoiceStep step ?
this.Index == step.Index &&
this.Current == step.Current &&
this.Value == step.Value :
false;
}
}
}

8
Source/Core/Runtime/Operations/ControlledOperation.cs
Просмотреть файл

@ -27,6 +27,11 @@ namespace Microsoft.Coyote.Runtime
/// </summary>
internal string Name { get; }
/// <summary>
/// The description of this operation.
/// </summary>
internal string Description { get; }
/// <summary>
/// The status of this operation. An operation can be scheduled only
/// if it is <see cref="OperationStatus.Enabled"/>.
@ -97,11 +102,12 @@ namespace Microsoft.Coyote.Runtime
/// <summary>
/// Initializes a new instance of the <see cref="ControlledOperation"/> class.
/// </summary>
internal ControlledOperation(ulong operationId, string name, OperationGroup group, CoyoteRuntime runtime)
internal ControlledOperation(ulong operationId, string name, string description, OperationGroup group, CoyoteRuntime runtime)
{
this.Runtime = runtime;
this.Id = operationId;
this.Name = name;
this.Description = description ?? string.Empty;
this.Status = OperationStatus.None;
this.Group = group ?? OperationGroup.Create(this);
this.Continuations = new Queue<Action>();

2
Source/Core/Runtime/Operations/DelayOperation.cs
Просмотреть файл

@ -17,7 +17,7 @@ namespace Microsoft.Coyote.Runtime
/// Initializes a new instance of the <see cref="DelayOperation"/> class.
/// </summary>
internal DelayOperation(ulong operationId, string name, uint delay, OperationGroup group, CoyoteRuntime runtime)
: base(operationId, name, group, runtime)
: base(operationId, name, "delay", group, runtime)
{
this.Delay = delay > int.MaxValue ? int.MaxValue : (int)delay;
}

2
Source/Core/Runtime/Operations/UserDefinedOperation.cs
Просмотреть файл

@ -27,7 +27,7 @@ namespace Microsoft.Coyote.Runtime
/// Initializes a new instance of the <see cref="UserDefinedOperation"/> class.
/// </summary>
internal UserDefinedOperation(CoyoteRuntime runtime, IOperationBuilder builder, ulong operationId)
: base(operationId, builder.Name, null, runtime)
: base(operationId, builder.Name, string.Empty, null, runtime)
{
this.HashedStateCallback = builder.HashedStateCallback;
}

9
Source/Core/Runtime/Scheduling/OperationScheduler.cs
Просмотреть файл

@ -221,11 +221,12 @@ namespace Microsoft.Coyote.Runtime
/// </summary>
/// <param name="ops">The set of available operations.</param>
/// <param name="current">The currently scheduled operation.</param>
/// <param name="target">The target operation.</param>
/// <param name="isYielding">True if the current operation is yielding, else false.</param>
/// <param name="next">The next operation to schedule.</param>
/// <returns>True if there is a next choice, else false.</returns>
internal bool GetNextOperation(IEnumerable<ControlledOperation> ops, ControlledOperation current,
bool isYielding, out ControlledOperation next)
ControlledOperation target, bool isYielding, out ControlledOperation next)
{
// Filter out any operations that cannot be scheduled.
var enabledOps = ops.Where(op => op.Status is OperationStatus.Enabled);
@ -245,7 +246,7 @@ namespace Microsoft.Coyote.Runtime
if (this.Strategy is InterleavingStrategy strategy &&
strategy.GetNextOperation(enabledOps, current, isYielding, out next))
{
this.Trace.AddSchedulingChoice(next.Id, current.LastSchedulingPoint);
this.Trace.AddSchedulingDecision(current.Id, current.LastSchedulingPoint, target.Id, next.Id);
return true;
}
}
@ -265,7 +266,7 @@ namespace Microsoft.Coyote.Runtime
if (this.Strategy is InterleavingStrategy strategy &&
strategy.GetNextBoolean(current, out next))
{
this.Trace.AddNondeterministicBooleanChoice(next, current.LastSchedulingPoint);
this.Trace.AddNondeterministicBooleanDecision(current.Id, next);
return true;
}
@ -285,7 +286,7 @@ namespace Microsoft.Coyote.Runtime
if (this.Strategy is InterleavingStrategy strategy &&
strategy.GetNextInteger(current, maxValue, out next))
{
this.Trace.AddNondeterministicIntegerChoice(next, current.LastSchedulingPoint);
this.Trace.AddNondeterministicIntegerDecision(current.Id, next);
return true;
}

15
Source/Core/Runtime/Scheduling/SchedulingPointType.cs
Просмотреть файл

@ -28,6 +28,16 @@ namespace Microsoft.Coyote.Runtime
/// </summary>
ContinueWith,
/// <summary>
/// A controlled operation is paused until its dependency is resolved.
/// </summary>
Pause,
/// <summary>
/// A controlled operation has delayed its execution.
/// </summary>
Delay,
/// <summary>
/// A controlled operation yielded its execution.
/// </summary>
@ -48,11 +58,6 @@ namespace Microsoft.Coyote.Runtime
/// </summary>
Write,
/// <summary>
/// A controlled operation is paused until its dependency is resolved.
/// </summary>
Pause,
/// <summary>
/// A controlled operation is acquiring a synchronized resource.
/// </summary>

65
Source/Core/Testing/Interleaving/InterleavingStrategy.cs
Просмотреть файл

@ -51,21 +51,24 @@ namespace Microsoft.Coyote.Testing.Interleaving
if (this.StepCount < this.TracePrefix.Length)
{
ExecutionTrace.Step nextStep = this.TracePrefix[this.StepCount];
if (nextStep.Kind != ExecutionTrace.DecisionKind.SchedulingChoice)
if (nextStep is ExecutionTrace.SchedulingStep step)
{
this.ErrorText = this.FormatReplayError(nextStep.Index, "next step is not a scheduling choice");
throw new InvalidOperationException(this.ErrorText);
}
next = ops.FirstOrDefault(op => op.Id == nextStep.ScheduledOperationId);
next = ops.FirstOrDefault(op => op.Id == step.Value);
if (next is null)
{
this.ErrorText = this.FormatReplayError(nextStep.Index, $"cannot detect id '{nextStep.ScheduledOperationId}'");
this.ErrorText = this.FormatReplayError(nextStep.Index, $"cannot detect id '{step.Value}'");
throw new InvalidOperationException(this.ErrorText);
}
else if (nextStep.SchedulingPoint != current.LastSchedulingPoint)
else if (step.SchedulingPoint != current.LastSchedulingPoint)
{
this.ErrorText = this.FormatSchedulingPointReplayError(nextStep.Index, nextStep.SchedulingPoint, current.LastSchedulingPoint);
this.ErrorText = this.FormatReplayError(nextStep.Index,
$"expected scheduling point '{step.SchedulingPoint}' instead of '{current.LastSchedulingPoint}'");
throw new InvalidOperationException(this.ErrorText);
}
}
else
{
this.ErrorText = this.FormatReplayError(nextStep.Index, "next step is not a scheduling choice");
throw new InvalidOperationException(this.ErrorText);
}
}
@ -110,24 +113,15 @@ namespace Microsoft.Coyote.Testing.Interleaving
if (this.StepCount < this.TracePrefix.Length)
{
ExecutionTrace.Step nextStep = this.TracePrefix[this.StepCount];
if (nextStep.Kind != ExecutionTrace.DecisionKind.NondeterministicChoice)
if (nextStep is ExecutionTrace.BooleanChoiceStep step)
{
next = step.Value;
}
else
{
this.ErrorText = this.FormatReplayError(nextStep.Index, "next step is not a nondeterministic choice");
throw new InvalidOperationException(this.ErrorText);
}
if (nextStep.BooleanChoice is null)
{
this.ErrorText = this.FormatReplayError(nextStep.Index, "next step is not a nondeterministic boolean choice");
throw new InvalidOperationException(this.ErrorText);
}
else if (nextStep.SchedulingPoint != current.LastSchedulingPoint)
{
this.ErrorText = this.FormatSchedulingPointReplayError(nextStep.Index, nextStep.SchedulingPoint, current.LastSchedulingPoint);
throw new InvalidOperationException(this.ErrorText);
}
next = nextStep.BooleanChoice.Value;
}
else
{
@ -168,24 +162,15 @@ namespace Microsoft.Coyote.Testing.Interleaving
if (this.StepCount < this.TracePrefix.Length)
{
ExecutionTrace.Step nextStep = this.TracePrefix[this.StepCount];
if (nextStep.Kind != ExecutionTrace.DecisionKind.NondeterministicChoice)
if (nextStep is ExecutionTrace.IntegerChoiceStep step)
{
next = step.Value;
}
else
{
this.ErrorText = this.FormatReplayError(nextStep.Index, "next step is not a nondeterministic choice");
throw new InvalidOperationException(this.ErrorText);
}
if (nextStep.IntegerChoice is null)
{
this.ErrorText = this.FormatReplayError(nextStep.Index, "next step is not a nondeterministic integer choice");
throw new InvalidOperationException(this.ErrorText);
}
else if (nextStep.SchedulingPoint != current.LastSchedulingPoint)
{
this.ErrorText = this.FormatSchedulingPointReplayError(nextStep.Index, nextStep.SchedulingPoint, current.LastSchedulingPoint);
throw new InvalidOperationException(this.ErrorText);
}
next = nextStep.IntegerChoice.Value;
}
else
{
@ -220,12 +205,6 @@ namespace Microsoft.Coyote.Testing.Interleaving
/// </remarks>
internal virtual void Reset() => this.StepCount = 0;
/// <summary>
/// Formats the error message regarding an unexpected scheduling point.
/// </summary>
private string FormatSchedulingPointReplayError(int step, SchedulingPointType expected, SchedulingPointType actual) =>
this.FormatReplayError(step, $"expected scheduling point '{expected}' instead of '{actual}'");
/// <summary>
/// Formats the error message.
/// </summary>

2
Source/Core/Web/HttpOperation.cs
Просмотреть файл

@ -24,7 +24,7 @@ namespace Microsoft.Coyote.Web
/// Initializes a new instance of the <see cref="HttpOperation"/> class.
/// </summary>
private HttpOperation(ulong operationId, HttpMethod method, string path, CoyoteRuntime runtime)
: base(operationId, $"{method}HttpOp({operationId})", null, runtime)
: base(operationId, $"{method}HttpOp({operationId})", string.Empty, null, runtime)
{
this.Method = method;
this.Path = path;

2
Source/Test/Rewriting/Types/Threading/Thread.cs
Просмотреть файл

@ -23,7 +23,7 @@ namespace Microsoft.Coyote.Rewriting.Types.Threading
if (runtime.SchedulingPolicy is SchedulingPolicy.Interleaving &&
runtime.TryGetExecutingOperation(out ControlledOperation current))
{
return runtime.ScheduleNextOperation(current, SchedulingPointType.Yield, true, true);
return runtime.ScheduleNextOperation(current, SchedulingPointType.Yield, isYielding: true);
}
return SystemThread.Yield();

186
Source/Test/SystematicTesting/Reports/TraceReport.cs
Просмотреть файл

@ -4,6 +4,7 @@
using System;
using System.Collections.Generic;
using System.Reflection;
using System.Text;
using System.Text.Encodings.Web;
using System.Text.Json;
using System.Text.Json.Serialization;
@ -33,15 +34,20 @@ namespace Microsoft.Coyote.SystematicTesting
public TestSettings Settings { get; set; }
/// <summary>
/// The controlled decisions of this trace.
/// The operations executing in this trace.
/// </summary>
public List<string> Decisions { get; set; }
public Dictionary<string, string> Operations { get; set; }
/// <summary>
/// The execution steps in this trace.
/// </summary>
public List<string> Steps { get; set; }
/// <summary>
/// Constructs a <see cref="TraceReport"/> from the specified <see cref="OperationScheduler"/>
/// and <see cref="Configuration"/>, and returns it in JSON format.
/// </summary>
internal static string GetJson(OperationScheduler scheduler, Configuration configuration)
internal static string GetJson(CoyoteRuntime runtime, OperationScheduler scheduler, Configuration configuration)
{
var report = new TraceReport();
report.TestName = configuration.TestMethodName;
@ -69,6 +75,7 @@ namespace Microsoft.Coyote.SystematicTesting
report.Settings.UncontrolledConcurrencyResolutionAttempts = configuration.UncontrolledConcurrencyResolutionAttempts;
report.Settings.UncontrolledConcurrencyResolutionDelay = configuration.UncontrolledConcurrencyResolutionDelay;
report.ReportOperations(runtime.OperationMap);
report.ReportTrace(scheduler.Trace);
return report.ToJson();
}
@ -110,35 +117,43 @@ namespace Microsoft.Coyote.SystematicTesting
configuration.UncontrolledConcurrencyResolutionAttempts = report.Settings.UncontrolledConcurrencyResolutionAttempts;
configuration.UncontrolledConcurrencyResolutionDelay = report.Settings.UncontrolledConcurrencyResolutionDelay;
foreach (var decision in report.Decisions)
for (int idx = 0; idx < report.Steps.Count; idx++)
{
string[] tokens = decision.Split(',');
string kindToken = tokens[0];
string spToken = tokens[1];
string[] tokens = report.Steps[idx].Split(',');
string opToken = tokens[0];
string decisionToken = tokens[1];
ulong op = ulong.Parse(opToken.Substring(3, opToken.Length - 4));
if (decisionToken.StartsWith("sp("))
{
#if NET || NETCOREAPP3_1
SchedulingPointType sp = Enum.Parse<SchedulingPointType>(spToken.Substring(3, spToken.Length - 4));
SchedulingPointType sp = Enum.Parse<SchedulingPointType>(decisionToken.Substring(
3, decisionToken.Length - 4));
#else
SchedulingPointType sp = (SchedulingPointType)Enum.Parse(typeof(SchedulingPointType), spToken.Substring(3, spToken.Length - 4));
SchedulingPointType sp = (SchedulingPointType)Enum.Parse(typeof(SchedulingPointType),
decisionToken.Substring(3, decisionToken.Length - 4));
#endif
if (kindToken.StartsWith("op("))
{
ulong id = ulong.Parse(kindToken.Substring(3, kindToken.Length - 4));
trace.AddSchedulingChoice(id, sp);
string targetToken = tokens[2];
string nextToken = tokens[3];
ulong target = ulong.Parse(targetToken.Substring(7, targetToken.Length - 8));
ulong next = ulong.Parse(nextToken.Substring(5, nextToken.Length - 6));
trace.AddSchedulingDecision(op, sp, target, next);
}
else if (kindToken.StartsWith("bool("))
else if (decisionToken.StartsWith("bool("))
{
bool value = bool.Parse(kindToken.Substring(5, kindToken.Length - 6));
trace.AddNondeterministicBooleanChoice(value, sp);
bool value = bool.Parse(decisionToken.Substring(5, decisionToken.Length - 6));
trace.AddNondeterministicBooleanDecision(op, value);
}
else if (kindToken.StartsWith("int("))
else if (decisionToken.StartsWith("int("))
{
int value = int.Parse(kindToken.Substring(4, kindToken.Length - 5));
trace.AddNondeterministicIntegerChoice(value, sp);
int value = int.Parse(decisionToken.Substring(4, decisionToken.Length - 5));
trace.AddNondeterministicIntegerDecision(op, value);
}
else
{
throw new InvalidOperationException($"Unexpected decision '{decision}'.");
throw new InvalidOperationException($"Unexpected execution step '{report.Steps[idx]}'.");
}
}
}
@ -146,26 +161,141 @@ namespace Microsoft.Coyote.SystematicTesting
return trace;
}
/// <summary>
/// Constructs a visualization graph from the specified parameters, and returns it in DOT format.
/// </summary>
internal static string GetGraph(CoyoteRuntime runtime, ExecutionTrace trace)
{
StringBuilder graph = new StringBuilder();
graph.AppendLine("digraph trace {");
if (trace.Length > 1)
{
// The first operation is always the main thread running the test method.
string firstOp = $"op(0)";
string firstDescription = runtime.OperationMap[0].Description;
string next = string.Empty;
var completedOps = new HashSet<ulong>();
var chainMap = new Dictionary<ulong, HashSet<ulong>>();
var aliasMap = new Dictionary<string, HashSet<ulong>>();
int stepCount = 0;
for (int idx = 0; idx < trace.Length; idx++)
{
if (trace[idx] is ExecutionTrace.SchedulingStep step)
{
string op = $"op({step.Current})";
string name = runtime.OperationMap[step.Current].Description;
string source = $"{name}({op})";
if (!chainMap.TryGetValue(step.Current, out HashSet<ulong> opChain))
{
opChain = new HashSet<ulong>();
chainMap.Add(step.Current, opChain);
}
if (!aliasMap.TryGetValue(name, out HashSet<ulong> opAliases))
{
opAliases = new HashSet<ulong>();
aliasMap.Add(name, opAliases);
}
opChain.Add(step.Current);
opAliases.Add(step.Current);
string nextOp = $"op({step.Value})";
string nextName = runtime.OperationMap[step.Value].Description;
next = $"{nextName}({nextOp})";
if (step.SchedulingPoint is SchedulingPointType.Create)
{
string targetOp = $"op({step.Target})";
string targetName = runtime.OperationMap[step.Target].Description;
string target = $"{targetName}({targetOp})";
graph.Append($" \"{source}\" -> \"{target}\"");
graph.AppendLine($" [label=\" {step.SchedulingPoint} [{stepCount}] \" color=\"#3868ceff\"];");
stepCount++;
}
else if (step.SchedulingPoint is SchedulingPointType.ContinueWith)
{
opChain.Add(step.Target);
if (!chainMap.ContainsKey(step.Target))
{
chainMap.Add(step.Target, opChain);
}
}
else if (step.SchedulingPoint is SchedulingPointType.Complete)
{
completedOps.Add(step.Current);
}
else if (step.Current != step.Target || opAliases.Count > 0)
{
graph.Append($" \"{source}\" -> \"{next}\"");
graph.AppendLine($" [label=\" {step.SchedulingPoint} [{stepCount}] \",style=dashed];");
stepCount++;
}
}
else
{
continue;
}
}
// Write the error state.
graph.Append($" \"{next}\" -> error");
graph.AppendLine($" [label=\" [{stepCount}] \",color=\"#ce3838ff\"];");
// Write the style options.
graph.AppendLine();
graph.AppendLine($" \"{firstDescription}\"[shape=box];");
graph.AppendLine(" error[shape=Mdiamond,color=\"#ce3838ff\"];");
}
else
{
// Write the empty graph.
graph.AppendLine(" \"N/A\"[shape=Mdiamond];");
}
graph.AppendLine("}");
return graph.ToString();
}
/// <summary>
/// Adds the specified entity information to the report.
/// </summary>
internal void ReportOperations(Dictionary<ulong, ControlledOperation> operations)
{
this.Operations = new Dictionary<string, string>();
foreach (var op in operations.Values)
{
this.Operations.Add($"op({op.Id})", op.Description);
}
}
/// <summary>
/// Adds the specified trace to the report.
/// </summary>
internal void ReportTrace(ExecutionTrace trace)
{
this.Decisions = new List<string>();
this.Steps = new List<string>();
if (trace.Length > 0)
{
for (int idx = 0; idx < trace.Length; idx++)
{
ExecutionTrace.Step step = trace[idx];
if (step.Kind == ExecutionTrace.DecisionKind.SchedulingChoice)
if (trace[idx] is ExecutionTrace.SchedulingStep step)
{
this.Decisions.Add($"op({step.ScheduledOperationId}),sp({step.SchedulingPoint})");
this.Steps.Add($"op({step.Current}),sp({step.SchedulingPoint}),target({step.Target}),next({step.Value})");
}
else if (step.BooleanChoice != null)
else if (trace[idx] is ExecutionTrace.BooleanChoiceStep boolChoiceStep)
{
this.Decisions.Add($"bool({step.BooleanChoice.Value}),sp({step.SchedulingPoint})");
this.Steps.Add($"op({boolChoiceStep.Current}),bool({boolChoiceStep.Value})");
}
else
else if (trace[idx] is ExecutionTrace.IntegerChoiceStep intChoiceStep)
{
this.Decisions.Add($"int({step.IntegerChoice.Value}),sp({step.SchedulingPoint})");
this.Steps.Add($"op({intChoiceStep.Current}),int({intChoiceStep.Value})");
}
}
}
}

44
Source/Test/SystematicTesting/TestingEngine.cs
Просмотреть файл

@ -83,7 +83,7 @@ namespace Microsoft.Coyote.SystematicTesting
private readonly LogWriter LogWriter;
/// <summary>
/// The DGML coverage graph of the execution path explored in the last iteration.
/// The coverage graph of the execution path explored in the last iteration.
/// </summary>
private CoverageGraph LastCoverageGraph;
@ -93,16 +93,21 @@ namespace Microsoft.Coyote.SystematicTesting
/// </summary>
private StringBuilder XmlLog;
/// <summary>
/// The readable trace, if any.
/// </summary>
public string ReadableTrace { get; private set; }
/// <summary>
/// The reproducible trace, if any.
/// </summary>
public string ReproducibleTrace { get; private set; }
/// <summary>
/// The visual trace in DOT format, if any.
/// </summary>
public string VisualTrace { get; private set; }
/// <summary>
/// The readable trace, if any.
/// </summary>
public string ReadableTrace { get; private set; }
/// <summary>
/// A guard for printing info.
/// </summary>
@ -181,8 +186,9 @@ namespace Microsoft.Coyote.SystematicTesting
this.StartIterationCallbacks = new HashSet<Action<uint>>();
this.EndIterationCallbacks = new HashSet<Action<uint>>();
this.TestReport = new TestReport(configuration);
this.ReadableTrace = string.Empty;
this.ReproducibleTrace = string.Empty;
this.VisualTrace = string.Empty;
this.ReadableTrace = string.Empty;
this.CancellationTokenSource = new CancellationTokenSource();
this.PrintGuard = 1;
this.EngineLock = new object();
@ -408,7 +414,8 @@ namespace Microsoft.Coyote.SystematicTesting
if (runtime.SchedulingPolicy is SchedulingPolicy.Interleaving)
{
this.ReproducibleTrace = TraceReport.GetJson(this.Scheduler, this.Configuration);
this.ReproducibleTrace = TraceReport.GetJson(runtime, this.Scheduler, this.Configuration);
this.VisualTrace = TraceReport.GetGraph(runtime, this.Scheduler.Trace);
}
}
@ -515,11 +522,19 @@ namespace Microsoft.Coyote.SystematicTesting
paths.Add(xmlPath);
}
if (this.LastCoverageGraph != null && this.TestReport.NumOfFoundBugs > 0)
// if (this.LastCoverageGraph != null && this.TestReport.NumOfFoundBugs > 0)
// {
// string extension = this.Configuration.IsDgmlFormatEnabled ? "dgml" : "gv";
// string graphPath = Path.Combine(directory, fileName + $".trace.{extension}");
// this.LastCoverageGraph.Save(graphPath, true, this.Configuration.IsDgmlFormatEnabled);
// paths.Add(graphPath);
// }
if (!string.IsNullOrEmpty(this.VisualTrace))
{
string graphPath = Path.Combine(directory, fileName + ".trace.dgml");
this.LastCoverageGraph.SaveDgml(graphPath, true);
paths.Add(graphPath);
string visualTracePath = Path.Combine(directory, fileName + $".trace.gv");
File.WriteAllText(visualTracePath, this.VisualTrace);
paths.Add(visualTracePath);
}
// Emits the reproducible trace, if it exists.
@ -553,8 +568,9 @@ namespace Microsoft.Coyote.SystematicTesting
var coverageReporter = new CoverageReporter(this.TestReport.CoverageInfo);
if (this.Configuration.IsActivityCoverageReported)
{
string graphFilePath = Path.Combine(directory, fileName + ".coverage.dgml");
if (coverageReporter.TryEmitVisualizationGraph(graphFilePath))
string extension = this.Configuration.IsDgmlFormatEnabled ? "dgml" : "gv";
string graphFilePath = Path.Combine(directory, fileName + $".coverage.{extension}");
if (coverageReporter.TryEmitVisualizationGraph(graphFilePath, this.Configuration.IsDgmlFormatEnabled))
{
paths.Add(graphFilePath);
}

290
Tests/Tests.Runtime/Exploration/ExecutionTraceTests.cs
Просмотреть файл

@ -20,43 +20,33 @@ namespace Microsoft.Coyote.Runtime.Tests
ExecutionTrace trace = ExecutionTrace.Create();
Assert.True(trace.Length is 0);
trace.AddSchedulingChoice(0, SchedulingPointType.Default);
trace.AddSchedulingChoice(2, SchedulingPointType.Default);
trace.AddSchedulingChoice(3, SchedulingPointType.Default);
trace.AddSchedulingChoice(1, SchedulingPointType.Default);
trace.AddSchedulingChoice(2, SchedulingPointType.Default);
trace.AddSchedulingDecision(0, SchedulingPointType.Default, 0, 0);
trace.AddSchedulingDecision(0, SchedulingPointType.Default, 0, 2);
trace.AddSchedulingDecision(0, SchedulingPointType.Default, 0, 3);
trace.AddSchedulingDecision(0, SchedulingPointType.Default, 0, 1);
trace.AddSchedulingDecision(0, SchedulingPointType.Default, 0, 2);
this.LogTrace(trace);
Assert.True(trace.Length is 5);
Assert.True(trace[0].Index is 0);
Assert.True(trace[0].Kind is ExecutionTrace.DecisionKind.SchedulingChoice);
Assert.True(trace[0].ScheduledOperationId is 0);
Assert.True(!trace[0].BooleanChoice.HasValue);
Assert.True(!trace[0].IntegerChoice.HasValue);
Assert.True(trace[0] is ExecutionTrace.SchedulingStep);
Assert.True((trace[0] as ExecutionTrace.SchedulingStep).Value is 0);
Assert.True(trace[1].Index is 1);
Assert.True(trace[1].Kind is ExecutionTrace.DecisionKind.SchedulingChoice);
Assert.True(trace[1].ScheduledOperationId is 2);
Assert.True(!trace[1].BooleanChoice.HasValue);
Assert.True(!trace[1].IntegerChoice.HasValue);
Assert.True(trace[1] is ExecutionTrace.SchedulingStep);
Assert.True((trace[1] as ExecutionTrace.SchedulingStep).Value is 2);
Assert.True(trace[2].Index is 2);
Assert.True(trace[2].Kind is ExecutionTrace.DecisionKind.SchedulingChoice);
Assert.True(trace[2].ScheduledOperationId is 3);
Assert.True(!trace[2].BooleanChoice.HasValue);
Assert.True(!trace[2].IntegerChoice.HasValue);
Assert.True(trace[2] is ExecutionTrace.SchedulingStep);
Assert.True((trace[2] as ExecutionTrace.SchedulingStep).Value is 3);
Assert.True(trace[3].Index is 3);
Assert.True(trace[3].Kind is ExecutionTrace.DecisionKind.SchedulingChoice);
Assert.True(trace[3].ScheduledOperationId is 1);
Assert.True(!trace[3].BooleanChoice.HasValue);
Assert.True(!trace[3].IntegerChoice.HasValue);
Assert.True(trace[3] is ExecutionTrace.SchedulingStep);
Assert.True((trace[3] as ExecutionTrace.SchedulingStep).Value is 1);
Assert.True(trace[4].Index is 4);
Assert.True(trace[4].Kind is ExecutionTrace.DecisionKind.SchedulingChoice);
Assert.True(trace[4].ScheduledOperationId is 2);
Assert.True(!trace[4].BooleanChoice.HasValue);
Assert.True(!trace[4].IntegerChoice.HasValue);
Assert.True(trace[4] is ExecutionTrace.SchedulingStep);
Assert.True((trace[4] as ExecutionTrace.SchedulingStep).Value is 2);
}
[Fact(Timeout = 5000)]
@ -65,32 +55,23 @@ namespace Microsoft.Coyote.Runtime.Tests
ExecutionTrace trace = ExecutionTrace.Create();
Assert.True(trace.Length is 0);
trace.AddNondeterministicBooleanChoice(true, SchedulingPointType.Default);
trace.AddNondeterministicBooleanChoice(false, SchedulingPointType.Default);
trace.AddNondeterministicBooleanChoice(true, SchedulingPointType.Default);
trace.AddNondeterministicBooleanDecision(0, true);
trace.AddNondeterministicBooleanDecision(0, false);
trace.AddNondeterministicBooleanDecision(0, true);
this.LogTrace(trace);
Assert.True(trace.Length is 3);
Assert.True(trace[0].Index is 0);
Assert.True(trace[0].Kind is ExecutionTrace.DecisionKind.NondeterministicChoice);
Assert.True(trace[0].ScheduledOperationId is 0);
Assert.True(trace[0].BooleanChoice.HasValue);
Assert.True(trace[0].BooleanChoice.Value is true);
Assert.True(!trace[0].IntegerChoice.HasValue);
Assert.True(trace[0] is ExecutionTrace.BooleanChoiceStep);
Assert.True((trace[0] as ExecutionTrace.BooleanChoiceStep).Value is true);
Assert.True(trace[1].Index is 1);
Assert.True(trace[1].Kind is ExecutionTrace.DecisionKind.NondeterministicChoice);
Assert.True(trace[1].ScheduledOperationId is 0);
Assert.True(trace[1].BooleanChoice.HasValue);
Assert.True(trace[1].BooleanChoice.Value is false);
Assert.True(!trace[1].IntegerChoice.HasValue);
Assert.True(trace[1] is ExecutionTrace.BooleanChoiceStep);
Assert.True((trace[1] as ExecutionTrace.BooleanChoiceStep).Value is false);
Assert.True(trace[2].Index is 2);
Assert.True(trace[2].Kind is ExecutionTrace.DecisionKind.NondeterministicChoice);
Assert.True(trace[2].ScheduledOperationId is 0);
Assert.True(trace[2].BooleanChoice.HasValue);
Assert.True(trace[2].BooleanChoice.Value is true);
Assert.True(!trace[2].IntegerChoice.HasValue);
Assert.True(trace[2] is ExecutionTrace.BooleanChoiceStep);
Assert.True((trace[2] as ExecutionTrace.BooleanChoiceStep).Value is true);
}
[Fact(Timeout = 5000)]
@ -99,32 +80,23 @@ namespace Microsoft.Coyote.Runtime.Tests
ExecutionTrace trace = ExecutionTrace.Create();
Assert.True(trace.Length is 0);
trace.AddNondeterministicIntegerChoice(3, SchedulingPointType.Default);
trace.AddNondeterministicIntegerChoice(7, SchedulingPointType.Default);
trace.AddNondeterministicIntegerChoice(4, SchedulingPointType.Default);
trace.AddNondeterministicIntegerDecision(0, 3);
trace.AddNondeterministicIntegerDecision(0, 7);
trace.AddNondeterministicIntegerDecision(0, 4);
this.LogTrace(trace);
Assert.True(trace.Length is 3);
Assert.True(trace[0].Index is 0);
Assert.True(trace[0].Kind is ExecutionTrace.DecisionKind.NondeterministicChoice);
Assert.True(trace[0].ScheduledOperationId is 0);
Assert.True(!trace[0].BooleanChoice.HasValue);
Assert.True(trace[0].IntegerChoice.HasValue);
Assert.True(trace[0].IntegerChoice.Value is 3);
Assert.True(trace[0] is ExecutionTrace.IntegerChoiceStep);
Assert.True((trace[0] as ExecutionTrace.IntegerChoiceStep).Value is 3);
Assert.True(trace[1].Index is 1);
Assert.True(trace[1].Kind is ExecutionTrace.DecisionKind.NondeterministicChoice);
Assert.True(trace[1].ScheduledOperationId is 0);
Assert.True(!trace[1].BooleanChoice.HasValue);
Assert.True(trace[1].IntegerChoice.HasValue);
Assert.True(trace[1].IntegerChoice.Value is 7);
Assert.True(trace[1] is ExecutionTrace.IntegerChoiceStep);
Assert.True((trace[1] as ExecutionTrace.IntegerChoiceStep).Value is 7);
Assert.True(trace[2].Index is 2);
Assert.True(trace[2].Kind is ExecutionTrace.DecisionKind.NondeterministicChoice);
Assert.True(trace[2].ScheduledOperationId is 0);
Assert.True(!trace[2].BooleanChoice.HasValue);
Assert.True(trace[2].IntegerChoice.HasValue);
Assert.True(trace[2].IntegerChoice.Value is 4);
Assert.True(trace[2] is ExecutionTrace.IntegerChoiceStep);
Assert.True((trace[2] as ExecutionTrace.IntegerChoiceStep).Value is 4);
}
[Fact(Timeout = 5000)]
@ -133,45 +105,33 @@ namespace Microsoft.Coyote.Runtime.Tests
ExecutionTrace trace = ExecutionTrace.Create();
Assert.True(trace.Length is 0);
trace.AddSchedulingChoice(0, SchedulingPointType.Default);
trace.AddSchedulingChoice(2, SchedulingPointType.Default);
trace.AddNondeterministicBooleanChoice(true, SchedulingPointType.Default);
trace.AddSchedulingChoice(1, SchedulingPointType.Default);
trace.AddNondeterministicIntegerChoice(5, SchedulingPointType.Default);
trace.AddSchedulingDecision(0, SchedulingPointType.Default, 0, 0);
trace.AddSchedulingDecision(0, SchedulingPointType.Default, 0, 2);
trace.AddNondeterministicBooleanDecision(0, true);
trace.AddSchedulingDecision(0, SchedulingPointType.Default, 0, 1);
trace.AddNondeterministicIntegerDecision(0, 5);
this.LogTrace(trace);
Assert.True(trace.Length is 5);
Assert.True(trace[0].Index is 0);
Assert.True(trace[0].Kind is ExecutionTrace.DecisionKind.SchedulingChoice);
Assert.True(trace[0].ScheduledOperationId is 0);
Assert.True(!trace[0].BooleanChoice.HasValue);
Assert.True(!trace[0].IntegerChoice.HasValue);
Assert.True(trace[0] is ExecutionTrace.SchedulingStep);
Assert.True((trace[0] as ExecutionTrace.SchedulingStep).Value is 0);
Assert.True(trace[1].Index is 1);
Assert.True(trace[1].Kind is ExecutionTrace.DecisionKind.SchedulingChoice);
Assert.True(trace[1].ScheduledOperationId is 2);
Assert.True(!trace[1].BooleanChoice.HasValue);
Assert.True(!trace[1].IntegerChoice.HasValue);
Assert.True(trace[1] is ExecutionTrace.SchedulingStep);
Assert.True((trace[1] as ExecutionTrace.SchedulingStep).Value is 2);
Assert.True(trace[2].Index is 2);
Assert.True(trace[2].Kind is ExecutionTrace.DecisionKind.NondeterministicChoice);
Assert.True(trace[2].ScheduledOperationId is 0);
Assert.True(trace[2].BooleanChoice.HasValue);
Assert.True(trace[2].BooleanChoice.Value is true);
Assert.True(!trace[2].IntegerChoice.HasValue);
Assert.True(trace[2] is ExecutionTrace.BooleanChoiceStep);
Assert.True((trace[2] as ExecutionTrace.BooleanChoiceStep).Value is true);
Assert.True(trace[3].Index is 3);
Assert.True(trace[3].Kind is ExecutionTrace.DecisionKind.SchedulingChoice);
Assert.True(trace[3].ScheduledOperationId is 1);
Assert.True(!trace[3].BooleanChoice.HasValue);
Assert.True(!trace[3].IntegerChoice.HasValue);
Assert.True(trace[3] is ExecutionTrace.SchedulingStep);
Assert.True((trace[3] as ExecutionTrace.SchedulingStep).Value is 1);
Assert.True(trace[4].Index is 4);
Assert.True(trace[4].Kind is ExecutionTrace.DecisionKind.NondeterministicChoice);
Assert.True(trace[4].ScheduledOperationId is 0);
Assert.True(!trace[4].BooleanChoice.HasValue);
Assert.True(trace[4].IntegerChoice.HasValue);
Assert.True(trace[4].IntegerChoice.Value is 5);
Assert.True(trace[4] is ExecutionTrace.IntegerChoiceStep);
Assert.True((trace[4] as ExecutionTrace.IntegerChoiceStep).Value is 5);
}
[Fact(Timeout = 5000)]
@ -180,17 +140,17 @@ namespace Microsoft.Coyote.Runtime.Tests
ExecutionTrace trace = ExecutionTrace.Create();
Assert.True(trace.Length is 0);
trace.AddSchedulingChoice(0, SchedulingPointType.Default);
trace.AddSchedulingChoice(2, SchedulingPointType.Default);
trace.AddNondeterministicBooleanChoice(true, SchedulingPointType.Default);
trace.AddSchedulingDecision(0, SchedulingPointType.Default, 0, 0);
trace.AddSchedulingDecision(0, SchedulingPointType.Default, 0, 2);
trace.AddNondeterministicBooleanDecision(0, true);
this.LogTrace(trace);
Assert.True(trace.Length is 3);
ExecutionTrace other = ExecutionTrace.Create();
Assert.True(other.Length is 0);
other.AddSchedulingChoice(0, SchedulingPointType.Default);
other.AddSchedulingChoice(2, SchedulingPointType.Default);
other.AddSchedulingDecision(0, SchedulingPointType.Default, 0, 0);
other.AddSchedulingDecision(0, SchedulingPointType.Default, 0, 2);
this.LogTrace(other);
Assert.True(other.Length is 2);
@ -199,23 +159,16 @@ namespace Microsoft.Coyote.Runtime.Tests
Assert.True(trace.Length is 3);
Assert.True(trace[0].Index is 0);
Assert.True(trace[0].Kind is ExecutionTrace.DecisionKind.SchedulingChoice);
Assert.True(trace[0].ScheduledOperationId is 0);
Assert.True(!trace[0].BooleanChoice.HasValue);
Assert.True(!trace[0].IntegerChoice.HasValue);
Assert.True(trace[0] is ExecutionTrace.SchedulingStep);
Assert.True((trace[0] as ExecutionTrace.SchedulingStep).Value is 0);
Assert.True(trace[1].Index is 1);
Assert.True(trace[1].Kind is ExecutionTrace.DecisionKind.SchedulingChoice);
Assert.True(trace[1].ScheduledOperationId is 2);
Assert.True(!trace[1].BooleanChoice.HasValue);
Assert.True(!trace[1].IntegerChoice.HasValue);
Assert.True(trace[1] is ExecutionTrace.SchedulingStep);
Assert.True((trace[1] as ExecutionTrace.SchedulingStep).Value is 2);
Assert.True(trace[2].Index is 2);
Assert.True(trace[2].Kind is ExecutionTrace.DecisionKind.NondeterministicChoice);
Assert.True(trace[2].ScheduledOperationId is 0);
Assert.True(trace[2].BooleanChoice.HasValue);
Assert.True(trace[2].BooleanChoice.Value is true);
Assert.True(!trace[2].IntegerChoice.HasValue);
Assert.True(trace[2] is ExecutionTrace.BooleanChoiceStep);
Assert.True((trace[2] as ExecutionTrace.BooleanChoiceStep).Value is true);
}
[Fact(Timeout = 5000)]
@ -224,20 +177,20 @@ namespace Microsoft.Coyote.Runtime.Tests
ExecutionTrace trace = ExecutionTrace.Create();
Assert.True(trace.Length is 0);
trace.AddSchedulingChoice(0, SchedulingPointType.Default);
trace.AddSchedulingChoice(2, SchedulingPointType.Default);
trace.AddNondeterministicBooleanChoice(true, SchedulingPointType.Default);
trace.AddSchedulingDecision(0, SchedulingPointType.Default, 0, 0);
trace.AddSchedulingDecision(0, SchedulingPointType.Default, 0, 2);
trace.AddNondeterministicBooleanDecision(0, true);
this.LogTrace(trace);
Assert.True(trace.Length is 3);
ExecutionTrace other = ExecutionTrace.Create();
Assert.True(other.Length is 0);
other.AddSchedulingChoice(0, SchedulingPointType.Default);
other.AddSchedulingChoice(2, SchedulingPointType.Default);
other.AddNondeterministicBooleanChoice(true, SchedulingPointType.Default);
other.AddSchedulingChoice(1, SchedulingPointType.Default);
other.AddNondeterministicIntegerChoice(5, SchedulingPointType.Default);
other.AddSchedulingDecision(0, SchedulingPointType.Default, 0, 0);
other.AddSchedulingDecision(0, SchedulingPointType.Default, 0, 2);
other.AddNondeterministicBooleanDecision(0, true);
other.AddSchedulingDecision(0, SchedulingPointType.Default, 0, 1);
other.AddNondeterministicIntegerDecision(0, 5);
this.LogTrace(other);
Assert.True(other.Length is 5);
@ -246,36 +199,24 @@ namespace Microsoft.Coyote.Runtime.Tests
Assert.True(trace.Length is 5);
Assert.True(trace[0].Index is 0);
Assert.True(trace[0].Kind is ExecutionTrace.DecisionKind.SchedulingChoice);
Assert.True(trace[0].ScheduledOperationId is 0);
Assert.True(!trace[0].BooleanChoice.HasValue);
Assert.True(!trace[0].IntegerChoice.HasValue);
Assert.True(trace[0] is ExecutionTrace.SchedulingStep);
Assert.True((trace[0] as ExecutionTrace.SchedulingStep).Value is 0);
Assert.True(trace[1].Index is 1);
Assert.True(trace[1].Kind is ExecutionTrace.DecisionKind.SchedulingChoice);
Assert.True(trace[1].ScheduledOperationId is 2);
Assert.True(!trace[1].BooleanChoice.HasValue);
Assert.True(!trace[1].IntegerChoice.HasValue);
Assert.True(trace[1] is ExecutionTrace.SchedulingStep);
Assert.True((trace[1] as ExecutionTrace.SchedulingStep).Value is 2);
Assert.True(trace[2].Index is 2);
Assert.True(trace[2].Kind is ExecutionTrace.DecisionKind.NondeterministicChoice);
Assert.True(trace[2].ScheduledOperationId is 0);
Assert.True(trace[2].BooleanChoice.HasValue);
Assert.True(trace[2].BooleanChoice.Value is true);
Assert.True(!trace[2].IntegerChoice.HasValue);
Assert.True(trace[2] is ExecutionTrace.BooleanChoiceStep);
Assert.True((trace[2] as ExecutionTrace.BooleanChoiceStep).Value is true);
Assert.True(trace[3].Index is 3);
Assert.True(trace[3].Kind is ExecutionTrace.DecisionKind.SchedulingChoice);
Assert.True(trace[3].ScheduledOperationId is 1);
Assert.True(!trace[3].BooleanChoice.HasValue);
Assert.True(!trace[3].IntegerChoice.HasValue);
Assert.True(trace[3] is ExecutionTrace.SchedulingStep);
Assert.True((trace[3] as ExecutionTrace.SchedulingStep).Value is 1);
Assert.True(trace[4].Index is 4);
Assert.True(trace[4].Kind is ExecutionTrace.DecisionKind.NondeterministicChoice);
Assert.True(trace[4].ScheduledOperationId is 0);
Assert.True(!trace[4].BooleanChoice.HasValue);
Assert.True(trace[4].IntegerChoice.HasValue);
Assert.True(trace[4].IntegerChoice.Value is 5);
Assert.True(trace[4] is ExecutionTrace.IntegerChoiceStep);
Assert.True((trace[4] as ExecutionTrace.IntegerChoiceStep).Value is 5);
}
[Fact(Timeout = 5000)]
@ -284,9 +225,9 @@ namespace Microsoft.Coyote.Runtime.Tests
ExecutionTrace trace = ExecutionTrace.Create();
Assert.True(trace.Length is 0);
trace.AddSchedulingChoice(0, SchedulingPointType.Default);
trace.AddSchedulingChoice(3, SchedulingPointType.Default);
trace.AddNondeterministicBooleanChoice(false, SchedulingPointType.Default);
trace.AddSchedulingDecision(0, SchedulingPointType.Default, 0, 0);
trace.AddSchedulingDecision(0, SchedulingPointType.Default, 0, 3);
trace.AddNondeterministicBooleanDecision(0, false);
this.LogTrace(trace);
Assert.True(trace.Length is 3);
@ -305,17 +246,17 @@ namespace Microsoft.Coyote.Runtime.Tests
ExecutionTrace trace = ExecutionTrace.Create();
Assert.True(trace.Length is 0);
trace.AddSchedulingChoice(0, SchedulingPointType.Default);
trace.AddSchedulingChoice(3, SchedulingPointType.Default);
trace.AddNondeterministicBooleanChoice(true, SchedulingPointType.Default);
trace.AddSchedulingDecision(0, SchedulingPointType.Default, 0, 0);
trace.AddSchedulingDecision(0, SchedulingPointType.Default, 0, 3);
trace.AddNondeterministicBooleanDecision(0, true);
this.LogTrace(trace);
Assert.True(trace.Length is 3);
ExecutionTrace other = ExecutionTrace.Create();
Assert.True(other.Length is 0);
other.AddSchedulingChoice(0, SchedulingPointType.Default);
other.AddNondeterministicIntegerChoice(5, SchedulingPointType.Default);
other.AddSchedulingDecision(0, SchedulingPointType.Default, 0, 0);
other.AddNondeterministicIntegerDecision(0, 5);
this.LogTrace(other);
Assert.True(other.Length is 2);
@ -324,17 +265,12 @@ namespace Microsoft.Coyote.Runtime.Tests
Assert.True(trace.Length is 2);
Assert.True(trace[0].Index is 0);
Assert.True(trace[0].Kind is ExecutionTrace.DecisionKind.SchedulingChoice);
Assert.True(trace[0].ScheduledOperationId is 0);
Assert.True(!trace[0].BooleanChoice.HasValue);
Assert.True(!trace[0].IntegerChoice.HasValue);
Assert.True(trace[0] is ExecutionTrace.SchedulingStep);
Assert.True((trace[0] as ExecutionTrace.SchedulingStep).Value is 0);
Assert.True(trace[1].Index is 1);
Assert.True(trace[1].Kind is ExecutionTrace.DecisionKind.NondeterministicChoice);
Assert.True(trace[1].ScheduledOperationId is 0);
Assert.True(!trace[1].BooleanChoice.HasValue);
Assert.True(trace[1].IntegerChoice.HasValue);
Assert.True(trace[1].IntegerChoice.Value is 5);
Assert.True(trace[1] is ExecutionTrace.IntegerChoiceStep);
Assert.True((trace[1] as ExecutionTrace.IntegerChoiceStep).Value is 5);
}
[Fact(Timeout = 5000)]
@ -343,20 +279,20 @@ namespace Microsoft.Coyote.Runtime.Tests
ExecutionTrace trace = ExecutionTrace.Create();
Assert.True(trace.Length is 0);
trace.AddSchedulingChoice(0, SchedulingPointType.Default);
trace.AddSchedulingChoice(2, SchedulingPointType.Default);
trace.AddNondeterministicBooleanChoice(true, SchedulingPointType.Default);
trace.AddSchedulingDecision(0, SchedulingPointType.Default, 0, 0);
trace.AddSchedulingDecision(0, SchedulingPointType.Default, 0, 2);
trace.AddNondeterministicBooleanDecision(0, true);
this.LogTrace(trace);
Assert.True(trace.Length is 3);
ExecutionTrace other = ExecutionTrace.Create();
Assert.True(other.Length is 0);
other.AddSchedulingChoice(0, SchedulingPointType.Default);
other.AddSchedulingChoice(3, SchedulingPointType.Default);
other.AddNondeterministicBooleanChoice(false, SchedulingPointType.Default);
other.AddSchedulingChoice(1, SchedulingPointType.Default);
other.AddNondeterministicIntegerChoice(5, SchedulingPointType.Default);
other.AddSchedulingDecision(0, SchedulingPointType.Default, 0, 0);
other.AddSchedulingDecision(0, SchedulingPointType.Default, 0, 3);
other.AddNondeterministicBooleanDecision(0, false);
other.AddSchedulingDecision(0, SchedulingPointType.Default, 0, 1);
other.AddNondeterministicIntegerDecision(0, 5);
this.LogTrace(other);
Assert.True(other.Length is 5);
@ -365,36 +301,24 @@ namespace Microsoft.Coyote.Runtime.Tests
Assert.True(trace.Length is 5);
Assert.True(trace[0].Index is 0);
Assert.True(trace[0].Kind is ExecutionTrace.DecisionKind.SchedulingChoice);
Assert.True(trace[0].ScheduledOperationId is 0);
Assert.True(!trace[0].BooleanChoice.HasValue);
Assert.True(!trace[0].IntegerChoice.HasValue);
Assert.True(trace[0] is ExecutionTrace.SchedulingStep);
Assert.True((trace[0] as ExecutionTrace.SchedulingStep).Value is 0);
Assert.True(trace[1].Index is 1);
Assert.True(trace[1].Kind is ExecutionTrace.DecisionKind.SchedulingChoice);
Assert.True(trace[1].ScheduledOperationId is 3);
Assert.True(!trace[1].BooleanChoice.HasValue);
Assert.True(!trace[1].IntegerChoice.HasValue);
Assert.True(trace[1] is ExecutionTrace.SchedulingStep);
Assert.True((trace[1] as ExecutionTrace.SchedulingStep).Value is 3);
Assert.True(trace[2].Index is 2);
Assert.True(trace[2].Kind is ExecutionTrace.DecisionKind.NondeterministicChoice);
Assert.True(trace[2].ScheduledOperationId is 0);
Assert.True(trace[2].BooleanChoice.HasValue);
Assert.True(trace[2].BooleanChoice.Value is false);
Assert.True(!trace[2].IntegerChoice.HasValue);
Assert.True(trace[2] is ExecutionTrace.BooleanChoiceStep);
Assert.True((trace[2] as ExecutionTrace.BooleanChoiceStep).Value is false);
Assert.True(trace[3].Index is 3);
Assert.True(trace[3].Kind is ExecutionTrace.DecisionKind.SchedulingChoice);
Assert.True(trace[3].ScheduledOperationId is 1);
Assert.True(!trace[3].BooleanChoice.HasValue);
Assert.True(!trace[3].IntegerChoice.HasValue);
Assert.True(trace[3] is ExecutionTrace.SchedulingStep);
Assert.True((trace[3] as ExecutionTrace.SchedulingStep).Value is 1);
Assert.True(trace[4].Index is 4);
Assert.True(trace[4].Kind is ExecutionTrace.DecisionKind.NondeterministicChoice);
Assert.True(trace[4].ScheduledOperationId is 0);
Assert.True(!trace[4].BooleanChoice.HasValue);
Assert.True(trace[4].IntegerChoice.HasValue);
Assert.True(trace[4].IntegerChoice.Value is 5);
Assert.True(trace[4] is ExecutionTrace.IntegerChoiceStep);
Assert.True((trace[4] as ExecutionTrace.IntegerChoiceStep).Value is 5);
}
private void LogTrace(ExecutionTrace trace)

13
Tools/Coyote/Cli/CommandLineParser.cs
Просмотреть файл

@ -321,6 +321,13 @@ namespace Microsoft.Coyote.Cli
var graphOption = new Option<bool>(
name: "--graph",
description: "Output a DOT graph that visualizes the failing execution path if a bug is found.")
{
Arity = ArgumentArity.Zero
};
var dgmlGraphOption = new Option<bool>(
name: "--dgml-graph",
description: "Output a DGML graph that visualizes the failing execution path if a bug is found.")
{
Arity = ArgumentArity.Zero
@ -519,6 +526,7 @@ namespace Microsoft.Coyote.Cli
maxUnfairStepsOption.AddValidator(result => ValidateOptionValueIsUnsignedInteger(result));
maxUnfairStepsOption.AddValidator(result => ValidateExclusiveOptionValueIsAvailable(result, maxStepsOption));
serializeCoverageInfoOption.AddValidator(result => ValidatePrerequisiteOptionValueIsAvailable(result, coverageOption));
graphOption.AddValidator(result => ValidateExclusiveOptionValueIsAvailable(result, dgmlGraphOption));
seedOption.AddValidator(result => ValidateOptionValueIsUnsignedInteger(result));
livenessTemperatureThresholdOption.AddValidator(result => ValidateOptionValueIsUnsignedInteger(result));
timeoutDelayOption.AddValidator(result => ValidateOptionValueIsUnsignedInteger(result));
@ -546,6 +554,7 @@ namespace Microsoft.Coyote.Cli
this.AddOption(command, scheduleCoverageOption);
this.AddOption(command, serializeCoverageInfoOption);
this.AddOption(command, graphOption);
this.AddOption(command, dgmlGraphOption);
this.AddOption(command, xmlLogOption);
this.AddOption(command, reduceSharedStateOption);
this.AddOption(command, seedOption);
@ -993,6 +1002,10 @@ namespace Microsoft.Coyote.Cli
case "graph":
this.Configuration.IsTraceVisualizationEnabled = true;
break;
case "dgml-graph":
this.Configuration.IsTraceVisualizationEnabled = true;
this.Configuration.IsDgmlFormatEnabled = true;
break;
case "xml-trace":
this.Configuration.IsXmlLogEnabled = true;
break;