There are also many examples available in the case studies section.
To get started, you can look at some examples in the prism-examples directory within the PRISM-games distribution. Corresponding properties files are in the same directory.
Instructions for key features specific to PRISM-games can be found below.
PRISM-games supports strategy synthesis for all property types. The fuctionality can be accessed using the "Strategies" menu when right-clicking a property in the "Properties" tab:
Once generated, a strategy can be viewed interactively in the simulator tab. Strategy information is displayed in the "Strategy information" panel (top, right). The simulator choice table column named "Strategy choice" displays what the optimal strategy would do. The notation used is "choice id -> probability", e.g., in the example from the screenshot below, the strategy would choose the action indexed 1 with probability 1.0, hence "1->1.0" is displayed.
Other properties can also be verified