Bug in Coverage Reporter

[ankushdesai]

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]

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]

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?