From 1b5e449bb73693a9595e8a9440ac4fa759ecbd31 Mon Sep 17 00:00:00 2001
From: Andrea Franchini <hello@andreafranchini.com>
Date: Wed, 22 Mar 2023 11:41:35 +0100
Subject: [PATCH] Remove stats module
---
mc_openapi/__main__.py | 5 -----
mc_openapi/doml_mc/imc.py | 2 --
mc_openapi/doml_mc/stats/__init__.py | 19 -------------------
3 files changed, 26 deletions(-)
delete mode 100644 mc_openapi/doml_mc/stats/__init__.py
diff --git a/mc_openapi/__main__.py b/mc_openapi/__main__.py
index 42877c0..6514370 100644
--- a/mc_openapi/__main__.py
+++ b/mc_openapi/__main__.py
@@ -17,7 +17,6 @@ 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()
@@ -27,7 +26,6 @@ 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")
@@ -146,9 +144,6 @@ else:
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 90cb836..b07fa52 100644
--- a/mc_openapi/doml_mc/imc.py
+++ b/mc_openapi/doml_mc/imc.py
@@ -5,8 +5,6 @@ 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,
diff --git a/mc_openapi/doml_mc/stats/__init__.py b/mc_openapi/doml_mc/stats/__init__.py
deleted file mode 100644
index 560161a..0000000
--- a/mc_openapi/doml_mc/stats/__init__.py
+++ /dev/null
@@ -1,19 +0,0 @@
-# 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
--
GitLab