From 471fc10988f4f74be6e6fe25cb3c8d4eacce4932 Mon Sep 17 00:00:00 2001
From: "Hsieh, Chiao" <chsieh16@illinois.edu>
Date: Thu, 1 Sep 2022 23:01:47 -0500
Subject: [PATCH] Add Jupyter note book for parsing results
---
out/load_dtree_synth_json.ipynb | 177 ++++++++++++++++++++++++++++++++
out/plot_feature_vectors.ipynb | 134 ++++++++++++++++++++++++
2 files changed, 311 insertions(+)
create mode 100644 out/load_dtree_synth_json.ipynb
create mode 100644 out/plot_feature_vectors.ipynb
diff --git a/out/load_dtree_synth_json.ipynb b/out/load_dtree_synth_json.ipynb
new file mode 100644
index 0000000..71b880f
--- /dev/null
+++ b/out/load_dtree_synth_json.ipynb
@@ -0,0 +1,177 @@
+{
+ "cells": [
+ {
+ "cell_type": "code",
+ "execution_count": null,
+ "metadata": {},
+ "outputs": [],
+ "source": [
+ "import json\n",
+ "import numpy as np\n",
+ "import pickle\n",
+ "import z3\n",
+ "\n",
+ "STATE_DIM = 3\n",
+ "PERC_DIM = 2\n",
+ "\n",
+ "filename = \"dtree_synth.4x10.out.json\"\n",
+ "\n",
+ "with open(filename, \"r\") as f:\n",
+ " data = json.load(f)\n",
+ "\n",
+ "found_dtree = [dict(part=entry[\"part\"], **entry[\"result\"]) for entry in data if entry[\"status\"] == \"found\"]\n",
+ "print(len(found_dtree))\n",
+ "\n",
+ "found, not_found, spur = 0, 0, 0\n",
+ "repeated_neg = 0\n",
+ "other = 0\n",
+ "for entry in data:\n",
+ " if entry[\"status\"] == \"found\":\n",
+ " found += 1\n",
+ " elif entry[\"status\"] == \"not found\":\n",
+ " not_found +=1\n",
+ " elif entry[\"status\"] == \"exception\":\n",
+ " if \"spurious cexs\" in entry[\"result\"]:\n",
+ " spur += 1\n",
+ " elif \"repeated\" in entry[\"result\"]:\n",
+ " repeated_neg += 1\n",
+ " else:\n",
+ " other += 1\n",
+ "print(found, not_found, spur, repeated_neg, other)"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": null,
+ "metadata": {},
+ "outputs": [],
+ "source": [
+ "def z3_float64_const_to_real(v: float) -> z3.RatNumRef:\n",
+ " return z3.simplify(\n",
+ " z3.fpToReal(z3.FPVal(v, z3.Float64()))\n",
+ " )\n",
+ "\n",
+ "def in_part(state_arr, part_arr):\n",
+ " assert part_arr.shape == (len(state_arr), 2)\n",
+ " lb_arr, ub_arr = part_arr.T\n",
+ " return np.all(lb_arr <= state_arr) and np.all(state_arr <= ub_arr)\n",
+ "\n",
+ "def calc_precision(part, z3_expr) -> float:\n",
+ " def in_z3_expr(sample, z3_expr) -> bool:\n",
+ " assert len(sample) == STATE_DIM + PERC_DIM\n",
+ " state_subs_map = [(z3.Real(f\"x_{i}\"), z3_float64_const_to_real(sample[i])) for i in range(STATE_DIM)]\n",
+ " perc_subs_map = [(z3.Real(f\"z_{i}\"), z3_float64_const_to_real(sample[i+STATE_DIM])) for i in range(PERC_DIM)]\n",
+ " sub_map = state_subs_map + perc_subs_map\n",
+ " val = z3.simplify(z3.substitute(z3_expr, *sub_map))\n",
+ " assert z3.is_bool(val)\n",
+ " if z3.is_false(val):\n",
+ " return False\n",
+ " elif z3.is_true(val):\n",
+ " return True\n",
+ " else:\n",
+ " raise RuntimeError(f\"Cannot validate negative example {sample} by substitution\")\n",
+ "\n",
+ " pkl_name = \"../data/800_truths-uniform_partition_4x20-1.2m-pi_12-one_straight_road-2021-10-27-08-49-17.bag.pickle\"\n",
+ " with open(pkl_name, \"rb\") as f:\n",
+ " pkl_data = pickle.load(f)\n",
+ " truth_samples_seq = pkl_data[\"truth_samples\"]\n",
+ "\n",
+ " part_arr = np.asfarray(part)\n",
+ " num_pos, num_neg, num_nan = 0, 0, 0\n",
+ " for _, ss in truth_samples_seq:\n",
+ " for s in ss:\n",
+ " state_arr = np.asfarray(s[0:3])\n",
+ " if not in_part(state_arr, part_arr):\n",
+ " continue\n",
+ " # else:\n",
+ " if np.any(np.isnan(s)):\n",
+ " num_nan += 1\n",
+ " elif in_z3_expr(s, z3_expr):\n",
+ " num_pos += 1\n",
+ " else:\n",
+ " num_neg += 1\n",
+ " return num_pos, num_neg, num_nan"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": null,
+ "metadata": {},
+ "outputs": [],
+ "source": [
+ "def visitor(e, seen):\n",
+ " if e in seen:\n",
+ " return\n",
+ " seen[e] = True\n",
+ " yield e\n",
+ " if z3.is_app(e):\n",
+ " for ch in e.children():\n",
+ " for e in visitor(ch, seen):\n",
+ " yield e\n",
+ " return\n",
+ " if z3.is_quantifier(e):\n",
+ " for e in visitor(e.body(), seen):\n",
+ " yield e\n",
+ " return"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": null,
+ "metadata": {},
+ "outputs": [],
+ "source": [
+ "for result in found_dtree:\n",
+ " print(result['part'])\n",
+ " decls = {vname: z3.Real(vname) for vname in [\"x_0\", \"x_1\", \"x_2\", \"z_0\", \"z_1\"]}\n",
+ " smt2_str = f\"(assert {result['formula']})\"\n",
+ "\n",
+ " z3_assertions = z3.parse_smt2_string(smt2_str, decls=decls)\n",
+ " z3_expr:z3.ExprRef = z3_assertions[0]\n",
+ " # print(\"#Atomic Predicates:\", sum(z3.is_le(e) or z3.is_ge(e) for e in visitor(z3_expr, {})))\n",
+ " # print(z3_expr)\n",
+ "\n",
+ " # Calculate the number of paths on a binary tree by adding one more path\n",
+ " # when there is an ite or a disjunction (due to simplification on ite).\n",
+ " # FIXME does not work if an ite expression is a common sub-expression of two paths.\n",
+ " num_paths = 1\n",
+ " for e in visitor(z3_expr, {}):\n",
+ " if z3.is_or(e) or z3.is_app_of(e, z3.Z3_OP_ITE):\n",
+ " num_paths += 1\n",
+ "\n",
+ " print(\"#Paths:\", num_paths)\n",
+ "\n",
+ " num_pos, num_neg, num_nan = calc_precision(result['part'], z3_expr)\n",
+ " print(f\"pos: {num_pos}; neg: {num_neg}; nan: {num_nan}\")\n",
+ " print(\"precision (pos/(pos+neg)):\", num_pos / (num_pos + num_neg) )\n"
+ ]
+ }
+ ],
+ "metadata": {
+ "kernelspec": {
+ "display_name": "Python 3.8.10 64-bit",
+ "language": "python",
+ "name": "python3"
+ },
+ "language_info": {
+ "codemirror_mode": {
+ "name": "ipython",
+ "version": 3
+ },
+ "file_extension": ".py",
+ "mimetype": "text/x-python",
+ "name": "python",
+ "nbconvert_exporter": "python",
+ "pygments_lexer": "ipython3",
+ "version": "3.8.10"
+ },
+ "orig_nbformat": 4,
+ "vscode": {
+ "interpreter": {
+ "hash": "e7370f93d1d0cde622a1f8e1c04877d8463912d04d973331ad4851f04de6915a"
+ }
+ }
+ },
+ "nbformat": 4,
+ "nbformat_minor": 2
+}
diff --git a/out/plot_feature_vectors.ipynb b/out/plot_feature_vectors.ipynb
new file mode 100644
index 0000000..d7a98f8
--- /dev/null
+++ b/out/plot_feature_vectors.ipynb
@@ -0,0 +1,134 @@
+{
+ "cells": [
+ {
+ "cell_type": "code",
+ "execution_count": null,
+ "metadata": {},
+ "outputs": [],
+ "source": [
+ "import ast\n",
+ "import csv\n",
+ "import itertools\n",
+ "import matplotlib.pyplot as plt\n",
+ "import numpy as np\n",
+ "import pathlib\n",
+ "import re\n",
+ "\n",
+ "X_LIM = np.inf\n",
+ "X_ARR = np.array([-X_LIM, X_LIM])\n",
+ "\n",
+ "Y_LIM = 1.2\n",
+ "NUM_Y_PARTS = 4\n",
+ "Y_ARR = np.linspace(-Y_LIM, Y_LIM, NUM_Y_PARTS + 1)\n",
+ "\n",
+ "YAW_LIM = np.pi / 12\n",
+ "NUM_YAW_PARTS = 10\n",
+ "YAW_ARR = np.linspace(-YAW_LIM, YAW_LIM, NUM_YAW_PARTS + 1)\n",
+ "\n",
+ "PARTITION = (X_ARR, Y_ARR, YAW_ARR)\n",
+ "BOUND_LIST = list(list(zip(x_arr[:-1], x_arr[1:])) for x_arr in PARTITION)\n",
+ "PART_LIST = list(itertools.product(*BOUND_LIST))"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": null,
+ "metadata": {},
+ "outputs": [],
+ "source": [
+ "from numpy import arange\n",
+ "from sympy import continued_fraction\n",
+ "\n",
+ "\n",
+ "csv_path_list = list(pathlib.Path(\".\").glob(\"part-???-pre.data\"))\n",
+ "csv_path_list.sort()\n",
+ "for csv_path in csv_path_list:\n",
+ " m = re.match(\"^part-(?P<partid>\\d+)-pre.data$\", csv_path.name)\n",
+ " partid = int(m[\"partid\"])\n",
+ " part_bnd = np.asfarray(PART_LIST[partid])\n",
+ "\n",
+ " # Reset the plot\n",
+ " plt.gca().clear()\n",
+ " plt.gca().set_title(\n",
+ " f\"x bound: {part_bnd[0]} (m)\\n\"\n",
+ " f\"y bound: {part_bnd[1]} (m)\\n\"\n",
+ " f\"θ bound: {np.rad2deg(part_bnd[2])} (deg)\"\n",
+ " )\n",
+ "\n",
+ " pos_fvs, neg_fvs = [], []\n",
+ "\n",
+ " with open(csv_path, 'r') as csvfile:\n",
+ " csvreader = csv.reader(csvfile)\n",
+ " for entry in csvreader:\n",
+ " if entry[2].lower() == \"true\":\n",
+ " pos_fvs.append(tuple(ast.literal_eval(e) for e in entry[0:2]))\n",
+ " else:\n",
+ " assert entry[2].lower() == \"false\"\n",
+ " neg_fvs.append(tuple(ast.literal_eval(e) for e in entry[0:2]))\n",
+ " print(f\"File: {csv_path.name}; #pos: {len(pos_fvs)}; #neg: {len(neg_fvs)}\")\n",
+ "\n",
+ " pos_fv_arr = np.asfarray(pos_fvs)\n",
+ " plt.scatter(pos_fv_arr[:, 0], pos_fv_arr[:, 1], c=\"g\", marker=\"o\", s=1)\n",
+ "\n",
+ " neg_fv_arr = np.asfarray(neg_fvs)\n",
+ " plt.scatter(neg_fv_arr[:, 0], neg_fv_arr[:, 1], c=\"r\", marker=\"x\", s=1)\n",
+ "\n",
+ " # dx = np.linspace(-1, 0.5,500)\n",
+ " # dy = np.linspace(-0.3, 0.5, 500)\n",
+ " # x,y = np.meshgrid(dx,dy)\n",
+ " # if partid == 16:\n",
+ " # region = (-3486699801877165/72057594037927936 < 1*y) & \\\n",
+ " # ((2774949835903621/36028797018963968 >= (1*x + -1*y))\n",
+ " # &(-649018808849943/1125899906842624 < (1*x + -1*y))\n",
+ " # &( (4806281874582455/288230376151711744 >= (1*x + 1*y))\n",
+ " # | (2006731648131879/288230376151711744 >= 1*y)\n",
+ " # )\n",
+ " # )\n",
+ " # if partid == 0:\n",
+ " # region = ((y>-0.008467263) & (x+y>-0.7293049)).astype(int)\n",
+ " # plt.gca().set_xlim(-1, 1)\n",
+ " # plt.gca().set_xlim(-2.2, 0.2)\n",
+ " # elif partid == 9:\n",
+ " # region = (((x+y<=-1.141609) & (y>0.09126037)) | ((x+y>-1.141609) & (y>-0.1772965))).astype(int)\n",
+ " # plt.gca().set_xlim(-2.5, 2.5)\n",
+ " # plt.gca().set_ylim(-0.42, 0.25)\n",
+ " # elif partid == 17: \n",
+ " # region = ((y>-0.0121161) & (y<=0.02008105) & (x+y>-0.6796197) & (x+y<=0.05748017)).astype(int)\n",
+ " # plt.gca().set_xlim(-1, 1)\n",
+ " # plt.gca().set_ylim(-0.25, 0.25)\n",
+ " # else:\n",
+ " # pass\n",
+ " # plt.imshow( region, \n",
+ " # extent=(x.min(),x.max(),y.min(),y.max()),origin=\"lower\", cmap=\"Greys\", alpha = 0.3)\n",
+ " plt.savefig(csv_path.name + \".png\")"
+ ]
+ }
+ ],
+ "metadata": {
+ "kernelspec": {
+ "display_name": "Python 3.8.10 64-bit",
+ "language": "python",
+ "name": "python3"
+ },
+ "language_info": {
+ "codemirror_mode": {
+ "name": "ipython",
+ "version": 3
+ },
+ "file_extension": ".py",
+ "mimetype": "text/x-python",
+ "name": "python",
+ "nbconvert_exporter": "python",
+ "pygments_lexer": "ipython3",
+ "version": "3.8.10"
+ },
+ "orig_nbformat": 4,
+ "vscode": {
+ "interpreter": {
+ "hash": "e7370f93d1d0cde622a1f8e1c04877d8463912d04d973331ad4851f04de6915a"
+ }
+ }
+ },
+ "nbformat": 4,
+ "nbformat_minor": 2
+}
--
GitLab