| Index Entry | Section |
|
E | | |
| Emacs | 2.3 Editing Petri Nets with GNU Emacs |
| Emacs, customizing | 2.3.3 Customizing Emacs |
| empty | 1.6 Operations on Multi-Sets |
| enabled | 1.3.4 Transition Definition: `trans' |
| enabled | 1.3.6.2 Defining Fairness Constraints |
| enum | 1.4.2.4 Enumerated Type |
| equals | 1.6 Operations on Multi-Sets |
| eval, query language | 2.2.2.7 Evaluating Expressions and Formulae |
| exit, query language | 2.2.2.19 Exiting |
| 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 |
| false | A.4.1 Literals |
| fatal | A.4.1 Literals |
| FIFO buffers | 1.5.6 Buffers |
| function, query language | 2.2.2.15 Defining Functions |
| functions, defining | 1.3.2 Function Definitions |
| functions, defining | 2.2.2.15 Defining Functions |
|
G | | |
| gate | 1.3.4 Transition Definition: `trans' |
| go, query language | 2.2.2.13 Moving in the Graph |
| grammar, summary | A. The Grammar |
| graph, query language | 2.2.2.1 Loading a Model |
| GraphViz | 2.2.4.1 GraphViz, the Graph Visualizer |
|
H | | |
| help, query language | 2.2.2.18 Miscellanous Commands |
| hide | 1.3.4 Transition Definition: `trans' |
| hide, query language | 2.2.2.9 Excluding Places from Displayed Markings |
|
I | | |
| id | 1.4.2.5 Identifier Type |
| identifiers, syntax of | 1.2.3.4 Identifiers |
| if-then-else, generalized | 1.5.2.5 Selection |
| in | 1.3.4 Transition Definition: `trans' |
| 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 |
| int | 1.4.2.1 Integer Types |
| intersect | 1.6 Operations on Multi-Sets |
| invoking `maria' | 2.1 Invoking Maria |
| is | 1.5.4 Unions |
| is, unary | 1.5.2.6 Type Casting |
|
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' |
| log, query language | 2.2.2.18 Miscellanous Commands |
| lsts, query language | 2.2.2.4 Exporting a Labelled State Transition System |
| 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 |
| max | 1.6 Operations on Multi-Sets |
| min | 1.6 Operations on Multi-Sets |
| minus | 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 |
| model, query language | 2.2.2.1 Loading a Model |
| 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 |
| out | 1.3.4 Transition Definition: `trans' |
| output variables | 1.8 Non-Determinism in Transitions |
|
P | | |
| path, query language | 2.2.2.17 Shortest Paths |
| Petri Net mode | 2.3.1 Installing the Petri Net mode |
| place | 1.3.3 Place Definition: `place' |
| place | 1.3.4 Transition Definition: `trans' |
| place | 1.6 Operations on Multi-Sets |
| places, input | 1.3.4 Transition Definition: `trans' |
| places, output | 1.3.4 Transition Definition: `trans' |
| pred, query language | 2.2.2.12 Listing Predecessor Nodes |
| 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' |
| prompt, query language | 2.2.2.18 Miscellanous Commands |
| prop | 1.3.6.3 Specifying State Propositions for LSTS Output |
|