Add docs for DSL/DOMLR and CLI

Fix a couple of typos that prevented the MC from working

docs/conf.py

@@ -19,11 +19,11 @@ import sphinx_rtd_theme
 # -- Project information -----------------------------------------------------
 
 project = 'DOML Model Checker'
-copyright = '2022, Michele Chiari and Michele De Pascalis'
-author = 'Michele Chiari and Michele De Pascalis'
+copyright = '2022, Michele Chiari, Michele De Pascalis, Andrea Franchini'
+author = 'Michele Chiari, Michele De Pascalis, Andrea Franchini'
 
 # The full version, including alpha/beta/rc tags
-release = '1.1.0'
+release = '2.0.0'
 
 
 # -- General configuration ---------------------------------------------------

docs/index.rst

@@ -3,7 +3,7 @@
    You can adapt this file completely to your liking, but it should at least
    contain the root `toctree` directive.
 
-DOML Model Checker's documentation
+DOML Model Checker Documentation
 ==================================
 
 The DOML Model Checker is a component of the `PIACERE`_ framework
@@ -15,7 +15,9 @@ in charge of checking the correctness and consistency of `DOML`_ models.
    :caption: Contents:
 
    installation
+   tests
    usage
+   writing-requirements
    requirements
    restapis
 
@@ -28,8 +30,8 @@ in charge of checking the correctness and consistency of `DOML`_ models.
    * :ref:`search`
 
 
-This project has received funding from the European Union's Horizon 2020
-research and innovation programme under grant agreement No. 101000162.
+*This project has received funding from the European Union's Horizon 2020
+research and innovation programme under grant agreement No. 101000162.*
 
 
 .. _PIACERE: https://www.piacere-project.eu/

docs/installation.rst

 Installation
-============
+************
 
-The DOML Model Checker receives user inputs through its REST APIs.
-In this guide we illuestrate saveral ways of setting up the server for these APIs.
+The model checker can be run in two configurations, *REST API* and *CLI*.
 
+First, you'll need to install the dependencies to run this tool.
 
-Build and run locally for testing
----------------------------------
+Installing the dependencies
+===========================
 
-This project is packaged with `Poetry`_, which we assume you have already
-`installed <https://python-poetry.org/docs/#installation>`_ into your system.
+This project is packaged with `Poetry`_, so you should install it first.
 
-
-Build with::
+Once *Poetry* has been installed, install the dependencies with::
   
   poetry install
 
-then run with::
+
+Run locally for testing
+-----------------------
+Run with::
 
   poetry run python -m mc_openapi
 
-this command serves the APIs through a `Flask`_ instance,
+This command serves the APIs through a `Flask`_ instance,
 which is suitable for testing, but not recommended for production.
-You may read the API specification generated by `Swagger-UI`_ by
-pointing your browser to http://127.0.0.1:8080/ui/.
-
-
-Then, run tests with::
-
-  poetry run python -m pytest
-
 
 Run locally with Uvicorn
 ------------------------
@@ -61,8 +54,13 @@ The Uvicorn server will be running and listening on port 80 of the container.
 To use it locally, you may e.g. bind it with port 8080 of ``localhost``
 by adding ``-p 127.0.0.1:8080:80/tcp`` to the ``docker run`` command.
 
+REST API Endpoints
+==================
+
+You may read the API specification generated by `Swagger-UI`_ at http://127.0.0.1:8080/ui/.
+
 Building the Documentation
---------------------------
+==========================
 
 The documentation has been written in `Sphinx`_.
 

docs/requirements.rst

-Checked Requirements
-====================
+Built-in Requirements
+=====================
 
 The DOML Model Checker verifies DOML models against a collection of requirements
 devised to highlight the most common mistakes made by users when specifying cloud deployments.

docs/tests.rst

+Testing
+=======
+
+To run the tests with *PyTest* you'll need to setup the server::
+  
+  poetry run python -m mc_openapi
+
+and then::
+
+  poetry run python -m pytest

docs/usage.rst

-Usage through the PIACERE IDE
-=============================
+Usage
+*****
 
 
-Invoking the DOML Model Checker from the PIACERE IDE
------------------------------------------------------
+Through the PIACERE IDE
+=======================
 
 The DOML Model Checker is usually invoked from the PIACERE IDE.
 It expects a DOML file in XMI format as its input,
@@ -48,3 +48,61 @@ and then choose *Piacere* -> *Model Checker Preferences*.
 
 Here you may enter the endpoint address and port, which is useful in case you want to
 run the DOML Model Checker locally, instead of using the official deployment.
+
+Through the Command Line Interface
+==================================
+
+Another way to use the model checker is through the CLI.
+It provides additional options that are not available in the IDE at
+the moment, such as support for a separate user requirement file
+and synthesis of DOMLX.
+
+You can run it with::
+
+  python -m mc_openapi [options]
+
+To display all the available flags, run::
+
+  python -m mc_openapi -h
+
+Options
+-------
+
+Please note that not all flags work with eachother. In most cases, some won't have
+any effect in certain CLI flags combinations.
+
+There are **3 Modes** in which the CLI can run:
+
+- REST API (**R**)
+- Model Checker (**C**)
+- Model Synthesis (**S**)
+
+======  =========================  =========  =================
+Flags                              Mode       Description
+---------------------------------  ---------  -----------------
+Short   Long         
+======  =========================  =========  =================
+``-h``  ``--help``                 C, S, T    Prints the all the available flags with an explanation
+``-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)
+``-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)
+======  =========================  =========  =================
+
+*If you do not provide the ``--doml`` option or the ``--synth`` option it will start the web server hosting the REST API!*
+
+Examples
+--------
+
+To check a DOMLX file with user-provided custom requirements, you may run::
+
+  python -m mc_openapi -d ./path/to/myModel.domlx -r ./path/to/myRequirements.domlr -V V2_0
+
+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

docs/writing-requirements.rst

+Writing Requirements
+********************
+
+A feature of the DOML Model Checker is a Domain Specific Language (DSL)
+called **DOMLR**.
+
+It will be integrated in the DOML in a future release.
+For now, it can be provided to the Model Checker through the CLI.
+
+Getting Started
+===============
+
+First, create a new file with a ``.domlr`` extension.
+
+If you use VS Code, there's an `Syntax Highlight`_ extension for it.
+
+Every user requirement file is a list of requirement::
+
+    + "All VMs have iface"
+    forall vm (
+        vm is class abstract.VirtualMachine
+        implies
+        exists iface (
+            vm has abstract.ComputingNode.ifaces iface
+        )
+    )
+    ---
+    "A vm does not have an associated interface"
+
+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 *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*
+    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.
+
+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.
+    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.
+
+.. `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``
+
+
+
+Operator Precedence
+-------------------
+
+``exists``/``forall`` > ``not`` > ``or`` > ``and`` > ``implies`` > ``iff``
+
+Grammar
+=======
+See the `grammar.lark`_ file on GitHub, it's written in a EBNF-like form.
+
+
+.. _`Syntax Highlight`: https://marketplace.visualstudio.com/items?itemName=andreafra.piacere-domlr
+.. _`First Order Logic`: https://en.wikipedia.org/wiki/First-order_logic
+.. _`grammar.lark`: https://github.com/andreafra/piacere-model-checker/blob/main/mc_openapi/doml_mc/dsl_parser/grammar.lark
\ No newline at end of file

mc_openapi/__main__.py

@@ -16,6 +16,7 @@ parser = argparse.ArgumentParser()
 parser.add_argument("-d", "--doml", dest="doml", help="the DOMLX file to check")
 parser.add_argument("-V", "--doml-version", dest="doml_version", default="V2_0", help="(optional) the version used by the DOMLX file")
 parser.add_argument("-r", "--requirements", dest="requirements", help="the user-specified requirements file to check")
+parser.add_argument("-p", "--port", dest="port", type=int, default=8080, help="the port exposing the model checker REST API (default: 8080)")
 # Model Checker
 parser.add_argument("-c", "--check-consistency", dest="consistency", action='store_true', help="check on additional built-in consistency requirements")
 parser.add_argument("-S", "--skip-common-checks", dest="skip_common", action='store_true', help="skip check on common built-in requirements")
@@ -28,7 +29,7 @@ args = parser.parse_args()
 
 if not args.doml and not args.synth:
     # Start the webserver
-    app.run(port=8080)
+    app.run(port=args.port)
 else:
     # Run only it via command line
     doml_path = args.doml

mc_openapi/doml_mc/dsl_parser/grammar.lark

@@ -41,9 +41,6 @@ value           : ESCAPED_STRING
 FLIP_EXPR       : "+"
                 | "-"
 
-EQUALITY_OP     : "is"
-                | "is not"
-
 COMPARISON_OP   : ">" | ">="
                 | "<" | "<="
                 | "==" | "!="

mc_openapi/doml_mc/mc.py

@@ -48,6 +48,7 @@ class ModelChecker:
         
         user_str_values = []
 
+        if user_requirements:
             req_store += user_requirements
 
         def worker(rfrom: int, rto: int):

mc_openapi/doml_mc/xmi_parser/doml_model.py

-from typing import Optional, Tuple
 import copy
 import importlib.resources as ilres
-from lxml import etree
+from typing import Optional, Tuple
 
-from mc_openapi import assets
-from mc_openapi.bytes_uri import BytesURI
+from lxml import etree
 from pyecore.ecore import EObject
 from pyecore.resources import ResourceSet
 
-from ..intermediate_model.doml_element import IntermediateModel, reciprocate_inverse_associations
-from ..intermediate_model.metamodel import DOMLVersion, MetaModels, InverseAssociations
+from mc_openapi import assets
+
+from ..intermediate_model.doml_element import (
+    IntermediateModel, reciprocate_inverse_associations)
+from ..intermediate_model.metamodel import (DOMLVersion, InverseAssociations,
+                                            MetaModels)
+from .bytes_uri import BytesURI
 from .ecore import ELayerParser
 from .special_parsers import SpecialParsers
 
-
 doml_rsets = {}
 def init_doml_rsets():  # noqa: E302
     global doml_rsets

mc_openapi/handlers.py

@@ -6,14 +6,15 @@ def make_error(user_msg, debug_msg=None):
     result = {"message": user_msg, "timestamp": datetime.datetime.now()}
     if debug_msg is not None:
         result["debug_message"] = debug_msg
+        print(f"ERROR [{datetime.datetime.now()}]: {debug_msg}")
     return result
 
 
-def post(body, requirement=None):
+def post(body):
     doml_xmi = body
     try:
         dmc = ModelChecker(doml_xmi)
-        results = dmc.check_common_requirements(threads=2, consistency_checks=False, timeout=50)
+        results = dmc.check_requirements(threads=2, consistency_checks=False, timeout=50)
         res, msg = results.summarize()
 
         if res == MCResult.sat:
@@ -22,5 +23,6 @@ def post(body, requirement=None):
             return {"result": res.name,
                     "description": msg}
 
+    # TODO: Make noteworthy exceptions to at least tell the user what is wrong
     except Exception as e:
         return make_error("The supplied DOMLX model is malformed or its DOML version is unsupported.", debug_msg=str(e)), 400

mc_openapi/openapi/model_checker.yaml

@@ -17,13 +17,6 @@ paths:
             schema:
               type: string
         required: true
-      parameters:
-        - in: query
-          name: requirement
-          required: false
-          schema:
-            type: string
-          description: Requirement to be verified (optional)
       responses:
         "200":
           content: