Skip to content
Snippets Groups Projects
Commit 0f47f5c0 authored by aastorg2's avatar aastorg2
Browse files

Merge branch 'main' of gitlab.engr.illinois.edu:chsieh16/cs598mp-fall2021-proj into main

parents 20ac18c7 bb83193a
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 210 additions and 577 deletions
dataCollectedFrom20Rounds.sl deleted 100644 → 0
+ 0
− 40
View file @ 20ac18c7
(constraint (inShape 26.6152701008448 0.9678239104943458 0.21114638865049587 2.345564365386963 (- 0.14508944749832153)))
(constraint (inShape 26.61529433389539 0.967828326685563 0.21114590159461266 2.4930434226989746 (- 0.1531599760055542)))
(constraint (inShape 26.61534953561334 0.9678393284980444 0.21114628135388033 2.510728359222412 (- 0.15152986347675323)))
(constraint (inShape 19.375177724969767 0.967824356037088 0.21114631866326478 3.4791932106018066 (- 0.22473394870758057)))
(constraint (inShape 19.37517508326423 0.9678238569539328 0.21114658296554917 3.5184550285339355 (- 0.22579112648963928)))
(constraint (inShape 19.375182233263544 0.967825497133969 0.21114633517139236 3.5097079277038574 (- 0.2239835113286972)))
(constraint (inShape 19.37518834132608 0.9678268184284384 0.21114626941534817 3.5298871994018555 (- 0.22639496624469757)))
(constraint (inShape 10.235571424573456 0.9678239111315996 0.21114638837361643 3.438933849334717 (- 0.21554206311702728)))
(constraint (inShape 10.235571539824214 0.9678240672511116 0.21114626519871993 3.436929702758789 (- 0.21290093660354614)))
(constraint (inShape 10.235574707144886 0.9678247544784639 0.21114635158339712 3.445437431335449 (- 0.21383893489837646)))
(constraint (inShape 10.235580857800862 0.9678260840358703 0.21114631984957144 3.4564030170440674 (- 0.21499930322170258)))
(constraint (inShape 3.8539052024320735 0.9678239099543191 0.21114638869176813 1.4183670282363892 (- 0.09801661968231201)))
(constraint (inShape 3.8539075220129626 0.9678245456809051 0.2111461465021146 1.60621976852417 (- 0.11350981146097183)))
(constraint (inShape 3.8539106462580315 0.9678252255298361 0.21114641134134055 1.6671497821807861 (- 0.11667919158935547)))
(constraint (inShape 3.853916709485315 0.9678265364059513 0.2111463338846634 2.38948392868042 (- 0.1834786981344223)))
(constraint (inShape 2.148526343357085 0.9678239101001935 0.21114638873517305 3.5696678161621094 (- 0.2203296720981598)))
(constraint (inShape 2.148528512694049 0.9678245109850732 0.21114624022727377 3.563772678375244 (- 0.21956664323806763)))
(constraint (inShape 2.148531637917875 0.9678251862298772 0.2111463826103695 3.5739736557006836 (- 0.22020605206489563)))
(constraint (inShape 2.1485376981887327 0.9678264979904956 0.2111463365188309 3.59548282623291 (- 0.2222861349582672)))
(constraint (inShape 30.64333925200089 0.9678237509999992 0.211146388 3.3627007007598877 (- 0.2056111842393875)))
(constraint (not (inShape (- 0.13435869420323682) (- 1.899551057941262) (- 0.28484593314155127) 0.0 0.0)))
(constraint (not (inShape (- 0.1357230736889143) (- 0.06896000765390979) (- 0.22565356332402542) (- 0.13792001530781958) 0.0)))
(constraint (not (inShape 0.031336154284762455 (- 0.6144592699844698) 1.485540123743981 2.0 0.0)))
(constraint (not (inShape (- 0.13404045455201255) 2.0 (- 0.31717354626777816) 2.0 0.6343470925355563)))
(constraint (not (inShape 0.054857568457900144 (- 1.7840911757006543) (- 1.3634267523794492) 2.0 (- 0.9427623290582445))))
(constraint (not (inShape 0.08020144441406736 (- 0.1386182570450704) (- 1.5707963267948966) 2.0 (- 1.2772365140901407))))
(constraint (not (inShape 0.08020144441406737 1.1247414813760792 (- 1.5707963267948966) 2.0 (- 1.2494829627521584))))
(constraint (not (inShape 0.07880745577985629 1.9509699384018293 (- 1.5587035427760474) (- 1.1174070855520948) (- 1.0))))
(constraint (not (inShape (- 0.12497763257869772) (- 0.02210191139819711) (- 0.23609212684430714) 1.5278157463113857 (- 0.4721842536886143))))
(constraint (not (inShape (- 0.02352354216660577) 2.0 1.3555842891942411 0.2888314216115177 0.0)))
(constraint (not (inShape (- 0.12238683784721333) (- 0.03674154677771748) (- 0.1983859678838836) (- 1.983859678838836) 0.0)))
(constraint (not (inShape (- 0.040430820847654904) 0.0 0.6678319322055949 0.0 0.6643361355888102)))
(constraint (not (inShape (- 0.12031953894476077) 0.0 0.02539164591081542 2.0 (- 0.8730417704459228))))
(constraint (not (inShape (- 0.1103297666085696) 2.0 0.411967253854291 2.0 (- 0.05983626927145515))))
(constraint (not (inShape 0.0 0.5076765232177733 (- 1.0227481658397863) 2.0 (- 0.9846469535644533))))
(constraint (not (inShape (- 0.11974449498937859) 0.23016658550473063 (- 0.06536763447759253) 1.9346323655224076 1.5396668289905389)))
(constraint (not (inShape 0.08020144441406735 0.7075142733814768 (- 1.5707963267948966) (- 0.15576778003194303) (- 0.5849714532370465))))
(constraint (not (inShape 0.08005426932065733 0.5695169602836916 (- 1.5695169602836918) (- 2.0) (- 0.8609660794326169))))
(constraint (not (inShape 0.08020144441406735 1.451479337228988 (- 1.5707963267948966) (- 0.23863397913181705) (- 0.9029586744579761))))
(constraint (not (inShape (- 0.13373748526757237) 1.9998255257227473 (- 0.30976749003865545) 0.0 0.6195349800773109)))
dtree_learner.py
+ 22
− 11
View file @ 0f47f5c0
......@@ -127,17 +127,28 @@ class DTreeLearner(LearnerBase):
self._append_to_data_file(feature_vec_list, "true")
def add_negative_examples(self, *args) -> None:
for samp in args:
if samp in self.debug_neg_conc:
self.count_neg_dup += 1
raise ValueError("repeated negative example: " + str(samp))
perc_samp = tuple(self._s2f_func(samp))
if perc_samp in self.debug_neg_perc:
raise ValueError("repeated negative example: " + str(perc_samp))
self.debug_neg_perc.add(perc_samp)
self.debug_neg_conc.add(samp)
print(f"number of negative duplicate {self.count_neg_dup}")
# NOTE the size of nonrepeating_samp_list and nonrepeating_fv_list can be different.
if len(args) == 0:
return
nonrepeating_samp_list = [
samp for samp in args if samp not in self.debug_neg_conc
]
if len(nonrepeating_samp_list) == 0:
raise ValueError(f"All negative examples {args} are repeated.")
fv_list = [
tuple(self._s2f_func(samp)) for samp in nonrepeating_samp_list
]
nonrepeating_fv_list = [
fv for fv in fv_list if fv not in self.debug_neg_perc
]
if len(nonrepeating_fv_list) == 0:
raise ValueError(f"All negative feature vectors {fv_list} are repeated.")
self.debug_neg_perc.update(nonrepeating_fv_list)
self.debug_neg_conc.update(nonrepeating_samp_list)
# print(f"number of negative duplicate {self.count_neg_dup}")
feature_vec_list = [self._s2f_func(sample) for sample in args]
print("Negative feature vectors:", feature_vec_list)
......
dtree_synth.py 100644 → 100755
+ 145
− 33
View file @ 0f47f5c0
#!/usr/bin/env python3
import itertools
import json
import matplotlib.pyplot as plt
import pathlib
import pickle
from typing import List, Tuple
import traceback
from typing import Dict, Hashable, List, Tuple
import numpy as np
import z3
......@@ -18,56 +25,53 @@ def load_examples(file_name: str, spec) -> Tuple[List[Tuple[float, ...]], List[T
pos_exs, neg_exs, num_excl_exs = [], [], 0
for _, ss in truth_samples_seq:
for s in ss:
ret = spec(s)
if np.any(np.isnan(s)) or ret is None:
if np.any(np.isnan(s)):
num_excl_exs += 1
elif ret:
elif spec(s):
pos_exs.append(s)
else:
neg_exs.append(s)
print("# Exculded examples:", num_excl_exs)
print("# Exculded NaN examples:", num_excl_exs)
return pos_exs, neg_exs
def test_synth_dtree():
teacher = Teacher(norm_ord=1)
# 0.0 <= x <= 32.0 and -1.0 <= y <= -0.9 and 0.2 <= theta <= 0.22
""" Test using filtered data where we know an abstraction exists. """
# Initialize Teacher
teacher = Teacher(norm_ord=1, ultimate_bound=0.25)
teacher.set_old_state_bound(lb=[0.0, -1.0, 0.2], ub=[32.0, -0.9, 0.22])
# teacher.set_old_state_bound(lb=[0.0, -0.9, 2*np.pi/60], ub=[32.0, -0.6, 3*np.pi/60])
# teacher.set_old_state_bound(lb=[0.0, 0.3, 1*np.pi/60], ub=[32.0, 0.9, 5*np.pi/60])
positive_examples, negative_examples = load_examples(
# "data/800_truths-uniform_partition_4x20-1.2m-pi_12-one_straight_road-2021-10-27-08-49-17.bag.pickle",
init_positive_examples, init_negative_examples = load_examples(
"data/collect_images_2021-11-22-17-59-46.cs598.filtered.pickle",
teacher.is_positive_example)
print("# positive examples: %d" % len(positive_examples))
print("# negative examples: %d" % len(negative_examples))
ex_dim = len(positive_examples[0])
print("# positive examples: %d" % len(init_positive_examples))
print("# negative examples: %d" % len(init_negative_examples))
ex_dim = len(init_positive_examples[0])
print("Dimension of each example: %d" % ex_dim)
assert all(len(ex) == ex_dim and not any(np.isnan(ex))
for ex in positive_examples)
for ex in init_positive_examples)
assert teacher.state_dim + teacher.perc_dim == ex_dim
synth_dtree(positive_examples, negative_examples, teacher, num_max_iterations=2000)
def synth_dtree(positive_examples, negative_examples, teacher, num_max_iterations: int = 10):
# Initialize Learner
learner = Learner(state_dim=teacher.state_dim,
perc_dim=teacher.perc_dim, timeout=20000)
a_mat_0 = np.array([[0., -1., 0.],
[0., 0., -1.]])
a_mat_0 = Teacher.PERC_GT
b_vec_0 = np.zeros(2)
# Let z = [z_0, z_1] = [d, psi]; x = [x_0, x_1, x_2] = [x, y, theta]
# a_mat_0 @ [x, y, theta] + b_vec_0 = [-y, -theta]
# z - (a_mat_0 @ x + b_vec_0) = [d, psi] - [-y, -theta] = [d+y, psi+theta] defined as [fvar0_A0, fvar1_A0]
learner.set_grammar([(a_mat_0, b_vec_0)])
learner.add_positive_examples(*positive_examples)
learner.add_negative_examples(*negative_examples)
learner.add_positive_examples(*init_positive_examples)
learner.add_negative_examples(*init_negative_examples)
synth_dtree(learner, teacher, num_max_iterations=2000)
def synth_dtree(learner: Learner, teacher: Teacher, num_max_iterations: int = 10):
past_candidate_list = []
for k in range(num_max_iterations):
print("="*80)
......@@ -85,7 +89,7 @@ def synth_dtree(positive_examples, negative_examples, teacher, num_max_iteration
print(f"Satisfiability: {result}")
if result == z3.sat:
negative_examples = teacher.model()
# assert len(negative_examples) > 0
assert len(negative_examples) > 0
print(f"negative examples: {negative_examples}")
# assert validate_cexs(teacher.state_dim, teacher.perc_dim, candidate, negative_examples)
......@@ -94,15 +98,11 @@ def synth_dtree(positive_examples, negative_examples, teacher, num_max_iteration
continue
elif result == z3.unsat:
print("we are done!")
print(f"Simplified candidate: {z3.simplify(candidate)}")
return past_candidate_list
return True, (k, z3.simplify(candidate, arith_lhs=True).sexpr())
else:
print("Reason Unknown", teacher.reason_unknown())
return past_candidate_list
print("Reached max iteration %d." % num_max_iterations)
return False, f"Reason Unknown {teacher.reason_unknown()}"
return []
return False, f"Reached max iteration {num_max_iterations}."
def validate_cexs(state_dim: int, perc_dim: int,
......@@ -117,5 +117,117 @@ def validate_cexs(state_dim: int, perc_dim: int,
return False
def search_part(partition, state):
assert len(partition) == len(state)
bounds = []
for sorted_list, v in zip(partition, state):
i = np.searchsorted(sorted_list, v)
if i == 0 or i == len(sorted_list):
return None
bounds.append((sorted_list[i-1], sorted_list[i]))
return tuple(bounds)
def load_partitioned_examples(file_name: str, teacher: Teacher, partition) \
-> Dict[Hashable, Tuple[List[Tuple[float, ...]], List[Tuple[float, ...]], int]]:
print("Loading examples")
with open(file_name, "rb") as pickle_file_io:
pkl_data = pickle.load(pickle_file_io)
truth_samples_seq = pkl_data["truth_samples"]
bound_list = list(list(zip(x_arr[:-1], x_arr[1:])) for x_arr in partition)
ret = {part: [[], [], 0] for part in itertools.product(*bound_list)}
# Convert from sampled states and percepts to positive and negative examples for learning
num_excl_samples = 0
for _, ss in truth_samples_seq:
for s in ss:
state = s[0:teacher.state_dim]
part = search_part(partition, state)
if part is None:
num_excl_samples += 1
continue
if np.any(np.isnan(s)):
ret[part][2] += 1
elif teacher.is_positive_example(s):
ret[part][0].append(s)
else:
ret[part][1].append(s)
print("# excluded samples:", num_excl_samples)
return ret
def main():
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)
PKL_FILE_PATH = "data/800_truths-uniform_partition_4x20-1.2m-pi_12-one_straight_road-2021-10-27-08-49-17.bag.pickle"
NORM_ORD = 1
NUM_MAX_ITER = 500
teacher = Teacher(norm_ord=NORM_ORD)
part_to_examples = load_partitioned_examples(
file_name=PKL_FILE_PATH,
teacher=teacher, partition=PARTITION
)
result = []
for i, (part, (pos_exs, neg_exs, num_nan)) in enumerate(part_to_examples.items()):
print("#"*80)
print(f"# positive: {len(pos_exs)}; "
f"# negative: {len(neg_exs)}; "
f"# NaN: {num_nan}")
lb, ub = np.asfarray(part).T
# XXX Create new teacher and learner for each part to avoid solutions from other parts
# TODO incremental solving
teacher = Teacher(norm_ord=NORM_ORD)
teacher.set_old_state_bound(lb=lb, ub=ub)
learner = Learner(state_dim=teacher.state_dim,
perc_dim=teacher.perc_dim, timeout=20000)
learner.set_grammar([(Teacher.PERC_GT, np.zeros(2))])
learner.add_positive_examples(*pos_exs)
learner.add_negative_examples(*neg_exs)
try:
found, ret = synth_dtree(learner, teacher,
num_max_iterations=NUM_MAX_ITER)
print(f"Found? {found}")
if found:
k, expr = ret
result.append({"part": part,
"status": "found",
"result": {"k": k, "formula": expr}})
else:
result.append({"part": part,
"status": "not found",
"result": ret})
except Exception as e:
result.append({"part": part,
"status": "exception",
"result": traceback.format_exc()})
print(e)
finally:
data_file = pathlib.Path("out/pre.data")
data_file.rename(f"out/part-{i:03}-pre.data")
del teacher
del learner
with open(f"out/dtree_synth.{NUM_Y_PARTS}x{NUM_YAW_PARTS}.out.json", "w") as f:
json.dump(result, f)
if __name__ == "__main__":
test_synth_dtree()
# test_synth_dtree()
main()
dtree_teacher_gem_stanley.py
+ 5
− 4
View file @ 0f47f5c0
......@@ -72,12 +72,12 @@ class DTreeGEMStanleyGurobiTeacher(GEMStanleyGurobiTeacher):
else: # !(lhs <= rhs) <=> (lhs > rhs) => lhs >= rhs + ð
cons = (lhs >= rhs + self.PRECISION)
else:
raise RuntimeError(f"Unsupprted atomic predicate expression {pred}")
raise RuntimeError(f"Unsupported atomic predicate expression {pred}")
gp_cons = self._gp_model.addConstr(cons)
self._prev_candidate_constr.append(gp_cons)
def _candidate_to_conjucts(self, candidate: z3.BoolRef):
def _candidate_to_conjuncts(self, candidate: z3.BoolRef):
init_path = [candidate]
stack = [init_path]
while stack:
......@@ -117,7 +117,7 @@ class DTreeGEMStanleyGurobiTeacher(GEMStanleyGurobiTeacher):
def check(self, candidate: z3.BoolRef) -> z3.CheckSatResult:
self._cexs.clear()
conjunct_iter = self._candidate_to_conjucts(candidate)
conjunct_iter = self._candidate_to_conjuncts(candidate)
print("Checking candidate", flush=True)
for conjunct in conjunct_iter:
# print(".", end='', flush=True)
......@@ -138,7 +138,8 @@ class DTreeGEMStanleyGurobiTeacher(GEMStanleyGurobiTeacher):
if filtered_cex_list:
self._cexs.extend(filtered_cex_list)
else:
raise RuntimeError(f"Only found spurious cexs {cex_list} for the conjuct {conjunct}.")
# raise RuntimeError(f"Only found spurious cexs {cex_list} for the conjuct {conjunct}.")
pass
elif self._gp_model.status == gp.GRB.INFEASIBLE:
continue
......
firstpass.smt2 deleted 100644 → 0
+ 0
− 57
View file @ 20ac18c7
; (set-logic NRA)
(set-logic LRA)
; Variable declarations
(declare-fun a00 () Real)
(declare-fun a01 () Real)
(declare-fun b0 () Real)
(declare-fun a10 () Real)
(declare-fun a11 () Real)
(declare-fun b1 () Real)
(declare-fun radius () Real)
; Constraints
(assert (>= radius 0.0))
; (define-fun norm ((x Real) (y Real)) Real (+ (* x x) (* y y)))
(define-fun Abs ((x Real)) Real (ite (>= x 0) x (- x)))
(define-fun norm ((x Real) (y Real)) Real (+ (Abs x) (Abs y)))
(define-fun err ((x Real) (y Real)) Real (Abs x))
(define-fun transitionX ((x Real) (xP Real)) Real
(ite (> xP 0) (- x 1) (ite (= xP 0) x (+ x 1)))
)
(define-fun transitionY ((y Real) (yP Real)) Real
(ite (> yP 0) (- y 1) (ite (= yP 0) y (+ y 1)))
)
(define-fun inCircle ((x Real) (y Real) (xP Real) (yP Real)) Bool
(<=
(norm
(+ (- xP) (* 1 x) (* 0 y) b0)
(+ (- yP) (* 0 x) (* 1 y) b1)
)
radius
)
)
(assert (inCircle 1 1 1.2 0.8))
(assert (inCircle 10 -10 9 10.8))
; (assert (forall ((xx Real) (yy Real) (xxP Real) (yyP Real))
; (=>
; (and (inCircle xx yy xxP yyP) (>= xx 5) (>= yy 5))
; (<= (err (transitionX xx xxP) (transitionY yy yyP)) (err xx yy) )
; )
; ))
(apply (then qe nnf) :print false :print-benchmark true)
;(apply (! qe :qe-nonlinear true))
; Solve
(check-sat)
(get-model)
firstpass_learner.py deleted 100644 → 0
+ 0
− 194
View file @ 20ac18c7
from typing import MutableMapping, Sequence, Optional, Tuple
import numpy as np
import z3
from learner_base import Z3LearnerBase
def affine_transform(
x_vec: Sequence[z3.ExprRef],
z_vec: Sequence[z3.ExprRef],
a_mat: np.ndarray, b_vec: np.ndarray) -> Sequence[z3.ExprRef]:
num_rows = len(z_vec)
num_cols = len(x_vec)
assert len(a_mat.shape) == 2 and a_mat.shape == (num_rows, num_cols)
assert b_vec.shape[0] == num_rows
return [z_vec[i] -
z3.Sum(*(a_mat[i][j]*x_vec[j] for j in range(num_cols)), b_vec[i])
for i in range(num_rows)]
def abs_expr(expr: z3.ExprRef) -> z3.ExprRef:
return z3.If(expr >= 0, expr, -expr)
def l1_norm(*exprs: z3.ExprRef) -> z3.ExprRef:
return z3.Sum(*(abs_expr(expr) for expr in exprs))
def l2_norm(*exprs: z3.ExprRef) -> z3.ExprRef:
return z3.Sum(*(expr*expr for expr in exprs))
def max_expr(*exprs: z3.ExprRef) -> z3.ExprRef:
m = exprs[0]
for v in exprs[1:]:
m = z3.If(m >= v, m, v)
return m
def loo_norm(*exprs) -> z3.ExprRef:
return max_expr(*(abs_expr(expr) for expr in exprs))
class FirstpassLearner(Z3LearnerBase):
def __init__(self, state_dim, perc_dim, timeout=10000) -> None:
super().__init__(state_dim=state_dim, perc_dim=perc_dim,
timeout=timeout)
self._in_shape_pred: z3.ExprRef = z3.BoolVal(True)
self._part_affine_map: MutableMapping[int, Tuple] = {}
self.set_grammar(None)
@property
def num_shapes(self) -> int:
return len([l1_norm, l2_norm, loo_norm])
def set_grammar(self, grammar) -> None:
# TODO replace hardcoded grammar
self._in_shape_pred = self._in_shape_pred and self._get_shape_def(0)
def _get_shape_def(self, idx: int) -> z3.ExprRef:
norm_sel = z3.BoolVector("sel%d" % idx, self.num_shapes,
ctx=self._solver.ctx)
coeff_list = z3.Reals(["A%d__%d_%d" % (idx, i, j)
for i in range(self.perc_dim)
for j in range(self.state_dim)],
ctx=self._solver.ctx)
a_mat = np.array(coeff_list).reshape(self.perc_dim, self.state_dim)
b_vec = np.array(
z3.RealVector("b%d" % idx, self.perc_dim, ctx=self._solver.ctx))
radius = z3.Real("r%d" % idx, ctx=self._solver.ctx)
self._part_affine_map[idx] = (norm_sel, a_mat, b_vec, radius)
transformed_perc_seq = affine_transform(self._state_vars,
self._percept_vars,
a_mat, b_vec)
# Add axioms on each constant
self._solver.add(
z3.AtLeast(*norm_sel, 1),
radius >= 0)
# Return template predicate
return z3.And(
z3.Implies(norm_sel[0], l1_norm(*transformed_perc_seq) <= radius),
z3.Implies(norm_sel[1], l2_norm(*transformed_perc_seq) <= radius),
z3.Implies(norm_sel[2], loo_norm(*transformed_perc_seq) <= radius),
)
def add_positive_examples(self, *vals) -> None:
assert all(len(val) == self.state_dim+self.perc_dim for val in vals)
self._solver.add(*(
z3.simplify(z3.substitute_vars(self._in_shape_pred,
*(z3.RealVal(v) for v in val)))
for val in vals
))
def add_negative_examples(self, *vals) -> None:
assert all(len(val) == self.state_dim+self.perc_dim for val in vals)
self._solver.add(*(
z3.simplify(z3.Not(z3.substitute_vars(self._in_shape_pred,
*(z3.RealVal(v) for v in val))))
for val in vals
))
def add_implication_examples(self, *args) -> None:
return super().add_implication_examples(*args)
def learn(self) -> Optional[Tuple]:
res = self._solver.check()
if res == z3.sat:
z3_shape_sel, z3_a_mat, z3_b_vec, z3_radius = \
self._part_affine_map[0] # FIXME
m = self._solver.model()
# TODO: return integer is not that good
shape_sel = extract_shape_from_z3_model(m, z3_shape_sel)
a_mat = np.vectorize(extract_real_from_z3_model(m))(z3_a_mat)
b_vec = np.vectorize(extract_real_from_z3_model(m))(z3_b_vec)
radius = extract_real_from_z3_model(m)(z3_radius)
return shape_sel, a_mat, b_vec, radius
elif res == z3.unsat:
print("(unsat)")
return None
else:
print(self._solver.reason_unknown())
return None
def extract_shape_from_z3_model(
m: z3.ModelRef,
vars: Sequence[z3.ExprRef]) -> int:
for i, var in enumerate(vars):
if m.eval(var, True):
return i
raise RuntimeError("Z3 did not select a shape. "
"Check SMT encoding.")
def extract_real_from_z3_model(m: z3.ModelRef):
def to_float(var: z3.ExprRef) -> float:
x2 = m.eval(var, True).as_fraction()
return float(x2.numerator) / float(x2.denominator)
return to_float
def test_affine_transform():
state_vars = z3.RealVector("x", 3)
percept_vars = z3.RealVector("z", 2)
coeff_list = z3.Reals(["A__%d_%d" % (i, j)
for i in range(len(percept_vars))
for j in range(len(state_vars))])
coeff = np.array(coeff_list).reshape((len(percept_vars), len(state_vars)))
print(coeff)
intercept = np.array([7.0, 8.0])
ret = affine_transform(state_vars, coeff, intercept)
print(ret)
def test_norms():
state_vars = z3.RealVarVector(3)
ret = l1_norm(*(v + float(i) for i, v in enumerate(state_vars)))
print(ret)
ret = l2_norm(*(v + float(i) for i, v in enumerate(state_vars)))
print(ret)
ret = loo_norm(*(v for i, v in enumerate(state_vars)))
print(ret)
def test_firstpass_learner():
learner = FirstpassLearner(state_dim=2, perc_dim=2)
pos_examples = [
(10.0, -10.0, 11.0, -11.0),
(10.0, -10.0, 9.0, -9.0),
(1.0, 1.0, 1.5, 2.3),
]
learner.add_positive_examples(*pos_examples)
neg_examples = [
(1.0, 1.0, 0.5, 0.5),
(1.0, 1.0, 1.5, 1.5),
(9.0, 9.0, 5.0, 5.0),
]
learner.add_negative_examples(*neg_examples)
print(learner._solver.assertions())
print(learner.learn())
if __name__ == "__main__":
# test_affine_transform()
# test_norms()
test_firstpass_learner()
firstpass_learner.sl deleted 100644 → 0
+ 0
− 78
View file @ 20ac18c7
;; The background theory
(set-logic LRA)
(define-fun split ((x Real) (c Real) (then_pred Bool) (e1se_pred Bool)) Bool
(and (=> (>= x c) then_pred) (=> (<= x c) e1se_pred))
)
(define-fun Abs ((x Real)) Real (ite (>= x 0) x (- x) ))
(define-fun L1_norm ((x1 Real) (x2 Real)) Real (+ (Abs x1) (Abs x2))) ; diamond
(define-fun sqr ((x Real)) Real (* x x))
(define-fun L2_norm ((x1 Real) (x2 Real)) Real (+ (sqr x1) (sqr x2))) ; circle
(define-fun max ((x1 Real) (x2 Real)) Real (ite (>= x1 x2) x1 x2))
(define-fun Loo_norm ((x1 Real) (x2 Real)) Real (max (Abs x1) (Abs x2))) ; squares
(synth-fun inShape ((x1 Real) (x2 Real) (x3 Real) (z1 Real) (z2 Real)) Bool
;; Declare the non-terminals that would be used in the grammar
( (B Bool) (Dist Real) (X Real) (C Real))
(
(B Bool (
false
(<= Dist C)
;(split X C B B)
))
(Dist Real (
(L1_norm (- z1 (+ (* C x1) (* C x2) (* C x3) C) ) (- z2 (+ (* C x1) (* C x2) (* C x3) C)))
(L2_norm (- z1 (+ (* C x1) (* C x2) (* C x3) C) ) (- z2 (+ (* C x1) (* C x2) (* C x3) C)))
(Loo_norm (- z1 (+ (* C x1) (* C x2) (* C x3) C) ) (- z2 (+ (* C x1) (* C x2) (* C x3) C)))
; TODO ellipsoid norm can be done with an upper triangle matrix U by ||Uv|| <= r
)
)
(X Real (x1 x2))
(C Real ( (Constant Real) ))
)
)
; (declare-var x1 Real)
; (declare-var x2 Real)
; (declare-var z1 Real)
; (declare-var z2 Real)
;; Define the semantic constraints on the function
; (constraint (inShape 2.372100525863791 0.9678239108338289 0.21114638864503218 3.1077494621276855 (- 0.16957582533359528)) )
; (constraint (inShape 20.547616744645502 0.9678266805486828 0.21114634046254058 0.08310934901237488 (- 0.1517469435930252)) )
; (constraint (inShape 18.006150893559386 0.9678099296179283 0.21114528600009771 3.360142707824707 (- 0.1889626532793045)) )
;(constraint (not (inShape 1 1 0.5 0.5)))
;(constraint (not (inShape 1 1 1.5 1.5)))
; outputs (define-fun inShape ((x1 Real) (x2 Real) (z1 Real) (z2 Real)) Bool (<= (Loo_norm (- z1 (+ (* 0 x1) (* 0 x2) 6)) (- z2 (+ (* 0 x1) (* 1 x2) 0))) 5))
;(constraint (=> (<= (L2_norm (- z1 (+ (* 1 x1) (* 0 x2) 0)) (- z2 (+ (* 1 x1) (* 2 x2) 0))) 2) (inShape x1 x2 z1 z2) ) )
(constraint (inShape 4.765463957714702 (- 0.9678235924238532) 0.2111463885489226 0.9355837106704712 (- 0.21412937343120575)))
(constraint (inShape 4.765463632180135 (- 0.9678235315764336) 0.21114631398199063 0.8767245411872864 (- 0.20872043073177338)))
(constraint (inShape 4.765469434861616 (- 0.9678222760374098) 0.21114633781371142 0.8548175096511841 (- 0.20760071277618408)))
(constraint (inShape 4.765472132991584 (- 0.967821690209135) 0.2111463135604636 0.8481259346008301 (- 0.20709337294101715)))
(constraint (inShape 26.014448722969494 (- 0.9678236080554914) 0.21114638862599663 0.9063019752502441 (- 0.21251192688941956)))
(constraint (inShape 26.014445186473395 (- 0.9678243278961034) 0.21114665030099153 0.849083423614502 (- 0.20872122049331665)))
(constraint (inShape 26.01445259548303 (- 0.9678226318697245) 0.2111464041592506 0.8819234371185303 (- 0.2109939455986023)))
(constraint (inShape 26.014455372438157 (- 0.967822032009428) 0.21114628958749526 0.8592063784599304 (- 0.20877516269683838)))
(constraint (inShape 26.014460524474426 (- 0.9678209148025161) 0.21114630912352733 0.2559255361557007 (- 0.17408597469329834)))
(constraint (inShape 20.07743429421359 (- 0.9678235953796133) 0.21114638864717244 0.32362231612205505 (- 0.17972034215927124)))
(constraint (inShape 20.077401903788825 (- 0.9678294397256906) 0.21114585965862093 (- 0.6266307830810547) 0.04582478478550911))
(constraint (inShape 20.07744007331555 (- 0.9678222060049109) 0.21114636311895862 (- 0.6973455548286438) 0.04908551648259163))
(constraint (inShape 20.077442852607035 (- 0.9678216080262558) 0.21114631408943035 (- 0.6066773533821106) 0.04362167418003082))
(constraint (inShape 5.993772873635214 (- 0.9678235959898132) 0.2111463887360923 0.9497198462486267 (- 0.21268075704574585)))
(constraint (inShape 5.993775929900048 (- 0.9678227989056012) 0.21114617156117935 0.9282993674278259 (- 0.20913195610046387)))
(constraint (inShape 5.993781491794785 (- 0.9678215943141169) 0.21114627376922074 0.9325944781303406 (- 0.20973370969295502)))
(constraint (inShape 5.993784071107384 (- 0.9678210348414424) 0.21114634014029712 0.8477240204811096 (- 0.20398835837841034)))
(constraint (inShape 2.9876647902045153 (- 0.9678235940334616) 0.21114638864409163 0.8357511162757874 (- 0.20139506459236145)))
(constraint (inShape 2.987666363074242 (- 0.9678231185708412) 0.21114621408801454 0.8440750241279602 (- 0.20274119079113007)))
(constraint (inShape 2.987672058705376 (- 0.967821885735006) 0.2111463087908345 0.843758761882782 (- 0.20223206281661987)))
(constraint (not (inShape (- 0.07083899923294591) (- 1.995804969797873) (- 1.0402636607228553) 0.0 0.0)))
(constraint (not (inShape 0.05005137750787882 (- 1.985812931697809) (- 1.326396471233834) 0.0 (- 1.326396471233834))))
(constraint (not (inShape (- 0.13999904590704734) 0.0 0.0 0.0 0.0)))
(constraint (not (inShape (- 0.035084224611038786) (- 1.001789119936619) 1.313916457014109 0.0 0.0)))
(check-synth)
firstpass_teacher.py deleted 100755 → 0
+ 0
− 76
View file @ 20ac18c7
#!/usr/bin/env python3
import gurobipy as gp
from gurobipy import GRB
import numpy as np
import z3
from teacher_base import GurobiTeacherBase
class FirstpassTeacher(GurobiTeacherBase):
def __init__(self) -> None:
super().__init__("firstpass", 2, 2, 2)
def _add_system(self) -> None:
# Controller
for zi, ui in zip(self._percept.tolist(), self._control.tolist()):
self._gp_model.addGenConstrPWL(
zi, ui, [-10, 0, 0, 0, 10], [1, 1, 0, -1, -1])
# Dynamics
self._gp_model.addConstr(
self._new_state == self._old_state + self._control)
def _add_unsafe(self) -> None:
old_state = self._old_state.tolist()
new_state = self._new_state.tolist()
assert len(old_state) == len(new_state)
m = self._gp_model
m.update()
old_V, new_V = 0.0, 0.0
for old_xi, new_xi in zip(old_state, new_state):
old_var_name = "|%s|" % old_xi.VarName
old_abs_xi = m.addVar(name=old_var_name, **self.NNEGVAR)
m.addConstr(old_abs_xi == gp.abs_(old_xi))
old_V += old_abs_xi
new_var_name = "|%s|" % new_xi.VarName
new_abs_xi = m.addVar(name=new_var_name, **self.NNEGVAR)
m.addConstr(new_abs_xi == gp.abs_(new_xi))
new_V += new_abs_xi
# Tracking error is non-decreasing (UNSAFE)
m.addConstr(new_V >= old_V, name="Unstable")
CAND0_A = np.array([[0.0, -1.0],
[0.0, 1.0]])
CAND0_b = np.array([0.0, 0.0])
CAND0_r = 2.0
CAND0 = (2, CAND0_A, CAND0_b, CAND0_r)
CAND1_A = np.array([[1.0, 0.0],
[0.0, 1.0]])
CAND1_b = np.array([0.0, 0.0])
CAND1_r = 2.0
CAND1 = (1, CAND1_A, CAND1_b, CAND1_r)
def test_firstpass_teacher():
teacher = FirstpassTeacher()
teacher.set_old_state_bound(lb=[6.0, 5.0], ub=[11.0, 10.0])
result = teacher.check(CAND0)
teacher.dump_system_encoding()
result = teacher.check(CAND1)
teacher.dump_system_encoding("firstpass2")
print(result)
if result == z3.sat:
print(teacher.model())
elif result == z3.unsat:
print("candidate is verified")
else:
print(teacher.reason_unknown())
if __name__ == "__main__":
test_firstpass_teacher()
gem_stanley_teacher.py
+ 38
− 22
View file @ 0f47f5c0
......@@ -30,10 +30,6 @@ NEW_K_CTE_V_LIM = K_CTE_V_LIM + FORWARD_VEL * CYCLE_TIME * 1.0
NEW_ATAN_K_CTE_V_LIM = np.arctan(NEW_K_CTE_V_LIM)
NEW_RAW_ANG_ERR_LIM = ANG_LIM + FORWARD_VEL * CYCLE_TIME
# Ideal perception as a linear transform from state to ground truth percept
PERC_GT = np.array([[0., -1., 0.],
[0., 0., -1.]], float)
def z3_float64_const_to_real(v: float) -> z3.RatNumRef:
return z3.simplify(
......@@ -90,6 +86,10 @@ class GEMStanleyDRealTeacher(DRealTeacherBase):
class GEMStanleyGurobiTeacher(GurobiTeacherBase):
# Ideal perception as a linear transform from state to ground truth percept
PERC_GT = np.array([[0., -1., 0.],
[0., 0., -1.]], float)
@staticmethod
def is_spurious_example(state_dim: int, perc_dim: int, candidate: z3.BoolRef, cex: Tuple[float, ...]) -> bool:
state_subs_map = [(z3.Real(f"x_{i}"), z3_float64_const_to_real(cex[i])) for i in range(state_dim)]
......@@ -104,15 +104,18 @@ class GEMStanleyGurobiTeacher(GurobiTeacherBase):
else:
raise RuntimeError(f"Cannot validate negative example {cex} by substitution")
def __init__(self, name="gem_stanley", norm_ord=2) -> None:
def __init__(self, name="gem_stanley", norm_ord=2, ultimate_bound: float=0.0) -> None:
assert ultimate_bound >= 0.0
self._ultimate_bound = ultimate_bound
super().__init__(name=name,
state_dim=3, perc_dim=2, ctrl_dim=1, norm_ord=norm_ord)
def is_positive_example(self, ex) -> bool:
assert len(ex) == self.state_dim + self.perc_dim
def g(cte, phi):
error = phi + np.arctan(K_P*cte/FORWARD_VEL)
def g(cte, psi):
error = psi + np.arctan(K_P*cte/FORWARD_VEL)
steer = np.clip(error, -STEERING_LIM, STEERING_LIM)
return (steer,)
......@@ -122,13 +125,16 @@ class GEMStanleyGurobiTeacher(GurobiTeacherBase):
new_theta = theta + FORWARD_VEL*np.sin(steer)/WHEEL_BASE*CYCLE_TIME
return new_x, new_y, new_theta
def v(x, y, theta) -> float:
return np.linalg.norm([y, theta], ord=float(self._norm_ord))
def m_star(x, y, theta) -> Tuple[float, float]:
return -y, -theta
def v(cte, psi) -> float:
return np.linalg.norm([cte, psi], ord=float(self._norm_ord))
def spec(x, y, theta, d, phi) -> bool:
v_old = v(x, y, theta)
v_new = v(*f(x, y, theta, *g(d, phi)))
return v_new <= v_old
def spec(x, y, theta, cte, psi) -> bool:
v_old = v(*m_star(x, y, theta))
v_new = v(*m_star(*f(x, y, theta, *g(cte, psi))))
return v_new <= max(v_old, self._ultimate_bound)
return spec(*ex)
def _add_system(self) -> None:
......@@ -144,7 +150,7 @@ class GEMStanleyGurobiTeacher(GurobiTeacherBase):
m = self._gp_model
old_x, old_y, old_yaw = self._old_state.tolist()
new_x, new_y, new_yaw = self._new_state.tolist()
cte, phi = self._percept.tolist()
cte, psi = self._percept.tolist()
steering, = self._control.tolist()
# Controller
......@@ -156,7 +162,7 @@ class GEMStanleyGurobiTeacher(GurobiTeacherBase):
# Clip steering angle
error = m.addVar(name="(φ+atan(K*d/Vf))",
lb=-RAW_ANG_ERR_LIM, ub=RAW_ANG_ERR_LIM)
m.addConstr(error == phi + atan_K_cte_V)
m.addConstr(error == psi + atan_K_cte_V)
xpts = [-RAW_ANG_ERR_LIM, -STEERING_LIM, STEERING_LIM, RAW_ANG_ERR_LIM]
ypts = [-STEERING_LIM, -STEERING_LIM, STEERING_LIM, STEERING_LIM]
......@@ -183,19 +189,29 @@ class GEMStanleyGurobiTeacher(GurobiTeacherBase):
m.update()
def _add_unsafe(self) -> None:
assert PERC_GT.shape == (self.perc_dim, self.state_dim)
assert self.PERC_GT.shape == (self.perc_dim, self.state_dim)
# Variable Aliases
m = self._gp_model
# Add nonincreasing constraints
old_truth = m.addMVar(shape=(self.perc_dim,), name="m(x)", **self.FREEVAR)
m.addConstr(old_truth == PERC_GT @ self._old_state)
m.addConstr(old_truth == self.PERC_GT @ self._old_state)
old_lya_val = m.addVar(name="|m(x)|", vtype=gp.GRB.CONTINUOUS,
lb=0.0, ub=RAW_ANG_ERR_LIM)
m.addConstr(old_lya_val == gp.norm(old_truth, float(self._norm_ord)))
# Add ultimate bound
if self._ultimate_bound > 0:
bound_new_lya_val = m.addVar(name=f"max(|m(x)|,{self._ultimate_bound})",
vtype=gp.GRB.CONTINUOUS,
lb=0.0, ub=RAW_ANG_ERR_LIM)
m.addConstr(bound_new_lya_val == gp.max_(old_lya_val, constant=self._ultimate_bound))
else:
bound_new_lya_val = old_lya_val
new_truth = m.addMVar(shape=(self.perc_dim,), name="m(x')", **self.FREEVAR)
m.addConstr(new_truth == PERC_GT @ self._new_state)
m.addConstr(new_truth == self.PERC_GT @ self._new_state)
new_lya_val = m.addVar(name="|m(x')|", vtype=gp.GRB.CONTINUOUS,
lb=0.0, ub=NEW_RAW_ANG_ERR_LIM)
m.addConstr(new_lya_val == gp.norm(new_truth, float(self._norm_ord)))
......@@ -212,7 +228,7 @@ class GEMStanleyGurobiTeacher(GurobiTeacherBase):
# Add objective
norm_var = m.addVar(name="|z-m(x)|", **self.NNEGVAR)
m.addConstr(z_diff == z - PERC_GT @ x)
m.addConstr(z_diff == z - self.PERC_GT @ x)
m.addConstr(norm_var == gp.norm(z_diff, float(self._norm_ord)))
m.setObjective(norm_var, gp.GRB.MINIMIZE)
......@@ -249,10 +265,10 @@ class GEMStanleySymPyTeacher(SymPyTeacherBase):
# Variable Aliases
old_x, old_y, old_yaw = self._old_state
new_x, new_y, new_yaw = self._new_state
cte, phi = self._percept
cte, psi = self._percept
steering, = self._control
err = phi + sympy.atan2(cte*self.K_P, self.FORWARD_VEL)
err = psi + sympy.atan2(cte*self.K_P, self.FORWARD_VEL)
clipped_err = sympy.Piecewise(
(self.STEERING_LIM, err > self.STEERING_LIM),
(-self.STEERING_LIM, err < -self.STEERING_LIM),
......@@ -313,7 +329,7 @@ def test_gem_stanley_sympy_teacher():
def test_gem_stanley_gurobi_teacher():
teacher = GEMStanleyGurobiTeacher()
teacher = GEMStanleyGurobiTeacher(ultimate_bound=.4)
teacher.set_old_state_bound(
lb=(-np.inf, 0.5, 0.0625),
ub=(np.inf, 1.0, 0.25)
......
plot_abstractions.py deleted 100644 → 0
+ 0
− 60
View file @ 20ac18c7
from typing import List, Tuple
import numpy as np
import matplotlib.pyplot as plt
def plot_dtree_abs(state: np.ndarray, dnf: List[Tuple[np.ndarray, np.ndarray, np.ndarray, np.ndarray]]):
d_lim = 2.0 # PRE_Y_LIM
psi_lim = np.pi/3 # PRE_YAW_LIM
d_space = np.linspace(-d_lim, d_lim, 800)
psi_space = np.linspace(-psi_lim, psi_lim, 800)
d, psi = np.meshgrid(d_space, psi_space)
disjunct_bool_arr = np.zeros((len(d_space)*len(psi_space),))
for a_mat, b_vec, coeff_mat, cut_vec in dnf:
center = a_mat @ state + b_vec
dbar = d - center[0]
psibar = psi - center[1]
v_arr = np.dot(coeff_mat, [dbar.ravel(), psibar.ravel()])
bool_arr = np.all(v_arr.T <= cut_vec, axis=1)
disjunct_bool_arr = np.logical_or(disjunct_bool_arr, bool_arr)
disjunct_bool_arr = disjunct_bool_arr.reshape(d.shape)
im = plt.imshow(disjunct_bool_arr.astype(int),
extent=(d.min(), d.max(), psi.min(), psi.max()),
aspect="auto",
origin="lower", cmap="Greens")
plt.savefig("temp.png")
def plot_sygus_abs():
pass
state = np.array([0., 0., 0.])
a_mat_0 = np.array([[0., -1., 0.],
[0., 0., -1.]])
b_vec_0 = np.zeros(2)
coeff_mat_0 = np.array(
[[1., 1.],
[-1., 0.],
[0., 1.],
[1., -1.]])
coeff_mat_1 = np.array(
[[1., 0.],
[-1., 0.],
[0., 1.],
[0., -1.]])
cut_vec_0 = np.array(
[0.5, 0.5, 0.75, 0.75])
candidate_dnf_0 = [
# (a_mat_0, b_vec_0, coeff_mat_0, cut_vec_0),
(a_mat_0, b_vec_0, coeff_mat_1, cut_vec_0)
]
plot_dtree_abs(state, candidate_dnf_0)
region_synth.py
+ 0
− 2
View file @ 0f47f5c0
......@@ -6,9 +6,7 @@ import numpy as np
import z3
from z3 import *
#from firstpass_learner import FirstpassLearner as Learner
from sygus_learner import SygusLearner as Learner
# from firstpass_teacher import FirstpassTeacher as Teacher
from gem_stanley_teacher import GEMStanleyGurobiTeacher as Teacher
......
winnerDnf.pickle deleted 100644 → 0
+ 0
− 0
View file @ 20ac18c7
File deleted
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