From 017cad8b778c92377e1b23e50e7fdc73202ab6db Mon Sep 17 00:00:00 2001
From: Levente Bajczi <bajczilevi@gmail.com>
Date: Thu, 15 Feb 2024 17:22:09 +0100
Subject: [PATCH] UNknown<S, A>

---
 .../bme/mit/theta/analysis/algorithm/SafetyResult.java | 10 +++++-----
 .../theta/analysis/algorithm/bounded/BoundedChecker.kt |  2 +-
 .../bme/mit/theta/xcfa/cli/checkers/ConfigToChecker.kt |  2 +-
 3 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/SafetyResult.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/SafetyResult.java
index 8e57705a30..ebc215711c 100644
--- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/SafetyResult.java
+++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/SafetyResult.java
@@ -86,8 +86,8 @@ public static Unsafe<State, Action> unsafe() {
         return new Unsafe<>();
     }
 
-    public static Unknown unknown() {
-        return new Unknown();
+    public static <S extends State, A extends Action> Unknown<S, A> unknown() {
+        return new Unknown<>();
     }
 
     public abstract boolean isSafe();
@@ -195,7 +195,7 @@ public String toString() {
         }
     }
 
-    public static final class Unknown extends SafetyResult<State, Action> {
+    public static final class Unknown<S extends State, A extends Action> extends SafetyResult<S, A> {
         @Override
         public boolean isSafe() {
             return false;
@@ -207,12 +207,12 @@ public boolean isUnsafe() {
         }
 
         @Override
-        public Safe<State, Action> asSafe() {
+        public Safe<S, A> asSafe() {
             return null;
         }
 
         @Override
-        public Unsafe<State, Action> asUnsafe() {
+        public Unsafe<S, A> asUnsafe() {
             return null;
         }
 
diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/BoundedChecker.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/BoundedChecker.kt
index 0cfef733e4..528df05d9d 100644
--- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/BoundedChecker.kt
+++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/BoundedChecker.kt
@@ -116,7 +116,7 @@ class BoundedChecker<S : ExprState, A : StmtAction> @JvmOverloads constructor(
                 lastIterLookup = lastIterLookup.copy(second = iteration)
             }
         }
-        return SafetyResult.unknown() as SafetyResult<S, A>
+        return SafetyResult.unknown()
     }
 
     private fun bmc(): SafetyResult<S, A>? {
diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToChecker.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToChecker.kt
index 5fa1c31df8..5cece3382a 100644
--- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToChecker.kt
+++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToChecker.kt
@@ -39,7 +39,7 @@ fun getChecker(xcfa: XCFA, mcm: MCM, config: XcfaConfig<*, *>, parseContext: Par
             Backend.BOUNDED -> getBoundedChecker(xcfa, mcm, config, logger)
             Backend.LAZY -> TODO()
             Backend.PORTFOLIO -> getPortfolioChecker(xcfa, mcm, config, parseContext, logger, uniqueLogger)
-            Backend.NONE -> SafetyChecker<XcfaState<*>, XcfaAction, XcfaPrec<*>> { _ -> SafetyResult.unknown() as SafetyResult<XcfaState<*>, XcfaAction> }
+            Backend.NONE -> SafetyChecker<XcfaState<*>, XcfaAction, XcfaPrec<*>> { _ -> SafetyResult.unknown() }
         }
     }