From 99f5d833db2ae11247bbbeaccd5354c36dbe528b Mon Sep 17 00:00:00 2001
From: sp <stefan.pranger@iaik.tugraz.at>
Date: Tue, 14 May 2024 13:33:49 +0200
Subject: [PATCH] more changes for rom_evaluate

---
 rom_evaluate.py | 57 +++++++++++++------------------------------------
 1 file changed, 15 insertions(+), 42 deletions(-)

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: