Adjust tests to enums

subprojects/xsts/xsts-analysis/src/test/java/hu/bme/mit/theta/xsts/analysis/XstsEnumSemanticsTest.java

@@ -0,0 +1,37 @@
+/*
+ *  Copyright 2023 Budapest University of Technology and Economics
+ *
+ *  Licensed under the Apache License, Version 2.0 (the "License");
+ *  you may not use this file except in compliance with the License.
+ *  You may obtain a copy of the License at
+ *
+ *      http://www.apache.org/licenses/LICENSE-2.0
+ *
+ *  Unless required by applicable law or agreed to in writing, software
+ *  distributed under the License is distributed on an "AS IS" BASIS,
+ *  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ *  See the License for the specific language governing permissions and
+ *  limitations under the License.
+ */
+package hu.bme.mit.theta.xsts.analysis;
+
+import hu.bme.mit.theta.xsts.dsl.XstsDslManager;
+import org.junit.Test;
+
+import java.io.FileInputStream;
+import java.io.IOException;
+import java.io.InputStream;
+import java.io.SequenceInputStream;
+
+public class XstsEnumSemanticsTest {
+
+    @Test(expected = ClassCastException.class)
+    public void test() throws IOException {
+
+        try (InputStream inputStream = new SequenceInputStream(new FileInputStream("src/test/resources/model/literals_bad.xsts"),
+                new FileInputStream("src/test/resources/property/literals.prop"))) {
+            XstsDslManager.createXsts(inputStream);
+        }
+    }
+
+}

subprojects/xsts/xsts-analysis/src/test/java/hu/bme/mit/theta/xsts/analysis/XstsTest.java

@@ -131,16 +131,14 @@ public static Collection<Object[]> data() {
                 {"src/test/resources/model/choices.xsts", "src/test/resources/property/choices.prop",
                         false, XstsConfigBuilder.Domain.EXPL_PRED_COMBINED},
 
-//                The following three tests are invalid now, as two different types can't be equal even if they have
-//                literals of the same name
-//                {"src/test/resources/model/literals.xsts", "src/test/resources/property/literals.prop",
-//                        true, XstsConfigBuilder.Domain.PRED_CART},
-//
-//                {"src/test/resources/model/literals.xsts", "src/test/resources/property/literals.prop",
-//                        true, XstsConfigBuilder.Domain.EXPL},
-//
-//                {"src/test/resources/model/literals.xsts", "src/test/resources/property/literals.prop",
-//                        true, XstsConfigBuilder.Domain.EXPL_PRED_COMBINED},
+                {"src/test/resources/model/literals.xsts", "src/test/resources/property/literals.prop",
+                        false, XstsConfigBuilder.Domain.PRED_CART},
+
+                {"src/test/resources/model/literals.xsts", "src/test/resources/property/literals.prop",
+                        false, XstsConfigBuilder.Domain.EXPL},
+
+                {"src/test/resources/model/literals.xsts", "src/test/resources/property/literals.prop",
+                        false, XstsConfigBuilder.Domain.EXPL_PRED_COMBINED},
 
                 {"src/test/resources/model/cross3.xsts", "src/test/resources/property/cross.prop",
                         false, XstsConfigBuilder.Domain.PRED_CART},

subprojects/xsts/xsts-analysis/src/test/resources/model/literals.xsts

@@ -1,8 +1,7 @@
-type first : { A, B, C, D }
-type second : { D, C, B, A }
+type alphabet : { A, B, C, D }
 
-var f : first = A
-var s : second = A
+var f : alphabet = A
+var g : alphabet = B
 
 trans {}
 

subprojects/xsts/xsts-analysis/src/test/resources/model/literals_bad.xsts

@@ -0,0 +1,11 @@
+type alphabet : { A, B, C, D }
+type second_alphabet : { A, B, C, D }
+
+var f : alphabet = A
+var g : second_alphabet = A
+
+trans {}
+
+init {}
+
+env {}

subprojects/xsts/xsts-analysis/src/test/resources/property/literals.prop

@@ -1,3 +1,3 @@
 prop {
-    f == s
+    f == g
 }