Merge branch 'mar23-modelchecker-update' into 'main'

Update Model Checker to latest version

See merge request piacere/private/t41-doml-model-checker!8

.github/workflows/docs.yml

+name: Pages
+on:
+  push:
+    branches:
+    - master
+jobs:
+  build:
+    runs-on: ubuntu-latest
+    steps:
+    - uses: actions/setup-python@v2
+    - uses: actions/checkout@master
+      with:
+        fetch-depth: 0 # otherwise, you will failed to push refs to dest repo
+    - name: Build and Commit
+      uses: sphinx-notes/pages@v2
+      with:
+        requirements_path: ./docs/requirements.txt
+    - name: Push changes
+      uses: ad-m/github-push-action@master
+      with:
+        github_token: ${{ secrets.GITHUB_TOKEN }}
+        branch: gh-pages
\ No newline at end of file

.gitignore

-*~
-*__pycache__*
-.vscode
-docs/_build
+# Byte-compiled / optimized / DLL files
+__pycache__/
+*.py[cod]
+*$py.class
+
+# C extensions
+*.so
+
+# Distribution / packaging
+.Python
+build/
+develop-eggs/
+dist/
+downloads/
+eggs/
+.eggs/
+lib/
+lib64/
+parts/
+sdist/
+var/
+wheels/
+share/python-wheels/
+*.egg-info/
+.installed.cfg
+*.egg
+MANIFEST
+
+# PyInstaller
+#  Usually these files are written by a python script from a template
+#  before PyInstaller builds the exe, so as to inject date/other infos into it.
+*.manifest
+*.spec
+
+# Installer logs
+pip-log.txt
+pip-delete-this-directory.txt
+
+# Unit test / coverage reports
+htmlcov/
+.tox/
+.nox/
+.coverage
+.coverage.*
+.cache
+nosetests.xml
+coverage.xml
+*.cover
+*.py,cover
+.hypothesis/
+.pytest_cache/
+cover/
+
+# Translations
+*.mo
+*.pot
+
+# Django stuff:
+*.log
+local_settings.py
+db.sqlite3
+db.sqlite3-journal
+
+# Flask stuff:
+instance/
+.webassets-cache
+
+# Scrapy stuff:
+.scrapy
+
+# Sphinx documentation
+docs/_build/
+
+# PyBuilder
+.pybuilder/
+target/
+
+# Jupyter Notebook
+.ipynb_checkpoints
+
+# IPython
+profile_default/
+ipython_config.py
+
+# pyenv
+#   For a library or package, you might want to ignore these files since the code is
+#   intended to run in multiple environments; otherwise, check them in:
+# .python-version
+
+# pipenv
+#   According to pypa/pipenv#598, it is recommended to include Pipfile.lock in version control.
+#   However, in case of collaboration, if having platform-specific dependencies or dependencies
+#   having no cross-platform support, pipenv may install dependencies that don't work, or not
+#   install all needed dependencies.
+#Pipfile.lock
+
+# poetry
+#   Similar to Pipfile.lock, it is generally recommended to include poetry.lock in version control.
+#   This is especially recommended for binary packages to ensure reproducibility, and is more
+#   commonly ignored for libraries.
+#   https://python-poetry.org/docs/basic-usage/#commit-your-poetrylock-file-to-version-control
+#poetry.lock
+
+# pdm
+#   Similar to Pipfile.lock, it is generally recommended to include pdm.lock in version control.
+#pdm.lock
+#   pdm stores project-wide configurations in .pdm.toml, but it is recommended to not include it
+#   in version control.
+#   https://pdm.fming.dev/#use-with-ide
+.pdm.toml
+
+# PEP 582; used by e.g. github.com/David-OConnor/pyflow and github.com/pdm-project/pdm
+__pypackages__/
+
+# Celery stuff
+celerybeat-schedule
+celerybeat.pid
+
+# SageMath parsed files
+*.sage.py
+
+# Environments
+.env
+.venv
+env/
+venv/
+ENV/
+env.bak/
+venv.bak/
+
+# Spyder project settings
+.spyderproject
+.spyproject
+
+# Rope project settings
+.ropeproject
+
+# mkdocs documentation
+/site
+
+# mypy
+.mypy_cache/
+.dmypy.json
+dmypy.json
+
+# Pyre type checker
+.pyre/
+
+# pytype static type analyzer
+.pytype/
+
+# Cython debug symbols
+cython_debug/
+
+# PyCharm
+#  JetBrains specific template is maintained in a separate JetBrains.gitignore that can
+#  be found at https://github.com/github/gitignore/blob/main/Global/JetBrains.gitignore
+#  and can be added to the global gitignore or merged into this file.  For a more nuclear
+#  option (not recommended) you can uncomment the following to ignore the entire idea folder.
+#.idea/
\ No newline at end of file

.gitlab-ci.yml

@@ -80,7 +80,7 @@ run-functional-tests:
     # Thus, we need to override the command so that the server is run on port 8080.
     - docker run --name $TESTS_CONTAINER_NAME -d -e "UVICORN_PORT=8080" $TMP_IMAGE
     # Install everything required for the tests.
-    - docker exec -i $TESTS_CONTAINER_NAME /bin/bash -c "pip install -r dev-requirements.txt"
+    - docker exec -i $TESTS_CONTAINER_NAME /bin/bash -c "pip install -r requirements.txt"
     # Run the tests.
     - docker exec -i $TESTS_CONTAINER_NAME /bin/bash -c "python -m pytest"
     # Stop the tests container.

.readthedocs.yaml

+# .readthedocs.yaml
+# Read the Docs configuration file
+# See https://docs.readthedocs.io/en/stable/config-file/v2.html for details
+
+# Required
+version: 2
+
+# Set the version of Python and other tools you might need
+build:
+  os: ubuntu-22.04
+  tools:
+    python: "3.11"
+    # You can also specify other tool versions:
+    # nodejs: "19"
+    # rust: "1.64"
+    # golang: "1.19"
+
+# Build documentation in the docs/ directory with Sphinx
+sphinx:
+   configuration: docs/conf.py
+
+# If using Sphinx, optionally build your docs in additional formats such as PDF
+# formats:
+#    - pdf
+
+# Optionally declare the Python requirements required to build your docs
+python:
+   install:
+   - requirements: docs/requirements.txt
\ No newline at end of file

.vscode/launch.json

+{
+    // Use IntelliSense to learn about possible attributes.
+    // Hover to view descriptions of existing attributes.
+    // For more information, visit: https://go.microsoft.com/fwlink/?linkid=830387
+    "version": "0.2.0",
+    "configurations": [
+        {
+            "name": "Python: MC Synthesis",
+            "type": "python",
+            "request": "launch",
+            "module": "mc_openapi",
+            "justMyCode": true,
+            "args": [
+                "-d", "tests/doml/openstack_template.domlx",
+                "--synth"
+            ]
+        }
+    ]
+}
\ No newline at end of file

.vscode/settings.json

+{
+    "python.testing.pytestArgs": [
+        "tests"
+    ],
+    "python.testing.unittestEnabled": false,
+    "python.testing.pytestEnabled": true
+}
\ No newline at end of file

Dockerfile

@@ -9,7 +9,7 @@ RUN pip install --upgrade pip \
     && pip install -r /opt/mc_openapi/requirements.txt
 WORKDIR /opt/mc_openapi
 
-ENV UVICORN_PORT=80 \
+ENV UVICORN_PORT=8080 \
     UVICORN_HOST=0.0.0.0
 
 CMD ["uvicorn", "--interface", "wsgi", "mc_openapi.app_config:app"]

README.md

+[![Documentation Status](https://readthedocs.org/projects/piacere-model-checker/badge/?version=latest)](https://piacere-model-checker.readthedocs.io/en/latest/?badge=latest)
+
 # PIACERE Model Checker
 
+**📖 You can read the [docs here](https://piacere-model-checker.readthedocs.io/en/latest/) for more details. 📖**
+
 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/).
 
+ We provide a `requirements.txt` file for CI/CD purposes.
 
-## Build and Run
+ If you add a new package, regenerate it by running:
  
-Build with
  ```sh
-poetry install
+ pip freeze > requirements.txt
  ```
-then run with
+
+## Setup
+
+Activate the Python Virtual Environment with:
 ```sh
-poetry run python -m mc_openapi
+source .venv/bin/activate
 ```
-
-Run tests with:
+Install the required packages with:
 ```sh
-poetry run python -m pytest
+pip install -r requirements.txt
 ```
 
+## Run the model checker web server
+```sh
+python -m mc_openapi
+```
 
 ## Run with Uvicorn
 
@@ -30,6 +39,12 @@ The project may be run with [Uvicorn](https://www.uvicorn.org/) as follows:
 ```sh
 uvicorn --port 8080 --host 0.0.0.0 --interface wsgi --workers 2 mc_openapi.app_config:app
 ```
+## Run tests
+
+Run tests with:
+```sh
+python -m pytest
+```
 
 
 ## Run with Docker
@@ -42,21 +57,18 @@ And then run it with
 ```sh
 docker run -d wp4/dmc
 ```
-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.
+The Uvicorn server will be running and listening on port `8080` of the container.
+To use it locally, you may bind it with port `8080` of `localhost`
+by adding `-p 127.0.0.1:8080:8080/tcp` to the `docker run` command.
 
 
 ## Building the Documentation
 
 The documentation has been written in [Sphinx](https://www.sphinx-doc.org/)
 and covers both usage through the PIACERE IDE and the REST APIs.
+You can read the latest version at [readthedocs.io](https://piacere-model-checker.readthedocs.io/en/latest/)
 
-To build it, type
-```sh
-poetry shell
-```
-and then
+If you want to build the documentation manually, run:
 ```sh
 cd docs
 make html

dev-requirements.txt

-alabaster==0.7.12 ; python_version >= "3.9" and python_version < "4.0"
-anyio==3.6.1 ; python_version >= "3.9" and python_version < "4.0"
-appnope==0.1.3 ; python_version >= "3.9" and python_version < "4.0" and platform_system == "Darwin" or python_version >= "3.9" and python_version < "4.0" and sys_platform == "darwin"
-asttokens==2.0.8 ; python_version >= "3.9" and python_version < "4.0"
-attrs==22.1.0 ; python_version >= "3.9" and python_version < "4.0"
-babel==2.10.3 ; python_version >= "3.9" and python_version < "4.0"
-backcall==0.2.0 ; python_version >= "3.9" and python_version < "4.0"
-certifi==2022.9.24 ; python_version >= "3.9" and python_version < "4"
-cffi==1.15.1 ; python_version >= "3.9" and python_version < "4.0" and implementation_name == "pypy"
-charset-normalizer==2.1.1 ; python_version >= "3.9" and python_version < "4"
-click==8.1.3 ; python_version >= "3.9" and python_version < "4.0"
-clickclick==20.10.2 ; python_version >= "3.9" and python_version < "4.0"
-colorama==0.4.5 ; python_version >= "3.9" and python_version < "4.0" and sys_platform == "win32" or python_version >= "3.9" and python_version < "4.0" and platform_system == "Windows"
-colorful==0.5.4 ; python_version >= "3.9" and python_version < "4.0"
-connexion[swagger-ui]==2.14.1 ; python_version >= "3.9" and python_version < "4.0"
-debugpy==1.6.3 ; python_version >= "3.9" and python_version < "4.0"
-decorator==5.1.1 ; python_version >= "3.9" and python_version < "4.0"
-docutils==0.17.1 ; python_version >= "3.9" and python_version < "4.0"
-entrypoints==0.4 ; python_version >= "3.9" and python_version < "4.0"
-executing==1.1.0 ; python_version >= "3.9" and python_version < "4.0"
-flask==2.2.2 ; python_version >= "3.9" and python_version < "4.0"
-future-fstrings==1.2.0 ; python_version >= "3.9" and python_version < "4.0"
-h11==0.14.0 ; python_version >= "3.9" and python_version < "4.0"
-httptools==0.5.0 ; python_version >= "3.9" and python_version < "4.0"
-idna==3.4 ; python_version >= "3.9" and python_version < "4"
-imagesize==1.4.1 ; python_version >= "3.9" and python_version < "4.0"
-importlib-metadata==5.0.0 ; python_version >= "3.9" and python_version < "3.10"
-inflection==0.5.1 ; python_version >= "3.9" and python_version < "4.0"
-iniconfig==1.1.1 ; python_version >= "3.9" and python_version < "4.0"
-ipykernel==6.16.0 ; python_version >= "3.9" and python_version < "4.0"
-ipython==8.5.0 ; python_version >= "3.9" and python_version < "4.0"
-itsdangerous==2.1.2 ; python_version >= "3.9" and python_version < "4.0"
-jedi==0.18.1 ; python_version >= "3.9" and python_version < "4.0"
-jinja2==3.1.2 ; python_version >= "3.9" and python_version < "4.0"
-joblib==1.2.0 ; python_version >= "3.9" and python_version < "4.0"
-jsonschema==4.16.0 ; python_version >= "3.9" and python_version < "4.0"
-jupyter-client==7.3.5 ; python_version >= "3.9" and python_version < "4.0"
-jupyter-core==4.11.1 ; python_version >= "3.9" and python_version < "4.0"
-lxml==4.9.1 ; python_version >= "3.9" and python_version < "4.0"
-markupsafe==2.1.1 ; python_version >= "3.9" and python_version < "4.0"
-matplotlib-inline==0.1.6 ; python_version >= "3.9" and python_version < "4.0"
-nest-asyncio==1.5.6 ; python_version >= "3.9" and python_version < "4.0"
-networkx==2.8.7 ; python_version >= "3.9" and python_version < "4.0"
-ordered-set==4.1.0 ; python_version >= "3.9" and python_version < "4.0"
-packaging==21.3 ; python_version >= "3.9" and python_version < "4.0"
-parso==0.8.3 ; python_version >= "3.9" and python_version < "4.0"
-pexpect==4.8.0 ; python_version >= "3.9" and python_version < "4.0" and sys_platform != "win32"
-pickleshare==0.7.5 ; python_version >= "3.9" and python_version < "4.0"
-pluggy==1.0.0 ; python_version >= "3.9" and python_version < "4.0"
-prettyprinter==0.18.0 ; python_version >= "3.9" and python_version < "4.0"
-prompt-toolkit==3.0.31 ; python_version >= "3.9" and python_version < "4.0"
-psutil==5.9.2 ; python_version >= "3.9" and python_version < "4.0"
-ptyprocess==0.7.0 ; python_version >= "3.9" and python_version < "4.0" and sys_platform != "win32"
-pure-eval==0.2.2 ; python_version >= "3.9" and python_version < "4.0"
-py==1.11.0 ; python_version >= "3.9" and python_version < "4.0"
-pycparser==2.21 ; python_version >= "3.9" and python_version < "4.0" and implementation_name == "pypy"
-pyecore==0.12.2 ; python_version >= "3.9" and python_version < "4.0"
-pygments==2.13.0 ; python_version >= "3.9" and python_version < "4.0"
-pyparsing==3.0.9 ; python_version >= "3.9" and python_version < "4.0"
-pyrsistent==0.18.1 ; python_version >= "3.9" and python_version < "4.0"
-pytest==7.1.3 ; python_version >= "3.9" and python_version < "4.0"
-python-dateutil==2.8.2 ; python_version >= "3.9" and python_version < "4.0"
-python-dotenv==0.21.0 ; python_version >= "3.9" and python_version < "4.0"
-pytz==2022.4 ; python_version >= "3.9" and python_version < "4.0"
-pywin32==304 ; sys_platform == "win32" and platform_python_implementation != "PyPy" and python_version >= "3.9" and python_version < "4.0"
-pyyaml==6.0 ; python_version >= "3.9" and python_version < "4.0"
-pyzmq==24.0.1 ; python_version >= "3.9" and python_version < "4.0"
-requests==2.28.1 ; python_version >= "3.9" and python_version < "4"
-restrictedpython==5.0 ; python_version >= "3.9" and python_version < "4.0"
-setuptools==65.4.1 ; python_version >= "3.9" and python_version < "4.0"
-six==1.16.0 ; python_version >= "3.9" and python_version < "4.0"
-sniffio==1.3.0 ; python_version >= "3.9" and python_version < "4.0"
-snowballstemmer==2.2.0 ; python_version >= "3.9" and python_version < "4.0"
-sphinx-rtd-theme==1.0.0 ; python_version >= "3.9" and python_version < "4.0"
-sphinx==5.2.3 ; python_version >= "3.9" and python_version < "4.0"
-sphinxcontrib-applehelp==1.0.2 ; python_version >= "3.9" and python_version < "4.0"
-sphinxcontrib-devhelp==1.0.2 ; python_version >= "3.9" and python_version < "4.0"
-sphinxcontrib-htmlhelp==2.0.0 ; python_version >= "3.9" and python_version < "4.0"
-sphinxcontrib-jsmath==1.0.1 ; python_version >= "3.9" and python_version < "4.0"
-sphinxcontrib-qthelp==1.0.3 ; python_version >= "3.9" and python_version < "4.0"
-sphinxcontrib-serializinghtml==1.1.5 ; python_version >= "3.9" and python_version < "4.0"
-stack-data==0.5.1 ; python_version >= "3.9" and python_version < "4.0"
-swagger-ui-bundle==0.0.9 ; python_version >= "3.9" and python_version < "4.0"
-tomli==2.0.1 ; python_version >= "3.9" and python_version < "4.0"
-tornado==6.2 ; python_version >= "3.9" and python_version < "4.0"
-traitlets==5.4.0 ; python_version >= "3.9" and python_version < "4.0"
-urllib3==1.26.12 ; python_version >= "3.9" and python_version < "4"
-uvicorn[standard]==0.18.3 ; python_version >= "3.9" and python_version < "4.0"
-uvloop==0.17.0 ; sys_platform != "win32" and sys_platform != "cygwin" and platform_python_implementation != "PyPy" and python_version >= "3.9" and python_version < "4.0"
-watchfiles==0.17.0 ; python_version >= "3.9" and python_version < "4.0"
-wcwidth==0.2.5 ; python_version >= "3.9" and python_version < "4.0"
-websockets==10.3 ; python_version >= "3.9" and python_version < "4.0"
-werkzeug==2.2.2 ; python_version >= "3.9" and python_version < "4.0"
-z3-solver==4.11.2.0 ; python_version >= "3.9" and python_version < "4.0"
-zipp==3.8.1 ; python_version >= "3.9" and python_version < "3.10"

docker-compose.yaml

@@ -3,8 +3,8 @@ services:
   dmc:
     build: .
     ports:
-      - "8080:80"
+      - "8080:8080"
     environment:
-      UVICORN_PORT: 80
+      UVICORN_PORT: 8080
       UVICORN_HOST: "0.0.0.0"
       UVICORN_WORKERS: 2

docs/conf.py

@@ -13,17 +13,17 @@
 # import os
 # import sys
 # sys.path.insert(0, os.path.abspath('.'))
-import sphinx_rtd_theme
+# 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 ---------------------------------------------------
@@ -32,7 +32,7 @@ release = '1.1.0'
 # extensions coming with Sphinx (named 'sphinx.ext.*') or your custom
 # ones.
 extensions = [
-    'sphinx_rtd_theme'
+    # 'sphinx_rtd_theme'
 ]
 
 # Add any paths that contain templates here, relative to this directory.
@@ -41,7 +41,7 @@ templates_path = []
 # List of patterns, relative to source directory, that match files and
 # directories to ignore when looking for source files.
 # This pattern also affects html_static_path and html_extra_path.
-exclude_patterns = ['_build', 'Thumbs.db', '.DS_Store']
+exclude_patterns = ['_build', 'Thumbs.db', '.DS_Store', 'requirements.txt']
 
 
 # -- Options for HTML output -------------------------------------------------
@@ -49,8 +49,9 @@ exclude_patterns = ['_build', 'Thumbs.db', '.DS_Store']
 # The theme to use for HTML and HTML Help pages.  See the documentation for
 # a list of builtin themes.
 #
-html_theme = 'sphinx_rtd_theme'
-
+# html_theme = 'sphinx_rtd_theme'
+html_theme = 'furo'
+html_logo = "PIACERE_logo.png"
 # Add any paths that contain custom static files (such as style sheets) here,
 # relative to this directory. They are copied after the builtin static files,
 # so a file named "default.css" will overwrite the builtin "default.css".

docs/dict_reference.rst

+Reference for Attributes, Association and Classes keys
+======================================================
+
+Attributes
+----------
+
+commons_DOMLElement::name
+commons_DOMLElement::description
+commons_Property::key
+commons_IProperty::value
+commons_SProperty::value
+commons_FProperty::value
+commons_BProperty::value
+application_SoftwareComponent::isPersistent
+application_SoftwareComponent::licenseCost
+application_SoftwareComponent::configFile
+application_SaaS::licenseCost
+application_SoftwareInterface::endPoint
+infrastructure_ComputingNode::architecture
+infrastructure_ComputingNode::os
+infrastructure_ComputingNode::memory_mb
+infrastructure_ComputingNode::memory_kb
+infrastructure_ComputingNode::storage
+infrastructure_ComputingNode::cpu_count
+infrastructure_ComputingNode::cost
+infrastructure_VirtualMachine::sizeDescription
+infrastructure_Location::region
+infrastructure_Location::zone
+infrastructure_ComputingNodeGenerator::uri
+infrastructure_ComputingNodeGenerator::kind
+infrastructure_AutoScalingGroup::min
+infrastructure_AutoScalingGroup::max
+infrastructure_AutoScalingGroup::loadBalancer
+infrastructure_Storage::label
+infrastructure_Storage::size_gb
+infrastructure_Storage::cost
+infrastructure_FunctionAsAService::cost
+infrastructure_Network::protocol
+infrastructure_Network::address_lb
+infrastructure_Network::address_ub
+infrastructure_NetworkInterface::endPoint
+infrastructure_NetworkInterface::speed
+infrastructure_Rule::kind
+infrastructure_Rule::protocol
+infrastructure_Rule::fromPort
+infrastructure_Rule::toPort
+infrastructure_Rule::cidr
+infrastructure_KeyPair::user
+infrastructure_KeyPair::keyfile
+infrastructure_KeyPair::algorithm
+infrastructure_KeyPair::bits
+infrastructure_UserPass::username
+infrastructure_UserPass::password
+infrastructure_SwarmRole::kind
+concrete_ConcreteElement::configurationScript
+
+Associations
+------------
+
+commons_DOMLElement::annotations
+commons_Property::reference
+commons_Configuration::deployments
+commons_Deployment::component
+commons_Deployment::node
+application_ApplicationLayer::components
+application_SoftwareComponent::exposedInterfaces
+application_SoftwareComponent::consumedInterfaces
+application_SaaS::exposedInterfaces
+infrastructure_InfrastructureLayer::nodes
+infrastructure_InfrastructureLayer::generators
+infrastructure_InfrastructureLayer::storages
+infrastructure_InfrastructureLayer::faas
+infrastructure_InfrastructureLayer::credentials
+infrastructure_InfrastructureLayer::groups
+infrastructure_InfrastructureLayer::securityGroups
+infrastructure_InfrastructureLayer::networks
+infrastructure_ComputingNode::ifaces
+infrastructure_ComputingNode::location
+infrastructure_ComputingNode::credentials
+infrastructure_ComputingNode::group
+infrastructure_VirtualMachine::generatedFrom
+infrastructure_Container::generatedFrom
+infrastructure_Container::hosts
+infrastructure_VMImage::generatedVMs
+infrastructure_ContainerImage::generatedContainers
+infrastructure_AutoScalingGroup::machineDefinition
+infrastructure_AutoScalingGroup::deploymentNetwork
+infrastructure_AutoScalingGroup::securityGroup
+infrastructure_Storage::ifaces
+infrastructure_FunctionAsAService::ifaces
+infrastructure_Network::connectedIfaces
+infrastructure_Network::igws
+infrastructure_Network::subnets
+infrastructure_Subnet::connectedTo
+infrastructure_NetworkInterface::belongsTo
+infrastructure_NetworkInterface::associated
+infrastructure_ComputingGroup::groupedNodes
+infrastructure_SecurityGroup::rules
+infrastructure_SecurityGroup::ifaces
+infrastructure_SwarmRole::nodes
+infrastructure_Swarm::roles
+concrete_ConcreteInfrastructure::providers
+concrete_RuntimeProvider::vms
+concrete_RuntimeProvider::vmImages
+concrete_RuntimeProvider::containerImages
+concrete_RuntimeProvider::networks
+concrete_RuntimeProvider::storages
+concrete_RuntimeProvider::faas
+concrete_RuntimeProvider::group
+concrete_VirtualMachine::maps
+concrete_VMImage::maps
+concrete_ContainerImage::maps
+concrete_Network::maps
+concrete_Storage::maps
+concrete_FunctionAsAService::maps
+concrete_ComputingGroup::maps
+
+Classes
+-------
+
+commons_DOMLElement
+commons_Property
+commons_IProperty
+commons_SProperty
+commons_FProperty
+commons_BProperty
+commons_Configuration
+commons_Deployment
+application_ApplicationLayer
+application_ApplicationComponent
+application_SoftwareComponent
+application_SaaS
+application_SoftwareInterface
+application_DBMS
+application_SaaSDBMS
+infrastructure_InfrastructureLayer
+infrastructure_InfrastructureElement
+infrastructure_ComputingNode
+infrastructure_PhysicalComputingNode
+infrastructure_VirtualMachine
+infrastructure_Location
+infrastructure_Container
+infrastructure_ComputingNodeGenerator
+infrastructure_VMImage
+infrastructure_ContainerImage
+infrastructure_AutoScalingGroup
+infrastructure_Storage
+infrastructure_FunctionAsAService
+infrastructure_Network
+infrastructure_Subnet
+infrastructure_NetworkInterface
+infrastructure_InternetGateway
+infrastructure_ComputingGroup
+infrastructure_SecurityGroup
+infrastructure_Rule
+infrastructure_Credentials
+infrastructure_KeyPair
+infrastructure_UserPass
+infrastructure_SwarmRole
+infrastructure_Swarm
+infrastructure_ExtInfrastructureElement
+concrete_ConcreteInfrastructure
+concrete_ConcreteElement
+concrete_RuntimeProvider
+concrete_VirtualMachine
+concrete_VMImage
+concrete_ContainerImage
+concrete_Network
+concrete_Storage
+concrete_FunctionAsAService
+concrete_ComputingGroup
\ No newline at end of file

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.
@@ -60,3 +60,18 @@ Concrete Infrastructure Elements have a maps Association
   All elements in the active concretization are mapped to some abstract infrastructure element.
 
 Makes sure each concrete infrastructure element is mapped to a node in the Abstract Infrastructure Layer.
+
+Network Interfaces belong to a Security Group
+---------------------------------------------
+
+  All network interfaces belong to a security group.
+
+Makes sure all network interfaces have been configured to belong to a security group.
+This way, the user will be reminded to configure adequate rules for each network.
+
+External Services are reached through HTTPS
+-------------------------------------------
+
+  All external SaaS can be reached only through a secure connection.
+
+Makes sure that an HTTPS rule is enforced for a Network Interface of a Software Component that interfaces with a SaaS.
\ No newline at end of file

docs/requirements.txt

+furo
\ No newline at end of file

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 run separately::
+
+  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,62 @@ 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, 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, 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)
+======  =========================  =========  =================
+
+*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 -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** (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.
+
+Getting Started
+===============
+
+First, create a new file with a ``.domlr`` extension.
+
+If you use VS Code, there's a `Syntax Highlight`_ extension for it.
+
+Every user requirement file is a list of requirement::
+
+    + "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_count >= 4 
+        )
+    )
+    error: "A vm does lacks an associated interface or has less than 4 CPUs"
+
+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 **negative form**: the requirement is satisfied when its logic expression **is not** satisfied.
+
+    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 ``"..."``.
+    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, 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}``. 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`` 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_count >= 4`` is an **Attribute** Relationship, as it compares a property (``cpu_count``) 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_count >= 4`` compares attribute ``cpu_count`` with a numeric constant.
+        - ``vm1 has abstract.ComputingNode.cpu_count >= vm2 abstract.ComputingNode.cpu_count`` compares attribute ``cpu_count`` of ``vm1`` with the one of ``vm2``.
+
+
+
+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