Nội dung chương 7 trình bày đến người học những vấn đề liên quan đến "Mô hình động trong Alloy", cụ thể như: Các mô hình tĩnh, mô hình hóa chuyển đổi trạng thái, signature mang tính chất tĩnh, các chuỗi trạng thái, biểu diễn một chuyển đổi,. | 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 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 Các mô hình tĩnh 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 = {} Nguyễn Thị Minh Tuyền 3 Đặ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 Nguyễn Thị Minh Tuyền 4 Đặ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 } Nguyễn Thị Minh Tuyền 5 Đặc tả hình .
