diff --git a/build.gradle.kts b/build.gradle.kts index 98c951d787..b9d79d9d42 100644 --- a/build.gradle.kts +++ b/build.gradle.kts @@ -10,7 +10,7 @@ buildscript { allprojects { group = "hu.bme.mit.inf.theta" - version = "2.12.1" + version = "2.13.0" apply(from = rootDir.resolve("gradle/shared-with-buildSrc/mirrors.gradle.kts")) } diff --git a/doc/CEGAR-algorithms.md b/doc/CEGAR-algorithms.md index 9377275491..bac81ae6ca 100644 --- a/doc/CEGAR-algorithms.md +++ b/doc/CEGAR-algorithms.md @@ -36,8 +36,7 @@ The domain controls the abstract information that is being tracked about the sys * `PRED_BOOL`: [Boolean predicate abstraction](https://link.springer.com/article/10.1007/s10009-002-0095-0) keeps track of arbitrary Boolean combination of predicates. * `PRED_SPLIT`: Boolean predicate abstraction, but states are [split]((https://link.springer.com/content/pdf/10.1007%2Fs10817-019-09535-x.pdf)) into sub-states along disjunctions. * `EXPL`: [Explicit-value abstraction]((https://link.springer.com/chapter/10.1007/978-3-642-37057-1_11)) keeps track of concrete values, but only for a (continuously expanded) set of variables. -* `PROD`: Product abstraction, available for XSTS models. The set of control variables (marked with `ctrl`) are tracked explicitly while others are tracked by predicates. -* `PROD_AUTO`: Automatic product abstraction, available for XSTS models. The set of control variables (marked with `ctrl`) are tracked explicitly. Other variables are also tracked explicitly if they appear in a given number of predicates (defined with the `--maxpredcount` option). +* `EXPL_PRED_CARD`, `EXPL_PRED_SPLIT` and `EXPL_PRED_BOOL`: Product abstraction domains, available for XSTS models. The set of control variables (marked with `ctrl`) are tracked explicitly while others are tracked by predicates (using the corresponding predicate domain). Other variables are also tracked explicitly if they appear in a given number of predicates (defined with the `--maxpredcount` option). Predicate abstraction (`PRED_*`) tracks logical formulas instead of concrete values of variables, which can be efficient for variables with large (or infinite) domain. Explicit-values (`EXPL`) keep track of a subset of system variables, which can be efficient if variables are mostly deterministic or have a small domain. @@ -58,7 +57,7 @@ Controls the initial precision of the abstraction (e.g., what predicates or vari * `ALLVARS`: Tracks all variables from the beginning. Available for CFA and XSTS if `--domain` is `EXPL`. * `ALLASSUMES`: Track all assumptions by default (e.g., branch/loop conditions). Only applicable for CFA and if `--domain` is `PRED_*`. * `PROP`: Available for XSTS. Tracks variables from the property if `--domain` is `EXPL` and predicates from the property if `--domain` is `PRED_*`. -* `CTRL`: Available for XSTS if `--domain` is `PROD` or `EXPL`. Tracks all control variables. +* `CTRL`: Available for XSTS if `--domain` is `EXPL` or `EXPL_PRED_*`. Tracks all control variables. We observed that usually the `EMPTY` initial precision yields good performance: the algorithm can automatically determine the precision. However, if the system is mostly deterministic, it might be suitable to track all variables from the beginning. @@ -93,7 +92,7 @@ In general, values between `5` to `50` perform well (see Section 3.1.1 of [our J ### `--maxpredcount` Available for XSTS. -The number of predicates a variable has to appear in before it is tracked explicitly when the `PRED_AUTO` domain is used. +The number of predicates a variable has to appear in before it is tracked explicitly when `--domain` is `EXPL_PRED_*`. Default is `0` (unlimited). ### `--refinement` diff --git a/subprojects/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/CfaInitPrecs.java b/subprojects/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/CfaInitPrecs.java index 302427a300..dd13fcbcc2 100644 --- a/subprojects/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/CfaInitPrecs.java +++ b/subprojects/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/CfaInitPrecs.java @@ -10,8 +10,8 @@ import hu.bme.mit.theta.core.type.booltype.BoolType; import hu.bme.mit.theta.core.utils.ExprUtils; -import java.util.HashMap; -import java.util.HashSet; +import hu.bme.mit.theta.common.container.Containers; + import java.util.Map; import java.util.Set; @@ -20,9 +20,9 @@ public final class CfaInitPrecs { private CfaInitPrecs() {} public static LocalCfaPrec collectAssumesLocal(CFA cfa) { - Map precs = new HashMap<>(); + Map precs = Containers.createMap(); for (CFA.Loc l : cfa.getLocs()) { - Set> exprs = new HashSet<>(); + Set> exprs = Containers.createSet(); for (CFA.Edge e : l.getInEdges()) { CFA.Edge running = e; while (running != null) { @@ -42,7 +42,7 @@ public static LocalCfaPrec collectAssumesLocal(CFA cfa) { } public static GlobalCfaPrec collectAssumesGlobal(CFA cfa) { - Set> assumes = new HashSet<>(); + Set> assumes = Containers.createSet(); for (CFA.Edge e : cfa.getEdges()) { if (e.getStmt() instanceof AssumeStmt) { AssumeStmt assumeStmt = (AssumeStmt)e.getStmt(); diff --git a/subprojects/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/DistToErrComparator.java b/subprojects/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/DistToErrComparator.java index ed283affc8..13d0876b6f 100644 --- a/subprojects/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/DistToErrComparator.java +++ b/subprojects/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/DistToErrComparator.java @@ -17,7 +17,7 @@ import static com.google.common.base.Preconditions.checkArgument; -import java.util.HashMap; +import hu.bme.mit.theta.common.container.Containers; import java.util.LinkedList; import java.util.List; import java.util.Map; @@ -83,7 +83,7 @@ private int getDistanceToError(final Loc loc) { static Map calculateDistancesToError(final CFA cfa, final Loc errLoc) { List queue = new LinkedList<>(); - final Map distancesToError = new HashMap<>(); + final Map distancesToError = Containers.createMap(); queue.add(errLoc); distancesToError.put(errLoc, 0); int distance = 1; diff --git a/subprojects/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/impact/ImpactReachedSet.java b/subprojects/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/impact/ImpactReachedSet.java index a8c93b76e9..0480ae5c5a 100644 --- a/subprojects/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/impact/ImpactReachedSet.java +++ b/subprojects/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/impact/ImpactReachedSet.java @@ -20,7 +20,7 @@ import java.util.ArrayList; import java.util.Collection; import java.util.Collections; -import java.util.HashMap; +import hu.bme.mit.theta.common.container.Containers; import java.util.List; import java.util.Map; import java.util.function.Function; @@ -38,7 +38,7 @@ public final class ImpactReachedSet implem private ImpactReachedSet(final Function partitioning) { this.partitioning = checkNotNull(partitioning); - partitions = new HashMap<>(); + partitions = Containers.createMap(); } public static ImpactReachedSet create( diff --git a/subprojects/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/lts/CfaCachedLts.java b/subprojects/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/lts/CfaCachedLts.java index 8c82664d31..6bd8ca3acc 100644 --- a/subprojects/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/lts/CfaCachedLts.java +++ b/subprojects/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/lts/CfaCachedLts.java @@ -1,7 +1,7 @@ package hu.bme.mit.theta.cfa.analysis.lts; import java.util.Collection; -import java.util.HashMap; +import hu.bme.mit.theta.common.container.Containers; import java.util.Map; import hu.bme.mit.theta.cfa.CFA.Loc; @@ -19,7 +19,7 @@ public final class CfaCachedLts implements CfaLts { public CfaCachedLts(final CfaLts lts) { this.lts = lts; - this.actionCache = new HashMap<>(); + this.actionCache = Containers.createMap(); } @Override diff --git a/subprojects/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/prec/LocalCfaPrec.java b/subprojects/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/prec/LocalCfaPrec.java index 8917a1a4dc..31f7508440 100644 --- a/subprojects/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/prec/LocalCfaPrec.java +++ b/subprojects/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/prec/LocalCfaPrec.java @@ -18,7 +18,7 @@ import static com.google.common.base.Preconditions.checkNotNull; import java.util.Collections; -import java.util.HashMap; +import hu.bme.mit.theta.common.container.Containers; import java.util.Map; import java.util.Map.Entry; import java.util.NoSuchElementException; @@ -80,7 +80,7 @@ public P getPrec(final Loc loc) { public LocalCfaPrec

refine(final Map refinedPrecs) { checkNotNull(refinedPrecs); - final Map refinedMapping = new HashMap<>(this.mapping); + final Map refinedMapping = Containers.createMap(this.mapping); for (final Entry entry : refinedPrecs.entrySet()) { final Loc loc = entry.getKey(); diff --git a/subprojects/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/prec/LocalCfaPrecRefiner.java b/subprojects/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/prec/LocalCfaPrecRefiner.java index f0edd21dac..5eab5e9476 100644 --- a/subprojects/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/prec/LocalCfaPrecRefiner.java +++ b/subprojects/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/prec/LocalCfaPrecRefiner.java @@ -18,7 +18,7 @@ import static com.google.common.base.Preconditions.checkArgument; import static com.google.common.base.Preconditions.checkNotNull; -import java.util.HashMap; +import hu.bme.mit.theta.common.container.Containers; import java.util.Map; import hu.bme.mit.theta.analysis.Action; @@ -59,7 +59,7 @@ public CfaPrec

refine(final CfaPrec

prec, final Trace, A> trac // joining them to the old precision of the location final LocalCfaPrec

genPrec = (LocalCfaPrec

) prec; - final Map runningPrecs = new HashMap<>(); + final Map runningPrecs = Containers.createMap(); for (final CfaState state : trace.getStates()) { runningPrecs.put(state.getLoc(), genPrec.getPrec(state.getLoc())); } diff --git a/subprojects/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/utils/CfaVisualizer.java b/subprojects/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/utils/CfaVisualizer.java index 139e0efa51..5c77c3a00e 100644 --- a/subprojects/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/utils/CfaVisualizer.java +++ b/subprojects/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/utils/CfaVisualizer.java @@ -16,7 +16,7 @@ package hu.bme.mit.theta.cfa.analysis.utils; import java.awt.Color; -import java.util.HashMap; +import hu.bme.mit.theta.common.container.Containers; import java.util.LinkedHashSet; import java.util.Map; import java.util.Optional; @@ -56,7 +56,7 @@ private CfaVisualizer() { public static Graph visualize(final CFA cfa) { final Graph graph = new Graph(CFA_ID, CFA_LABEL); - final Map ids = new HashMap<>(); + final Map ids = Containers.createMap(); addVars(graph, cfa); for (final Loc loc : cfa.getLocs()) { addLocation(graph, cfa, loc, ids); diff --git a/subprojects/cfa/cfa-analysis/src/test/java/hu/bme/mit/theta/cfa/analysis/EncodingTest.java b/subprojects/cfa/cfa-analysis/src/test/java/hu/bme/mit/theta/cfa/analysis/EncodingTest.java index c90ec26889..6cc225b677 100644 --- a/subprojects/cfa/cfa-analysis/src/test/java/hu/bme/mit/theta/cfa/analysis/EncodingTest.java +++ b/subprojects/cfa/cfa-analysis/src/test/java/hu/bme/mit/theta/cfa/analysis/EncodingTest.java @@ -15,7 +15,7 @@ import java.io.FileInputStream; import java.io.IOException; -import java.util.HashSet; +import hu.bme.mit.theta.common.container.Containers; import java.util.Set; public class EncodingTest { @@ -30,7 +30,7 @@ private CFA.Loc getLocByName(String name) { } private Set getNextLocs(CfaLts lts, String loc) { - Set locs = new HashSet<>(); + Set locs = Containers.createSet(); SS ss = new SS(); for (var act : lts.getEnabledActionsFor(CfaState.of(getLocByName(loc), ss))) { locs.add(act.getTarget().getName()); diff --git a/subprojects/cfa/cfa-cli/src/main/java/hu/bme/mit/theta/cfa/cli/CfaMetrics.java b/subprojects/cfa/cfa-cli/src/main/java/hu/bme/mit/theta/cfa/cli/CfaMetrics.java index bdb64217cf..e8a9c689c1 100644 --- a/subprojects/cfa/cfa-cli/src/main/java/hu/bme/mit/theta/cfa/cli/CfaMetrics.java +++ b/subprojects/cfa/cfa-cli/src/main/java/hu/bme/mit/theta/cfa/cli/CfaMetrics.java @@ -25,7 +25,7 @@ import hu.bme.mit.theta.core.type.bvtype.BvType; import hu.bme.mit.theta.core.type.inttype.IntType; -import java.util.HashSet; +import hu.bme.mit.theta.common.container.Containers; import java.util.LinkedList; import java.util.Queue; import java.util.Set; @@ -48,7 +48,7 @@ public static void printMetrics(Logger logger, CFA cfa){ } public static int getCfaComponents(final CFA cfa) { - final Set visited = new HashSet<>(); + final Set visited = Containers.createSet(); int components = 0; for (final CFA.Loc loc : cfa.getLocs()) { diff --git a/subprojects/cfa/cfa/src/main/java/hu/bme/mit/theta/cfa/CFA.java b/subprojects/cfa/cfa/src/main/java/hu/bme/mit/theta/cfa/CFA.java index 387b73ae06..14d6428d3f 100644 --- a/subprojects/cfa/cfa/src/main/java/hu/bme/mit/theta/cfa/CFA.java +++ b/subprojects/cfa/cfa/src/main/java/hu/bme/mit/theta/cfa/CFA.java @@ -27,6 +27,7 @@ import com.google.common.collect.ImmutableSet; import hu.bme.mit.theta.common.Utils; +import hu.bme.mit.theta.common.container.Containers; import hu.bme.mit.theta.core.decl.VarDecl; import hu.bme.mit.theta.core.stmt.Stmt; import hu.bme.mit.theta.core.utils.StmtUtils; @@ -176,7 +177,7 @@ public static final class Builder { private boolean built; private Builder() { - locs = new HashSet<>(); + locs = Containers.createSet(); edges = new LinkedList<>(); built = false; } diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/ARG.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/ARG.java index 4eede1fe9f..16221bf33e 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/ARG.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/ARG.java @@ -21,7 +21,7 @@ import static java.util.stream.Collectors.toList; import java.util.Collection; -import java.util.HashSet; +import hu.bme.mit.theta.common.container.Containers; import java.util.Optional; import java.util.OptionalInt; import java.util.stream.Stream; @@ -42,7 +42,7 @@ public final class ARG { final PartialOrd partialOrd; private ARG(final PartialOrd partialOrd) { - initNodes = new HashSet<>(); + initNodes = Containers.createSet(); this.partialOrd = partialOrd; this.initialized = false; } diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/ArgNode.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/ArgNode.java index c1130757d6..039c50c95f 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/ArgNode.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/ArgNode.java @@ -20,7 +20,7 @@ import java.util.ArrayList; import java.util.Collection; -import java.util.HashSet; +import hu.bme.mit.theta.common.container.Containers; import java.util.Optional; import java.util.stream.Stream; @@ -58,7 +58,7 @@ public final class ArgNode { inEdge = Optional.empty(); outEdges = new ArrayList<>(); coveringNode = Optional.empty(); - coveredNodes = new HashSet<>(); + coveredNodes = Containers.createSet(); expanded = false; } diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/expl/ExplStmtOptimizer.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/expl/ExplStmtOptimizer.java new file mode 100644 index 0000000000..8906f6733b --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/expl/ExplStmtOptimizer.java @@ -0,0 +1,23 @@ +package hu.bme.mit.theta.analysis.expl; + +import hu.bme.mit.theta.analysis.stmtoptimizer.StmtOptimizer; +import hu.bme.mit.theta.analysis.stmtoptimizer.StmtSimplifier; +import hu.bme.mit.theta.core.stmt.Stmt; + +public class ExplStmtOptimizer implements StmtOptimizer { + + private ExplStmtOptimizer(){} + + private static class LazyHolder { + static final ExplStmtOptimizer INSTANCE = new ExplStmtOptimizer(); + } + + public static ExplStmtOptimizer getInstance() { + return LazyHolder.INSTANCE; + } + + @Override + public Stmt optimizeStmt(final ExplState state, final Stmt stmt) { + return StmtSimplifier.simplifyStmt(state,stmt); + } +} diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/expl/StmtApplier.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/expl/StmtApplier.java index bf855b7d75..99616721b2 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/expl/StmtApplier.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/expl/StmtApplier.java @@ -32,7 +32,7 @@ import java.util.ArrayList; import java.util.List; -final class StmtApplier { +public final class StmtApplier { public enum ApplyResult { FAILURE, SUCCESS, BOTTOM @@ -62,6 +62,9 @@ public static ApplyResult apply(final Stmt stmt, final MutableValuation val, fin } else if (stmt instanceof OrtStmt) { final OrtStmt ortStmt = (OrtStmt) stmt; return applyOrt(ortStmt, val, approximate); + } else if (stmt instanceof LoopStmt) { + final LoopStmt loopStmt = (LoopStmt) stmt; + return applyLoop(loopStmt, val, approximate); } else { throw new UnsupportedOperationException("Unhandled statement: " + stmt); } @@ -170,6 +173,11 @@ private static ApplyResult applySequence(final SequenceStmt stmt, final MutableV return ApplyResult.SUCCESS; } + private static ApplyResult applyLoop(final LoopStmt stmt, final MutableValuation val, + final boolean approximate) { + throw new UnsupportedOperationException(String.format("Loop statement %s was not unrolled",stmt)); + } + private static ApplyResult applyNonDet(final NonDetStmt stmt, final MutableValuation val, final boolean approximate) { List valuations = new ArrayList(); diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/expr/refinement/ExprTraceNewtonChecker.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/expr/refinement/ExprTraceNewtonChecker.java index 92b187b8c3..903d2aae94 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/expr/refinement/ExprTraceNewtonChecker.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/expr/refinement/ExprTraceNewtonChecker.java @@ -13,15 +13,7 @@ import hu.bme.mit.theta.core.model.BasicSubstitution; import hu.bme.mit.theta.core.model.ImmutableValuation; import hu.bme.mit.theta.core.model.Valuation; -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.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.stmt.*; 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; @@ -35,11 +27,10 @@ import hu.bme.mit.theta.solver.Solver; import hu.bme.mit.theta.solver.utils.WithPushPop; -import java.util.ArrayList; -import java.util.Collection; -import java.util.Collections; -import java.util.HashSet; -import java.util.List; +import java.util.*; + +import hu.bme.mit.theta.common.container.Containers; + import java.util.stream.Collectors; import java.util.stream.IntStream; import java.util.stream.Stream; @@ -284,6 +275,11 @@ public Stmt visit(NonDetStmt stmt, Void param) { public Stmt visit(OrtStmt stmt, Void param) { throw new UnsupportedOperationException(); } + + @Override + public Stmt visit(LoopStmt stmt, Void param) { + throw new UnsupportedOperationException(); + } }, null); } @@ -354,7 +350,7 @@ private List> computeAssertionsFromTraceWithWeakestPrecondition( */ private Collection> collectVariablesInTrace(final Trace trace) { - var variables = new HashSet>(); + Set> variables = Containers.createSet(); for(var state : trace.getStates()) { ExprUtils.collectVars(state.toExpr(), variables); @@ -402,6 +398,9 @@ public Collection> visit(NonDetStmt stmt, Void param) { public Collection> visit(OrtStmt stmt, Void param) { throw new UnsupportedOperationException(); } + + @Override + public Collection> visit(LoopStmt stmt, Void param) { throw new UnsupportedOperationException(); } }, null); } @@ -441,6 +440,9 @@ public Collection> visit(NonDetStmt stmt, Void param) { public Collection> visit(OrtStmt stmt, Void param) { throw new UnsupportedOperationException(); } + + @Override + public Collection> visit(LoopStmt stmt, Void param) { throw new UnsupportedOperationException(); } }, null); } @@ -480,6 +482,9 @@ public Collection> visit(NonDetStmt stmt, Void param) { public Collection> visit(OrtStmt stmt, Void param) { throw new UnsupportedOperationException(); } + + @Override + public Collection> visit(LoopStmt stmt, Void param) { throw new UnsupportedOperationException(); } }, null); } @@ -501,7 +506,7 @@ private List>> collectFutureLiveVariablesForTrace(final Tr futureLiveVariables.set(stateCount - 1, Collections.emptySet()); for(var i = stateCount - 2; i >= 0; i--) { - var vars = new HashSet<>(futureLiveVariables.get(i + 1)); + var vars = Containers.createSet(futureLiveVariables.get(i + 1)); vars.addAll(actionReadsVariables(trace.getAction(i))); vars.removeAll(actionWritesVariables(trace.getAction(i))); vars.removeAll(actionHavocsVariables(trace.getAction(i))); @@ -517,7 +522,7 @@ private List>> collectPastLiveVariablesForTrace(final Trac pastLiveVariables.set(0, Collections.emptySet()); for(var i = 1; i < stateCount; i++) { - var vars = new HashSet<>(pastLiveVariables.get(i - 1)); + var vars = Containers.createSet(pastLiveVariables.get(i - 1)); vars.addAll(actionReadsVariables(trace.getAction(i - 1))); vars.addAll(actionWritesVariables(trace.getAction(i - 1))); vars.removeAll(actionHavocsVariables(trace.getAction(i - 1))); diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/expr/refinement/ExprTraceUCBChecker.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/expr/refinement/ExprTraceUCBChecker.java index 7319d3b88e..e1a9737537 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/expr/refinement/ExprTraceUCBChecker.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/expr/refinement/ExprTraceUCBChecker.java @@ -26,7 +26,7 @@ import java.util.ArrayList; import java.util.Collection; import java.util.Collections; -import java.util.HashSet; +import hu.bme.mit.theta.common.container.Containers; import java.util.List; import java.util.stream.Collectors; import java.util.stream.IntStream; @@ -180,7 +180,7 @@ private ExprTraceStatus.Infeasible createRefinement( /* Add the negated of the above expression as the new predicate */ predicates.add( ExprSimplifier.simplify( - Not(And(new HashSet<>(predicate))), + Not(And(Containers.createSet(predicate))), ImmutableValuation.empty() ) ); diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/pred/PredAbstractors.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/pred/PredAbstractors.java index 79f6f708bd..6808e72486 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/pred/PredAbstractors.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/pred/PredAbstractors.java @@ -25,7 +25,7 @@ import java.util.ArrayList; import java.util.Collection; import java.util.Collections; -import java.util.HashSet; +import hu.bme.mit.theta.common.container.Containers; import java.util.LinkedList; import java.util.List; import java.util.Optional; @@ -137,7 +137,7 @@ public Collection createStatesForExpr(final Expr expr, fina } while (solver.check().isSat()) { final Valuation model = solver.getModel(); - final Set> newStatePreds = new HashSet<>(); + final Set> newStatePreds = Containers.createSet(); final List> feedback = new LinkedList<>(); feedback.add(True()); for (int i = 0; i < preds.size(); ++i) { diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/pred/PredPrec.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/pred/PredPrec.java index 3c7b100ac0..b209880630 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/pred/PredPrec.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/pred/PredPrec.java @@ -21,7 +21,6 @@ import java.util.Collection; import java.util.Collections; -import java.util.HashMap; import java.util.Map; import java.util.Set; @@ -29,6 +28,7 @@ import hu.bme.mit.theta.analysis.Prec; import hu.bme.mit.theta.common.Utils; +import hu.bme.mit.theta.common.container.Containers; import hu.bme.mit.theta.core.type.Expr; import hu.bme.mit.theta.core.type.booltype.BoolLitExpr; import hu.bme.mit.theta.core.type.booltype.BoolType; @@ -44,7 +44,7 @@ public final class PredPrec implements Prec { private PredPrec(final Iterable> preds) { checkNotNull(preds); - this.predToNegMap = new HashMap<>(); + this.predToNegMap = Containers.createMap(); for (final Expr pred : preds) { if (pred instanceof BoolLitExpr) { diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/pred/PredStmtOptimizer.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/pred/PredStmtOptimizer.java new file mode 100644 index 0000000000..942be26b85 --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/pred/PredStmtOptimizer.java @@ -0,0 +1,24 @@ +package hu.bme.mit.theta.analysis.pred; + +import hu.bme.mit.theta.analysis.stmtoptimizer.StmtOptimizer; +import hu.bme.mit.theta.analysis.stmtoptimizer.StmtSimplifier; +import hu.bme.mit.theta.core.model.ImmutableValuation; +import hu.bme.mit.theta.core.stmt.Stmt; + +public class PredStmtOptimizer implements StmtOptimizer { + + private PredStmtOptimizer(){} + + private static class LazyHolder { + static final PredStmtOptimizer INSTANCE = new PredStmtOptimizer(); + } + + public static PredStmtOptimizer getInstance() { + return PredStmtOptimizer.LazyHolder.INSTANCE; + } + + @Override + public Stmt optimizeStmt(final PredState state, final Stmt stmt){ + return StmtSimplifier.simplifyStmt(ImmutableValuation.empty(),stmt); + } +} diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/prod2/Prod2StmtOptimizer.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/prod2/Prod2StmtOptimizer.java new file mode 100644 index 0000000000..230673f93d --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/prod2/Prod2StmtOptimizer.java @@ -0,0 +1,27 @@ +package hu.bme.mit.theta.analysis.prod2; + +import hu.bme.mit.theta.analysis.Action; +import hu.bme.mit.theta.analysis.State; +import hu.bme.mit.theta.analysis.stmtoptimizer.StmtOptimizer; +import hu.bme.mit.theta.core.stmt.Stmt; + +public class Prod2StmtOptimizer implements StmtOptimizer> { + + private final StmtOptimizer stmtOptimizer1; + private final StmtOptimizer stmtOptimizer2; + + private Prod2StmtOptimizer(final StmtOptimizer stmtOptimizer1, final StmtOptimizer stmtOptimizer2) { + this.stmtOptimizer1 = stmtOptimizer1; + this.stmtOptimizer2 = stmtOptimizer2; + } + + public static Prod2StmtOptimizer create(final StmtOptimizer stmtOptimizer1, + final StmtOptimizer stmtOptimizer2){ + return new Prod2StmtOptimizer<>(stmtOptimizer1,stmtOptimizer2); + } + + @Override + public Stmt optimizeStmt(final Prod2State state, final Stmt stmt) { + return stmtOptimizer2.optimizeStmt(state.getState2(),stmtOptimizer1.optimizeStmt(state.getState1(),stmt)); + } +} diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/prod2/prod2explpred/AutomaticItpRefToProd2ExplPredPrec.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/prod2/prod2explpred/AutomaticItpRefToProd2ExplPredPrec.java index d5e3b2c6fa..06f9e93f18 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/prod2/prod2explpred/AutomaticItpRefToProd2ExplPredPrec.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/prod2/prod2explpred/AutomaticItpRefToProd2ExplPredPrec.java @@ -12,9 +12,11 @@ import hu.bme.mit.theta.core.utils.ExprUtils; import java.util.*; +import java.util.stream.Collectors; import static com.google.common.base.Preconditions.checkArgument; import static com.google.common.base.Preconditions.checkNotNull; +import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Bool; public final class AutomaticItpRefToProd2ExplPredPrec implements RefutationToPrec, ItpRefutation> { @@ -28,7 +30,7 @@ private AutomaticItpRefToProd2ExplPredPrec(final Set> explPreferredVa this.exprSplitter = checkNotNull(exprSplitter); this.maxPredCount = maxPredCount; - this.predCount = new HashMap<>(); + this.predCount = new LinkedHashMap<>(); } public static AutomaticItpRefToProd2ExplPredPrec create(final Set> explPreferredVars, final ExprSplitter exprSplitter, final int maxPredCount) { @@ -39,13 +41,13 @@ public static AutomaticItpRefToProd2ExplPredPrec create(final Set> ex @Override public Prod2Prec toPrec(ItpRefutation refutation, int index) { final Collection> exprs = exprSplitter.apply(refutation.get(index)); - Set> explSelectedVars = new HashSet<>(); - Set> predSelectedExprs = new HashSet<>(); + Set> explSelectedVars = new LinkedHashSet<>(); + Set> predSelectedExprs = new LinkedHashSet<>(); for (var expr : exprs) { final Set> containedVars = ExprUtils.getVars(expr); boolean allExpl = true; for (var decl : containedVars) { - if(maxPredCount>=0){ + if(maxPredCount>0){ if (!predCount.containsKey(decl)) { predCount.put(decl, 1); } @@ -55,6 +57,9 @@ public Prod2Prec toPrec(ItpRefutation refutation, int index) predCount.put(decl, predCount.get(decl) + 1); } } + if(decl.getType() == Bool()){ + explPreferredVars.add(decl); + } if (explPreferredVars.contains(decl)) { explSelectedVars.add(decl); } else allExpl = false; @@ -67,7 +72,13 @@ public Prod2Prec toPrec(ItpRefutation refutation, int index) @Override public Prod2Prec join(Prod2Prec prec1, Prod2Prec prec2) { - return Prod2Prec.of(prec1.getPrec1().join(prec2.getPrec1()), prec1.getPrec2().join(prec2.getPrec2())); + final ExplPrec joinedExpl = prec1.getPrec1().join(prec2.getPrec1()); + final PredPrec joinedPred = prec1.getPrec2().join(prec2.getPrec2()); + final var filteredPreds = joinedPred.getPreds().stream() + .filter(pred -> !ExprUtils.getVars(pred).stream().allMatch(decl -> joinedExpl.getVars().contains(decl))) + .collect(Collectors.toList()); + final PredPrec filteredPred = PredPrec.of(filteredPreds); + return Prod2Prec.of(joinedExpl,filteredPred); } @Override diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/prod2/prod2explpred/ItpRefToProd2ExplPredPrec.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/prod2/prod2explpred/ItpRefToProd2ExplPredPrec.java index a5b294d7b4..831af65d7e 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/prod2/prod2explpred/ItpRefToProd2ExplPredPrec.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/prod2/prod2explpred/ItpRefToProd2ExplPredPrec.java @@ -12,7 +12,7 @@ import hu.bme.mit.theta.core.utils.ExprUtils; import java.util.Collection; -import java.util.HashSet; +import hu.bme.mit.theta.common.container.Containers; import java.util.Set; import static com.google.common.base.Preconditions.checkNotNull; @@ -34,8 +34,8 @@ public static ItpRefToProd2ExplPredPrec create(final Set> explPreferr @Override public Prod2Prec toPrec(ItpRefutation refutation, int index) { final Collection> exprs = exprSplitter.apply(refutation.get(index)); - Set> explSelectedVars = new HashSet<>(); - Set> predSelectedExprs = new HashSet<>(); + Set> explSelectedVars = Containers.createSet(); + Set> predSelectedExprs = Containers.createSet(); for (var expr : exprs) { final Set> containedVars = ExprUtils.getVars(expr); boolean allExpl = true; diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/prod2/prod2explpred/Prod2ExplPredStmtOptimizer.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/prod2/prod2explpred/Prod2ExplPredStmtOptimizer.java new file mode 100644 index 0000000000..9e96fc336e --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/prod2/prod2explpred/Prod2ExplPredStmtOptimizer.java @@ -0,0 +1,25 @@ +package hu.bme.mit.theta.analysis.prod2.prod2explpred; + +import hu.bme.mit.theta.analysis.stmtoptimizer.StmtOptimizer; +import hu.bme.mit.theta.analysis.expl.ExplState; +import hu.bme.mit.theta.analysis.pred.PredState; +import hu.bme.mit.theta.analysis.prod2.Prod2State; +import hu.bme.mit.theta.core.stmt.Stmt; + +public class Prod2ExplPredStmtOptimizer implements StmtOptimizer> { + + private final StmtOptimizer stmtOptimizer; + + private Prod2ExplPredStmtOptimizer(final StmtOptimizer stmtOptimizer) { + this.stmtOptimizer = stmtOptimizer; + } + + public static Prod2ExplPredStmtOptimizer create(final StmtOptimizer stmtOptimizer){ + return new Prod2ExplPredStmtOptimizer(stmtOptimizer); + } + + @Override + public Stmt optimizeStmt(Prod2State state, Stmt stmt) { + return stmtOptimizer.optimizeStmt(state.getState1(),stmt); + } +} diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/prod2/prod2explpred/Prod2ExplPredStrengtheningOperator.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/prod2/prod2explpred/Prod2ExplPredStrengtheningOperator.java index f36a64be64..beec656d7a 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/prod2/prod2explpred/Prod2ExplPredStrengtheningOperator.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/prod2/prod2explpred/Prod2ExplPredStrengtheningOperator.java @@ -12,7 +12,7 @@ import hu.bme.mit.theta.solver.utils.WithPushPop; import java.util.Collection; -import java.util.HashSet; +import hu.bme.mit.theta.common.container.Containers; import java.util.Set; public final class Prod2ExplPredStrengtheningOperator implements StrengtheningOperator { @@ -30,7 +30,7 @@ public static Prod2ExplPredStrengtheningOperator create(final Solver solver) { @Override public Collection> strengthen(Collection> prod2States, Prod2Prec prec) { - Set> validStates = new HashSet<>(); + Set> validStates = Containers.createSet(); for (Prod2State prod2State : prod2States) { @@ -45,7 +45,7 @@ public Collection> strengthen(Collection(); + var removed = Containers.createSet(); for (var state : prod2States) { if (!validStates.contains(state)) removed.add(state); } diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/reachedset/Partition.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/reachedset/Partition.java index 8179e1e2c7..8e054bc9d3 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/reachedset/Partition.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/reachedset/Partition.java @@ -15,12 +15,13 @@ */ package hu.bme.mit.theta.analysis.reachedset; +import hu.bme.mit.theta.common.container.Containers; + import static com.google.common.base.Preconditions.checkNotNull; import java.util.ArrayList; import java.util.Collection; import java.util.Collections; -import java.util.HashMap; import java.util.List; import java.util.Map; import java.util.function.Function; @@ -33,7 +34,7 @@ public final class Partition { private Partition(final Function projection) { this.projection = checkNotNull(projection); - classes = new HashMap<>(); + classes = Containers.createMap(); } public static Partition of(final Function projection) { diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/stmtoptimizer/DefaultStmtOptimizer.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/stmtoptimizer/DefaultStmtOptimizer.java new file mode 100644 index 0000000000..7029bb87ad --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/stmtoptimizer/DefaultStmtOptimizer.java @@ -0,0 +1,17 @@ +package hu.bme.mit.theta.analysis.stmtoptimizer; + +import hu.bme.mit.theta.analysis.State; +import hu.bme.mit.theta.core.stmt.Stmt; + +public class DefaultStmtOptimizer implements StmtOptimizer { + + public static DefaultStmtOptimizer create() { + return new DefaultStmtOptimizer<>(); + } + + @Override + public Stmt optimizeStmt(S state, Stmt stmt) { + return stmt; + } + +} diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/stmtoptimizer/StmtOptimizer.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/stmtoptimizer/StmtOptimizer.java new file mode 100644 index 0000000000..e029e47d05 --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/stmtoptimizer/StmtOptimizer.java @@ -0,0 +1,10 @@ +package hu.bme.mit.theta.analysis.stmtoptimizer; + +import hu.bme.mit.theta.analysis.State; +import hu.bme.mit.theta.core.stmt.Stmt; + +public interface StmtOptimizer{ + + Stmt optimizeStmt(final S state, final Stmt stmt); + +} diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/stmtoptimizer/StmtSimplifier.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/stmtoptimizer/StmtSimplifier.java new file mode 100644 index 0000000000..63a4e19c76 --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/stmtoptimizer/StmtSimplifier.java @@ -0,0 +1,173 @@ +package hu.bme.mit.theta.analysis.stmtoptimizer; + +import com.google.common.collect.ImmutableList; +import hu.bme.mit.theta.core.decl.Decl; +import hu.bme.mit.theta.core.decl.VarDecl; +import hu.bme.mit.theta.core.model.MutableValuation; +import hu.bme.mit.theta.core.model.Valuation; +import hu.bme.mit.theta.core.stmt.*; +import hu.bme.mit.theta.core.type.Expr; +import hu.bme.mit.theta.core.type.LitExpr; +import hu.bme.mit.theta.core.type.Type; +import hu.bme.mit.theta.core.type.booltype.BoolLitExpr; +import hu.bme.mit.theta.core.type.booltype.BoolType; +import hu.bme.mit.theta.core.type.inttype.IntLitExpr; +import hu.bme.mit.theta.core.utils.ExprUtils; + +import java.math.BigInteger; +import java.util.ArrayList; +import java.util.List; +import java.util.stream.Collectors; + +import static hu.bme.mit.theta.core.type.booltype.BoolExprs.False; +import static hu.bme.mit.theta.core.type.inttype.IntExprs.Int; + +public class StmtSimplifier { + + public static Stmt simplifyStmt(final Valuation valuation, final Stmt stmt) { + MutableValuation mutableValuation = MutableValuation.copyOf(valuation); + final var result = stmt.accept(new StmtSimplifierVisitor(),mutableValuation); + return result.stmt; + } + + private enum SimplifyStatus { + SUCCESS, BOTTOM + } + + private static class SimplifyResult{ + + private final Stmt stmt; + private final SimplifyStatus status; + + public static SimplifyResult of(final Stmt stmt, final SimplifyStatus status){ + return new SimplifyResult(stmt,status); + } + + private SimplifyResult(final Stmt stmt, final SimplifyStatus status) { + this.stmt = stmt; + this.status = status; + } + } + + private static class StmtSimplifierVisitor implements StmtVisitor { + + @Override + public SimplifyResult visit(final SkipStmt stmt, final MutableValuation valuation) { + return SimplifyResult.of(SkipStmt.getInstance(), SimplifyStatus.SUCCESS); + } + + @Override + public SimplifyResult visit(final AssumeStmt stmt, final MutableValuation valuation) { + final Expr simplifiedExpr = ExprUtils.simplify(stmt.getCond(),valuation); + final Stmt simplifiedStmt = AssumeStmt.of(simplifiedExpr); + if (simplifiedExpr instanceof BoolLitExpr) { + final BoolLitExpr condLit = (BoolLitExpr) simplifiedExpr; + if (!condLit.getValue()) { + return SimplifyResult.of(simplifiedStmt, SimplifyStatus.BOTTOM); + } + } + return SimplifyResult.of(simplifiedStmt,SimplifyStatus.SUCCESS); + } + + @Override + public SimplifyResult visit(final AssignStmt stmt, final MutableValuation valuation) { + final VarDecl varDecl = stmt.getVarDecl(); + final Expr expr = ExprUtils.simplify(stmt.getExpr(), valuation); + if (expr instanceof LitExpr) { + final LitExpr lit = (LitExpr) expr; + valuation.put(varDecl, lit); + } else { + valuation.remove(varDecl); + } + return SimplifyResult.of(AssignStmt.of(varDecl,expr),SimplifyStatus.SUCCESS); + } + + @Override + public SimplifyResult visit(final HavocStmt stmt, final MutableValuation valuation) { + final VarDecl varDecl = stmt.getVarDecl(); + valuation.remove(varDecl); + return SimplifyResult.of(stmt,SimplifyStatus.SUCCESS); + } + + @Override + public SimplifyResult visit(final SequenceStmt stmt, final MutableValuation valuation) { + final var subStmtsUnrolled = stmt.getStmts().stream() + .map(subStmt -> subStmt.accept(this,valuation)).collect(Collectors.toList()); + final var simplifiedStmt = SequenceStmt.of(subStmtsUnrolled.stream().map(result -> result.stmt) + .collect(Collectors.toList())); + final boolean anyBottom = subStmtsUnrolled.stream().anyMatch(result -> result.status==SimplifyStatus.BOTTOM); + if(anyBottom){ + return SimplifyResult.of(AssumeStmt.of(False()),SimplifyStatus.BOTTOM); + } else { + return SimplifyResult.of(simplifiedStmt,SimplifyStatus.SUCCESS); + } + } + + @Override + public SimplifyResult visit(final NonDetStmt stmt, final MutableValuation valuation) { + final List valuations = new ArrayList<>(); + final List successfulSubStmts = new ArrayList<>(); + for (int i = 0; i < stmt.getStmts().size(); i++) { + final MutableValuation subVal = MutableValuation.copyOf(valuation); + final SimplifyResult result = stmt.getStmts().get(i).accept(this,subVal); + if(result.status==SimplifyStatus.SUCCESS){ + valuations.add(subVal); + successfulSubStmts.add(result.stmt); + } + + } + if(successfulSubStmts.size()==0){ + return SimplifyResult.of(AssumeStmt.of(False()),SimplifyStatus.BOTTOM); + } else if(successfulSubStmts.size()==1){ + successfulSubStmts.get(0).accept(this,valuation); + return SimplifyResult.of(successfulSubStmts.get(0),SimplifyStatus.SUCCESS); + } else { + successfulSubStmts.get(0).accept(this,valuation); + List> toRemove = new ArrayList<>(); + for (Decl decl : valuation.getDecls()) { + for (MutableValuation subVal : valuations) { + if (!valuation.eval(decl).equals(subVal.eval(decl))) { + toRemove.add(decl); + break; + } + } + } + for (Decl decl : toRemove) valuation.remove(decl); + return SimplifyResult.of(NonDetStmt.of(successfulSubStmts),SimplifyStatus.SUCCESS); + } + + } + + @Override + public SimplifyResult visit(final OrtStmt stmt, final MutableValuation valuation) { + throw new UnsupportedOperationException(); + } + + @Override + public SimplifyResult visit(final LoopStmt stmt, final MutableValuation valuation) { + var from = stmt.getFrom(); + var to = stmt.getTo(); + var fromUnrolled = ExprUtils.simplify(from,valuation); + var toUnrolled = ExprUtils.simplify(to,valuation); + if(fromUnrolled instanceof IntLitExpr && toUnrolled instanceof IntLitExpr){ + var fromValue = ((IntLitExpr) fromUnrolled).getValue(); + var toValue = ((IntLitExpr) toUnrolled).getValue(); + var stmts = new ArrayList(); + for (BigInteger bi = fromValue; bi.compareTo(toValue) < 0; bi = bi.add(BigInteger.ONE)) { + var assignToLoopVar = AssignStmt.of(stmt.getLoopVariable(),Int(bi)); + var loopVarIncAndSubStmt = SequenceStmt.of(ImmutableList.of(assignToLoopVar,stmt.getStmt())); + var result = loopVarIncAndSubStmt.accept(this,valuation); + if(result.status==SimplifyStatus.SUCCESS){ + stmts.add(result.stmt); + } else { + return SimplifyResult.of(AssumeStmt.of(False()),SimplifyStatus.BOTTOM); + } + + } + return SimplifyResult.of(SequenceStmt.of(stmts),SimplifyStatus.SUCCESS); + } + throw new IllegalArgumentException(String.format("Couldn't unroll loop statement %s", stmt)); + } + } + +} diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/utils/ArgVisualizer.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/utils/ArgVisualizer.java index 037e97d70d..868d1d06b8 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/utils/ArgVisualizer.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/utils/ArgVisualizer.java @@ -19,7 +19,7 @@ import static hu.bme.mit.theta.common.visualization.Shape.RECTANGLE; import java.awt.Color; -import java.util.HashSet; +import hu.bme.mit.theta.common.container.Containers; import java.util.Set; import java.util.function.Function; import java.util.stream.Collectors; @@ -78,7 +78,7 @@ public static ArgVisualizer getStructureOnly() { public Graph visualize(final ARG arg) { final Graph graph = new Graph(ARG_ID, ARG_LABEL); - final Set> traversed = new HashSet<>(); + final Set> traversed = Containers.createSet(); for (final ArgNode initNode : arg.getInitNodes().collect(Collectors.toSet())) { traverse(graph, initNode, traversed); diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/utils/TraceVisualizer.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/utils/TraceVisualizer.java index 8673b242e6..94cd3095eb 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/utils/TraceVisualizer.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/utils/TraceVisualizer.java @@ -17,13 +17,13 @@ import java.awt.Color; import java.util.Collection; -import java.util.HashMap; import java.util.Map; import java.util.function.Function; 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.common.container.Containers; import hu.bme.mit.theta.common.visualization.EdgeAttributes; import hu.bme.mit.theta.common.visualization.Graph; import hu.bme.mit.theta.common.visualization.LineStyle; @@ -76,7 +76,7 @@ public Graph visualize(final Trace trace) { public Graph visualizeMerged(final Collection> traces) { final Graph graph = new Graph(TRACE_ID, TRACE_LABEL); - final Map stateIds = new HashMap<>(); + final Map stateIds = Containers.createMap(); for (final Trace trace : traces) { for (final S state : trace.getStates()) { diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/BoundFunc.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/BoundFunc.java index d8380eda93..45765cda73 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/BoundFunc.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/BoundFunc.java @@ -21,7 +21,7 @@ import java.util.Collection; import java.util.Collections; -import java.util.HashMap; +import hu.bme.mit.theta.common.container.Containers; import java.util.Map; import java.util.Optional; @@ -59,8 +59,8 @@ private BoundFunc(final Map, Integer> varToLower, public BoundFunc merge(final BoundFunc that) { checkNotNull(that); - final Map, Integer> varToLower = new HashMap<>(this.varToLower); - final Map, Integer> varToUpper = new HashMap<>(this.varToUpper); + final Map, Integer> varToLower = Containers.createMap(this.varToLower); + final Map, Integer> varToUpper = Containers.createMap(this.varToUpper); that.varToLower.forEach((c, b) -> varToLower.merge(c, b, Integer::max)); that.varToUpper.forEach((c, b) -> varToUpper.merge(c, b, Integer::max)); @@ -160,14 +160,14 @@ public static final class Builder { private Builder() { this.boundFunction = null; - this.varToLower = new HashMap<>(); - this.varToUpper = new HashMap<>(); + this.varToLower = Containers.createMap(); + this.varToUpper = Containers.createMap(); } private Builder(final BoundFunc boundFunction) { this.boundFunction = null; - this.varToLower = new HashMap<>(boundFunction.varToLower); - this.varToUpper = new HashMap<>(boundFunction.varToUpper); + this.varToLower = Containers.createMap(boundFunction.varToLower); + this.varToUpper = Containers.createMap(boundFunction.varToUpper); } public Builder remove(final VarDecl varDecl) { diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/DBM.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/DBM.java index 23688c6827..fe6c8ddfce 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/DBM.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/DBM.java @@ -30,7 +30,7 @@ import java.util.Arrays; import java.util.Collection; import java.util.Collections; -import java.util.HashSet; +import hu.bme.mit.theta.common.container.Containers; import java.util.Map; import java.util.Set; import java.util.function.BiFunction; @@ -478,7 +478,7 @@ private static final int LtMinusLy(final VarDecl y, final BoundFunc bou } public Collection getConstrs() { - final Collection result = new HashSet<>(); + final Collection result = Containers.createSet(); for (final VarDecl leftVar : signature) { for (final VarDecl rightVar : signature) { diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/DbmSignature.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/DbmSignature.java index be5b976926..43d7a4f77f 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/DbmSignature.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/DbmSignature.java @@ -19,7 +19,7 @@ import static com.google.common.base.Preconditions.checkElementIndex; import static com.google.common.base.Preconditions.checkNotNull; -import java.util.HashSet; +import hu.bme.mit.theta.common.container.Containers; import java.util.Iterator; import java.util.List; import java.util.Map; @@ -44,7 +44,7 @@ private DbmSignature(final Iterable> varDecls) { final ImmutableList.Builder> indexToVarBuilder = ImmutableList.builder(); final ImmutableMap.Builder, Integer> varToIndexBuilder = ImmutableMap.builder(); - final Set> addedVars = new HashSet<>(); + final Set> addedVars = Containers.createSet(); indexToVarBuilder.add(ZeroVar.getInstance()); varToIndexBuilder.put(ZeroVar.getInstance(), addedVars.size()); diff --git a/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/expl/ExplStmtTransFuncTest.java b/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/expl/ExplStmtTransFuncTest.java index 8665228e2d..575e3f387d 100644 --- a/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/expl/ExplStmtTransFuncTest.java +++ b/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/expl/ExplStmtTransFuncTest.java @@ -29,7 +29,7 @@ import java.util.ArrayList; import java.util.Collection; import java.util.Collections; -import java.util.HashMap; +import hu.bme.mit.theta.common.container.Containers; import java.util.List; import java.util.Map; import java.util.Map.Entry; @@ -129,7 +129,7 @@ public void testComplex3() { final List stmts = new ArrayList<>(); stmts.add(Assume(BoolExprs.And(Leq(Int(0), x.getRef()), Leq(x.getRef(), Int(2))))); - final Map solverCallsToExpectedStates = new HashMap<>(); + final Map solverCallsToExpectedStates = Containers.createMap(); solverCallsToExpectedStates.put(1, 1); solverCallsToExpectedStates.put(2, 1); solverCallsToExpectedStates.put(3, 3); diff --git a/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/expl/StmtApplierTest.java b/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/expl/StmtApplierTest.java index de9864e485..db9cd05826 100644 --- a/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/expl/StmtApplierTest.java +++ b/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/expl/StmtApplierTest.java @@ -34,6 +34,7 @@ import java.util.Collection; import java.util.Set; +import hu.bme.mit.theta.analysis.expl.StmtApplier; import org.junit.Test; import org.junit.runner.RunWith; import org.junit.runners.Parameterized; diff --git a/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/utils/StmtSimplifierTest.java b/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/utils/StmtSimplifierTest.java new file mode 100644 index 0000000000..8cac163c03 --- /dev/null +++ b/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/utils/StmtSimplifierTest.java @@ -0,0 +1,160 @@ +package hu.bme.mit.theta.analysis.utils; + +import static com.google.common.collect.ImmutableSet.of; +import static hu.bme.mit.theta.core.decl.Decls.Var; +import static hu.bme.mit.theta.core.stmt.Stmts.*; +import static hu.bme.mit.theta.core.type.booltype.BoolExprs.False; +import static hu.bme.mit.theta.core.type.booltype.BoolExprs.True; +import static hu.bme.mit.theta.core.type.inttype.IntExprs.Gt; +import static hu.bme.mit.theta.core.type.inttype.IntExprs.Int; +import static hu.bme.mit.theta.core.type.inttype.IntExprs.Leq; +import static hu.bme.mit.theta.core.type.inttype.IntExprs.Eq; +import static org.junit.Assert.assertEquals; + +import java.util.Arrays; +import java.util.Collection; +import java.util.Set; + +import com.google.common.collect.ImmutableList; +import hu.bme.mit.theta.analysis.stmtoptimizer.StmtSimplifier; +import hu.bme.mit.theta.core.stmt.NonDetStmt; +import hu.bme.mit.theta.core.stmt.SequenceStmt; +import org.junit.Test; +import org.junit.runner.RunWith; +import org.junit.runners.Parameterized; +import org.junit.runners.Parameterized.Parameter; +import org.junit.runners.Parameterized.Parameters; + +import hu.bme.mit.theta.common.Tuple2; +import hu.bme.mit.theta.core.decl.Decl; +import hu.bme.mit.theta.core.decl.VarDecl; +import hu.bme.mit.theta.core.model.MutableValuation; +import hu.bme.mit.theta.core.stmt.Stmt; +import hu.bme.mit.theta.core.type.LitExpr; +import hu.bme.mit.theta.core.type.inttype.IntType; + +@RunWith(Parameterized.class) +public final class StmtSimplifierTest { + + private static final VarDecl X = Var("x", Int()); + private static final VarDecl Y = Var("y", Int()); + + private static final Tuple2, LitExpr> X_IS_1 = Tuple2.of(X, Int(1)); + private static final Tuple2, LitExpr> Y_IS_2 = Tuple2.of(Y, Int(2)); + + private static final Stmt SKIP = Skip(); + private static final Stmt HAVOC_X = Havoc(X); + private static final Stmt ASSUME_GT_X_0 = Assume(Gt(X.getRef(), Int(0))); + private static final Stmt ASSUME_LEQ_X_0 = Assume(Leq(X.getRef(), Int(0))); + private static final Stmt ASSUME_EQ_X_1 = Assume(Eq(X.getRef(), Int(1))); + private static final Stmt ASSUME_LEQ_X_2 = Assume(Leq(X.getRef(), Int(2))); + private static final Stmt ASSUME_LEQ_X_Y = Assume(Leq(X.getRef(), Y.getRef())); + private static final Stmt ASSUME_LEQ_1_Y = Assume(Leq(Int(1), Y.getRef())); + private static final Stmt ASSUME_TRUE = Assume(True()); + private static final Stmt ASSUME_FALSE = Assume(False()); + private static final Stmt ASSIGN_X_1 = Assign(X, Int(1)); + private static final Stmt ASSIGN_X_2 = Assign(X, Int(2)); + private static final Stmt ASSIGN_X_Y = Assign(X, Y.getRef()); + private static final Stmt SEQ_ASSIGN_X_1_ASSUME_EQ_X_1 = SequenceStmt.of(ImmutableList.of(ASSIGN_X_1,ASSUME_EQ_X_1)); + private static final Stmt SEQ_ASSIGN_X_1_ASSUME_LEQ_X_0 = SequenceStmt.of(ImmutableList.of(ASSIGN_X_1,ASSUME_LEQ_X_0)); + private static final Stmt SEQ_ASSIGN_X_1_ASSUME_TRUE = SequenceStmt.of(ImmutableList.of(ASSIGN_X_1,ASSUME_TRUE)); + private static final Stmt NONDET_SEQ_ASSIGN_X_1_ASSUME_EQ_X_1_OR_SEQ_ASSIGN_X_1_ASSUME_LEQ_X_0 = NonDetStmt.of(ImmutableList.of(SEQ_ASSIGN_X_1_ASSUME_EQ_X_1,SEQ_ASSIGN_X_1_ASSUME_LEQ_X_0)); + private static final Stmt NONDET_SEQ_ASSIGN_X_1_ASSUME_TRUE_OR_SEQ_ASSIGN_X_1_ASSUME_TRUE = NonDetStmt.of(ImmutableList.of(SEQ_ASSIGN_X_1_ASSUME_TRUE,SEQ_ASSIGN_X_1_ASSUME_TRUE)); + private static final Stmt NONDET_SEQ_ASSIGN_X_1_ASSUME_EQ_X_1_OR_SEQ_ASSIGN_X_1_ASSUME_LEQ_X_0_OR_SEQ_ASSIGN_X_1_ASSUME_EQ_X_1 = NonDetStmt.of(ImmutableList.of(SEQ_ASSIGN_X_1_ASSUME_EQ_X_1,SEQ_ASSIGN_X_1_ASSUME_LEQ_X_0,SEQ_ASSIGN_X_1_ASSUME_EQ_X_1)); + + @Parameter(0) + public Stmt stmt; + + @Parameter(1) + public Set, LitExpr>> initialEntries; + + @Parameter(2) + public Stmt expectedStmt; + + @Parameters + public static Collection data() { + return Arrays.asList(new Object[][]{ + + {HAVOC_X, of(X_IS_1), HAVOC_X}, + + {HAVOC_X, of(Y_IS_2), HAVOC_X}, + + {HAVOC_X, of(X_IS_1, Y_IS_2), HAVOC_X}, + + {HAVOC_X, of(), HAVOC_X}, + + {ASSUME_GT_X_0, of(X_IS_1), ASSUME_TRUE}, + + {ASSUME_GT_X_0, of(Y_IS_2), ASSUME_GT_X_0}, + + {ASSUME_GT_X_0, of(X_IS_1, Y_IS_2), ASSUME_TRUE}, + + {ASSUME_GT_X_0, of(), ASSUME_GT_X_0}, + + {ASSUME_LEQ_X_0, of(X_IS_1), ASSUME_FALSE}, + + {ASSUME_LEQ_X_0, of(Y_IS_2), ASSUME_LEQ_X_0}, + + {ASSUME_LEQ_X_0, of(X_IS_1, Y_IS_2), ASSUME_FALSE}, + + {ASSUME_LEQ_X_Y, of(X_IS_1), ASSUME_LEQ_1_Y}, + + {ASSUME_LEQ_X_Y, of(Y_IS_2), ASSUME_LEQ_X_2}, + + {ASSUME_LEQ_X_Y, of(X_IS_1, Y_IS_2), ASSUME_TRUE}, + + {ASSUME_LEQ_X_Y, of(), ASSUME_LEQ_X_Y}, + + {ASSIGN_X_1, of(), ASSIGN_X_1}, + + {ASSIGN_X_1, of(Y_IS_2), ASSIGN_X_1}, + + {ASSIGN_X_1, of(X_IS_1, Y_IS_2), ASSIGN_X_1}, + + {ASSIGN_X_2, of(), ASSIGN_X_2}, + + {ASSIGN_X_2, of(X_IS_1), ASSIGN_X_2}, + + {ASSIGN_X_Y, of(), ASSIGN_X_Y}, + + {ASSIGN_X_Y, of(X_IS_1), ASSIGN_X_Y}, + + {ASSIGN_X_Y, of(X_IS_1), ASSIGN_X_Y}, + + {ASSIGN_X_Y, of(X_IS_1, Y_IS_2), ASSIGN_X_2}, + + {ASSIGN_X_Y, of(Y_IS_2), ASSIGN_X_2}, + + {SKIP, of(X_IS_1), SKIP}, + + {ASSUME_EQ_X_1, of(), ASSUME_EQ_X_1}, + + {SEQ_ASSIGN_X_1_ASSUME_EQ_X_1, of(), SEQ_ASSIGN_X_1_ASSUME_TRUE}, + + {SEQ_ASSIGN_X_1_ASSUME_LEQ_X_0, of(), ASSUME_FALSE}, + + {NONDET_SEQ_ASSIGN_X_1_ASSUME_EQ_X_1_OR_SEQ_ASSIGN_X_1_ASSUME_LEQ_X_0, of(), SEQ_ASSIGN_X_1_ASSUME_TRUE}, + + {NONDET_SEQ_ASSIGN_X_1_ASSUME_EQ_X_1_OR_SEQ_ASSIGN_X_1_ASSUME_LEQ_X_0_OR_SEQ_ASSIGN_X_1_ASSUME_EQ_X_1, of(), NONDET_SEQ_ASSIGN_X_1_ASSUME_TRUE_OR_SEQ_ASSIGN_X_1_ASSUME_TRUE}, + + {NONDET_SEQ_ASSIGN_X_1_ASSUME_TRUE_OR_SEQ_ASSIGN_X_1_ASSUME_TRUE, of(), NONDET_SEQ_ASSIGN_X_1_ASSUME_TRUE_OR_SEQ_ASSIGN_X_1_ASSUME_TRUE} + + }); + } + + @Test + public void test() { + // Arrange + final MutableValuation val = new MutableValuation(); + for (final Tuple2, LitExpr> entry : initialEntries) { + val.put(entry.get1(), entry.get2()); + } + + // Act + final Stmt actualStmt = StmtSimplifier.simplifyStmt(val, stmt); + + // Assert + assertEquals(expectedStmt, actualStmt); + } + +} diff --git a/subprojects/common/common/src/main/java/hu/bme/mit/theta/common/DispatchTable.java b/subprojects/common/common/src/main/java/hu/bme/mit/theta/common/DispatchTable.java index 0ad0039e5f..8ecdbc6399 100644 --- a/subprojects/common/common/src/main/java/hu/bme/mit/theta/common/DispatchTable.java +++ b/subprojects/common/common/src/main/java/hu/bme/mit/theta/common/DispatchTable.java @@ -18,7 +18,7 @@ import static com.google.common.base.Preconditions.checkNotNull; import static com.google.common.base.Preconditions.checkState; -import java.util.HashMap; +import hu.bme.mit.theta.common.container.Containers; import java.util.Map; import java.util.function.Function; @@ -54,7 +54,7 @@ public static final class Builder { private boolean built; private Builder() { - cases = new HashMap<>(); + cases = Containers.createMap(); defaultCase = null; built = false; } diff --git a/subprojects/common/common/src/main/java/hu/bme/mit/theta/common/DispatchTable2.java b/subprojects/common/common/src/main/java/hu/bme/mit/theta/common/DispatchTable2.java index f8b79ac746..a5828e958d 100644 --- a/subprojects/common/common/src/main/java/hu/bme/mit/theta/common/DispatchTable2.java +++ b/subprojects/common/common/src/main/java/hu/bme/mit/theta/common/DispatchTable2.java @@ -15,10 +15,11 @@ */ package hu.bme.mit.theta.common; +import hu.bme.mit.theta.common.container.Containers; + import static com.google.common.base.Preconditions.checkNotNull; import static com.google.common.base.Preconditions.checkState; -import java.util.HashMap; import java.util.Map; import java.util.function.BiFunction; @@ -55,7 +56,7 @@ public static final class Builder { private boolean built; private Builder() { - cases = new HashMap<>(); + cases = Containers.createMap(); defaultCase = null; built = false; } diff --git a/subprojects/common/common/src/main/java/hu/bme/mit/theta/common/container/Containers.java b/subprojects/common/common/src/main/java/hu/bme/mit/theta/common/container/Containers.java new file mode 100644 index 0000000000..59eb67d990 --- /dev/null +++ b/subprojects/common/common/src/main/java/hu/bme/mit/theta/common/container/Containers.java @@ -0,0 +1,53 @@ +package hu.bme.mit.theta.common.container; + +import hu.bme.mit.theta.common.container.factory.ContainerFactory; +import hu.bme.mit.theta.common.container.factory.LinkedHashContainerFactory; + +import java.util.Collection; +import java.util.Map; +import java.util.Set; + +import static com.google.common.base.Preconditions.checkNotNull; + +public class Containers { + + private static ContainerFactory containerFactory = new LinkedHashContainerFactory(); + + public static void setContainerFactory(final ContainerFactory containerFactory){ + checkNotNull(containerFactory); + Containers.containerFactory = containerFactory; + } + + public static Map createMap(){ + return containerFactory.createMap(); + } + + public static Map createMap(int initialCapacity){ + return containerFactory.createMap(initialCapacity); + } + + public static Map createMap(int initialCapacity, float loadFactor){ + return containerFactory.createMap(initialCapacity,loadFactor); + } + + public static Map createMap(Map m){ + return containerFactory.createMap(m); + } + + public static Set createSet(){ + return containerFactory.createSet(); + } + + public static Set createSet(int initialCapacity){ + return containerFactory.createSet(initialCapacity); + } + + public static Set createSet(int initialCapacity, float loadFactor){ + return containerFactory.createSet(initialCapacity,loadFactor); + } + + public static Set createSet(Collection c){ + return containerFactory.createSet(c); + } + +} diff --git a/subprojects/common/common/src/main/java/hu/bme/mit/theta/common/container/factory/ContainerFactory.java b/subprojects/common/common/src/main/java/hu/bme/mit/theta/common/container/factory/ContainerFactory.java new file mode 100644 index 0000000000..eca31db162 --- /dev/null +++ b/subprojects/common/common/src/main/java/hu/bme/mit/theta/common/container/factory/ContainerFactory.java @@ -0,0 +1,25 @@ +package hu.bme.mit.theta.common.container.factory; + +import java.util.Collection; +import java.util.Map; +import java.util.Set; + +public interface ContainerFactory { + + Map createMap(); + + Map createMap(int initialCapacity); + + Map createMap(int initialCapacity, float loadFactor); + + Map createMap(Map m); + + Set createSet(); + + Set createSet(int initialCapacity); + + Set createSet(int initialCapacity, float loadFactor); + + Set createSet(Collection c); + +} diff --git a/subprojects/common/common/src/main/java/hu/bme/mit/theta/common/container/factory/HashContainerFactory.java b/subprojects/common/common/src/main/java/hu/bme/mit/theta/common/container/factory/HashContainerFactory.java new file mode 100644 index 0000000000..9cab88a2a4 --- /dev/null +++ b/subprojects/common/common/src/main/java/hu/bme/mit/theta/common/container/factory/HashContainerFactory.java @@ -0,0 +1,45 @@ +package hu.bme.mit.theta.common.container.factory; + +import java.util.*; + +public class HashContainerFactory implements ContainerFactory { + @Override + public Map createMap() { + return new HashMap(); + } + + @Override + public Map createMap(int initialCapacity) { + return new HashMap(initialCapacity); + } + + @Override + public Map createMap(int initialCapacity, float loadFactor) { + return new HashMap(initialCapacity,loadFactor); + } + + @Override + public Map createMap(Map m) { + return new HashMap(m); + } + + @Override + public Set createSet() { + return new HashSet(); + } + + @Override + public Set createSet(int initialCapacity) { + return new HashSet(initialCapacity); + } + + @Override + public Set createSet(int initialCapacity, float loadFactor) { + return new HashSet(initialCapacity,loadFactor); + } + + @Override + public Set createSet(Collection c) { + return new HashSet(c); + } +} diff --git a/subprojects/common/common/src/main/java/hu/bme/mit/theta/common/container/factory/LinkedHashContainerFactory.java b/subprojects/common/common/src/main/java/hu/bme/mit/theta/common/container/factory/LinkedHashContainerFactory.java new file mode 100644 index 0000000000..6f9ed42161 --- /dev/null +++ b/subprojects/common/common/src/main/java/hu/bme/mit/theta/common/container/factory/LinkedHashContainerFactory.java @@ -0,0 +1,45 @@ +package hu.bme.mit.theta.common.container.factory; + +import java.util.*; + +public class LinkedHashContainerFactory implements ContainerFactory{ + @Override + public Map createMap() { + return new LinkedHashMap(); + } + + @Override + public Map createMap(int initialCapacity) { + return new LinkedHashMap(initialCapacity); + } + + @Override + public Map createMap(int initialCapacity, float loadFactor) { + return new LinkedHashMap(initialCapacity,loadFactor); + } + + @Override + public Map createMap(Map m) { + return new LinkedHashMap(m); + } + + @Override + public Set createSet() { + return new LinkedHashSet(); + } + + @Override + public Set createSet(int initialCapacity) { + return new LinkedHashSet(initialCapacity); + } + + @Override + public Set createSet(int initialCapacity, float loadFactor) { + return new LinkedHashSet(initialCapacity,loadFactor); + } + + @Override + public Set createSet(Collection c) { + return new LinkedHashSet(c); + } +} diff --git a/subprojects/common/common/src/main/java/hu/bme/mit/theta/common/dsl/Env.java b/subprojects/common/common/src/main/java/hu/bme/mit/theta/common/dsl/Env.java index 11bccab3cb..ee5d1271c7 100644 --- a/subprojects/common/common/src/main/java/hu/bme/mit/theta/common/dsl/Env.java +++ b/subprojects/common/common/src/main/java/hu/bme/mit/theta/common/dsl/Env.java @@ -20,7 +20,7 @@ import static com.google.common.base.Preconditions.checkState; import static java.util.stream.Collectors.toList; -import java.util.HashMap; +import hu.bme.mit.theta.common.container.Containers; import java.util.Map; import java.util.function.Function; @@ -80,7 +80,7 @@ private static final class Frame { private Frame(final Frame parent) { this.parent = parent; - symbolToValue = new HashMap<>(); + symbolToValue = Containers.createMap(); } public void define(final Symbol symbol, final Object value) { diff --git a/subprojects/common/common/src/main/java/hu/bme/mit/theta/common/visualization/Graph.java b/subprojects/common/common/src/main/java/hu/bme/mit/theta/common/visualization/Graph.java index e0628b4c73..26271f9d06 100644 --- a/subprojects/common/common/src/main/java/hu/bme/mit/theta/common/visualization/Graph.java +++ b/subprojects/common/common/src/main/java/hu/bme/mit/theta/common/visualization/Graph.java @@ -21,7 +21,7 @@ import java.util.ArrayList; import java.util.Collection; import java.util.Collections; -import java.util.HashMap; +import hu.bme.mit.theta.common.container.Containers; import java.util.Map; import java.util.stream.Stream; @@ -44,7 +44,7 @@ public final class Graph { public Graph(final String id, final String label) { this.id = checkNotNull(id); this.label = checkNotNull(label); - this.nodes = new HashMap<>(); + this.nodes = Containers.createMap(); this.edges = new ArrayList<>(); } diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/op/ClockOps.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/op/ClockOps.java index 5acf153384..6cfcfbe4c0 100644 --- a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/op/ClockOps.java +++ b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/op/ClockOps.java @@ -21,15 +21,7 @@ import hu.bme.mit.theta.core.clock.constr.ClockConstrs; import hu.bme.mit.theta.core.decl.Decl; import hu.bme.mit.theta.core.decl.VarDecl; -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.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.stmt.*; import hu.bme.mit.theta.core.type.Expr; import hu.bme.mit.theta.core.type.Type; import hu.bme.mit.theta.core.type.abstracttype.AddExpr; @@ -110,6 +102,9 @@ public ClockOp visit(NonDetStmt stmt, Void param) { @Override public ClockOp visit(OrtStmt stmt, Void param) { throw new UnsupportedOperationException(); } + @Override + public ClockOp visit(LoopStmt stmt, Void param) { throw new UnsupportedOperationException(); } + @Override public ClockOp visit(final AssignStmt stmt, final Void param) { diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/decl/VarDecl.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/decl/VarDecl.java index 04b17e1094..77b0ac617d 100644 --- a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/decl/VarDecl.java +++ b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/decl/VarDecl.java @@ -17,7 +17,7 @@ import static com.google.common.base.Preconditions.checkArgument; -import java.util.HashMap; +import hu.bme.mit.theta.common.container.Containers; import java.util.Map; import hu.bme.mit.theta.common.Utils; @@ -36,7 +36,7 @@ public final class VarDecl extends Decl { VarDecl(final String name, final DeclType type) { super(name, type); - indexToConst = new HashMap<>(); + indexToConst = Containers.createMap(); } public IndexedConstDecl getConstDecl(final int index) { diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/dsl/ParamBinding.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/dsl/ParamBinding.java index a735f058a8..5bcf16a823 100644 --- a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/dsl/ParamBinding.java +++ b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/dsl/ParamBinding.java @@ -19,7 +19,7 @@ import static com.google.common.base.Preconditions.checkNotNull; import java.util.Collection; -import java.util.HashMap; +import hu.bme.mit.theta.common.container.Containers; import java.util.List; import java.util.Map; import java.util.Optional; @@ -43,7 +43,7 @@ public ParamBinding(final List> params, final List(); + this.paramToArg = Containers.createMap(); for (int i = 0; i < params.size(); i++) { final ParamDecl param = params.get(i); diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/dsl/impl/StmtWriter.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/dsl/impl/StmtWriter.java index eff6925de8..858a3ed677 100644 --- a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/dsl/impl/StmtWriter.java +++ b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/dsl/impl/StmtWriter.java @@ -15,14 +15,7 @@ */ package hu.bme.mit.theta.core.dsl.impl; -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.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.StmtVisitor; +import hu.bme.mit.theta.core.stmt.*; import hu.bme.mit.theta.core.type.Expr; import hu.bme.mit.theta.core.type.Type; @@ -65,4 +58,7 @@ public String visit(NonDetStmt stmt, Void param) { @Override public String visit(OrtStmt stmt, Void param) { throw new UnsupportedOperationException(); } + @Override + public String visit(LoopStmt stmt, Void param) { throw new UnsupportedOperationException(); } + } diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/model/BasicSubstitution.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/model/BasicSubstitution.java index 2eca1622e2..079c97151d 100644 --- a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/model/BasicSubstitution.java +++ b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/model/BasicSubstitution.java @@ -21,7 +21,7 @@ import java.util.Collection; import java.util.Collections; -import java.util.HashMap; +import hu.bme.mit.theta.common.container.Containers; import java.util.LinkedHashMap; import java.util.Map; import java.util.Optional; @@ -100,7 +100,7 @@ public static final class Builder { private boolean built; private Builder() { - this(new HashMap<>()); + this(Containers.createMap()); } private Builder(final Map, Expr> declToExpr) { diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/model/NestedSubstitution.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/model/NestedSubstitution.java index 16bc5d90ee..9ba07256c5 100644 --- a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/model/NestedSubstitution.java +++ b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/model/NestedSubstitution.java @@ -18,7 +18,7 @@ import static com.google.common.base.Preconditions.checkNotNull; import java.util.Collection; -import java.util.HashSet; +import hu.bme.mit.theta.common.container.Containers; import java.util.Optional; import java.util.Set; @@ -47,7 +47,7 @@ public static NestedSubstitution create(final Substitution enclosingSubst, final @Override public Collection> getDecls() { - final Set> decls = new HashSet<>(); + final Set> decls = Containers.createSet(); decls.addAll(subst.getDecls()); decls.addAll(enclosingSubst.getDecls()); return decls; diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/parser/Env.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/parser/Env.java index 227253fde0..f187b1daef 100644 --- a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/parser/Env.java +++ b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/parser/Env.java @@ -19,7 +19,7 @@ import static com.google.common.base.Preconditions.checkNotNull; import static com.google.common.base.Preconditions.checkState; -import java.util.HashMap; +import hu.bme.mit.theta.common.container.Containers; import java.util.Map; import java.util.function.Function; @@ -78,7 +78,7 @@ private static final class Frame { private Frame(final Frame parent) { this.parent = parent; - symbolToValue = new HashMap<>(); + symbolToValue = Containers.createMap(); } public void define(final String symbol, final Object value) { diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/stmt/LoopStmt.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/stmt/LoopStmt.java new file mode 100644 index 0000000000..d4ade6d1f1 --- /dev/null +++ b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/stmt/LoopStmt.java @@ -0,0 +1,83 @@ +package hu.bme.mit.theta.core.stmt; + +import hu.bme.mit.theta.common.Utils; +import hu.bme.mit.theta.core.decl.VarDecl; +import hu.bme.mit.theta.core.type.Expr; +import hu.bme.mit.theta.core.type.inttype.IntType; + +public final class LoopStmt implements Stmt { + + private final Stmt stmt; + private final VarDecl loopVariable; + private final Expr from; + private final Expr to; + + private static final int HASH_SEED = 361; + private static final String STMT_LABEL = "loop"; + + private volatile int hashCode = 0; + + private LoopStmt(final Stmt stmt, final VarDecl loopVariable, final Expr from, final Expr to) { + this.stmt = stmt; + this.loopVariable = loopVariable; + this.from = from; + this.to = to; + } + + public static LoopStmt of(final Stmt stmt, final VarDecl loopVariable, final Expr from, final Expr to) { + return new LoopStmt(stmt, loopVariable, from, to); + } + + public Stmt getStmt() { + return stmt; + } + + public VarDecl getLoopVariable() { + return loopVariable; + } + + public Expr getFrom() { + return from; + } + + public Expr getTo() { + return to; + } + + @Override + public R accept(final StmtVisitor visitor, final P param) { + return visitor.visit(this, param); + } + + @Override + public int hashCode() { + int result = hashCode; + if (result == 0) { + result = HASH_SEED; + result = 37 * result + stmt.hashCode() + loopVariable.hashCode() + from.hashCode() + to.hashCode(); + hashCode = result; + } + return result; + } + + @Override + public boolean equals(final Object obj) { + if (this == obj) { + return true; + } else if (obj instanceof LoopStmt) { + final LoopStmt that = (LoopStmt) obj; + return this.getStmt().equals(that.getStmt()) + && this.loopVariable.equals(that.loopVariable) + && this.from.equals(that.from) + && this.to.equals(that.to); + } else { + return false; + } + } + + @Override + public String toString() { + return Utils.lispStringBuilder(STMT_LABEL).add(loopVariable+" from "+from+" to "+to+" "+stmt).toString(); + } + +} diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/stmt/StmtVisitor.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/stmt/StmtVisitor.java index 8fa0bf5418..bc9808fd68 100644 --- a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/stmt/StmtVisitor.java +++ b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/stmt/StmtVisitor.java @@ -33,4 +33,6 @@ public interface StmtVisitor { R visit(OrtStmt stmt, P param); + R visit(LoopStmt stmt, P param); + } diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/ExprCnfTransformer.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/ExprCnfTransformer.java index 25750c63e9..33c871d734 100644 --- a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/ExprCnfTransformer.java +++ b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/ExprCnfTransformer.java @@ -22,7 +22,7 @@ import java.util.ArrayList; import java.util.Collection; -import java.util.HashMap; +import hu.bme.mit.theta.common.container.Containers; import java.util.Map; import hu.bme.mit.theta.core.decl.Decls; @@ -57,7 +57,7 @@ private static final class CnfTransformationHelper { private CnfTransformationHelper() { nextCnfVarId = 0; - representatives = new HashMap<>(); + representatives = Containers.createMap(); } public Expr transform(final Expr expr, final Collection> encoding) { diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/ExprUtils.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/ExprUtils.java index 776e27eef9..e42d208762 100644 --- a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/ExprUtils.java +++ b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/ExprUtils.java @@ -20,7 +20,7 @@ import java.util.ArrayList; import java.util.Collection; import java.util.Collections; -import java.util.HashSet; +import hu.bme.mit.theta.common.container.Containers; import java.util.List; import java.util.Map; import java.util.Set; @@ -64,7 +64,7 @@ public static void collectAtoms(final Expr expr, final Collection> getAtoms(final Expr expr) { - final Set> atoms = new HashSet<>(); + final Set> atoms = Containers.createSet(); collectAtoms(expr, atoms); return atoms; } @@ -143,7 +143,7 @@ public static void collectVars(final Iterable> exprs, final Co * @return Set of variables appearing in the expression */ public static Set> getVars(final Expr expr) { - final Set> vars = new HashSet<>(); + final Set> vars = Containers.createSet(); collectVars(expr, vars); return vars; } @@ -155,7 +155,7 @@ public static Set> getVars(final Expr expr) { * @return Set of variables appearing in the expressions */ public static Set> getVars(final Iterable> exprs) { - final Set> vars = new HashSet<>(); + final Set> vars = Containers.createSet(); collectVars(exprs, vars); return vars; } diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/IndexedVars.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/IndexedVars.java index 64c028e7a1..f7119f5809 100644 --- a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/IndexedVars.java +++ b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/IndexedVars.java @@ -19,8 +19,8 @@ import java.util.Collection; import java.util.Collections; -import java.util.HashMap; -import java.util.HashSet; +import hu.bme.mit.theta.common.container.Containers; + import java.util.Map; import java.util.Map.Entry; import java.util.Set; @@ -105,14 +105,14 @@ public static final class Builder { private boolean built; private Builder() { - varSets = new HashMap<>(); + varSets = Containers.createMap(); built = false; } public void add(final int i, final VarDecl varDecl) { checkState(!built, "Already built."); if (!varSets.containsKey(i)) { - varSets.put(i, new HashSet<>()); + varSets.put(i, Containers.createSet()); } varSets.get(i).add(varDecl); } @@ -124,7 +124,7 @@ public void add(final int i, final Collection> varDecls) { } if (!varSets.containsKey(i)) { - varSets.put(i, new HashSet<>()); + varSets.put(i, Containers.createSet()); } varSets.get(i).addAll(varDecls); } diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/SpState.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/SpState.java index c85d400950..681d24498e 100644 --- a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/SpState.java +++ b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/SpState.java @@ -4,15 +4,7 @@ import hu.bme.mit.theta.core.decl.VarDecl; import hu.bme.mit.theta.core.model.BasicSubstitution; import hu.bme.mit.theta.core.model.Substitution; -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.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.stmt.*; 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; @@ -157,5 +149,10 @@ public SpState visit(NonDetStmt stmt, SpState param) { public SpState visit(OrtStmt stmt, SpState param) { throw new UnsupportedOperationException(); } + + @Override + public SpState visit(LoopStmt stmt, SpState param) { + throw new UnsupportedOperationException(); + } } } diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/StmtCounterVisitor.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/StmtCounterVisitor.java index 00b786ee9d..1dd78a05fb 100644 --- a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/StmtCounterVisitor.java +++ b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/StmtCounterVisitor.java @@ -54,6 +54,11 @@ public Integer visit(NonDetStmt stmt, Void param) { return count+1; } + @Override + public Integer visit(LoopStmt stmt, Void param) { + return stmt.accept(this,null)+1; + } + @Override public Integer visit(OrtStmt stmt, Void param) { int count = 0; diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/StmtToExprTransformer.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/StmtToExprTransformer.java index 84741e6225..fa83414981 100644 --- a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/StmtToExprTransformer.java +++ b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/StmtToExprTransformer.java @@ -20,23 +20,12 @@ import static hu.bme.mit.theta.core.type.booltype.BoolExprs.*; import static hu.bme.mit.theta.core.type.inttype.IntExprs.Int; -import java.util.ArrayList; -import java.util.Collection; -import java.util.List; -import java.util.Set; +import java.util.*; import com.google.common.collect.ImmutableList; import hu.bme.mit.theta.core.decl.VarDecl; -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.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.stmt.*; 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; @@ -150,6 +139,10 @@ public StmtUnfoldResult visit(NonDetStmt nonDetStmt, VarIndexing indexing) { public StmtUnfoldResult visit(OrtStmt ortStmt, VarIndexing indexing) { throw new UnsupportedOperationException(); } - } + @Override + public StmtUnfoldResult visit(LoopStmt stmt, VarIndexing indexing) { + throw new UnsupportedOperationException(String.format("Loop statement %s was not unrolled",stmt)); + } + } } diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/StmtUtils.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/StmtUtils.java index 0d957d5fa8..61e15b20e2 100644 --- a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/StmtUtils.java +++ b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/StmtUtils.java @@ -15,7 +15,7 @@ */ package hu.bme.mit.theta.core.utils; -import java.util.HashSet; +import hu.bme.mit.theta.common.container.Containers; import java.util.List; import java.util.Set; @@ -37,7 +37,7 @@ private StmtUtils() { * @return Variables */ public static Set> getVars(final Stmt stmt) { - final Set> vars = new HashSet<>(); + final Set> vars = Containers.createSet(); stmt.accept(VarCollectorStmtVisitor.getInstance(), vars); return vars; } @@ -49,7 +49,7 @@ public static Set> getVars(final Stmt stmt) { * @return Variables */ public static Set> getVars(final Iterable stmts) { - final Set> vars = new HashSet<>(); + final Set> vars = Containers.createSet(); stmts.forEach(s -> s.accept(VarCollectorStmtVisitor.getInstance(), vars)); return vars; } diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/VarCollectorStmtVisitor.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/VarCollectorStmtVisitor.java index 077a2d8845..1e62991635 100644 --- a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/VarCollectorStmtVisitor.java +++ b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/VarCollectorStmtVisitor.java @@ -82,4 +82,12 @@ public Void visit(OrtStmt stmt, Collection> vars) { return null; } + @Override + public Void visit(LoopStmt stmt, Collection> vars) { + ExprUtils.collectVars(stmt.getFrom(),vars); + ExprUtils.collectVars(stmt.getTo(),vars); + vars.add(stmt.getLoopVariable()); + return stmt.getStmt().accept(VarCollectorStmtVisitor.getInstance(),vars); + } + } diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/VarIndexing.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/VarIndexing.java index cd6ee87439..28f8ff2927 100644 --- a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/VarIndexing.java +++ b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/VarIndexing.java @@ -19,7 +19,7 @@ import static com.google.common.base.Preconditions.checkNotNull; import static java.lang.Math.max; -import java.util.HashMap; +import hu.bme.mit.theta.common.container.Containers; import java.util.Map; import java.util.Set; import java.util.StringJoiner; @@ -174,12 +174,12 @@ public static final class Builder { private Builder(final int defaultIndex) { checkArgument(defaultIndex >= 0, "Negative default index"); this.defaultIndex = defaultIndex; - varToOffset = new HashMap<>(); + varToOffset = Containers.createMap(); } private Builder(final VarIndexing indexing) { this.defaultIndex = indexing.defaultIndex; - this.varToOffset = new HashMap<>(indexing.varToOffset); + this.varToOffset = Containers.createMap(indexing.varToOffset); } public Builder inc(final VarDecl varDecl, final int n) { @@ -208,7 +208,7 @@ public Builder add(final Builder that) { checkNotNull(that); final int newDefaultIndex = this.defaultIndex + that.defaultIndex; - final Map, Integer> newVarToOffset = new HashMap<>(); + final Map, Integer> newVarToOffset = Containers.createMap(); final Set> varDecls = Sets.union(this.varToOffset.keySet(), that.varToOffset.keySet()); for (final VarDecl varDecl : varDecls) { @@ -232,7 +232,7 @@ public Builder sub(final Builder that) { final int newDefaultIndex = this.defaultIndex - that.defaultIndex; checkArgument(newDefaultIndex >= 0, "Negative default index"); - final Map, Integer> newVarToOffset = new HashMap<>(); + final Map, Integer> newVarToOffset = Containers.createMap(); final Set> varDecls = Sets.union(this.varToOffset.keySet(), that.varToOffset.keySet()); for (final VarDecl varDecl : varDecls) { @@ -255,7 +255,7 @@ public Builder join(final Builder that) { checkNotNull(that); final int newDefaultIndex = max(this.defaultIndex, that.defaultIndex); - final Map, Integer> newVarToOffset = new HashMap<>(); + final Map, Integer> newVarToOffset = Containers.createMap(); final Set> varDecls = Sets.union(this.varToOffset.keySet(), that.varToOffset.keySet()); for (final VarDecl varDecl : varDecls) { diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/WpState.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/WpState.java index 5d026737c6..17161ccf88 100644 --- a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/WpState.java +++ b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/WpState.java @@ -161,6 +161,9 @@ public WpState visit(NonDetStmt stmt, WpState param) { @Override public WpState visit(OrtStmt stmt, WpState param) { throw new UnsupportedOperationException(); } + @Override + public WpState visit(LoopStmt stmt, WpState param) { throw new UnsupportedOperationException(); } + @Override public WpState visit(final AssumeStmt stmt, final WpState state) { final Expr expr = Imply(stmt.getCond(), state.getExpr()); @@ -210,6 +213,9 @@ public WpState visit(NonDetStmt stmt, WpState param) { @Override public WpState visit(OrtStmt stmt, WpState param) { throw new UnsupportedOperationException(); } + @Override + public WpState visit(LoopStmt stmt, WpState param) { throw new UnsupportedOperationException(); } + @Override public WpState visit(final AssumeStmt stmt, final WpState state) { final Expr expr = And(stmt.getCond(), state.getExpr()); diff --git a/subprojects/common/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3ItpSolver.java b/subprojects/common/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3ItpSolver.java index 39e2ac77cd..7e392db51e 100644 --- a/subprojects/common/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3ItpSolver.java +++ b/subprojects/common/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3ItpSolver.java @@ -20,7 +20,7 @@ import static com.google.common.base.Preconditions.checkState; import java.util.Collection; -import java.util.HashMap; +import hu.bme.mit.theta.common.container.Containers; import java.util.LinkedList; import java.util.List; import java.util.Map; @@ -102,7 +102,7 @@ public Interpolant getInterpolant(final ItpPattern pattern) { itpList.add(itpExpr); } - final Map> itpMap = new HashMap<>(); + final Map> itpMap = Containers.createMap(); buildItpMapFormList(pattern, itpList, itpMap); return new Z3Interpolant(itpMap); diff --git a/subprojects/common/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3Solver.java b/subprojects/common/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3Solver.java index 5558b50665..6a58baccba 100644 --- a/subprojects/common/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3Solver.java +++ b/subprojects/common/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3Solver.java @@ -21,7 +21,7 @@ import java.util.ArrayList; import java.util.Collection; import java.util.Collections; -import java.util.HashMap; +import hu.bme.mit.theta.common.container.Containers; import java.util.LinkedList; import java.util.Map; import java.util.Optional; @@ -76,7 +76,7 @@ public Z3Solver(final Z3SymbolTable symbolTable, final Z3TransformationManager t this.z3Solver = z3Solver; assertions = new StackImpl<>(); - assumptions = new HashMap<>(); + assumptions = Containers.createMap(); } //// @@ -234,7 +234,7 @@ private final class Z3Model extends Valuation { public Z3Model(final com.microsoft.z3.Model z3Model) { this.z3Model = z3Model; - constToExpr = new HashMap<>(); + constToExpr = Containers.createMap(); } @Override diff --git a/subprojects/common/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3SymbolTable.java b/subprojects/common/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3SymbolTable.java index a819401872..4b1c6f58cf 100644 --- a/subprojects/common/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3SymbolTable.java +++ b/subprojects/common/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3SymbolTable.java @@ -42,19 +42,19 @@ public boolean definesSymbol(final com.microsoft.z3.FuncDecl symbol) { } public com.microsoft.z3.FuncDecl getSymbol(final ConstDecl constDecl) { - checkArgument(definesConst(constDecl), "Declaration " + constDecl + " not found in symbol table"); + checkArgument(definesConst(constDecl), "Declaration %s not found in symbol table",constDecl); return constToSymbol.get(constDecl); } public ConstDecl getConst(final com.microsoft.z3.FuncDecl symbol) { - checkArgument(definesSymbol(symbol), "Symbol " + symbol + " not found in symbol table"); + checkArgument(definesSymbol(symbol), "Symbol %s not found in symbol table",symbol); return constToSymbol.inverse().get(symbol); } public void put(final ConstDecl constDecl, final com.microsoft.z3.FuncDecl symbol) { checkNotNull(constDecl); checkNotNull(symbol); - checkState(!constToSymbol.containsKey(constDecl), "Constant " + constDecl + " not found."); + checkState(!constToSymbol.containsKey(constDecl), "Constant %s not found.",constDecl); constToSymbol.put(constDecl, symbol); } diff --git a/subprojects/common/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3TermTransformer.java b/subprojects/common/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3TermTransformer.java index e09139c7d2..9b4e647de8 100644 --- a/subprojects/common/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3TermTransformer.java +++ b/subprojects/common/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3TermTransformer.java @@ -41,14 +41,12 @@ import java.util.stream.Stream; import com.google.common.collect.ImmutableList; -import com.microsoft.z3.ArrayExpr; -import com.microsoft.z3.ArraySort; -import com.microsoft.z3.FuncDecl; -import com.microsoft.z3.Model; +import com.microsoft.z3.*; import hu.bme.mit.theta.common.TernaryOperator; import hu.bme.mit.theta.common.TriFunction; import hu.bme.mit.theta.common.Tuple2; +import hu.bme.mit.theta.common.container.Containers; import hu.bme.mit.theta.core.decl.Decl; import hu.bme.mit.theta.core.decl.ParamDecl; import hu.bme.mit.theta.core.type.Expr; @@ -91,7 +89,7 @@ final class Z3TermTransformer { public Z3TermTransformer(final Z3SymbolTable symbolTable) { this.symbolTable = symbolTable; - environment = new HashMap<>(); + environment = Containers.createMap(); environment.put("true", exprNullaryOperator(TrueExpr::getInstance)); environment.put("false", exprNullaryOperator(FalseExpr::getInstance)); environment.put("not", exprUnaryOperator(NotExpr::create)); @@ -188,8 +186,13 @@ private Expr transform(final com.microsoft.z3.Expr term, final Model model, private Expr transformIntLit(final com.microsoft.z3.Expr term) { final com.microsoft.z3.IntNum intNum = (com.microsoft.z3.IntNum) term; - final var value = intNum.getBigInteger(); - return Int(value); + try{ + final var value = intNum.getInt64(); + return Int(BigInteger.valueOf(value)); + } catch (Z3Exception ex){ + final var value = intNum.getBigInteger(); + return Int(value); + } } private Expr transformRatLit(final com.microsoft.z3.Expr term) { diff --git a/subprojects/sts/sts/src/main/java/hu/bme/mit/theta/sts/STS.java b/subprojects/sts/sts/src/main/java/hu/bme/mit/theta/sts/STS.java index 910f5dda4b..e16cef9acc 100644 --- a/subprojects/sts/sts/src/main/java/hu/bme/mit/theta/sts/STS.java +++ b/subprojects/sts/sts/src/main/java/hu/bme/mit/theta/sts/STS.java @@ -23,7 +23,7 @@ import java.util.Collection; import java.util.Collections; -import java.util.HashSet; +import hu.bme.mit.theta.common.container.Containers; import java.util.Set; import hu.bme.mit.theta.common.Utils; @@ -53,7 +53,7 @@ public STS(final Expr init, final Expr trans, final Expr> tmpVars = new HashSet<>(); + final Set> tmpVars = Containers.createSet(); ExprUtils.collectVars(init, tmpVars); ExprUtils.collectVars(trans, tmpVars); ExprUtils.collectVars(prop, tmpVars); @@ -113,8 +113,8 @@ public static final class Builder { private Expr prop; private Builder() { - init = new HashSet<>(); - trans = new HashSet<>(); + init = Containers.createSet(); + trans = Containers.createSet(); prop = null; } diff --git a/subprojects/sts/sts/src/main/java/hu/bme/mit/theta/sts/aiger/AigerToSts.java b/subprojects/sts/sts/src/main/java/hu/bme/mit/theta/sts/aiger/AigerToSts.java index 2436823d04..b19b2aaa19 100644 --- a/subprojects/sts/sts/src/main/java/hu/bme/mit/theta/sts/aiger/AigerToSts.java +++ b/subprojects/sts/sts/src/main/java/hu/bme/mit/theta/sts/aiger/AigerToSts.java @@ -20,7 +20,7 @@ import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Iff; import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Not; -import java.util.HashMap; +import hu.bme.mit.theta.common.container.Containers; import java.util.Map; import hu.bme.mit.theta.core.decl.Decls; @@ -55,7 +55,7 @@ private AigerToSts() { public static STS createSts(final AigerSystem aigerSys) { final Builder builder = STS.builder(); - final Map> vars = new HashMap<>(); + final Map> vars = Containers.createMap(); aigerSys.getNodes().forEach(n -> vars.put(n, Decls.Var(n.getName(), Bool()))); for (final AigerNode node : aigerSys.getNodes()) { diff --git a/subprojects/sts/sts/src/main/java/hu/bme/mit/theta/sts/aiger/utils/AigerCoi.java b/subprojects/sts/sts/src/main/java/hu/bme/mit/theta/sts/aiger/utils/AigerCoi.java index 00a5e4ac0d..d91d37a9c0 100644 --- a/subprojects/sts/sts/src/main/java/hu/bme/mit/theta/sts/aiger/utils/AigerCoi.java +++ b/subprojects/sts/sts/src/main/java/hu/bme/mit/theta/sts/aiger/utils/AigerCoi.java @@ -16,7 +16,7 @@ package hu.bme.mit.theta.sts.aiger.utils; import java.util.ArrayDeque; -import java.util.HashSet; +import hu.bme.mit.theta.common.container.Containers; import java.util.Iterator; import java.util.Queue; import java.util.Set; @@ -45,7 +45,7 @@ public static void apply(final AigerSystem system) { } private static Set getReachableNodes(final AigerSystem system) { - final Set reached = new HashSet<>(); + final Set reached = Containers.createSet(); final Queue queue = new ArrayDeque<>(); queue.add(system.getOutput()); diff --git a/subprojects/sts/sts/src/main/java/hu/bme/mit/theta/sts/aiger/utils/AigerVisualizer.java b/subprojects/sts/sts/src/main/java/hu/bme/mit/theta/sts/aiger/utils/AigerVisualizer.java index ea3e261d46..59e4301bd3 100644 --- a/subprojects/sts/sts/src/main/java/hu/bme/mit/theta/sts/aiger/utils/AigerVisualizer.java +++ b/subprojects/sts/sts/src/main/java/hu/bme/mit/theta/sts/aiger/utils/AigerVisualizer.java @@ -17,7 +17,7 @@ import static java.lang.System.lineSeparator; -import java.util.HashSet; +import hu.bme.mit.theta.common.container.Containers; import java.util.Set; import hu.bme.mit.theta.sts.aiger.elements.AigerNode; @@ -73,7 +73,7 @@ private static void appendNodes(final AigerSystem system, final StringBuilder sb } private static void appendWires(final AigerSystem system, final StringBuilder sb) { - final Set wires = new HashSet<>(); + final Set wires = Containers.createSet(); system.getNodes().forEach(n -> wires.addAll(n.getInWires())); system.getNodes().forEach(n -> wires.addAll(n.getOutWires())); wires.addAll(system.getOutput().getInWires()); diff --git a/subprojects/sts/sts/src/main/java/hu/bme/mit/theta/sts/dsl/StsDslHelper.java b/subprojects/sts/sts/src/main/java/hu/bme/mit/theta/sts/dsl/StsDslHelper.java index 2f39561d14..77c6108b79 100644 --- a/subprojects/sts/sts/src/main/java/hu/bme/mit/theta/sts/dsl/StsDslHelper.java +++ b/subprojects/sts/sts/src/main/java/hu/bme/mit/theta/sts/dsl/StsDslHelper.java @@ -23,7 +23,7 @@ import static java.util.stream.Collectors.toList; import java.util.Collections; -import java.util.HashMap; +import hu.bme.mit.theta.common.container.Containers; import java.util.List; import java.util.Map; import java.util.Optional; @@ -87,7 +87,7 @@ public static VarDecl createVarDecl(final VarDeclContext varDeclCtx) { public static Substitution createConstDefs(final Scope scope, final Substitution assignment, final List constDeclCtxs) { - final Map, Expr> declToExpr = new HashMap<>(); + final Map, Expr> declToExpr = Containers.createMap(); for (final ConstDeclContext constDeclCtx : constDeclCtxs) { addDef(scope, assignment, declToExpr, constDeclCtx); } diff --git a/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/XstsAction.java b/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/XstsAction.java index 1b99a47184..6470324c40 100644 --- a/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/XstsAction.java +++ b/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/XstsAction.java @@ -9,19 +9,23 @@ public final class XstsAction extends StmtAction { - private final Stmt stmt; + private final List stmts; - private XstsAction(final Stmt stmt) { - this.stmt = stmt; + private XstsAction(final List stmts) { + this.stmts = stmts; } public static XstsAction create(final Stmt stmt) { - return new XstsAction(stmt); + return new XstsAction(ImmutableList.of(stmt)); + } + + public static XstsAction create(final List stmts) { + return new XstsAction(stmts); } @Override public List getStmts() { - return ImmutableList.of(stmt); + return stmts; } @Override @@ -30,7 +34,7 @@ public boolean equals(final Object obj) { return true; } else if (obj instanceof XstsAction) { final XstsAction that = (XstsAction) obj; - return this.stmt.equals(that.stmt); + return this.stmts.equals(that.stmts); } else { return false; } @@ -38,6 +42,6 @@ public boolean equals(final Object obj) { @Override public String toString() { - return Utils.lispStringBuilder(getClass().getSimpleName()).body().add(stmt).toString(); + return Utils.lispStringBuilder(getClass().getSimpleName()).body().addAll(stmts).toString(); } } diff --git a/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/XstsLts.java b/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/XstsLts.java index f238f1fc92..0ddf55858c 100644 --- a/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/XstsLts.java +++ b/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/XstsLts.java @@ -1,31 +1,43 @@ package hu.bme.mit.theta.xsts.analysis; import hu.bme.mit.theta.analysis.LTS; +import hu.bme.mit.theta.analysis.expr.ExprState; +import hu.bme.mit.theta.core.stmt.NonDetStmt; import hu.bme.mit.theta.xsts.XSTS; import java.util.Collection; import java.util.stream.Collectors; -public final class XstsLts implements LTS { +public final class XstsLts implements LTS, XstsAction> { - private final Collection internalActions; - private final Collection externalActions; - private final Collection initActions; + private final NonDetStmt trans; + private final NonDetStmt env; + private final NonDetStmt init; - private XstsLts(final XSTS xsts) { - internalActions = xsts.getTran().getStmts().stream().map(XstsAction::create).collect(Collectors.toList()); - externalActions = xsts.getEnv().getStmts().stream().map(XstsAction::create).collect(Collectors.toList()); - initActions = xsts.getInit().getStmts().stream().map(XstsAction::create).collect(Collectors.toList()); + private final XstsStmtOptimizer stmtOptimizer; + + private XstsLts(final XSTS xsts, final XstsStmtOptimizer stmtOptimizer) { + trans = xsts.getTran(); + env = xsts.getEnv(); + init = xsts.getInit(); + + this.stmtOptimizer = stmtOptimizer; } - public static LTS create(final XSTS xsts) { - return new XstsLts(xsts); + public static LTS, XstsAction> create(final XSTS xsts, final XstsStmtOptimizer stmtOptimizer) { + return new XstsLts<>(xsts,stmtOptimizer); } @Override - public Collection getEnabledActionsFor(XstsState state) { - if (!state.isInitialized()) return initActions; - else if (state.lastActionWasEnv()) return internalActions; - else return externalActions; + public Collection getEnabledActionsFor(XstsState state) { + NonDetStmt enabledSet; + if (!state.isInitialized()) enabledSet = init; + else if (state.lastActionWasEnv()) enabledSet = trans; + else enabledSet = env; + + return enabledSet.getStmts().stream() + .map(stmt -> stmtOptimizer.optimizeStmt(state,stmt)) + .map(XstsAction::create) + .collect(Collectors.toList()); } } diff --git a/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/XstsStmtOptimizer.java b/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/XstsStmtOptimizer.java new file mode 100644 index 0000000000..7afc6b0dcb --- /dev/null +++ b/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/XstsStmtOptimizer.java @@ -0,0 +1,23 @@ +package hu.bme.mit.theta.xsts.analysis; + +import hu.bme.mit.theta.analysis.stmtoptimizer.StmtOptimizer; +import hu.bme.mit.theta.analysis.expr.ExprState; +import hu.bme.mit.theta.core.stmt.Stmt; + +public class XstsStmtOptimizer implements StmtOptimizer> { + + private final StmtOptimizer stmtOptimizer; + + private XstsStmtOptimizer(final StmtOptimizer stmtOptimizer) { + this.stmtOptimizer = stmtOptimizer; + } + + public static XstsStmtOptimizer create(final StmtOptimizer stmtOptimizer){ + return new XstsStmtOptimizer<>(stmtOptimizer); + } + + @Override + public Stmt optimizeStmt(final XstsState state, final Stmt stmt) { + return stmtOptimizer.optimizeStmt(state.getState(),stmt); + } +} diff --git a/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/config/XstsConfigBuilder.java b/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/config/XstsConfigBuilder.java index b48607af33..7e5ec58a0b 100644 --- a/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/config/XstsConfigBuilder.java +++ b/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/config/XstsConfigBuilder.java @@ -16,10 +16,8 @@ import hu.bme.mit.theta.analysis.prod2.Prod2Analysis; import hu.bme.mit.theta.analysis.prod2.Prod2Prec; import hu.bme.mit.theta.analysis.prod2.Prod2State; -import hu.bme.mit.theta.analysis.prod2.prod2explpred.AutomaticItpRefToProd2ExplPredPrec; -import hu.bme.mit.theta.analysis.prod2.prod2explpred.ItpRefToProd2ExplPredPrec; -import hu.bme.mit.theta.analysis.prod2.prod2explpred.Prod2ExplPredPreStrengtheningOperator; -import hu.bme.mit.theta.analysis.prod2.prod2explpred.Prod2ExplPredStrengtheningOperator; +import hu.bme.mit.theta.analysis.prod2.prod2explpred.*; +import hu.bme.mit.theta.analysis.stmtoptimizer.DefaultStmtOptimizer; import hu.bme.mit.theta.analysis.waitlist.PriorityWaitlist; import hu.bme.mit.theta.common.logging.Logger; import hu.bme.mit.theta.common.logging.NullLogger; @@ -40,7 +38,7 @@ public class XstsConfigBuilder { public enum Domain { - EXPL, PRED_BOOL, PRED_CART, PRED_SPLIT, PROD, PROD_AUTO + EXPL, PRED_BOOL, PRED_CART, PRED_SPLIT, EXPL_PRED_BOOL, EXPL_PRED_CART, EXPL_PRED_SPLIT } public enum Refinement { @@ -91,6 +89,10 @@ private InitPrec(final XstsInitPrec builder) { } + public enum OptimizeStmts { + ON, OFF + } + private Logger logger = NullLogger.getInstance(); private final SolverFactory solverFactory; private final Domain domain; @@ -101,6 +103,7 @@ private InitPrec(final XstsInitPrec builder) { private int maxPredCount = 0; private InitPrec initPrec = InitPrec.EMPTY; private PruneStrategy pruneStrategy = PruneStrategy.LAZY; + private OptimizeStmts optimizeStmts = OptimizeStmts.ON; public XstsConfigBuilder(final Domain domain, final Refinement refinement, final SolverFactory solverFactory) { this.domain = domain; @@ -143,12 +146,23 @@ public XstsConfigBuilder pruneStrategy(final PruneStrategy pruneStrategy) { return this; } + public XstsConfigBuilder optimizeStmts(final OptimizeStmts optimizeStmts) { + this.optimizeStmts = optimizeStmts; + return this; + } + public XstsConfig build(final XSTS xsts) { final ItpSolver solver = solverFactory.createItpSolver(); - LTS lts = XstsLts.create(xsts); final Expr negProp = Not(xsts.getProp()); if (domain == Domain.EXPL) { + final LTS, XstsAction> lts; + if(optimizeStmts == OptimizeStmts.ON){ + lts = XstsLts.create(xsts,XstsStmtOptimizer.create(ExplStmtOptimizer.getInstance())); + } else { + lts = XstsLts.create(xsts, XstsStmtOptimizer.create(DefaultStmtOptimizer.create())); + } + final Predicate> target = new XstsStatePredicate(new ExplStatePredicate(negProp, solver)); final Analysis, XstsAction, ExplPrec> analysis = XstsAnalysis.create(ExplStmtAnalysis.create(solver, xsts.getInitFormula(), maxEnum)); final ArgBuilder, XstsAction, ExplPrec> argBuilder = ArgBuilder.create(lts, analysis, target, @@ -206,6 +220,14 @@ public XstsConfigBuilder pruneStrategy(final PruneStrategy pruneStrategy) { default: throw new UnsupportedOperationException(domain + " domain is not supported."); } + + final LTS, XstsAction> lts; + if(optimizeStmts == OptimizeStmts.ON){ + lts = XstsLts.create(xsts,XstsStmtOptimizer.create(PredStmtOptimizer.getInstance())); + } else { + lts = XstsLts.create(xsts, XstsStmtOptimizer.create(DefaultStmtOptimizer.create())); + } + final Predicate> target = new XstsStatePredicate(new ExprStatePredicate(negProp, solver)); final Analysis, XstsAction, PredPrec> analysis = XstsAnalysis.create(PredAnalysis.create(solver, predAbstractor, xsts.getInitFormula())); @@ -249,15 +271,38 @@ public XstsConfigBuilder pruneStrategy(final PruneStrategy pruneStrategy) { final PredPrec prec = initPrec.builder.createPred(xsts); return XstsConfig.create(checker, prec); - } else if (domain == Domain.PROD || domain==domain.PROD_AUTO) { - final PredAbstractors.PredAbstractor predAbstractor = PredAbstractors.cartesianAbstractor(solver); + } else if (domain == Domain.EXPL_PRED_BOOL || domain == Domain.EXPL_PRED_CART || domain == Domain.EXPL_PRED_SPLIT) { + final LTS>, XstsAction> lts; + if(optimizeStmts == OptimizeStmts.ON){ + lts = XstsLts.create(xsts,XstsStmtOptimizer.create( + Prod2ExplPredStmtOptimizer.create( + ExplStmtOptimizer.getInstance() + ))); + } else { + lts = XstsLts.create(xsts, XstsStmtOptimizer.create(DefaultStmtOptimizer.create())); + } + + final PredAbstractors.PredAbstractor predAbstractor; + switch (domain) { + case EXPL_PRED_BOOL: + predAbstractor = PredAbstractors.booleanAbstractor(solver); + break; + case EXPL_PRED_SPLIT: + predAbstractor = PredAbstractors.booleanSplitAbstractor(solver); + break; + case EXPL_PRED_CART: + predAbstractor = PredAbstractors.cartesianAbstractor(solver); + break; + default: + throw new UnsupportedOperationException(domain + " domain is not supported."); + } final Predicate>> target = new XstsStatePredicate>(new ExprStatePredicate(negProp, solver)); final Analysis>, XstsAction, Prod2Prec> analysis = XstsAnalysis.create(Prod2Analysis.create( - ExplStmtAnalysis.create(solver, xsts.getInitFormula(), maxEnum), - PredAnalysis.create(solver, predAbstractor, xsts.getInitFormula()), - Prod2ExplPredPreStrengtheningOperator.create(), - Prod2ExplPredStrengtheningOperator.create(solver))); + ExplStmtAnalysis.create(solver, xsts.getInitFormula(), maxEnum), + PredAnalysis.create(solver, predAbstractor, xsts.getInitFormula()), + Prod2ExplPredPreStrengtheningOperator.create(), + Prod2ExplPredStrengtheningOperator.create(solver))); final ArgBuilder>, XstsAction, Prod2Prec> argBuilder = ArgBuilder.create(lts, analysis, target, true); final Abstractor>, XstsAction, Prod2Prec> abstractor = BasicAbstractor.builder(argBuilder) @@ -269,18 +314,7 @@ public XstsConfigBuilder pruneStrategy(final PruneStrategy pruneStrategy) { Refiner>, XstsAction, Prod2Prec> refiner = null; final Set> ctrlVars = xsts.getCtrlVars(); - final RefutationToPrec, ItpRefutation> precRefiner; - switch (domain) { - case PROD: - precRefiner = ItpRefToProd2ExplPredPrec.create(ctrlVars, predSplit.splitter); - break; - case PROD_AUTO: - precRefiner = AutomaticItpRefToProd2ExplPredPrec.create(ctrlVars, predSplit.splitter, maxPredCount); - break; - default: - throw new UnsupportedOperationException( - "Unknown domain " + domain); - } + final RefutationToPrec, ItpRefutation> precRefiner = AutomaticItpRefToProd2ExplPredPrec.create(ctrlVars, predSplit.splitter, maxPredCount); switch (refinement) { case FW_BIN_ITP: diff --git a/subprojects/xsts/xsts-analysis/src/test/java/hu/bme/mit/theta/xsts/analysis/PnmlTest.java b/subprojects/xsts/xsts-analysis/src/test/java/hu/bme/mit/theta/xsts/analysis/PnmlTest.java index 1c8de23cfd..9743347692 100644 --- a/subprojects/xsts/xsts-analysis/src/test/java/hu/bme/mit/theta/xsts/analysis/PnmlTest.java +++ b/subprojects/xsts/xsts-analysis/src/test/java/hu/bme/mit/theta/xsts/analysis/PnmlTest.java @@ -63,9 +63,9 @@ public class PnmlTest { public static Collection data() { return Arrays.asList(new Object[][] { - { "src/test/resources/model/pnml/DPhil-10.pnml", "0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0", "0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1", true, XstsConfigBuilder.Domain.EXPL}, +// { "src/test/resources/model/pnml/DPhil-10.pnml", "0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0", "0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1", true, XstsConfigBuilder.Domain.EXPL}, - { "src/test/resources/model/pnml/DPhil-100.pnml", "0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0", "0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1", true, XstsConfigBuilder.Domain.EXPL}, +// { "src/test/resources/model/pnml/DPhil-100.pnml", "0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 1 0", "0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1", true, XstsConfigBuilder.Domain.EXPL}, }); } diff --git a/subprojects/xsts/xsts-analysis/src/test/java/hu/bme/mit/theta/xsts/analysis/XstsTest.java b/subprojects/xsts/xsts-analysis/src/test/java/hu/bme/mit/theta/xsts/analysis/XstsTest.java index 06b7b4d0bb..8277eaf515 100644 --- a/subprojects/xsts/xsts-analysis/src/test/java/hu/bme/mit/theta/xsts/analysis/XstsTest.java +++ b/subprojects/xsts/xsts-analysis/src/test/java/hu/bme/mit/theta/xsts/analysis/XstsTest.java @@ -60,25 +60,25 @@ public static Collection data() { { "src/test/resources/model/trafficlight.xsts", "src/test/resources/property/green_and_red.prop", true, XstsConfigBuilder.Domain.PRED_CART}, - { "src/test/resources/model/trafficlight.xsts", "src/test/resources/property/green_and_red.prop", true, XstsConfigBuilder.Domain.PROD}, + { "src/test/resources/model/trafficlight.xsts", "src/test/resources/property/green_and_red.prop", true, XstsConfigBuilder.Domain.EXPL_PRED_CART}, { "src/test/resources/model/trafficlight_v2.xsts", "src/test/resources/property/green_and_red.prop", true, XstsConfigBuilder.Domain.EXPL}, { "src/test/resources/model/trafficlight_v2.xsts", "src/test/resources/property/green_and_red.prop", true, XstsConfigBuilder.Domain.PRED_CART}, - { "src/test/resources/model/trafficlight_v2.xsts", "src/test/resources/property/green_and_red.prop", true, XstsConfigBuilder.Domain.PROD}, + { "src/test/resources/model/trafficlight_v2.xsts", "src/test/resources/property/green_and_red.prop", true, XstsConfigBuilder.Domain.EXPL_PRED_CART}, { "src/test/resources/model/counter5.xsts", "src/test/resources/property/x_between_0_and_5.prop", true, XstsConfigBuilder.Domain.EXPL}, { "src/test/resources/model/counter5.xsts", "src/test/resources/property/x_between_0_and_5.prop", true, XstsConfigBuilder.Domain.PRED_CART}, - { "src/test/resources/model/counter5.xsts", "src/test/resources/property/x_between_0_and_5.prop", true, XstsConfigBuilder.Domain.PROD}, + { "src/test/resources/model/counter5.xsts", "src/test/resources/property/x_between_0_and_5.prop", true, XstsConfigBuilder.Domain.EXPL_PRED_CART}, { "src/test/resources/model/counter5.xsts", "src/test/resources/property/x_eq_5.prop", false, XstsConfigBuilder.Domain.EXPL}, { "src/test/resources/model/counter5.xsts", "src/test/resources/property/x_eq_5.prop", false, XstsConfigBuilder.Domain.PRED_CART}, - { "src/test/resources/model/counter5.xsts", "src/test/resources/property/x_eq_5.prop", false, XstsConfigBuilder.Domain.PROD}, + { "src/test/resources/model/counter5.xsts", "src/test/resources/property/x_eq_5.prop", false, XstsConfigBuilder.Domain.EXPL_PRED_CART}, { "src/test/resources/model/x_and_y.xsts", "src/test/resources/property/x_geq_y.prop", true, XstsConfigBuilder.Domain.PRED_CART}, @@ -86,13 +86,13 @@ public static Collection data() { { "src/test/resources/model/cross_with.xsts", "src/test/resources/property/cross.prop", false, XstsConfigBuilder.Domain.PRED_CART}, - { "src/test/resources/model/cross_with.xsts", "src/test/resources/property/cross.prop", false, XstsConfigBuilder.Domain.EXPL}, +// { "src/test/resources/model/cross_with.xsts", "src/test/resources/property/cross.prop", false, XstsConfigBuilder.Domain.EXPL}, // { "src/test/resources/model/cross_with.xsts", "src/test/resources/property/cross.prop", false, XstsConfigBuilder.Domain.PROD}, { "src/test/resources/model/cross_without.xsts", "src/test/resources/property/cross.prop", false, XstsConfigBuilder.Domain.PRED_CART}, - { "src/test/resources/model/cross_without.xsts", "src/test/resources/property/cross.prop", false, XstsConfigBuilder.Domain.EXPL}, +// { "src/test/resources/model/cross_without.xsts", "src/test/resources/property/cross.prop", false, XstsConfigBuilder.Domain.EXPL}, // { "src/test/resources/model/cross_without.xsts", "src/test/resources/property/cross.prop", false, XstsConfigBuilder.Domain.PROD}, @@ -100,13 +100,13 @@ public static Collection data() { { "src/test/resources/model/choices.xsts", "src/test/resources/property/choices.prop", false, XstsConfigBuilder.Domain.EXPL}, - { "src/test/resources/model/choices.xsts", "src/test/resources/property/choices.prop", false, XstsConfigBuilder.Domain.PROD}, + { "src/test/resources/model/choices.xsts", "src/test/resources/property/choices.prop", false, XstsConfigBuilder.Domain.EXPL_PRED_CART}, { "src/test/resources/model/literals.xsts", "src/test/resources/property/literals.prop", true, XstsConfigBuilder.Domain.PRED_CART}, { "src/test/resources/model/literals.xsts", "src/test/resources/property/literals.prop", true, XstsConfigBuilder.Domain.EXPL}, - { "src/test/resources/model/literals.xsts", "src/test/resources/property/literals.prop", true, XstsConfigBuilder.Domain.PROD}, + { "src/test/resources/model/literals.xsts", "src/test/resources/property/literals.prop", true, XstsConfigBuilder.Domain.EXPL_PRED_CART}, { "src/test/resources/model/cross3.xsts", "src/test/resources/property/cross.prop", false, XstsConfigBuilder.Domain.PRED_CART}, @@ -118,61 +118,61 @@ public static Collection data() { { "src/test/resources/model/sequential.xsts", "src/test/resources/property/sequential.prop", true, XstsConfigBuilder.Domain.EXPL}, - { "src/test/resources/model/sequential.xsts", "src/test/resources/property/sequential.prop", true, XstsConfigBuilder.Domain.PROD}, + { "src/test/resources/model/sequential.xsts", "src/test/resources/property/sequential.prop", true, XstsConfigBuilder.Domain.EXPL_PRED_CART}, { "src/test/resources/model/sequential.xsts", "src/test/resources/property/sequential2.prop", false, XstsConfigBuilder.Domain.PRED_CART}, { "src/test/resources/model/sequential.xsts", "src/test/resources/property/sequential2.prop", false, XstsConfigBuilder.Domain.EXPL}, - { "src/test/resources/model/sequential.xsts", "src/test/resources/property/sequential2.prop", false, XstsConfigBuilder.Domain.PROD}, + { "src/test/resources/model/sequential.xsts", "src/test/resources/property/sequential2.prop", false, XstsConfigBuilder.Domain.EXPL_PRED_CART}, { "src/test/resources/model/on_off_statemachine.xsts", "src/test/resources/property/on_off_statemachine.prop", false, XstsConfigBuilder.Domain.PRED_CART}, { "src/test/resources/model/on_off_statemachine.xsts", "src/test/resources/property/on_off_statemachine.prop", false, XstsConfigBuilder.Domain.EXPL}, - { "src/test/resources/model/on_off_statemachine.xsts", "src/test/resources/property/on_off_statemachine.prop", false, XstsConfigBuilder.Domain.PROD}, + { "src/test/resources/model/on_off_statemachine.xsts", "src/test/resources/property/on_off_statemachine.prop", false, XstsConfigBuilder.Domain.EXPL_PRED_CART}, { "src/test/resources/model/on_off_statemachine.xsts", "src/test/resources/property/on_off_statemachine2.prop", true, XstsConfigBuilder.Domain.PRED_CART}, { "src/test/resources/model/on_off_statemachine.xsts", "src/test/resources/property/on_off_statemachine2.prop", true, XstsConfigBuilder.Domain.EXPL}, - { "src/test/resources/model/on_off_statemachine.xsts", "src/test/resources/property/on_off_statemachine2.prop", true, XstsConfigBuilder.Domain.PROD}, + { "src/test/resources/model/on_off_statemachine.xsts", "src/test/resources/property/on_off_statemachine2.prop", true, XstsConfigBuilder.Domain.EXPL_PRED_CART}, { "src/test/resources/model/on_off_statemachine.xsts", "src/test/resources/property/on_off_statemachine3.prop", false, XstsConfigBuilder.Domain.PRED_CART}, { "src/test/resources/model/on_off_statemachine.xsts", "src/test/resources/property/on_off_statemachine3.prop", false, XstsConfigBuilder.Domain.EXPL}, - { "src/test/resources/model/on_off_statemachine.xsts", "src/test/resources/property/on_off_statemachine3.prop", false, XstsConfigBuilder.Domain.PROD}, + { "src/test/resources/model/on_off_statemachine.xsts", "src/test/resources/property/on_off_statemachine3.prop", false, XstsConfigBuilder.Domain.EXPL_PRED_CART}, { "src/test/resources/model/counter50.xsts", "src/test/resources/property/x_eq_5.prop", false, XstsConfigBuilder.Domain.PRED_CART}, { "src/test/resources/model/counter50.xsts", "src/test/resources/property/x_eq_5.prop", false, XstsConfigBuilder.Domain.EXPL}, - { "src/test/resources/model/counter50.xsts", "src/test/resources/property/x_eq_5.prop", false, XstsConfigBuilder.Domain.PROD}, + { "src/test/resources/model/counter50.xsts", "src/test/resources/property/x_eq_5.prop", false, XstsConfigBuilder.Domain.EXPL_PRED_CART}, // { "src/test/resources/model/counter50.xsts", "src/test/resources/property/x_eq_50.prop", false, XstsConfigBuilder.Domain.PRED_CART}, { "src/test/resources/model/counter50.xsts", "src/test/resources/property/x_eq_50.prop", false, XstsConfigBuilder.Domain.EXPL}, - { "src/test/resources/model/counter50.xsts", "src/test/resources/property/x_eq_50.prop", false, XstsConfigBuilder.Domain.PROD}, + { "src/test/resources/model/counter50.xsts", "src/test/resources/property/x_eq_50.prop", false, XstsConfigBuilder.Domain.EXPL_PRED_CART}, { "src/test/resources/model/counter50.xsts", "src/test/resources/property/x_eq_51.prop", true, XstsConfigBuilder.Domain.PRED_CART}, { "src/test/resources/model/counter50.xsts", "src/test/resources/property/x_eq_51.prop", true, XstsConfigBuilder.Domain.EXPL}, - { "src/test/resources/model/counter50.xsts", "src/test/resources/property/x_eq_51.prop", true, XstsConfigBuilder.Domain.PROD}, + { "src/test/resources/model/counter50.xsts", "src/test/resources/property/x_eq_51.prop", true, XstsConfigBuilder.Domain.EXPL_PRED_CART}, { "src/test/resources/model/count_up_down.xsts", "src/test/resources/property/count_up_down.prop", false, XstsConfigBuilder.Domain.PRED_CART}, { "src/test/resources/model/count_up_down.xsts", "src/test/resources/property/count_up_down.prop", false, XstsConfigBuilder.Domain.EXPL}, - { "src/test/resources/model/count_up_down.xsts", "src/test/resources/property/count_up_down.prop", false, XstsConfigBuilder.Domain.PROD}, + { "src/test/resources/model/count_up_down.xsts", "src/test/resources/property/count_up_down.prop", false, XstsConfigBuilder.Domain.EXPL_PRED_CART}, { "src/test/resources/model/count_up_down.xsts", "src/test/resources/property/count_up_down2.prop", true, XstsConfigBuilder.Domain.PRED_CART}, { "src/test/resources/model/count_up_down.xsts", "src/test/resources/property/count_up_down2.prop", true, XstsConfigBuilder.Domain.EXPL}, - { "src/test/resources/model/count_up_down.xsts", "src/test/resources/property/count_up_down2.prop", true, XstsConfigBuilder.Domain.PROD}, + { "src/test/resources/model/count_up_down.xsts", "src/test/resources/property/count_up_down2.prop", true, XstsConfigBuilder.Domain.EXPL_PRED_CART}, { "src/test/resources/model/bhmr2007.xsts", "src/test/resources/property/bhmr2007.prop", true, XstsConfigBuilder.Domain.PRED_CART}, @@ -184,7 +184,7 @@ public static Collection data() { { "src/test/resources/model/css2003.xsts", "src/test/resources/property/css2003.prop", true, XstsConfigBuilder.Domain.EXPL}, - { "src/test/resources/model/css2003.xsts", "src/test/resources/property/css2003.prop", true, XstsConfigBuilder.Domain.PROD}, + { "src/test/resources/model/css2003.xsts", "src/test/resources/property/css2003.prop", true, XstsConfigBuilder.Domain.EXPL_PRED_CART}, // { "src/test/resources/model/ort.xsts", "src/test/resources/property/x_gt_2.prop", false, XstsConfigBuilder.Domain.PRED_CART}, @@ -196,31 +196,31 @@ public static Collection data() { { "src/test/resources/model/array_counter.xsts", "src/test/resources/property/array_10.prop", false, XstsConfigBuilder.Domain.EXPL}, - { "src/test/resources/model/array_counter.xsts", "src/test/resources/property/array_10.prop", false, XstsConfigBuilder.Domain.PROD}, - - { "src/test/resources/model/array_counter.xsts", "src/test/resources/property/array_10.prop", false, XstsConfigBuilder.Domain.PROD_AUTO}, + { "src/test/resources/model/array_counter.xsts", "src/test/resources/property/array_10.prop", false, XstsConfigBuilder.Domain.EXPL_PRED_CART}, { "src/test/resources/model/array_constant.xsts", "src/test/resources/property/array_constant.prop", true, XstsConfigBuilder.Domain.PRED_CART}, { "src/test/resources/model/array_constant.xsts", "src/test/resources/property/array_constant.prop", true, XstsConfigBuilder.Domain.EXPL}, - { "src/test/resources/model/array_constant.xsts", "src/test/resources/property/array_constant.prop", true, XstsConfigBuilder.Domain.PROD}, - - { "src/test/resources/model/array_constant.xsts", "src/test/resources/property/array_constant.prop", true, XstsConfigBuilder.Domain.PROD_AUTO}, + { "src/test/resources/model/array_constant.xsts", "src/test/resources/property/array_constant.prop", true, XstsConfigBuilder.Domain.EXPL_PRED_CART}, { "src/test/resources/model/localvars.xsts", "src/test/resources/property/localvars.prop", true, XstsConfigBuilder.Domain.PRED_CART}, { "src/test/resources/model/localvars.xsts", "src/test/resources/property/localvars.prop", true, XstsConfigBuilder.Domain.EXPL}, - { "src/test/resources/model/localvars.xsts", "src/test/resources/property/localvars.prop", true, XstsConfigBuilder.Domain.PROD_AUTO}, + { "src/test/resources/model/localvars.xsts", "src/test/resources/property/localvars.prop", true, XstsConfigBuilder.Domain.EXPL_PRED_CART}, { "src/test/resources/model/localvars2.xsts", "src/test/resources/property/localvars2.prop", true, XstsConfigBuilder.Domain.PRED_CART}, { "src/test/resources/model/localvars2.xsts", "src/test/resources/property/localvars2.prop", true, XstsConfigBuilder.Domain.EXPL}, - { "src/test/resources/model/localvars2.xsts", "src/test/resources/property/localvars2.prop", true, XstsConfigBuilder.Domain.PROD_AUTO} + { "src/test/resources/model/localvars2.xsts", "src/test/resources/property/localvars2.prop", true, XstsConfigBuilder.Domain.EXPL_PRED_CART}, + + { "src/test/resources/model/loopxy.xsts", "src/test/resources/property/loopxy.prop", true, XstsConfigBuilder.Domain.EXPL}, + { "src/test/resources/model/loopxy.xsts", "src/test/resources/property/loopxy.prop", true, XstsConfigBuilder.Domain.EXPL_PRED_CART}, + { "src/test/resources/model/loopxy.xsts", "src/test/resources/property/loopxy.prop", true, XstsConfigBuilder.Domain.PRED_CART} }); } @@ -234,7 +234,7 @@ public void test() throws IOException { xsts = XstsDslManager.createXsts(inputStream); } - final XstsConfig configuration = new XstsConfigBuilder(domain, XstsConfigBuilder.Refinement.SEQ_ITP, Z3SolverFactory.getInstance()).initPrec(XstsConfigBuilder.InitPrec.CTRL).predSplit(XstsConfigBuilder.PredSplit.CONJUNCTS).maxEnum(250).logger(logger).build(xsts); + final XstsConfig configuration = new XstsConfigBuilder(domain, XstsConfigBuilder.Refinement.SEQ_ITP, Z3SolverFactory.getInstance()).initPrec(XstsConfigBuilder.InitPrec.CTRL).optimizeStmts(XstsConfigBuilder.OptimizeStmts.ON).predSplit(XstsConfigBuilder.PredSplit.CONJUNCTS).maxEnum(250).logger(logger).build(xsts); final SafetyResult status = configuration.check(); if (safe) { assertTrue(status.isSafe()); diff --git a/subprojects/xsts/xsts-analysis/src/test/resources/model/loopxy.xsts b/subprojects/xsts/xsts-analysis/src/test/resources/model/loopxy.xsts new file mode 100644 index 0000000000..4cb0b58e30 --- /dev/null +++ b/subprojects/xsts/xsts-analysis/src/test/resources/model/loopxy.xsts @@ -0,0 +1,18 @@ +ctrl var x: integer = 0 + +trans { + choice{ + x:=3; + } or { + x:=3; + } + local var y: integer = 0; + for i from 1 to x*x/x+1 do y:=y+1; + for i from 1 to y+1 do { + x:=x-1; + } +} + +init{} + +env{} \ No newline at end of file diff --git a/subprojects/xsts/xsts-analysis/src/test/resources/property/loopxy.prop b/subprojects/xsts/xsts-analysis/src/test/resources/property/loopxy.prop new file mode 100644 index 0000000000..7e75676fba --- /dev/null +++ b/subprojects/xsts/xsts-analysis/src/test/resources/property/loopxy.prop @@ -0,0 +1,3 @@ +prop{ + x==0 +} \ No newline at end of file diff --git a/subprojects/xsts/xsts-cli/README.md b/subprojects/xsts/xsts-cli/README.md index a320e0aafb..65bb0c5e6a 100644 --- a/subprojects/xsts/xsts-cli/README.md +++ b/subprojects/xsts/xsts-cli/README.md @@ -50,6 +50,9 @@ All arguments are optional, except `--model` and `--property`. * `--version`: Print version info (in this case `--model` and `--property` is of course not required). * `--metrics`: Print metrics about the XSTS model (number of variables and statements). * `--initialmarking`: Can be used with the PNML frontend. Override the initial markings of the places. Format: list the values to be assigned to each place in the order of their definition in the PNML file separated with spaces. +* `--visualize`: Visualize the result of the analysis (the reachability graph if the model is safe, or a counterexample trace if it is unsafe). Prints to the dotfile given as parameter. +* `--optimizestmts`: The algorithm can optimize stmts by detecting failing assumptions and unreachable branches of choices. + * Possible values: `ON` (default), `OFF`. The arguments related to the algorithm are described in more detail (along with best practices) in [CEGAR-algorithms.md](../../../doc/CEGAR-algorithms.md). diff --git a/subprojects/xsts/xsts-cli/src/main/java/hu/bme/mit/theta/xsts/cli/XstsCli.java b/subprojects/xsts/xsts-cli/src/main/java/hu/bme/mit/theta/xsts/cli/XstsCli.java index 1dc97c1763..6d2c1c509a 100644 --- a/subprojects/xsts/xsts-cli/src/main/java/hu/bme/mit/theta/xsts/cli/XstsCli.java +++ b/subprojects/xsts/xsts-cli/src/main/java/hu/bme/mit/theta/xsts/cli/XstsCli.java @@ -8,12 +8,16 @@ import hu.bme.mit.theta.analysis.algorithm.SafetyResult; import hu.bme.mit.theta.analysis.algorithm.cegar.CegarStatistics; import hu.bme.mit.theta.analysis.expr.refinement.PruneStrategy; +import hu.bme.mit.theta.analysis.utils.ArgVisualizer; +import hu.bme.mit.theta.analysis.utils.TraceVisualizer; import hu.bme.mit.theta.common.CliUtils; import hu.bme.mit.theta.common.logging.ConsoleLogger; import hu.bme.mit.theta.common.logging.Logger; import hu.bme.mit.theta.common.logging.NullLogger; import hu.bme.mit.theta.common.table.BasicTableWriter; import hu.bme.mit.theta.common.table.TableWriter; +import hu.bme.mit.theta.common.visualization.Graph; +import hu.bme.mit.theta.common.visualization.writer.GraphvizWriter; import hu.bme.mit.theta.solver.z3.Z3SolverFactory; import hu.bme.mit.theta.xsts.XSTS; import hu.bme.mit.theta.xsts.analysis.XstsAction; @@ -71,6 +75,9 @@ public class XstsCli { @Parameter(names = "--prunestrategy", description = "Strategy for pruning the ARG after refinement") PruneStrategy pruneStrategy = PruneStrategy.LAZY; + @Parameter(names = "--optimizestmts", description = "Turn statement optimization on or off") + OptimizeStmts optimizeStmts = OptimizeStmts.ON; + @Parameter(names = {"--loglevel"}, description = "Detailedness of logging") Logger.Level logLevel = Logger.Level.SUBSTEP; @@ -92,6 +99,9 @@ public class XstsCli { @Parameter(names = "--version", description = "Display version", help = true) boolean versionInfo = false; + @Parameter(names = {"--visualize"}, description = "Write proof or counterexample to file in dot format") + String dotfile = null; + private Logger logger; public XstsCli(final String[] args) { @@ -141,6 +151,9 @@ private void run() { if (status.isUnsafe() && cexfile != null) { writeCex(status.asUnsafe(), xsts); } + if (dotfile != null) { + writeVisualStatus(status, dotfile); + } } catch (final Throwable ex) { printError(ex); System.exit(1); @@ -189,7 +202,7 @@ private XSTS loadModel() throws Exception { try { return new XstsConfigBuilder(domain, refinement, Z3SolverFactory.getInstance()) .maxEnum(maxEnum).maxPredCount(maxPredCount).initPrec(initPrec).pruneStrategy(pruneStrategy) - .search(search).predSplit(predSplit).logger(logger).build(xsts); + .search(search).predSplit(predSplit).optimizeStmts(optimizeStmts).logger(logger).build(xsts); } catch (final Exception ex) { throw new Exception("Could not create configuration: " + ex.getMessage(), ex); } @@ -244,4 +257,11 @@ private void writeCex(final SafetyResult.Unsafe status, final XSTS xsts) t } } + private void writeVisualStatus(final SafetyResult status, final String filename) + throws FileNotFoundException { + final Graph graph = status.isSafe() ? ArgVisualizer.getDefault().visualize(status.asSafe().getArg()) + : TraceVisualizer.getDefault().visualize(status.asUnsafe().getTrace()); + GraphvizWriter.getInstance().writeFile(graph, filename); + } + } diff --git a/subprojects/xsts/xsts/README.md b/subprojects/xsts/xsts/README.md index a193970328..055e24bb52 100644 --- a/subprojects/xsts/xsts/README.md +++ b/subprojects/xsts/xsts/README.md @@ -96,6 +96,7 @@ The behaviour of XSTSs can be described using transitions. A transition is an at * nondeterministic choices of the form `choice { } or { }`, with 1 or more branches * sequences of the form ` ` * blocks + * loops of the form `for from to do `, where `` has to be evaluable before the start of the loop and `` must not affect the value of `` (experimental, can only be used with `--optimizestmts ON`, the upper bound is not included in the range, the loop variable only exists in the loop body) Only those branches of a choice statement are considered for execution, of which all contained assumptions evaluate to true. @@ -114,6 +115,9 @@ choice { } or { havoc y; } + for i from 1 to z do { + z := i+1; + } x := x-1; } y := y * 2; diff --git a/subprojects/xsts/xsts/src/main/antlr/XstsDsl.g4 b/subprojects/xsts/xsts/src/main/antlr/XstsDsl.g4 index d7e9e5a89b..4a9f5369ab 100644 --- a/subprojects/xsts/xsts/src/main/antlr/XstsDsl.g4 +++ b/subprojects/xsts/xsts/src/main/antlr/XstsDsl.g4 @@ -261,23 +261,28 @@ stmt: localVarDeclStmt | assumeStmt | nonDetStmt | blockStmt + | loopStmt ; nonDetStmt - : CHOICE blocks+=blockStmt (NONDET_OR blocks+=blockStmt)* + : CHOICE blocks+=stmt (NONDET_OR blocks+=stmt)* ; blockStmt - : LCURLY subStmt=seqStmt RCURLY + : LCURLY (stmts+=stmt)* RCURLY + ; + +loopStmt + : FOR loopVar=ID FROM from=expr TO to=expr DO subStmt=stmt ; localVarDeclStmt : LOCAL VAR name=ID DP ttype=type (EQUALS initValue=expr)? SEMICOLON ; -seqStmt - : (stmts+=stmt)* - ; +//seqStmt +// : +// ; assignStmt : lhs=ID ASSIGN value=expr SEMICOLON @@ -310,6 +315,22 @@ CHOICE : 'choice' ; +FOR + : 'for' + ; + +FROM + : 'from' + ; + +TO + : 'to' + ; + +DO + : 'do' + ; + NONDET_OR : 'or' ; diff --git a/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/XSTS.java b/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/XSTS.java index 446f7e92a9..3c0695f436 100644 --- a/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/XSTS.java +++ b/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/XSTS.java @@ -1,5 +1,6 @@ package hu.bme.mit.theta.xsts; +import hu.bme.mit.theta.common.container.Containers; import hu.bme.mit.theta.core.decl.VarDecl; import hu.bme.mit.theta.core.stmt.NonDetStmt; import hu.bme.mit.theta.core.type.Expr; @@ -55,7 +56,7 @@ public XSTS(final Map, XstsTypeDeclSymbol> varToType, final Set> tmpVars = new HashSet<>(); + final Set> tmpVars = Containers.createSet(); tmpVars.addAll(varToType.keySet()); tmpVars.addAll(StmtUtils.getVars(tran)); tmpVars.addAll(StmtUtils.getVars(env)); diff --git a/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/dsl/XstsSpecification.java b/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/dsl/XstsSpecification.java index dff61e390f..401e387f5a 100644 --- a/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/dsl/XstsSpecification.java +++ b/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/dsl/XstsSpecification.java @@ -1,5 +1,6 @@ package hu.bme.mit.theta.xsts.dsl; +import hu.bme.mit.theta.common.container.Containers; import hu.bme.mit.theta.common.dsl.*; import hu.bme.mit.theta.core.decl.VarDecl; import hu.bme.mit.theta.core.dsl.ParseException; @@ -45,8 +46,8 @@ public Optional resolve(String name) { public XSTS instantiate(){ final Env env = new Env(); - final Map, XstsTypeDeclSymbol> varToType = new HashMap<>(); - final Set> ctrlVars = new HashSet<>(); + final Map, XstsTypeDeclSymbol> varToType = Containers.createMap(); + final Set> ctrlVars = Containers.createSet(); final List> initExprs = new ArrayList<>(); for(var typeDeclContext: context.typeDeclarations){ diff --git a/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/dsl/XstsStatement.java b/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/dsl/XstsStatement.java index 63b4090beb..21c5eb4d3f 100644 --- a/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/dsl/XstsStatement.java +++ b/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/dsl/XstsStatement.java @@ -4,13 +4,12 @@ import hu.bme.mit.theta.core.decl.Decls; import hu.bme.mit.theta.core.decl.VarDecl; import hu.bme.mit.theta.core.dsl.DeclSymbol; -import hu.bme.mit.theta.core.stmt.NonDetStmt; -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.dsl.ParseException; +import hu.bme.mit.theta.core.stmt.*; 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 hu.bme.mit.theta.core.type.inttype.IntType; import hu.bme.mit.theta.core.utils.TypeUtils; import hu.bme.mit.theta.xsts.dsl.gen.XstsDslBaseVisitor; import hu.bme.mit.theta.xsts.dsl.gen.XstsDslParser.*; @@ -23,6 +22,8 @@ import static com.google.common.base.Preconditions.checkState; import static hu.bme.mit.theta.core.stmt.Stmts.*; import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Bool; +import static hu.bme.mit.theta.core.type.inttype.IntExprs.Int; +import static hu.bme.mit.theta.core.utils.TypeUtils.cast; public class XstsStatement { @@ -80,25 +81,30 @@ public Stmt visitHavocStmt(final HavocStmtContext ctx) { @Override public Stmt visitAssumeStmt(final AssumeStmtContext ctx) { final XstsExpression expression = new XstsExpression(currentScope, typeTable, ctx.cond); - final Expr expr = TypeUtils.cast(expression.instantiate(env), Bool()); + final Expr expr = cast(expression.instantiate(env), Bool()); return Assume(expr); } @Override public Stmt visitAssignStmt(final AssignStmtContext ctx) { - final String lhsId = ctx.lhs.getText(); - final Symbol lhsSymbol = currentScope.resolve(lhsId).get(); - final VarDecl var = (VarDecl) env.eval(lhsSymbol); + try{ + final String lhsId = ctx.lhs.getText(); + final Symbol lhsSymbol = currentScope.resolve(lhsId).get(); + final VarDecl var = (VarDecl) env.eval(lhsSymbol); - final XstsExpression expression = new XstsExpression(currentScope, typeTable, ctx.value); - final Expr expr = expression.instantiate(env); + final XstsExpression expression = new XstsExpression(currentScope, typeTable, ctx.value); + final Expr expr = expression.instantiate(env); - if (expr.getType().equals(var.getType())) { - @SuppressWarnings("unchecked") final VarDecl tVar = (VarDecl) var; - @SuppressWarnings("unchecked") final Expr tExpr = (Expr) expr; - return Assign(tVar, tExpr); - } else { - throw new IllegalArgumentException("Type of " + var + " is incompatilbe with " + expr); + if (expr.getType().equals(var.getType())) { + @SuppressWarnings("unchecked") final VarDecl tVar = (VarDecl) var; + @SuppressWarnings("unchecked") final Expr tExpr = (Expr) expr; + return Assign(tVar, tExpr); + } else { + throw new IllegalArgumentException("Type of " + var + " is incompatilbe with " + expr); + } + } + catch (Exception e){ + throw new ParseException(ctx,e.getMessage()); } } @@ -113,49 +119,66 @@ public Stmt visitNonDetStmt(NonDetStmtContext ctx) { } @Override - public Stmt visitSeqStmt(SeqStmtContext ctx) { - if(ctx.stmts.size()==0) return SkipStmt.getInstance(); - if(ctx.stmts.size()==1) return ctx.stmt.accept(this); + public Stmt visitLoopStmt(LoopStmtContext ctx) { + push(); - final List stmts = new ArrayList<>(); - for(var stmtCtx: ctx.stmts){ - final Stmt stmt = stmtCtx.accept(this); - stmts.add(stmt); - } - return SequenceStmt.of(stmts); + final String loopVarId = ctx.loopVar.getText(); + if(currentScope.resolve(loopVarId).isPresent()) throw new ParseException(ctx,String.format("Loop variable %s is already declared in this scope.",loopVarId)); + final var decl = Decls.Var(loopVarId,Int()); + final Symbol symbol = DeclSymbol.of(decl); + currentScope.declare(symbol); + env.define(symbol, decl); + final Expr from = cast(new XstsExpression(currentScope, typeTable, ctx.from).instantiate(env),Int()); + final Expr to = cast(new XstsExpression(currentScope, typeTable, ctx.to).instantiate(env),Int()); + final Stmt stmt = ctx.subStmt.accept(this); + + pop(); + + return LoopStmt.of(stmt,decl,from,to); } @Override public Stmt visitLocalVarDeclStmt(LocalVarDeclStmtContext ctx) { final String name = ctx.name.getText(); final Type type = new XstsType(typeTable,ctx.ttype).instantiate(env); - var decl = Decls.Var(name,type); - + final var decl = Decls.Var(name,type); final Symbol symbol = DeclSymbol.of(decl); - currentScope.declare(symbol); - env.define(symbol, decl); + + final Stmt result; if(ctx.initValue==null){ - return SkipStmt.getInstance(); + result = SkipStmt.getInstance(); } else { var expr = new XstsExpression(currentScope,typeTable,ctx.initValue).instantiate(env); if (expr.getType().equals(decl.getType())) { @SuppressWarnings("unchecked") final VarDecl tVar = (VarDecl) decl; @SuppressWarnings("unchecked") final Expr tExpr = (Expr) expr; - return Assign(tVar, tExpr); + result = Assign(tVar, tExpr); } else { throw new IllegalArgumentException("Type of " + decl + " is incompatilbe with " + expr); } } + + currentScope.declare(symbol); + env.define(symbol, decl); + + return result; } @Override public Stmt visitBlockStmt(BlockStmtContext ctx) { push(); - final Stmt subStmt = ctx.subStmt.accept(this); + if(ctx.stmts.size()==0) return SkipStmt.getInstance(); + if(ctx.stmts.size()==1) return ctx.stmt.accept(this); + + final List stmts = new ArrayList<>(); + for(var stmtCtx: ctx.stmts){ + final Stmt stmt = stmtCtx.accept(this); + stmts.add(stmt); + } pop(); - return subStmt; + return SequenceStmt.of(stmts); } } diff --git a/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/pnml/PnmlParser.java b/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/pnml/PnmlParser.java index b8f98e0771..918d73b72a 100644 --- a/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/pnml/PnmlParser.java +++ b/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/pnml/PnmlParser.java @@ -1,5 +1,6 @@ package hu.bme.mit.theta.xsts.pnml; +import hu.bme.mit.theta.common.container.Containers; import hu.bme.mit.theta.xsts.pnml.elements.*; import org.w3c.dom.Document; import org.w3c.dom.Element; @@ -47,7 +48,7 @@ public static PnmlNet parse(final String fileName, final String initialMarkingSt checkArgument(netList.getLength()==1,"Pnml model contains multiple nets"); final Element netElement = (Element) netList.item(0); - final Map idToNodeMap = new HashMap<>(); + final Map idToNodeMap = Containers.createMap(); final List places = new ArrayList<>(); final List transitions = new ArrayList<>(); @@ -119,7 +120,8 @@ public static PnmlNet parse(final String fileName, final String initialMarkingSt checkNotNull(source,"Target node not found of arc "+id); final XPathExpression toolspecificWeightExpr = xPath.compile("./toolspecific/weight/text()"); - final int weight = ((Double) toolspecificWeightExpr.evaluate(arcElement,XPathConstants.NUMBER)).intValue(); + final int toolspecificWeight = ((Double) toolspecificWeightExpr.evaluate(arcElement,XPathConstants.NUMBER)).intValue(); + final int weight = toolspecificWeight==0?1:toolspecificWeight; final PnmlArc arc = new PnmlArc(id,weight,source,target); source.addOutArc(arc); diff --git a/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/pnml/PnmlToXSTS.java b/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/pnml/PnmlToXSTS.java index 326f75911c..6664a3eb83 100644 --- a/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/pnml/PnmlToXSTS.java +++ b/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/pnml/PnmlToXSTS.java @@ -3,6 +3,7 @@ import com.google.common.collect.ImmutableList; import com.google.common.collect.ImmutableMap; import com.google.common.collect.ImmutableSet; +import hu.bme.mit.theta.common.container.Containers; import hu.bme.mit.theta.core.decl.Decls; import hu.bme.mit.theta.core.decl.VarDecl; import hu.bme.mit.theta.core.dsl.CoreDslManager; @@ -31,7 +32,7 @@ private PnmlToXSTS(){ } public static XSTS createXSTS(final PnmlNet net, final InputStream propStream){ - final Map> placeIdToVar = new HashMap<>(); + final Map> placeIdToVar = Containers.createMap(); final List> initExprs = new ArrayList<>(); // Create a variable for each place and initialize them diff --git a/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/lazy/ItpExplStrategy.java b/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/lazy/ItpExplStrategy.java index cf15f9a4ee..052de9165b 100644 --- a/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/lazy/ItpExplStrategy.java +++ b/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/lazy/ItpExplStrategy.java @@ -22,7 +22,7 @@ import static java.util.stream.Collectors.toList; import java.util.Collection; -import java.util.HashSet; +import hu.bme.mit.theta.common.container.Containers; import java.util.function.Function; import hu.bme.mit.theta.analysis.Analysis; @@ -106,7 +106,7 @@ protected final void strengthen(final ArgNode node, final Valuatio final ExplState concreteExpl = itpExplState.getConcrState(); final ExplState abstractExpl = itpExplState.getAbstrState(); - final Collection> newVars = new HashSet<>(); + final Collection> newVars = Containers.createSet(); newVars.addAll(interpolant.getDecls()); newVars.addAll(abstractExpl.getDecls()); final ImmutableValuation.Builder builder = ImmutableValuation.builder(); diff --git a/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/zone/XtaActZoneUtils.java b/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/zone/XtaActZoneUtils.java index f99791693b..cd5bb7f2bb 100644 --- a/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/zone/XtaActZoneUtils.java +++ b/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/zone/XtaActZoneUtils.java @@ -16,7 +16,7 @@ package hu.bme.mit.theta.xta.analysis.zone; import java.util.Collection; -import java.util.HashSet; +import hu.bme.mit.theta.common.container.Containers; import java.util.List; import java.util.Set; @@ -37,7 +37,7 @@ private XtaActZoneUtils() { } public static Set> pre(final Set> activeVars, final XtaAction action) { - final Set> result = new HashSet<>(); + final Set> result = Containers.createSet(); final List sourceLocs = action.getSourceLocs(); final List targetLocs = action.getTargetLocs(); diff --git a/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/zone/lu/LuZoneState.java b/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/zone/lu/LuZoneState.java index 238b7f4e76..32f8e57830 100644 --- a/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/zone/lu/LuZoneState.java +++ b/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/zone/lu/LuZoneState.java @@ -26,7 +26,7 @@ import java.util.ArrayList; import java.util.Collection; -import java.util.HashMap; +import hu.bme.mit.theta.common.container.Containers; import java.util.Map; import java.util.Optional; import java.util.StringJoiner; @@ -87,7 +87,7 @@ public Expr toExpr() { Expr result = expr; if (result == null) { // TODO create class for mapping - final Map, ParamDecl> mapping = new HashMap<>(); + final Map, ParamDecl> mapping = Containers.createMap(); final Expr zoneExpr = ExprUtils.close(zone.toExpr(), mapping); final Collection> conjuncts = new ArrayList<>(); diff --git a/subprojects/xta/xta/src/main/java/hu/bme/mit/theta/xta/XtaProcess.java b/subprojects/xta/xta/src/main/java/hu/bme/mit/theta/xta/XtaProcess.java index f6bbdfcb47..68fbf3072e 100644 --- a/subprojects/xta/xta/src/main/java/hu/bme/mit/theta/xta/XtaProcess.java +++ b/subprojects/xta/xta/src/main/java/hu/bme/mit/theta/xta/XtaProcess.java @@ -17,6 +17,7 @@ import com.google.common.collect.ImmutableList; import hu.bme.mit.theta.common.Utils; +import hu.bme.mit.theta.common.container.Containers; import hu.bme.mit.theta.core.decl.VarDecl; import hu.bme.mit.theta.core.stmt.Stmt; import hu.bme.mit.theta.core.type.Expr; @@ -44,7 +45,7 @@ public final class XtaProcess { private XtaProcess(final XtaSystem system, final String name) { this.system = checkNotNull(system); this.name = checkNotNull(name); - locs = new HashSet<>(); + locs = Containers.createSet(); edges = new ArrayList<>(); unmodLocs = Collections.unmodifiableCollection(locs); diff --git a/subprojects/xta/xta/src/main/java/hu/bme/mit/theta/xta/XtaSystem.java b/subprojects/xta/xta/src/main/java/hu/bme/mit/theta/xta/XtaSystem.java index 49317bf79e..94db2fca49 100644 --- a/subprojects/xta/xta/src/main/java/hu/bme/mit/theta/xta/XtaSystem.java +++ b/subprojects/xta/xta/src/main/java/hu/bme/mit/theta/xta/XtaSystem.java @@ -15,6 +15,7 @@ */ package hu.bme.mit.theta.xta; +import hu.bme.mit.theta.common.container.Containers; import hu.bme.mit.theta.core.decl.VarDecl; import hu.bme.mit.theta.core.model.MutableValuation; import hu.bme.mit.theta.core.model.Valuation; @@ -40,8 +41,8 @@ public final class XtaSystem { private XtaSystem() { processes = new ArrayList<>(); - dataVars = new HashSet<>(); - clockVars = new HashSet<>(); + dataVars = Containers.createSet(); + clockVars = Containers.createSet(); initVal = new MutableValuation(); unmodProcesses = Collections.unmodifiableList(processes); diff --git a/subprojects/xta/xta/src/main/java/hu/bme/mit/theta/xta/XtaVisualizer.java b/subprojects/xta/xta/src/main/java/hu/bme/mit/theta/xta/XtaVisualizer.java index 4e7fd3e993..938bd347ba 100644 --- a/subprojects/xta/xta/src/main/java/hu/bme/mit/theta/xta/XtaVisualizer.java +++ b/subprojects/xta/xta/src/main/java/hu/bme/mit/theta/xta/XtaVisualizer.java @@ -16,7 +16,7 @@ package hu.bme.mit.theta.xta; import java.awt.Color; -import java.util.HashMap; +import hu.bme.mit.theta.common.container.Containers; import java.util.Map; import java.util.StringJoiner; @@ -44,7 +44,7 @@ private XtaVisualizer() { public static Graph visualize(final XtaSystem system) { final Graph graph = new Graph("System", XTA_LABEL); - final Map ids = new HashMap<>(); + final Map ids = Containers.createMap(); for (final XtaProcess process : system.getProcesses()) { traverseProcess(process, graph, ids); } @@ -53,7 +53,7 @@ public static Graph visualize(final XtaSystem system) { public static Graph visualize(final XtaProcess process) { final Graph graph = new Graph(process.getName(), XTA_LABEL); - final Map ids = new HashMap<>(); + final Map ids = Containers.createMap(); traverseProcess(process, graph, ids); return graph; }