@@ -122,21 +122,22 @@ def contain_all_fix(reach1: Dict[int, List[List[float]]], reach2: Dict[int, List
122
122
in_r1 = Or () #just set this boolean statement to just Or for now, can sub with Or(False) if having issues
123
123
in_r2 = Or () #as above, sub with Or(False) if having issues
124
124
s = Solver ()
125
- for node in nodes : # for each node
125
+ # print(reach1, reach2[5][3], reach2[5][5], reach2[6][3], reach2[6][5])
126
+ for node in reach1 : # for each node
126
127
for i in range (0 , len (reach1 [node ]), 2 ): # for each vertex in the node
127
128
includes = And ()
128
129
hr = [reach1 [node ][i ], reach1 [node ][i + 1 ]] # clarifies expressions and matches logic with contain_all
129
130
for j in range (state_len ):
130
131
includes = And (includes , P [j ] >= hr [0 ][j ], P [j ] <= hr [1 ][j ])
131
132
in_r1 = Or (in_r1 , includes )
132
133
133
- for node in nodes : #same as above loop except for r2
134
+ for node in reach2 : #same as above loop except for r2
134
135
for i in range (0 , len (reach2 [node ]), 2 ): # for each vertex in the node
135
136
includes = And ()
136
137
hr = [reach2 [node ][i ], reach2 [node ][i + 1 ]] # clarifies expressions and matches logic with contain_all
137
138
for j in range (state_len ):
138
139
includes = And (includes , P [j ] >= hr [0 ][j ], P [j ] <= hr [1 ][j ])
139
- in_r1 = Or (in_r2 , includes )
140
+ in_r2 = Or (in_r2 , includes )
140
141
141
142
s .add (in_r1 , Not (in_r2 ))
142
143
return s .check () == unsat
0 commit comments