Daniel Jackson's software concepts formalized using Alloy and TLA+.
The repository includes formal models of both the individual concepts and of apps built by composing those concepts using synchronization rules (aka reactions).
| Concept | Parameters | State | Actions | Formalizations | Used in |
|---|---|---|---|---|---|
| Chat | User Content |
joined: User → lone Time sent: set Message read: User → set Message time: one Time |
join leave send delete read |
Alloy, TLA+ | Zoomy |
| Label | Item Tag |
labels: Item → set Tag |
affix detach clear |
Alloy, TLA+ | ColoredFiles1 ColoredFiles1 ColoredFiles2 ColoredFiles3 Restaurant1 |
| Meeting | User |
host: lone User participants: set User |
start join leave end |
Alloy, TLA+ | Zoomy |
| Messaging | User Content |
inbox: User → set Message outbox: User → set Message read: User → set Message time: one Time |
send read deleteFromInbox deleteFromOutbox |
Alloy, TLA+ | Restaurant2 |
| Owning | User Resource |
owns: User → set Resource |
acquire release |
Alloy, TLA+ | FileSystem OnlineDrive Zoomy |
| Permalink | Resource URL |
urls: Resource → set URL revoked: set URL accessed: set URL |
share revoke access |
Alloy, TLA+ | FileSharing1 FileSharing2 FileSharing3 |
| Reservation | User Resource |
available: set Resource reservations: User → set Resource |
provide retract reserve cancel use |
Alloy, TLA+ | Restaurant1 Restaurant2 |
| Trash | Item |
accessible: set Item trashed: set Item |
create delete restore empty |
Alloy, TLA+ | ColoredFiles1 ColoredFiles2 ColoredFiles3 FileSharing1 FileSharing2 FileSharing3 FileSystem NoSecretsInTrash1 NoSecretsInTrash2 OnlineDrive |
| WebApp | User |
registered: set User loggedin: lone User |
register login logout delete |
Alloy | OnlineDrive |
| App | Uses | Formalizations | Description |
|---|---|---|---|
| ColoredFiles1 | Label Trash | Alloy, TLA+ | Accessible files can be labeled with a color. When the file is deleted the colors are removed. |
| ColoredFiles2 | Label Trash | Alloy, TLA+ | Both accessible and trashed files can be labeled with a color. When the trash is emptied the colors are removed. |
| ColoredFiles3 | Label Trash | Alloy, TLA+ | Both accessible and trashed files can be labeled with a color. The special color red is used to label trashed files, and added or removed automatically when the file is deleted or restored. When the trash is emptied the colors are removed. |
| FileSharing1 | Permalink Trash | Alloy | Accessible files can be shared with permalinks. When a file is deleted or a permalink is accessed, the permalink is revoked. User cannot directly revoke permalinks. |
| FileSharing2 | Permalink Trash | Alloy | Accessible files can be shared with permalinks. Permalinks are kept when the file is deleted, but cannot be accessed unless the file is restored. When the trash is emptied all permalinks are revoked. User cannot directly revoke permalinks. |
| FileSharing3 | Permalink Trash | Alloy, TLA+ | When a file is created it is automatically shared via a permalink. When the permalink is accessed, the file is deleted, the permalink is revoked, and the trash is emptied. User cannot directly delete and share files or revoke permalinks. |
| FileSystem | Trash Owning | Alloy, TLA+ | A simple hierarchical file system with trash functionality. |
| NoSecretsInTrash1 | Trash | Alloy, TLA+ | Secret files cannot be in the trash. When a secret file is deleted the trash is emptied, possibly leading to the loss of other files. |
| NoSecretsInTrash2 | Trash | Alloy | Secret files cannot be in the trash. When a secret file is deleted the non-secret files are temporarily restored before the trash is emptied. |
| OnlineDrive | Owning Trash WebApp | Alloy | A simple online drive with trash functionality. The files do not have to be permanently deleted when the account is deleted, but when an account is created the acquired trash must be empty. |
| Restaurant1 | Label Reservation | Alloy, TLA+ | A restaurant where reserved tables are automatically assigned a Reserved label. |
| Restaurant2 | Messaging Reservation | Alloy, TLA+ | A restaurant that confirms reservations via messages and keeps track of active reservations by the messages in its outbox. |
| Zoomy | Chat Meeting Owning | Alloy, TLA+ | A simple video conferencing app where when a chat is created when a meeting starts. The owning concept is used in two different ways, for hosts to schedule meetings, and for meetings to acquire chats. The acquired chat can actually contain messages from previous meetings, but they can not be read. |