Giáo trình Đặc tả hình thức - Chương 7: Mô hình động trong Alloy - Nguyễn Thị Minh Tuyền

Nội dung text: Giáo trình Đặc tả hình thức - Chương 7: Mô hình động trong Alloy - Nguyễn Thị Minh Tuyền

1. LOGO Đặc tả hình thức Mô hình động trong Alloy Nguyễn Thị Minh Tuyền Nguyễn Thị Minh Tuyền 1
2. Các mô hình tĩnh v Trong các buổi học trước § định nghĩa các mô hình dựa vào tập hợp và quan hệ v Một instance của mô hình là một tập các giá trị thỏa mãn các ràng buộc được định nghĩa bởi multiplicity, fact, Nguyễn Thị Minh Tuyền 2 Đặc tả hình thức
3. Các mô hình tĩnh Person = {Matt, Sue} Person = {Matt, Sue} Man = {Matt} Man = {Matt} Woman = {Sue} Woman = {Sue} Married = {} Married = {Matt, Sue} spouse = {} spouse = {(Matt,Sue), (Sue,Matt)} children = {} children = {} siblings = {} siblings = {} Person = {Matt, Sue, Sean} Man = {Matt} Woman = {Sue} Married = {Matt, Sue} spouse = {(Matt,Sue), (Sue,Matt)} children = {(Matt,Sean), (Sue,Sean)} siblings = {} Nguyễn Thị Minh Tuyền 3 Đặc tả hình thức
4. Mô hình động v Các mô hình tĩnh cho phép mô tả trạng thái hợp lệ của một hệ thống động. v Ta cũng có thể mô tả các chuyển đổi hợp lệ giữa các trạng thái. v Ví dụ: § Một người được sinh ra trước khi họ cưới § Một người kết hôn trước khi có con § Một người là con cho đến khi họ chết Nguyễn Thị Minh Tuyền 4 Đặc tả hình thức
5. Ví dụ abstract sig Person { children: set Person, siblings: set Person } sig Man, Woman extends Person {} sig Married in Person { spouse: one Married } Nguyễn Thị Minh Tuyền 5 Đặc tả hình thức
6. Chuyển đổi v Hai người cưới nhau: § Tại thời điểm t, spouse = {} § Tại thời điểm t’, spouse = {(Matt, Sue), (Sue,Matt)} v ⇒ Ta thêm khái niệm về thời gian vào trong quan hệ spouse Nguyễn Thị Minh Tuyền 6 Đặc tả hình thức
7. Mô hình hóa chuyển đổi trạng thái v Alloy không có khái niệm về chuyển đổi trạng thái. v Một phương pháp tổng quát và khá đơn giản để mô hình hóa khía cạnh động của một hệ thống: § thêm signature Time để biểu diễn thời gian § thêm thành phần thời gian vào mỗi quan hệ mà nó sẽ thay đổi theo thời gian. Nguyễn Thị Minh Tuyền 7 Đặc tả hình thức
8. Ví dụ abstract sig Person { children: set Person, siblings: set Person } sig Man, Woman extends Person {} sig Married in Person { spouse: one Married } Nguyễn Thị Minh Tuyền 8 Đặc tả hình thức
9. sig Time{} abstract sig Person { children: Person set -> Time, siblings: Person set -> Time } sig Man, Woman extends Person {} sig Married in Person { spouse: Married one -> Time } Nguyễn Thị Minh Tuyền 9 Đặc tả hình thức
10. Các chuyển đổi v Hai người cưới nhau § Tại thời điểm t, Married = {} § Tại thời điểm t’, Married = {Matt, Sue} v Thực tế, ta không thể có một signature phụ thuộc thời gian, vì signature độc lập về thời gian. § Ví dụ: quan hệ Married Person = {Matt,Sue} Person = {Matt, Sue} Man = {Matt} Man = {Matt} Woman = {Sue} Woman = {Sue} Married = {} Married = {Matt, Sue} spouse = {} spouse = {(Matt,Sue), (Sue,Matt)} children = {} children = {} siblings = {} siblings = {} thời điểm t thời điểm t’ Nguyễn Thị Minh Tuyền 10 Đặc tả hình thức
11. Các chuyển đổi v Một người được sinh ra § Tại thời điểm t, Person = {} § Tại thời điểm t’, Person = {Sue} v Ta không thể thêm khái niệm được sinh ra vào signature Person vì signature độc lập về thời gian. Person = {} Person = {Sue} Man = {} Man = {} Woman = {} Woman = {Sue} spouse = {} spouse = {} children = {} children = {} siblings = {} siblings = {} thời điểm t thời điểm t’ Nguyễn Thị Minh Tuyền 11 Đặc tả hình thức
12. Signature mang tính chất tĩnh abstract sig Person { children: Person set -> Time, siblings: Person set -> Time, spouse: Person lone -> Time } sig Man, Woman extends Person {} sig Married in Person { spouse: Married one -> Time } Nguyễn Thị Minh Tuyền 12 Đặc tả hình thức
13. abstract sig Person { children: Person set -> Time, siblings: Person set -> Time, spouse: Person lone -> Time } sig Man, Woman extends Person {} Ta cần thêm quan hệ sau, nhưng thêm vào đâu? alive: Person set -> Time Nguyễn Thị Minh Tuyền 13 Đặc tả hình thức
14. abstract sig Person { children: Person set -> Time, siblings: Person set -> Time, spouse: Person lone -> Time alive: Person set -> Time } sig Man, Woman extends Person {} Nguyễn Thị Minh Tuyền 14 Đặc tả hình thức
15. Ôn lại các ràng buộc abstract sig Person { children: Person set -> Time, siblings: Person set -> Time, spouse: Person lone -> Time, alive: set Time parents: Person set -> Time } sig Man, Woman extends Person {} fun parents[] : Person->Person {~children} fact parentsDef { all t: Time | parents.t = ~(children.t) } Nguyễn Thị Minh Tuyền 15 Đặc tả hình thức
16. fact parentsDef { all t: Time | parents.t = ~(children.t) } Hai người có quan hệ huyết thống nếu họ có chung tổ tiên pred BloodRelatives [p, q: Person, t: Time]{ some p.*(parents.t) & q.*(parents.t) } Nguyễn Thị Minh Tuyền 16 Đặc tả hình thức
17. fact static { Một người không thể là tổ tiên của chính họ all t: Time | no p: Person | p in p.^(parents.t) Không ai có nhiều hơn một bố và nhiều hơn một mẹ all t: Time | all p: Person | lone (p.parents.t & Man) and lone (p.parents.t & Woman) Nguyễn Thị Minh Tuyền 17 Đặc tả hình thức
18. Anh chị em của một người p là những người khác p và có cùng bố mẹ với p all t: Time | all p: Person | p.siblings.t = ({q: Person | p.parents.t = q.parents.t} – p ) Mỗi người có đàn ông/phụ nữ có gia đình thì có một vợ/chồng all t: Time | all p: Person | let s = p.spouse.t | (p in Man implies s in Woman) and (p in Woman implies s in Man) Nguyễn Thị Minh Tuyền 18 Đặc tả hình thức
19. Hai người không thể vừa là vợ chồng vừa là anh em của nhau được all t: Time | no p: Person | some p.spouse.t and p.spouse.t in p.siblings.t Người ta không thể cưới người có quan hệ huyết thống all t: Time | no p: Person | let s = p.spouse.t | some s and BloodRelatives [p, p.spouse.t, t] Nguy ễn Thị Minh Tuyền 19 Đặc tả hình thức
20. một người không thể có con với người có quan hệ huyết thống với mình all t: Time | all p, q: Person | (some (p.children.t & q.children.t) and p != q) implies not BloodRelatives [p, q, t] quan hệ spouse là đối xứng all t: Time | spouse.t = ~(spouse.t) } Nguyễn Thị Minh Tuyền 20 Đặc tả hình thức
21. Chuyển đổi v Một người được sinh ra § Thêm vào quan hệ alive. v Chú ý: ở đây không có yêu cầu một người phải có bố mẹ. Person = {Matt, Sue, Sean} Person = {Matt, Sue, Sean} Man = {Matt, Sean} Man = {Matt, Sean} Woman = {Sue} Woman = {Sue} spouse = {} spouse = {} children = {} children = {} siblings = {} siblings = {} alive = {} alive = {Sue} thời điểm t thời điểm t’ Nguyễn Thị Minh Tuyền 21 Đặc tả hình thức
22. v Một người được sinh ra § Thêm vào quan hệ alive Person = {Matt, Sue, Sean} Person = {Matt, Sue, Sean} Man = {Matt, Sean} Man = {Matt, Sean} Woman = {Sue} Woman = {Sue} spouse = {(Matt,Sue), (Sue,Matt)} spouse = {(Matt,Sue), (Sue,Matt)} children = {} children = {(Matt,Sean), (Sue,Sean)} siblings = {} siblings = {} alive = {Matt, Sue} alive = {Matt, Sue, Sean} Nguyễn Thị Minh Tuyền 22 Đặc tả hình thức
23. Các chuỗi trạng thái Person = {Matt, Sue, Sean} Person = {Matt, Sue, Sean} Man = {Matt, Sean} Man = {Matt, Sean} Woman = {Sue} Woman = {Sue} spouse = {} spouse = {(Matt,Sue), (Sue,Matt)} children = {} children = {} siblings = {} siblings = {} alive = {Sue} alive = {Sue, Matt} Person = {Matt, Sue, Sean} Person = {Matt, Sue, Sean} Man = {Matt, Sean} Man = {Matt, Sean} Woman = {Sue} Woman = {Sue} spouse = {} spouse = {(Matt,Sue), (Sue,Matt)} children = {} children = {(Matt,Sean), (Sue,Sean)} siblings = {} siblings = {} alive = {} alive = {Sue, Matt, Sean} Nguyễn Thị Minh Tuyền 23 Đặc tả hình thức
24. Biểu diễn một chuyển đổi v Một chuyển đổi có thể được mô hình hóa như một vị từ giữa hai trạng thái: § Trạng thái ngay trước khi chuyển đổi và § Trạng thái ngay sau khi chuyển đổi. v Ta định nghĩa nó như một vị từ với (ít nhất) hai tham số hình thức: t, t’: Time v Các ràng buộc trên thời gian t (t’) mô hình hóa trạng thái ngay trước (ngay sau) chuyển đổi. Nguyễn Thị Minh Tuyền 24 Đặc tả hình thức
25. Biểu diễn một chuyển đổi v Ràng buộc điều kiện trước § Mô tả các trạng thái mà chuyển đổi áp dụng v Ràng buộc điều kiện sau § Mô tả hiệu ứng của chuyển đổi khi sinh ra trạng thái tiếp theo v Ràng buộc frame condition § Mô tả cái gì không thay đổi giữa trạng thái trước và trạng thái sau khi chuyển đổi. Nguyễn Thị Minh Tuyền 25 Đặc tả hình thức
26. Ví dụ pred marriage [m: Man, w: Woman, t,t': Time, ] { điều kiện trước m và w phải sống trước khi cưới m+w in alive.t m và w chưa có gia đình no (m+w).spouse.t m và w không có quan hệ huyết thống với nhau not BloodRelatives [m, w, t] điều kiện sau sau khi cưới w là vợ của m m.spouse.t' = w sau khi cưới m là chồng của w (dư thừa) frame condition ?? } Nguyễn Thị Minh Tuyền 26 Đặc tả hình thức
27. Frame condition v Những quan hệ nào không bị ảnh hưởng bởi quan hệ hôn nhân? v Có 5 quan hệ: § children, parents, siblings § spouse § alive v Quan hệ parents và siblings được định nghĩa dựa vào quan hệ children. Vì vậy frame condition chỉ xem xét các quan hệ children, spouse và alive. Nguyễn Thị Minh Tuyền 27 Đặc tả hình thức
28. Các vị từ frame condition pred noChildrenChangeExcept [ps: set Person t,t': Time] { all p: Person - ps | p.children.t' = p.children.t } pred noSpouseChangeExcept [ ps: set Person t,t': Time] { all p: Person - ps | p.spouse.t' = p.spouse.t } pred noAliveChange [t,t': Time] { alive.t’ = alive.t } Nguyễn Thị Minh Tuyền 28 Đặc tả hình thức
29. Ví dụ: marriage pred marriage [m: Man, w: Woman, t,t': Time]{ điều kiện trước m+w in alive.t no (m+w).spouse.t not BloodRelatives [m, w, t] điều kiện sau m.spouse.t' = w frame condition noChildrenChangeExcept [none, t, t’] noSpouseChangeExcept [m+w, t, t’] noAliveChange [t, t’] } Nguyễn Thị Minh Tuyền 29 Đặc tả hình thức
30. Instance của marriage open ordering [Time] as T pred marriageInstance { some t: Time | some m: Man | some w: Woman | let t' = T/next [t] | marriage [m, w, t, t’] } run {marriageInstance } Nguyễn Thị Minh Tuyền 30 Đặc tả hình thức
31. pred birth [t, t': Time]{ điều kiện trước và điều kiện sau one p: Person | p !in alive.t and alive.t’ = alive.t + p frame condition noChildrenChangeExcept [none, t, t'] noSpouseChangeExcept [none, t, t'] } Nguyễn Thị Minh Tuyền 31 Đặc tả hình thức
32. pred birthFromParents [m, w: Person, t,t': Time]{ điều kiện trước về m, w m+w in alive.t m.spouse.t = w điều kiện trước và điều kiện sau về một đứa con p nào đó one p: Person | { điều kiện trước p !in alive.t điều kiện sau alive.t’ = alive.t + p m.children.t’ = m.children.t + p w.children.t’ = w.children.t + p } frame condition noChildrenChangeExcept [m+w, t, t’] noSpouseChangeExcept [none, t, t’] } Nguyễn Thị Minh Tuyền 32 Đặc tả hình thức
33. pred birthInstance { some t: Time | let t' = T/next [t] | birth [t, t'] } pred birthFromParentsInstance { some t: Time | some m, w: Person | let t' = T/next [t] | birthFromParents [m, w, t, t’] } Nguyễn Thị Minh Tuyền 33 Đặc tả hình thức
34. Đặc tả hệ thống chuyển đổi v Một hệ thống chuyển đổi là một tập các trace: các chuỗi tuần tự các bước liên quan đến thời gian được phát sinh ra từ các phép toán. v Với mỗi trace: § Bước thời gian đầu tiên thỏa mãn điều kiện đầu. § Mỗi cặp các bước kế tiếp nhau liên quan đến nhau bởi: • một toán tử birth, hoặc • một toán tử marriage, hoặc • một toán từ birthFromParents Nguyễn Thị Minh Tuyền 34 Đặc tả hình thức
35. Đặc tả bước đầu tiên pred init [t: Time] { no children.t no spouse.t no alive.t } Nguyễn Thị Minh Tuyền 35 Đặc tả hình thức
36. Đặc tả của một trace fact Trace { init [T/first] all t: Time - T/last | let t’ = T/next [t] | birth [t, t’] or one m: Man | one w: Woman | marriage [m, w, t, t’] or birthFromParents [m, w, t, t’] } run {Trace and some Man and some Woman} Nguyễn Thị Minh Tuyền 36 Đặc tả hình thức
37. Ràng buộc trên quan hệ alive fact staticAlive { all t: Time | all p: Person | let mainRels = children + spouse | p !in alive.t implies ( no p.mainRels.t and no q: Person | p in q.mainRels.t ) } Nguyễn Thị Minh Tuyền 37 Đặc tả hình thức