The following example model and properties files can be used to test PRISM-games's functionality for rPATL model checking and strategy synthesis.
The example files are also available in the examples directory included with downloads of PRISM-games
A selection of larger benchmark examples can be found on this page. These include:
See also the PRISM-games publications list for papers describing various case studies that illustrate the application of PRISM-games.