From 9b8c51e6e7d29a0860ad336613b3111029a3c008 Mon Sep 17 00:00:00 2001 From: AdamZsofi Date: Fri, 20 Sep 2024 20:35:48 +0200 Subject: [PATCH] added basic trace metadata collection; tracegen refactored to clikt --- .../tracegeneration/AdvancedArgTrace.java | 4 +- .../tracegeneration/PatchArgTrace.kt | 4 +- .../tracegeneration/TraceGenerationChecker.kt | 27 +++--- .../tracegeneration/TraceGenerationResult.kt | 27 ++++++ .../tracegeneration/TraceMetadata.kt | 27 +++++- .../XstsDoubleEndNodeRemover.java | 14 +-- .../theta/core/utils/StmtAssumeCollector.java | 84 ---------------- .../initprec/XstsTracegenPredInitPrec.kt | 1 - .../tracegeneration/XstsTracegenBuilder.kt | 15 ++- .../tracegeneration/XstsTracegenConfig.kt | 10 +- .../mit/theta/xsts/cli/XstsCliBaseCommand.kt | 2 +- .../hu/bme/mit/theta/xsts/cli/XstsCliMain.kt | 2 +- .../bme/mit/theta/xsts/cli/XstsCliTracegen.kt | 95 +++++++++++++++++++ .../xsts/cli/optiongroup/InputOptions.kt | 1 - 14 files changed, 189 insertions(+), 124 deletions(-) create mode 100644 subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/TraceGenerationResult.kt delete mode 100644 subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/StmtAssumeCollector.java create mode 100644 subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliTracegen.kt diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/AdvancedArgTrace.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/AdvancedArgTrace.java index 201d8b61c4..a89405d5ae 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/AdvancedArgTrace.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/AdvancedArgTrace.java @@ -3,8 +3,8 @@ import hu.bme.mit.theta.analysis.Action; import hu.bme.mit.theta.analysis.State; import hu.bme.mit.theta.analysis.Trace; -import hu.bme.mit.theta.analysis.algorithm.ArgEdge; -import hu.bme.mit.theta.analysis.algorithm.ArgNode; +import hu.bme.mit.theta.analysis.algorithm.arg.ArgEdge; +import hu.bme.mit.theta.analysis.algorithm.arg.ArgNode; import java.util.*; import java.util.stream.Collectors; diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/PatchArgTrace.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/PatchArgTrace.kt index 2ea6c28f90..e77a198a49 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/PatchArgTrace.kt +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/PatchArgTrace.kt @@ -2,8 +2,8 @@ package hu.bme.mit.theta.analysis.algorithm.tracegeneration import hu.bme.mit.theta.analysis.Action import hu.bme.mit.theta.analysis.State -import hu.bme.mit.theta.analysis.algorithm.ArgNode -import hu.bme.mit.theta.analysis.algorithm.ArgTrace +import hu.bme.mit.theta.analysis.algorithm.arg.ArgNode +import hu.bme.mit.theta.analysis.algorithm.arg.ArgTrace /** * Traces built on ArgTraces, but capable of handling traces going through covered nodes diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/TraceGenerationChecker.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/TraceGenerationChecker.kt index a8909a2dfc..ef232c2ea3 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/TraceGenerationChecker.kt +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/TraceGenerationChecker.kt @@ -1,28 +1,27 @@ package hu.bme.mit.theta.analysis.algorithm.tracegeneration import com.google.common.base.Preconditions -import hu.bme.mit.theta.analysis.Prec -import hu.bme.mit.theta.analysis.Trace +import hu.bme.mit.theta.analysis.* import hu.bme.mit.theta.analysis.algorithm.* -import hu.bme.mit.theta.analysis.algorithm.arg.ARG +import hu.bme.mit.theta.analysis.algorithm.SafetyResult import hu.bme.mit.theta.analysis.algorithm.arg.ArgNode import hu.bme.mit.theta.analysis.algorithm.arg.ArgTrace import hu.bme.mit.theta.analysis.algorithm.cegar.Abstractor -import hu.bme.mit.theta.analysis.expr.ExprAction -import hu.bme.mit.theta.analysis.expr.ExprState import hu.bme.mit.theta.common.logging.Logger +import java.util.* import java.util.function.Consumer +import kotlin.collections.ArrayList -class TraceGenerationChecker( +class TraceGenerationChecker( private val logger: Logger, private val abstractor: Abstractor, private val getFullTraces : Boolean, -) : SafetyChecker, Trace, P> { // TODO refactor templates? +) : SafetyChecker, EmptyCex, P> { // TODO refactor templates? private var traces: List> = ArrayList() companion object { - fun create( + fun create( logger: Logger, abstractor: Abstractor, getFullTraces: Boolean @@ -31,7 +30,7 @@ class TraceGenerationChecker( } } - override fun check(prec: P): SafetyResult, Trace> { + override fun check(prec: P): SafetyResult, EmptyCex> { logger.write(Logger.Level.SUBSTEP, "Printing prec for trace generation...\n" + System.lineSeparator()) logger.write(Logger.Level.SUBSTEP, prec.toString()) @@ -70,6 +69,12 @@ class TraceGenerationChecker( ) }.toList()) + // TODO does not work with full traces (see below - modification should be done to arg traces?) + assert(!getFullTraces) + val metadataBuilder = TraceGenerationMetadataBuilder() + argTraces.forEach { trace -> metadataBuilder.addTrace(trace) } + val traceMetadata = metadataBuilder.build() + // filter 2, optional, to get full traces even where there is coverage // why?: otherwise we stop at the leaf, which is covered in many traces by other nodes traces = if (getFullTraces) { @@ -87,8 +92,8 @@ class TraceGenerationChecker( ) logger.write(Logger.Level.SUBSTEP, "-- Trace generation done --\n") - return SafetyResult.traces(traces) - + // TODO return unsafe if coverage not full? (is that known here? not yet) + return SafetyResult.safe(TraceGenerationResult(traceMetadata, traces)) } private fun filterEndNodes( diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/TraceGenerationResult.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/TraceGenerationResult.kt new file mode 100644 index 0000000000..fdbafa3e49 --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/TraceGenerationResult.kt @@ -0,0 +1,27 @@ +/* + * Copyright 2024 Budapest University of Technology and Economics + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ + +package hu.bme.mit.theta.analysis.algorithm.tracegeneration + +import hu.bme.mit.theta.analysis.Action +import hu.bme.mit.theta.analysis.State +import hu.bme.mit.theta.analysis.Trace +import hu.bme.mit.theta.analysis.algorithm.Witness + +data class TraceGenerationResult ( + val metadata: Collection>, + val traces: Collection> +) : Witness diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/TraceMetadata.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/TraceMetadata.kt index 9b77c54ff9..99348218cd 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/TraceMetadata.kt +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/TraceMetadata.kt @@ -4,6 +4,7 @@ import hu.bme.mit.theta.analysis.Action import hu.bme.mit.theta.analysis.State import hu.bme.mit.theta.analysis.algorithm.arg.ArgNode import hu.bme.mit.theta.analysis.algorithm.arg.ArgTrace +import kotlin.jvm.optionals.getOrNull class TraceGenerationMetadataBuilder { @@ -50,13 +51,13 @@ class TraceGenerationMetadataBuilder { metadataTraces.keys.forEach { trace -> metadataStates[Pair(trace, coveredNode)]?.let { coveredMetaState -> if (coveredMetaState != state) { - coveredMetaState.coveringState.add(state) + coveredMetaState.coveredState.add(state) } } } } - node.coveringNode.get().let { coveringNode -> + node.coveringNode.getOrNull()?.let { coveringNode -> metadataTraces.keys.forEach { trace -> metadataStates[Pair(trace, coveringNode)]?.let { coveredMetaState -> if (coveredMetaState != state) { @@ -66,6 +67,15 @@ class TraceGenerationMetadataBuilder { } } } + + var missingCover = false + for (stateMetadata in metadataStates.values) { + stateMetadata.coveringState.forEach { coveringState -> if(!coveringState.coveredState.contains(stateMetadata)) missingCover = true } + stateMetadata.coveredState.forEach { coveredState -> if(!coveredState.coveringState.contains(stateMetadata)) missingCover = true } + } + + assert(!missingCover + ) { "Some coverages are only stored in one direction (covering not stored in covered or vica versa)" } } } @@ -107,7 +117,18 @@ class StateMetadata (val state: State, val id : Long = cou } override fun toString(): String { - return "S$id" + val sb = StringBuilder() + sb.append("S$id{") + if(coveredState.isNotEmpty()) { + sb.append("covering: ") + coveredState.forEach { coveringState -> sb.append("S${coveringState.id} ") } + } + if(coveringState.isNotEmpty()) { + sb.append("covered by: ") + coveringState.forEach { coveredState -> sb.append("S${coveredState.id} ") } + } + sb.append("}") + return sb.toString() } } diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/XstsDoubleEndNodeRemover.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/XstsDoubleEndNodeRemover.java index fcbb0a226a..4861ae5abf 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/XstsDoubleEndNodeRemover.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/XstsDoubleEndNodeRemover.java @@ -1,10 +1,10 @@ package hu.bme.mit.theta.analysis.algorithm.tracegeneration; +import hu.bme.mit.theta.analysis.Action; +import hu.bme.mit.theta.analysis.State; import hu.bme.mit.theta.analysis.Trace; -import hu.bme.mit.theta.analysis.algorithm.ARG; -import hu.bme.mit.theta.analysis.algorithm.ArgNode; -import hu.bme.mit.theta.analysis.expr.ExprAction; -import hu.bme.mit.theta.analysis.expr.ExprState; +import hu.bme.mit.theta.analysis.algorithm.arg.ARG; +import hu.bme.mit.theta.analysis.algorithm.arg.ArgNode; import hu.bme.mit.theta.analysis.expr.StmtAction; import java.io.BufferedReader; @@ -13,8 +13,8 @@ import java.util.ArrayList; import java.util.List; -public class XstsDoubleEndNodeRemover { - static List> collectBadLeaves(ARG arg) { +public class XstsDoubleEndNodeRemover { + static List> collectBadLeaves(ARG arg) { // TODO XSTS SPECIFIC for now! collecting nodes that look like there should be traces to it, but shouldn't ("not firing anything" nodes) XstsDoubleEndNodeRemover instance = new XstsDoubleEndNodeRemover(); List> badNodes = new ArrayList<>(); @@ -63,7 +63,7 @@ private boolean isBadLeaf(ArgNode node) { } } - static Trace filterSuperfluousEndNode(Trace trace) { + static Trace filterSuperfluousEndNode(Trace trace) { if(trace.getStates().size()>3) { boolean transitionFired = false; int size = trace.getStates().size(); diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/StmtAssumeCollector.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/StmtAssumeCollector.java deleted file mode 100644 index cb3e5dcbdd..0000000000 --- a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/StmtAssumeCollector.java +++ /dev/null @@ -1,84 +0,0 @@ -package hu.bme.mit.theta.core.utils; - -import hu.bme.mit.theta.common.container.Containers; -import hu.bme.mit.theta.core.stmt.AssignStmt; -import hu.bme.mit.theta.core.stmt.AssumeStmt; -import hu.bme.mit.theta.core.stmt.HavocStmt; -import hu.bme.mit.theta.core.stmt.IfStmt; -import hu.bme.mit.theta.core.stmt.LoopStmt; -import hu.bme.mit.theta.core.stmt.NonDetStmt; -import hu.bme.mit.theta.core.stmt.OrtStmt; -import hu.bme.mit.theta.core.stmt.SequenceStmt; -import hu.bme.mit.theta.core.stmt.SkipStmt; -import hu.bme.mit.theta.core.stmt.Stmt; -import hu.bme.mit.theta.core.stmt.StmtVisitor; -import hu.bme.mit.theta.core.type.Expr; -import hu.bme.mit.theta.core.type.Type; -import hu.bme.mit.theta.core.type.booltype.BoolType; -import java.util.Set; - -public class StmtAssumeCollector { - - public static Set> collectAssumes(final Stmt stmt) { - final Set> assigns = Containers.createSet(); - stmt.accept(new StmtAssumeCollector.AllAssumesCollector(), assigns); - return assigns; - } - - private static class AllAssumesCollector implements - StmtVisitor>, Void> { - - @Override - public Void visit(SkipStmt stmt, Set> atoms) { - return null; - } - - @Override - public Void visit(AssumeStmt stmt, Set> atoms) { - atoms.addAll(ExprUtils.getAtoms(stmt.getCond())); - return null; - } - - @Override - public Void visit(AssignStmt stmt, - Set> atoms) { - return null; - } - - @Override - public Void visit(HavocStmt stmt, - Set> atoms) { - return null; - } - - @Override - public Void visit(SequenceStmt stmt, Set> atoms) { - stmt.getStmts().forEach(s -> s.accept(this, atoms)); - return null; - } - - @Override - public Void visit(NonDetStmt stmt, Set> atoms) { - stmt.getStmts().forEach(s -> s.accept(this, atoms)); - return null; - } - - @Override - public Void visit(OrtStmt stmt, Set> atoms) { - throw new UnsupportedOperationException(); - } - - @Override - public Void visit(LoopStmt stmt, Set> atoms) { - stmt.getStmt().accept(this, atoms); - return null; - } - - public Void visit(IfStmt stmt, Set> atoms) { - stmt.getThen().accept(this, atoms); - stmt.getElze().accept(this, atoms); - atoms.addAll(ExprUtils.getAtoms(stmt.getCond())); - return null; - } - } -} diff --git a/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/initprec/XstsTracegenPredInitPrec.kt b/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/initprec/XstsTracegenPredInitPrec.kt index 6efdea731a..3ae551c92b 100644 --- a/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/initprec/XstsTracegenPredInitPrec.kt +++ b/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/initprec/XstsTracegenPredInitPrec.kt @@ -3,7 +3,6 @@ package hu.bme.mit.theta.xsts.analysis.initprec import hu.bme.mit.theta.analysis.expl.ExplPrec import hu.bme.mit.theta.analysis.pred.PredPrec import hu.bme.mit.theta.analysis.prod2.Prod2Prec -import hu.bme.mit.theta.core.utils.StmtAssumeCollector import hu.bme.mit.theta.core.utils.StmtAtomCollector import hu.bme.mit.theta.xsts.XSTS diff --git a/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/tracegeneration/XstsTracegenBuilder.kt b/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/tracegeneration/XstsTracegenBuilder.kt index eb226096c1..99dda26400 100644 --- a/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/tracegeneration/XstsTracegenBuilder.kt +++ b/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/tracegeneration/XstsTracegenBuilder.kt @@ -1,8 +1,10 @@ package hu.bme.mit.theta.xsts.analysis.tracegeneration import com.google.common.base.Preconditions +import hu.bme.mit.theta.analysis.Action import hu.bme.mit.theta.analysis.Prec -import hu.bme.mit.theta.analysis.algorithm.ArgBuilder +import hu.bme.mit.theta.analysis.State +import hu.bme.mit.theta.analysis.algorithm.arg.ArgBuilder import hu.bme.mit.theta.analysis.algorithm.cegar.Abstractor import hu.bme.mit.theta.analysis.algorithm.cegar.BasicAbstractor import hu.bme.mit.theta.analysis.algorithm.cegar.abstractor.StopCriterions @@ -10,8 +12,6 @@ import hu.bme.mit.theta.analysis.algorithm.tracegeneration.TraceGenerationChecke import hu.bme.mit.theta.analysis.expl.* import hu.bme.mit.theta.analysis.expr.ExprAction import hu.bme.mit.theta.analysis.expr.ExprState -import hu.bme.mit.theta.analysis.expr.ExprStatePredicate -import hu.bme.mit.theta.analysis.pred.* import hu.bme.mit.theta.analysis.waitlist.PriorityWaitlist import hu.bme.mit.theta.common.logging.Logger import hu.bme.mit.theta.common.logging.NullLogger @@ -24,7 +24,6 @@ import hu.bme.mit.theta.xsts.XSTS import hu.bme.mit.theta.xsts.analysis.* import hu.bme.mit.theta.xsts.analysis.config.XstsConfigBuilder import hu.bme.mit.theta.xsts.analysis.initprec.XstsAllVarsInitPrec -import hu.bme.mit.theta.xsts.analysis.initprec.XstsTracegenPredInitPrec import hu.bme.mit.theta.xsts.analysis.initprec.XstsVarListInitPrec import java.io.File import java.io.IOException @@ -57,7 +56,7 @@ class XstsTracegenBuilder( return this } - private fun buildExpl(xsts: XSTS) : XstsTracegenConfig { + private fun buildExpl(xsts: XSTS) : XstsTracegenConfig { val solver2 = solverFactory.createSolver() // abstraction // TODO handle separate solvers in a nicer way @@ -70,7 +69,7 @@ class XstsTracegenBuilder( val argBuilder = ArgBuilder.create(lts, analysis, target, true) if (abstraction==TracegenerationAbstraction.VARLIST) { - val abstractor: Abstractor?, XstsAction?, ExplPrec?> = + val abstractor: Abstractor, XstsAction, ExplPrec> = BasicAbstractor.builder(argBuilder) .waitlist(PriorityWaitlist.create(XstsConfigBuilder.Search.DFS.comparator)) .stopCriterion(StopCriterions.fullExploration()) @@ -106,7 +105,7 @@ class XstsTracegenBuilder( } } else { assert(abstraction==TracegenerationAbstraction.NONE) - val abstractor: Abstractor?, XstsAction?, ExplPrec?> = + val abstractor: Abstractor, XstsAction, ExplPrec> = BasicAbstractor.builder(argBuilder) .waitlist(PriorityWaitlist.create(XstsConfigBuilder.Search.DFS.comparator)) .stopCriterion(StopCriterions.fullExploration()) @@ -154,7 +153,7 @@ class XstsTracegenBuilder( } */ - fun build(xsts: XSTS): XstsTracegenConfig { + fun build(xsts: XSTS): XstsTracegenConfig { val solver2 = solverFactory.createSolver() // abstraction // TODO handle separate solvers in a nicer way diff --git a/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/tracegeneration/XstsTracegenConfig.kt b/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/tracegeneration/XstsTracegenConfig.kt index c52b447885..136b47fd7a 100644 --- a/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/tracegeneration/XstsTracegenConfig.kt +++ b/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/tracegeneration/XstsTracegenConfig.kt @@ -1,22 +1,26 @@ package hu.bme.mit.theta.xsts.analysis.tracegeneration +import hu.bme.mit.theta.analysis.Action +import hu.bme.mit.theta.analysis.EmptyCex import hu.bme.mit.theta.analysis.Prec +import hu.bme.mit.theta.analysis.State import hu.bme.mit.theta.analysis.algorithm.SafetyResult import hu.bme.mit.theta.analysis.algorithm.tracegeneration.TraceGenerationChecker +import hu.bme.mit.theta.analysis.algorithm.tracegeneration.TraceGenerationResult import hu.bme.mit.theta.analysis.expr.ExprAction import hu.bme.mit.theta.analysis.expr.ExprState import hu.bme.mit.theta.analysis.expr.StmtAction -class XstsTracegenConfig private constructor( +class XstsTracegenConfig private constructor( private val checker: TraceGenerationChecker, private val prec: P ) { - fun check(): SafetyResult { + fun check(): SafetyResult, EmptyCex> { return checker.check(prec) } companion object { - fun create( + fun create( checker: TraceGenerationChecker, initPrec: P ): XstsTracegenConfig { return XstsTracegenConfig(checker, initPrec) diff --git a/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliBaseCommand.kt b/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliBaseCommand.kt index 90c2af692e..729302f57d 100644 --- a/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliBaseCommand.kt +++ b/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliBaseCommand.kt @@ -58,7 +58,7 @@ abstract class XstsCliBaseCommand(name: String? = null, help: String = "") : protected val logger: Logger by lazy { if (outputOptions.benchmarkMode) NullLogger.getInstance() else ConsoleLogger(outputOptions.logLevel) } - protected val writer = BasicTableWriter(System.out, ",", "\"", "\"") + protected val writer = BasicTableWriter(System.out, ",", "\"", "\"") // TODO shouldn't this be done through logger?? fun printError(exception: Exception) { val message = exception.message ?: "" diff --git a/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliMain.kt b/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliMain.kt index 73b01a8568..4d78312422 100644 --- a/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliMain.kt +++ b/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliMain.kt @@ -40,6 +40,6 @@ class XstsCliMainCommand : CliktCommand() { fun main(args: Array) = XstsCliMainCommand().subcommands( XstsCliCegar(), XstsCliBounded(), XstsCliMdd(), XstsCliPetrinetMdd(), XstsCliChc(), XstsCliHeader(), - XstsCliMetrics() + XstsCliMetrics(), XstsCliTracegen(), ) .main(args) \ No newline at end of file diff --git a/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliTracegen.kt b/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliTracegen.kt new file mode 100644 index 0000000000..07660c81d4 --- /dev/null +++ b/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliTracegen.kt @@ -0,0 +1,95 @@ +/* + * Copyright 2024 Budapest University of Technology and Economics + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * 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.option +import com.github.ajalt.clikt.parameters.types.file +import com.google.common.base.Stopwatch +import com.google.common.io.MoreFiles +import com.google.common.io.RecursiveDeleteOption +import hu.bme.mit.theta.analysis.Action +import hu.bme.mit.theta.analysis.EmptyCex +import hu.bme.mit.theta.analysis.Prec +import hu.bme.mit.theta.analysis.State +import hu.bme.mit.theta.analysis.algorithm.SafetyResult +import hu.bme.mit.theta.analysis.algorithm.tracegeneration.TraceGenerationResult +import hu.bme.mit.theta.common.logging.Logger +import hu.bme.mit.theta.solver.SolverManager +import hu.bme.mit.theta.solver.z3.Z3SolverFactory +import hu.bme.mit.theta.xsts.analysis.tracegeneration.XstsTracegenBuilder +import hu.bme.mit.theta.xsts.analysis.tracegeneration.XstsTracegenConfig +import hu.bme.mit.theta.xsts.dsl.XstsDslManager +import java.io.* +import java.util.concurrent.TimeUnit +import kotlin.system.exitProcess + + +class XstsCliTracegen : XstsCliBaseCommand( + name = "TRACEGEN", + help = "Trace generation (instead of verification). Property and input options will be ignored" +) { + val traceDir: File? by option( + help = "Directory the traces should be written into. If not specified, traces are written into model directory." + ).file(mustExist = true, canBeFile = false) + + private fun printResult(status: SafetyResult, EmptyCex>, totalTimeMs: Long) { + logger.write(Logger.Level.RESULT, "Successfully generated ${status.asSafe().witness.traces.size} traces in ${totalTimeMs}ms") + // TODO print coverage (full or not)? + logger.write(Logger.Level.VERBOSE, "Trace Metadata:") + logger.write(Logger.Level.VERBOSE, status.asSafe().witness.metadata.toString()) + } + + override fun run() { + try { + doRun() + } catch (e: Exception) { + printError(e) + exitProcess(1) + } + } + + private fun doRun() { + registerSolverManagers() + val solverFactory = SolverManager.resolveSolverFactory(solver) + + val modelFile = inputOptions.model + val tracePath = modelFile.parent + File.separator + "traces" + val traceDir = File(tracePath) + if (traceDir.exists()) { + MoreFiles.deleteRecursively(traceDir.toPath(), RecursiveDeleteOption.ALLOW_INSECURE) + } + traceDir.mkdir() + + val propStream = ByteArrayInputStream( + ("prop {\n" + + "\ttrue\n" + + "}\n").toByteArray()) + val xsts = XstsDslManager.createXsts( + SequenceInputStream(FileInputStream(modelFile), propStream) + ) + val sw = Stopwatch.createStarted() + val checker: XstsTracegenConfig = + XstsTracegenBuilder(Z3SolverFactory.getInstance(), true).logger(logger) + .setGetFullTraces(false).build(xsts) + val result = checker.check() + + // TODO concretization, writing into file + sw.stop() + printResult(result, sw.elapsed(TimeUnit.MILLISECONDS)) + } + +} \ No newline at end of file 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 24c474808f..edb15561c0 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 @@ -34,7 +34,6 @@ class InputOptions : OptionGroup( name = "Input options", help = "Options related to model and property input" ) { - val model: File by option( help = "Path of the input model (XSTS or Pnml). Extension should be .pnml to be handled as petri-net input" ).file(mustExist = true, canBeDir = false).required()