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

cleanup

This commit is contained in:
Pantazis Deligiannis 2022-01-20 17:34:10 -08:00
Родитель b213da4867
Коммит 5d60fc11ec
7 изменённых файлов: 46 добавлений и 67 удалений
Показать статистику Скачать Patch файл Скачать Diff файл Показать все файлы Свернуть все файлы

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

@ -810,7 +810,7 @@ namespace Microsoft.Coyote.Runtime
if (this.Configuration.IsProgramStateHashingEnabled)
{
// Update the current operation with the hashed program state.
current.HashedProgramState = this.GetHashedProgramState();
current.HashedProgramState = this.GetHashedProgramState(current);
}
// Choose the next operation to schedule, if there is one enabled.
@ -971,7 +971,7 @@ namespace Microsoft.Coyote.Runtime
if (this.Configuration.IsProgramStateHashingEnabled)
{
// Update the current operation with the hashed program state.
this.ScheduledOperation.HashedProgramState = this.GetHashedProgramState();
this.ScheduledOperation.HashedProgramState = this.GetHashedProgramState(this.ScheduledOperation);
}
if (!this.Scheduler.GetNextBooleanChoice(this.ScheduledOperation, maxValue, out bool choice))
@ -1009,7 +1009,7 @@ namespace Microsoft.Coyote.Runtime
if (this.Configuration.IsProgramStateHashingEnabled)
{
// Update the current operation with the hashed program state.
this.ScheduledOperation.HashedProgramState = this.GetHashedProgramState();
this.ScheduledOperation.HashedProgramState = this.GetHashedProgramState(this.ScheduledOperation);
}
if (!this.Scheduler.GetNextIntegerChoice(this.ScheduledOperation, maxValue, out int choice))
@ -1032,9 +1032,15 @@ namespace Microsoft.Coyote.Runtime
// Checks if the scheduling steps bound has been reached.
this.CheckIfSchedulingStepsBoundIsReached();
if (this.Configuration.IsProgramStateHashingEnabled)
{
// Update the operation with the hashed program state.
op.HashedProgramState = this.GetHashedProgramState(op);
}
// Choose the next delay to inject.
int maxDelay = maxValue > 0 ? (int)this.Configuration.TimeoutDelay : 1;
if (!this.Scheduler.GetNextDelay(this.OperationMap.Values, op, maxDelay, out int next))
if (!this.Scheduler.GetNextDelay(op, maxDelay, out int next))
{
this.Detach(SchedulerDetachmentReason.BoundReached);
}
@ -1278,27 +1284,43 @@ namespace Microsoft.Coyote.Runtime
/// The hash is updated in each execution step.
/// </remarks>
[DebuggerStepThrough]
private int GetHashedProgramState()
private int GetHashedProgramState(AsyncOperation current)
{
unchecked
{
int hash = 19;
foreach (var operation in this.GetRegisteredOperations().OrderBy(op => op.Id))
if (this.SchedulingPolicy is SchedulingPolicy.Systematic)
{
if (operation is ActorOperation actorOperation)
foreach (var operation in this.GetRegisteredOperations().OrderBy(op => op.Id))
{
int operationHash = 31 + actorOperation.Actor.GetHashedState();
operationHash = (operationHash * 31) + actorOperation.Type.GetHashCode();
hash *= operationHash;
if (operation is ActorOperation actorOperation)
{
int operationHash = 31 + actorOperation.Actor.GetHashedState();
operationHash = (operationHash * 31) + actorOperation.Type.GetHashCode();
hash *= operationHash;
}
else if (operation is TaskOperation taskOperation)
{
hash *= 31 + taskOperation.Type.GetHashCode();
}
}
else if (operation is TaskOperation taskOperation)
hash = (hash * 31) + this.SpecificationEngine.GetHashedMonitorState();
}
else if (this.SchedulingPolicy is SchedulingPolicy.Fuzzing)
{
// Add the hash of the current operation.
hash = (hash * 31) + current.Name.GetHashCode();
// Add the hash of the status of each operation.
foreach (var operation in this.GetRegisteredOperations().OrderBy(op => op.Name))
{
hash *= 31 + taskOperation.Type.GetHashCode();
Console.WriteLine($" |---> {operation.Name}: status: {operation.Status}");
hash *= 31 + operation.Status.GetHashCode();
}
}
hash = (hash * 31) + this.SpecificationEngine.GetHashedMonitorState();
return hash;
}
}

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

@ -164,13 +164,12 @@ namespace Microsoft.Coyote.Runtime
/// <summary>
/// Returns the next delay.
/// </summary>
/// <param name="ops">Operations executing during the current test iteration.</param>
/// <param name="current">The operation requesting the delay.</param>
/// <param name="maxValue">The max value.</param>
/// <param name="next">The next delay.</param>
/// <returns>True if there is a next delay, else false.</returns>
internal bool GetNextDelay(IEnumerable<AsyncOperation> ops, AsyncOperation current, int maxValue, out int next) =>
(this.Strategy as FuzzingStrategy).GetNextDelay(ops, current, maxValue, out next);
internal bool GetNextDelay(AsyncOperation current, int maxValue, out int next) =>
(this.Strategy as FuzzingStrategy).GetNextDelay(current, maxValue, out next);
/// <summary>
/// Returns a description of the scheduling strategy in text format.

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

@ -3,7 +3,6 @@
using System;
using System.Collections.Concurrent;
using System.Collections.Generic;
using Microsoft.Coyote.Runtime;
namespace Microsoft.Coyote.Testing.Fuzzing
@ -56,8 +55,7 @@ namespace Microsoft.Coyote.Testing.Fuzzing
/// The delay has an injection probability of 0.05 and is in the range of [10, maxValue * 10]
/// with an increment of 10 and an upper bound of 5000ms per operation.
/// </remarks>
internal override bool GetNextDelay(IEnumerable<AsyncOperation> ops, AsyncOperation current,
int maxValue, out int next)
internal override bool GetNextDelay(AsyncOperation current, int maxValue, out int next)
{
Guid id = this.GetOperationId();

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

@ -3,7 +3,6 @@
using System;
using System.Collections.Concurrent;
using System.Collections.Generic;
using System.Threading;
using System.Threading.Tasks;
using Microsoft.Coyote.Runtime;
@ -53,13 +52,11 @@ namespace Microsoft.Coyote.Testing.Fuzzing
/// <summary>
/// Returns the next delay.
/// </summary>
/// <param name="ops">Operations executing during the current test iteration.</param>
/// <param name="current">The operation requesting the delay.</param>
/// <param name="maxValue">The max value.</param>
/// <param name="next">The next delay.</param>
/// <returns>True if there is a next delay, else false.</returns>
internal abstract bool GetNextDelay(IEnumerable<AsyncOperation> ops, AsyncOperation current,
int maxValue, out int next);
internal abstract bool GetNextDelay(AsyncOperation current, int maxValue, out int next);
/// <summary>
/// Returns the current operation id.

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

@ -77,8 +77,7 @@ namespace Microsoft.Coyote.Testing.Fuzzing
}
/// <inheritdoc/>
internal override bool GetNextDelay(IEnumerable<AsyncOperation> ops, AsyncOperation current,
int maxValue, out int next)
internal override bool GetNextDelay(AsyncOperation current, int maxValue, out int next)
{
Guid id = this.GetOperationId();

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

@ -2,7 +2,6 @@
// Licensed under the MIT License.
using System;
using System.Collections.Concurrent;
using System.Collections.Generic;
using System.Linq;
using Microsoft.Coyote.Runtime;
@ -68,10 +67,9 @@ namespace Microsoft.Coyote.Testing.Fuzzing
}
/// <inheritdoc/>
internal override bool GetNextDelay(IEnumerable<AsyncOperation> ops, AsyncOperation current,
int maxValue, out int next)
internal override bool GetNextDelay(AsyncOperation current, int maxValue, out int next)
{
int state = this.CaptureExecutionStep(ops, current);
int state = this.CaptureExecutionStep(current);
this.InitializeDelayQValues(state, maxValue);
next = this.GetNextDelayByPolicy(state, maxValue);
@ -154,48 +152,16 @@ namespace Microsoft.Coyote.Testing.Fuzzing
/// Captures metadata related to the current execution step, and returns
/// a value representing the current program state.
/// </summary>
private int CaptureExecutionStep(IEnumerable<AsyncOperation> ops, AsyncOperation operation)
private int CaptureExecutionStep(AsyncOperation current)
{
int state = ComputeStateHash(operation);
Console.WriteLine($">---> {operation.Name}: state: {state}");
foreach (var op in ops)
{
Console.WriteLine($" |---> {op.Name}: status: {op.Status}");
}
int state = current.HashedProgramState;
Console.WriteLine($">---> {current.Name}: state: {state}");
// Update the list of chosen delays with the current state.
this.ExecutionPath.AddLast((this.PreviousDelay, state));
return state;
}
/// <summary>
/// Computes a hash representing the current program state.
/// </summary>
private static int ComputeStateHash(AsyncOperation operation)
{
unchecked
{
int hash = 19;
// Add the hash of the current operation.
hash = (hash * 31) + operation.Name.GetHashCode();
// foreach (var kvp in this.OperationStatusMap)
// {
// // Console.WriteLine($">>>>>>> Hashing: id {kvp.Key} - status {kvp.Value}");
// // int operationHash = 31 + kvp.Key.GetHashCode();
// // removing inactive actors from statehash
// // operationHash = !(kvp.Value is ActorStatus.Inactive) ? (operationHash * 31) + kvp.Value.GetHashCode() : operationHash;
// // including inactive actors in statehash
// // operationHash = (operationHash * 31) + kvp.Value.GetHashCode();
// // hash *= operationHash;
// }
return hash;
}
}
/// <summary>
/// Initializes the Q values of all delays that can be chosen at the specified state
/// that have not been previously encountered.

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

@ -1,7 +1,6 @@
// Copyright (c) Microsoft Corporation.
// Licensed under the MIT License.
using System.Collections.Generic;
using Microsoft.Coyote.Runtime;
namespace Microsoft.Coyote.Testing.Fuzzing
@ -43,8 +42,7 @@ namespace Microsoft.Coyote.Testing.Fuzzing
}
/// <inheritdoc/>
internal override bool GetNextDelay(IEnumerable<AsyncOperation> ops, AsyncOperation current,
int maxValue, out int next)
internal override bool GetNextDelay(AsyncOperation current, int maxValue, out int next)
{
next = this.RandomValueGenerator.Next(maxValue);
this.StepCount++;