Fix for #56 (Explicit -steadystate computation broken for initial BSCCs)

[merkste]

Test whether all initial states are in same BSCC is wrong.

[kleinj]

Thanks. I've opened an issue #56 to document the problem.

We should probably add a test case with the fix as well.

Have not yet looked at your proposed fix.

[kleinj]

To clarify the logic of the tests, it might make sense to rename the BitSet test to BitSet initNotInBSCC or something. The if ((test.cardinality() < numInit) could use some intuitive explanation in the comment as well. Perhaps something like
// not all of the init states are outside the BSCC, so they are spread over at least 2 (B)SCCs and we can abort here

Otherwise, looks good to me.

Could you please do the following:

1. Update the commit from Variable scopes explicit ss #53 (see comment there). Then, we can merge that as part of this PR.
2. Combine the test case commit from kleinj/prism@6aa40ae with your fix commit.
3. Add a 'Fixes: 56' in the commit message of the fix commit.

Then, from my side, we could merge. I'll look into using SCCInfo to avoid the Bitsets later on.

[merkste]

Done. =)

[kleinj]

Looks good to me, now.

[davexparker]

Looks good to me too. Thanks both.