Added else tests

ftsrg · Oct 28, 2023 · 524052d · 524052d
1 parent 7ecd628
commit 524052d
Show file tree

Hide file tree

Showing 7 changed files with 509 additions and 1 deletion.
diff --git a/subprojects/xsts/xsts-analysis/src/test/java/hu/bme/mit/theta/xsts/analysis/XstsTest.java b/subprojects/xsts/xsts-analysis/src/test/java/hu/bme/mit/theta/xsts/analysis/XstsTest.java
@@ -339,8 +339,26 @@ public static Collection<Object[]> data() {
                 {"src/test/resources/model/if1.xsts", "src/test/resources/property/if1.prop", true,
                         XstsConfigBuilder.Domain.PRED_CART},
 
+                {"src/test/resources/model/crossroads_choice_else.xsts", "src/test/resources/property/cross.prop",
+                        false, XstsConfigBuilder.Domain.PRED_CART},
+
                 {"src/test/resources/model/if2.xsts", "src/test/resources/property/if2.prop", false,
-                        XstsConfigBuilder.Domain.EXPL_PRED_COMBINED}
+                        XstsConfigBuilder.Domain.EXPL_PRED_COMBINED},
+
+                {"src/test/resources/model/choice-else.xsts", "src/test/resources/property/choice-else1.prop", true,
+                        XstsConfigBuilder.Domain.EXPL_PRED_COMBINED},
+
+                {"src/test/resources/model/choice-else.xsts", "src/test/resources/property/choice-else2.prop", false,
+                        XstsConfigBuilder.Domain.EXPL_PRED_COMBINED},
+
+                {"src/test/resources/model/choice-else2.xsts", "src/test/resources/property/choice-else1.prop", true,
+                        XstsConfigBuilder.Domain.EXPL_PRED_COMBINED},
+
+                {"src/test/resources/model/choice-else2.xsts", "src/test/resources/property/choice-else2.prop", false,
+                        XstsConfigBuilder.Domain.EXPL_PRED_COMBINED},
+
+                {"src/test/resources/model/choice-else2.xsts", "src/test/resources/property/choice-else3.prop", true,
+                        XstsConfigBuilder.Domain.EXPL_PRED_COMBINED},
         });
     }
 

diff --git a/subprojects/xsts/xsts-analysis/src/test/resources/model/choice-else.xsts b/subprojects/xsts/xsts-analysis/src/test/resources/model/choice-else.xsts
@@ -0,0 +1,14 @@
+var x : integer = 0
+
+trans {
+    choice {
+        assume (false);
+        x := 1;
+    } else {
+        x := 2;
+    }
+}
+
+init {}
+
+env {}
diff --git a/subprojects/xsts/xsts-analysis/src/test/resources/model/choice-else2.xsts b/subprojects/xsts/xsts-analysis/src/test/resources/model/choice-else2.xsts
@@ -0,0 +1,17 @@
+var x : integer = 0
+
+trans {
+    choice {
+        assume (false);
+        x := 1;
+    } or {
+        assume (true);
+        x := 2;
+    } else {
+        x := 3;
+    }
+}
+
+init {}
+
+env {}