| Index Entry | Section |
|
A | | |
| assertions | 1.3.6.1 Verifying Safety Properties |
| assertions | 1.5.1.3 Dynamic Errors |
| assignments | 3.1.3 Matching Concrete and Formal Tokens |
| assignments | 3.1.4 Finding Assignment Candidates |
|
B | | |
| buffers | 1.5.6 Buffers |
| bugs, reporting | C.5 Reporting Bugs |
|
C | | |
| capacity constraint | 1.3.3 Place Definition: ‘place’ |
| catching dynamic errors | 1.5.1.3 Dynamic Errors |
| character constants | 1.2.3.3 Character Constants |
| command line interface | 2.2.1 The Line Editor |
| command line options, ‘maria’ | 2.1 Invoking Maria |
| compiling | C. Compiling Maria |
| completion of names | 2.2.1.1 Name Completion |
| concepts, unification | 3.1.1 Concepts |
| conditional processing | 1.2.4.2 Conditional Processing |
| conditional processing, interactively | 2.2.3.2 Conditional Processing in the Editor |
| constants | 1.5.1.1 Constants |
| constants, character | 1.2.3.3 Character Constants |
| constants, numeric | 1.2.3.2 Numeric Constants |
|
D | | |
| data types | 1.4 Data Types |
| data types, array | 1.4.3.3 Array |
| data types, boolean | 1.4.2.2 Boolean Type |
| data types, buffer | 1.4.3.4 Buffer (Queue or Stack) |
| data types, character | 1.4.2.3 Character Type |
| data types, conversions | 1.5.2.6 Type Casting |
| data types, defining | 1.3.1 Type Definitions: ‘typedef’ |
| data types, enumerated | 1.4.2.4 Enumerated Type |
| data types, identifier | 1.4.2.5 Identifier Type |
| data types, integer | 1.4.2.1 Integer Types |
| data types, limiting with constraints | 1.4.4 Constraints |
| data types, structure | 1.4.3.1 Structure |
| data types, union | 1.4.3.2 Union |
| debugging ‘maria’ | C.4 Compiling Maria for Debugging |
| dining philosophers (example) | D.1 Dining Philosophers (‘dining.pn’) |
| distributed database management (example) | D.2 Distributed Database Management (‘dbm.pn’) |
|
E | | |
| Emacs | 2.3 Editing Petri Nets with GNU Emacs |
| Emacs, customizing | 2.3.3 Customizing Emacs |
| expressions, arithmetic | 1.5.2.1 Integer Arithmetic |
| expressions, arrays | 1.5.5 Arrays |
| expressions, atomicity | 1.5.2.7 Atomicity |
| expressions, comparison | 1.5.2.3 Comparison |
| expressions, evaluating | 2.2.2.7 Evaluating Expressions and Formulae |
| expressions, logic | 1.5.2.4 Boolean Logic |
| expressions, multi-set valued | 1.6 Operations on Multi-Sets |
| expressions, overview | 1.5 Expressions and Formulae |
| expressions, predecessor | 1.5.2.2 Successor and Predecessor |
| expressions, prohibiting transformations | 1.5.2.7 Atomicity |
| expressions, selection | 1.5.2.5 Selection |
| expressions, short-circuit evaluation | 1.5.2.4 Boolean Logic |
| expressions, structures | 1.5.3 Structures |
| expressions, successor | 1.5.2.2 Successor and Predecessor |
| expressions, temporal | 1.7 Temporal Logic |
| expressions, unions | 1.5.4 Unions |
|
F | | |
| fairness sets | 1.3.4 Transition Definition: ‘trans’ |
| fairness sets | 1.3.6.2 Defining Fairness Constraints |
| FIFO buffers | 1.5.6 Buffers |
| functions, defining | 1.3.2 Function Definitions |
| functions, defining | 2.2.2.15 Defining Functions |
|
G | | |
| grammar, summary | A. The Grammar |
| GraphViz | 2.2.4.1 GraphViz, the Graph Visualizer |
|
I | | |
| identifiers, syntax of | 1.2.3.4 Identifiers |
| if-then-else, generalized | 1.5.2.5 Selection |
| include files | 1.2.4.1 Embedding Other Files: ‘#include’ |
| indentation | 2.3.1 Installing the Petri Net mode |
| initial marking | 1.3.3 Place Definition: ‘place’ |
| installing ‘maria’ | C.3 Installing Maria |
| invoking ‘maria’ | 2.1 Invoking Maria |
|
L | | |
| lexical conventions | 1.2 Lexical Conventions |
| LIFO buffers | 1.5.6 Buffers |
| line counter, setting | 1.2.4.3 Setting the Line Number: ‘#line’ |
| LTL | 1.7 Temporal Logic |
| lvalue | 3.1.4 Finding Assignment Candidates |
|
M | | |
| ‘Makefile’ | C.2 Editing the ‘Makefile’ files |
| marking expressions | 1.6 Operations on Multi-Sets |
| model checking | 2.2.2.7 Evaluating Expressions and Formulae |
| model checking, liveness | 3.2.2 Checking Liveness Properties |
| model checking, safety | 3.2.1 Checking Safety Properties |
| modeling | 1. The Net Description Language |
| modules | 1.3.4 Transition Definition: ‘trans’ |
| modules | 1.3.5 Defining Subnets for Modular State Space Exploration |
| modules | 2.2.2.10 Selecting the Active Subnet |
| multi-sets | 1.6 Operations on Multi-Sets |
| multiplicity | 1.6 Operations on Multi-Sets |
|
N | | |
| name spaces | 1.9 Scoping of Identifiers |
| names, completion of | 2.2.1.1 Name Completion |
| nets, composing | 1. The Net Description Language |
| nets, constructs | 1.3 Constructs for Defining Nets |
| nets, on-the-fly verification | 1.3.6 On-the-Fly Verification |
| nets, place definition | 1.3.3 Place Definition: ‘place’ |
| nets, transition definition | 1.3.4 Transition Definition: ‘trans’ |
| non-determinism | 1.8 Non-Determinism in Transitions |
| numeric constants | 1.2.3.2 Numeric Constants |
|
O | | |
| operator precedence | 1.5.2 Operators |
| output variables | 1.8 Non-Determinism in Transitions |
|
P | | |
| Petri Net mode | 2.3.1 Installing the Petri Net mode |
| places, input | 1.3.4 Transition Definition: ‘trans’ |
| places, output | 1.3.4 Transition Definition: ‘trans’ |
| preprocessor | 1.2.4 Preprocessor Directives |
| preprocessor symbols | 1.2.4.2 Conditional Processing |
| printing | 2.2.4.1 GraphViz, the Graph Visualizer |
| priority transitions | 1.3.4 Transition Definition: ‘trans’ |
|