diff options
author | knm17 <knm17@ic.ac.uk> | 2019-09-11 12:54:49 +0100 |
---|---|---|
committer | Cristian Cadar <c.cadar@imperial.ac.uk> | 2020-01-17 18:36:56 +0000 |
commit | 17a08f63c157fae3ccd2065563664d4fa15c1fa2 (patch) | |
tree | 53ea8c5122fa3de844e12ce7656be85a614e5328 /tools | |
parent | 83c6487e68824453d961da874381231c58149f5e (diff) | |
download | klee-17a08f63c157fae3ccd2065563664d4fa15c1fa2.tar.gz |
Extended the grafana dashboard.
Added units for some of the data and modified klee-stats source code to provide solver time as a fraction of walltime along with fork, resolve and cexcache time.
Diffstat (limited to 'tools')
-rwxr-xr-x | tools/klee-stats/klee-stats | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/tools/klee-stats/klee-stats b/tools/klee-stats/klee-stats index 864e8993..6fc803b2 100755 --- a/tools/klee-stats/klee-stats +++ b/tools/klee-stats/klee-stats @@ -216,7 +216,6 @@ def grafana(dirs): sqlTarget = ",".join(["AVG( {0} )".format(t) for t in targets if t.isalnum()]) conn = sqlite3.connect(dr) - s = "SELECT WallTime + ? , {fields} " \ + " FROM stats" \ + " WHERE WallTime >= ? AND WallTime <= ?" \ @@ -229,7 +228,12 @@ def grafana(dirs): for line in cursor: unixtimestamp = int(line[0]) / 1000 #Convert from microsecond to miliseconds for field, datastream in zip(line[1:], result): - datastream["datapoints"].append([field, unixtimestamp]) + if "Time" in datastream["target"] and "Wall" not in datastream["target"]\ + and "User" not in datastream["target"]: + val = (field/(line[0]-startTime))*100 + datastream["datapoints"].append([val, unixtimestamp]) + else: + datastream["datapoints"].append([field, unixtimestamp]) ret = jsonify(result) return ret |