I tried the implementation on csma.-2-2 model (both JANI and PRISM can be found here: csma.2-2.v1.zip) and it seems it works mostly fine, however, there is one additional label with no name when parsing JANI.

PRISM model output:

Model type: MDP (sparse)
States: 1038
Transitions: 1282
Choices: 1054
Reward Models: none

State Labels: 2 labels

• deadlock -> 0 item(s)
• init -> 1 item(s)

Choice Labels: 8 labels

• send1 -> 12 item(s)
• send2 -> 12 item(s)
• end2 -> 20 item(s)
• cd -> 6 item(s)
• time -> 844 item(s)
• busy2 -> 30 item(s)
• busy1 -> 30 item(s)
• end1 -> 20 item(s)

JANI model output:

Model type: MDP (sparse)
States: 1038
Transitions: 1282
Choices: 1054
Reward Models: none

State Labels: 2 labels

• deadlock -> 0 item(s)
• init -> 1 item(s)

Choice Labels: 9 labels

• send1 -> 12 item(s)
• send2 -> 12 item(s)
• end2 -> 20 item(s)
• cd -> 6 item(s)
• time -> 844 item(s)
• busy2 -> 30 item(s)
• -> 80 item(s)
• busy1 -> 30 item(s)
• end1 -> 20 item(s)

Could you create a smaller file to show where these empty labels come from?

Ok I see what's happening. If there are empty action labels [] in the PRISM file then the corresponding edges in the JANI file don't have any "action" property. While building models from PRISM these are ignored when it comes to choice labeling, but here a new "empty" label is created for these choices. In this zip jani-empty-labels-example.zip there are 2 versions of the same model. In tiny_rewards all actions have labels and therefore this is not a problem, in tiny_rewards2 there is one action with no label leading to this behaviour.

Ok, so the expected solution is that for empty labels, I just dont add a label? :-)

Yes, that should be all.