docs: add existing tutorial

Add tutorial from https://github.com/graphs4value/refinery-tutorials

11 files changed, 221 insertions, 10 deletions

diff --git a/subprojects/docs/src/css/custom.css b/subprojects/docs/src/css/custom.css
index 9b839f53..82c0c972 100644
--- a/subprojects/docs/src/css/custom.css
+++ b/subprojects/docs/src/css/custom.css
@@ -16,7 +16,7 @@
     'Helvetica',
     'Arial',
     sans-serif;
-  --ifm-fony-family-monospace: 'JetBrains Mono Variable',
+  --ifm-font-family-monospace: 'JetBrains Mono Variable',
     'JetBrains Mono',
     'Cascadia Code',
     'Fira Code',
@@ -74,6 +74,13 @@ code {
   font-variation-settings: 'wdth' 87.5;
 }
 
+.button--play::before {
+  content: '▶';
+  display: inline-block;
+  transform: translatey(-0.1em);
+  padding-right: 1ch;
+}
+
 .button, .navbar__link {
   font-weight: 600;
 }
diff --git a/subprojects/docs/src/docs/tutorials/file-system.md b/subprojects/docs/src/docs/tutorials/file-system.md
deleted file mode 100644
index aed1cd87..00000000
--- a/subprojects/docs/src/docs/tutorials/file-system.md
+++ /dev/null
@@ -1,9 +0,0 @@
----
-SPDX-FileCopyrightText: 2023-2024 The Refinery Authors
-SPDX-License-Identifier: EPL-2.0
-description: Introduction to classes, references, and error predicates
-sidebar_position: 0
-sidebar_label: File system
----
-
-# File system tutorial
diff --git a/subprojects/docs/src/docs/tutorials/file-system/fig1.png b/subprojects/docs/src/docs/tutorials/file-system/fig1.png
new file mode 100644
index 00000000..da30af3c
--- /dev/null
+++ b/subprojects/docs/src/docs/tutorials/file-system/fig1.png
diff --git a/subprojects/docs/src/docs/tutorials/file-system/fig1.png.license b/subprojects/docs/src/docs/tutorials/file-system/fig1.png.license
new file mode 100644
index 00000000..ff75bc7c
--- /dev/null
+++ b/subprojects/docs/src/docs/tutorials/file-system/fig1.png.license
@@ -0,0 +1,3 @@
+SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+
+SPDX-License-Identifier: EPL-2.0
diff --git a/subprojects/docs/src/docs/tutorials/file-system/fig2.png b/subprojects/docs/src/docs/tutorials/file-system/fig2.png
new file mode 100644
index 00000000..f42e3d3e
--- /dev/null
+++ b/subprojects/docs/src/docs/tutorials/file-system/fig2.png
diff --git a/subprojects/docs/src/docs/tutorials/file-system/fig2.png.license b/subprojects/docs/src/docs/tutorials/file-system/fig2.png.license
new file mode 100644
index 00000000..ff75bc7c
--- /dev/null
+++ b/subprojects/docs/src/docs/tutorials/file-system/fig2.png.license
@@ -0,0 +1,3 @@
+SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+
+SPDX-License-Identifier: EPL-2.0
diff --git a/subprojects/docs/src/docs/tutorials/file-system/fig3.png b/subprojects/docs/src/docs/tutorials/file-system/fig3.png
new file mode 100644
index 00000000..9506417a
--- /dev/null
+++ b/subprojects/docs/src/docs/tutorials/file-system/fig3.png
diff --git a/subprojects/docs/src/docs/tutorials/file-system/fig3.png.license b/subprojects/docs/src/docs/tutorials/file-system/fig3.png.license
new file mode 100644
index 00000000..ff75bc7c
--- /dev/null
+++ b/subprojects/docs/src/docs/tutorials/file-system/fig3.png.license
@@ -0,0 +1,3 @@
+SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+
+SPDX-License-Identifier: EPL-2.0
diff --git a/subprojects/docs/src/docs/tutorials/file-system/fig4.png b/subprojects/docs/src/docs/tutorials/file-system/fig4.png
new file mode 100644
index 00000000..cc012f24
--- /dev/null
+++ b/subprojects/docs/src/docs/tutorials/file-system/fig4.png
diff --git a/subprojects/docs/src/docs/tutorials/file-system/fig4.png.license b/subprojects/docs/src/docs/tutorials/file-system/fig4.png.license
new file mode 100644
index 00000000..ff75bc7c
--- /dev/null
+++ b/subprojects/docs/src/docs/tutorials/file-system/fig4.png.license
@@ -0,0 +1,3 @@
+SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+
+SPDX-License-Identifier: EPL-2.0
diff --git a/subprojects/docs/src/docs/tutorials/file-system/index.md b/subprojects/docs/src/docs/tutorials/file-system/index.md
new file mode 100644
index 00000000..1d15512f
--- /dev/null
+++ b/subprojects/docs/src/docs/tutorials/file-system/index.md
@@ -0,0 +1,201 @@
+---
+SPDX-FileCopyrightText: 2023-2024 The Refinery Authors
+SPDX-License-Identifier: EPL-2.0
+description: Introduction to classes, references, and error predicates
+sidebar_position: 0
+sidebar_label: File system
+---
+
+# File system tutorial
+
+The goal of this tutorial is to give a brief overview of the partial modeling and model generation features of the Refinery framework. The running example will be the modeling of files, directories, and repositories.
+
+## Partial models
+
+### Types and relations
+
+- First, let us introduce some basic types: `Dir`, `File`, and `FileSystem`, along with the relations between them: `element` and `root`. There is a `scope` expression at the end, which we will ignore for now.
+
+```refinery
+class FileSystem {
+    contains File[1] root
+}
+
+class File.
+
+class Dir extends File {
+    contains File[] element
+}
+
+scope node = 10.
+```
+
+import Link from '@docusaurus/Link';
+
+<p>
+  <Link
+    href="https://refinery.services/#/1/KLUv_SDT_QMAQkcXGnBL2-ikxOa10ZNeN1bwnxijfsojpwHQAxAE5pzBk5uCd8F5EjAGJrUNQBWIbdRU7tkRB-VsG_aVuMlSEWzzTShXE8h-eBHzK_cK11NoD9P_2_GFrS61RRmuipYUCwA046ljtvEqgDAGQyDQwsIqKACEt2LiANXAaUxBAQ=="
+    className="button button--lg button--primary button--play"
+  >Try in Refinery</Link>
+</p>
+
+- Notice that the syntax is essentially identical to [Xcore](https://wiki.eclipse.org/Xcore).
+- Review the partial model visualization. You should get something like this:
+
+![Initial model](fig1.png)
+
+- Add some statements about a partial model:
+
+```refinery
+class FileSystem {
+    contains File[1] root
+}
+
+class File.
+
+class Dir extends File {
+    contains File[] element
+}
+
+Dir(resources).
+element(resources, img).
+File(img).
+
+scope node = 10.
+```
+
+![Partial model extended with new facts](fig2.png)
+
+### Partial models
+
+- Notice that the instance model elements are coexisting with ```<type>::new``` nodes representing the prototypes of newly created objects.
+
+- Check the disabled `equals` and `exist` predicates. check the visual annotation of those predicates in the visualization (dashed line, shadow).
+
+![Object existence and equality](fig3.png)
+
+### Information merging
+
+- For the object `img`, we didn't specify if it is a directory or not. Therefore, it will typically be a folder.
+
+- If we want to state that img is not a directory, we need to a negative statement:
+
+```refinery
+!Dir(img).
+```
+
+- Statements are merged with respect to the refinement relation of 4-valued logic.
+
+- If we add, a statement both negatively and positively, it will create an inconsistency:
+
+```refinery
+element(resources, img).
+!element(resources, img).
+```
+
+- Inconsistent models parts in a partial model typically make the problem trivially unsatisfiable.
+
+![Inconsistent partial model](fig4.png)
+
+- However, the model can be saved if the inconsistent part may not exist...
+
+```refinery
+!File(File::new).
+```
+
+### Default values
+
+- A large amount of statements can be expressed by using `*`.
+- The `default` keyword defines lower priority statements that need to be considered unless other statement specifies otherwise. No information merging is happening.
+
+## Constraints
+
+Let's extend the metamodel with a new class `SymLink`:
+
+```refinery
+class FileSystem {
+    contains File[1] root
+}
+
+class File.
+
+class Dir extends File {
+    contains File[0..10] element
+}
+
+class SymLink extends File {
+    File[1] target
+}
+
+Dir(resources).
+element(resources, img).
+element(resources, link).
+target(link, img).
+
+scope node = 10.
+```
+
+- Add some simple constraints:
+
+```refinery
+% Simple constraints:
+pred hasReference(f) <-> target(_, f).
+error pred selfLoop(s) <-> target(s, s).
+target(x,x).
+```
+
+- There are no empty directories in a git repository, so let's forbid them!
+
+```refinery
+error pred emptyDir(d) <-> Dir(d), !element(d,_).
+```
+
+- End result:
+
+```refinery
+class FileSystem {
+    contains File[1] root
+}
+
+class File.
+
+class Dir extends File {
+    contains File[0..10] element
+}
+
+class SymLink extends File {
+    File[1] target
+}
+
+Dir(resources).
+element(resources, img).
+!Dir(img).
+element(resources, link).
+target(link,img).
+
+% Simple constraints:
+pred hasReference(f) <-> target(_, f).
+error pred selfLoop(s) <-> target(s, s).
+
+% Object equality with ==:
+error pred emptyDir(d) <-> Dir(d), !element(d, _).
+pred importantFile(f) <-> target(l1, f), target(l2, f), l1 != l2.
+
+% Transitive closure, and
+pred containsFile(fs, file) <->
+    FileSystem(fs),
+    root(fs, file)
+;
+    FileSystem(fs),
+    root(fs, rootDir),
+    element+(rootDir, file).
+
+% Predicate reuse
+error conflictBetweenTwoFileSystem(fs1, fs2, l, t) <->
+    containsFile(fs1, l),
+    containsFile(fs2, t),
+    fs1 != fs2,
+    target(l, t).
+
+scope node = 40..50, FileSystem = 2, importantFile = 1..*.
+```