finalize OEGrover in _all, LSTA and CAV23

benchmarks/CAV23/OEGrover/02/post.hsl

@@ -0,0 +1,4 @@
+Predicates
+p := (and (> (* real($) real($)) (* real(b) real(b))) (= imag($) 0))
+Extended Dirac
+p |011>

benchmarks/CAV23/OEGrover/02/post.spec

@@ -0,0 +1,14 @@
+Predicates
+p1 := (and (< (* $R $R) (* aR aR)) (= $I 0))
+p2 := (and (= $R 0) (= $I 0))
+p3 := (and (> (* $R $R) (* bR bR)) (= $I 0))
+Root States 0
+Colored Transitions
+[1,1](2, 1) -> 0
+[2,1](3, 3) -> 1
+[2,1](3, 4) -> 2
+[3,1](5, 6) -> 3
+[3,1](5, 7) -> 4
+[p2,1] -> 5
+[p1,1] -> 6
+[p3,1] -> 7

benchmarks/CAV23/OEGrover/02/pre.hsl

@@ -0,0 +1,8 @@
+Extended Dirac
+b |01> + a |*> # |1>
+Constraints
+3 * real(a) > real(b)
+real(a) > 0
+real(b) > 0
+imag(a) = 0
+imag(b) = 0

benchmarks/CAV23/OEGrover/02/pre.spec

@@ -0,0 +1,18 @@
+Constants
+c0 := 0
+Root States 0
+Colored Transitions
+[1,1](2, 1) -> 0
+[2,1](3, 3) -> 1
+[2,1](3, 4) -> 2
+[3,1](5, 6) -> 3
+[3,1](5, 7) -> 4
+[c0,1] -> 5
+[a,1] -> 6
+[b,1] -> 7
+Constraints
+3 * real(a) > real(b)
+real(a) > 0
+real(b) > 0
+imag(a) = 0
+imag(b) = 0

benchmarks/CAV23/OEGrover/100/post.hsl

@@ -0,0 +1,4 @@
+Predicates
+p := (and (> (* real($) real($)) (* real(b) real(b))) (= imag($) 0))
+Extended Dirac
+p |01010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101011000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000>