Skip to content
Snippets Groups Projects
Unverified Commit 1b5e449b authored by Andrea Franchini's avatar Andrea Franchini
Browse files

Remove stats module

parent d2a90631
No related branches found
No related tags found
No related merge requests found
......@@ -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...")
......
......@@ -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,
......
# 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
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment