search

p-org / PSharp

A framework for rapid development of reliable asynchronous software.
MIT License
390 stars 37 forks source link

Bug in Coverage Reporter #471

Open ankushdesai opened 4 years ago

ankushdesai commented 4 years ago

I think there is a bug in the coverage reporter, it is not taking into account the "default" transitions.

I am 100% sure that the default transition is triggered during testing but the coverage reporter says: Events not covered: Microsoft.PSharp.Default

Can you please take a look and confirm that this is bug in the current implementation.

akashlal commented 4 years ago

Hey Ankush, can you send a short P# program with the bug? I don't understand what exactly is the bug that you're referring to.

ankushdesai commented 4 years ago

Sorry, for the incomplete information.

I have a P program with following state: state X { entry { } on null goto X; } on running PSharpTester with coverage enabled. The coverage report always says:

Machine: Y Machine event coverage: 50.0% State: InitState State event coverage: 100.0% Next states: Init_7

State: X State event coverage: 0.0% Events not covered: Microsoft.PSharp.Default Previous states: Init_7

I am very sure that the null transition which is the default transition in PSharp is triggered. But its not covered in the coverage report and shows 0.0%.

Does this help?