Skip to content
Snippets Groups Projects
Commit 471fc109 authored by chsieh16's avatar chsieh16
Browse files

Add Jupyter note book for parsing results

parent bb83193a
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
out/load_dtree_synth_json.ipynb 0 → 100644
+ 177
− 0
View file @ 471fc109
%% Cell type:code id: tags:
``` python
import json
import numpy as np
import pickle
import z3
STATE_DIM = 3
PERC_DIM = 2
filename = "dtree_synth.4x10.out.json"
with open(filename, "r") as f:
data = json.load(f)
found_dtree = [dict(part=entry["part"], **entry["result"]) for entry in data if entry["status"] == "found"]
print(len(found_dtree))
found, not_found, spur = 0, 0, 0
repeated_neg = 0
other = 0
for entry in data:
if entry["status"] == "found":
found += 1
elif entry["status"] == "not found":
not_found +=1
elif entry["status"] == "exception":
if "spurious cexs" in entry["result"]:
spur += 1
elif "repeated" in entry["result"]:
repeated_neg += 1
else:
other += 1
print(found, not_found, spur, repeated_neg, other)
```
%% Cell type:code id: tags:
``` python
def z3_float64_const_to_real(v: float) -> z3.RatNumRef:
return z3.simplify(
z3.fpToReal(z3.FPVal(v, z3.Float64()))
)
def in_part(state_arr, part_arr):
assert part_arr.shape == (len(state_arr), 2)
lb_arr, ub_arr = part_arr.T
return np.all(lb_arr <= state_arr) and np.all(state_arr <= ub_arr)
def calc_precision(part, z3_expr) -> float:
def in_z3_expr(sample, z3_expr) -> bool:
assert len(sample) == STATE_DIM + PERC_DIM
state_subs_map = [(z3.Real(f"x_{i}"), z3_float64_const_to_real(sample[i])) for i in range(STATE_DIM)]
perc_subs_map = [(z3.Real(f"z_{i}"), z3_float64_const_to_real(sample[i+STATE_DIM])) for i in range(PERC_DIM)]
sub_map = state_subs_map + perc_subs_map
val = z3.simplify(z3.substitute(z3_expr, *sub_map))
assert z3.is_bool(val)
if z3.is_false(val):
return False
elif z3.is_true(val):
return True
else:
raise RuntimeError(f"Cannot validate negative example {sample} by substitution")
pkl_name = "../data/800_truths-uniform_partition_4x20-1.2m-pi_12-one_straight_road-2021-10-27-08-49-17.bag.pickle"
with open(pkl_name, "rb") as f:
pkl_data = pickle.load(f)
truth_samples_seq = pkl_data["truth_samples"]
part_arr = np.asfarray(part)
num_pos, num_neg, num_nan = 0, 0, 0
for _, ss in truth_samples_seq:
for s in ss:
state_arr = np.asfarray(s[0:3])
if not in_part(state_arr, part_arr):
continue
# else:
if np.any(np.isnan(s)):
num_nan += 1
elif in_z3_expr(s, z3_expr):
num_pos += 1
else:
num_neg += 1
return num_pos, num_neg, num_nan
```
%% Cell type:code id: tags:
``` python
def visitor(e, seen):
if e in seen:
return
seen[e] = True
yield e
if z3.is_app(e):
for ch in e.children():
for e in visitor(ch, seen):
yield e
return
if z3.is_quantifier(e):
for e in visitor(e.body(), seen):
yield e
return
```
%% Cell type:code id: tags:
``` python
for result in found_dtree:
print(result['part'])
decls = {vname: z3.Real(vname) for vname in ["x_0", "x_1", "x_2", "z_0", "z_1"]}
smt2_str = f"(assert {result['formula']})"
z3_assertions = z3.parse_smt2_string(smt2_str, decls=decls)
z3_expr:z3.ExprRef = z3_assertions[0]
# print("#Atomic Predicates:", sum(z3.is_le(e) or z3.is_ge(e) for e in visitor(z3_expr, {})))
# print(z3_expr)
# Calculate the number of paths on a binary tree by adding one more path
# when there is an ite or a disjunction (due to simplification on ite).
# FIXME does not work if an ite expression is a common sub-expression of two paths.
num_paths = 1
for e in visitor(z3_expr, {}):
if z3.is_or(e) or z3.is_app_of(e, z3.Z3_OP_ITE):
num_paths += 1
print("#Paths:", num_paths)
num_pos, num_neg, num_nan = calc_precision(result['part'], z3_expr)
print(f"pos: {num_pos}; neg: {num_neg}; nan: {num_nan}")
print("precision (pos/(pos+neg)):", num_pos / (num_pos + num_neg) )
```
out/plot_feature_vectors.ipynb 0 → 100644
+ 134
− 0
View file @ 471fc109
%% Cell type:code id: tags:
``` python
import ast
import csv
import itertools
import matplotlib.pyplot as plt
import numpy as np
import pathlib
import re
X_LIM = np.inf
X_ARR = np.array([-X_LIM, X_LIM])
Y_LIM = 1.2
NUM_Y_PARTS = 4
Y_ARR = np.linspace(-Y_LIM, Y_LIM, NUM_Y_PARTS + 1)
YAW_LIM = np.pi / 12
NUM_YAW_PARTS = 10
YAW_ARR = np.linspace(-YAW_LIM, YAW_LIM, NUM_YAW_PARTS + 1)
PARTITION = (X_ARR, Y_ARR, YAW_ARR)
BOUND_LIST = list(list(zip(x_arr[:-1], x_arr[1:])) for x_arr in PARTITION)
PART_LIST = list(itertools.product(*BOUND_LIST))
```
%% Cell type:code id: tags:
``` python
from numpy import arange
from sympy import continued_fraction
csv_path_list = list(pathlib.Path(".").glob("part-???-pre.data"))
csv_path_list.sort()
for csv_path in csv_path_list:
m = re.match("^part-(?P<partid>\d+)-pre.data$", csv_path.name)
partid = int(m["partid"])
part_bnd = np.asfarray(PART_LIST[partid])
# Reset the plot
plt.gca().clear()
plt.gca().set_title(
f"x bound: {part_bnd[0]} (m)\n"
f"y bound: {part_bnd[1]} (m)\n"
f"θ bound: {np.rad2deg(part_bnd[2])} (deg)"
)
pos_fvs, neg_fvs = [], []
with open(csv_path, 'r') as csvfile:
csvreader = csv.reader(csvfile)
for entry in csvreader:
if entry[2].lower() == "true":
pos_fvs.append(tuple(ast.literal_eval(e) for e in entry[0:2]))
else:
assert entry[2].lower() == "false"
neg_fvs.append(tuple(ast.literal_eval(e) for e in entry[0:2]))
print(f"File: {csv_path.name}; #pos: {len(pos_fvs)}; #neg: {len(neg_fvs)}")
pos_fv_arr = np.asfarray(pos_fvs)
plt.scatter(pos_fv_arr[:, 0], pos_fv_arr[:, 1], c="g", marker="o", s=1)
neg_fv_arr = np.asfarray(neg_fvs)
plt.scatter(neg_fv_arr[:, 0], neg_fv_arr[:, 1], c="r", marker="x", s=1)
# dx = np.linspace(-1, 0.5,500)
# dy = np.linspace(-0.3, 0.5, 500)
# x,y = np.meshgrid(dx,dy)
# if partid == 16:
# region = (-3486699801877165/72057594037927936 < 1*y) & \
# ((2774949835903621/36028797018963968 >= (1*x + -1*y))
# &(-649018808849943/1125899906842624 < (1*x + -1*y))
# &( (4806281874582455/288230376151711744 >= (1*x + 1*y))
# | (2006731648131879/288230376151711744 >= 1*y)
# )
# )
# if partid == 0:
# region = ((y>-0.008467263) & (x+y>-0.7293049)).astype(int)
# plt.gca().set_xlim(-1, 1)
# plt.gca().set_xlim(-2.2, 0.2)
# elif partid == 9:
# region = (((x+y<=-1.141609) & (y>0.09126037)) | ((x+y>-1.141609) & (y>-0.1772965))).astype(int)
# plt.gca().set_xlim(-2.5, 2.5)
# plt.gca().set_ylim(-0.42, 0.25)
# elif partid == 17:
# region = ((y>-0.0121161) & (y<=0.02008105) & (x+y>-0.6796197) & (x+y<=0.05748017)).astype(int)
# plt.gca().set_xlim(-1, 1)
# plt.gca().set_ylim(-0.25, 0.25)
# else:
# pass
# plt.imshow( region,
# extent=(x.min(),x.max(),y.min(),y.max()),origin="lower", cmap="Greys", alpha = 0.3)
plt.savefig(csv_path.name + ".png")
```
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment