finalize GroverSym in _all and CAV23 with unittests

benchmarks/CAV23/SOGrover03/circuit.qasm → benchmarks/CAV23/GroverSym/03/circuit.qasm

@@ -10,9 +10,9 @@ h qubits[5];
 x qubits[3];
 x qubits[0];
 ccx qubits[0], qubits[1], qubits[2];
-ccx qubits[3], qubits[2], qubits[4];
+ccx qubits[2], qubits[3], qubits[4];
 cx qubits[4], qubits[5];
-ccx qubits[3], qubits[2], qubits[4];
+ccx qubits[2], qubits[3], qubits[4];
 ccx qubits[0], qubits[1], qubits[2];
 x qubits[3];
 x qubits[0];
@@ -34,9 +34,9 @@ h qubits[3];
 x qubits[3];
 x qubits[0];
 ccx qubits[0], qubits[1], qubits[2];
-ccx qubits[3], qubits[2], qubits[4];
+ccx qubits[2], qubits[3], qubits[4];
 cx qubits[4], qubits[5];
-ccx qubits[3], qubits[2], qubits[4];
+ccx qubits[2], qubits[3], qubits[4];
 ccx qubits[0], qubits[1], qubits[2];
 x qubits[3];
 x qubits[0];

benchmarks/CAV23/GroverSym/03/post.hsl

@@ -0,0 +1,6 @@
+Predicates
+pH := (and (> (* $R $R) 0.9) (= $I 0))
+Variable Order
+1 2 4 3 5 6
+Extended Dirac
+pH |010001>

benchmarks/CAV23/GroverSym/03/post.spec

@@ -0,0 +1,23 @@
+Predicates
+pL := (and (< (* $R $R) 0.1) (= $I 0))
+p0 := (and (= $R 0) (= $I 0))
+pH := (and (> (* $R $R) 0.9) (= $I 0))
+Root States 0
+Colored Transitions
+[1,1](2, 1) -> 0
+[2,1](3, 3) -> 1
+[2,1](3, 4) -> 2
+[3,1](6, 5) -> 3
+[3,1](7, 5) -> 4
+[4,1](8, 8) -> 5
+[4,1](9, 9) -> 6
+[4,1](10, 9) -> 7
+[5,1](11, 11) -> 8
+[5,1](12, 11) -> 9
+[5,1](13, 11) -> 10
+[6,1](14, 14) -> 11
+[6,1](14, 15) -> 12
+[6,1](14, 16) -> 13
+[p0,1] -> 14
+[pL,1] -> 15
+[pH,1] -> 16

benchmarks/CAV23/GroverSym/03/pre.hsl

@@ -0,0 +1,2 @@
+Extended Dirac
+|000000>

benchmarks/CAV23/GroverSym/03/pre.spec

@@ -0,0 +1,18 @@
+Constants
+c0 := 0
+c1 := 1
+Root States 0
+Colored Transitions
+[1,1](2, 1) -> 0
+[2,1](3, 3) -> 1
+[2,1](4, 3) -> 2
+[3,1](5, 5) -> 3
+[3,1](6, 5) -> 4
+[4,1](7, 7) -> 5
+[4,1](8, 7) -> 6
+[5,1](9, 9) -> 7
+[5,1](10, 9) -> 8
+[6,1](11, 11) -> 9
+[6,1](12, 11) -> 10
+[c0,1] -> 11
+[c1,1] -> 12