Fix formatting

ftsrg · Nov 5, 2024 · 48fc830 · 48fc830
1 parent ef9654b
commit 48fc830
Show file tree

Hide file tree

Showing 6 changed files with 33 additions and 24 deletions.
diff --git a/...cts/cfa/cfa-analysis/src/main/kotlin/hu/bme/mit/theta/cfa/analysis/CfaToMonolithicExpr.kt b/...cts/cfa/cfa-analysis/src/main/kotlin/hu/bme/mit/theta/cfa/analysis/CfaToMonolithicExpr.kt
@@ -61,15 +61,23 @@ fun CFA.toMonolithicExpr(): MonolithicExpr {
       }
       .toList()
 
-  val defaultValues = this.vars.map {
-    when (it.type) {
-      is IntType -> Eq(it.ref, Int(0))
-      is BoolType -> Eq(it.ref, Bool(false))
-      is BvType -> Eq(it.ref, BvUtils.bigIntegerToNeutralBvLitExpr(BigInteger.ZERO, (it.type as BvType).size))
-      is FpType -> FpAssign(it.ref as Expr<FpType>, NaN(it.type as FpType))
-      else -> throw IllegalArgumentException("Unsupported type")
-    }
-  }.toList().let { And(it)}
+  val defaultValues =
+    this.vars
+      .map {
+        when (it.type) {
+          is IntType -> Eq(it.ref, Int(0))
+          is BoolType -> Eq(it.ref, Bool(false))
+          is BvType ->
+            Eq(
+              it.ref,
+              BvUtils.bigIntegerToNeutralBvLitExpr(BigInteger.ZERO, (it.type as BvType).size),
+            )
+          is FpType -> FpAssign(it.ref as Expr<FpType>, NaN(it.type as FpType))
+          else -> throw IllegalArgumentException("Unsupported type")
+        }
+      }
+      .toList()
+      .let { And(it) }
 
   val trans = NonDetStmt.of(tranList)
   val transUnfold = StmtUtils.toExpr(trans, VarIndexingFactory.indexing(0))
@@ -79,7 +87,13 @@ fun CFA.toMonolithicExpr(): MonolithicExpr {
 
   val offsetIndex = transUnfold.indexing
 
-  return MonolithicExpr(initExpr, transExpr, propExpr, offsetIndex, vars = listOf(locVar) + this.vars.toList())
+  return MonolithicExpr(
+    initExpr,
+    transExpr,
+    propExpr,
+    offsetIndex,
+    vars = listOf(locVar) + this.vars.toList(),
+  )
 }
 
 fun CFA.valToAction(val1: Valuation, val2: Valuation): CfaAction {

diff --git a/...mmon/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/MonolithicExpr.kt b/...mmon/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/MonolithicExpr.kt
@@ -13,7 +13,6 @@
  *  See the License for the specific language governing permissions and
  *  limitations under the License.
  */
-
 package hu.bme.mit.theta.analysis.algorithm.bounded
 
 import hu.bme.mit.theta.core.decl.VarDecl
@@ -24,10 +23,11 @@ import hu.bme.mit.theta.core.utils.indexings.VarIndexing
 import hu.bme.mit.theta.core.utils.indexings.VarIndexingFactory
 
 data class MonolithicExpr(
-    val initExpr: Expr<BoolType>,
-    val transExpr: Expr<BoolType>,
-    val propExpr: Expr<BoolType>,
-    val transOffsetIndex: VarIndexing = VarIndexingFactory.indexing(1),
-    val initOffsetIndex: VarIndexing = VarIndexingFactory.indexing(0),
-    val vars: List<VarDecl<*>> = (getVars(initExpr) union getVars(transExpr) union getVars(propExpr)).toList()
-)
+  val initExpr: Expr<BoolType>,
+  val transExpr: Expr<BoolType>,
+  val propExpr: Expr<BoolType>,
+  val transOffsetIndex: VarIndexing = VarIndexingFactory.indexing(1),
+  val initOffsetIndex: VarIndexing = VarIndexingFactory.indexing(0),
+  val vars: List<VarDecl<*>> =
+    (getVars(initExpr) union getVars(transExpr) union getVars(propExpr)).toList(),
+)
diff --git a/...cts/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/MddChecker.java b/...cts/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/MddChecker.java
@@ -41,13 +41,11 @@
 import hu.bme.mit.theta.core.decl.VarDecl;
 import hu.bme.mit.theta.core.type.Expr;
 import hu.bme.mit.theta.core.type.booltype.BoolType;
-import hu.bme.mit.theta.core.utils.ExprUtils;
 import hu.bme.mit.theta.core.utils.PathUtils;
 import hu.bme.mit.theta.core.utils.indexings.VarIndexing;
 import hu.bme.mit.theta.core.utils.indexings.VarIndexingFactory;
 import hu.bme.mit.theta.solver.SolverPool;
 import java.util.List;
-import java.util.Set;
 
 public class MddChecker<A extends ExprAction> implements SafetyChecker<MddProof, MddCex, Void> {
 

diff --git a/...common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/mdd/MddCheckerTest.java b/...common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/mdd/MddCheckerTest.java
@@ -41,7 +41,6 @@
 import java.util.Arrays;
 import java.util.Collection;
 import java.util.List;
-
 import org.junit.Test;
 import org.junit.runner.RunWith;
 import org.junit.runners.Parameterized;

diff --git a/...jects/sts/sts-analysis/src/test/java/hu/bme/mit/theta/sts/analysis/StsMddCheckerTest.java b/...jects/sts/sts-analysis/src/test/java/hu/bme/mit/theta/sts/analysis/StsMddCheckerTest.java
@@ -28,7 +28,6 @@
 import hu.bme.mit.theta.common.logging.Logger;
 import hu.bme.mit.theta.core.type.Expr;
 import hu.bme.mit.theta.core.type.booltype.BoolType;
-import hu.bme.mit.theta.core.utils.ExprUtils;
 import hu.bme.mit.theta.core.utils.indexings.VarIndexing;
 import hu.bme.mit.theta.core.utils.indexings.VarIndexingFactory;
 import hu.bme.mit.theta.solver.SolverPool;
@@ -42,7 +41,6 @@
 import java.util.Arrays;
 import java.util.Collection;
 import java.util.List;
-
 import org.junit.Test;
 import org.junit.runner.RunWith;
 import org.junit.runners.Parameterized;

diff --git a/...s/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaToMonolithicExpr.kt b/...s/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaToMonolithicExpr.kt
@@ -109,7 +109,7 @@ fun XCFA.toMonolithicExpr(): MonolithicExpr {
     transExpr = And(transUnfold.exprs),
     propExpr = Neq(locVar.ref, Int(map[proc.errorLoc.get()]!!)),
     transOffsetIndex = transUnfold.indexing,
-    vars = listOf(locVar) + this.vars.map { it.wrappedVar }.toList()
+    vars = listOf(locVar) + this.vars.map { it.wrappedVar }.toList(),
   )
 }