Merge pull request ftsrg#281 from ftsrg/zeta-merge

MDD-based analysis
RipplB · Jul 12, 2024 · d825dc1 · d825dc1
2 parents 081d68e + 3a80d94
commit d825dc1
Show file tree

Hide file tree

Showing 250 changed files with 30,445 additions and 1,174 deletions.
diff --git a/build.gradle.kts b/build.gradle.kts
@@ -28,7 +28,7 @@ buildscript {
 
 allprojects {
     group = "hu.bme.mit.theta"
-    version = "5.4.0"
+    version = "6.0.0"
 
     apply(from = rootDir.resolve("gradle/shared-with-buildSrc/mirrors.gradle.kts"))
 }

diff --git a/buildSrc/gradle.properties b/buildSrc/gradle.properties
@@ -25,6 +25,16 @@ junitVersion=5.9.3
 junit4Version=4.12
 jacocoVersion=0.8.8
 mockitoVersion=2.2.11
+pnmlFrameworkVersion=2.2.12
+emfCommonVersion=2.10.1
+emfCodegenVersion=2.10.0
+emfCodegenEcoreVersion=2.10.2-v20150123-0452
+emfEcoreVersion=2.10.2-v20150123-0348
+axiomVersion=1.2.20
+jingVersion=20091111
+kolobokeVersion=1.0.0
+deltaVersion=0.0.1
+deltaCollectionsVersion=0.0.1
 gsonVersion=2.9.1
 javasmtVersion=4.1.1
 sosylabVersion=0.3000-569-g89796f98
diff --git a/buildSrc/src/main/kotlin/Deps.kt b/buildSrc/src/main/kotlin/Deps.kt
@@ -36,6 +36,29 @@ object Deps {
 
     val jcommander = "com.beust:jcommander:${Versions.jcommander}"
 
+    val pnmlCore = "fr.lip6.pnml:fr.lip6.pnml.framework.coremodel:${Versions.pnmlFramework}"
+    val pnmlPtnet = "fr.lip6.pnml:fr.lip6.pnml.framework.ptnet:${Versions.pnmlFramework}"
+    val pnmlSymmetric = "fr.lip6.pnml:fr.lip6.pnml.framework.symmetricnet:${Versions.pnmlFramework}"
+    val pnmlHlpn = "fr.lip6.pnml:fr.lip6.pnml.framework.hlpn:${Versions.pnmlFramework}"
+    val pnmlPthlpng = "fr.lip6.pnml:fr.lip6.pnml.framework.pthlpng:${Versions.pnmlFramework}"
+    val pnmlUtils = "fr.lip6.pnml:fr.lip6.pnml.framework.utils:${Versions.pnmlFramework}"
+    val pnmlNupn = "fr.lip6.pnml:fr.lip6.pnml.nupn.toolinfo:${Versions.pnmlFramework}"
+
+    val emfCommon = "org.eclipse.emf:org.eclipse.emf.common:${Versions.emfCommon}"
+    val emfCodegen = "org.eclipse.emf:org.eclipse.emf.codegen:${Versions.emfCodegen}"
+    val emfCodegenEcore = "org.eclipse.emf:org.eclipse.emf.codegen.ecore:${Versions.emfCodegenEcore}"
+    val emfEcore = "org.eclipse.emf:org.eclipse.emf.ecore:${Versions.emfEcore}"
+    val emfEcoreXmi = "org.eclipse.emf:org.eclipse.emf.ecore.xmi:${Versions.emfEcore}"
+
+    val axiomApi = "org.apache.ws.commons.axiom:axiom-api:${Versions.axiom}"
+    val axiomImpl = "org.apache.ws.commons.axiom:axiom-impl:${Versions.axiom}"
+    val jing = "com.thaiopensource:jing:${Versions.jing}"
+
+    val delta = "lib/hu.bme.mit.delta"
+    val deltaCollections = "lib/hu.bme.mit.delta.collections:${Versions.deltaCollections}"
+
+    val koloboke = "com.koloboke:koloboke-api-jdk8:${Versions.koloboke}"
+
     val junit4 = "junit:junit:${Versions.junit4}"
     val junit4engine = "org.junit.vintage:junit-vintage-engine"
     val junit5 = "org.junit.jupiter:junit-jupiter-api:${Versions.junit}"

diff --git a/buildSrc/src/main/kotlin/java-common.gradle.kts b/buildSrc/src/main/kotlin/java-common.gradle.kts
@@ -47,6 +47,7 @@ tasks {
     withType<Test>() {
         environment["PATH"] = execPath
         environment["LD_LIBRARY_PATH"] = libPath
+        enableAssertions = true
     }
 
     named("jacocoTestReport") {

diff --git a/lib/hu.bme.mit.delta-0.0.1-all.jar b/lib/hu.bme.mit.delta-0.0.1-all.jar
diff --git a/settings.gradle.kts b/settings.gradle.kts
@@ -23,6 +23,9 @@ include(
     "common/multi-tests",
 
     "frontends/c-frontend",
+    "frontends/petrinet-frontend/petrinet-model",
+    "frontends/petrinet-frontend/petrinet-analysis",
+    "frontends/petrinet-frontend/petrinet-xsts",
     "frontends/chc-frontend",
     "frontends/llvm",
 

diff --git a/subprojects/cfa/cfa-analysis/README.md b/subprojects/cfa/cfa-analysis/README.md
@@ -1,9 +1,11 @@
 ## Overview
 
-This project contains analysis modules related to the Control Flow Automata (CFA) formalism. Its main purpose is to enable the algorithms to operate over CFA models.
+This project contains analysis modules related to the Control Flow Automata (CFA) formalism. Its
+main purpose is to enable the algorithms to operate over CFA models.
 
 ### Related projects
 
 * [`analysis`](../../common/analysis/README.md): Common analysis modules.
-* [`cfa`](../cfa/README.md): Classes to represent CFAs and a domain specific language (DSL) to parse CFAs from a textual representation.
+* [`cfa`](../cfa/README.md): Classes to represent CFAs and a domain specific language (DSL) to parse
+  CFAs from a textual representation.
 * [`cfa-cli`](../cfa-cli/README.md): An executable tool (command line) for running analyses on CFAs.
diff --git a/...cts/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/DistToErrComparator.java b/...cts/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/DistToErrComparator.java
@@ -25,8 +25,8 @@
 
 import hu.bme.mit.theta.analysis.Action;
 import hu.bme.mit.theta.analysis.State;
-import hu.bme.mit.theta.analysis.algorithm.ArgNode;
-import hu.bme.mit.theta.analysis.algorithm.ArgNodeComparators.ArgNodeComparator;
+import hu.bme.mit.theta.analysis.algorithm.arg.ArgNode;
+import hu.bme.mit.theta.analysis.algorithm.arg.ArgNodeComparators.ArgNodeComparator;
 import hu.bme.mit.theta.cfa.CFA;
 import hu.bme.mit.theta.cfa.CFA.Edge;
 import hu.bme.mit.theta.cfa.CFA.Loc;

diff --git a/...ojects/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/config/CfaConfig.java b/...ojects/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/config/CfaConfig.java
@@ -15,28 +15,27 @@
  */
 package hu.bme.mit.theta.cfa.analysis.config;
 
-import hu.bme.mit.theta.analysis.Action;
-import hu.bme.mit.theta.analysis.Prec;
-import hu.bme.mit.theta.analysis.State;
+import hu.bme.mit.theta.analysis.*;
 import hu.bme.mit.theta.analysis.algorithm.SafetyChecker;
 import hu.bme.mit.theta.analysis.algorithm.SafetyResult;
+import hu.bme.mit.theta.analysis.algorithm.arg.ARG;
 
 public final class CfaConfig<S extends State, A extends Action, P extends Prec> {
 
-    private final SafetyChecker<S, A, P> checker;
+    private final SafetyChecker<ARG<S, A>, Trace<S, A>, P> checker;
     private final P initPrec;
 
-    private CfaConfig(final SafetyChecker<S, A, P> checker, final P initPrec) {
+    private CfaConfig(final SafetyChecker<ARG<S, A>, Trace<S, A>, P> checker, final P initPrec) {
         this.checker = checker;
         this.initPrec = initPrec;
     }
 
     public static <S extends State, A extends Action, P extends Prec> CfaConfig<S, A, P> create(
-            final SafetyChecker<S, A, P> checker, final P initPrec) {
+            final SafetyChecker<ARG<S, A>, Trace<S, A>, P> checker, final P initPrec) {
         return new CfaConfig<>(checker, initPrec);
     }
 
-    public SafetyResult<S, A> check() {
+    public SafetyResult<ARG<S, A>, Trace<S, A>> check() {
         return checker.check(initPrec);
     }
 

diff --git a/...cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/config/CfaConfigBuilder.java b/...cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/config/CfaConfigBuilder.java
@@ -15,13 +15,11 @@
  */
 package hu.bme.mit.theta.cfa.analysis.config;
 
-import hu.bme.mit.theta.analysis.Action;
-import hu.bme.mit.theta.analysis.Analysis;
-import hu.bme.mit.theta.analysis.Prec;
-import hu.bme.mit.theta.analysis.State;
-import hu.bme.mit.theta.analysis.algorithm.ArgBuilder;
-import hu.bme.mit.theta.analysis.algorithm.ArgNodeComparators;
-import hu.bme.mit.theta.analysis.algorithm.ArgNodeComparators.ArgNodeComparator;
+import hu.bme.mit.theta.analysis.*;
+import hu.bme.mit.theta.analysis.algorithm.arg.ARG;
+import hu.bme.mit.theta.analysis.algorithm.arg.ArgBuilder;
+import hu.bme.mit.theta.analysis.algorithm.arg.ArgNodeComparators;
+import hu.bme.mit.theta.analysis.algorithm.arg.ArgNodeComparators.ArgNodeComparator;
 import hu.bme.mit.theta.analysis.algorithm.SafetyChecker;
 import hu.bme.mit.theta.analysis.algorithm.cegar.Abstractor;
 import hu.bme.mit.theta.analysis.algorithm.cegar.BasicAbstractor;
@@ -431,7 +429,7 @@ public CfaConfig<CfaState<S>, CfaAction, CfaPrec<P>> buildConfig(CFA.Loc errLoc)
                     .stopCriterion(refinement.getStopCriterion())
                     .logger(logger).build();
             final Refiner<CfaState<S>, CfaAction, CfaPrec<P>> refiner = refinement.getRefiner(this);
-            final SafetyChecker<CfaState<S>, CfaAction, CfaPrec<P>> checker = CegarChecker.create(
+            final SafetyChecker<ARG<CfaState<S>, CfaAction>, Trace<CfaState<S>, CfaAction>, CfaPrec<P>> checker = CegarChecker.create(
                     abstractor, refiner,
                     logger);
             return CfaConfig.create(checker, createInitPrec());

diff --git a/...ts/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/impact/ImpactChecker.java b/...ts/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/impact/ImpactChecker.java
@@ -24,18 +24,18 @@
 import hu.bme.mit.theta.analysis.Prec;
 import hu.bme.mit.theta.analysis.State;
 import hu.bme.mit.theta.analysis.Trace;
-import hu.bme.mit.theta.analysis.algorithm.ARG;
-import hu.bme.mit.theta.analysis.algorithm.ArgBuilder;
-import hu.bme.mit.theta.analysis.algorithm.ArgNode;
-import hu.bme.mit.theta.analysis.algorithm.ArgTrace;
-import hu.bme.mit.theta.analysis.algorithm.SafetyChecker;
 import hu.bme.mit.theta.analysis.algorithm.SafetyResult;
+import hu.bme.mit.theta.analysis.algorithm.arg.ARG;
+import hu.bme.mit.theta.analysis.algorithm.arg.ArgBuilder;
+import hu.bme.mit.theta.analysis.algorithm.arg.ArgNode;
+import hu.bme.mit.theta.analysis.algorithm.arg.ArgTrace;
+import hu.bme.mit.theta.analysis.algorithm.SafetyChecker;
 import hu.bme.mit.theta.analysis.reachedset.ReachedSet;
 import hu.bme.mit.theta.analysis.waitlist.FifoWaitlist;
 import hu.bme.mit.theta.analysis.waitlist.Waitlist;
 
 public final class ImpactChecker<S extends State, A extends Action, P extends Prec> implements
-        SafetyChecker<S, A, P> {
+        SafetyChecker<ARG<S, A>, Trace<S, A>, P> {
 
     private final ArgBuilder<S, A, P> argBuilder;
     private final ImpactRefiner<S, A> refiner;
@@ -57,7 +57,7 @@ public static <S extends State, A extends Action, P extends Prec> ImpactChecker<
     ////
 
     @Override
-    public SafetyResult<S, A> check(final P prec) {
+    public SafetyResult<ARG<S, A>, Trace<S, A>> check(final P prec) {
         return new CheckMethod(prec).run();
     }
 
@@ -76,7 +76,7 @@ private CheckMethod(final P prec) {
             reachedSet = ImpactReachedSet.create(partitioning);
         }
 
-        private SafetyResult<S, A> run() {
+        private SafetyResult<ARG<S, A>, Trace<S, A>> run() {
             final Optional<ArgNode<S, A>> unsafeNode = unwind();
 
             if (unsafeNode.isPresent()) {

diff --git a/...cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/impact/ImpactReachedSet.java b/...cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/impact/ImpactReachedSet.java
@@ -29,7 +29,7 @@
 
 import hu.bme.mit.theta.analysis.Action;
 import hu.bme.mit.theta.analysis.State;
-import hu.bme.mit.theta.analysis.algorithm.ArgNode;
+import hu.bme.mit.theta.analysis.algorithm.arg.ArgNode;
 import hu.bme.mit.theta.analysis.reachedset.ReachedSet;
 
 public final class ImpactReachedSet<S extends State, A extends Action, K> implements

diff --git a/...fa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/impact/PredImpactChecker.java b/...fa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/impact/PredImpactChecker.java
@@ -17,9 +17,11 @@
 
 import hu.bme.mit.theta.analysis.Analysis;
 import hu.bme.mit.theta.analysis.LTS;
-import hu.bme.mit.theta.analysis.algorithm.ArgBuilder;
+import hu.bme.mit.theta.analysis.Trace;
 import hu.bme.mit.theta.analysis.algorithm.SafetyChecker;
 import hu.bme.mit.theta.analysis.algorithm.SafetyResult;
+import hu.bme.mit.theta.analysis.algorithm.arg.ARG;
+import hu.bme.mit.theta.analysis.algorithm.arg.ArgBuilder;
 import hu.bme.mit.theta.analysis.expr.ExprAction;
 import hu.bme.mit.theta.analysis.impl.PrecMappingAnalysis;
 import hu.bme.mit.theta.analysis.pred.PredAbstractors;
@@ -42,7 +44,7 @@
 import static hu.bme.mit.theta.core.type.booltype.BoolExprs.True;
 import static java.util.Collections.emptySet;
 
-public final class PredImpactChecker implements SafetyChecker<CfaState<PredState>, CfaAction, UnitPrec> {
+public final class PredImpactChecker implements SafetyChecker<ARG<CfaState<PredState>, CfaAction>, Trace<CfaState<PredState>, CfaAction>, UnitPrec> {
 
     private final ImpactChecker<CfaState<PredState>, CfaAction, UnitPrec> checker;
 
@@ -82,7 +84,7 @@ public static PredImpactChecker create(final LTS<? super CfaState<PredState>, Cf
     }
 
     @Override
-    public SafetyResult<CfaState<PredState>, CfaAction> check(final UnitPrec prec) {
+    public SafetyResult<ARG<CfaState<PredState>, CfaAction>, Trace<CfaState<PredState>, CfaAction>> check(final UnitPrec prec) {
         return checker.check(prec);
     }
 

diff --git a/subprojects/cfa/cfa-analysis/src/test/java/hu/bme/mit/theta/cfa/analysis/CfaTest.java b/subprojects/cfa/cfa-analysis/src/test/java/hu/bme/mit/theta/cfa/analysis/CfaTest.java
@@ -20,6 +20,7 @@
 import hu.bme.mit.theta.analysis.State;
 import hu.bme.mit.theta.analysis.Trace;
 import hu.bme.mit.theta.analysis.algorithm.SafetyResult;
+import hu.bme.mit.theta.analysis.algorithm.arg.ARG;
 import hu.bme.mit.theta.analysis.expl.ExplState;
 import hu.bme.mit.theta.cfa.CFA;
 import hu.bme.mit.theta.cfa.analysis.config.CfaConfig;
@@ -172,11 +173,11 @@ public void test() throws Exception {
             CfaConfig<? extends State, ? extends Action, ? extends Prec> config
                     = new CfaConfigBuilder(domain, refinement, solverFactory).build(cfa,
                     cfa.getErrorLoc().get());
-            SafetyResult<? extends State, ? extends Action> result = config.check();
+            SafetyResult<?, ?> result = config.check();
             Assert.assertEquals(isSafe, result.isSafe());
             if (result.isUnsafe()) {
                 Trace<CfaState<ExplState>, CfaAction> trace = CfaTraceConcretizer.concretize(
-                        (Trace<CfaState<?>, CfaAction>) result.asUnsafe().getTrace(),
+                        (Trace<CfaState<?>, CfaAction>) result.asUnsafe().getCex(),
                         solverFactory);
                 Assert.assertEquals(cexLength, trace.length());
             }

diff --git a/...analysis/src/test/java/hu/bme/mit/theta/cfa/analysis/impact/CfaPredImpactCheckerTest.java b/...analysis/src/test/java/hu/bme/mit/theta/cfa/analysis/impact/CfaPredImpactCheckerTest.java
@@ -21,12 +21,16 @@
 import java.io.FileNotFoundException;
 import java.io.IOException;
 
+import hu.bme.mit.theta.analysis.Trace;
+import hu.bme.mit.theta.analysis.algorithm.SafetyResult;
+import hu.bme.mit.theta.analysis.pred.PredState;
+import hu.bme.mit.theta.cfa.analysis.CfaAction;
+import hu.bme.mit.theta.cfa.analysis.CfaState;
 import hu.bme.mit.theta.solver.Solver;
 import org.junit.Test;
 
-import hu.bme.mit.theta.analysis.algorithm.ARG;
-import hu.bme.mit.theta.analysis.algorithm.ArgChecker;
-import hu.bme.mit.theta.analysis.algorithm.SafetyResult;
+import hu.bme.mit.theta.analysis.algorithm.arg.ARG;
+import hu.bme.mit.theta.analysis.algorithm.arg.ArgChecker;
 import hu.bme.mit.theta.analysis.expr.ExprAction;
 import hu.bme.mit.theta.analysis.expr.ExprState;
 import hu.bme.mit.theta.analysis.unit.UnitPrec;
@@ -54,13 +58,13 @@ public void test() throws FileNotFoundException, IOException {
                 l -> l.equals(cfa.getErrorLoc().get()), abstractionSolver, refinementSolver);
 
         // Act
-        final SafetyResult<? extends ExprState, ? extends ExprAction> status = checker.check(
+        final SafetyResult<ARG<CfaState<PredState>, CfaAction>, Trace<CfaState<PredState>, CfaAction>> status = checker.check(
                 UnitPrec.getInstance());
 
         // Assert
         assertTrue(status.isSafe());
 
-        final ARG<? extends ExprState, ? extends ExprAction> arg = status.getArg();
+        final ARG<? extends ExprState, ? extends ExprAction> arg = status.getWitness();
         arg.minimize();
 
         final ArgChecker argChecker = ArgChecker.create(abstractionSolver);