Finish documentation.

README.md

-# PIACERE Model Checker REST API server
+# PIACERE Model Checker
+
+The DOML Model Checker is a component of the [PIACERE](https://www.piacere-project.eu/) framework
+in charge of checking the correctness and consistency of
+[DOML](https://www.piacere-doml.deib.polimi.it/) models.
 
 This project is packaged with [Poetry](https://python-poetry.org/).
 
+
 ## Build and Run
 
 Build with
@@ -18,6 +23,7 @@ Run tests with:
 poetry run python -m pytest
 ```
 
+
 ## Run with uWSGI
 
 The project may be run with [uWSGI](https://uwsgi-docs.readthedocs.io/) as follows:
@@ -25,6 +31,7 @@ The project may be run with [uWSGI](https://uwsgi-docs.readthedocs.io/) as follo
 uwsgi --http :8080 -w mc_openapi.app_config -p 4
 ```
 
+
 ## Run with Docker
 
 First, build the docker image with the usual
@@ -38,14 +45,19 @@ docker run -d wp4/dmc
 The uWSGI server will be running and listening on port 80 of the container.
 
 
-## REST APIs
-
-The OpenAPI definition of the REST APIs is in `mc_openapi/openapi/model_checker.yaml`.
+## Building the Documentation
 
-The APIs can also be browsed with [Swagger UI](https://swagger.io/tools/swagger-ui/) by appending `/ui/` to the API HTTP address.
+The documentation has been written in [Sphinx](https://www.sphinx-doc.org/)
+and covers both usage through the PIACERE IDE and the REST APIs.
 
-For APIs usage examples, you may look into the tests, in `tests/test_mc_openapi.py`.
-Two DOML examples in XMI format are sent to the server.
-One of them is correct (`tests/doml/nginx-openstack_v2.domlx`), and the server answers with `"sat"` (meaning the requirements are satisfied), and the other one contains an error (`tests/doml/nginx-openstack_v2_wrong.domlx`), so the server answers with `"unsat"`.
+To build it, type
+```sh
+poetry shell
+```
+and then
+```sh
+cd docs
+make html
+```
 
-**Note:** for the time being, the `model` field of the POST request's body accepts any XML object. This will be changed to the DOML XMI schema when possible.
+The documentation will be generated in `docs/_build`.

docs/index.rst

@@ -3,8 +3,12 @@
    You can adapt this file completely to your liking, but it should at least
    contain the root `toctree` directive.
 
-Welcome to the DOML Model Checker's documentation!
-==================================================
+DOML Model Checker's documentation
+==================================
+
+The DOML Model Checker is a component of the `PIACERE`_ framework
+in charge of checking the correctness and consistency of `DOML`_ models.
+
 
 .. toctree::
    :maxdepth: 2
@@ -12,11 +16,21 @@ Welcome to the DOML Model Checker's documentation!
 
    installation
    usage
+   requirements
+   restapis
 
-
+..
    Indices and tables
    ==================
 
-* :ref:`genindex`
+.. * :ref:`genindex`
    * :ref:`modindex`
    * :ref:`search`
+
+
+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/
+.. _DOML: https://www.piacere-doml.deib.polimi.it/

docs/installation.rst

@@ -56,8 +56,26 @@ And then run it with::
 The uWSGI server will be running and listening on port 80 of the container.
 
 
+Building the Documentation
+--------------------------
+
+The documentation has been written in `Sphinx`_.
+
+To build it, type::
+
+  poetry shell
+
+and then::
+
+  cd docs
+  make html
+
+The documentation will be generated in ``docs/_build``.
+
+
 .. _Poetry: https://python-poetry.org/
 .. _Flask: https://flask.palletsprojects.com/
 .. _Swagger-UI: https://swagger.io/tools/swagger-ui/
 .. _uWSGI: https://uwsgi-docs.readthedocs.io/
 .. _Docker: https://www.docker.com/
+.. _Sphinx: https://www.sphinx-doc.org/

docs/requirements.rst

+Checked 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.
+Here we list and describe such requirements.
+
+
+VM Network Interfaces
+---------------------
+
+  All virtual machines must be connected to at least one network interface.
+
+Virtual machines can communicate with other components of a deployment or with external clients
+only through an appropriately configured network.
+this check makes sure no virtual machines are isolated.
+
+
+Concretization of Software Interfaces
+-------------------------------------
+
+  All software packages can see the interfaces they need through a common network.
+
+This check makes sure all exposed and consumed software interfaces at the application layer level
+have been actually concretized through a network connection that allows the involved components
+to communicate.
+
+
+Duplicated Interfaces
+---------------------
+
+  There are no duplicated interfaces.
+
+Checks whether two or more interfaces have been assigned the same IP address in the same network.
+
+
+Deployed Software Components
+----------------------------
+
+  All software components have been deployed to some node.
+
+Makes sure that all software components specified in the application layer have been
+associated to at least one node in the abstract infrastructure layer
+through the currently active deployment.
+
+
+Concretization of Abstract Infrastructure
+-----------------------------------------
+
+  All abstract infrastructure elements are mapped to an element in the active concretization.
+
+Makes sure all abstract infrastructure are concretized by the currently active concretization layer.

docs/restapis.rst

+REST APIs
+=========
+
+The `OpenAPI`_ definition of the REST APIs is in ``mc_openapi/openapi/model_checker.yaml``.
+
+The APIs can also be browsed with `Swagger UI`_ by appending ``/ui/`` to the APIs' HTTP address.
+
+For APIs usage examples, you may look into the tests, in ``tests/test_mc_openapi.py``.
+Some DOML examples in XMI format are sent to the server.
+One of them is correct (``tests/doml/nginx-openstack_v2.domlx``),
+and the server answers with ``"sat"`` (meaning the requirements are satisfied),
+and the other one contains an error (``tests/doml/nginx-openstack_v2_wrong.domlx``),
+so the server answers with ``"unsat"``.
+
+
+.. _OpenAPI: https://www.openapis.org/
+.. _Swagger UI: https://swagger.io/tools/swagger-ui/