New tests - about 40 of them - added to:
Core.Tests.Features
Core.Tests.Machines
The tests are mostly borrowed from the P regression suite and check the following P# features:
send/receive
goto transitions
push/pop
defer/ignore
halt events
There are a few issues with the tests not passing; for now, those tests are disabled, but they have to be analyzed to determine if the test is wrong, or if there's a bug. The tests are marked in the code with the comment line starting with:
// TODO:
These issues affect the following files:
\PSharp\Tests\Core.Tests\Features\GotoTests.cs
\PSharp\Tests\Core.Tests\Features\PushTests.cs
\PSharp\Tests\Core.Tests\Machines\ReceiveEventTest-Ellab.cs
New tests - about 40 of them - added to: Core.Tests.Features Core.Tests.Machines
The tests are mostly borrowed from the P regression suite and check the following P# features:
There are a few issues with the tests not passing; for now, those tests are disabled, but they have to be analyzed to determine if the test is wrong, or if there's a bug. The tests are marked in the code with the comment line starting with: // TODO: These issues affect the following files: \PSharp\Tests\Core.Tests\Features\GotoTests.cs \PSharp\Tests\Core.Tests\Features\PushTests.cs \PSharp\Tests\Core.Tests\Machines\ReceiveEventTest-Ellab.cs