initial version of better aligned bibliography

Thesis/Bibliography.bib

@@ -1,3 +1,56 @@
+@article{replicated_abstract_data_types,
+title = {Replicated abstract data types: Building blocks for collaborative applications},
+journal = {Journal of Parallel and Distributed Computing},
+volume = {71},
+number = {3},
+pages = {354-368},
+year = {2011},
+issn = {0743-7315},
+doi = {https://doi.org/10.1016/j.jpdc.2010.12.006},
+url = {https://www.sciencedirect.com/science/article/pii/S0743731510002716},
+author = {Hyun-Gul Roh and Myeongjae Jeon and Jin-Soo Kim and Joonwon Lee},
+keywords = {Distributed data structures, Optimistic replication, Replicated abstract data types, Optimistic algorithm, Collaboration},
+abstract = {For distributed applications requiring collaboration, responsive and transparent interactivity is highly desired. Though such interactivity can be achieved with optimistic replication, maintaining replica consistency is difficult. To support efficient implementations of collaborative applications, this paper extends a few representative abstract data types (ADTs), such as arrays, hash tables, and growable arrays (or linked lists), into replicated abstract data types (RADTs). In RADTs, a shared ADT is replicated and modified with optimistic operations. Operation commutativity and precedence transitivity are two principles enabling RADTs to maintain consistency despite different execution orders. Especially, replicated growable arrays (RGAs) support insertion/deletion/update operations. Over previous approaches to the optimistic insertion and deletion, RGAs show significant improvement in performance, scalability, and reliability.}
+}
+
+@article{verifying_strong_eventual_consistency,
+author = {Gomes, Victor B. F. and Kleppmann, Martin and Mulligan, Dominic P. and Beresford, Alastair R.},
+title = {Verifying strong eventual consistency in distributed systems},
+year = {2017},
+issue_date = {October 2017},
+publisher = {Association for Computing Machinery},
+address = {New York, NY, USA},
+volume = {1},
+number = {OOPSLA},
+url = {https://doi.org/10.1145/3133933},
+doi = {10.1145/3133933},
+abstract = {Data replication is used in distributed systems to maintain up-to-date copies of shared data across multiple computers in a network. However, despite decades of research, algorithms for achieving consistency in replicated systems are still poorly understood. Indeed, many published algorithms have later been shown to be incorrect, even some that were accompanied by supposed mechanised proofs of correctness. In this work, we focus on the correctness of Conflict-free Replicated Data Types (CRDTs), a class of algorithm that provides strong eventual consistency guarantees for replicated data. We develop a modular and reusable framework in the Isabelle/HOL interactive proof assistant for verifying the correctness of CRDT algorithms. We avoid correctness issues that have dogged previous mechanised proofs in this area by including a network model in our formalisation, and proving that our theorems hold in all possible network behaviours. Our axiomatic network model is a standard abstraction that accurately reflects the behaviour of real-world computer networks. Moreover, we identify an abstract convergence theorem, a property of order relations, which provides a formal definition of strong eventual consistency. We then obtain the first machine-checked correctness theorems for three concrete CRDTs: the Replicated Growable Array, the Observed-Remove Set, and an Increment-Decrement Counter. We find that our framework is highly reusable, developing proofs of correctness for the latter two CRDTs in a few hours and with relatively little CRDT-specific code.},
+journal = {Proc. ACM Program. Lang.},
+month = oct,
+articleno = {109},
+numpages = {28},
+keywords = {verification, strong eventual consistency, replication, distributed systems, convergence, automated theorem proving, CRDTs}
+}
+
+@article{eventually_consistent,
+author = {Vogels, Werner},
+title = {Eventually consistent},
+year = {2009},
+issue_date = {January 2009},
+publisher = {Association for Computing Machinery},
+address = {New York, NY, USA},
+volume = {52},
+number = {1},
+issn = {0001-0782},
+url = {https://doi.org/10.1145/1435417.1435432},
+doi = {10.1145/1435417.1435432},
+abstract = {Building reliable distributed systems at a worldwide scale demands trade-offs between consistency and availability.},
+journal = {Commun. ACM},
+month = jan,
+pages = {40–44},
+numpages = {5}
+}
+
 @inproceedings{convergence_in_distributed_real_time_collaborative_environment,
 author = {Vidot, Nicolas and Cart, Michelle and Ferri\'{e}, Jean and Suleiman, Maher},
 title = {Copies convergence in a distributed real-time collaborative environment},

Thesis/Bibliography.typ

@@ -1,27 +1,213 @@
-#import "@preview/alexandria:0.2.2": *
+#import "@preview/alexandria:0.2.2": alexandria, get-bibliography, load-bibliography
 
-= Spis literatury
+// Global state
+#let used-refs = state("used-refs", ())
 
-== Książki
-#bibliographyx(
-  "Bibliography/Books.bib",
-  prefix: "book-",
-  title: none,
-  style: "ieee",
-)
+// 1. Analizes and sets up the document
+#let bib-setup(body) = {
+  show: alexandria(prefix: "cite:", read: path => read(path))
 
-== Artykuły
-#bibliographyx(
-  "Bibliography/Articles.bib",
-  prefix: "article-",
-  title: none,
-  style: "ieee",
-)
+  // Searching for references in document
+  show ref: it => {
+    let target = str(it.target)
+    if target.starts-with("cite:") {
+      let key = target.slice(5)
+      used-refs.update(arr => if key not in arr { arr + (key,) } else { arr })
+      context {
+        let cites = used-refs.final()
+        let bib = get-bibliography("cite:")
+        let get-type(k) = {
+          let e = bib.references.find(x => x.key == k)
+          if e != none { lower(e.details.at("type", default: "")) } else { "" }
+        }
+        let is-book(t) = t == "book"
+        let is-article(t) = t == "article" or t == "paper-conference" or t == "inproceedings"
+        let is-other(t) = not is-book(t) and not is-article(t)
 
-== Źródła internetowe i inne
-#bibliographyx(
-  "Bibliography/Others.bib",
-  prefix: "other-",
-  title: none,
-  style: "ieee",
-)
+        let books = cites.filter(k => is-book(get-type(k)))
+        let articles = cites.filter(k => is-article(get-type(k)))
+        let others = cites.filter(k => is-other(get-type(k)))
+
+        let sorted = books + articles + others
+        let idx = sorted.position(k => k == key)
+
+        if idx != none { link(it.target, [\[#(idx + 1)\]]) } else { [\[?\]] }
+      }
+    } else { it }
+  }
+
+  body
+}
+
+// 2. Bibliography rendering
+#let render-bib() = {
+  load-bibliography("Bibliography.bib", prefix: "cite:", full: true, style: "ieee")
+
+  heading(level: 1)[Spis literatury]
+  v(1em)
+
+  context {
+    let cites = used-refs.final()
+    if cites.len() > 0 {
+      let bib = get-bibliography("cite:")
+      let get-entry(k) = bib.references.find(e => e.key == k)
+
+      // custom implementation adapting the ZUT's formatting
+      let format-custom(entry) = {
+        let d = entry.details
+        let entry-type = lower(d.at("type", default: ""))
+
+        let format-author(a) = {
+          if type(a) == dictionary {
+            let parts = ()
+            if "given" in a { parts.push(str(a.given)) }
+            if "family" in a { parts.push(str(a.family)) }
+            if parts.len() > 0 { return parts.join(" ") }
+            if "name" in a { return str(a.name) }
+            return ""
+          } else {
+            let s = str(a)
+            let parts = s.split(",")
+            if parts.len() == 2 { return parts.at(1).trim() + " " + parts.at(0).trim() }
+            return s
+          }
+        }
+
+        let raw-auth = d.at("author", default: ())
+        let author-list = if type(raw-auth) == array {
+          raw-auth.map(format-author)
+        } else if raw-auth != none and raw-auth != "" {
+          (format-author(raw-auth),)
+        } else { () }
+
+        let authors = if author-list.len() > 1 {
+          author-list.slice(0, -1).join(", ") + " i " + author-list.last()
+        } else if author-list.len() == 1 { author-list.first() } else { "" }
+
+        let get-val(..keys) = {
+          let extract(obj, k) = {
+            if type(obj) != dictionary { return none }
+            let v = obj.at(k, default: none)
+            if v == none { return none }
+            if type(v) == str { return v }
+            if type(v) in (int, float) { return str(v) }
+            if type(v) == array { return v.filter(x => type(x) in (str, int, float)).map(x => str(x)).join(", ") }
+            if type(v) == dictionary {
+              if "isbn" in v { return str(v.isbn) }
+              if "value" in v { return str(v.value) }
+              if "name" in v { return str(v.name) }
+              if "text" in v { return str(v.text) }
+              return ""
+            }
+            return ""
+          }
+          for k in keys.pos() {
+            let res = extract(d, k)
+            if res == none and "parent" in d { res = extract(d.parent, k) }
+            if res != none and res != "" { return res }
+          }
+          return ""
+        }
+
+        let y = ""
+        let m = ""
+        let date-val = d.at("date", default: none)
+        if type(date-val) == dictionary {
+          y = str(date-val.at("year", default: ""))
+          m = str(date-val.at("month", default: ""))
+        } else if date-val != none { y = str(date-val) }
+        if y == "" { y = get-val("year") }
+        if m == "" { m = get-val("month") }
+
+        if m != "" {
+          if m.match(regex("^\d+$")) != none {
+            let idx = int(m)
+            let months = (
+              "",
+              "sty.",
+              "lut.",
+              "mar.",
+              "kwi.",
+              "maj",
+              "cze.",
+              "lip.",
+              "sie.",
+              "wrz.",
+              "paź.",
+              "lis.",
+              "gru.",
+            )
+            if idx >= 1 and idx <= 12 { m = months.at(idx) }
+          }
+        }
+        let year = if m != "" { m + y } else { y }
+        let title-txt = get-val("title")
+        let series = get-val("collection-title", "series")
+        let pub-place = get-val("location", "address", "publisher-place")
+        let pub = get-val("publisher")
+        let edition = get-val("edition")
+        let volume = get-val("volume")
+        let pages = get-val("page-range", "pages").replace("--", "–").replace("-", "–")
+        let isbn = get-val("isbn", "ISBN", "serial-number", "number")
+        let issue = get-val("issue", "number")
+        let url = get-val("url")
+
+        if entry-type == "book" [
+          #authors. #emph(title-txt).
+          #if edition != "" { if edition.match(regex("^\d+$")) != none [#edition wyd. ] else [#edition. ] }
+          #if volume != "" [T. #volume. ]
+          #if series != "" [#series. ]
+          #if pub-place != "" [#pub-place: ]
+          #if pub != "" [#pub, ]
+          #year#if pages != "" [, s. #pages].
+          #if isbn != "" [ isbn: #isbn.]
+        ] else if entry-type == "article" or entry-type == "paper-conference" [
+          #authors. „#title-txt”. W:#if volume != "" or issue != "" [ #volume#if issue != "" [.#issue]] (#year)#if pages != "" [, s. #pages].
+        ] else [
+          #authors. #emph(title-txt).
+          #if url != "" [ URL: #link(url)[#raw(url)].]
+        ]
+      }
+
+      let get-type(k) = {
+        let e = get-entry(k)
+        if e != none { lower(e.details.at("type", default: "")) } else { "" }
+      }
+
+      let is-book(t) = t == "book"
+      let is-article(t) = t == "article" or t == "paper-conference" or t == "inproceedings"
+      let is-other(t) = not is-book(t) and not is-article(t)
+
+      let render-group(title, keys, start-idx) = {
+        if keys.len() > 0 [
+          == #title
+          #grid(
+            columns: (auto, 1fr),
+            column-gutter: 0.65em,
+            row-gutter: 1em,
+            ..keys
+              .enumerate()
+              .map(((i, k)) => {
+                let entry = get-entry(k)
+                if entry == none { return () }
+                let num = start-idx + i + 1
+                // Pamiętaj: musisz użyć format-custom, który wkleiłeś wyżej!
+                ([\[#num\]], [#format-custom(entry)#label("cite:" + k)])
+              })
+              .flatten()
+          )
+          #v(1em)
+        ]
+      }
+
+      let books = cites.filter(k => is-book(get-type(k)))
+      let articles = cites.filter(k => is-article(get-type(k)))
+      let others = cites.filter(k => is-other(get-type(k)))
+
+      // last parameter is start idx
+      render-group("Książki", books, 0)
+      render-group("Artykuły", articles, books.len())
+      render-group("Źródła internetowe i inne", others, books.len() + articles.len())
+    }
+  }
+}

Thesis/Bibliography/Articles.bib

@@ -1,52 +0,0 @@
-@article{replicated_abstract_data_types,
-title = {Replicated abstract data types: Building blocks for collaborative applications},
-journal = {Journal of Parallel and Distributed Computing},
-volume = {71},
-number = {3},
-pages = {354-368},
-year = {2011},
-issn = {0743-7315},
-doi = {https://doi.org/10.1016/j.jpdc.2010.12.006},
-url = {https://www.sciencedirect.com/science/article/pii/S0743731510002716},
-author = {Hyun-Gul Roh and Myeongjae Jeon and Jin-Soo Kim and Joonwon Lee},
-keywords = {Distributed data structures, Optimistic replication, Replicated abstract data types, Optimistic algorithm, Collaboration},
-abstract = {For distributed applications requiring collaboration, responsive and transparent interactivity is highly desired. Though such interactivity can be achieved with optimistic replication, maintaining replica consistency is difficult. To support efficient implementations of collaborative applications, this paper extends a few representative abstract data types (ADTs), such as arrays, hash tables, and growable arrays (or linked lists), into replicated abstract data types (RADTs). In RADTs, a shared ADT is replicated and modified with optimistic operations. Operation commutativity and precedence transitivity are two principles enabling RADTs to maintain consistency despite different execution orders. Especially, replicated growable arrays (RGAs) support insertion/deletion/update operations. Over previous approaches to the optimistic insertion and deletion, RGAs show significant improvement in performance, scalability, and reliability.}
-}
-
-@article{verifying_strong_eventual_consistency,
-author = {Gomes, Victor B. F. and Kleppmann, Martin and Mulligan, Dominic P. and Beresford, Alastair R.},
-title = {Verifying strong eventual consistency in distributed systems},
-year = {2017},
-issue_date = {October 2017},
-publisher = {Association for Computing Machinery},
-address = {New York, NY, USA},
-volume = {1},
-number = {OOPSLA},
-url = {https://doi.org/10.1145/3133933},
-doi = {10.1145/3133933},
-abstract = {Data replication is used in distributed systems to maintain up-to-date copies of shared data across multiple computers in a network. However, despite decades of research, algorithms for achieving consistency in replicated systems are still poorly understood. Indeed, many published algorithms have later been shown to be incorrect, even some that were accompanied by supposed mechanised proofs of correctness. In this work, we focus on the correctness of Conflict-free Replicated Data Types (CRDTs), a class of algorithm that provides strong eventual consistency guarantees for replicated data. We develop a modular and reusable framework in the Isabelle/HOL interactive proof assistant for verifying the correctness of CRDT algorithms. We avoid correctness issues that have dogged previous mechanised proofs in this area by including a network model in our formalisation, and proving that our theorems hold in all possible network behaviours. Our axiomatic network model is a standard abstraction that accurately reflects the behaviour of real-world computer networks. Moreover, we identify an abstract convergence theorem, a property of order relations, which provides a formal definition of strong eventual consistency. We then obtain the first machine-checked correctness theorems for three concrete CRDTs: the Replicated Growable Array, the Observed-Remove Set, and an Increment-Decrement Counter. We find that our framework is highly reusable, developing proofs of correctness for the latter two CRDTs in a few hours and with relatively little CRDT-specific code.},
-journal = {Proc. ACM Program. Lang.},
-month = oct,
-articleno = {109},
-numpages = {28},
-keywords = {verification, strong eventual consistency, replication, distributed systems, convergence, automated theorem proving, CRDTs}
-}
-
-@article{eventually_consistent,
-author = {Vogels, Werner},
-title = {Eventually consistent},
-year = {2009},
-issue_date = {January 2009},
-publisher = {Association for Computing Machinery},
-address = {New York, NY, USA},
-volume = {52},
-number = {1},
-issn = {0001-0782},
-url = {https://doi.org/10.1145/1435417.1435432},
-doi = {10.1145/1435417.1435432},
-abstract = {Building reliable distributed systems at a worldwide scale demands trade-offs between consistency and availability.},
-journal = {Commun. ACM},
-month = jan,
-pages = {40–44},
-numpages = {5}
-}

Thesis/Bibliography/Books.bib

@@ -1,21 +0,0 @@
-@book{book_key,
-	address = {Szczecin},
-	publisher = {Publisher},
-	author = {Smith, John and Bob Budowniczy and Nowak Jan},
-	title = {Book title},
-	year = {2012},
-	volume = {3},
-	series = {2},
-	edition = {1},
-	pages = {123--200},
-	month = {1}
-}
-
-@book{lam1994,
-	title =		"\LaTeX: A Document Preparation System",
-	edition =	"Second",
-	author =	"Leslie Lamport",
-	publisher =	"Addison-Wesley Publishing Company",
-	year =		"1994",
-	isbn =		"0-201-52983-1",
-}

Thesis/Chapters/1. Theoretical Scope.typ

@@ -2,20 +2,20 @@
 
 = Zakres teoretyczny <teoria>
 == Systemy współdzielenia dokumentów w czasie rzeczywistym
-Budując rozwiązania związane z równoczesnym tworzeniem i modyfikacją tekstu przez więcej niż jednego użytkownika, musimy rozważyć wyzwania napotykane w aktualizacji tworzonego dokumentu, gdzie każdy klient posiada lokalną kopię i nanosi na nie własne zmiany, ale też w międzyczasie musimy nanieść zmiany od pozostałych klientów. W takim systemie mówimy wtedy o zbieżności danych@article-eventually_consistent - czyli zapewnieniu tego samego stanu między każdym klientem. W przypadku edycji tekstu skupię się na ewentualnej zbieżności, która uwzględnia posiadanie rozbieżnych kopii tego samego źródła danych u każdego z klientów przez pewien czas. Dopiero gdy zostanie zakończona edycja tekstu, zmiany zostają propagowane i nanoszone do pozostałych klientów. Finalnie każdy klient po czasie posiada identyczną kopię dokumentu. Ze strony doświadczeń użytkowania jest to skuteczna strategia ze względu na możliwość zapewnienia płynności interfejsu graficznego oraz z pomocą złożonych mechanizmów umożliwia rozwiązywanie konfliktów między kopiami.
+Budując rozwiązania związane z równoczesnym tworzeniem i modyfikacją tekstu przez więcej niż jednego użytkownika, musimy rozważyć wyzwania napotykane w aktualizacji tworzonego dokumentu, gdzie każdy klient posiada lokalną kopię i nanosi na nie własne zmiany, ale też w międzyczasie musimy nanieść zmiany od pozostałych klientów. W takim systemie mówimy wtedy o zbieżności danych@cite:eventually_consistent - czyli zapewnieniu tego samego stanu między każdym klientem. W przypadku edycji tekstu skupię się na ewentualnej zbieżności, która uwzględnia posiadanie rozbieżnych kopii tego samego źródła danych u każdego z klientów przez pewien czas. Dopiero gdy zostanie zakończona edycja tekstu, zmiany zostają propagowane i nanoszone do pozostałych klientów. Finalnie każdy klient po czasie posiada identyczną kopię dokumentu. Ze strony doświadczeń użytkowania jest to skuteczna strategia ze względu na możliwość zapewnienia płynności interfejsu graficznego oraz z pomocą złożonych mechanizmów umożliwia rozwiązywanie konfliktów między kopiami.
 
-Wspomniany model nie jest bez wad. Największym problemem jest istnienie konfliktów, których rozwiązanie klienci muszą ustalić za pomocą dodatkowych strategii. Najeczęściej wykorzystywaną jest Last-Write-Wins (LWW). Rozstrzyga ona konflikty poprzez nanoszenie tylko tej zmiany, która jest uznawana jako ostatnia w kolejności zbioru konfliktujących operacji. Ustalanie kolejności nie jest jasno tutaj zdefiniowane. W systemach baz danych takich jak Cassandra@other-apache_cassandra_documentation oraz SQL Server P2P@other-microsoft_sql_server_p2p_replication_documentation każdy zapis otrzymuje własny znacznik czasowy, na podstawie którego wybierany jest najmłodszy wpis i nim nadpisywane są zmiany w źródle danych. Zmiany ze starszymi znacznikami są porzucane. Zauważalną wadą LWW jest wysokie ryzyko utraty danych w czasie nanoszenia zmian, ponieważ wszystkie konfliktujące starsze zmiany nie są brane pod uwagę.
+Wspomniany model nie jest bez wad. Największym problemem jest istnienie konfliktów, których rozwiązanie klienci muszą ustalić za pomocą dodatkowych strategii. Najeczęściej wykorzystywaną jest Last-Write-Wins (LWW). Rozstrzyga ona konflikty poprzez nanoszenie tylko tej zmiany, która jest uznawana jako ostatnia w kolejności zbioru konfliktujących operacji. Ustalanie kolejności nie jest jasno tutaj zdefiniowane. W systemach baz danych takich jak Cassandra@cite:apache_cassandra_documentation oraz SQL Server P2P@cite:microsoft_sql_server_p2p_replication_documentation każdy zapis otrzymuje własny znacznik czasowy, na podstawie którego wybierany jest najmłodszy wpis i nim nadpisywane są zmiany w źródle danych. Zmiany ze starszymi znacznikami są porzucane. Zauważalną wadą LWW jest wysokie ryzyko utraty danych w czasie nanoszenia zmian, ponieważ wszystkie konfliktujące starsze zmiany nie są brane pod uwagę.
 
-W przypadku tekstu jako typu danych, istnieje specjalny wariant ewentualnej zbieżności - silna ewentualna zbieżność. Ten model wykorzystuje specjalne struktury danych, które zapewniają bezkonfliktowe nanoszenie zmian, a ich skuteczność opiera się na matematycznych dowodach@article-verifying_strong_eventual_consistency.
+W przypadku tekstu jako typu danych, istnieje specjalny wariant ewentualnej zbieżności - silna ewentualna zbieżność. Ten model wykorzystuje specjalne struktury danych, które zapewniają bezkonfliktowe nanoszenie zmian, a ich skuteczność opiera się na matematycznych dowodach@cite:verifying_strong_eventual_consistency.
 
-Istnieje również model silnej zbieżności, gdzie każdy z klientów musi mieć tą samą kopię danych przez cały czas pracy systemu. Ze względu opóźnienia i potrzebę mechanizmu blokady klientów przed wprowadzaniem zmian, ten model został porzucony w dzisiejszych systemach, ponieważ wspomniane problemy skutkowały gorszą użytecznością w porównaniu do systemów wykorzystujących ewentualną zbieżność. Istnieją jednak prace, które wskazują na istnienie systemów opartych o model silnej zbieżności, które osiągają bardzo niskie czasy opóźnienia, co redukuje problem używalności takiego rozwiązania w rzeczywistych zastosowaniach.@other-paxos_document_editor
+Istnieje również model silnej zbieżności, gdzie każdy z klientów musi mieć tą samą kopię danych przez cały czas pracy systemu. Ze względu opóźnienia i potrzebę mechanizmu blokady klientów przed wprowadzaniem zmian, ten model został porzucony w dzisiejszych systemach, ponieważ wspomniane problemy skutkowały gorszą użytecznością w porównaniu do systemów wykorzystujących ewentualną zbieżność. Istnieją jednak prace, które wskazują na istnienie systemów opartych o model silnej zbieżności, które osiągają bardzo niskie czasy opóźnienia, co redukuje problem używalności takiego rozwiązania w rzeczywistych zastosowaniach.@cite:paxos_document_editor
 
 == Algorytmy zapewniające silną ewentualną zbieżność
 Podejście do rozwiązania problemu synchronizacji stanów między każdym klientem wymaga zaprojektowania algorytmu od podstaw skupionego na tym zagadnieniu. Przedstawię dwa najczęściej wykorzystywane algorytmy rozwiązujące opisany problem.
 
-Operational Transformation (OT) polega na zamianie każdej wykonanej operacji na kodowalny obiekt, który może być propagowany i nanoszony na kopie w innych replikach. Większość znanych implementacji zakłada też, że istnieje scentralizowany serwer określający kolejność każdej operacji zgłaszanej przez wszystkich klientów i dystrybujący wspomniane zmiany do pozostałych replik. W przypadku wystąpienia konfliktu, operacje są sortowane przez serwer, a następnie każda z nich jest transformowana tak, by uwzględnić zmianę poprzedniej w kolejności operacji. Przykładowymi propozycjami algorytmów OT, których skuteczność nie została obalona dowodami, są: Jupiter@other-windowing_in_jupiter, SOCT3/4@other-convergence_in_distributed_real_time_collaborative_environment oraz TTF@other-transformation_functions_consistency_ces. Jupiter oraz SOCT3/4 wymagają wcześniej wspomnianego scentralizowanego serwera. Google Docs początkowo korzystał z Operational Transformation@other-google_docs_ot. Ze względu na złożność implementacji większość systemów nie korzysta dziś z tych algorytmów do synchronizacji danych, gdzie przykładem takiej decyzji jest Figma@other-figma_multiplayer.
+Operational Transformation (OT) polega na zamianie każdej wykonanej operacji na kodowalny obiekt, który może być propagowany i nanoszony na kopie w innych replikach. Większość znanych implementacji zakłada też, że istnieje scentralizowany serwer określający kolejność każdej operacji zgłaszanej przez wszystkich klientów i dystrybujący wspomniane zmiany do pozostałych replik. W przypadku wystąpienia konfliktu, operacje są sortowane przez serwer, a następnie każda z nich jest transformowana tak, by uwzględnić zmianę poprzedniej w kolejności operacji. Przykładowymi propozycjami algorytmów OT, których skuteczność nie została obalona dowodami, są: Jupiter@cite:windowing_in_jupiter, SOCT3/4@cite:convergence_in_distributed_real_time_collaborative_environment oraz TTF@cite:transformation_functions_consistency_ces. Jupiter oraz SOCT3/4 wymagają wcześniej wspomnianego scentralizowanego serwera. Google Docs początkowo korzystał z Operational Transformation@cite:google_docs_ot. Ze względu na złożność implementacji większość systemów nie korzysta dziś z tych algorytmów do synchronizacji danych, gdzie przykładem takiej decyzji jest Figma@cite:figma_multiplayer.
 
-Następcą Operational Transformation są bezkonfliktowe replikowane typy danych (Conflict-free replicated data types - CRDT). Pozwalają one na nanoszenie zmian na własne kopie przez klientów, bez potrzeby uzgadniania tego z innymi klientami. Tak jak każdy algorytm ewentualnej zbieżńości, pozwala na tymczasową rozbieżność między replikami, ale po otrzymaniu wszystkich zmian przez każdego klienta, dane zawsze pozostają zbieżne. Przykładowymi algorytmami są RGA@article-replicated_abstract_data_types, WOOT@other-data_consistency_p2p_collaborative_editing oraz TreeDoc@other-commutative_replicated_data_type.
+Następcą Operational Transformation są bezkonfliktowe replikowane typy danych (Conflict-free replicated data types - CRDT). Pozwalają one na nanoszenie zmian na własne kopie przez klientów, bez potrzeby uzgadniania tego z innymi klientami. Tak jak każdy algorytm ewentualnej zbieżńości, pozwala na tymczasową rozbieżność między replikami, ale po otrzymaniu wszystkich zmian przez każdego klienta, dane zawsze pozostają zbieżne. Przykładowymi algorytmami są RGA@cite:replicated_abstract_data_types, WOOT@cite:data_consistency_p2p_collaborative_editing oraz TreeDoc@cite:commutative_replicated_data_type.
 
 // == Architektura Peer-to-Peer w środowiskach mobilnych
 // == Algorytmy synchronizacji tekstu

Thesis/main.typ

@@ -1,10 +1,8 @@
-#set text(lang: "pl")
 #import "style.typ": definition, example, theorem, zut-template
+#import "Bibliography.typ": bib-setup, render-bib
 
-#import "@preview/alexandria:0.2.2": *
-#show: alexandria(prefix: "book-", read: path => read(path))
-#show: alexandria(prefix: "article-", read: path => read(path))
-#show: alexandria(prefix: "other-", read: path => read(path))
+#set text(lang: "pl")
+#show: bib-setup
 
 #include "title_page.typ"
 #pagebreak(to: "odd")
@@ -16,4 +14,4 @@
   #include "Chapters/1. Theoretical Scope.typ"
 ])
 
-#include "Bibliography.typ"
+#render-bib()