diff options
author | Kristóf Marussy <kristof@marussy.com> | 2024-04-10 12:48:10 +0200 |
---|---|---|
committer | Kristóf Marussy <kristof@marussy.com> | 2024-04-10 12:48:10 +0200 |
commit | 0d0379504b4476d60275a61d0da1d6e053f67ab3 (patch) | |
tree | 813094020d5284cb4ff6be316d3c9c1a10859f59 /subprojects/docs/src/learn | |
parent | docs: add existing static assets (diff) | |
download | refinery-0d0379504b4476d60275a61d0da1d6e053f67ab3.tar.gz refinery-0d0379504b4476d60275a61d0da1d6e053f67ab3.tar.zst refinery-0d0379504b4476d60275a61d0da1d6e053f67ab3.zip |
refactor(docs): URL structure
Diffstat (limited to 'subprojects/docs/src/learn')
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 @@ | |||
1 | --- | ||
2 | SPDX-FileCopyrightText: 2024 The Refinery Authors | ||
3 | SPDX-License-Identifier: EPL-2.0 | ||
4 | sidebar_position: 100 | ||
5 | sidebar_label: Docker | ||
6 | --- | ||
7 | |||
8 | # Running in Docker | ||
9 | |||
10 | :::note | ||
11 | |||
12 | Refinery can run as a cloud-based _Graph Solver as a Service_ without local installation. | ||
13 | If you're just looking to try Refinery, our [online demo](https://refinery.services/) provides a seamless experience without installation. | ||
14 | |||
15 | ::: | ||
16 | |||
17 | :::info | ||
18 | |||
19 | Installing Refinery as a Docker container can support more advanced use cases, such as when generating models with more resources or a longer timeout. | ||
20 | |||
21 | ::: | ||
22 | |||
23 | 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: | ||
24 | |||
25 | ```shell | ||
26 | docker run --rm -it -p 8888:8888 ghcr.io/graphs4value/refinery | ||
27 | ``` | ||
28 | |||
29 | Once Docker pulls and starts the container, you can navigate to http://localhost:8888 to open the model generation interface and start editing. | ||
30 | |||
31 | Alternatively, you can follow the [instructions to set up a local development environment](/develop/contributing) and compile and run Refinery from source. | ||
32 | |||
33 | ## Updating | ||
34 | |||
35 | To take advantage of the latest updates, you can simply re-pull our Docker container from the GitHub Container Registry: | ||
36 | |||
37 | ```shell | ||
38 | docker pull ghcr.io/graphs4value/refinery | ||
39 | ``` | ||
40 | |||
41 | Restart the container to make sure that you're running the last pulled version. | ||
42 | |||
43 | ## Environmental variables | ||
44 | |||
45 | The Docker container supports the following environmental variables to customize its behavior. | ||
46 | Customizing these variable should only be needed if you want to _increase resource limits_ or _expose you Refinery instance over the network_ for others. | ||
47 | |||
48 | Notes for **local-only instances** are highlighted with the :arrow_right: arrow emoji. | ||
49 | |||
50 | Important security notices for **public instances** are highlighted with the :warning: warning emoji. | ||
51 | |||
52 | ### Networking | ||
53 | |||
54 | #### `REFINERY_LISTEN_HOST` | ||
55 | |||
56 | Hostname to listen at for incoming HTTP connections. | ||
57 | |||
58 | **Default value:** `0.0.0.0` (accepts connections on any IP address) | ||
59 | |||
60 | #### `REFINERY_LISTEN_PORT` | ||
61 | |||
62 | TCP port to listen at for incoming HTTP connections. | ||
63 | |||
64 | 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. | ||
65 | |||
66 | 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. | ||
67 | |||
68 | **Default value:** `8888` | ||
69 | |||
70 | #### `REFINERY_PUBLIC_HOST` | ||
71 | |||
72 | Publicly visible hostname of the Refinery instance. | ||
73 | |||
74 | :arrow_right: For installations only accessed locally (i.e., `localhost:8888`) without any reverse proxy, you can safely leave this empty. | ||
75 | |||
76 | :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/). | ||
77 | |||
78 | **Default value:** _empty_ | ||
79 | |||
80 | #### `REFINERY_PUBLIC_PORT` | ||
81 | |||
82 | Publicly visible port of the Refinery instance. | ||
83 | |||
84 | :arrow_right: For installations only accessed locally (i.e., `localhost:8888`), this value is ignored because `REFINERY_PUBLC_HOST` is not set. | ||
85 | |||
86 | **Default value:** `443` | ||
87 | |||
88 | #### `REFINERY_ALLOWED_ORIGINS` | ||
89 | |||
90 | Comma-separated list of allowed origins for incoming WebSocket connections. If this variable is empty, all incoming WebSocket connections are accepted. | ||
91 | |||
92 | :arrow_right: For installations only accessed locally (i.e., `localhost:8888`) without any reverse proxy, you can safely leave this empty. | ||
93 | |||
94 | :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. | ||
95 | |||
96 | **Default value:** equal to `REFINERY_PUBLIC_HOST:REFINERY_PUBLIC_PORT` if they are both set, _empty_ otherwise | ||
97 | |||
98 | ### Timeouts | ||
99 | |||
100 | #### `REFINERY_SEMANTICS_TIMEOUT_MS` | ||
101 | |||
102 | Timeout for partial model semantics calculation in milliseconds. | ||
103 | |||
104 | :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. | ||
105 | |||
106 | :warning: Increasing this timeout may increase server load. Excessively large timeout may allow users to overload you server by entering extremely complex partial models. | ||
107 | |||
108 | **Default value:** `1000` | ||
109 | |||
110 | #### `REFINERY_SEMANTICS_WARMUP_TIMEOUT_MS` | ||
111 | |||
112 | Timeout for partial model semantics calculation in milliseconds when the server first start. | ||
113 | |||
114 | 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). | ||
115 | |||
116 | **Default value:** equal to 2 × `REFINERY_SEMANTICS_TIMEOUT` | ||
117 | |||
118 | #### `REFINERY_MODEL_GENERATION_TIMEOUT_SEC` | ||
119 | |||
120 | Timeout for model generation in seconds. | ||
121 | |||
122 | :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. | ||
123 | |||
124 | :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. | ||
125 | |||
126 | **Default value:** `600` (10 minutes) | ||
127 | |||
128 | ### Threading | ||
129 | |||
130 | :warning: Excessively large values may overload the server. Make sure that _all_ Refinery threads can run at the same time to avoid thread starvation. | ||
131 | |||
132 | #### `REFINERY_XTEXT_THREAD_COUNT` | ||
133 | |||
134 | 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. | ||
135 | |||
136 | :warning: Excessively large values may overload the server. Make sure that _all_ Refinery threads can run at the same time to avoid thread starvation. | ||
137 | |||
138 | **Default value:** `1` | ||
139 | |||
140 | #### `REFINERY_XTEXT_LOCKING_THREAD_COUNT` | ||
141 | |||
142 | 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. | ||
143 | |||
144 | |||
145 | **Default value:** equal to `REFINERY_XTEXT_THREAD_COUNT` | ||
146 | |||
147 | #### `REFINERY_XTEXT_SEMANTICS_THREAD_COUNT` | ||
148 | |||
149 | 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. | ||
150 | |||
151 | Must be at least as large as `REFINERY_XTEXT_THREAD_COUNT`. | ||
152 | |||
153 | :warning: Excessively large values may overload the server. Make sure that _all_ Refinery threads can run at the same time to avoid thread starvation. | ||
154 | |||
155 | **Default value:** equal to `REFINERY_XTEXT_THREAD_COUNT` | ||
156 | |||
157 | #### `REFINERY_MODEL_GENERATION_THREAD_COUNT` | ||
158 | |||
159 | 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. | ||
160 | |||
161 | :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. | ||
162 | |||
163 | **Default value:** equal to `REFINERY_XTEXT_THREAD_COUNT` | ||
164 | |||
165 | ### Libraries | ||
166 | |||
167 | #### `REFINERY_LIBRARY_PATH` | ||
168 | |||
169 | Modules (`.refinery` files) in this directory or colon-separated list of directories will be exposed to user via Refinery's `import` mechanism. | ||
170 | |||
171 | :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. | ||
172 | |||
173 | :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. | ||
174 | |||
175 | **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 @@ | |||
1 | --- | ||
2 | SPDX-FileCopyrightText: 2024 The Refinery Authors | ||
3 | SPDX-License-Identifier: EPL-2.0 | ||
4 | sidebar_position: 0 | ||
5 | --- | ||
6 | |||
7 | # Introduction | ||
8 | |||
9 | 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. | ||
10 | |||
11 | **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 @@ | |||
1 | # SPDX-FileCopyrightText: 2024 The Refinery Authors | ||
2 | # | ||
3 | # SPDX-License-Identifier: EPL-2.0 | ||
4 | |||
5 | position: 2 | ||
6 | label: Language reference | ||
7 | link: | ||
8 | type: generated-index | ||
9 | slug: /language | ||
10 | 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 @@ | |||
1 | --- | ||
2 | SPDX-FileCopyrightText: 2024 The Refinery Authors | ||
3 | SPDX-License-Identifier: EPL-2.0 | ||
4 | description: Metamodeling in Refinery | ||
5 | sidebar_position: 0 | ||
6 | --- | ||
7 | |||
8 | # Classes and references | ||
9 | |||
10 | :::warning | ||
11 | |||
12 | Under construction | ||
13 | |||
14 | ::: | ||
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 @@ | |||
1 | # SPDX-FileCopyrightText: 2024 The Refinery Authors | ||
2 | # | ||
3 | # SPDX-License-Identifier: EPL-2.0 | ||
4 | |||
5 | position: 1 | ||
6 | label: Tutorials | ||
7 | link: | ||
8 | type: generated-index | ||
9 | slug: /tutorials | ||
10 | title: Tutorial overview | ||
11 | 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 | |||
Binary files differ | |||
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 @@ | |||
1 | SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
2 | |||
3 | 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 | |||
Binary files differ | |||
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 @@ | |||
1 | SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
2 | |||
3 | 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 | |||
Binary files differ | |||
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 @@ | |||
1 | SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
2 | |||
3 | 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 | |||
Binary files differ | |||
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 @@ | |||
1 | SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
2 | |||
3 | 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 @@ | |||
1 | --- | ||
2 | SPDX-FileCopyrightText: 2023-2024 The Refinery Authors | ||
3 | SPDX-License-Identifier: EPL-2.0 | ||
4 | description: Introduction to classes, references, and error predicates | ||
5 | sidebar_position: 0 | ||
6 | sidebar_label: File system | ||
7 | --- | ||
8 | |||
9 | # File system tutorial | ||
10 | |||
11 | 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. | ||
12 | |||
13 | ## Partial models | ||
14 | |||
15 | ### Types and relations | ||
16 | |||
17 | - 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. | ||
18 | |||
19 | ```refinery | ||
20 | class FileSystem { | ||
21 | contains File[1] root | ||
22 | } | ||
23 | |||
24 | class File. | ||
25 | |||
26 | class Dir extends File { | ||
27 | contains File[] element | ||
28 | } | ||
29 | |||
30 | scope node = 10. | ||
31 | ``` | ||
32 | |||
33 | import Link from '@docusaurus/Link'; | ||
34 | |||
35 | <p> | ||
36 | <Link | ||
37 | href="https://refinery.services/#/1/KLUv_SDT_QMAQkcXGnBL2-ikxOa10ZNeN1bwnxijfsojpwHQAxAE5pzBk5uCd8F5EjAGJrUNQBWIbdRU7tkRB-VsG_aVuMlSEWzzTShXE8h-eBHzK_cK11NoD9P_2_GFrS61RRmuipYUCwA046ljtvEqgDAGQyDQwsIqKACEt2LiANXAaUxBAQ==" | ||
38 | className="button button--lg button--primary button--play" | ||
39 | >Try in Refinery</Link> | ||
40 | </p> | ||
41 | |||
42 | - Notice that the syntax is essentially identical to [Xcore](https://wiki.eclipse.org/Xcore). | ||
43 | - Review the partial model visualization. You should get something like this: | ||
44 | |||
45 | ![Initial model](fig1.png) | ||
46 | |||
47 | - Add some statements about a partial model: | ||
48 | |||
49 | ```refinery | ||
50 | class FileSystem { | ||
51 | contains File[1] root | ||
52 | } | ||
53 | |||
54 | class File. | ||
55 | |||
56 | class Dir extends File { | ||
57 | contains File[] element | ||
58 | } | ||
59 | |||
60 | Dir(resources). | ||
61 | element(resources, img). | ||
62 | File(img). | ||
63 | |||
64 | scope node = 10. | ||
65 | ``` | ||
66 | |||
67 | ![Partial model extended with new facts](fig2.png) | ||
68 | |||
69 | ### Partial models | ||
70 | |||
71 | - Notice that the instance model elements are coexisting with ```<type>::new``` nodes representing the prototypes of newly created objects. | ||
72 | |||
73 | - Check the disabled `equals` and `exist` predicates. check the visual annotation of those predicates in the visualization (dashed line, shadow). | ||
74 | |||
75 | ![Object existence and equality](fig3.png) | ||
76 | |||
77 | ### Information merging | ||
78 | |||
79 | - For the object `img`, we didn't specify if it is a directory or not. Therefore, it will typically be a folder. | ||
80 | |||
81 | - If we want to state that img is not a directory, we need to a negative statement: | ||
82 | |||
83 | ```refinery | ||
84 | !Dir(img). | ||
85 | ``` | ||
86 | |||
87 | - Statements are merged with respect to the refinement relation of 4-valued logic. | ||
88 | |||
89 | - If we add, a statement both negatively and positively, it will create an inconsistency: | ||
90 | |||
91 | ```refinery | ||
92 | element(resources, img). | ||
93 | !element(resources, img). | ||
94 | ``` | ||
95 | |||
96 | - Inconsistent models parts in a partial model typically make the problem trivially unsatisfiable. | ||
97 | |||
98 | ![Inconsistent partial model](fig4.png) | ||
99 | |||
100 | - However, the model can be saved if the inconsistent part may not exist... | ||
101 | |||
102 | ```refinery | ||
103 | !File(File::new). | ||
104 | ``` | ||
105 | |||
106 | ### Default values | ||
107 | |||
108 | - A large amount of statements can be expressed by using `*`. | ||
109 | - The `default` keyword defines lower priority statements that need to be considered unless other statement specifies otherwise. No information merging is happening. | ||
110 | |||
111 | ## Constraints | ||
112 | |||
113 | Let's extend the metamodel with a new class `SymLink`: | ||
114 | |||
115 | ```refinery | ||
116 | class FileSystem { | ||
117 | contains File[1] root | ||
118 | } | ||
119 | |||
120 | class File. | ||
121 | |||
122 | class Dir extends File { | ||
123 | contains File[0..10] element | ||
124 | } | ||
125 | |||
126 | class SymLink extends File { | ||
127 | File[1] target | ||
128 | } | ||
129 | |||
130 | Dir(resources). | ||
131 | element(resources, img). | ||
132 | element(resources, link). | ||
133 | target(link, img). | ||
134 | |||
135 | scope node = 10. | ||
136 | ``` | ||
137 | |||
138 | - Add some simple constraints: | ||
139 | |||
140 | ```refinery | ||
141 | % Simple constraints: | ||
142 | pred hasReference(f) <-> target(_, f). | ||
143 | error pred selfLoop(s) <-> target(s, s). | ||
144 | target(x,x). | ||
145 | ``` | ||
146 | |||
147 | - There are no empty directories in a git repository, so let's forbid them! | ||
148 | |||
149 | ```refinery | ||
150 | error pred emptyDir(d) <-> Dir(d), !element(d,_). | ||
151 | ``` | ||
152 | |||
153 | - End result: | ||
154 | |||
155 | ```refinery | ||
156 | class FileSystem { | ||
157 | contains File[1] root | ||
158 | } | ||
159 | |||
160 | class File. | ||
161 | |||
162 | class Dir extends File { | ||
163 | contains File[0..10] element | ||
164 | } | ||
165 | |||
166 | class SymLink extends File { | ||
167 | File[1] target | ||
168 | } | ||
169 | |||
170 | Dir(resources). | ||
171 | element(resources, img). | ||
172 | !Dir(img). | ||
173 | element(resources, link). | ||
174 | target(link,img). | ||
175 | |||
176 | % Simple constraints: | ||
177 | pred hasReference(f) <-> target(_, f). | ||
178 | error pred selfLoop(s) <-> target(s, s). | ||
179 | |||
180 | % Object equality with ==: | ||
181 | error pred emptyDir(d) <-> Dir(d), !element(d, _). | ||
182 | pred importantFile(f) <-> target(l1, f), target(l2, f), l1 != l2. | ||
183 | |||
184 | % Transitive closure, and | ||
185 | pred containsFile(fs, file) <-> | ||
186 | FileSystem(fs), | ||
187 | root(fs, file) | ||
188 | ; | ||
189 | FileSystem(fs), | ||
190 | root(fs, rootDir), | ||
191 | element+(rootDir, file). | ||
192 | |||
193 | % Predicate reuse | ||
194 | error conflictBetweenTwoFileSystem(fs1, fs2, l, t) <-> | ||
195 | containsFile(fs1, l), | ||
196 | containsFile(fs2, t), | ||
197 | fs1 != fs2, | ||
198 | target(l, t). | ||
199 | |||
200 | scope node = 40..50, FileSystem = 2, importantFile = 1..*. | ||
201 | ``` | ||