I think I can do that with having an action for each player that passes if they don't have any money. The tricky bit is implementing the ante logic to only add n-1 coins to the pot, but I have an idea on how to hardcode that. After that it's "just" a matter of generating it all with another program.
This is also what I did when I used PRISM for my thesis. Honestly also not the greatest experience, but I think it does show that the limitations of the PRISM language are not inherent to the problem domain.
