PSharp
PSharp copied to clipboard
p-org
A framework for rapid development of reliable asynchronous software.
Specifically, we should detect if the user code is catching ExecutionCacelledException or the ASsertFailure exception.
We should have a callback notification for ignored events. This callback, in conjuction with OnEventHandledAsync, informs the machine of all events that its processing from its inbox.
There is an issue currently (that @shazqadeer faces) where a NuGet dependency is not loaded by the tester, resulting into a `System.IO.FileNotFoundException`. This is related to [this](https://github.com/dotnet/corefx/issues/11639) known issue. We...
The rewriter/compiler (from the high level P# syntax to the C# library version), as well as the language services and static analysis projects in general, are not ported yet to...
The procedures `GetNondeterministicBooleanChoice` and `GetNondeterministicIntegerChoice` do the following: `new Random(DateTime.Now.Millisecond)`. The use of `DateTime.Now.Millisecond` results in loss of randomness when the calls are close together in time, and in general...
We should support clean cancellation of `PSharpTester`. When the user gives a `Ctrl-C` signal to `PSharpTester`, it should abort cleanly, reporting whatever it has gathered so far. This involves two...
We should merge all overloads of `CreateMachine`, `CreateMachineAndExecute` and `RemoteCreateMachine` into a single procedure each that expects all arguments, with appropriate defaults. It makes our life easy with maintaining the...
This is probably a long-term issue. We should add the ability to detect non-determinism in tests, for instance, by noticing when we're unable to repro traces. Even better if we...
Copied from #238 (resolving #234): `PSharpRuntime` has several methods that take `(Type type, ...)`: * the `CreateMachine` variants * `RegisterMonitor` * `InvokeMonitor` This is the only one that also has...
I think there are some bugs in the PCT algorithm. I will send a pull request or more details later.
