Skip to content
This repository has been archived by the owner on Aug 26, 2022. It is now read-only.

Commit

Permalink
Exposed new send event APIs that receive an operation group id (#433)
Browse files Browse the repository at this point in the history
  • Loading branch information
@pdeligia
pdeligia committed Jun 4, 2019
1 parent eeb6f2f commit a093861
Show file tree
Hide file tree
Showing 29 changed files with 485 additions and 505 deletions.
2 changes: 1 addition & 1 deletion Common/version.props
View file
@@ -1,7 +1,7 @@
<!-- This file may be overwritten by automation. Only values allowed here are VersionPrefix and VersionSuffix. -->
<Project>
<PropertyGroup>
<VersionPrefix>1.6.0</VersionPrefix>
<VersionPrefix>1.6.1</VersionPrefix>
<VersionSuffix></VersionSuffix>
</PropertyGroup>
</Project>
2 changes: 1 addition & 1 deletion Samples/Framework/build.props
View file
Expand Up @@ -12,6 +12,6 @@
<OutputPath>..\bin\</OutputPath>
</PropertyGroup>
<ItemGroup>
<PackageReference Include="Microsoft.PSharp" Version="1.6.0" />
<PackageReference Include="Microsoft.PSharp" Version="1.6.1" />
</ItemGroup>
</Project>
2 changes: 1 addition & 1 deletion Samples/Language/build.props
View file
Expand Up @@ -10,6 +10,6 @@
<OutputPath>..\bin\</OutputPath>
</PropertyGroup>
<ItemGroup>
<PackageReference Include="Microsoft.PSharp" Version="1.6.0" />
<PackageReference Include="Microsoft.PSharp" Version="1.6.1" />
</ItemGroup>
</Project>
4 changes: 2 additions & 2 deletions Scripts/NuGet/PSharp.nuspec
View file
Expand Up @@ -2,13 +2,13 @@
<package >
<metadata>
<id>Microsoft.PSharp</id>
<version>1.6.0</version>
<version>1.6.1</version>
<authors>Microsoft</authors>
<projectUrl>https://github.com/p-org/PSharp</projectUrl>
<license type="expression">MIT</license>
<requireLicenseAcceptance>false</requireLicenseAcceptance>
<description>P# is a framework for rapid development of reliable asynchronous software.</description>
<releaseNotes>This release contains the 1.6.0 version of the P# framework.</releaseNotes>
<releaseNotes>This release contains the 1.6.1 version of the P# framework.</releaseNotes>
<copyright>© Microsoft Corporation. All rights reserved.</copyright>
<tags>asynchrony reliability specifications reactive state-machines testing</tags>
</metadata>
Expand Down
64 changes: 36 additions & 28 deletions Source/Core/IMachineRuntime.cs
View file
Expand Up @@ -39,7 +39,7 @@ public interface IMachineRuntime : IDisposable
/// </summary>
/// <param name="type">Type of the machine.</param>
/// <param name="machineName">Optional machine name used for logging.</param>
/// <returns>The result is the <see cref="MachineId"/>.</returns>
/// <returns>The result is the machine id.</returns>
MachineId CreateMachineId(Type type, string machineName = null);

/// <summary>
Expand All @@ -50,7 +50,7 @@ public interface IMachineRuntime : IDisposable
/// </summary>
/// <param name="type">Type of the machine.</param>
/// <param name="machineName">Unique name used to create or get the machine id.</param>
/// <returns>The result is the <see cref="MachineId"/>.</returns>
/// <returns>The result is the machine id.</returns>
MachineId CreateMachineIdFromName(Type type, string machineName);

/// <summary>
Expand All @@ -61,8 +61,8 @@ public interface IMachineRuntime : IDisposable
/// <param name="type">Type of the machine.</param>
/// <param name="e">Optional event used during initialization.</param>
/// <param name="operationGroupId">Optional operation group id.</param>
/// <returns>The result is the <see cref="MachineId"/>.</returns>
MachineId CreateMachine(Type type, Event e = null, Guid? operationGroupId = null);
/// <returns>The result is the machine id.</returns>
MachineId CreateMachine(Type type, Event e = null, Guid operationGroupId = default);

/// <summary>
/// Creates a new machine of the specified <see cref="Type"/> and name, and
Expand All @@ -73,8 +73,8 @@ public interface IMachineRuntime : IDisposable
/// <param name="machineName">Optional machine name used for logging.</param>
/// <param name="e">Optional event used during initialization.</param>
/// <param name="operationGroupId">Optional operation group id.</param>
/// <returns>The result is the <see cref="MachineId"/>.</returns>
MachineId CreateMachine(Type type, string machineName, Event e = null, Guid? operationGroupId = null);
/// <returns>The result is the machine id.</returns>
MachineId CreateMachine(Type type, string machineName, Event e = null, Guid operationGroupId = default);

/// <summary>
/// Creates a new machine of the specified type, using the specified <see cref="MachineId"/>.
Expand All @@ -85,8 +85,8 @@ public interface IMachineRuntime : IDisposable
/// <param name="type">Type of the machine.</param>
/// <param name="e">Optional event used during initialization.</param>
/// <param name="operationGroupId">Optional operation group id.</param>
/// <returns>The result is the <see cref="MachineId"/>.</returns>
MachineId CreateMachine(MachineId mid, Type type, Event e = null, Guid? operationGroupId = null);
/// <returns>The result is the machine id.</returns>
MachineId CreateMachine(MachineId mid, Type type, Event e = null, Guid operationGroupId = default);

/// <summary>
/// Creates a new machine of the specified <see cref="Type"/> and with the
Expand All @@ -97,8 +97,8 @@ public interface IMachineRuntime : IDisposable
/// <param name="type">Type of the machine.</param>
/// <param name="e">Optional event used during initialization.</param>
/// <param name="operationGroupId">Optional operation group id.</param>
/// <returns>Task that represents the asynchronous operation. The task result is the <see cref="MachineId"/>.</returns>
Task<MachineId> CreateMachineAndExecuteAsync(Type type, Event e = null, Guid? operationGroupId = null);
/// <returns>Task that represents the asynchronous operation. The task result is the machine id.</returns>
Task<MachineId> CreateMachineAndExecuteAsync(Type type, Event e = null, Guid operationGroupId = default);

/// <summary>
/// Creates a new machine of the specified <see cref="Type"/> and name, and with
Expand All @@ -110,8 +110,8 @@ public interface IMachineRuntime : IDisposable
/// <param name="machineName">Optional machine name used for logging.</param>
/// <param name="e">Optional event used during initialization.</param>
/// <param name="operationGroupId">Optional operation group id.</param>
/// <returns>Task that represents the asynchronous operation. The task result is the <see cref="MachineId"/>.</returns>
Task<MachineId> CreateMachineAndExecuteAsync(Type type, string machineName, Event e = null, Guid? operationGroupId = null);
/// <returns>Task that represents the asynchronous operation. The task result is the machine id.</returns>
Task<MachineId> CreateMachineAndExecuteAsync(Type type, string machineName, Event e = null, Guid operationGroupId = default);

/// <summary>
/// Creates a new machine of the specified <see cref="Type"/>, using the specified
Expand All @@ -124,8 +124,8 @@ public interface IMachineRuntime : IDisposable
/// <param name="type">Type of the machine.</param>
/// <param name="e">Optional event used during initialization.</param>
/// <param name="operationGroupId">Optional operation group id.</param>
/// <returns>Task that represents the asynchronous operation. The task result is the <see cref="MachineId"/>.</returns>
Task<MachineId> CreateMachineAndExecuteAsync(MachineId mid, Type type, Event e = null, Guid? operationGroupId = null);
/// <returns>Task that represents the asynchronous operation. The task result is the machine id.</returns>
Task<MachineId> CreateMachineAndExecuteAsync(MachineId mid, Type type, Event e = null, Guid operationGroupId = default);

/// <summary>
/// Creates a new machine of the specified <see cref="Type"/> and with the
Expand All @@ -136,9 +136,9 @@ public interface IMachineRuntime : IDisposable
/// <param name="type">Type of the machine.</param>
/// <param name="e">Optional event used during initialization.</param>
/// <param name="operationGroupId">Optional operation group id.</param>
/// <returns>Task that represents the asynchronous operation. The task result is the <see cref="MachineId"/>.</returns>
/// <returns>Task that represents the asynchronous operation. The task result is the machine id.</returns>
[Obsolete("Please use IMachineRuntime.CreateMachineAndExecuteAsync(...) instead.")]
Task<MachineId> CreateMachineAndExecute(Type type, Event e = null, Guid? operationGroupId = null);
Task<MachineId> CreateMachineAndExecute(Type type, Event e = null, Guid operationGroupId = default);

/// <summary>
/// Creates a new machine of the specified <see cref="Type"/> and name, and with
Expand All @@ -150,9 +150,9 @@ public interface IMachineRuntime : IDisposable
/// <param name="machineName">Optional machine name used for logging.</param>
/// <param name="e">Optional event used during initialization.</param>
/// <param name="operationGroupId">Optional operation group id.</param>
/// <returns>Task that represents the asynchronous operation. The task result is the <see cref="MachineId"/>.</returns>
/// <returns>Task that represents the asynchronous operation. The task result is the machine id.</returns>
[Obsolete("Please use IMachineRuntime.CreateMachineAndExecuteAsync(...) instead.")]
Task<MachineId> CreateMachineAndExecute(Type type, string machineName, Event e = null, Guid? operationGroupId = null);
Task<MachineId> CreateMachineAndExecute(Type type, string machineName, Event e = null, Guid operationGroupId = default);

/// <summary>
/// Creates a new machine of the specified <see cref="Type"/>, using the specified
Expand All @@ -165,40 +165,43 @@ public interface IMachineRuntime : IDisposable
/// <param name="type">Type of the machine.</param>
/// <param name="e">Optional event used during initialization.</param>
/// <param name="operationGroupId">Optional operation group id.</param>
/// <returns>Task that represents the asynchronous operation. The task result is the <see cref="MachineId"/>.</returns>
/// <returns>Task that represents the asynchronous operation. The task result is the machine id.</returns>
[Obsolete("Please use IMachineRuntime.CreateMachineAndExecuteAsync(...) instead.")]
Task<MachineId> CreateMachineAndExecute(MachineId mid, Type type, Event e = null, Guid? operationGroupId = null);
Task<MachineId> CreateMachineAndExecute(MachineId mid, Type type, Event e = null, Guid operationGroupId = default);

/// <summary>
/// Sends an asynchronous <see cref="Event"/> to a machine.
/// </summary>
/// <param name="target">The id of the target machine.</param>
/// <param name="e">The event to send.</param>
/// <param name="options">Optional parameters of a send operation.</param>
void SendEvent(MachineId target, Event e, SendOptions options = null);
/// <param name="operationGroupId">Optional operation group id.</param>
/// <param name="options">Optional configuration of a send operation.</param>
void SendEvent(MachineId target, Event e, Guid operationGroupId = default, SendOptions options = null);

/// <summary>
/// Sends an <see cref="Event"/> to a machine. Returns immediately if the target machine was already
/// running. Otherwise blocks until the machine handles the event and reaches quiescense again.
/// running. Otherwise blocks until the machine handles the event and reaches quiescense.
/// </summary>
/// <param name="target">The id of the target machine.</param>
/// <param name="e">The event to send.</param>
/// <param name="options">Optional parameters of a send operation.</param>
/// <param name="operationGroupId">Optional operation group id.</param>
/// <param name="options">Optional configuration of a send operation.</param>
/// <returns>Task that represents the asynchronous operation. The task result is true if
/// the event was handled, false if the event was only enqueued.</returns>
Task<bool> SendEventAndExecuteAsync(MachineId target, Event e, SendOptions options = null);
Task<bool> SendEventAndExecuteAsync(MachineId target, Event e, Guid operationGroupId = default, SendOptions options = null);

/// <summary>
/// Sends an <see cref="Event"/> to a machine. Returns immediately if the target machine was already
/// running. Otherwise blocks until the machine handles the event and reaches quiescense again.
/// running. Otherwise blocks until the machine handles the event and reaches quiescense.
/// </summary>
/// <param name="target">The id of the target machine.</param>
/// <param name="e">The event to send.</param>
/// <param name="options">Optional parameters of a send operation.</param>
/// <param name="operationGroupId">Optional operation group id.</param>
/// <param name="options">Optional configuration of a send operation.</param>
/// <returns>Task that represents the asynchronous operation. The task result is true if
/// the event was handled, false if the event was only enqueued.</returns>
[Obsolete("Please use IMachineRuntime.SendEventAndExecuteAsync(...) instead.")]
Task<bool> SendEventAndExecute(MachineId target, Event e, SendOptions options = null);
Task<bool> SendEventAndExecute(MachineId target, Event e, Guid operationGroupId = default, SendOptions options = null);

/// <summary>
/// Registers a new specification monitor of the specified <see cref="Type"/>.
Expand Down Expand Up @@ -313,5 +316,10 @@ public interface IMachineRuntime : IDisposable
/// </summary>
/// <param name="logger">The logger to install.</param>
void SetLogger(ILogger logger);

/// <summary>
/// Terminates the runtime and notifies each active machine to halt execution.
/// </summary>
void Stop();
}
}
5 changes: 3 additions & 2 deletions Source/Core/IO/Logging/DisposingLogger.cs
View file
Expand Up @@ -207,9 +207,10 @@ public void OnWait(MachineId machineId, string currStateName, params Type[] even
/// <param name="senderId">The machine that sent the event, if any.</param>
/// <param name="senderStateName">The name of the current state of the sender machine, if any.</param>
/// <param name="eventName">The event being sent.</param>
/// <param name="operationGroupId">The operation group id, if any.</param>
/// <param name="operationGroupId">The operation group id.</param>
/// <param name="isTargetHalted">Is the target machine halted.</param>
public void OnSend(MachineId targetMachineId, MachineId senderId, string senderStateName, string eventName, Guid? operationGroupId, bool isTargetHalted)
public void OnSend(MachineId targetMachineId, MachineId senderId, string senderStateName, string eventName,
Guid operationGroupId, bool isTargetHalted)
{
}

Expand Down
6 changes: 3 additions & 3 deletions Source/Core/IO/Logging/ILogger.cs
View file
Expand Up @@ -163,10 +163,10 @@ public interface ILogger : IDisposable
/// <param name="senderId">The id of the machine that sent the event, if any.</param>
/// <param name="senderStateName">The name of the current state of the sender machine, if any.</param>
/// <param name="eventName">The event being sent.</param>
/// <param name="operationGroupId">The operation group id, if any.</param>
/// <param name="operationGroupId">The operation group id.</param>
/// <param name="isTargetHalted">Is the target machine halted.</param>
void OnSend(MachineId targetMachineId, MachineId senderId, string senderStateName,
string eventName, Guid? operationGroupId, bool isTargetHalted);
void OnSend(MachineId targetMachineId, MachineId senderId, string senderStateName, string eventName,
Guid operationGroupId, bool isTargetHalted);

/// <summary>
/// Called when a machine has been created.
Expand Down
25 changes: 10 additions & 15 deletions Source/Core/IO/Logging/MachineLogger.cs
View file
Expand Up @@ -379,10 +379,10 @@ public virtual string FormatOnWaitString(MachineId machineId, string currStateNa
/// <param name="senderId">The id of the machine that sent the event, if any.</param>
/// <param name="senderStateName">The name of the current state of the sender machine, if any.</param>
/// <param name="eventName">The event being sent.</param>
/// <param name="operationGroupId">The operation group id, if any.</param>
/// <param name="operationGroupId">The operation group id.</param>
/// <param name="isTargetHalted">Is the target machine halted.</param>
public virtual void OnSend(MachineId targetMachineId, MachineId senderId, string senderStateName,
string eventName, Guid? operationGroupId, bool isTargetHalted)
public virtual void OnSend(MachineId targetMachineId, MachineId senderId, string senderStateName, string eventName,
Guid operationGroupId, bool isTargetHalted)
{
if (this.IsVerbose)
{
Expand All @@ -397,20 +397,15 @@ public virtual string FormatOnWaitString(MachineId machineId, string currStateNa
/// <param name="senderId">The id of the machine that sent the event, if any.</param>
/// <param name="senderStateName">The name of the current state of the sender machine, if any.</param>
/// <param name="eventName">The event being sent.</param>
/// <param name="operationGroupId">The operation group id, if any.</param>
/// <param name="operationGroupId">The operation group id.</param>
/// <param name="isTargetHalted">Is the target machine halted.</param>
public virtual string FormatOnSendString(MachineId targetMachineId, MachineId senderId, string senderStateName, string eventName,
Guid? operationGroupId, bool isTargetHalted)
{
var guid = (operationGroupId.HasValue && operationGroupId.Value != Guid.Empty) ?
operationGroupId.Value.ToString() : "<none>";
var target = isTargetHalted
? $"a halted machine '{targetMachineId}'"
: $"machine '{targetMachineId}'";
var sender = senderId != null
? $"Machine '{senderId}' in state '{senderStateName}'"
: $"The runtime";
return $"<SendLog> Operation Group {guid}: {sender} sent event '{eventName}' to {target}.";
Guid operationGroupId, bool isTargetHalted)
{
var operationGroupIdMsg = operationGroupId != Guid.Empty ? $" (operation group '{operationGroupId}')" : string.Empty;
var target = isTargetHalted ? $"halted machine '{targetMachineId}'" : $"machine '{targetMachineId}'";
var sender = senderId != null ? $"Machine '{senderId}' in state '{senderStateName}'" : $"The runtime";
return $"<SendLog> {sender} sent event '{eventName}' to {target}{operationGroupIdMsg}.";
}

/// <summary>
Expand Down

0 comments on commit a093861

Please sign in to comment.