Đặc tả hình thức - Mô hình động trong Alloy - Nguyễn Thị Minh Tuyền

LOGO Đặc tả hình thức Nguyễn Thị Minh Tuyền Mô hình động trong Alloy Nguyễn Thị Minh Tuyền 1 Đặc tả hình thức 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,.. 2 Nguyễn Thị Minh Tuyền Đặc tả hình thức Các mô hình tĩnh 3 Nguyễn Thị Minh Tuyền Person = {Matt, Sue} Man = {Matt} Woman = {Sue} Married = {} spouse = {} children = {} siblings = {} Person = {Matt, Sue} Man = {Matt} Woman = {Sue} Married = {Matt, Sue} spouse = {(Matt,Sue), (Sue,Matt)} children = {} siblings = {} Person = {Matt, Sue, Sean} Man = {Matt} Woman = {Sue} Married = {Matt, Sue} spouse = {(Matt,Sue), (Sue,Matt)} children = {(Matt,Sean), (Sue,Sean)} siblings = {} Đặc tả hình thức 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 4 Nguyễn Thị Minh Tuyền Đặc tả hình thức Ví dụ abstract sig Person { children: set Person, siblings: set Person } sig Man, Woman extends Person {} sig Married in Person { spouse: one Married } 5 Nguyễn Thị Minh Tuyền Đặc tả hình thức 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 6 Nguyễn Thị Minh Tuyền Đặc tả hình thức 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. 7 Nguyễn Thị Minh Tuyền Đặc tả hình thức Ví dụ abstract sig Person { children: set Person, siblings: set Person } sig Man, Woman extends Person {} sig Married in Person { spouse: one Married } 8 Nguyễn Thị Minh Tuyền Đặc tả hình thức 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 } 9 Nguyễn Thị Minh Tuyền Đặc tả hình thức 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 10 Nguyễn Thị Minh Tuyền Person = {Matt,Sue} Man = {Matt} Woman = {Sue} Married = {} spouse = {} children = {} siblings = {} thời điểm t Person = {Matt, Sue} Man = {Matt} Woman = {Sue} Married = {Matt, Sue} spouse = {(Matt,Sue), (Sue,Matt)} children = {} siblings = {} thời điểm t’ Đặc tả hình thức 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. 11 Nguyễn Thị Minh Tuyền Person = {} Man = {} Woman = {} spouse = {} children = {} siblings = {} thời điểm t Person = {Sue} Man = {} Woman = {Sue} spouse = {} children = {} siblings = {} thời điểm t’ Đặc tả hình thức 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 } 12 Nguyễn Thị Minh Tuyền Đặc tả hình thức abstract sig Person { children: Person set -> Time, siblings: Person set -> Time, spouse: Person lone -> Time } sig Man, Woman extends Person {} 13 Nguyễn Thị Minh Tuyền Ta cần thêm quan hệ sau, nhưng thêm vào đâu? alive: Person set -> Time Đặc tả hình thức 14 Nguyễn Thị Minh Tuyền abstract sig Person { children: Person set -> Time, siblings: Person set -> Time, spouse: Person lone -> Time alive: Person set -> Time } sig Man, Woman extends Person {} Đặc tả hình thức Ô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) } 15 Nguyễn Thị Minh Tuyền Đặc tả hình thức 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) } 16 Nguyễn Thị Minh Tuyền Đặc tả hình thức 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) ... 17 Nguyễn Thị Minh Tuyền Đặc tả hình thức -- 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) ... 18 Nguyễn Thị Minh Tuyền Đặc tả hình thức ... -- 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] ... 19 Nguyễn Thị Minh Tuyền Đặc tả hình thức -- 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) } 20 Nguyễn Thị Minh Tuyền Đặc tả hình thức 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ẹ. 21 Nguyễn Thị Minh Tuyền Person = {Matt, Sue, Sean} Man = {Matt, Sean} Woman = {Sue} spouse = {} children = {} siblings = {} alive = {} thời điểm t Person = {Matt, Sue, Sean} Man = {Matt, Sean} Woman = {Sue} spouse = {} children = {} siblings = {} alive = {Sue} thời điểm t’ Đặc tả hình thức v Một người được sinh ra §  Thêm vào quan hệ alive 22 Nguyễn Thị Minh Tuyền Person = {Matt, Sue, Sean} Man = {Matt, Sean} Woman = {Sue} spouse = {(Matt,Sue), (Sue,Matt)} children = {} siblings = {} alive = {Matt, Sue} Person = {Matt, Sue, Sean} Man = {Matt, Sean} Woman = {Sue} spouse = {(Matt,Sue), (Sue,Matt)} children = {(Matt,Sean), (Sue,Sean)} siblings = {} alive = {Matt, Sue, Sean} Đặc tả hình thức Các chuỗi trạng thái 23 Nguyễn Thị Minh Tuyền Person = {Matt, Sue, Sean} Man = {Matt, Sean} Woman = {Sue} spouse = {} children = {} siblings = {} alive = {Sue} Person = {Matt, Sue, Sean} Man = {Matt, Sean} Woman = {Sue} spouse = {} children = {} siblings = {} alive = {} Person = {Matt, Sue, Sean} Man = {Matt, Sean} Woman = {Sue} spouse = {(Matt,Sue), (Sue,Matt)} children = {} siblings = {} alive = {Sue, Matt} Person = {Matt, Sue, Sean} Man = {Matt, Sean} Woman = {Sue} spouse = {(Matt,Sue), (Sue,Matt)} children = {(Matt,Sean), (Sue,Sean)} siblings = {} alive = {Sue, Matt, Sean} Đặc tả hình thức 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. 24 Nguyễn Thị Minh Tuyền Đặc tả hình thức 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. 25 Nguyễn Thị Minh Tuyền Đặc tả hình thức 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 ?? } 26 Nguyễn Thị Minh Tuyền Đặc tả hình thức 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. 27 Nguyễn Thị Minh Tuyền Đặc tả hình thức 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 } 28 Nguyễn Thị Minh Tuyền Đặc tả hình thức 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’] } 29 Nguyễn Thị Minh Tuyền Đặc tả hình thức 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 } 30 Nguyễn Thị Minh Tuyền Đặc tả hình thức 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'] } 31 Nguyễn Thị Minh Tuyền Đặc tả hình thức 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’] } 32 Nguyễn Thị Minh Tuyền Đặc tả hình thức 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’] } 33 Nguyễn Thị Minh Tuyền Đặc tả hình thức Đặ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 34 Nguyễn Thị Minh Tuyền Đặc tả hình thức Đặc tả bước đầu tiên pred init [t: Time] { no children.t no spouse.t no alive.t } 35 Nguyễn Thị Minh Tuyền Đặc tả hình thức Đặ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} 36 Nguyễn Thị Minh Tuyền Đặc tả hình thức 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 ) } 37 Nguyễn Thị Minh Tuyền LOGO