diff --git a/mc_openapi/__main__.py b/mc_openapi/__main__.py index cfcfda51f6989a5776383219eabfa7c28dbe9871..7d04f2fee0db4692e5c32c7a2245f3d11cefcd9b 100644 --- a/mc_openapi/__main__.py +++ b/mc_openapi/__main__.py @@ -17,6 +17,7 @@ from mc_openapi.doml_mc.imc import RequirementStore from mc_openapi.doml_mc.intermediate_model.metamodel import MetaModelDocs from mc_openapi.doml_mc.mc import ModelChecker from mc_openapi.doml_mc.mc_result import MCResult +from mc_openapi.doml_mc.stats import STATS from mc_openapi.doml_mc.xmi_parser.doml_model import get_pyecore_model parser = argparse.ArgumentParser() @@ -26,6 +27,7 @@ parser.add_argument("-V", "--doml-version", dest="doml_version", help="(optional 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)") parser.add_argument("-v", "--verbose", dest="verbose", action='store_true', help="print a detailed human-readable output of everything going on. Helpful for debugging.") +parser.add_argument("-z", "--stats", dest="stats", action='store_true', help="print stats of Z3 solver") # 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") @@ -134,14 +136,19 @@ else: res, msg = results.summarize() + print("[RESULT]") if res == MCResult.sat: print("sat") else: print(res.name) + print("[ERRORS]") print("\033[91m{}\033[00m".format(msg)) except RequirementException as e: print(e.message) + if args.stats: + STATS.print() + else: # Synthesis printv("Running synthesis...") diff --git a/mc_openapi/doml_mc/imc.py b/mc_openapi/doml_mc/imc.py index 9f3ba898da6e5c33e7afaf8d51ca1d0a1a0f1b86..3bab3f156537e1cd46cd7ed0498711895d2c213b 100644 --- a/mc_openapi/doml_mc/imc.py +++ b/mc_openapi/doml_mc/imc.py @@ -5,6 +5,8 @@ from typing import Literal from z3 import (Context, DatatypeSortRef, ExprRef, FuncDeclRef, Solver, SortRef, sat) +from mc_openapi.doml_mc.stats import STATS + from .intermediate_model.doml_element import IntermediateModel from .mc_result import MCResult, MCResults from .z3encoding.im_encoding import (assert_im_associations, @@ -170,4 +172,6 @@ class IntermediateModelChecker: )) self.solver.pop() + stats = self.solver.statistics() + STATS.add(stats) return MCResults(results) diff --git a/mc_openapi/doml_mc/stats/__init__.py b/mc_openapi/doml_mc/stats/__init__.py new file mode 100644 index 0000000000000000000000000000000000000000..560161ade9b339b29c008e3085bf2bc04474eb48 --- /dev/null +++ b/mc_openapi/doml_mc/stats/__init__.py @@ -0,0 +1,19 @@ +# Singleton: use this for stats caching/logging like behaviour + +import pandas as pd + +class Stats: + def __init__(self) -> None: + self.df = pd.DataFrame(columns=['memory', 'conflicts', 'quant instantiations']) + def add(self, stats): + keys = ['memory', 'conflicts', 'quant instantiations'] # set(self.df.columns) & set(stats.keys()) + stats = dict(zip(keys, [stats.get_key_value(x) for x in keys])) + + df2 = pd.DataFrame.from_records(stats, index=[0]) + self.df = pd.concat([self.df, df2]) + + def print(self): + print("[STATS]") + print(self.df.to_csv(index=False)) + +STATS = Stats() \ No newline at end of file diff --git a/mc_openapi/doml_mc/xmi_parser/special_parsers.py b/mc_openapi/doml_mc/xmi_parser/special_parsers.py index c215ceed787d02dea075861be48a17b795b48e9e..d523391c62cb04b6e138598a8f3d8d41672c047a 100644 --- a/mc_openapi/doml_mc/xmi_parser/special_parsers.py +++ b/mc_openapi/doml_mc/xmi_parser/special_parsers.py @@ -17,6 +17,8 @@ def parse_iface_address(addrport: str) -> Attributes: addr, _, port = addrport.rpartition(":") if addr == "": addr = port + if addr == "": + raise Exception(f"Interface address with value '{addrport}' is not valid. It should be 'x.x.x.x/cidr'.") return {"endPoint": [int(ip_address(addr))]} @@ -66,6 +68,12 @@ def init_special_parsers(): ("infrastructure_ComputingNode", "memory_mb"): parse_memory_mb, ("commons_FProperty", "value"): parse_fproperty, }, + DOMLVersion.V2_2_1: { + ("infrastructure_Network", "addressRange"): parse_cidr, + ("infrastructure_NetworkInterface", "endPoint"): parse_iface_address, + ("infrastructure_ComputingNode", "memory_mb"): parse_memory_mb, + ("commons_FProperty", "value"): parse_fproperty, + }, } for ver in DOMLVersion: SpecialParsers[ver] = SpecialParser(MetaModels[ver], attribute_parsers[ver]) diff --git a/mc_openapi/notebooks/stats.ipynb b/mc_openapi/notebooks/stats.ipynb new file mode 100644 index 0000000000000000000000000000000000000000..08318bbb50f864e2df5ce8456edd537b4b5e89ae --- /dev/null +++ b/mc_openapi/notebooks/stats.ipynb @@ -0,0 +1,297 @@ +{ + "cells": [ + { + "cell_type": "code", + "execution_count": 246, + "metadata": {}, + "outputs": [], + "source": [ + "PROJ_PATH = '/home/andrea/Projects/piacere-model-checker'\n", + "TESTS_PATH = PROJ_PATH + '/tests/doml/CaseStudies/*.domlx'" + ] + }, + { + "cell_type": "code", + "execution_count": 247, + "metadata": {}, + "outputs": [], + "source": [ + "from glob import glob" + ] + }, + { + "cell_type": "code", + "execution_count": 248, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "['/home/andrea/Projects/piacere-model-checker/tests/doml/CaseStudies/SIMPA_Validation_v2.domlx',\n", + " '/home/andrea/Projects/piacere-model-checker/tests/doml/CaseStudies/nio3_test_exec_env.domlx',\n", + " '/home/andrea/Projects/piacere-model-checker/tests/doml/CaseStudies/posidonia.domlx',\n", + " '/home/andrea/Projects/piacere-model-checker/tests/doml/CaseStudies/posidonia_IOP.domlx',\n", + " '/home/andrea/Projects/piacere-model-checker/tests/doml/CaseStudies/uc3-openstack_v2.domlx']" + ] + }, + "execution_count": 248, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "domlx_files = glob(TESTS_PATH)\n", + "\n", + "domlx_files" + ] + }, + { + "cell_type": "code", + "execution_count": 249, + "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "/home/andrea/Projects/piacere-model-checker\n", + "Using DOML v2.2.1\n", + "[RESULT]\n", + "unsat\n", + "[ERRORS]\n", + "\u001b[91m[Built-in]\n", + "Software component 'nio3_git' is not deployed to any abstract infrastructure node.\u001b[00m\n", + "[STATS]\n", + "memory,conflicts,quant instantiations\n", + "40.38,1273,1253\n", + "\n", + "\n", + "Using DOML v2.2.1\n", + "[RESULT]\n", + "sat\n", + "[STATS]\n", + "memory,conflicts,quant instantiations\n", + "43.29,2592,2614\n", + "\n", + "\n", + "Using DOML v2.2.1\n", + "[RESULT]\n", + "unsat\n", + "[ERRORS]\n", + "\u001b[91m[Built-in]\n", + "Virtual machine gestaut_vm is connected to no network interface.\n", + "Software components 'Database' and 'Gestaut' are supposed to communicate through interface 'dbAccess', but they are deployed to nodes that cannot communicate through a common network.\n", + "Abstract infrastructure element 'gestaut_vm' has not been mapped to any element in the active concretization.\n", + "Security group 'sg' is not associated with any network interface.\u001b[00m\n", + "[STATS]\n", + "memory,conflicts,quant instantiations\n", + "91.13,1875,2794\n", + "\n", + "\n", + "Using DOML v2.2.1\n", + "[RESULT]\n", + "unsat\n", + "[ERRORS]\n", + "\u001b[91m[Built-in]\n", + "Virtual machine gestaut_vm is connected to no network interface.\n", + "Software components 'Database' and 'Gestaut' are supposed to communicate through interface 'dbAccess', but they are deployed to nodes that cannot communicate through a common network.\n", + "Abstract infrastructure element 'gestaut_vm' has not been mapped to any element in the active concretization.\n", + "Security group 'sg' is not associated with any network interface.\u001b[00m\n", + "[STATS]\n", + "memory,conflicts,quant instantiations\n", + "91.45,1417,2263\n", + "\n", + "\n", + "Using DOML v2.2.1\n", + "[RESULT]\n", + "unsat\n", + "[ERRORS]\n", + "\u001b[91m[Built-in]\n", + "Security group 'sg' is not associated with any network interface.\u001b[00m\n", + "[STATS]\n", + "memory,conflicts,quant instantiations\n", + "91.29,7649,8422\n", + "\n", + "\n" + ] + }, + { + "data": { + "text/html": [ + "<div>\n", + "<style scoped>\n", + " .dataframe tbody tr th:only-of-type {\n", + " vertical-align: middle;\n", + " }\n", + "\n", + " .dataframe tbody tr th {\n", + " vertical-align: top;\n", + " }\n", + "\n", + " .dataframe thead th {\n", + " text-align: right;\n", + " }\n", + "</style>\n", + "<table border=\"1\" class=\"dataframe\">\n", + " <thead>\n", + " <tr style=\"text-align: right;\">\n", + " <th></th>\n", + " <th>filename</th>\n", + " <th>time</th>\n", + " <th>doml_ver</th>\n", + " <th>result</th>\n", + " <th>#error</th>\n", + " <th>memory</th>\n", + " <th>conflicts</th>\n", + " <th>quant inst</th>\n", + " </tr>\n", + " </thead>\n", + " <tbody>\n", + " <tr>\n", + " <th>0</th>\n", + " <td>SIMPA_Validation_v2.domlx</td>\n", + " <td>1.344904</td>\n", + " <td>2.2.1</td>\n", + " <td>unsat</td>\n", + " <td>3</td>\n", + " <td>40.38</td>\n", + " <td>1273</td>\n", + " <td>1253</td>\n", + " </tr>\n", + " <tr>\n", + " <th>0</th>\n", + " <td>nio3_test_exec_env.domlx</td>\n", + " <td>1.602703</td>\n", + " <td>2.2.1</td>\n", + " <td></td>\n", + " <td>2</td>\n", + " <td>43.29</td>\n", + " <td>2592</td>\n", + " <td>2614</td>\n", + " </tr>\n", + " <tr>\n", + " <th>0</th>\n", + " <td>posidonia.domlx</td>\n", + " <td>16.781076</td>\n", + " <td>2.2.1</td>\n", + " <td>unsat</td>\n", + " <td>6</td>\n", + " <td>91.13</td>\n", + " <td>1875</td>\n", + " <td>2794</td>\n", + " </tr>\n", + " <tr>\n", + " <th>0</th>\n", + " <td>posidonia_IOP.domlx</td>\n", + " <td>16.956536</td>\n", + " <td>2.2.1</td>\n", + " <td>unsat</td>\n", + " <td>6</td>\n", + " <td>91.45</td>\n", + " <td>1417</td>\n", + " <td>2263</td>\n", + " </tr>\n", + " <tr>\n", + " <th>0</th>\n", + " <td>uc3-openstack_v2.domlx</td>\n", + " <td>10.553367</td>\n", + " <td>2.2.1</td>\n", + " <td>unsat</td>\n", + " <td>3</td>\n", + " <td>91.29</td>\n", + " <td>7649</td>\n", + " <td>8422</td>\n", + " </tr>\n", + " </tbody>\n", + "</table>\n", + "</div>" + ], + "text/plain": [ + " filename time doml_ver result #error memory \\\n", + "0 SIMPA_Validation_v2.domlx 1.344904 2.2.1 unsat 3 40.38 \n", + "0 nio3_test_exec_env.domlx 1.602703 2.2.1 2 43.29 \n", + "0 posidonia.domlx 16.781076 2.2.1 unsat 6 91.13 \n", + "0 posidonia_IOP.domlx 16.956536 2.2.1 unsat 6 91.45 \n", + "0 uc3-openstack_v2.domlx 10.553367 2.2.1 unsat 3 91.29 \n", + "\n", + " conflicts quant inst \n", + "0 1273 1253 \n", + "0 2592 2614 \n", + "0 1875 2794 \n", + "0 1417 2263 \n", + "0 7649 8422 " + ] + }, + "execution_count": 249, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "import subprocess\n", + "import os\n", + "from time import time\n", + "import pandas as pd\n", + "\n", + "os.chdir(PROJ_PATH)\n", + "\n", + "print(os.getcwd())\n", + "\n", + "test_cmd = lambda file: f\"python -m mc_openapi -z -d {file}\"\n", + "\n", + "df = pd.DataFrame(columns=['filename', 'time', 'doml_ver', 'result', '#error', 'memory', 'conflicts', 'quant inst'])\n", + "\n", + "for file in domlx_files:\n", + "\n", + " filename = file.split(\"/\")[-1]\n", + "\n", + " # I know that using time is inaccurate, but it's simple and it works for generating simple benchmarks\n", + " start_time = time()\n", + " out = subprocess.run(test_cmd(file), shell=True, capture_output=True)\n", + " run_time = time() - start_time\n", + "\n", + " r = out.stdout.decode('utf-8')\n", + "\n", + " print(r)\n", + "\n", + " doml_ver, _, r = r.rpartition(\"[RESULT]\")\n", + " result, _, r = r.rpartition(\"[ERRORS]\")\n", + " errors, _, stats = r.rpartition(\"[STATS]\")\n", + " _, _, doml_ver = doml_ver.rpartition(\"v\")\n", + "\n", + " doml_ver = doml_ver.replace(\"\\n\", \"\")\n", + " result = result.replace(\"\\n\", \"\")\n", + " error_num = len(errors.split(\"\\n\")) - 1\n", + " stats = stats.split(\"\\n\")[2].split(\",\")[-3:]\n", + "\n", + " df2 = pd.DataFrame([[filename, run_time, doml_ver, result, error_num, *stats]], columns=df.columns)\n", + "\n", + " df = pd.concat([df, df2])\n", + "\n", + "df" + ] + } + ], + "metadata": { + "kernelspec": { + "display_name": ".venv", + "language": "python", + "name": "python3" + }, + "language_info": { + "codemirror_mode": { + "name": "ipython", + "version": 3 + }, + "file_extension": ".py", + "mimetype": "text/x-python", + "name": "python", + "nbconvert_exporter": "python", + "pygments_lexer": "ipython3", + "version": "3.11.2" + }, + "orig_nbformat": 4 + }, + "nbformat": 4, + "nbformat_minor": 2 +}