Differences in CTMC bisimulation quotient

[volkm]

Applying bisimulation minimization on the CTMC resources/examples/testfiles/ctmc/embedded2.sm yields differently sized quotients, see below.
I can understand that floating point bisimulation can yield different quotient due to precision issues, but I would have expected that using exact arithmetic does not make a difference.

• Encountered when adding a CTMC test case in Add member transition matrix to bisimulation #826
• Could be related to Difference results in MDP bisimulation by using dd engine and sparse engine #91

Original model

Model type: 	CTMC (sparse)
States: 		3478
Transitions: 	14639

Exact without labels

storm --prism embedded2.sm --bisimulation:type strong -bisim -pc -e sparse --exact

On Linux Docker image (stable and ci):

Model type: 	CTMC (sparse)
States: 		180
Transitions: 	1195

On Mac:

Model type: 	CTMC (sparse)
States: 		136
Transitions: 	793

Exact with labels

storm --prism embedded2.sm --bisimulation:type strong -bisim -pc -e sparse --exact --build-all-labels

Same results on both Linux Docker image and Mac:

Model type: 	CTMC (sparse)
States: 		1127
Transitions: 	5730

Double without labels

storm --prism embedded2.sm --bisimulation:type strong -bisim -pc -e sparse

On Linux Docker image (stable and ci):

Model type: 	CTMC (sparse)
States: 	 	1734
Transitions: 	9355

On Mac:

Model type: 	CTMC (sparse)
States: 	 	1318
Transitions: 	7276

Double with labels

storm --prism embedded2.sm --bisimulation:type strong -bisim -pc -e sparse --build-all-labels

On Linux Docker image (stable and ci):

Model type: 	CTMC (sparse)
States: 		1720
Transitions: 	8623

On Mac:

Model type: 	CTMC (sparse)
States: 		1731
Transitions: 	8619

DD

The Dd engine yields an assertion error:

ERROR (QuotientExtractor.cpp:1178): Illegal non-probabilistic matrix.

which is related to #822