Update docs for new DOMLR

docs/tests.rst

@@ -5,6 +5,6 @@ To run the tests with *PyTest* you'll need to setup the server::
   
   poetry run python -m mc_openapi
 
-and then::
+and then run separately::
 
   poetry run python -m pytest

docs/usage.rst

@@ -82,15 +82,15 @@ Flags                              Mode       Description
 ---------------------------------  ---------  -----------------
 Short   Long         
 ======  =========================  =========  =================
-``-h``  ``--help``                 C, S, T    Print the all the available flags with an explanation
-``-v``  ``--verbose``              C, S, T    Print a detailed human-readable output of everything going on. Helpful for debugging
+``-h``  ``--help``                 C, S, R    Print the all the available flags with an explanation
+``-v``  ``--verbose``              C, S, R    Print a detailed human-readable output of everything going on. Helpful for debugging
 ``-p``  ``--port``                 R          The port that will expose the REST API (default: 8080)
 ``-d``  ``--doml``                 C, S       The DOMLX file to check with the model checker
 ``-V``  ``--doml-version``         C, S       The DOML version in which the DOMLX file is written in
 ``-r``  ``--requirements``         C, S       A text file containing the user-defined requirements written in :doc:`DOMLR <writing-requirements>`.
 ``-S``  ``--skip-common-checks``   C          Skips :doc:`build-in requirements <requirements>` checks
 ``-c``  ``--check-consistency``    C          Perform additional consistency checks (legacy)
-``-t``  ``--threads``              C, S, T    The number of threads used by the model checker (default: 2)
+``-t``  ``--threads``              C, R       The number of threads used by the model checker (default: 2)
 ``-s``  ``--synth``                S          Synthetize a new DOMLX file from requirements
 ``-m``  ``--max-tries``            S          Max number of tries to solve a model during synthesis (default: 10)
 ======  =========================  =========  =================
@@ -106,4 +106,4 @@ To check a DOMLX file with user-provided custom requirements, you may run::
 
 To synthetize a new DOMLX file with 4 threads and a maximum of 15 tries, you may run::
 
-  python -m mc_openapi -d ./path/to/myModel.domlx --synth -t 4 -m 15
\ No newline at end of file
+  python -m mc_openapi -d ./path/to/myModel.domlx --synth -m 15
\ No newline at end of file

docs/writing-requirements.rst

@@ -2,7 +2,7 @@ Writing Requirements
 ********************
 
 A feature of the DOML Model Checker is a Domain Specific Language (DSL)
-called **DOMLR**.
+called **DOMLR** (the R stands for requirements).
 
 It will be integrated in the DOML in a future release.
 For now, it can be provided to the Model Checker through the CLI.
@@ -16,41 +16,43 @@ If you use VS Code, there's a `Syntax Highlight`_ extension for it.
 
 Every user requirement file is a list of requirement::
 
-    + "All VMs have iface"
+    + "All Virtual Machines have a Interface and at least 4 cpu cores"
     forall vm (
         vm is class abstract.VirtualMachine
         implies
         exists iface (
             vm has abstract.ComputingNode.ifaces iface
+            and
+            vm has abstract.ComputingNode.cpu_cores >= 4 
         )
     )
-    ---
-    "A vm does not have an associated interface"
+    error: "A vm does lacks an associated interface or has less than 4 cpu cores"
+
+Rules in 1 minute
+-----------------
 
 The language is *case-sensitive* but it's not indentation-based, so you are free to write it as you prefer.
 
 1.  A requirement must **start** with a ``+`` or ``-`` character.
 
-    -   ``+`` means that the requirement is in *positive form*: the requirement is satisfied when its
-        logic expression is satisfied.
+    -   ``+`` means that the requirement is in **positive form**: the requirement is satisfied when its logic expression is satisfied.
 
-    -   ``-`` means that the requirement is in *negative form*: the requirement is satisfied when its
-        logic expression **is not** satisfied.
+    -   ``-`` means that the requirement is in **negative form**: the requirement is satisfied when its logic expression **is not** satisfied.
 
-    The difference is that in *positive form* you'll generally use a *for all* quantifier at the beginning,
-    which doesn't allow you to know which specific element didn't satisfy the requirement, while in *negative form*
+    The difference is that in **positive form** you would generally use a *for all* quantifier at the beginning,
+    which doesn't allow you to know which specific element didn't satisfy the requirement, while in **negative form**
     you'll have some variables that are not quantified, meaning that it's usually possible to retrieve the names of the
     elements associated to those variables that do not satisfy the requirement.
 
 2.  After the ``+`` or ``-`` there's the **name** of the requirement, which is a string between double quotes ``"..."``.
-    They must be *double quotes*, single quotes ``'...'`` won't work.
+    Single quotes ``'...'`` won't work.
 
 3.  Following the requirement name, there's the **logic expression** which is the core of the requirement.
     It is written in `First Order Logic`_, so it will evaluate to either true or false. See the `Syntax`_ for details.
 
-4.  Last, delimited by ``---``, there is the **error message** that is printed when the requirement is not satisfied.
+4.  Last, following ``error:``, there is the **error message** that is printed when the requirement is not satisfied.
     If you have a free variable, which means a variable that is not quantified, you can print its value by putting it in the
-    string between curly brackets like this: ``{myVar}``. It may not always work.
+    string between curly brackets like this: ``{myVar}``. You'll get a warning if the Model Checker can't assign a value to that variable.
 
 .. `Syntax`:
 
@@ -66,37 +68,38 @@ Syntax
 - Quantifiers: ``forall``, ``exists``
     - Example: ``forall x, y ( <expression> )``
     - After the quantifier keywork (``forall``, ``exists``) you must specify a list of quantified variables
-          (separated by a comma ``,`` if there's more than one)
+        (separated by a comma ``,`` if there's more than one).
     - Between the mandatory pair of parenthesis, you'll be able to use the quantified variables in a logic expression.
 - Parenthesis: ``(`` ... ``)``
     - Useful when you have doubts about the precedence of operators, or want to increase legibility in certain situations.
 - Elements (variables):
     - Begin with a lowercase letter.
-        - Example: ``virtualMachine``
-    - Values (variables):
-        - Begin with an uppercase letter.
-        - Example: ``CpuCores``
+    - Example: ``virtualMachine`` or ``vm``
 - Values (constants):
     - Strings are delimited by double quotes ``"..."``
-        - Numbers are integers
-        - Booleans are either ``!True`` or ``!False``
-        - Example: ``56``, ``"linux"``, ``!False``, ``!False``
+    - Numbers are integers.
+    - Booleans are either ``:true`` or ``:false``
+    - Example: ``56``, ``"linux"``, ``:true``
 - Relationships: ``<elem> has <relationship> <elem/value>``
     - There are two types of relationships:
-            - *Associations* are a relationship between two elements (variables).
-            - *Attributes* are a relationship between an element (variable) and a value (variable or constant)
+        - **Associations** are a relationship between two elements (variables).
+        - **Attributes** are a relationship between an element (variable) and a value (variable or constant).
     - Relationships follow this naming structure ``<package>.<class>.<relationship>``.
+    - Example:
+        - ``vm has abstract.ComputingNode.ifaces iface`` is an **Association**, as it puts in relationship the element ``vm`` with the element ``iface``.
+
+        - ``vm has abstract.ComputingNode.cpu_cores >= 4`` is an **Attribute** Relationship, as it compares a property (``cpu_cores``) of the element ``vm`` with a constant number.
 - Classes: ``class <class name>``
     - They represent a kind of element in the architecture.
     - Classes follow this naming structure ``<package>.<class>``
 - Equality: ``is``, ``is not``
-        - Used to set an equality (or inequality) constraint on an element variable. You can compare elements and classes. 
-          You can even compare classes between each other, but it's kinda pointless.
+    - Used to set an equality (or inequality) constraint on an element variable. You can use it to assign a class to an element.
     - Example: ``vm is class abstract.VirtualMachine``
 - Comparisons: ``>``,  ``>=``,  ``<``,  ``<=``,  ``==``,  ``!=``
-        - Used to compare two values between each other.
-        - You can compare variables and constants alike.
-        - Example: ``CpuCores >= 4``
+    - You can compare attributes with constants, or attributes with attributes.
+    - Example: 
+        - ``vm has abstract.ComputingNode.cpu_cores >= 4`` compares attribute ``cpu_cores`` with a numeric constant.
+        - ``vm1 has abstract.ComputingNode.cpu_cores >= vm2 abstract.ComputingNode.cpu_cores`` compares attribute ``cpu_cores`` of ``vm1`` with the one of ``vm2``.
 
 
 

tests/domlr/example_single_req.domlr

@@ -13,6 +13,6 @@
     vm is class infrastructure.VirtualMachine
     and
     not exists iface (
-        vm has infrastructure.ComputingNode.ifaces iface
+        vm has abstract.ComputingNode.ifaces iface
     )
     error: "VM {vm} has no associated interface."