Enable model checking of nondeterministic models under an arbitrary scheduler

[tquatmann]

Checking nondeterministic models under an arbitrary scheduler allows us to use the (faster) algorithms for DTMCs/CTMCs. This might be useful, e.g., when the nondeterminism is known to be spurious.

In some sense, this would be the reverse operation of --transformation:to-nondet. Note that for MAs it might be necessary to also invoke --[transformation:]eliminate-chains to get a CTMC (this should probably be invoked automatically). Special care has to be taken regarding labels and rewards on non-Markovion states, though.

Further note that there are multiple ways to pick an arbitrary scheduler. For simplicity, we could just take the first action of each state. We also have to be careful with terminology (picking a scheduler at random is not the same as having a scheduler that makes choices at random).