Course Description
Course Schedule
Team Compositions
Final Assignment
Course Literature
Specification Languages
Education Page
PIRRO
• Team A
• Team B
• Team C
Center
Master Program
Center
Home
Courses
People
Projects
Page
Edit Page
Rename Page
Attach File
Printable
Wiki Source
More ...
Web
Recent Changes
Notify Service
News
Page Index
Search
More ...
Wiki
About TWiki
Text Formatting
Registration
Change Password
Reset Password
Users
Groups
Log In
or
Register
Team_A_2
Sws
---+ Conventions * Calligraphic letters (e.g. %$\mathcal{P}$%) represent types * Capital letters (e.g. %$C$%) represent sets * Lowercase letters (e.g. %$b$%) represent an instance of a type * Indexing: most interior index determines the type (e.g. %$n_R$% is revision %$R$% with revision number %$n$%) ---+ Basic definitions ---++Pieces A piece is a scan of a single physical scroll fragment. * Can be disabled/re-enabled (e.g. duplicates) * When disabled will be marked in compositions %$\mathcal{P}$%: the set of all pieces ---++Composition members A composition member is a piece along with a position (relative to the origin of the workspace) and rotation. %$\mathcal{M}$%: the set of all possible composition members<br/> %$\mathcal{M} = \{(p,pos,rot)\,|\, p\in \mathcal{P}, pos\in Position, rot\in Double \}$%<br/> %$Position = Double \times Double \times Integer$% The position includes a z-index which is used to determine how overlapping pieces are displayed. A composition member can only be used in one composition. ---++Compositions A composition consists of a set of 0 or more composition members and an annotation string. %$\mathcal{C}$%: the set of all compositions<br/> %$\mathcal{C} = \{ (ann, members) \;|\; ann \in Annotation, members \subset \mathcal{M}\}$% An annotation is a string which may be empty and may contain newlines.<br/> %$Annotation = String$% ---+ Versioning system ---++ Definitions (informal) ---+++ Branches A branch has * a unique identifier * a sequence of revisions * initially one empty revision with revision number 0. ---+++ Revisions A revision has * a set of compositions * a revision number. ---+++ Workspaces A workspace is a local copy of a branch. ---++ Definitions (formal) ---+++ Branches %$\mathcal{B}$% * sequence of revisions %$R \subseteq \mathcal{R}$% * unique identifier %$i \in String$% ---+++ Revisions %$\mathcal{R}$% * set of compositions %$C \subseteq \mathcal{C}$% * revision number %$n \in \mathcal{N}$% (unique within branch) ---+++ Workspaces %$\mathcal{W}$% representation of a branch in the compositor * set of compositions %$C \subseteq \mathcal{C}$% * branch %$b \in \mathcal{B}$% * revision number %$n \in \mathcal{N}$% ---++ Uniqueness constraint ---+++ Revision Piece uniqueness: pieces can only occur once. ---+++ Workspace No piece uniqueness: pieces can occur in multiple compositions (conflicts can occur). ---++ State/operations (informal) ---+++ Initial state * Only one branch, named "trunk". ---+++ Checkout * Create a new workspace from a branch * Optionally specify revision number ---+++ Update * Add all compositions from newer revisions in the branch to the workspace * Optionally specify revision number * Can result in conflicts ---+++ Import * Copy one or more compositions from another branch into the workspace * Can result in conflicts ---+++ Branch * Create a new branch as a copy of another branch * Optionally specify revision number ---+++ Commit * Stores the workspace as a new revision in the branch * Requires conflicts to be resolved first (uniqueness constraint) * Requires workspace to be up-to-date (same revision as branch) * The revision number is the previous revision number increased by 1 ---++ State/operations (formal) ---+++Bigbang <div style="float: left"> %BEGINLATEX{density="150"}% \begin{description} \item[Pre-state] $\emptyset$ \item[In-event] $bigbang() $ \item[Out-event] \item[Post-state] $ \{b | b_i = $ "trunk" $, b_R = \{ R | R_C = \emptyset, R_n = 0 \} \} $ \end{description} %ENDLATEX% </div> <div style="clear: both"></div> ---+++Checkout <div style="float: left"> %BEGINLATEX{density="150"}% \begin{description} \item[Pre-state] $\mathcal{B}$ \item[In-event] $ checkout(b, n)$ \\ $ b \in \mathcal{B}, n_R \subseteq b_\mathcal{R} $ \item[Out-event] $ create (w | w_C = R_C, w_b = b, w_n = n) $ \item[Post-state] $\mathcal{B}$ \end{description} %ENDLATEX% </div> <div style="clear: both"></div> ---+++Update <div style="float: left"> %BEGINLATEX{density="150"}% \begin{description} \item[Pre-state] $\mathcal{B}$ \item[In-event] $update(w) $ \\ $ w \in \mathcal{W}, w_b \in \mathcal{B} $ \item[Out-event] $modify (w| w_C = w_C \cup last(w_{b_R})_C, w_n = last(w_{b_R})_n ) $ \item[Post-state] $\mathcal{B}$ \end{description} %ENDLATEX% </div> <div style="clear: both"></div> ---+++Import <div style="float: left"> %BEGINLATEX{density="150"}% \begin{description} \item[Pre-state] $\mathcal{B}$ \item[In-event] $import(b, n, c, w) $ \\ $ b \in \mathcal{B}, n_r \in b_\mathcal{R} , C \subseteq r_C , w \in \mathcal{W} $ \item[Out-event] $modify (w, w_C = w_C \cup R_C ) $ \item[Post-state] $\mathcal{B}$ \end{description} %ENDLATEX% </div> <div style="clear: both"></div> ---+++Branch <div style="float: left"> %BEGINLATEX{density="150"}% \begin{description} \item[Pre-state] $\mathcal{B}$ \item[In-event] $branch(b, n, i) $ \\ $ b \in \mathcal{B}, n_R \in b_\mathcal{R}, i \in String $ \item[Out-event] - \item[Post-state] $\mathcal{B} \cup \{ b'| b'_i = i , b'_{R_C} = n_{R_C} , b'_{R_n} = 0 \} $ \end{description} %ENDLATEX% </div> <div style="clear: both"></div> ---+++Commit <div style="float: left"> %BEGINLATEX{density="150"}% \begin{description} \item[Pre-state] $\mathcal{B}$ \item[In-event] $commit(w) $ \\ $ w \in \mathcal{W} , w_b \in \mathcal{B} $ \item[Out-event] - \item[Post-state] $ ( \mathcal{B} / b ) \cup \{ b' | b'_i = b_i, b'_R = b_R \cup $\\$ \{ R | R_C = w_C, b'_{R_n} = last(b_\mathcal{R})_n + 1 \} \} $ \end{description} %ENDLATEX% </div> <div style="clear: both"></div>