UNknown<S, A>

ftsrg · Feb 15, 2024 · 017cad8 · 017cad8
1 parent cdeaed3
commit 017cad8
Show file tree

Hide file tree

Showing 3 changed files with 7 additions and 7 deletions.
diff --git a/...jects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/SafetyResult.java b/...jects/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/...mmon/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/BoundedChecker.kt b/...mmon/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/...rojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToChecker.kt b/...rojects/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() }
         }
     }