fixes region restoration not updating region list in state inspector

DecwLK · Mar 10, 2024 · e6f90d7 · e6f90d7
1 parent 080831a
commit e6f90d7
Show file tree

Hide file tree

Showing 2 changed files with 12 additions and 1 deletion.
diff --git a/src/main/java/org/gecko/actions/DeleteRegionViewModelElementAction.java b/src/main/java/org/gecko/actions/DeleteRegionViewModelElementAction.java
@@ -1,10 +1,13 @@
 package org.gecko.actions;
 
+import java.util.ArrayList;
+import java.util.List;
 import org.gecko.exceptions.GeckoException;
 import org.gecko.model.Automaton;
 import org.gecko.viewmodel.GeckoViewModel;
 import org.gecko.viewmodel.PositionableViewModelElement;
 import org.gecko.viewmodel.RegionViewModel;
+import org.gecko.viewmodel.StateViewModel;
 
 /**
  * A concrete representation of an {@link Action} that removes a {@link RegionViewModel} from the {@link GeckoViewModel}
@@ -25,6 +28,12 @@ public class DeleteRegionViewModelElementAction extends AbstractPositionableView
     @Override
     boolean run() throws GeckoException {
         automaton.removeRegion(regionViewModel.getTarget());
+       List<StateViewModel> states = new ArrayList<>(regionViewModel.getStatesProperty());
+
+        for (StateViewModel state : states) {
+            regionViewModel.removeState(state);
+        }
+
         geckoViewModel.deleteViewModelElement(regionViewModel);
         geckoViewModel.getCurrentEditor().updateRegions();
         return true;

diff --git a/src/main/java/org/gecko/actions/RestoreRegionViewModelElementAction.java b/src/main/java/org/gecko/actions/RestoreRegionViewModelElementAction.java
@@ -1,5 +1,6 @@
 package org.gecko.actions;
 
+import org.gecko.exceptions.ModelException;
 import org.gecko.model.Automaton;
 import org.gecko.viewmodel.GeckoViewModel;
 import org.gecko.viewmodel.RegionViewModel;
@@ -22,9 +23,10 @@ public class RestoreRegionViewModelElementAction extends Action {
 
 
     @Override
-    boolean run() {
+    boolean run() throws ModelException {
         automaton.addRegion(regionViewModel.getTarget());
         geckoViewModel.addViewModelElement(regionViewModel);
+        geckoViewModel.getCurrentEditor().updateRegions();
         return true;
     }