[
Top
]
[
Contents
]
[
Index
]
[
?
]
Table of Contents
Introduction
1. The Net Description Language
1.1 Design Criteria
1.2 Lexical Conventions
1.2.1 Formatting
1.2.2 Comments
1.2.3 Lexical Tokens
1.2.3.1 Reserved Words
1.2.3.2 Numeric Constants
1.2.3.3 Character Constants
1.2.3.4 Identifiers
1.2.4 Preprocessor Directives
1.2.4.1 Embedding Other Files: ‘
#include
’
1.2.4.2 Conditional Processing
1.2.4.3 Setting the Line Number: ‘
#line
’
1.2.4.4 Preprocessor Comment: ‘
#!
’
1.3 Constructs for Defining Nets
1.3.1 Type Definitions: ‘
typedef
’
1.3.2 Function Definitions
1.3.3 Place Definition: ‘
place
’
1.3.4 Transition Definition: ‘
trans
’
1.3.5 Defining Subnets for Modular State Space Exploration
1.3.6 On-the-Fly Verification
1.3.6.1 Verifying Safety Properties
1.3.6.2 Defining Fairness Constraints
1.3.6.3 Specifying State Propositions for LSTS Output
1.4 Data Types
1.4.1 Background
1.4.2 Leaf Types
1.4.2.1 Integer Types
1.4.2.2 Boolean Type
1.4.2.3 Character Type
1.4.2.4 Enumerated Type
1.4.2.5 Identifier Type
1.4.3 Composite Types
1.4.3.1 Structure
1.4.3.2 Union
1.4.3.3 Array
1.4.3.4 Buffer (Queue or Stack)
1.4.4 Constraints
1.5 Expressions and Formulae
1.5.1 Literals
1.5.1.1 Constants
1.5.1.2 Variables
1.5.1.3 Dynamic Errors
1.5.2 Operators
1.5.2.1 Integer Arithmetic
1.5.2.2 Successor and Predecessor
1.5.2.3 Comparison
1.5.2.4 Boolean Logic
1.5.2.5 Selection
1.5.2.6 Type Casting
1.5.2.7 Atomicity
1.5.3 Structures
1.5.4 Unions
1.5.5 Arrays
1.5.6 Buffers
1.6 Operations on Multi-Sets
1.7 Temporal Logic
1.8 Non-Determinism in Transitions
1.9 Scoping of Identifiers
2. Reachability Analysis with Maria
2.1 Invoking Maria
2.1.1 Interrupting the Reachability Analysis
2.1.2 Options
2.1.3 Option Cross Key
2.2 The Maria Shell
2.2.1 The Line Editor
2.2.1.1 Name Completion
2.2.2 The Query Language
2.2.2.1 Loading a Model
2.2.2.2 Displaying a Model
2.2.2.3 Unfolding a Model
2.2.2.4 Exporting a Labelled State Transition System
2.2.2.5 Exporting the Reachability Graph
2.2.2.6 Exhaustive Analysis
2.2.2.7 Evaluating Expressions and Formulae
2.2.2.8 Displaying Markings
2.2.2.9 Excluding Places from Displayed Markings
2.2.2.10 Selecting the Active Subnet
2.2.2.11 Listing Successor Nodes
2.2.2.12 Listing Predecessor Nodes
2.2.2.13 Moving in the Graph
2.2.2.14 Anonymous Transitions
2.2.2.15 Defining Functions
2.2.2.16 Strongly Connected Components
2.2.2.17 Shortest Paths
2.2.2.18 Miscellanous Commands
2.2.2.19 Exiting
2.2.3 Some Quirks with the Query Language
2.2.3.1 Separating Statements
2.2.3.2 Conditional Processing in the Editor
2.2.4 Visualizing Graphs and Paths
2.2.4.1 GraphViz, the Graph Visualizer
2.2.4.2 Known Bugs in the Visualizer
2.3 Editing Petri Nets with GNU Emacs
2.3.1 Installing the Petri Net mode
2.3.2 Syntax Highlighting
2.3.3 Customizing Emacs
3. Algorithms used in Maria
3.1 The Unification Algorithm
3.1.1 Concepts
3.1.2 Expanding Quantifications
3.1.3 Matching Concrete and Formal Tokens
3.1.4 Finding Assignment Candidates
3.1.5 Transition Instance Analysis
3.2 Model Checking Algorithms
3.2.1 Checking Safety Properties
3.2.2 Checking Liveness Properties
A. The Grammar
A.1 Terminal Symbols
A.2 The Net Description Language
A.2.1 Type
A.2.1.1 Constraint
A.2.2 Function
A.2.3 Place
A.2.4 Transition
A.2.5 State Properties
A.3 The Query Language
A.4 Formulae and Expressions
A.4.1 Literals
A.4.2 Functions
A.4.3 Basic Formulae
A.4.4 Typecasting and Union Values
A.4.5 Non-Determinism and Quantification
A.4.6 Multi-Set Operations
A.4.7 Temporal Logic
B. The Graph Files
C. Compiling Maria
C.1 System Requirements
C.2 Editing the ‘
Makefile
’ files
C.3 Installing Maria
C.4 Compiling Maria for Debugging
C.5 Reporting Bugs
D. Examples
D.1 Dining Philosophers (‘
dining.pn
’)
D.2 Distributed Database Management (‘
dbm.pn
’)
GNU GENERAL PUBLIC LICENSE
Preamble
How to Apply These Terms to Your New Programs
Index
[
Top
]
[
Contents
]
[
Index
]
[
?
]
This document was generated by
root
on
November 22, 2009
using
texi2html 1.82
.