From b44c06a901f8ead3ecaf3eaf2fa9868be7525ebe Mon Sep 17 00:00:00 2001 From: Kristóf Marussy Date: Tue, 9 Apr 2024 18:12:17 +0200 Subject: docs: add existing tutorial Add tutorial from https://github.com/graphs4value/refinery-tutorials --- subprojects/docs/src/css/custom.css | 9 +- subprojects/docs/src/docs/tutorials/file-system.md | 9 - .../docs/src/docs/tutorials/file-system/fig1.png | Bin 0 -> 20110 bytes .../docs/tutorials/file-system/fig1.png.license | 3 + .../docs/src/docs/tutorials/file-system/fig2.png | Bin 0 -> 44020 bytes .../docs/tutorials/file-system/fig2.png.license | 3 + .../docs/src/docs/tutorials/file-system/fig3.png | Bin 0 -> 26950 bytes .../docs/tutorials/file-system/fig3.png.license | 3 + .../docs/src/docs/tutorials/file-system/fig4.png | Bin 0 -> 38143 bytes .../docs/tutorials/file-system/fig4.png.license | 3 + .../docs/src/docs/tutorials/file-system/index.md | 201 +++++++++++++++++++++ 11 files changed, 221 insertions(+), 10 deletions(-) delete mode 100644 subprojects/docs/src/docs/tutorials/file-system.md create mode 100644 subprojects/docs/src/docs/tutorials/file-system/fig1.png create mode 100644 subprojects/docs/src/docs/tutorials/file-system/fig1.png.license create mode 100644 subprojects/docs/src/docs/tutorials/file-system/fig2.png create mode 100644 subprojects/docs/src/docs/tutorials/file-system/fig2.png.license create mode 100644 subprojects/docs/src/docs/tutorials/file-system/fig3.png create mode 100644 subprojects/docs/src/docs/tutorials/file-system/fig3.png.license create mode 100644 subprojects/docs/src/docs/tutorials/file-system/fig4.png create mode 100644 subprojects/docs/src/docs/tutorials/file-system/fig4.png.license create mode 100644 subprojects/docs/src/docs/tutorials/file-system/index.md (limited to 'subprojects') 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 Binary files /dev/null and b/subprojects/docs/src/docs/tutorials/file-system/fig1.png differ 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 + +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 Binary files /dev/null and b/subprojects/docs/src/docs/tutorials/file-system/fig2.png differ 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 + +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 Binary files /dev/null and b/subprojects/docs/src/docs/tutorials/file-system/fig3.png differ 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 + +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 Binary files /dev/null and b/subprojects/docs/src/docs/tutorials/file-system/fig4.png differ 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 + +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'; + +

+ Try in Refinery +

+ +- 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 ```::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..*. +``` -- cgit v1.2.3-54-g00ecf