diff --git a/mc_openapi/__main__.py b/mc_openapi/__main__.py index 42877c0d2501d435bb5d2555e8956b4049c89197..65143702bc94856cc0817a2aa5789d879cc1af34 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 90cb8367f9349bf2b2aa119332aa33c9a5431f0b..b07fa528a06b5ddcfa8ed0eaa53f1a5faafb26f7 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 560161ade9b339b29c008e3085bf2bc04474eb48..0000000000000000000000000000000000000000 --- 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