Correctly group non-consecutive transitions for the same state

src/prism-converter/Tests.hs

@@ -40,6 +40,16 @@ convertToMcrlSpec = describe "convertToMcrl" $ do
     let trans = Mcrl2Transition 0 "0" (V.fromList [Mcrl2PropTrans 0.5 0, Mcrl2PropTrans 0.5 1])
     res ^? transitions . ix 0 `shouldBe` Just trans
 
+  it "groups non-consecutive transitions with same source and label" $ do
+    let mdp = Mdp 2 1 (V.fromList [Transition 0 0 0 0.5 Nothing
+                                  , Transition 0 1 1 1.0 Nothing
+                                  , Transition 0 0 1 0.5 Nothing])
+    let res = convertToMcrl Nothing mdp
+    let trans = [ Mcrl2Transition 0 "0" (V.fromList [Mcrl2PropTrans 0.5 0, Mcrl2PropTrans 0.5 1])
+                , Mcrl2Transition 0 "1" (V.fromList [Mcrl2PropTrans 1.0 1])
+                ]
+    res ^.. transitions . each `shouldBe` trans
+
   it "generates two two distinct transitions for two transitions with different label" $ do
     let mdp = Mdp 2 2 (V.fromList [Transition 0 0 1 1.0 Nothing, Transition 0 1 1 1.0 Nothing])
     let res = convertToMcrl Nothing mdp

src/prism-converter/lib/Mdp/Mcrl2.hs

@@ -96,7 +96,7 @@ convertTransitionsToMcrl trans = mkMcrl2Tans <$> partitionVector (view source &&
   where
     sorted = V.create $ do
       v <- V.thaw trans -- TODO Maybe use unsafe thaw
-      V.sortBy (comparing $ view source) v
+      V.sortBy (comparing $ view source &&& view choice) v
       return v