Usage of Prism

Modelling Language

Concurrent Stochastic Multi-player Games (CSGs)

• For a CSG, each player controls one or more modules and the actions that label commands in a player’s modules must only be used by that player.
• Keyword: CSG
• Specifying each player and the modules of each player: player…endplayer construct

Source Code

Run through CL

• src/prism/PrismCL.java
  • PrismCL
    • go()
    • run()
      • Normal model checking
• src/prism/Prism.java
  • modelCheck()
• src/explicit/StateModelChecker.java
  • createModelChecker()
• src/explicit/CSGModelChecker.java
  • computeProbReachEquilibria()
• src/explicit/CSGModelCheckerEquilibria.java
  • computeRewReachEquilibria()
• src/explicit/StateModelChecker.java
  • check()
  • checkExpression()
  • checkExpressionFilter()
  • checkExpressionLabel()

    Questions

• what is the difference between explicit and prism folder in src?

References

• https://www.prismmodelchecker.org/games/