PSharp icon indicating copy to clipboard operation
PSharp copied to clipboard
verified publisher icon p-org

Bug in Coverage Reporter

Open ankushdesai opened this issue 6 years ago • 2 comments

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.

ankushdesai avatar Oct 22 '19 04:10 ankushdesai

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.

akashlal avatar Oct 22 '19 04:10 akashlal

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?

ankushdesai avatar Oct 22 '19 05:10 ankushdesai