From a7fef2383537134871c1a84c92720ad3533fc7bf Mon Sep 17 00:00:00 2001 From: DecwLK Date: Tue, 19 Mar 2024 13:50:28 +0100 Subject: [PATCH] fix region not being applied correctly when exporting --- src/main/java/org/gecko/io/AutomatonFileSerializer.java | 9 ++++++--- src/main/java/org/gecko/model/Condition.java | 8 +++++++- 2 files changed, 13 insertions(+), 4 deletions(-) diff --git a/src/main/java/org/gecko/io/AutomatonFileSerializer.java b/src/main/java/org/gecko/io/AutomatonFileSerializer.java index aba050fe..05cd073f 100644 --- 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 relevantRegions, Contract c return newContract; } List 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 andConditions(List 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 index ded3345e..afb9e00c 100644 --- 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; }