Initial commit.

.gitignore

+*~
+*__pycache__*

README.md

+# PIACERE Model Checker REST API server
+
+Thys project is packaged with Poetry.
+
+## Build and Run
+
+Build with
+```
+$ poetry install
+```
+then run with
+```
+poetry run python -m mc_openapi
+```
+
+Run tests with:
+```
+$ poetry run python -m pytest
+```
+
+## Run with uWSGI
+
+The project may be run with uWSGI as follows:
+```
+$ uwsgi --http :8080 -w mc_openapi.app_config -p 4
+```

mc_openapi/__init__.py

+__version__ = '0.1.0'

mc_openapi/__main__.py

+#!/usr/bin/env python3
+
+from mc_openapi.app_config import app
+
+app.run(port=8080)

mc_openapi/app_config.py

+import connexion
+
+app = connexion.App(__name__, specification_dir='openapi/')
+app.add_api('model_checker.yaml')
+
+application = app.app

mc_openapi/handlers.py

+import datetime
+
+def make_error(user_msg, debug_msg=None):
+    result = { "message": user_msg, "timestamp": datetime.now() }
+    if debug_msg is not None:
+        result["debug_message"] = debug_msg
+    return result
+
+def post(body):
+    if body["model"] is None:
+        return make_error("Model to be checked is missing."), 400
+    return  { "result": "dontknow" }

mc_openapi/openapi/model_checker.yaml

+openapi: 3.0.2
+info:
+  license:
+    name: Apache-2.0
+  title: PIACERE Model Checker
+  version: "1.0"
+paths:
+  /modelcheck:
+    post:
+      description: Send a DOML model in JSON format and a requirement to check.
+        The response says whether the requirement is satisfied by the model,
+        with a description of the issue if it is not.
+      operationId: mc_openapi.handlers.post
+      requestBody:
+        content:
+          application/json:
+            schema:
+              type: object
+              properties:
+                model:
+                  $ref: '#/components/schemas/doml'
+                requirement:
+                  type: string
+              required:
+                - model
+        required: true
+      responses:
+        "200":
+          content:
+            application/json:
+              schema:
+                type: object
+                properties:
+                  result:
+                    type: string
+                    enum:
+                      - sat
+                      - unsat
+                      - dontknow
+                  description:
+                    type: string
+                required:
+                  - result
+          description: OK - model checking succeded
+        "400":
+          content:
+            application/json:
+              schema:
+                $ref: '#/components/schemas/error'
+          description: malformed request
+        "500":
+          content:
+            application/json:
+              schema:
+                $ref: '#/components/schemas/error'
+          description: internal error
+components:
+  schemas:
+    doml:
+      type: object
+      additionalProperties: true
+    error:
+      type: object
+      properties:
+        timestamp:
+          type: string
+          format: date-time
+        message:
+          type: string
+          description: Error message for the user
+        debug_message:
+          type: string
+          description: Detailed error message for debugging purposes
+      required:
+        - timestamp
+        - message

pyproject.toml

+[tool.poetry]
+name = "mc_openapi"
+version = "0.1.0"
+description = "OpenAPI interface for the PIACERE DOML model checker."
+authors = ["Michele Chiari <michele.chiari@polimi.it>"]
+license = "Apache-2.0"
+
+[tool.poetry.dependencies]
+python = "^3.8"
+connexion = "^2.9.0"
+uWSGI = "^2.0.20"
+
+[tool.poetry.dev-dependencies]
+pytest = "^5.2"
+requests = "^2.26.0"
+
+[build-system]
+requires = ["poetry-core>=1.0.0"]
+build-backend = "poetry.core.masonry.api"

tests/test_mc_openapi.py

+from mc_openapi import __version__
+import requests
+
+def test_version():
+    assert __version__ == '0.1.0'
+
+def test_post():
+    r = requests.post("http://0.0.0.0:8080/modelcheck", json={'model': {'sbirio': 'frosco'}})
+    payload = r.json()
+    assert r.status_code == requests.codes.ok
+    assert payload["result"] is not None