Add stats viewer

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...")
         

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)

mc_openapi/doml_mc/stats/__init__.py

+# 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

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])

mc_openapi/notebooks/stats.ipynb

+{
+ "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
+}