P# 1.6.0

This release contains the 1.6.0 version of the P# framework.

This is a major release containing new features and performance optimizations, as well as some minor API changes (to give us extra flexibility towards designing the below, but also planned upcoming features).

• Support for MachineTestKit, a new built-in unit-testing API that allows to test machines (and methods of machines) in isolation. You can learn more about this here. Done in #427.
• Improved memory consumption (and reduced GCs) in production and testing by optimizing internal string (and some other types) allocations. In our microbenchmarks, the peak working set of some scenarios is cut by half (not taking into account user code of course). Done in #425.
• Improved messaging latency and throughput, by redesigning and optimizing the internal Machine inbox and its various operations. We are now implementing it internally using an IEventQueue interface that allows us to inject different queues for different scenarios. Done in #426.
• Support for running an async Task test (that uses the Test attribute) with PSharpTester. Done in #430.

Changes:

• The runtime type (returned by PSharpRuntime.Create(…) is now an interface of type IMachineRuntime. This allows us to modify the internal implementation without affecting the user by giving this interface.
• Event has now an optional constructor that takes the Guid operationGroupId (this was used to be passed via the SendOptions optional parameter of the Machine.Send method).
• Default event cannot be manually instantiated anymore, use Default.Event to get a static instance. This improved memory consumption in machines that use the Default event.
• The ILogger interface exposes a few new overloads of Write and WriteLine for reducing boxing and array creations (similar to the string.Format overloads).
• The OnWait method of the ILogger interface has changed from OnWait(MachineId machineId, string currStateName, string eventNames) to OnWait(MachineId machineId, string currStateName, Type eventType) and OnWait(MachineId machineId, string currStateName, params Type[] eventTypes).
• Setting verbosity in the PSharp.Configuration has changed to a boolean IsVerbose property. Similarly, from command line (e.g. using PSharpTester) you have to pass /v instead of /v:N.
• Removed deprecated timer API, which was replaced by a redesigned timer API in 1.5.0.

P# 1.5.1

This release contains the 1.5.1 version of the P# framework.

Changes:

• Fixed a bug with the new Timer API (introduced in 1.5.0).

P# 1.5.0

This release contains the 1.5.0 version of the P# framework.

Changes:

• Redesigned the built-in timer APIs to make them easier to use and more efficient (see documentation here)
• Previous timer APIs are now deprecated and moved under the Microsoft.PSharp.Deprecated.Timers namespace
• The FairRandom API is exposed by the runtime
• Fixed a bug where the SharedObjects library was not included for .NET Core targets
• Removed support for net45

P# 1.4.7

This release contains the 1.4.7 version of the P# framework.

The release fixes a bug where the Microsoft.PSharp.SharedObjects library was not available in the NuGet package for .NET Core, and also exposes the FairRandom() runtime API.

P# 1.4.6

This release contains the 1.4.6 version of the P# framework.

The release updates PSharpTester.exe to return exit codes: 0 for success (no bugs found), 1 for bug(s) found, and 2 for internal error.

P# 1.4.5

This release contains the 1.4.5 version of the P# language, runtime and testing infrastructure.

The release contains bug fixes related to printing the state names for logging and coverage reporting.

P# 1.4.0

This release contains the 1.4.0 version of the P# language, runtime and testing infrastructure.

P# 1.3.9

This release contains the 1.3.9 version of the P# language, runtime and testing infrastructure.

P# 1.3.8

This release contains the 1.3.8 version of the P# language, runtime and testing infrastructure.

P# 1.3.7

This release contains the 1.3.7 version of the P# language, runtime and testing infrastructure.