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
• Initial States
• Commands
• Parallel Composition
• Local Nondeterminism
• Module Renaming
• Example 2
• Constants
• Expressions
• Synchronisation
• Process Algebra Operators
• Global Variables
• Formulas And Labels
• PRISM Language Files
• Costs And Rewards

Property Specification

• Introduction
• Identifying A Set Of States
• Basic Syntax
• The P Operator
• The S Operator
• Satisfaction Of Properties
• Determining The Actual Probability
• Properties Files
• Specification Of Reward-based Properties

Running PRISM

• Starting PRISM
• Loading And Building a Model
• Debugging Models With The Simulator
• Exporting The Model
• Model Checking
• Approximate Computation Of Quantitative Properties
• Computing Steady-state And Transient Probabilities
• Experiments
• Support For PEPA Models
• Support For SBML
• Explicit Model Import

Configuring PRISM

• Introduction
• Computation Engines
• Iterative Numerical Methods
• Other Options

References