Merge pull request #211 from DecwLK/export_fixes

fix region not being applied correctly when exporting
DecwLK · Mar 19, 2024 · 0feebf1 · 0feebf1
2 parents a860b98 + a7fef23
commit 0feebf1
Show file tree

Hide file tree

Showing 2 changed files with 13 additions and 4 deletions.
diff --git a/src/main/java/org/gecko/io/AutomatonFileSerializer.java b/src/main/java/org/gecko/io/AutomatonFileSerializer.java
@@ -175,8 +175,8 @@ private Contract applyRegionsToContract(List<Region> relevantRegions, Contract c
             return newContract;
         }
         List<Condition> newConditions = andConditions(relevantRegions);
-        newContract.setPreCondition(newConditions.getFirst());
-        newContract.setPostCondition(newConditions.get(1));
+        newContract.setPreCondition(newConditions.getFirst().and(newContract.getPreCondition()));
+        newContract.setPostCondition(newConditions.get(1).and(newContract.getPostCondition()));
         return newContract;
     }
 
@@ -191,8 +191,11 @@ private List<Condition> andConditions(List<Region> regions) {
         } catch (ModelException e) {
             throw new RuntimeException("Failed to build conditions out of other valid conditions", e);
         }
+        newPre = newPre.and(first.getInvariant());
+        newPost = newPost.and(first.getInvariant());
 
-        for (Region region : regions) {
+        for (int i = 1; i < regions.size(); i++) {
+            Region region = regions.get(i);
             newPre = newPre.and(region.getPreAndPostCondition().getPreCondition());
             newPre = newPre.and(region.getInvariant());
             newPost = newPost.and(region.getPreAndPostCondition().getPostCondition());

diff --git a/src/main/java/org/gecko/model/Condition.java b/src/main/java/org/gecko/model/Condition.java
@@ -32,9 +32,15 @@ public void setCondition(@NonNull String condition) throws ModelException {
 
     @JsonIgnore
     public Condition and(Condition other) {
+        String newCondition;
+        if (other.getCondition().equals(TRUE_CONDITION)) {
+            newCondition = condition;
+        } else {
+            newCondition = AND_CONDITIONS.formatted(condition, other.condition);
+        }
         try {
             // This and other are always valid
-            return new Condition(AND_CONDITIONS.formatted(condition, other.condition));
+            return new Condition(newCondition);
         } catch (ModelException e) {
             return null;
         }