search

xhajnal / DiPS

Multiple properties Probabilistic systems Model checker
BSD 3-Clause "New" or "Revised" License
4 stars 1 forks source link

probably refinement bug #48

Closed xhajnal closed 4 years ago

xhajnal commented 4 years ago

image2 while self.constraints ['r_0**2-2*r_0+1>=0.726166837943366', 'r_0**2-2*r_0+1<=0.907166495456634', '(-2)*If(r_0 + 1*delta > 1, 1, r_0 + 1*delta )*r_0+2*r_0>=0.0401642685583240', '(-2)*If(r_0 + 1*delta > 1, 1, r_0 + 1*delta )*r_0+2*r_0<=0.193169064841676', '(-1)*r_0**2+2*If(r_0 + 1*delta > 1, 1, r_0 + 1*delta )*r_0>=0.00536401422323720', '(-1)*r_0**2+2*If(r_0 + 1*delta > 1, 1, r_0 + 1*delta )*r_0<=0.127969319116763'] image3


data = [0.8166666667,
0.1166666667,
0.06666666667]

intervals = [(0.726166837943366, 0.907166495456634),
(0.0401642685583240, 0.193169064841676),
(0.00536401422323720, 0.127969319116763)]
xhajnal commented 4 years ago

delta assigned as 0.001 in one check_safe / check_unsafe hence the value assigned in constraints, solved only for z3 solver, global solution required