Download IMITATOR User Manual - LSV

Contents
1 Introduction
3
2 Behavioral Cartography
2.1 Parametric Timed Automata . . . . . .
2.2 A Motivating Example . . . . . . . . . .
2.3 The Inverse Method . . . . . . . . . . .
2.4 The Behavioral Cartography Algorithm
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
4
4
5
6
8
3 Implementation
10
3.1 Inputs and Outputs . . . . . . . . . . . . . . . . . . . . . . . . . 10
3.2 Structure and Implementation . . . . . . . . . . . . . . . . . . . . 11
3.3 Features . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11
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 . . . . . .
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
12
12
12
13
13
13
13
13
14
14
14
17
5 Example: SR-latch
18
5.1 Parametric Reachability Analysis . . . . . . . . . . . . . . . . . . 18
5.2 Behavioral Cartography Algorithm . . . . . . . . . . . . . . . . . 18
6 Final Remarks
22
A Source Code of the Example
25
A.1 Main Input File . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25
A.2 𝑉0 File . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
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
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
30
30
30
32
33