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

delay steps

This commit is contained in:
Pantazis Deligiannis 2022-01-21 14:22:36 -08:00
Родитель 2f68a18647
Коммит 4bc65b4ba6
2 изменённых файлов: 71 добавлений и 28 удалений
Показать статистику Скачать Patch файл Скачать Diff файл Показать все файлы Свернуть все файлы

83
Source/Core/Testing/Fuzzing/QLearningStrategy.cs
Просмотреть файл

@ -18,17 +18,25 @@ namespace Microsoft.Coyote.Testing.Fuzzing
/// </summary>
private readonly Dictionary<int, Dictionary<int, double>> OperationQTable;
/// <summary>
/// The path that is being executed during the current iteration. Each
/// step of the execution is represented by a delay value and a value
/// representing the program state after the delay happened.
/// </summary>
private readonly LinkedList<(int delay, int state)> ExecutionPath;
private readonly HashSet<int> UniqueStates;
/// <summary>
/// The previously chosen delay.
/// The path that is being executed during the current iteration. Each step
/// of the execution is represented by an operation requesting a delay, the
/// chosen delay value and a value representing the program state after the
/// delay happened.
/// </summary>
private int PreviousDelay;
private readonly LinkedList<(string op, int delay, int state)> ExecutionPath;
/// <summary>
/// Map from operations to number of steps they are currently delayed.
/// </summary>
private readonly Dictionary<string, ulong> DelayedOperationSteps;
/// <summary>
/// The last delayed operation.
/// </summary>
private (string op, int delay) LastDelayedOperation;
/// <summary>
/// The value of the learning rate.
@ -58,8 +66,10 @@ namespace Microsoft.Coyote.Testing.Fuzzing
: base(maxSteps, random)
{
this.OperationQTable = new Dictionary<int, Dictionary<int, double>>();
this.ExecutionPath = new LinkedList<(int, int)>();
this.PreviousDelay = 0;
this.UniqueStates = new HashSet<int>();
this.ExecutionPath = new LinkedList<(string, int, int)>();
this.DelayedOperationSteps = new Dictionary<string, ulong>();
this.LastDelayedOperation = ("Task(0)", 0);
this.LearningRate = 0.3;
this.Gamma = 0.7;
this.BasicActionReward = -1;
@ -74,7 +84,7 @@ namespace Microsoft.Coyote.Testing.Fuzzing
this.InitializeDelayQValues(state, maxValue);
next = this.GetNextDelayByPolicy(state);
this.PreviousDelay = next;
this.LastDelayedOperation = (current.Name, next);
this.StepCount++;
return true;
@ -158,32 +168,63 @@ namespace Microsoft.Coyote.Testing.Fuzzing
/// </summary>
private int CaptureExecutionStep(IEnumerable<AsyncOperation> ops, AsyncOperation current)
{
int state = ComputeProgramState(ops, current);
this.UpdateDelayedOperationSteps(ops);
int state = this.ComputeProgramState(ops, current);
Console.WriteLine($">---> {current.Name}: state: {state}");
// Update the list of chosen delays with the current state.
this.ExecutionPath.AddLast((this.PreviousDelay, state));
// Update the execution path with the current state.
this.ExecutionPath.AddLast((this.LastDelayedOperation.op, this.LastDelayedOperation.delay, state));
return state;
}
/// <summary>
/// Computes the number of steps that each operation has been delayed.
/// </summary>
private void UpdateDelayedOperationSteps(IEnumerable<AsyncOperation> ops)
{
foreach (var op in ops.OrderBy(op => op.Name))
{
if (!this.DelayedOperationSteps.ContainsKey(op.Name))
{
this.DelayedOperationSteps.Add(op.Name, 0);
}
if (op.Status is AsyncOperationStatus.Delayed)
{
this.DelayedOperationSteps[op.Name]++;
}
else
{
this.DelayedOperationSteps[op.Name] = 0;
}
Console.WriteLine($" |---> {op.Name}: delayed: {this.DelayedOperationSteps[op.Name]}");
}
}
/// <summary>
/// Computes the current program state.
/// </summary>
private static int ComputeProgramState(IEnumerable<AsyncOperation> ops, AsyncOperation current)
private int ComputeProgramState(IEnumerable<AsyncOperation> ops, AsyncOperation current)
{
unchecked
{
int hash = 19;
// Add the hash of the current operation.
var pre = hash;
hash = (hash * 31) + current.Name.GetHashCode();
hash = pre;
// Add the hash of the status of each operation.
// Add the hash of each operation.
foreach (var op in ops.OrderBy(op => op.Name))
{
Console.WriteLine($" |---> {op.Name}: status: {op.Status}");
hash *= 31 + op.GetHashedState(SchedulingPolicy.Fuzzing);
int operationHash = 31 + op.GetHashedState(SchedulingPolicy.Fuzzing);
this.UniqueStates.Add(op.GetHashedState(SchedulingPolicy.Fuzzing));
operationHash = (operationHash * 31) + this.DelayedOperationSteps[op.Name].GetHashCode();
hash *= operationHash;
}
return hash;
@ -216,7 +257,8 @@ namespace Microsoft.Coyote.Testing.Fuzzing
{
this.LearnQValues();
this.ExecutionPath.Clear();
this.PreviousDelay = 0;
this.DelayedOperationSteps.Clear();
this.LastDelayedOperation = ("Task(0)", 0);
this.Epochs++;
return base.InitializeNextIteration(iteration);
@ -235,8 +277,8 @@ namespace Microsoft.Coyote.Testing.Fuzzing
{
// pathBuilder.Append($"({node.Value.delay},{node.Value.state}), ");
var (_, state) = node.Value;
var (nextDelay, nextState) = node.Next.Value;
var (_, _, state) = node.Value;
var (nextOp, nextDelay, nextState) = node.Next.Value;
// Compute the max Q value.
double maxQ = double.MinValue;
@ -273,6 +315,7 @@ namespace Microsoft.Coyote.Testing.Fuzzing
}
Console.WriteLine($"Visited {this.OperationQTable.Count} states.");
Console.WriteLine($"Found {this.UniqueStates.Count} unique custom states.");
// Console.WriteLine(pathBuilder.ToString());
}

16
Source/Core/Testing/Systematic/QLearningStrategy.cs
Просмотреть файл

@ -32,9 +32,9 @@ namespace Microsoft.Coyote.Testing.Systematic
private readonly Dictionary<int, ulong> TransitionFrequencies;
/// <summary>
/// The previously chosen operation.
/// The last chosen operation.
/// </summary>
private ulong PreviousOperation;
private ulong LastOperation;
/// <summary>
/// The value of the learning rate.
@ -86,7 +86,7 @@ namespace Microsoft.Coyote.Testing.Systematic
this.OperationQTable = new Dictionary<int, Dictionary<ulong, double>>();
this.ExecutionPath = new LinkedList<(ulong, AsyncOperationType, int)>();
this.TransitionFrequencies = new Dictionary<int, ulong>();
this.PreviousOperation = 0;
this.LastOperation = 0;
this.LearningRate = 0.3;
this.Gamma = 0.7;
this.TrueChoiceOpValue = ulong.MaxValue;
@ -112,7 +112,7 @@ namespace Microsoft.Coyote.Testing.Systematic
this.InitializeOperationQValues(state, ops);
next = this.GetNextOperationByPolicy(state, ops);
this.PreviousOperation = next.Id;
this.LastOperation = next.Id;
this.StepCount++;
return true;
@ -126,7 +126,7 @@ namespace Microsoft.Coyote.Testing.Systematic
next = this.GetNextBooleanChoiceByPolicy(state);
this.PreviousOperation = next ? this.TrueChoiceOpValue : this.FalseChoiceOpValue;
this.LastOperation = next ? this.TrueChoiceOpValue : this.FalseChoiceOpValue;
this.StepCount++;
return true;
}
@ -139,7 +139,7 @@ namespace Microsoft.Coyote.Testing.Systematic
next = this.GetNextIntegerChoiceByPolicy(state, maxValue);
this.PreviousOperation = this.MinIntegerChoiceOpValue - (ulong)next;
this.LastOperation = this.MinIntegerChoiceOpValue - (ulong)next;
this.StepCount++;
return true;
}
@ -263,7 +263,7 @@ namespace Microsoft.Coyote.Testing.Systematic
int state = current.HashedProgramState;
// Update the execution path with the current state.
this.ExecutionPath.AddLast((this.PreviousOperation, current.Type, state));
this.ExecutionPath.AddLast((this.LastOperation, current.Type, state));
if (!this.TransitionFrequencies.ContainsKey(state))
{
@ -348,7 +348,7 @@ namespace Microsoft.Coyote.Testing.Systematic
{
this.LearnQValues();
this.ExecutionPath.Clear();
this.PreviousOperation = 0;
this.LastOperation = 0;
this.Epochs++;
return base.InitializeNextIteration(iteration);