Download CGMTool User Manual

5 Well-formedness Analysis, Scenario Generation and Reasoning
5.1
5.2
5.3
27
Well-formedness Check . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
27
5.1.1
Launch Well-formedness Analysis . . . . . . . . . . . . . . . . . . . .
28
Scenario Generation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
29
5.2.1
Generate Scenario Model . . . . . . . . . . . . . . . . . . . . . . . . .
29
Reasoning on the Model . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
5.3.1
31
Launch Reasoner . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
6 Acknowledgment
34
Appendices
35
A BNF of SMT Formulas
35
7 Acronym
37
ii