diff --git a/build.gradle.kts b/build.gradle.kts index 83a0f58034..fc78de175e 100644 --- a/build.gradle.kts +++ b/build.gradle.kts @@ -10,7 +10,7 @@ buildscript { allprojects { group = "hu.bme.mit.inf.theta" - version = "2.6.1" + version = "2.7.0" apply(from = rootDir.resolve("gradle/shared-with-buildSrc/mirrors.gradle.kts")) } diff --git a/subprojects/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/DistToErrComparator.java b/subprojects/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/DistToErrComparator.java index ae25849a1d..ed283affc8 100644 --- a/subprojects/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/DistToErrComparator.java +++ b/subprojects/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/DistToErrComparator.java @@ -41,13 +41,15 @@ public class DistToErrComparator implements ArgNodeComparator { private final int errorWeight; private final int depthWeight; private final CFA cfa; + private final Loc errLoc; - public DistToErrComparator(final CFA cfa) { - this(cfa, 1, 0); + public DistToErrComparator(final CFA cfa, final Loc errLoc) { + this(cfa, errLoc, 1, 0); } - public DistToErrComparator(final CFA cfa, final int errorWeight, final int depthWeight) { + public DistToErrComparator(final CFA cfa, final Loc errLoc, final int errorWeight, final int depthWeight) { this.cfa = cfa; + this.errLoc = errLoc; this.errorWeight = errorWeight; this.depthWeight = depthWeight; distancesToError = null; @@ -74,16 +76,16 @@ private int getWeightedDistance(final ArgNode private int getDistanceToError(final Loc loc) { if (distancesToError == null) { - distancesToError = calculateDistancesToError(cfa); + distancesToError = calculateDistancesToError(cfa, errLoc); } return distancesToError.getOrDefault(loc, Integer.MAX_VALUE); } - static Map calculateDistancesToError(final CFA cfa) { + static Map calculateDistancesToError(final CFA cfa, final Loc errLoc) { List queue = new LinkedList<>(); final Map distancesToError = new HashMap<>(); - queue.add(cfa.getErrorLoc()); - distancesToError.put(cfa.getErrorLoc(), 0); + queue.add(errLoc); + distancesToError.put(errLoc, 0); int distance = 1; while (!queue.isEmpty()) { diff --git a/subprojects/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/config/CfaConfigBuilder.java b/subprojects/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/config/CfaConfigBuilder.java index c86e2793a7..08ead09daf 100644 --- a/subprojects/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/config/CfaConfigBuilder.java +++ b/subprojects/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/config/CfaConfigBuilder.java @@ -74,26 +74,26 @@ public enum Refinement { public enum Search { BFS { @Override - public ArgNodeComparator getComp(final CFA cfa) { + public ArgNodeComparator getComp(final CFA cfa, final CFA.Loc errLoc) { return ArgNodeComparators.combine(ArgNodeComparators.targetFirst(), ArgNodeComparators.bfs()); } }, DFS { @Override - public ArgNodeComparator getComp(final CFA cfa) { + public ArgNodeComparator getComp(final CFA cfa, final CFA.Loc errLoc) { return ArgNodeComparators.combine(ArgNodeComparators.targetFirst(), ArgNodeComparators.dfs()); } }, ERR { @Override - public ArgNodeComparator getComp(final CFA cfa) { - return new DistToErrComparator(cfa); + public ArgNodeComparator getComp(final CFA cfa, final CFA.Loc errLoc) { + return new DistToErrComparator(cfa, errLoc); } }; - public abstract ArgNodeComparator getComp(CFA cfa); + public abstract ArgNodeComparator getComp(CFA cfa, CFA.Loc errLoc); } @@ -147,19 +147,19 @@ public abstract build(final CFA cfa) { + public CfaConfig build(final CFA cfa, final CFA.Loc errLoc) { final ItpSolver solver = solverFactory.createItpSolver(); - final CfaLts lts = encoding.getLts(); + final CfaLts lts = encoding.getLts(errLoc); if (domain == Domain.EXPL) { final Analysis, CfaAction, CfaPrec> analysis = CfaAnalysis .create(cfa.getInitLoc(), ExplStmtAnalysis.create(solver, True(), maxEnum)); final ArgBuilder, CfaAction, CfaPrec> argBuilder = ArgBuilder.create(lts, - analysis, s -> s.getLoc().equals(cfa.getErrorLoc()), true); + analysis, s -> s.getLoc().equals(errLoc), true); final Abstractor, CfaAction, CfaPrec> abstractor = BasicAbstractor .builder(argBuilder).projection(CfaState::getLoc) - .waitlist(PriorityWaitlist.create(search.getComp(cfa))) + .waitlist(PriorityWaitlist.create(search.getComp(cfa, errLoc))) .stopCriterion(refinement == Refinement.MULTI_SEQ ? StopCriterions.fullExploration() : StopCriterions.firstCex()).logger(logger).build(); @@ -372,10 +372,10 @@ public CfaConfigBuilder pruneStrategy(final PruneStrategy pruneStrategy) { final Analysis, CfaAction, CfaPrec> analysis = CfaAnalysis .create(cfa.getInitLoc(), PredAnalysis.create(solver, predAbstractor, True())); final ArgBuilder, CfaAction, CfaPrec> argBuilder = ArgBuilder.create(lts, - analysis, s -> s.getLoc().equals(cfa.getErrorLoc()), true); + analysis, s -> s.getLoc().equals(errLoc), true); final Abstractor, CfaAction, CfaPrec> abstractor = BasicAbstractor .builder(argBuilder).projection(CfaState::getLoc) - .waitlist(PriorityWaitlist.create(search.getComp(cfa))) + .waitlist(PriorityWaitlist.create(search.getComp(cfa, errLoc))) .stopCriterion(refinement == Refinement.MULTI_SEQ ? StopCriterions.fullExploration() : StopCriterions.firstCex()).logger(logger).build(); diff --git a/subprojects/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/lts/CfaLbeLts.java b/subprojects/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/lts/CfaLbeLts.java index 1cd8496dd1..d714732c2e 100644 --- a/subprojects/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/lts/CfaLbeLts.java +++ b/subprojects/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/lts/CfaLbeLts.java @@ -26,21 +26,22 @@ import hu.bme.mit.theta.cfa.analysis.CfaState; import hu.bme.mit.theta.common.Utils; +import static com.google.common.base.Preconditions.checkNotNull; + /** * Large block encoding (LBE) implementation for CFA LTS. It maps each path * (with no branching) into a single action. */ public final class CfaLbeLts implements CfaLts { - private static final class LazyHolder { - private static final CfaLbeLts INSTANCE = new CfaLbeLts(); - } + private final Loc targetLoc; - private CfaLbeLts() { + private CfaLbeLts(Loc targetLoc) { + this.targetLoc = checkNotNull(targetLoc, "Target location must be given for LBE encoder."); } - public static CfaLbeLts getInstance() { - return LazyHolder.INSTANCE; + public static CfaLbeLts of(Loc targetLoc) { + return new CfaLbeLts(targetLoc); } @Override @@ -52,7 +53,7 @@ public Collection getEnabledActionsFor(final CfaState state) { final List edges = new LinkedList<>(); edges.add(edge); Loc running = edge.getTarget(); - while (running.getInEdges().size() == 1 && running.getOutEdges().size() == 1) { + while (running.getInEdges().size() == 1 && running.getOutEdges().size() == 1 && !running.equals(targetLoc)) { final Edge next = Utils.singleElementOf(running.getOutEdges()); edges.add(next); running = next.getTarget(); diff --git a/subprojects/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/utils/CfaVisualizer.java b/subprojects/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/utils/CfaVisualizer.java index 94e27f7e15..139e0efa51 100644 --- a/subprojects/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/utils/CfaVisualizer.java +++ b/subprojects/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/utils/CfaVisualizer.java @@ -82,14 +82,15 @@ private static void addLocation(final Graph graph, final CFA cfa, final Loc loc, final String id = LOC_ID_PREFIX + ids.size(); ids.put(loc, id); String label = loc.getName(); + boolean isError = cfa.getErrorLoc().isPresent() && loc == cfa.getErrorLoc().get(); if (loc == cfa.getInitLoc()) { label += " (init)"; - } else if (loc == cfa.getFinalLoc()) { + } else if (cfa.getFinalLoc().isPresent() && loc == cfa.getFinalLoc().get()) { label += " (end)"; - } else if (loc == cfa.getErrorLoc()) { + } else if (isError) { label += " (error)"; } - final int peripheries = loc == cfa.getErrorLoc() ? 2 : 1; + final int peripheries = isError ? 2 : 1; final NodeAttributes nAttrs = NodeAttributes.builder().label(label).fillColor(FILL_COLOR).lineColor(LINE_COLOR) .lineStyle(LOC_LINE_STYLE).peripheries(peripheries).build(); graph.addNode(id, nAttrs); diff --git a/subprojects/cfa-analysis/src/test/java/hu/bme/mit/theta/cfa/analysis/CfaTest.java b/subprojects/cfa-analysis/src/test/java/hu/bme/mit/theta/cfa/analysis/CfaTest.java index 91c119306c..c30795f075 100644 --- a/subprojects/cfa-analysis/src/test/java/hu/bme/mit/theta/cfa/analysis/CfaTest.java +++ b/subprojects/cfa-analysis/src/test/java/hu/bme/mit/theta/cfa/analysis/CfaTest.java @@ -125,7 +125,7 @@ public static Collection data() { public void test() throws IOException { CFA cfa = CfaDslManager.createCfa(new FileInputStream(filePath)); CfaConfig config - = new CfaConfigBuilder(domain, refinement, Z3SolverFactory.getInstance()).build(cfa); + = new CfaConfigBuilder(domain, refinement, Z3SolverFactory.getInstance()).build(cfa, cfa.getErrorLoc().get()); SafetyResult result = config.check(); Assert.assertEquals(isSafe, result.isSafe()); if (result.isUnsafe()) { diff --git a/subprojects/cfa-analysis/src/test/java/hu/bme/mit/theta/cfa/analysis/DistanceToErrorLocComparatorTest.java b/subprojects/cfa-analysis/src/test/java/hu/bme/mit/theta/cfa/analysis/DistanceToErrorLocComparatorTest.java index aa280f08e0..0bc8c5e631 100644 --- a/subprojects/cfa-analysis/src/test/java/hu/bme/mit/theta/cfa/analysis/DistanceToErrorLocComparatorTest.java +++ b/subprojects/cfa-analysis/src/test/java/hu/bme/mit/theta/cfa/analysis/DistanceToErrorLocComparatorTest.java @@ -49,7 +49,7 @@ public void test() { builder.createEdge(loc2, locFinal, stmt); final CFA cfa = builder.build(); - final Map distancesToError = DistToErrComparator.calculateDistancesToError(cfa); + final Map distancesToError = DistToErrComparator.calculateDistancesToError(cfa, cfa.getErrorLoc().get()); Assert.assertEquals(0, (int) distancesToError.get(locErr)); Assert.assertEquals(2, (int) distancesToError.get(loc0)); diff --git a/subprojects/cfa-analysis/src/test/java/hu/bme/mit/theta/cfa/analysis/EncodingTest.java b/subprojects/cfa-analysis/src/test/java/hu/bme/mit/theta/cfa/analysis/EncodingTest.java new file mode 100644 index 0000000000..c90ec26889 --- /dev/null +++ b/subprojects/cfa-analysis/src/test/java/hu/bme/mit/theta/cfa/analysis/EncodingTest.java @@ -0,0 +1,98 @@ +package hu.bme.mit.theta.cfa.analysis; + +import com.google.common.collect.ImmutableSet; +import hu.bme.mit.theta.analysis.expr.ExprState; +import hu.bme.mit.theta.cfa.CFA; +import hu.bme.mit.theta.cfa.analysis.lts.CfaLbeLts; +import hu.bme.mit.theta.cfa.analysis.lts.CfaLts; +import hu.bme.mit.theta.cfa.analysis.lts.CfaSbeLts; +import hu.bme.mit.theta.cfa.dsl.CfaDslManager; +import hu.bme.mit.theta.core.type.Expr; +import hu.bme.mit.theta.core.type.booltype.BoolType; +import org.junit.Assert; +import org.junit.Before; +import org.junit.Test; + +import java.io.FileInputStream; +import java.io.IOException; +import java.util.HashSet; +import java.util.Set; + +public class EncodingTest { + + private CFA cfa; + + private CFA.Loc getLocByName(String name) { + for (CFA.Loc loc : cfa.getLocs()) { + if (loc.getName().equals(name)) return loc; + } + throw new IllegalArgumentException("Location not found"); + } + + private Set getNextLocs(CfaLts lts, String loc) { + Set locs = new HashSet<>(); + SS ss = new SS(); + for (var act : lts.getEnabledActionsFor(CfaState.of(getLocByName(loc), ss))) { + locs.add(act.getTarget().getName()); + } + return locs; + } + + private class SS implements ExprState { + @Override + public boolean isBottom() { + return false; + } + + @Override + public Expr toExpr() { + return null; + } + } + + @Before + public void load() throws IOException { + try (var fis = new FileInputStream("src/test/resources/block-encoding.cfa")) { + cfa = CfaDslManager.createCfa(fis); + } + } + + @Test + public void testSbe() { + CfaSbeLts lts = CfaSbeLts.getInstance(); + Assert.assertEquals(ImmutableSet.of("L1"), getNextLocs(lts, "L0")); + Assert.assertEquals(ImmutableSet.of("L2", "L4"), getNextLocs(lts, "L1")); + Assert.assertEquals(ImmutableSet.of("L3"), getNextLocs(lts, "L2")); + Assert.assertEquals(ImmutableSet.of("L4"), getNextLocs(lts, "L3")); + Assert.assertEquals(ImmutableSet.of("L5"), getNextLocs(lts, "L4")); + Assert.assertEquals(ImmutableSet.of("L1", "L6"), getNextLocs(lts, "L5")); + Assert.assertEquals(ImmutableSet.of("L7"), getNextLocs(lts, "L6")); + Assert.assertEquals(ImmutableSet.of(), getNextLocs(lts, "L7")); + } + + @Test + public void testLbe1() { + CfaLbeLts lts = CfaLbeLts.of(getLocByName("L7")); + Assert.assertEquals(ImmutableSet.of("L1"), getNextLocs(lts, "L0")); + Assert.assertEquals(ImmutableSet.of("L4"), getNextLocs(lts, "L1")); + Assert.assertEquals(ImmutableSet.of("L4"), getNextLocs(lts, "L2")); + Assert.assertEquals(ImmutableSet.of("L4"), getNextLocs(lts, "L3")); + Assert.assertEquals(ImmutableSet.of("L5"), getNextLocs(lts, "L4")); + Assert.assertEquals(ImmutableSet.of("L1", "L7"), getNextLocs(lts, "L5")); + Assert.assertEquals(ImmutableSet.of("L7"), getNextLocs(lts, "L6")); + Assert.assertEquals(ImmutableSet.of(), getNextLocs(lts, "L7")); + } + + @Test + public void testLbe2() { + CfaLbeLts lts = CfaLbeLts.of(getLocByName("L3")); + Assert.assertEquals(ImmutableSet.of("L1"), getNextLocs(lts, "L0")); + Assert.assertEquals(ImmutableSet.of("L3", "L4"), getNextLocs(lts, "L1")); + Assert.assertEquals(ImmutableSet.of("L3"), getNextLocs(lts, "L2")); + Assert.assertEquals(ImmutableSet.of("L4"), getNextLocs(lts, "L3")); + Assert.assertEquals(ImmutableSet.of("L5"), getNextLocs(lts, "L4")); + Assert.assertEquals(ImmutableSet.of("L1", "L7"), getNextLocs(lts, "L5")); + Assert.assertEquals(ImmutableSet.of("L7"), getNextLocs(lts, "L6")); + Assert.assertEquals(ImmutableSet.of(), getNextLocs(lts, "L7")); + } +} diff --git a/subprojects/cfa-analysis/src/test/java/hu/bme/mit/theta/cfa/analysis/impact/CfaPredImpactCheckerTest.java b/subprojects/cfa-analysis/src/test/java/hu/bme/mit/theta/cfa/analysis/impact/CfaPredImpactCheckerTest.java index ebffd1ac6c..6bf6f0275e 100644 --- a/subprojects/cfa-analysis/src/test/java/hu/bme/mit/theta/cfa/analysis/impact/CfaPredImpactCheckerTest.java +++ b/subprojects/cfa-analysis/src/test/java/hu/bme/mit/theta/cfa/analysis/impact/CfaPredImpactCheckerTest.java @@ -46,8 +46,8 @@ public void test() throws FileNotFoundException, IOException { final ItpSolver solver = Z3SolverFactory.getInstance().createItpSolver(); - final PredImpactChecker checker = PredImpactChecker.create(CfaLbeLts.getInstance(), cfa.getInitLoc(), - l -> l.equals(cfa.getErrorLoc()), solver); + final PredImpactChecker checker = PredImpactChecker.create(CfaLbeLts.of(cfa.getErrorLoc().get()), cfa.getInitLoc(), + l -> l.equals(cfa.getErrorLoc().get()), solver); // Act final SafetyResult status = checker.check(UnitPrec.getInstance()); diff --git a/subprojects/cfa-analysis/src/test/resources/block-encoding.cfa b/subprojects/cfa-analysis/src/test/resources/block-encoding.cfa new file mode 100644 index 0000000000..b4d142f397 --- /dev/null +++ b/subprojects/cfa-analysis/src/test/resources/block-encoding.cfa @@ -0,0 +1,20 @@ +main process cfa { + init loc L0 + loc L1 + loc L2 + loc L3 + loc L4 + loc L5 + loc L6 + loc L7 + + L0 -> L1 { } + L1 -> L2 { } + L2 -> L3 { } + L3 -> L4 { } + L1 -> L4 { } + L4 -> L5 { } + L5 -> L6 { } + L6 -> L7 { } + L5 -> L1 { } +} \ No newline at end of file diff --git a/subprojects/cfa-cli/README.md b/subprojects/cfa-cli/README.md index 0e23bab5ef..95f1e5d6a9 100644 --- a/subprojects/cfa-cli/README.md +++ b/subprojects/cfa-cli/README.md @@ -1,6 +1,6 @@ ## Overview -The `cfa-cli` project is an executable (command line) tool for running CEGAR-based analyses on CFAs. +The `cfa-cli` project is an executable (command line) tool for running CEGAR-based location-reachability analyses on CFAs. Furthermore, it also includes some utilities, such as calculating metrics or visualizing the CFA. For more information about the CFA formalism and its supported language elements, take a look at the [`cfa`](../cfa/README.md) project. @@ -46,6 +46,7 @@ Note that the model must be given as the first positional argument (without `--m All arguments are optional, except `--model`. * `--model`: Path of the input CFA model (mandatory). +* `--errorloc`: Name of the error (target) location in the CFA, which is checked for reachability. The CFA is safe if the error location is not reachable, and unsafe otherwise. This argument can be omitted if a location in the CFA is marked with the error keyword. If there is an error location marked in the CFA and this argument is also given, the argument has priority. * `--cex`: Output file where the counterexample is written (if the result is unsafe). If the argument is not given (default) the counterexample is not printed. Use `CON` (Windows) or `/dev/stdout` (Linux) as argument to print to the standard output. * `--loglevel`: Detailedness of logging. * Possible values (from the least to the most detailed): `RESULT`, `MAINSTEP`, `SUBSTEP` (default), `INFO`, `DETAIL`, `VERBOSE`. diff --git a/subprojects/cfa-cli/src/main/java/hu/bme/mit/theta/cfa/cli/CfaCli.java b/subprojects/cfa-cli/src/main/java/hu/bme/mit/theta/cfa/cli/CfaCli.java index f79d22b568..12fdb42ade 100644 --- a/subprojects/cfa-cli/src/main/java/hu/bme/mit/theta/cfa/cli/CfaCli.java +++ b/subprojects/cfa-cli/src/main/java/hu/bme/mit/theta/cfa/cli/CfaCli.java @@ -15,7 +15,12 @@ */ package hu.bme.mit.theta.cfa.cli; -import java.io.*; +import java.io.File; +import java.io.FileInputStream; +import java.io.FileNotFoundException; +import java.io.InputStream; +import java.io.PrintWriter; +import java.io.StringWriter; import java.util.concurrent.TimeUnit; import java.util.stream.Stream; @@ -54,8 +59,9 @@ 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.*; -import hu.bme.mit.theta.solver.z3.*; +import hu.bme.mit.theta.solver.z3.Z3SolverFactory; + +import static com.google.common.base.Preconditions.checkNotNull; /** * A command line interface for running a CEGAR configuration on a CFA. @@ -80,6 +86,9 @@ public class CfaCli { @Parameter(names = "--model", description = "Path of the input CFA model", required = true) String model; + @Parameter(names = "--errorloc", description = "Error (target) location") + String errorLoc = ""; + @Parameter(names = "--precgranularity", description = "Precision granularity") PrecGranularity precGranularity = PrecGranularity.GLOBAL; @@ -167,7 +176,22 @@ private void run() { return; } - final CfaConfig configuration = buildConfiguration(cfa); + CFA.Loc errLoc = null; + if (cfa.getErrorLoc().isPresent()) { + errLoc = cfa.getErrorLoc().get(); + } + if (!errorLoc.isEmpty()) { + errLoc = null; + for (CFA.Loc running : cfa.getLocs()) { + if (running.getName().equals(errorLoc)) { + errLoc = running; + } + } + checkNotNull(errLoc, "Location '" + errorLoc + "' not found in CFA"); + } + + checkNotNull(errLoc, "Error location must be specified in CFA or as argument"); + final CfaConfig configuration = buildConfiguration(cfa, errLoc); final SafetyResult status = check(configuration); sw.stop(); printResult(status, sw.elapsed(TimeUnit.MILLISECONDS)); @@ -196,12 +220,12 @@ private CFA loadModel() throws Exception { } } - private CfaConfig buildConfiguration(final CFA cfa) throws Exception { + private CfaConfig buildConfiguration(final CFA cfa, final CFA.Loc errLoc) throws Exception { try { return new CfaConfigBuilder(domain, refinement, Z3SolverFactory.getInstance()) .precGranularity(precGranularity).search(search) .predSplit(predSplit).encoding(encoding).maxEnum(maxEnum).initPrec(initPrec) - .pruneStrategy(pruneStrategy).logger(logger).build(cfa); + .pruneStrategy(pruneStrategy).logger(logger).build(cfa, errLoc); } catch (final Exception ex) { throw new Exception("Could not create configuration: " + ex.getMessage(), ex); } diff --git a/subprojects/cfa/README.md b/subprojects/cfa/README.md index 634be359a4..a6aba8f3e0 100644 --- a/subprojects/cfa/README.md +++ b/subprojects/cfa/README.md @@ -15,7 +15,7 @@ The project contains: A CFA is a directed graph (`V`, `L`, `E`) with * variables `V = {v1, v2, ..., vn}`, -* locations `L`, with dedicated initial (`l0`), final (`lf`) and error (`le`) locations, +* locations `L`, with a dedicated initial (`l0`) location and optionally with dedicated final (`lf`) and error (`le`) locations, * edges `E` between locations, labeled with statements over the variables. Currently, there are three kind of supported statements. @@ -30,7 +30,7 @@ After the assumption, variables are unchanged. After performing the havoc, `v` is assigned a non-deterministic value. This can be used to simulate non-deterministic input from the user or the environment. -Algorithms are usually interested in proving that the error location is not reachable. +Algorithms are usually interested in proving that the error location (given in the CFA or as a separate argument) is not reachable. For more information see Section 2.1 of [our JAR paper](https://link.springer.com/content/pdf/10.1007%2Fs10817-019-09535-x.pdf). Variables of the CFA can have the following types. diff --git a/subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/CFA.java b/subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/CFA.java index c9c70d24ab..387b73ae06 100644 --- a/subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/CFA.java +++ b/subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/CFA.java @@ -21,10 +21,7 @@ import static com.google.common.collect.ImmutableSet.toImmutableSet; import static java.lang.String.format; -import java.util.Collection; -import java.util.Collections; -import java.util.HashSet; -import java.util.LinkedList; +import java.util.*; import com.google.common.collect.ImmutableList; import com.google.common.collect.ImmutableSet; @@ -41,8 +38,8 @@ public final class CFA { private final Loc initLoc; - private final Loc finalLoc; - private final Loc errorLoc; + private final Optional finalLoc; + private final Optional errorLoc; private final Collection> vars; private final Collection locs; @@ -50,8 +47,8 @@ public final class CFA { private CFA(final Builder builder) { initLoc = builder.initLoc; - finalLoc = builder.finalLoc; - errorLoc = builder.errorLoc; + finalLoc = Optional.ofNullable(builder.finalLoc); + errorLoc = Optional.ofNullable(builder.errorLoc); locs = ImmutableSet.copyOf(builder.locs); edges = ImmutableList.copyOf(builder.edges); vars = edges.stream().flatMap(e -> StmtUtils.getVars(e.getStmt()).stream()).collect(toImmutableSet()); @@ -61,11 +58,11 @@ public Loc getInitLoc() { return initLoc; } - public Loc getFinalLoc() { + public Optional getFinalLoc() { return finalLoc; } - public Loc getErrorLoc() { + public Optional getErrorLoc() { return errorLoc; } @@ -97,9 +94,9 @@ public String toString() { private String locToString(final Loc loc) { if (initLoc.equals(loc)) { return format("(init %s)", loc.getName()); - } else if (finalLoc.equals(loc)) { + } else if (finalLoc.isPresent() && finalLoc.get().equals(loc)) { return format("(final %s)", loc.getName()); - } else if (errorLoc.equals(loc)) { + } else if (errorLoc.isPresent() && errorLoc.get().equals(loc)) { return format("(error %s)", loc.getName()); } else { return format("(loc %s)", loc.getName()); @@ -244,10 +241,10 @@ public Edge createEdge(final Loc source, final Loc target, final Stmt stmt) { public CFA build() { checkState(initLoc != null, "Initial location must be set."); - checkState(finalLoc != null, "Final location must be set."); - checkState(errorLoc != null, "Error location must be set."); - checkState(finalLoc.getOutEdges().isEmpty(), "Final location cannot have outgoing edges."); - checkState(errorLoc.getOutEdges().isEmpty(), "Error location cannot have outgoing edges."); + if (finalLoc != null) + checkState(finalLoc.getOutEdges().isEmpty(), "Final location cannot have outgoing edges."); + if (errorLoc != null) + checkState(errorLoc.getOutEdges().isEmpty(), "Error location cannot have outgoing edges."); built = true; return new CFA(this); } diff --git a/subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/dsl/CfaProcessSymbol.java b/subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/dsl/CfaProcessSymbol.java index 8ec07b6423..5fd0df4709 100644 --- a/subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/dsl/CfaProcessSymbol.java +++ b/subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/dsl/CfaProcessSymbol.java @@ -147,9 +147,9 @@ private List createLocations(final List locContex result.add(symbol); } - checkArgument(nInitLocs == 1, "Exactly one initial location must be specififed"); - checkArgument(nFinalLocs == 1, "Exactly one final location must be specififed"); - checkArgument(nErrorLocs == 1, "Exactly one error location must be specififed"); + checkArgument(nInitLocs == 1, "Exactly one initial location must be specified"); + checkArgument(nFinalLocs <= 1, "At most one final location must be specified"); + checkArgument(nErrorLocs <= 1, "At most one error location must be specified"); return result; } diff --git a/subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/dsl/CfaWriter.java b/subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/dsl/CfaWriter.java index d004e6536b..9a37726f2c 100644 --- a/subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/dsl/CfaWriter.java +++ b/subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/dsl/CfaWriter.java @@ -50,13 +50,13 @@ public static void write(final CFA cfa, final OutputStream outStream) throws IOE for (final Loc loc : cfa.getLocs()) { final String locName = "L" + loc.getName(); String locPrefix = ""; - if (loc == cfa.getErrorLoc()) { + if (cfa.getErrorLoc().isPresent() && loc == cfa.getErrorLoc().get()) { locPrefix += "error "; } if (loc == cfa.getInitLoc()) { locPrefix += "init "; } - if (loc == cfa.getFinalLoc()) { + if (cfa.getFinalLoc().isPresent() && loc == cfa.getFinalLoc().get()) { locPrefix += "final "; } bw.write(String.format("\t%sloc %s", locPrefix, locName));