From 324c0648bbc025e64fc5922bf12710b16e515759 Mon Sep 17 00:00:00 2001 From: mondokm Date: Tue, 18 Feb 2025 15:26:05 +0100 Subject: [PATCH] Fix formatting --- .../bme/mit/theta/sts/analysis/Ic3Test.java | 1 - .../java/hu/bme/mit/theta/sts/cli/StsCli.java | 12 ++-- .../xsts/analysis/XstsToMonolithicExpr.kt | 63 +++++++++---------- .../hu/bme/mit/theta/xsts/cli/XstsCliIC3.kt | 38 +++++------ .../xsts/cli/XstsCliMonolithicBaseCommand.kt | 31 +++++---- .../xsts/cli/optiongroup/InputOptions.kt | 2 - 6 files changed, 70 insertions(+), 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 index 42d8f436c8..ea5d8b4b72 100644 --- 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 index dd2f42c3ce..10a3d8c368 100644 --- 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/subprojects/xsts/xsts-analysis/src/main/kotlin/hu/bme/mit/theta/xsts/analysis/XstsToMonolithicExpr.kt b/subprojects/xsts/xsts-analysis/src/main/kotlin/hu/bme/mit/theta/xsts/analysis/XstsToMonolithicExpr.kt index c6da8aa170..0052ce798b 100644 --- a/subprojects/xsts/xsts-analysis/src/main/kotlin/hu/bme/mit/theta/xsts/analysis/XstsToMonolithicExpr.kt +++ b/subprojects/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 { 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 index 8eb4c86e97..09a2339cb9 100644 --- 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) } -} \ No newline at end of file +} diff --git a/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliMonolithicBaseCommand.kt b/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliMonolithicBaseCommand.kt index fee4734e37..f11f526c79 100644 --- a/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliMonolithicBaseCommand.kt +++ b/subprojects/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() } - -} \ No newline at end of file + if (reversed) { + monolithicExpr = monolithicExpr.createReversed() + } + return monolithicExpr + } +} diff --git a/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/optiongroup/InputOptions.kt b/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/optiongroup/InputOptions.kt index 82476e43c0..7882eabc5b 100644 --- a/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/optiongroup/InputOptions.kt +++ b/subprojects/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.*