From c69558f7cddf0a5a8faa446b50fc11fcea0cce8b Mon Sep 17 00:00:00 2001
From: Andrea Franchini <hello@andreafranchini.com>
Date: Thu, 2 Feb 2023 14:22:34 +0100
Subject: [PATCH] Update docs for new DOMLR
---
docs/tests.rst | 2 +-
docs/usage.rst | 8 +-
docs/writing-requirements.rst | 109 ++++++++++++++-------------
tests/domlr/example_single_req.domlr | 2 +-
4 files changed, 62 insertions(+), 59 deletions(-)
diff --git a/docs/tests.rst b/docs/tests.rst
index 1e21a31..fb6c26c 100644
--- a/docs/tests.rst
+++ b/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
diff --git a/docs/usage.rst b/docs/usage.rst
index 2ab00ab..0d0478b 100644
--- a/docs/usage.rst
+++ b/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
diff --git a/docs/writing-requirements.rst b/docs/writing-requirements.rst
index 33622e8..05ba4cb 100644
--- a/docs/writing-requirements.rst
+++ b/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,87 +16,90 @@ 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`:
Syntax
======
- The syntax is the following:
-
- - Unary operators: ``not``
- - Example: ``not <expression>``
- - Binary operators: ``or``, ``and``, ``implies``, ``iff`` (if and only if, AKA double implication)
- - Example: ``<expression> and <expression>``
- - 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)
- - 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``
- - Values (constants):
- - Strings are delimited by double quotes ``"..."``
- - Numbers are integers
- - Booleans are either ``!True`` or ``!False``
- - Example: ``56``, ``"linux"``, ``!False``, ``!False``
- - 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)
- - Relationships follow this naming structure ``<package>.<class>.<relationship>``.
- - 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.
- - 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``
+The syntax is the following:
+
+- Unary operators: ``not``
+ - Example: ``not <expression>``
+- Binary operators: ``or``, ``and``, ``implies``, ``iff`` (if and only if, AKA double implication)
+ - Example: ``<expression> and <expression>``
+- 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).
+ - 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`` or ``vm``
+- Values (constants):
+ - Strings are delimited by double quotes ``"..."``
+ - 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).
+ - 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 use it to assign a class to an element.
+ - Example: ``vm is class abstract.VirtualMachine``
+- Comparisons: ``>``, ``>=``, ``<``, ``<=``, ``==``, ``!=``
+ - 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``.
diff --git a/tests/domlr/example_single_req.domlr b/tests/domlr/example_single_req.domlr
index 759ace0..a3e87f4 100644
--- a/tests/domlr/example_single_req.domlr
+++ b/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."
--
GitLab