Home
•
About
»
About PRISM
»
People
»
Sponsors
»
Contact
»
News
»
Screenshots
»
Other tools
»
Links
•
Downloads
»
PRISM
»
Development versions
»
Benchmarks
»
PRISM-games
»
Other downloads
•
Documentation
»
Installation
»
Manual
»
FAQ
»
Tutorial
»
Lectures
•
Manual
•
Publications
»
Selected publications
»
PRISM publications
»
PRISM bibliography
»
External publications
»
Search
•
Case Studies
•
Support
»
Installation FAQ
»
PRISM FAQ
»
Forum (Google)
•
Developers
»
Developer resources
»
Developer forum
•
PRISM-games
»
Download
»
Publications
View
-
Edit
-
Print
-
Search
Main
/
Contents
Introduction
Installing PRISM
Instructions
Common Problems And Questions
The PRISM Language
Introduction
Example 1
Model Type
Modules And Variables
Commands
Parallel Composition
Local Nondeterminism
CTMCs
Example 2
Constants
Expressions
Synchronisation
Module Renaming
Multiple Initial States
Global Variables
Formulas And Labels
Costs And Rewards
Real-time Models
Partially Observable Models
Uncertain Models
Process Algebra Operators
PRISM Model Files
Property Specification
Introduction
Identifying A Set Of States
The P Operator
The S Operator
Reward-based Properties
Multi-objective Properties
Real-time Models
Partially Observable Models
Uncertain Models
Non-probabilistic Properties
Syntax And Semantics
Filters
Properties Files
Running PRISM
Starting PRISM
Loading And Building a Model
Debugging Models With The Simulator
Exporting The Model
Model Checking
Statistical Model Checking
Computing Steady-state And Transient Probabilities
Experiments
Strategies
Support For PEPA Models
Support For SBML
Explicit Model Import
Parametric Model Checking
Configuring PRISM
Introduction
Computation Engines
Solution Methods And Options
Automata Generation
Other Options
References
Appendices
Explicit Model Files
PRISM Manual
Contents
Introduction
Installing PRISM
The PRISM Language
Property Specification
Running PRISM
Configuring PRISM
References
FAQ
Appendices
[
View all
]