Download IMITATOR User Manual

Contents
Table of contents
2
1 Introduction
3
2 Installing IMITATOR
3
3 Implementation
3.1 Inputs and Outputs . . . . . . . . . . . . . . . . . . . . . . .
3.2 Features . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
3
3
4
4 How to Use Imitator
4.1 Installation . . . . . . . . . . . . . .
4.2 The Imitator Input File . . . . . .
4.2.1 Variables . . . . . . . . . . .
4.2.2 Parametric Timed Automata
4.2.3 Initial region and π0 . . . . .
4.3 Calling Imitator . . . . . . . . . . .
4.3.1 Reachability Analysis . . . .
4.3.2 Inverse Method . . . . . . . .
4.3.3 Cartography . . . . . . . . .
4.3.4 Options . . . . . . . . . . . .
4.3.5 Examples of Calls . . . . . .
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
5
5
5
5
6
6
6
6
6
7
8
12
5 Example: SR-latch
13
5.1 Parametric Reachability Analysis . . . . . . . . . . . . . . . . 13
5.2 Behavioral Cartography Algorithm . . . . . . . . . . . . . . . 14
Acknowledgments
18
References
19
A Source Code of the Example
21
A.1 Main Input File . . . . . . . . . . . . . . . . . . . . . . . . . . 21
A.2 V0 File . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25
B Complete Grammar
B.1 Grammar of the Input File . .
B.1.1 Automata Descriptions
B.1.2 Initial State . . . . . . .
B.2 Reserved Words . . . . . . . . .
2
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
26
26
26
29
30