-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathassumption.txt
62 lines (38 loc) · 3.12 KB
/
assumption.txt
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
Các giả định và các hướng giải quyết:
1. Tập trung vào 01 ràng buộc người dùng đang hướng đến
2. Đưa oclUndefined vào invalid snapshots
3. Đưa oclUndefined vào valid snapshots
Các câu hỏi:
1. Một ràng buộc mà người dùng hướng tới có tương ứng với 1 thể hiện của 1 pattern không ?
2. Một ràng buộc mà người dùng hướng tới có thể được chia nhỏ và tương ứng với nhiều hơn 01 pattern?
3. Một phát biểu lỗi đối với 1 snapshot liên quan đến nhiều hơn 01 pattern?
4. Người dùng có thể đặc tả 1 khuôn snapshot mà nó sẽ luôn vi phạm ràng buộc hiện thời
/ hoặc luôn thỏa mãn ràng buộc hiện thời ?
5. Khuôn invalid snapshot tương ứng với Snok1:
- Inv_i is relevant if it always rejects T<Snok1>
- Inv_j is irrelevant if we could find a snapshot T<Snok1> that is accepted by it
- How to find such a snapshot? (domain restrictions được xác định dựa vào tập dữ liệu vào)
6. Khuôn valid snapshot tương ứng với Sok1?
Hướng giải quyết:
Bước 1: Tiếp nhận tập đầu vào SOK, SNOK và sinh tập candidates INV = {Inv1, ..., InvN} như sau:
===============================================================================================
| inv11 inv12 ... inv1n1 | inv21 inv22 ... inv2n2 | ... | invN1 invN2 ... invNnN |
===============================================================================================
Sok1 | 0 0 0 | 0 0 0 | | 0 0 0 |
-------+--------------------------+--------------------------+-----+--------------------------+
Sok2 | 0 0 0 | 0 0 0 | | 0 0 0 |
-------+--------------------------+--------------------------+-----+--------------------------+
.... | | | | |
-------+--------------------------+--------------------------+-----+--------------------------+
SokH | 0 0 0 | 0 0 0 | | 0 0 0 |
===============================================================================================
Snok1 | 1 0 0 | 1 1 0 | ... | 0 1 0 |
-------+--------------------------+--------------------------+-----+--------------------------+
Snok2 | 0 1 0 | 0 1 0 | ... | 1 0 0 |
-------+--------------------------+--------------------------+-----+--------------------------+
... | | | | |
-------+--------------------------+--------------------------+-----+--------------------------+
SnokM | 0 1 1 | 0 0 1 | ... | 1 0 1 |
===============================================================================================
Bước 2:
- Đặc tả khuôn invalid snapshot tương ứng với Snok1