Fix formatting

ftsrg · Feb 18, 2025 · 324c064 · 324c064
1 parent 58a8fc5
commit 324c064
Show file tree

Hide file tree

Showing 6 changed files with 70 additions and 77 deletions.
diff --git a/subprojects/sts/sts-analysis/src/test/java/hu/bme/mit/theta/sts/analysis/Ic3Test.java b/subprojects/sts/sts-analysis/src/test/java/hu/bme/mit/theta/sts/analysis/Ic3Test.java
@@ -32,7 +32,6 @@
  */
 
 import hu.bme.mit.theta.analysis.algorithm.bounded.MonolithicExpr;
-import hu.bme.mit.theta.analysis.algorithm.bounded.ReversedMonolithicExprKt;
 import hu.bme.mit.theta.analysis.algorithm.ic3.Ic3Checker;
 import hu.bme.mit.theta.common.Utils;
 import hu.bme.mit.theta.core.model.Valuation;

diff --git a/subprojects/sts/sts-cli/src/main/java/hu/bme/mit/theta/sts/cli/StsCli.java b/subprojects/sts/sts-cli/src/main/java/hu/bme/mit/theta/sts/cli/StsCli.java
@@ -306,7 +306,9 @@ private STS loadModel() throws Exception {
             final STS sts, final SolverFactory abstractionSolverFactory) {
         final MonolithicExpr monolithicExpr;
         if (reversed) {
-            monolithicExpr = ReversedMonolithicExprKt.createReversed(StsToMonolithicExprKt.toMonolithicExpr(sts));
+            monolithicExpr =
+                    ReversedMonolithicExprKt.createReversed(
+                            StsToMonolithicExprKt.toMonolithicExpr(sts));
         } else {
             monolithicExpr = StsToMonolithicExprKt.toMonolithicExpr(sts);
         }
@@ -377,7 +379,9 @@ public VarIndexing nextIndexing() {
             throws Exception {
         final MonolithicExpr monolithicExpr;
         if (reversed) {
-            monolithicExpr = ReversedMonolithicExprKt.createReversed(StsToMonolithicExprKt.toMonolithicExpr(sts));
+            monolithicExpr =
+                    ReversedMonolithicExprKt.createReversed(
+                            StsToMonolithicExprKt.toMonolithicExpr(sts));
         } else {
             monolithicExpr = StsToMonolithicExprKt.toMonolithicExpr(sts);
         }
@@ -386,15 +390,13 @@ public VarIndexing nextIndexing() {
                 true,
                 solverFactory,
                 valuation -> monolithicExpr.getValToState().invoke(valuation),
-                (Valuation v1, Valuation v2) ->
-                        monolithicExpr.getBiValToAction().invoke(v1, v2),
+                (Valuation v1, Valuation v2) -> monolithicExpr.getBiValToAction().invoke(v1, v2),
                 true,
                 true,
                 true,
                 true,
                 true,
                 true);
-
     }
 
     private void printResult(

diff --git a/...xsts/xsts-analysis/src/main/kotlin/hu/bme/mit/theta/xsts/analysis/XstsToMonolithicExpr.kt b/...xsts/xsts-analysis/src/main/kotlin/hu/bme/mit/theta/xsts/analysis/XstsToMonolithicExpr.kt
@@ -24,7 +24,6 @@ import hu.bme.mit.theta.core.model.Valuation
 import hu.bme.mit.theta.core.stmt.AssignStmt
 import hu.bme.mit.theta.core.stmt.IfStmt
 import hu.bme.mit.theta.core.stmt.SequenceStmt
-import hu.bme.mit.theta.core.stmt.Stmts
 import hu.bme.mit.theta.core.type.booltype.BoolExprs.False
 import hu.bme.mit.theta.core.type.booltype.BoolExprs.True
 import hu.bme.mit.theta.core.type.booltype.BoolLitExpr
@@ -49,59 +48,53 @@ fun XSTS.toMonolithicExpr(): MonolithicExpr {
   val monolithicTransition =
     IfStmt.of(
       Not(initialized.ref),
-      SequenceStmt.of(
-        ImmutableList.of(
-          this.init,
-          AssignStmt.of(initialized, True())
-        )
-      ),
+      SequenceStmt.of(ImmutableList.of(this.init, AssignStmt.of(initialized, True()))),
       IfStmt.of(
         lastActionWasEnv.ref,
-        SequenceStmt.of(
-          ImmutableList.of(
-            this.tran,
-            AssignStmt.of(lastActionWasEnv, False())
-          )
-        ),
-        SequenceStmt.of(
-          ImmutableList.of(
-            this.env,
-            AssignStmt.of(lastActionWasEnv, True())
-          )
-        )
-      )
+        SequenceStmt.of(ImmutableList.of(this.tran, AssignStmt.of(lastActionWasEnv, False()))),
+        SequenceStmt.of(ImmutableList.of(this.env, AssignStmt.of(lastActionWasEnv, True()))),
+      ),
     )
-  val monolithicUnfoldResult = StmtUtils.toExpr(monolithicTransition, VarIndexingFactory.indexing(0))
+  val monolithicUnfoldResult =
+    StmtUtils.toExpr(monolithicTransition, VarIndexingFactory.indexing(0))
   val transExpr = And(monolithicUnfoldResult.exprs)
 
-  return MonolithicExpr(initExpr, transExpr, propExpr, monolithicUnfoldResult.indexing, VarIndexingFactory.indexing(0))
+  return MonolithicExpr(
+    initExpr,
+    transExpr,
+    propExpr,
+    monolithicUnfoldResult.indexing,
+    VarIndexingFactory.indexing(0),
+  )
 }
 
 fun XSTS.valToAction(val1: Valuation, val2: Valuation): XstsAction {
   val val1Map = val1.toMap()
-  val lastActionWasEnv1 = (val1Map[val1Map.keys.first { it.name == "__lastActionWasEnv__" }] as BoolLitExpr).value
-  val initialized1 = (val1Map[val1Map.keys.first { it.name == "__initialized__" }] as BoolLitExpr).value
+  val lastActionWasEnv1 =
+    (val1Map[val1Map.keys.first { it.name == "__lastActionWasEnv__" }] as BoolLitExpr).value
+  val initialized1 =
+    (val1Map[val1Map.keys.first { it.name == "__initialized__" }] as BoolLitExpr).value
 
   val val2Map = val1.toMap()
-  val lastActionWasEnv2 = (val2Map[val2Map.keys.first { it.name == "__lastActionWasEnv__" }] as BoolLitExpr).value
-  val initialized2 = (val2Map[val2Map.keys.first { it.name == "__initialized__" }] as BoolLitExpr).value
+  val lastActionWasEnv2 =
+    (val2Map[val2Map.keys.first { it.name == "__lastActionWasEnv__" }] as BoolLitExpr).value
+  val initialized2 =
+    (val2Map[val2Map.keys.first { it.name == "__initialized__" }] as BoolLitExpr).value
 
   checkArgument(initialized2)
   checkArgument(lastActionWasEnv1 != lastActionWasEnv2)
 
-  if(!initialized1) return XstsAction.create(this.init)
-  else if(lastActionWasEnv1) return XstsAction.create(this.tran)
+  if (!initialized1) return XstsAction.create(this.init)
+  else if (lastActionWasEnv1) return XstsAction.create(this.tran)
   else return XstsAction.create(this.env)
 }
 
 fun XSTS.valToState(val1: Valuation): XstsState<ExplState> {
   val valMap = val1.toMap()
-  val lastActionWasEnv = (valMap[valMap.keys.first { it.name == "__lastActionWasEnv__" }] as BoolLitExpr).value
-  val initialized = (valMap[valMap.keys.first { it.name == "__initialized__" }] as BoolLitExpr).value
+  val lastActionWasEnv =
+    (valMap[valMap.keys.first { it.name == "__lastActionWasEnv__" }] as BoolLitExpr).value
+  val initialized =
+    (valMap[valMap.keys.first { it.name == "__initialized__" }] as BoolLitExpr).value
 
-  return XstsState.of(
-    ExplState.of(val1),
-    lastActionWasEnv,
-    initialized
-  )
+  return XstsState.of(ExplState.of(val1), lastActionWasEnv, initialized)
 }
diff --git a/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliIC3.kt b/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliIC3.kt
@@ -13,7 +13,6 @@
  *  See the License for the specific language governing permissions and
  *  limitations under the License.
  */
-
 package hu.bme.mit.theta.xsts.cli
 
 import com.github.ajalt.clikt.parameters.options.default
@@ -34,11 +33,7 @@ import java.util.concurrent.TimeUnit
 import kotlin.system.exitProcess
 
 class XstsCliIC3 :
-  XstsCliMonolithicBaseCommand(
-    name = "IC3",
-    help =
-      "Model checking using the IC3 algorithm.",
-  ) {
+  XstsCliMonolithicBaseCommand(name = "IC3", help = "Model checking using the IC3 algorithm.") {
 
   private val formerFramesOpt: Boolean by option().boolean().default(true)
   private val unSatOpt: Boolean by option().boolean().default(true)
@@ -61,7 +56,7 @@ class XstsCliIC3 :
       doRun()
     } catch (e: Exception) {
       printError(e)
-        exitProcess(1)
+      exitProcess(1)
     }
   }
 
@@ -71,22 +66,23 @@ class XstsCliIC3 :
     val xsts = inputOptions.loadXsts()
     val monolithicExpr = createMonolithicExpr(xsts)
     val sw = Stopwatch.createStarted()
-    val checker = Ic3Checker(
-            monolithicExpr,
-            reversed,
-            solverFactory,
-            xsts::valToState,
-            xsts::valToAction,
-            formerFramesOpt,
-            unSatOpt,
-            notBOpt,
-            propagateOpt,
-            filterOpt,
-            false
-        )
+    val checker =
+      Ic3Checker(
+        monolithicExpr,
+        reversed,
+        solverFactory,
+        xsts::valToState,
+        xsts::valToAction,
+        formerFramesOpt,
+        unSatOpt,
+        notBOpt,
+        propagateOpt,
+        filterOpt,
+        false,
+      )
     val result = checker.check()
     sw.stop()
     printResult(result, xsts, sw.elapsed(TimeUnit.MILLISECONDS))
     writeCex(result, xsts)
   }
-}
+}
diff --git a/...s/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliMonolithicBaseCommand.kt b/...s/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliMonolithicBaseCommand.kt
@@ -13,7 +13,6 @@
  *  See the License for the specific language governing permissions and
  *  limitations under the License.
  */
-
 package hu.bme.mit.theta.xsts.cli
 
 import com.github.ajalt.clikt.parameters.options.default
@@ -25,18 +24,24 @@ import hu.bme.mit.theta.analysis.l2s.createMonolithicL2S
 import hu.bme.mit.theta.xsts.XSTS
 import hu.bme.mit.theta.xsts.analysis.hu.bme.mit.theta.xsts.analysis.toMonolithicExpr
 
-abstract class XstsCliMonolithicBaseCommand(name: String? = null, help: String = ""):
-    XstsCliBaseCommand(name = name, help = help) {
+abstract class XstsCliMonolithicBaseCommand(name: String? = null, help: String = "") :
+  XstsCliBaseCommand(name = name, help = help) {
 
-    protected val reversed: Boolean by option(help = "Reversed state space exploration").boolean().default(false)
-    protected val livenessToSafety: Boolean by option(help = "Use liveness to safety transformation").boolean().default(false)
-    protected val abstracted: Boolean by option(help = "Wrap analysis in CEGAR loop").boolean().default(false)
+  protected val reversed: Boolean by
+    option(help = "Reversed state space exploration").boolean().default(false)
+  protected val livenessToSafety: Boolean by
+    option(help = "Use liveness to safety transformation").boolean().default(false)
+  protected val abstracted: Boolean by
+    option(help = "Wrap analysis in CEGAR loop").boolean().default(false)
 
-    fun createMonolithicExpr(xsts: XSTS): MonolithicExpr {
-        var monolithicExpr = xsts.toMonolithicExpr()
-        if (livenessToSafety) { monolithicExpr = monolithicExpr.createMonolithicL2S() }
-        if (reversed) { monolithicExpr = monolithicExpr.createReversed() }
-        return monolithicExpr
+  fun createMonolithicExpr(xsts: XSTS): MonolithicExpr {
+    var monolithicExpr = xsts.toMonolithicExpr()
+    if (livenessToSafety) {
+      monolithicExpr = monolithicExpr.createMonolithicL2S()
     }
-
-}
+    if (reversed) {
+      monolithicExpr = monolithicExpr.createReversed()
+    }
+    return monolithicExpr
+  }
+}
diff --git a/...jects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/optiongroup/InputOptions.kt b/...jects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/optiongroup/InputOptions.kt
@@ -21,13 +21,11 @@ import com.github.ajalt.clikt.parameters.options.option
 import com.github.ajalt.clikt.parameters.options.required
 import com.github.ajalt.clikt.parameters.types.file
 import com.github.ajalt.clikt.parameters.types.inputStream
-import hu.bme.mit.theta.analysis.algorithm.bounded.MonolithicExpr
 import hu.bme.mit.theta.frontend.petrinet.model.PetriNet
 import hu.bme.mit.theta.frontend.petrinet.pnml.PetriNetParser
 import hu.bme.mit.theta.frontend.petrinet.pnml.XMLPnmlToPetrinet
 import hu.bme.mit.theta.frontend.petrinet.xsts.PetriNetToXSTS
 import hu.bme.mit.theta.xsts.XSTS
-import hu.bme.mit.theta.xsts.analysis.hu.bme.mit.theta.xsts.analysis.toMonolithicExpr
 import hu.bme.mit.theta.xsts.dsl.XstsDslManager
 import java.io.*