make mmath a directory

diff --git a/bandali-mmath.txt b/bandali-mmath.txt
deleted file mode 100644 (file)
index ebca8b6..0000000
--- a/bandali-mmath.txt
+++ /dev/null
@@ -1,105 +0,0 @@
-bandali's master of mathematics
--------------------------------
-
-I graduated from the University of Waterloo with the degree of Master
-of Mathematics in Computer Science in Spring 2020.  My research at the
-Waterloo Formal Methods group focused on formal logic, model checking,
-and verification; under supervision of Prof. Nancy Day.
-
-
-       A Comprehensive Study of Declarative Modelling Languages
-
-THESIS
-
-  Reference version:
-    - https://p.bndl.org/bandali-mmath-thesis.pdf
-  LaTeX sources:
-    - https://p.bndl.org/bandali-mmath-thesis.tar.gz
-    - https://p.bndl.org/bandali-mmath-thesis.zip
-
-  Abstract:
-
-    Declarative behavioural modelling is a powerful modelling paradigm
-    that enables users to model system functionality abstractly and
-    formally.  An abstract model is a concise and compact
-    representation of key characteristics of a system, and enables the
-    stakeholders to reason about the correctness of the system in the
-    early stages of development.
-
-    There are many different declarative languages and they have
-    greatly varying constructs for representing a transition system,
-    and they sometimes differ in rather subtle ways.  In this thesis,
-    we compare seven formal declarative modelling languages B,
-    Event-B, Alloy, Dash, TLA+, PlusCal, and AsmetaL on several
-    criteria.  We classify these criteria under three main categories:
-    structuring transition systems (control modelling), data
-    descriptions in transition systems (data modelling), and
-    modularity aspects of modelling.  We developed this comparison by
-    completing a set of case studies across the data-
-    vs. control-oriented spectrum in all of the above languages.
-
-    Structurally, a transition system is comprised of a snapshot
-    declaration and snapshot space, initialization, and a transition
-    relation, which is potentially composed of individual transitions.
-    We meticulously outline the differences between the languages with
-    respect to how the modeller would express each of the above
-    components of a transition system in each language, and include
-    discussions regarding stuttering and inconsistencies in the
-    transition relation.  Data-related aspects of a formal model
-    include use of basic and composite datatypes, well-formedness and
-    typechecking, and separation of name spaces with respect to global
-    and local variables.  Modularity criteria includes subtransition
-    systems and data decomposition.  We employ a series of small and
-    concise exemplars we have devised to highlight these differences
-    in each language.  To help modellers answer the important question
-    of which declarative modelling language may be most suited for
-    modelling their system, we present recommendations based on our
-    observations about the differentiating characteristics of each of
-    these languages.
-
-  License:
-
-    This thesis is free software: you can redistribute it and/or
-    modify it under the terms of the GNU General Public License as
-    published by the Free Software Foundation, either version 3 of
-    the License, or (at your option) any later version.
-
-    This thesis is distributed in the hope that it will be useful,
-    but WITHOUT ANY WARRANTY; without even the implied warranty of
-    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
-    GNU General Public License for more details.
-
-    You should have received a copy of the GNU General Public License
-    along with this thesis.  If not, see
-    <https://www.gnu.org/licenses/>.
-
-  A copy of the GNU General Public License is available from the
-  COPYING file included in both of the LaTeX source archives linked
-  above.
-
-PRESENTATION
-
-  Reference version: (coming soon)
-  LaTeX sources: (coming soon)
-
-  This is the presentation I delivered to my supervisor and the second
-  readers of my thesis on Jun 30, 2020, as announced on the Cheriton
-  School of Computer Science website:
-
-  https://cs.uwaterloo.ca/events/masters-thesis-presentation-formal-methods-comprehensive-study-declarative-modelling-languages
-
-MODELS
-
-  Reference version: (coming soon)
-
-
-                                 -*-
-
-Copyright (c) 2020 bandali
-
-Copying and distribution of this file, with or without modification,
-are permitted in any medium without royalty provided the copyright
-notice and this notice are preserved.  This file is offered as-is,
-without any warranty.
-
-plain text: https://bndl.org/bandali-mmath.txt

diff --git a/mmath.html b/mmath.html
deleted file mode 100644 (file)
index b9dcbea..0000000
--- a/mmath.html
+++ /dev/null
@@ -1,144 +0,0 @@
-<!doctype html><html lang="en"><head>
-<meta charset="utf-8" />
-<meta name="author" content="bandali" />
-<meta name="viewport" content="width=device-width, initial-scale=1" />
-<title>master of mathematics &mdash; bandali</title>
-<link rel="icon" href="data:,">
-<link rel="canonical" href="https://bndl.org/mmath" />
-<link rel="alternate" href="bandali-mmath.txt" title="plain text" type="text/plain" />
-<style>
-body{line-height:1.6;padding:0 2em;}p,details{max-width:37.5em}
-.box{background:#f8f8f8;border:1px solid #e6e6e6;border-radius:4px;
-font-size:0.95em;padding:0.6em 0.9em;}
-details{margin:1em 0}details summary{cursor:pointer}
-blockquote{text-align:justify}
-.tex{font-family:"Tex Gyre Termes",serif;text-transform:uppercase;}
-.tex span{font-size:0.75em;margin-left:-0.05em;margin-right:-0.20em;}
-.tex sub{font-size:1em;margin-left:-0.1667em;margin-right:-0.125em;
-vertical-align:-0.5ex;}.tex sup{font-size:0.85em;margin-left:-0.36em;
-margin-right:-0.15em;vertical-align:0.15em;}
-#copy,#license{font-size:0.84em;line-height:1.3;}
-#copy{margin-bottom:0.5em}#license{margin-top:0.5em}
-@media(prefers-color-scheme:dark){body{background:#1c1c1c;color:white;}
-a:link{color:#acdeff}a:visited{color:#f8f}a:active{color:#e00}
-.box{background:#1b1d1e;border-color:#373c34;}}
-</style></head>
-<body>
-<h1><a href=".">bandali</a>'s master of mathematics</h1>
-
-<p>I graduated from the University of Waterloo with the degree of
-Master of Mathematics in Computer Science in Spring 2020.
-My research at
-the <a href="https://watform.uwaterloo.ca">Waterloo Formal Methods</a>
-group focused on formal logic, model checking, and verification; under
-supervision
-of <a href="https://cs.uwaterloo.ca/~nday/">Prof. Nancy Day</a>.</p>
-
-
-<h2>A Comprehensive Study of Declarative Modelling Languages</h2>
-
-<p><em>Jump to:</em>
-<a href="#thesis">thesis</a> |
-<a href="#presentation">presentation</a> |
-<a href="#models">models</a></p>
-
-<h3 id="thesis">Thesis</h3>
-
-<p>Reference version:
-<a href="https://p.bndl.org/bandali-mmath-thesis.pdf">pdf</a> |
-<a href="bandali.bib">bib</a><br />
-
-<span class="tex">L<sup>a</sup>T<sub>e</sub>X</span> sources:
-<a href="https://p.bndl.org/bandali-mmath-thesis.tar.gz">tar.gz</a> |
-<a href="https://p.bndl.org/bandali-mmath-thesis.zip">zip</a></p>
-
-<details class="box">
-<summary>Abstract</summary>
-<blockquote>
-<p>Declarative behavioural modelling is a powerful modelling paradigm
-that enables users to model system functionality abstractly and
-formally.  An abstract model is a concise and compact representation
-of key characteristics of a system, and enables the stakeholders to
-reason about the correctness of the system in the early stages of
-development.</p>
-
-<p>There are many different declarative languages and they have
-greatly varying constructs for representing a transition system, and
-they sometimes differ in rather subtle ways.  In this thesis, we
-compare seven formal declarative modelling languages B, Event-B,
-Alloy, Dash, TLA<sup>+</sup>, PlusCal, and AsmetaL on several
-criteria.  We classify these criteria under three main categories:
-structuring transition systems (control modelling), data descriptions
-in transition systems (data modelling), and modularity aspects of
-modelling.  We developed this comparison by completing a set of case
-studies across the data- vs. control-oriented spectrum in all of the
-above languages.</p>
-
-<p>Structurally, a transition system is comprised of a snapshot
-declaration and snapshot space, initialization, and a transition
-relation, which is potentially composed of individual transitions.
-We meticulously outline the differences between the languages with
-respect to how the modeller would express each of the above components
-of a transition system in each language, and include discussions
-regarding stuttering and inconsistencies in the transition relation.
-Data-related aspects of a formal model include use of basic and
-composite datatypes, well-formedness and typechecking, and separation
-of name spaces with respect to global and local variables.  Modularity
-criteria includes subtransition systems and data decomposition.
-We employ a series of small and concise exemplars we have devised to
-highlight these differences in each language.  To help modellers
-answer the important question of which declarative modelling language
-may be most suited for modelling their system, we present
-recommendations based on our observations about the differentiating
-characteristics of each of these languages.</p>
-</blockquote>
-</details>
-
-<details class="box" open>
-<summary>License</summary>
-<pre>
-This thesis is free software: you can redistribute it and/or modify
-it under the terms of the GNU General Public License as published by
-the Free Software Foundation, either version 3 of the License, or
-(at your option) any later version.
-
-This thesis is distributed in the hope that it will be useful,
-but WITHOUT ANY WARRANTY; without even the implied warranty of
-MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
-GNU General Public License for more details.
-
-You should have received a copy of the GNU General Public License
-along with this thesis.  If not, see &lt;<a href="https://www.gnu.org/licenses/">https://www.gnu.org/licenses/</a>&gt;.
-</pre>
-</details>
-
-<p>A copy of the GNU General Public License is available from the
-COPYING file included in both of
-the <span class="tex">L<sup>a</sup>T<sub>e</sub>X</span> source
-archives linked above.</p>
-
-<h3 id="presentation">Presentation</h3>
-
-<p>Reference version:
-pdf (coming soon)<br />
-<span class="tex">L<sup>a</sup>T<sub>e</sub>X</span> sources:
-tar.gz | zip (coming soon)</p>
-
-<p>This is the presentation I delivered to my supervisor and the
-second readers of my thesis on Jun 30, 2020, as
-<a href="https://cs.uwaterloo.ca/events/masters-thesis-presentation-formal-methods-comprehensive-study-declarative-modelling-languages">announced</a>
-on the Cheriton School of Computer Science website.</p>
-
-<h3 id="models">Models</h3>
-
-<p>Reference version:
-tar.gz | zip (coming soon)</p>
-
-<hr />
-<p id="copy">Copyright &copy; 2020 bandali</p>
-<p id="license">Copying and distribution of this file, with or without
-modification, are permitted in any medium without royalty provided the
-copyright notice and this notice are preserved.  This file is offered
-as-is, without any warranty.</p>
-</body>
-</html>

diff --git a/mmath/bandali-mmath.txt b/mmath/bandali-mmath.txt
new file mode 100644 (file)
index 0000000..ebca8b6
--- /dev/null
+++ b/mmath/bandali-mmath.txt
@@ -0,0 +1,105 @@
+bandali's master of mathematics
+-------------------------------
+
+I graduated from the University of Waterloo with the degree of Master
+of Mathematics in Computer Science in Spring 2020.  My research at the
+Waterloo Formal Methods group focused on formal logic, model checking,
+and verification; under supervision of Prof. Nancy Day.
+
+
+       A Comprehensive Study of Declarative Modelling Languages
+
+THESIS
+
+  Reference version:
+    - https://p.bndl.org/bandali-mmath-thesis.pdf
+  LaTeX sources:
+    - https://p.bndl.org/bandali-mmath-thesis.tar.gz
+    - https://p.bndl.org/bandali-mmath-thesis.zip
+
+  Abstract:
+
+    Declarative behavioural modelling is a powerful modelling paradigm
+    that enables users to model system functionality abstractly and
+    formally.  An abstract model is a concise and compact
+    representation of key characteristics of a system, and enables the
+    stakeholders to reason about the correctness of the system in the
+    early stages of development.
+
+    There are many different declarative languages and they have
+    greatly varying constructs for representing a transition system,
+    and they sometimes differ in rather subtle ways.  In this thesis,
+    we compare seven formal declarative modelling languages B,
+    Event-B, Alloy, Dash, TLA+, PlusCal, and AsmetaL on several
+    criteria.  We classify these criteria under three main categories:
+    structuring transition systems (control modelling), data
+    descriptions in transition systems (data modelling), and
+    modularity aspects of modelling.  We developed this comparison by
+    completing a set of case studies across the data-
+    vs. control-oriented spectrum in all of the above languages.
+
+    Structurally, a transition system is comprised of a snapshot
+    declaration and snapshot space, initialization, and a transition
+    relation, which is potentially composed of individual transitions.
+    We meticulously outline the differences between the languages with
+    respect to how the modeller would express each of the above
+    components of a transition system in each language, and include
+    discussions regarding stuttering and inconsistencies in the
+    transition relation.  Data-related aspects of a formal model
+    include use of basic and composite datatypes, well-formedness and
+    typechecking, and separation of name spaces with respect to global
+    and local variables.  Modularity criteria includes subtransition
+    systems and data decomposition.  We employ a series of small and
+    concise exemplars we have devised to highlight these differences
+    in each language.  To help modellers answer the important question
+    of which declarative modelling language may be most suited for
+    modelling their system, we present recommendations based on our
+    observations about the differentiating characteristics of each of
+    these languages.
+
+  License:
+
+    This thesis is free software: you can redistribute it and/or
+    modify it under the terms of the GNU General Public License as
+    published by the Free Software Foundation, either version 3 of
+    the License, or (at your option) any later version.
+
+    This thesis is distributed in the hope that it will be useful,
+    but WITHOUT ANY WARRANTY; without even the implied warranty of
+    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+    GNU General Public License for more details.
+
+    You should have received a copy of the GNU General Public License
+    along with this thesis.  If not, see
+    <https://www.gnu.org/licenses/>.
+
+  A copy of the GNU General Public License is available from the
+  COPYING file included in both of the LaTeX source archives linked
+  above.
+
+PRESENTATION
+
+  Reference version: (coming soon)
+  LaTeX sources: (coming soon)
+
+  This is the presentation I delivered to my supervisor and the second
+  readers of my thesis on Jun 30, 2020, as announced on the Cheriton
+  School of Computer Science website:
+
+  https://cs.uwaterloo.ca/events/masters-thesis-presentation-formal-methods-comprehensive-study-declarative-modelling-languages
+
+MODELS
+
+  Reference version: (coming soon)
+
+
+                                 -*-
+
+Copyright (c) 2020 bandali
+
+Copying and distribution of this file, with or without modification,
+are permitted in any medium without royalty provided the copyright
+notice and this notice are preserved.  This file is offered as-is,
+without any warranty.
+
+plain text: https://bndl.org/bandali-mmath.txt

diff --git a/mmath/index.html b/mmath/index.html
new file mode 100644 (file)
index 0000000..b9dcbea
--- /dev/null
+++ b/mmath/index.html
@@ -0,0 +1,144 @@
+<!doctype html><html lang="en"><head>
+<meta charset="utf-8" />
+<meta name="author" content="bandali" />
+<meta name="viewport" content="width=device-width, initial-scale=1" />
+<title>master of mathematics &mdash; bandali</title>
+<link rel="icon" href="data:,">
+<link rel="canonical" href="https://bndl.org/mmath" />
+<link rel="alternate" href="bandali-mmath.txt" title="plain text" type="text/plain" />
+<style>
+body{line-height:1.6;padding:0 2em;}p,details{max-width:37.5em}
+.box{background:#f8f8f8;border:1px solid #e6e6e6;border-radius:4px;
+font-size:0.95em;padding:0.6em 0.9em;}
+details{margin:1em 0}details summary{cursor:pointer}
+blockquote{text-align:justify}
+.tex{font-family:"Tex Gyre Termes",serif;text-transform:uppercase;}
+.tex span{font-size:0.75em;margin-left:-0.05em;margin-right:-0.20em;}
+.tex sub{font-size:1em;margin-left:-0.1667em;margin-right:-0.125em;
+vertical-align:-0.5ex;}.tex sup{font-size:0.85em;margin-left:-0.36em;
+margin-right:-0.15em;vertical-align:0.15em;}
+#copy,#license{font-size:0.84em;line-height:1.3;}
+#copy{margin-bottom:0.5em}#license{margin-top:0.5em}
+@media(prefers-color-scheme:dark){body{background:#1c1c1c;color:white;}
+a:link{color:#acdeff}a:visited{color:#f8f}a:active{color:#e00}
+.box{background:#1b1d1e;border-color:#373c34;}}
+</style></head>
+<body>
+<h1><a href=".">bandali</a>'s master of mathematics</h1>
+
+<p>I graduated from the University of Waterloo with the degree of
+Master of Mathematics in Computer Science in Spring 2020.
+My research at
+the <a href="https://watform.uwaterloo.ca">Waterloo Formal Methods</a>
+group focused on formal logic, model checking, and verification; under
+supervision
+of <a href="https://cs.uwaterloo.ca/~nday/">Prof. Nancy Day</a>.</p>
+
+
+<h2>A Comprehensive Study of Declarative Modelling Languages</h2>
+
+<p><em>Jump to:</em>
+<a href="#thesis">thesis</a> |
+<a href="#presentation">presentation</a> |
+<a href="#models">models</a></p>
+
+<h3 id="thesis">Thesis</h3>
+
+<p>Reference version:
+<a href="https://p.bndl.org/bandali-mmath-thesis.pdf">pdf</a> |
+<a href="bandali.bib">bib</a><br />
+
+<span class="tex">L<sup>a</sup>T<sub>e</sub>X</span> sources:
+<a href="https://p.bndl.org/bandali-mmath-thesis.tar.gz">tar.gz</a> |
+<a href="https://p.bndl.org/bandali-mmath-thesis.zip">zip</a></p>
+
+<details class="box">
+<summary>Abstract</summary>
+<blockquote>
+<p>Declarative behavioural modelling is a powerful modelling paradigm
+that enables users to model system functionality abstractly and
+formally.  An abstract model is a concise and compact representation
+of key characteristics of a system, and enables the stakeholders to
+reason about the correctness of the system in the early stages of
+development.</p>
+
+<p>There are many different declarative languages and they have
+greatly varying constructs for representing a transition system, and
+they sometimes differ in rather subtle ways.  In this thesis, we
+compare seven formal declarative modelling languages B, Event-B,
+Alloy, Dash, TLA<sup>+</sup>, PlusCal, and AsmetaL on several
+criteria.  We classify these criteria under three main categories:
+structuring transition systems (control modelling), data descriptions
+in transition systems (data modelling), and modularity aspects of
+modelling.  We developed this comparison by completing a set of case
+studies across the data- vs. control-oriented spectrum in all of the
+above languages.</p>
+
+<p>Structurally, a transition system is comprised of a snapshot
+declaration and snapshot space, initialization, and a transition
+relation, which is potentially composed of individual transitions.
+We meticulously outline the differences between the languages with
+respect to how the modeller would express each of the above components
+of a transition system in each language, and include discussions
+regarding stuttering and inconsistencies in the transition relation.
+Data-related aspects of a formal model include use of basic and
+composite datatypes, well-formedness and typechecking, and separation
+of name spaces with respect to global and local variables.  Modularity
+criteria includes subtransition systems and data decomposition.
+We employ a series of small and concise exemplars we have devised to
+highlight these differences in each language.  To help modellers
+answer the important question of which declarative modelling language
+may be most suited for modelling their system, we present
+recommendations based on our observations about the differentiating
+characteristics of each of these languages.</p>
+</blockquote>
+</details>
+
+<details class="box" open>
+<summary>License</summary>
+<pre>
+This thesis is free software: you can redistribute it and/or modify
+it under the terms of the GNU General Public License as published by
+the Free Software Foundation, either version 3 of the License, or
+(at your option) any later version.
+
+This thesis is distributed in the hope that it will be useful,
+but WITHOUT ANY WARRANTY; without even the implied warranty of
+MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+GNU General Public License for more details.
+
+You should have received a copy of the GNU General Public License
+along with this thesis.  If not, see &lt;<a href="https://www.gnu.org/licenses/">https://www.gnu.org/licenses/</a>&gt;.
+</pre>
+</details>
+
+<p>A copy of the GNU General Public License is available from the
+COPYING file included in both of
+the <span class="tex">L<sup>a</sup>T<sub>e</sub>X</span> source
+archives linked above.</p>
+
+<h3 id="presentation">Presentation</h3>
+
+<p>Reference version:
+pdf (coming soon)<br />
+<span class="tex">L<sup>a</sup>T<sub>e</sub>X</span> sources:
+tar.gz | zip (coming soon)</p>
+
+<p>This is the presentation I delivered to my supervisor and the
+second readers of my thesis on Jun 30, 2020, as
+<a href="https://cs.uwaterloo.ca/events/masters-thesis-presentation-formal-methods-comprehensive-study-declarative-modelling-languages">announced</a>
+on the Cheriton School of Computer Science website.</p>
+
+<h3 id="models">Models</h3>
+
+<p>Reference version:
+tar.gz | zip (coming soon)</p>
+
+<hr />
+<p id="copy">Copyright &copy; 2020 bandali</p>
+<p id="license">Copying and distribution of this file, with or without
+modification, are permitted in any medium without royalty provided the
+copyright notice and this notice are preserved.  This file is offered
+as-is, without any warranty.</p>
+</body>
+</html>