restricted invariants to always be downward closed

luth1um · Aug 29, 2024 · 7d256b0 · 7d256b0
1 parent fe6dfb1
commit 7d256b0
Show file tree

Hide file tree

Showing 2 changed files with 13 additions and 8 deletions.
diff --git a/src/view/ClausesManipulation.tsx b/src/view/ClausesManipulation.tsx
@@ -10,10 +10,11 @@ import { useButtonUtils } from '../utils/buttonUtils';
 interface ClausesManipulationProps {
   viewModel: ClausesViewModel;
   clocks: Clock[];
+  downwardClosedOnly?: boolean;
 }
 
 export const ClausesManipulation: React.FC<ClausesManipulationProps> = (props) => {
-  const { viewModel, clocks } = props;
+  const { viewModel, clocks, downwardClosedOnly } = props;
   const { clauses, deleteClause, changeClause } = viewModel;
   const { t } = useTranslation();
   const { executeOnKeyboardClick } = useButtonUtils();
@@ -30,12 +31,14 @@ export const ClausesManipulation: React.FC<ClausesManipulationProps> = (props) =
 
   const comparisonDropdownItems = useMemo(
     () =>
-      Object.values(ClockComparator).map((v) => (
-        <MenuItem key={v} value={v} data-testid={'menu-item-comparison-' + v}>
-          {v}
-        </MenuItem>
-      )),
-    []
+      Object.values(ClockComparator)
+        .filter((comp) => !downwardClosedOnly || comp === ClockComparator.LESSER || comp === ClockComparator.LEQ)
+        .map((v) => (
+          <MenuItem key={v} value={v} data-testid={'menu-item-comparison-' + v}>
+            {v}
+          </MenuItem>
+        )),
+    [downwardClosedOnly]
   );
 
   return (

diff --git a/src/view/ManipulateLocationDialog.tsx b/src/view/ManipulateLocationDialog.tsx
@@ -156,7 +156,9 @@ export const ManipulateLocationDialog: React.FC<ManipulateLocationDialogProps> =
           label={t('locDialog.hasInvariant')}
           data-testid={'checkbox-location-hasInvariant'}
         />
-        {invariantChecked && <ClausesManipulation viewModel={clausesViewModel} clocks={clocks} />}
+        {invariantChecked && (
+          <ClausesManipulation viewModel={clausesViewModel} clocks={clocks} downwardClosedOnly={true} />
+        )}
         {invariantChecked && (
           <Button
             variant="outlined"