diff --git a/rom_evaluate.py b/rom_evaluate.py index 657438a..390a6fe 100644 --- a/rom_evaluate.py +++ b/rom_evaluate.py @@ -90,7 +90,7 @@ class TestResult: init_check_opt_avg: {self.init_check_opt_avg} """ def csv(self, ws=" "): - return f"{self.init_check_pes_min:0.04f}{ws}{self.init_check_pes_max:0.04f}{ws}{self.init_check_pes_avg:0.04f}{ws}{self.init_check_opt_min:0.04f}{ws}{self.init_check_opt_max:0.04f}{ws}{self.init_check_opt_avg:0.04f}{ws}{self.safeStates}{ws}{self.unsafeStates}{ws}{self.policy_queries}" + return f"{self.init_check_pes_min:0.04f}{ws}{self.init_check_pes_max:0.04f}{ws}{self.init_check_pes_avg:0.04f}{ws}{self.init_check_opt_min:0.04f}{ws}{self.init_check_opt_max:0.04f}{ws}{self.init_check_opt_avg:0.04f}{ws}{self.safe_states}{ws}{self.unsafe_states}{ws}{self.policy_queries}" def exec(command,verbose=True): if verbose: print(f"Executing {command}") @@ -250,25 +250,21 @@ def statesFormulaTrimmed(states, name): formulas = list() for skiPosition, skiPos_group in skiPositionGroup.items(): formula = f"formula {name}_{skiPosition} = ( ski_position={skiPosition} & " - firstVelocity = True + #print(f"{name} ski_pos:{skiPosition}") velocityGroup = defaultdict(list) + velocityFormulas = list() for item in skiPos_group: velocityGroup[item[3]].append(item) for velocity, velocity_group in velocityGroup.items(): - if firstVelocity: - firstVelocity = False - else: - formula += " | " + #print(f"\tvel:{velocity}") formulasPerSkiPosition = list() - formula += f" (velocity={velocity} & " - firstY = True yPosGroup = defaultdict(list) - yAndXRanges = dict() + yFormulas = list() for item in velocity_group: yPosGroup[item[1]].append(item) for y, y_group in yPosGroup.items(): + #print(f"\t\ty:{y}") sorted_y_group = sorted(y_group, key=lambda s: s[0]) - #formula += f"( y={y} & (" current_x_min = sorted_y_group[0][0] current_x = sorted_y_group[0][0] x_ranges = list() @@ -279,38 +275,15 @@ def statesFormulaTrimmed(states, name): x_ranges.append(f" ({current_x_min}<=x&x<={current_x})") current_x_min = state[0] current_x = state[0] - x_ranges.append(f" ({current_x_min}<=x&x<={sorted_y_group[-1][0]})") - xRangesDisjunction = createBalancedDisjunction(x_ranges) - if xRangesDisjunction in yAndXRanges: - yAndXRanges[xRangesDisjunction].append(y) - else: - yAndXRanges[xRangesDisjunction] = list() - yAndXRanges[xRangesDisjunction].append(y) - for xRange, ys in yAndXRanges.items(): - #if firstY: - # firstY = False - #else: - # formula += " | " - sorted_ys = sorted(ys) - if len(ys) == 1: - formulasPerSkiPosition.append(f" ({xRange} & y={ys[0]})") - continue - current_y_min = sorted_ys[0] - current_y = sorted_ys[0] - y_ranges = list() - for y in sorted_ys[1:]: - if y - current_y == 2: - current_y = y - elif abs(y - current_y) > 2: - y_ranges.append(f" ({current_y_min}<=y&y<={current_y})") - current_y_min = y - current_y = y - y_ranges.append(f" ({current_y_min}<=y&y<={sorted_ys[-1]})") - formulasPerSkiPosition.append(f" ({xRange} & ({createBalancedDisjunction(y_ranges)}))") - - formula += createBalancedDisjunction(formulasPerSkiPosition) - formula += ")" - formula += ");" + x_ranges.append(f" {current_x_min}<=x&x<={sorted_y_group[-1][0]}") + yFormulas.append(f" (y={y} & {createBalancedDisjunction(x_ranges)})") + #x_ranges.clear() + + #velocityFormulas.append(f"(velocity={velocity} & {createBalancedDisjunction(yFormulas)})") + velocityFormulas.append(f"({createBalancedDisjunction(yFormulas)})") + #yFormulas.clear() + formula += createBalancedDisjunction(velocityFormulas) + ");" + #velocityFormulas.clear() formulas.append(formula) for i in range(1, num_ski_positions+1): if i in skiPositionGroup: