refactor(docs): URL structure

14 files changed, 434 insertions, 0 deletions

diff --git a/subprojects/docs/src/learn/docker.md b/subprojects/docs/src/learn/docker.md
new file mode 100644
index 00000000..0df87da8
--- /dev/null
+++ b/subprojects/docs/src/learn/docker.md
@@ -0,0 +1,175 @@
+---
+SPDX-FileCopyrightText: 2024 The Refinery Authors
+SPDX-License-Identifier: EPL-2.0
+sidebar_position: 100
+sidebar_label: Docker
+---
+
+# Running in Docker
+
+:::note
+
+Refinery can run as a cloud-based _Graph Solver as a Service_ without local installation.
+If you're just looking to try Refinery, our [online demo](https://refinery.services/) provides a seamless experience without installation.
+
+:::
+
+:::info
+
+Installing Refinery as a Docker container can support more advanced use cases, such as when generating models with more resources or a longer timeout.
+
+:::
+
+To generate larger models with a longer timeout, you can use our [Docker container](https://github.com/graphs4value/refinery/pkgs/container/refinery) on either `amd64` or `arm64` machines:
+
+```shell
+docker run --rm -it -p 8888:8888 ghcr.io/graphs4value/refinery
+```
+
+Once Docker pulls and starts the container, you can navigate to http://localhost:8888 to open the model generation interface and start editing.
+
+Alternatively, you can follow the [instructions to set up a local development environment](/develop/contributing) and compile and run Refinery from source.
+
+## Updating
+
+To take advantage of the latest updates, you can simply re-pull our Docker container from the GitHub Container Registry:
+
+```shell
+docker pull ghcr.io/graphs4value/refinery
+```
+
+Restart the container to make sure that you're running the last pulled version.
+
+## Environmental variables
+
+The Docker container supports the following environmental variables to customize its behavior.
+Customizing these variable should only be needed if you want to _increase resource limits_ or _expose you Refinery instance over the network_ for others.
+
+Notes for **local-only instances** are highlighted with the :arrow_right: arrow emoji.
+
+Important security notices for **public instances** are highlighted with the :warning: warning emoji.
+
+### Networking
+
+#### `REFINERY_LISTEN_HOST`
+
+Hostname to listen at for incoming HTTP connections.
+
+**Default value:** `0.0.0.0` (accepts connections on any IP address)
+
+#### `REFINERY_LISTEN_PORT`
+
+TCP port to listen at for incoming HTTP connections.
+
+Refinery doesn't support HTTPS connections out of the box, so there's no point in setting this to `443`. Use a [reverse proxy](https://en.wikipedia.org/wiki/Reverse_proxy) instead if you wish to expose Refinery to encrypted connections.
+
+If you change this value, don't forget to adjust the `-p 8888:8888` option of the `docker run` command to [expose](https://docs.docker.com/reference/cli/docker/container/run/#publish) the selected port.
+
+**Default value:** `8888`
+
+#### `REFINERY_PUBLIC_HOST`
+
+Publicly visible hostname of the Refinery instance.
+
+:arrow_right: For installations only accessed locally (i.e., `localhost:8888`) without any reverse proxy, you can safely leave this empty.
+
+:warning: You should set this to the publicly visible hostname of your Refinery instance if you wish to expose Refinery over the network. Most likely, this will be the hostname of a reverse proxy that terminates TLS connections. Our online demo sets this to [refinery.services](https://refinery.services/).
+
+**Default value:** _empty_
+
+#### `REFINERY_PUBLIC_PORT`
+
+Publicly visible port of the Refinery instance.
+
+:arrow_right: For installations only accessed locally (i.e., `localhost:8888`), this value is ignored because `REFINERY_PUBLC_HOST` is not set.
+
+**Default value:** `443`
+
+#### `REFINERY_ALLOWED_ORIGINS`
+
+Comma-separated list of allowed origins for incoming WebSocket connections. If this variable is empty, all incoming WebSocket connections are accepted.
+
+:arrow_right: For installations only accessed locally (i.e., `localhost:8888`) without any reverse proxy, you can safely leave this empty.
+
+:warning: The value inferred from `REFINERY_PUBLIC_HOST` and `REFINERY_PUBLIC_PORT` should be suitable for instances exposed over the network. For security reasons, public instances should never leave this empty.
+
+**Default value:** equal to `REFINERY_PUBLIC_HOST:REFINERY_PUBLIC_PORT` if they are both set, _empty_ otherwise
+
+### Timeouts
+
+#### `REFINERY_SEMANTICS_TIMEOUT_MS`
+
+Timeout for partial model semantics calculation in milliseconds.
+
+:arrow_right: Increase this if you have a slower machine and the editor times out before showing a preview of your partial model in the _Graph_ or _Table_ views.
+
+:warning: Increasing this timeout may increase server load. Excessively large timeout may allow users to overload you server by entering extremely complex partial models.
+
+**Default value:** `1000`
+
+#### `REFINERY_SEMANTICS_WARMUP_TIMEOUT_MS`
+
+Timeout for partial model semantics calculation in milliseconds when the server first start.
+
+Due to various initialization tasks, the first partial model semantics generation may take longer the `REFINERY_SEMANTICS_TIMEOUT_MS` and display a timeout error. This setting increases the timeout for the first generation, leading to seamless use even after server start (especially in auto-scaling setups).
+
+**Default value:** equal to 2 × `REFINERY_SEMANTICS_TIMEOUT`
+
+#### `REFINERY_MODEL_GENERATION_TIMEOUT_SEC`
+
+Timeout for model generation in seconds.
+
+:arrow_right: Adjust this value if you're generating very large models (> 10000 nodes) and need more time to complete a generation. Note that some _unsatisfiable_ model generation problems cannot be detected by Refinery and will result in model generation running for an arbitrarily long time without producing any solution.
+
+:warning: Long running model generation will block a [_model generation thread_](#refinery_model_generation_thread_count). Try to balance the number of threads and the timeout to avoid exhausting system resources, but keep the wait time for a free model generation thread for users reasonably short. Auto-scaling to multiple instances may help with bursty demand.
+
+**Default value:** `600` (10 minutes)
+
+### Threading
+
+:warning: Excessively large values may overload the server. Make sure that _all_ Refinery threads can run at the same time to avoid thread starvation.
+
+#### `REFINERY_XTEXT_THREAD_COUNT`
+
+Number of threads used for non-blocking text editing operations. A value of `0` allows an _unlimited_ number of threads by running each semantics calculation in a new thread.
+
+:warning: Excessively large values may overload the server. Make sure that _all_ Refinery threads can run at the same time to avoid thread starvation.
+
+**Default value:** `1`
+
+#### `REFINERY_XTEXT_LOCKING_THREAD_COUNT`
+
+Number of threads used for text editing operations that lock the document. A value of `0` allows an _unlimited_ number of threads by running each semantics calculation in a new thread.
+
+
+**Default value:** equal to `REFINERY_XTEXT_THREAD_COUNT`
+
+#### `REFINERY_XTEXT_SEMANTICS_THREAD_COUNT`
+
+Number of threads used for model semantics calculation. A value of `0` allows an _unlimited_ number of threads by running each semantics calculation in a new thread.
+
+Must be at least as large as `REFINERY_XTEXT_THREAD_COUNT`.
+
+:warning: Excessively large values may overload the server. Make sure that _all_ Refinery threads can run at the same time to avoid thread starvation.
+
+**Default value:** equal to `REFINERY_XTEXT_THREAD_COUNT`
+
+#### `REFINERY_MODEL_GENERATION_THREAD_COUNT`
+
+Number of threads used for model semantics calculation. A value of `0` allows an _unlimited_ number of threads by running each semantics calculation in a new thread.
+
+:warning: Excessively large values may overload the server. Make sure that _all_ Refinery threads can run at the same time to avoid thread starvation. Each model generation task may also demand a large amount of memory in addition to CPU time.
+
+**Default value:** equal to `REFINERY_XTEXT_THREAD_COUNT`
+
+### Libraries
+
+#### `REFINERY_LIBRARY_PATH`
+
+Modules (`.refinery` files) in this directory or colon-separated list of directories will be exposed to user via Refinery's `import` mechanism.
+
+:arrow_right: Use this in conjunction with the [mount volume (-v)](https://docs.docker.com/reference/cli/docker/container/run/#volume) option of `docker run` to work with multi-file projects in Refinery.
+
+:warning: Make sure you only expose files that you want to make public. It's best to expose a directory that contains nothing other that `.refinery` files to minimize potential information leaks.
+
+**Default value:** _empty_ (no directories are exposed)
diff --git a/subprojects/docs/src/learn/index.md b/subprojects/docs/src/learn/index.md
new file mode 100644
index 00000000..bb28df57
--- /dev/null
+++ b/subprojects/docs/src/learn/index.md
@@ -0,0 +1,11 @@
+---
+SPDX-FileCopyrightText: 2024 The Refinery Authors
+SPDX-License-Identifier: EPL-2.0
+sidebar_position: 0
+---
+
+# Introduction
+
+Various software and systems engineering scenarios rely on the systematic construction of consistent graph models. However, **automatically generating a diverse set of consistent graph models** for complex domain specifications is challenging. First, the graph generation problem must be specified with mathematical precision. Moreover, graph generation is a computationally complex task, which necessitates specialized logic solvers.
+
+**Refinery is a novel open-source software framework** to automatically synthesize a diverse set of consistent domain-specific graph models. The framework offers an expressive high-level specification language using partial models to succinctly formulate a wide range of graph generation challenges. It also provides a modern cloud-based architecture for a scalable _Graph Solver as a Service,_ which uses logic reasoning rules to efficiently synthesize a diverse set of solutions to graph generation problems by partial model refinement. Applications include system-level architecture synthesis, test generation for modeling tools or traffic scenario synthesis for autonomous vehicles.
diff --git a/subprojects/docs/src/learn/language/_category_.yml b/subprojects/docs/src/learn/language/_category_.yml
new file mode 100644
index 00000000..f5a6f896
--- /dev/null
+++ b/subprojects/docs/src/learn/language/_category_.yml
@@ -0,0 +1,10 @@
+# SPDX-FileCopyrightText: 2024 The Refinery Authors
+#
+# SPDX-License-Identifier: EPL-2.0
+
+position: 2
+label: Language reference
+link:
+  type: generated-index
+  slug: /language
+  description: Learn more about the Refinery partial modeling language!
diff --git a/subprojects/docs/src/learn/language/classes.md b/subprojects/docs/src/learn/language/classes.md
new file mode 100644
index 00000000..7278dc35
--- /dev/null
+++ b/subprojects/docs/src/learn/language/classes.md
@@ -0,0 +1,14 @@
+---
+SPDX-FileCopyrightText: 2024 The Refinery Authors
+SPDX-License-Identifier: EPL-2.0
+description: Metamodeling in Refinery
+sidebar_position: 0
+---
+
+# Classes and references
+
+:::warning
+
+Under construction
+
+:::
diff --git a/subprojects/docs/src/learn/tutorials/_category_.yml b/subprojects/docs/src/learn/tutorials/_category_.yml
new file mode 100644
index 00000000..adf8293f
--- /dev/null
+++ b/subprojects/docs/src/learn/tutorials/_category_.yml
@@ -0,0 +1,11 @@
+# SPDX-FileCopyrightText: 2024 The Refinery Authors
+#
+# SPDX-License-Identifier: EPL-2.0
+
+position: 1
+label: Tutorials
+link:
+  type: generated-index
+  slug: /tutorials
+  title: Tutorial overview
+  description: Try Refinery in practical partial modeling challenges!
diff --git a/subprojects/docs/src/learn/tutorials/file-system/fig1.png b/subprojects/docs/src/learn/tutorials/file-system/fig1.png
new file mode 100644
index 00000000..da30af3c
--- /dev/null
+++ b/subprojects/docs/src/learn/tutorials/file-system/fig1.png
diff --git a/subprojects/docs/src/learn/tutorials/file-system/fig1.png.license b/subprojects/docs/src/learn/tutorials/file-system/fig1.png.license
new file mode 100644
index 00000000..ff75bc7c
--- /dev/null
+++ b/subprojects/docs/src/learn/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/learn/tutorials/file-system/fig2.png b/subprojects/docs/src/learn/tutorials/file-system/fig2.png
new file mode 100644
index 00000000..f42e3d3e
--- /dev/null
+++ b/subprojects/docs/src/learn/tutorials/file-system/fig2.png
diff --git a/subprojects/docs/src/learn/tutorials/file-system/fig2.png.license b/subprojects/docs/src/learn/tutorials/file-system/fig2.png.license
new file mode 100644
index 00000000..ff75bc7c
--- /dev/null
+++ b/subprojects/docs/src/learn/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/learn/tutorials/file-system/fig3.png b/subprojects/docs/src/learn/tutorials/file-system/fig3.png
new file mode 100644
index 00000000..9506417a
--- /dev/null
+++ b/subprojects/docs/src/learn/tutorials/file-system/fig3.png
diff --git a/subprojects/docs/src/learn/tutorials/file-system/fig3.png.license b/subprojects/docs/src/learn/tutorials/file-system/fig3.png.license
new file mode 100644
index 00000000..ff75bc7c
--- /dev/null
+++ b/subprojects/docs/src/learn/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/learn/tutorials/file-system/fig4.png b/subprojects/docs/src/learn/tutorials/file-system/fig4.png
new file mode 100644
index 00000000..cc012f24
--- /dev/null
+++ b/subprojects/docs/src/learn/tutorials/file-system/fig4.png
diff --git a/subprojects/docs/src/learn/tutorials/file-system/fig4.png.license b/subprojects/docs/src/learn/tutorials/file-system/fig4.png.license
new file mode 100644
index 00000000..ff75bc7c
--- /dev/null
+++ b/subprojects/docs/src/learn/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/learn/tutorials/file-system/index.md b/subprojects/docs/src/learn/tutorials/file-system/index.md
new file mode 100644
index 00000000..1d15512f
--- /dev/null
+++ b/subprojects/docs/src/learn/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..*.
+```