From ea0177b08471a1795d191e9ff936ec303fc31798 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Krist=C3=B3f=20Marussy?= Date: Tue, 6 Nov 2018 18:04:08 +0100 Subject: [PATCH] Convert to Gradle.kts Split projects for easier assembly of jars with the application and shadow plugins. TODO: * Add z3 libs to application distributions. * Set up the jacocoRootReport task. * Copy jars to the dest directory. * Set up maven-publish and bintray * Modularize the project for Java 11 compatibility * Set up cross-os builds for OpenJFX --- build.gradle.kts | 13 + build.gradle => build.gradle.old | 0 buildSrc/build.gradle.kts | 91 +++++++ buildSrc/gradle.properties | 10 + buildSrc/settings.gradle.kts | 0 buildSrc/src/main/kotlin/Deps.kt | 18 ++ .../main/kotlin/GenerateGrammarExtension.kt | 3 + .../src/main/kotlin/antlr-grammar.gradle.kts | 28 +++ buildSrc/src/main/kotlin/cli-tool.gradle.kts | 8 + .../src/main/kotlin/java-common.gradle.kts | 30 +++ .../src/main/kotlin/tool-common.gradle.kts | 17 ++ common-methods.gradle | 34 --- .../shared-with-buildSrc/mirrors.gradle.kts | 6 + settings.gradle | 16 -- settings.gradle.kts | 26 ++ subprojects/analysis/.gitignore | 1 - subprojects/analysis/build.gradle | 9 - subprojects/analysis/build.gradle.kts | 10 + subprojects/cfa-analysis/build.gradle.kts | 11 + .../bme/mit/theta/cfa/analysis/CfaAction.java | 0 .../mit/theta/cfa/analysis/CfaAnalysis.java | 0 .../mit/theta/cfa/analysis/CfaInitFunc.java | 0 .../hu/bme/mit/theta/cfa/analysis/CfaOrd.java | 0 .../bme/mit/theta/cfa/analysis/CfaPrec.java | 0 .../bme/mit/theta/cfa/analysis/CfaState.java | 0 .../cfa/analysis/CfaTraceConcretizer.java | 7 +- .../mit/theta/cfa/analysis/CfaTransFunc.java | 0 .../cfa/analysis/DistToErrComparator.java | 0 .../theta/cfa/analysis/config/CfaConfig.java} | 10 +- .../analysis/config}/CfaConfigBuilder.java | 25 +- .../cfa/analysis/impact/ImpactChecker.java | 3 +- .../cfa/analysis/impact/ImpactReachedSet.java | 0 .../cfa/analysis/impact/ImpactRefiner.java | 0 .../analysis/impact/PredImpactChecker.java | 0 .../analysis/impact/PredImpactRefiner.java | 0 .../analysis/initprec/CfaAllVarsInitPrec.java | 0 .../analysis/initprec/CfaEmptyInitPrec.java | 0 .../cfa/analysis/initprec/CfaInitPrec.java | 0 .../theta/cfa/analysis/lts/CfaCachedLts.java | 0 .../mit/theta/cfa/analysis/lts/CfaLbeLts.java | 0 .../mit/theta/cfa/analysis/lts/CfaLts.java | 0 .../mit/theta/cfa/analysis/lts/CfaSbeLts.java | 0 .../theta/cfa/analysis/lts/package-info.java | 0 .../mit/theta/cfa/analysis/package-info.java | 0 .../cfa/analysis/prec/GlobalCfaPrec.java | 0 .../analysis/prec/GlobalCfaPrecRefiner.java | 0 .../theta/cfa/analysis/prec/LocalCfaPrec.java | 0 .../analysis/prec/LocalCfaPrecRefiner.java | 0 .../theta/cfa/analysis/prec/package-info.java | 0 .../cfa/analysis}/utils/CfaVisualizer.java | 2 +- .../DistanceToErrorLocComparatorTest.java | 1 - .../mit/theta/cfa/analysis/LocPrecTest.java | 0 .../impact/CfaPredImpactCheckerTest.java | 0 .../src/test/resources/counter5_true.cfa | 17 ++ subprojects/cfa-cli/build.gradle.kts | 14 ++ .../hu/bme/mit/theta/cfa/cli}/CfaCli.java | 31 ++- subprojects/cfa-metrics/build.gradle.kts | 12 + .../mit/theta/cfa/metrics}/CfaMetrics.java | 2 +- subprojects/cfa/.gitignore | 1 - subprojects/cfa/build.gradle | 36 --- subprojects/cfa/build.gradle.kts | 9 + .../hu/bme/mit/theta/cfa/dsl/gen/.gitignore | 2 - subprojects/cfa2dot/build.gradle.kts | 12 + .../mit/theta/cfa/cfa2dot}/CfaToDotMain.java | 6 +- subprojects/common/.gitignore | 1 - subprojects/common/build.gradle | 4 - subprojects/common/build.gradle.kts | 3 + subprojects/core/.gitignore | 1 - subprojects/core/build.gradle | 29 --- subprojects/core/build.gradle.kts | 8 + .../hu/bme/mit/theta/core/dsl/gen/.gitignore | 2 - subprojects/solver-z3/.gitignore | 1 - subprojects/solver-z3/build.gradle | 8 - subprojects/solver-z3/build.gradle.kts | 10 + subprojects/solver/.gitignore | 1 - subprojects/solver/build.gradle | 6 - subprojects/solver/build.gradle.kts | 8 + subprojects/sts-analysis/build.gradle.kts | 11 + .../analysis/StsAction.java | 0 .../analysis/StsLts.java | 0 .../analysis/StsTraceConcretizer.java | 7 +- .../analysis/config/StsConfig.java} | 10 +- .../analysis/config}/StsConfigBuilder.java | 19 +- .../analysis/initprec/StsEmptyInitPrec.java | 0 .../analysis/initprec/StsInitPrec.java | 0 .../analysis/initprec/StsPropInitPrec.java | 0 .../analysis/package-info.java | 0 .../analysis}/utils/StsTraceVisualizer.java | 2 +- .../mit/theta/sts/analysis/StsExplTest.java | 0 .../mit/theta/sts/analysis/StsPredTest.java | 0 subprojects/sts-cli/build.gradle.kts | 14 ++ .../hu/bme/mit/theta/sts/cli}/StsCli.java | 27 +- subprojects/sts/.gitignore | 1 - subprojects/sts/build.gradle | 34 --- subprojects/sts/build.gradle.kts | 9 + subprojects/sts/src/gen/java/.gitignore | 2 - subprojects/xta-analysis/build.gradle.kts | 11 + .../bme/mit/theta/xta/analysis/XtaAction.java | 0 .../mit/theta/xta/analysis/XtaAnalysis.java | 0 .../mit/theta/xta/analysis/XtaInitFunc.java | 0 .../hu/bme/mit/theta/xta/analysis/XtaLts.java | 0 .../hu/bme/mit/theta/xta/analysis/XtaOrd.java | 0 .../bme/mit/theta/xta/analysis/XtaState.java | 0 .../mit/theta/xta/analysis/XtaTransFunc.java | 0 .../xta/analysis/expl/XtaExplAnalysis.java | 0 .../xta/analysis/expl/XtaExplInitFunc.java | 0 .../xta/analysis/expl/XtaExplTransFunc.java | 0 .../theta/xta/analysis/expl/XtaExplUtils.java | 0 .../analysis/expl/itp/ItpExplAnalysis.java | 0 .../analysis/expl/itp/ItpExplInitFunc.java | 0 .../xta/analysis/expl/itp/ItpExplOrd.java | 0 .../xta/analysis/expl/itp/ItpExplState.java | 0 .../analysis/expl/itp/ItpExplTransFunc.java | 0 .../xta/analysis/lazy/AlgorithmStrategy.java | 0 .../xta/analysis/lazy/BwItpExplStrategy.java | 0 .../xta/analysis/lazy/BwItpZoneStrategy.java | 0 .../xta/analysis/lazy/ClockStrategies.java | 0 .../xta/analysis/lazy/ClockStrategy.java | 0 .../xta/analysis/lazy/CombinedStrategy.java | 0 .../xta/analysis/lazy/DataStrategies.java | 0 .../theta/xta/analysis/lazy/DataStrategy.java | 0 .../theta/xta/analysis/lazy/ExplStrategy.java | 0 .../xta/analysis/lazy/FwItpExplStrategy.java | 0 .../xta/analysis/lazy/FwItpZoneStrategy.java | 0 .../xta/analysis/lazy/ItpExplStrategy.java | 0 .../xta/analysis/lazy/ItpZoneStrategy.java | 0 .../xta/analysis/lazy/LazyXtaChecker.java | 0 .../analysis/lazy/LazyXtaCheckerFactory.java | 0 .../xta/analysis/lazy/LazyXtaStatistics.java | 0 .../bme/mit/theta/xta/analysis/lazy/Lens.java | 0 .../xta/analysis/lazy/LuZoneStrategy.java | 0 .../xta/analysis/zone/XtaActZoneUtils.java | 0 .../xta/analysis/zone/XtaLuZoneUtils.java | 0 .../xta/analysis/zone/XtaZoneAnalysis.java | 0 .../xta/analysis/zone/XtaZoneInitFunc.java | 0 .../xta/analysis/zone/XtaZoneTransFunc.java | 0 .../theta/xta/analysis/zone/XtaZoneUtils.java | 0 .../analysis/zone/itp/ItpZoneAnalysis.java | 0 .../analysis/zone/itp/ItpZoneInitFunc.java | 0 .../xta/analysis/zone/itp/ItpZoneOrd.java | 0 .../xta/analysis/zone/itp/ItpZoneState.java | 0 .../analysis/zone/itp/ItpZoneTransFunc.java | 0 .../xta/analysis/zone/lu/LuZoneAnalysis.java | 0 .../xta/analysis/zone/lu/LuZoneInitFunc.java | 0 .../theta/xta/analysis/zone/lu/LuZoneOrd.java | 0 .../xta/analysis/zone/lu/LuZoneState.java | 0 .../xta/analysis/zone/lu/LuZoneTransFunc.java | 0 .../xta/analysis/LazyXtaCheckerTest.java | 0 .../theta/xta/analysis/XtaAnalysisTest.java | 0 .../xta/analysis/XtaZoneAnalysisTest.java | 0 .../src/test/resources/critical-2-25-50.xta | 61 +++++ .../src/test/resources/csma-2.xta | 57 +++++ .../src/test/resources/engine-classic.xta | 233 ++++++++++++++++++ .../src/test/resources/fddi-2.xta | 58 +++++ .../src/test/resources/fischer-2-32-64.xta | 27 ++ .../src/test/resources/lynch-2-16.xta | 39 +++ subprojects/xta-cli/build.gradle.kts | 14 ++ .../hu/bme/mit/theta/xta/cli}/XtaCli.java | 2 +- subprojects/xta/.gitignore | 1 - subprojects/xta/build.gradle | 35 --- subprojects/xta/build.gradle.kts | 9 + .../hu/bme/mit/theta/xta/dsl/gen/.gitignore | 2 - 162 files changed, 982 insertions(+), 306 deletions(-) create mode 100644 build.gradle.kts rename build.gradle => build.gradle.old (100%) create mode 100644 buildSrc/build.gradle.kts create mode 100644 buildSrc/gradle.properties create mode 100644 buildSrc/settings.gradle.kts create mode 100644 buildSrc/src/main/kotlin/Deps.kt create mode 100644 buildSrc/src/main/kotlin/GenerateGrammarExtension.kt create mode 100644 buildSrc/src/main/kotlin/antlr-grammar.gradle.kts create mode 100644 buildSrc/src/main/kotlin/cli-tool.gradle.kts create mode 100644 buildSrc/src/main/kotlin/java-common.gradle.kts create mode 100644 buildSrc/src/main/kotlin/tool-common.gradle.kts delete mode 100644 common-methods.gradle create mode 100644 gradle/shared-with-buildSrc/mirrors.gradle.kts delete mode 100644 settings.gradle create mode 100644 settings.gradle.kts delete mode 100644 subprojects/analysis/.gitignore delete mode 100644 subprojects/analysis/build.gradle create mode 100644 subprojects/analysis/build.gradle.kts create mode 100644 subprojects/cfa-analysis/build.gradle.kts rename subprojects/{cfa => cfa-analysis}/src/main/java/hu/bme/mit/theta/cfa/analysis/CfaAction.java (100%) rename subprojects/{cfa => cfa-analysis}/src/main/java/hu/bme/mit/theta/cfa/analysis/CfaAnalysis.java (100%) rename subprojects/{cfa => cfa-analysis}/src/main/java/hu/bme/mit/theta/cfa/analysis/CfaInitFunc.java (100%) rename subprojects/{cfa => cfa-analysis}/src/main/java/hu/bme/mit/theta/cfa/analysis/CfaOrd.java (100%) rename subprojects/{cfa => cfa-analysis}/src/main/java/hu/bme/mit/theta/cfa/analysis/CfaPrec.java (100%) rename subprojects/{cfa => cfa-analysis}/src/main/java/hu/bme/mit/theta/cfa/analysis/CfaState.java (100%) rename subprojects/{cfa => cfa-analysis}/src/main/java/hu/bme/mit/theta/cfa/analysis/CfaTraceConcretizer.java (92%) rename subprojects/{cfa => cfa-analysis}/src/main/java/hu/bme/mit/theta/cfa/analysis/CfaTransFunc.java (100%) rename subprojects/{cfa => cfa-analysis}/src/main/java/hu/bme/mit/theta/cfa/analysis/DistToErrComparator.java (100%) rename subprojects/{cfa/src/main/java/hu/bme/mit/theta/cfa/tool/Config.java => cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/config/CfaConfig.java} (81%) rename subprojects/{cfa/src/main/java/hu/bme/mit/theta/cfa/tool => cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/config}/CfaConfigBuilder.java (94%) rename subprojects/{cfa => cfa-analysis}/src/main/java/hu/bme/mit/theta/cfa/analysis/impact/ImpactChecker.java (97%) rename subprojects/{cfa => cfa-analysis}/src/main/java/hu/bme/mit/theta/cfa/analysis/impact/ImpactReachedSet.java (100%) rename subprojects/{cfa => cfa-analysis}/src/main/java/hu/bme/mit/theta/cfa/analysis/impact/ImpactRefiner.java (100%) rename subprojects/{cfa => cfa-analysis}/src/main/java/hu/bme/mit/theta/cfa/analysis/impact/PredImpactChecker.java (100%) rename subprojects/{cfa => cfa-analysis}/src/main/java/hu/bme/mit/theta/cfa/analysis/impact/PredImpactRefiner.java (100%) rename subprojects/{cfa => cfa-analysis}/src/main/java/hu/bme/mit/theta/cfa/analysis/initprec/CfaAllVarsInitPrec.java (100%) rename subprojects/{cfa => cfa-analysis}/src/main/java/hu/bme/mit/theta/cfa/analysis/initprec/CfaEmptyInitPrec.java (100%) rename subprojects/{cfa => cfa-analysis}/src/main/java/hu/bme/mit/theta/cfa/analysis/initprec/CfaInitPrec.java (100%) rename subprojects/{cfa => cfa-analysis}/src/main/java/hu/bme/mit/theta/cfa/analysis/lts/CfaCachedLts.java (100%) rename subprojects/{cfa => cfa-analysis}/src/main/java/hu/bme/mit/theta/cfa/analysis/lts/CfaLbeLts.java (100%) rename subprojects/{cfa => cfa-analysis}/src/main/java/hu/bme/mit/theta/cfa/analysis/lts/CfaLts.java (100%) rename subprojects/{cfa => cfa-analysis}/src/main/java/hu/bme/mit/theta/cfa/analysis/lts/CfaSbeLts.java (100%) rename subprojects/{cfa => cfa-analysis}/src/main/java/hu/bme/mit/theta/cfa/analysis/lts/package-info.java (100%) rename subprojects/{cfa => cfa-analysis}/src/main/java/hu/bme/mit/theta/cfa/analysis/package-info.java (100%) rename subprojects/{cfa => cfa-analysis}/src/main/java/hu/bme/mit/theta/cfa/analysis/prec/GlobalCfaPrec.java (100%) rename subprojects/{cfa => cfa-analysis}/src/main/java/hu/bme/mit/theta/cfa/analysis/prec/GlobalCfaPrecRefiner.java (100%) rename subprojects/{cfa => cfa-analysis}/src/main/java/hu/bme/mit/theta/cfa/analysis/prec/LocalCfaPrec.java (100%) rename subprojects/{cfa => cfa-analysis}/src/main/java/hu/bme/mit/theta/cfa/analysis/prec/LocalCfaPrecRefiner.java (100%) rename subprojects/{cfa => cfa-analysis}/src/main/java/hu/bme/mit/theta/cfa/analysis/prec/package-info.java (100%) rename subprojects/{cfa/src/main/java/hu/bme/mit/theta/cfa => cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis}/utils/CfaVisualizer.java (99%) rename subprojects/{cfa => cfa-analysis}/src/test/java/hu/bme/mit/theta/cfa/analysis/DistanceToErrorLocComparatorTest.java (97%) rename subprojects/{cfa => cfa-analysis}/src/test/java/hu/bme/mit/theta/cfa/analysis/LocPrecTest.java (100%) rename subprojects/{cfa => cfa-analysis}/src/test/java/hu/bme/mit/theta/cfa/analysis/impact/CfaPredImpactCheckerTest.java (100%) create mode 100644 subprojects/cfa-analysis/src/test/resources/counter5_true.cfa create mode 100644 subprojects/cfa-cli/build.gradle.kts rename subprojects/{cfa/src/main/java/hu/bme/mit/theta/cfa/tool => cfa-cli/src/main/java/hu/bme/mit/theta/cfa/cli}/CfaCli.java (85%) create mode 100644 subprojects/cfa-metrics/build.gradle.kts rename subprojects/{cfa/src/main/java/hu/bme/mit/theta/cfa/tool => cfa-metrics/src/main/java/hu/bme/mit/theta/cfa/metrics}/CfaMetrics.java (98%) delete mode 100644 subprojects/cfa/.gitignore delete mode 100644 subprojects/cfa/build.gradle create mode 100644 subprojects/cfa/build.gradle.kts delete mode 100644 subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/dsl/gen/.gitignore create mode 100644 subprojects/cfa2dot/build.gradle.kts rename subprojects/{cfa/src/main/java/hu/bme/mit/theta/cfa/tool => cfa2dot/src/main/java/hu/bme/mit/theta/cfa/cfa2dot}/CfaToDotMain.java (94%) delete mode 100644 subprojects/common/.gitignore delete mode 100644 subprojects/common/build.gradle create mode 100644 subprojects/common/build.gradle.kts delete mode 100644 subprojects/core/.gitignore delete mode 100644 subprojects/core/build.gradle create mode 100644 subprojects/core/build.gradle.kts delete mode 100644 subprojects/core/src/main/java/hu/bme/mit/theta/core/dsl/gen/.gitignore delete mode 100644 subprojects/solver-z3/.gitignore delete mode 100644 subprojects/solver-z3/build.gradle create mode 100644 subprojects/solver-z3/build.gradle.kts delete mode 100644 subprojects/solver/.gitignore delete mode 100644 subprojects/solver/build.gradle create mode 100644 subprojects/solver/build.gradle.kts create mode 100644 subprojects/sts-analysis/build.gradle.kts rename subprojects/{sts/src/main/java/hu/bme/mit/theta/sts => sts-analysis/src/main/java/hu.bme.mit.theta.sts}/analysis/StsAction.java (100%) rename subprojects/{sts/src/main/java/hu/bme/mit/theta/sts => sts-analysis/src/main/java/hu.bme.mit.theta.sts}/analysis/StsLts.java (100%) rename subprojects/{sts/src/main/java/hu/bme/mit/theta/sts => sts-analysis/src/main/java/hu.bme.mit.theta.sts}/analysis/StsTraceConcretizer.java (87%) rename subprojects/{sts/src/main/java/hu/bme/mit/theta/sts/tool/Config.java => sts-analysis/src/main/java/hu.bme.mit.theta.sts/analysis/config/StsConfig.java} (81%) rename subprojects/{sts/src/main/java/hu/bme/mit/theta/sts/tool => sts-analysis/src/main/java/hu.bme.mit.theta.sts/analysis/config}/StsConfigBuilder.java (95%) rename subprojects/{sts/src/main/java/hu/bme/mit/theta/sts => sts-analysis/src/main/java/hu.bme.mit.theta.sts}/analysis/initprec/StsEmptyInitPrec.java (100%) rename subprojects/{sts/src/main/java/hu/bme/mit/theta/sts => sts-analysis/src/main/java/hu.bme.mit.theta.sts}/analysis/initprec/StsInitPrec.java (100%) rename subprojects/{sts/src/main/java/hu/bme/mit/theta/sts => sts-analysis/src/main/java/hu.bme.mit.theta.sts}/analysis/initprec/StsPropInitPrec.java (100%) rename subprojects/{sts/src/main/java/hu/bme/mit/theta/sts => sts-analysis/src/main/java/hu.bme.mit.theta.sts}/analysis/package-info.java (100%) rename subprojects/{sts/src/main/java/hu/bme/mit/theta/sts => sts-analysis/src/main/java/hu.bme.mit.theta.sts/analysis}/utils/StsTraceVisualizer.java (95%) rename subprojects/{sts => sts-analysis}/src/test/java/hu/bme/mit/theta/sts/analysis/StsExplTest.java (100%) rename subprojects/{sts => sts-analysis}/src/test/java/hu/bme/mit/theta/sts/analysis/StsPredTest.java (100%) create mode 100644 subprojects/sts-cli/build.gradle.kts rename subprojects/{sts/src/main/java/hu/bme/mit/theta/sts/tool => sts-cli/src/main/java/hu/bme/mit/theta/sts/cli}/StsCli.java (88%) delete mode 100644 subprojects/sts/.gitignore delete mode 100644 subprojects/sts/build.gradle create mode 100644 subprojects/sts/build.gradle.kts delete mode 100644 subprojects/sts/src/gen/java/.gitignore create mode 100644 subprojects/xta-analysis/build.gradle.kts rename subprojects/{xta => xta-analysis}/src/main/java/hu/bme/mit/theta/xta/analysis/XtaAction.java (100%) rename subprojects/{xta => xta-analysis}/src/main/java/hu/bme/mit/theta/xta/analysis/XtaAnalysis.java (100%) rename subprojects/{xta => xta-analysis}/src/main/java/hu/bme/mit/theta/xta/analysis/XtaInitFunc.java (100%) rename subprojects/{xta => xta-analysis}/src/main/java/hu/bme/mit/theta/xta/analysis/XtaLts.java (100%) rename subprojects/{xta => xta-analysis}/src/main/java/hu/bme/mit/theta/xta/analysis/XtaOrd.java (100%) rename subprojects/{xta => xta-analysis}/src/main/java/hu/bme/mit/theta/xta/analysis/XtaState.java (100%) rename subprojects/{xta => xta-analysis}/src/main/java/hu/bme/mit/theta/xta/analysis/XtaTransFunc.java (100%) rename subprojects/{xta => xta-analysis}/src/main/java/hu/bme/mit/theta/xta/analysis/expl/XtaExplAnalysis.java (100%) rename subprojects/{xta => xta-analysis}/src/main/java/hu/bme/mit/theta/xta/analysis/expl/XtaExplInitFunc.java (100%) rename subprojects/{xta => xta-analysis}/src/main/java/hu/bme/mit/theta/xta/analysis/expl/XtaExplTransFunc.java (100%) rename subprojects/{xta => xta-analysis}/src/main/java/hu/bme/mit/theta/xta/analysis/expl/XtaExplUtils.java (100%) rename subprojects/{xta => xta-analysis}/src/main/java/hu/bme/mit/theta/xta/analysis/expl/itp/ItpExplAnalysis.java (100%) rename subprojects/{xta => xta-analysis}/src/main/java/hu/bme/mit/theta/xta/analysis/expl/itp/ItpExplInitFunc.java (100%) rename subprojects/{xta => xta-analysis}/src/main/java/hu/bme/mit/theta/xta/analysis/expl/itp/ItpExplOrd.java (100%) rename subprojects/{xta => xta-analysis}/src/main/java/hu/bme/mit/theta/xta/analysis/expl/itp/ItpExplState.java (100%) rename subprojects/{xta => xta-analysis}/src/main/java/hu/bme/mit/theta/xta/analysis/expl/itp/ItpExplTransFunc.java (100%) rename subprojects/{xta => xta-analysis}/src/main/java/hu/bme/mit/theta/xta/analysis/lazy/AlgorithmStrategy.java (100%) rename subprojects/{xta => xta-analysis}/src/main/java/hu/bme/mit/theta/xta/analysis/lazy/BwItpExplStrategy.java (100%) rename subprojects/{xta => xta-analysis}/src/main/java/hu/bme/mit/theta/xta/analysis/lazy/BwItpZoneStrategy.java (100%) rename subprojects/{xta => xta-analysis}/src/main/java/hu/bme/mit/theta/xta/analysis/lazy/ClockStrategies.java (100%) rename subprojects/{xta => xta-analysis}/src/main/java/hu/bme/mit/theta/xta/analysis/lazy/ClockStrategy.java (100%) rename subprojects/{xta => xta-analysis}/src/main/java/hu/bme/mit/theta/xta/analysis/lazy/CombinedStrategy.java (100%) rename subprojects/{xta => xta-analysis}/src/main/java/hu/bme/mit/theta/xta/analysis/lazy/DataStrategies.java (100%) rename subprojects/{xta => xta-analysis}/src/main/java/hu/bme/mit/theta/xta/analysis/lazy/DataStrategy.java (100%) rename subprojects/{xta => xta-analysis}/src/main/java/hu/bme/mit/theta/xta/analysis/lazy/ExplStrategy.java (100%) rename subprojects/{xta => xta-analysis}/src/main/java/hu/bme/mit/theta/xta/analysis/lazy/FwItpExplStrategy.java (100%) rename subprojects/{xta => xta-analysis}/src/main/java/hu/bme/mit/theta/xta/analysis/lazy/FwItpZoneStrategy.java (100%) rename subprojects/{xta => xta-analysis}/src/main/java/hu/bme/mit/theta/xta/analysis/lazy/ItpExplStrategy.java (100%) rename subprojects/{xta => xta-analysis}/src/main/java/hu/bme/mit/theta/xta/analysis/lazy/ItpZoneStrategy.java (100%) rename subprojects/{xta => xta-analysis}/src/main/java/hu/bme/mit/theta/xta/analysis/lazy/LazyXtaChecker.java (100%) rename subprojects/{xta => xta-analysis}/src/main/java/hu/bme/mit/theta/xta/analysis/lazy/LazyXtaCheckerFactory.java (100%) rename subprojects/{xta => xta-analysis}/src/main/java/hu/bme/mit/theta/xta/analysis/lazy/LazyXtaStatistics.java (100%) rename subprojects/{xta => xta-analysis}/src/main/java/hu/bme/mit/theta/xta/analysis/lazy/Lens.java (100%) rename subprojects/{xta => xta-analysis}/src/main/java/hu/bme/mit/theta/xta/analysis/lazy/LuZoneStrategy.java (100%) rename subprojects/{xta => xta-analysis}/src/main/java/hu/bme/mit/theta/xta/analysis/zone/XtaActZoneUtils.java (100%) rename subprojects/{xta => xta-analysis}/src/main/java/hu/bme/mit/theta/xta/analysis/zone/XtaLuZoneUtils.java (100%) rename subprojects/{xta => xta-analysis}/src/main/java/hu/bme/mit/theta/xta/analysis/zone/XtaZoneAnalysis.java (100%) rename subprojects/{xta => xta-analysis}/src/main/java/hu/bme/mit/theta/xta/analysis/zone/XtaZoneInitFunc.java (100%) rename subprojects/{xta => xta-analysis}/src/main/java/hu/bme/mit/theta/xta/analysis/zone/XtaZoneTransFunc.java (100%) rename subprojects/{xta => xta-analysis}/src/main/java/hu/bme/mit/theta/xta/analysis/zone/XtaZoneUtils.java (100%) rename subprojects/{xta => xta-analysis}/src/main/java/hu/bme/mit/theta/xta/analysis/zone/itp/ItpZoneAnalysis.java (100%) rename subprojects/{xta => xta-analysis}/src/main/java/hu/bme/mit/theta/xta/analysis/zone/itp/ItpZoneInitFunc.java (100%) rename subprojects/{xta => xta-analysis}/src/main/java/hu/bme/mit/theta/xta/analysis/zone/itp/ItpZoneOrd.java (100%) rename subprojects/{xta => xta-analysis}/src/main/java/hu/bme/mit/theta/xta/analysis/zone/itp/ItpZoneState.java (100%) rename subprojects/{xta => xta-analysis}/src/main/java/hu/bme/mit/theta/xta/analysis/zone/itp/ItpZoneTransFunc.java (100%) rename subprojects/{xta => xta-analysis}/src/main/java/hu/bme/mit/theta/xta/analysis/zone/lu/LuZoneAnalysis.java (100%) rename subprojects/{xta => xta-analysis}/src/main/java/hu/bme/mit/theta/xta/analysis/zone/lu/LuZoneInitFunc.java (100%) rename subprojects/{xta => xta-analysis}/src/main/java/hu/bme/mit/theta/xta/analysis/zone/lu/LuZoneOrd.java (100%) rename subprojects/{xta => xta-analysis}/src/main/java/hu/bme/mit/theta/xta/analysis/zone/lu/LuZoneState.java (100%) rename subprojects/{xta => xta-analysis}/src/main/java/hu/bme/mit/theta/xta/analysis/zone/lu/LuZoneTransFunc.java (100%) rename subprojects/{xta => xta-analysis}/src/test/java/hu/bme/mit/theta/xta/analysis/LazyXtaCheckerTest.java (100%) rename subprojects/{xta => xta-analysis}/src/test/java/hu/bme/mit/theta/xta/analysis/XtaAnalysisTest.java (100%) rename subprojects/{xta => xta-analysis}/src/test/java/hu/bme/mit/theta/xta/analysis/XtaZoneAnalysisTest.java (100%) create mode 100644 subprojects/xta-analysis/src/test/resources/critical-2-25-50.xta create mode 100644 subprojects/xta-analysis/src/test/resources/csma-2.xta create mode 100644 subprojects/xta-analysis/src/test/resources/engine-classic.xta create mode 100644 subprojects/xta-analysis/src/test/resources/fddi-2.xta create mode 100644 subprojects/xta-analysis/src/test/resources/fischer-2-32-64.xta create mode 100644 subprojects/xta-analysis/src/test/resources/lynch-2-16.xta create mode 100644 subprojects/xta-cli/build.gradle.kts rename subprojects/{xta/src/main/java/hu/bme/mit/theta/xta/tool => xta-cli/src/main/java/hu/bme/mit/theta/xta/cli}/XtaCli.java (99%) delete mode 100644 subprojects/xta/.gitignore delete mode 100644 subprojects/xta/build.gradle create mode 100644 subprojects/xta/build.gradle.kts delete mode 100644 subprojects/xta/src/main/java/hu/bme/mit/theta/xta/dsl/gen/.gitignore diff --git a/build.gradle.kts b/build.gradle.kts new file mode 100644 index 0000000000..b248c2bdd4 --- /dev/null +++ b/build.gradle.kts @@ -0,0 +1,13 @@ +plugins { + base +} + +allprojects { + group = "hu.bme.mit.inf.theta" + version = "0.0.1-SNAPSHOT" + + apply(from = rootDir.resolve("gradle/shared-with-buildSrc/mirrors.gradle.kts")) +} + +val libPath: String by extra { rootProject.rootDir.resolve("lib").path } +val execPath by extra { "$libPath${File.pathSeparator}${System.getenv("PATH")}" } diff --git a/build.gradle b/build.gradle.old similarity index 100% rename from build.gradle rename to build.gradle.old diff --git a/buildSrc/build.gradle.kts b/buildSrc/build.gradle.kts new file mode 100644 index 0000000000..2c68f41c6a --- /dev/null +++ b/buildSrc/build.gradle.kts @@ -0,0 +1,91 @@ +import java.io.FileOutputStream +import org.jetbrains.kotlin.gradle.plugin.KotlinSourceSet +import org.jetbrains.kotlin.gradle.tasks.KotlinCompile + +plugins { + `java-gradle-plugin` + `kotlin-dsl` + `kotlin-dsl-precompiled-script-plugins` +} + +repositories { + gradlePluginPortal() +} + +apply(from = rootDir.resolve("../gradle/shared-with-buildSrc/mirrors.gradle.kts")) + +kotlinDslPluginOptions { + experimentalWarning.set(false) +} + +val kotlinVersion: String by project +val shadowVersion: String by project + +// https://github.com/gradle/kotlin-dsl/issues/430#issuecomment-414768887 +fun gradlePlugin(id: String, version: String): String = "$id:$id.gradle.plugin:$version" + +dependencies { + compileOnly(gradleKotlinDsl()) + compile(kotlin("gradle-plugin", kotlinVersion)) + compile(gradlePlugin("com.github.johnrengelman.shadow", shadowVersion)) +} + +// Force the embeddable Kotlin compiler version to be the selected kotlinVersion. +// https://github.com/gradle/kotlin-dsl/issues/1207 +configurations.all { + val isKotlinCompiler = name == "embeddedKotlin" || name.startsWith("kotlin") || name.startsWith("kapt") + if (!isKotlinCompiler) { + resolutionStrategy.eachDependency { + if (requested.group == "org.jetbrains.kotlin" && requested.module.name == "kotlin-compiler-embeddable") { + useVersion(kotlinVersion) + } + } + } +} + +val versionsClassName = "Versions" +val generatedVersionsKotlinSrcDir = buildDir.resolve("generated-sources/versions/kotlin") +val generatedVersionsFile = generatedVersionsKotlinSrcDir.resolve("$versionsClassName.kt") + +sourceSets { + named("main") { + withConvention(KotlinSourceSet::class) { + kotlin.srcDir(generatedVersionsKotlinSrcDir) + } + } +} + +fun generateVersionsSource(): String { + val text = StringBuilder() + + text.appendln("object $versionsClassName {") + + for (property in project.properties) { + if (property.key.endsWith("Version")) { + val keyWithoutVersion = property.key.substringBefore("Version") + text.appendln(" const val `$keyWithoutVersion` = \"${property.value}\"") + } + } + + text.appendln("}") + + return text.toString() +} + +tasks { + val generateVersions by creating { + description = "Updates Versions.kt from project properties." + group = "build" + outputs.dirs(generatedVersionsKotlinSrcDir) + + doLast { + val versionsSource = generateVersionsSource() + generatedVersionsKotlinSrcDir.mkdirs() + generatedVersionsFile.writeText(versionsSource) + } + } + + named("compileKotlin", KotlinCompile::class) { + dependsOn(generateVersions) + } +} diff --git a/buildSrc/gradle.properties b/buildSrc/gradle.properties new file mode 100644 index 0000000000..d208442b97 --- /dev/null +++ b/buildSrc/gradle.properties @@ -0,0 +1,10 @@ +javaVersion=11 +kotlinVersion=1.3.0 +shadowVersion=4.0.2 +antlrVersion=4.5.3 +guavaVersion=23.6-jre +jcommanderVersion=1.72 +z3Version=4.5.0 +junitVersion=4.12 +jacocoVersion=0.8.2 +mockitoVersion=2.2.11 diff --git a/buildSrc/settings.gradle.kts b/buildSrc/settings.gradle.kts new file mode 100644 index 0000000000..e69de29bb2 diff --git a/buildSrc/src/main/kotlin/Deps.kt b/buildSrc/src/main/kotlin/Deps.kt new file mode 100644 index 0000000000..bd19649726 --- /dev/null +++ b/buildSrc/src/main/kotlin/Deps.kt @@ -0,0 +1,18 @@ +object Deps { + val guava = "com.google.guava:guava:${Versions.guava}" + + object Antlr { + val antlr = "org.antlr:antlr4:${Versions.antlr}" + val runtime = "org.antlr:antlr4-runtime:${Versions.antlr}" + } + + val z3 = "z3:com.microsoft.z3:${Versions.z3}" + + val jcommander = "com.beust:jcommander:${Versions.jcommander}" + + val junit4 = "junit:junit:${Versions.junit}" + + object Mockito { + val core = "org.mockito:mockito-core:${Versions.mockito}" + } +} diff --git a/buildSrc/src/main/kotlin/GenerateGrammarExtension.kt b/buildSrc/src/main/kotlin/GenerateGrammarExtension.kt new file mode 100644 index 0000000000..86cd4cb0a7 --- /dev/null +++ b/buildSrc/src/main/kotlin/GenerateGrammarExtension.kt @@ -0,0 +1,3 @@ +import org.gradle.api.Project +import org.gradle.kotlin.dsl.property + diff --git a/buildSrc/src/main/kotlin/antlr-grammar.gradle.kts b/buildSrc/src/main/kotlin/antlr-grammar.gradle.kts new file mode 100644 index 0000000000..d6da26c19a --- /dev/null +++ b/buildSrc/src/main/kotlin/antlr-grammar.gradle.kts @@ -0,0 +1,28 @@ +import java.nio.file.Files + +apply() + +dependencies { + val antlr: Configuration by configurations + val implementation: Configuration by configurations + + antlr(Deps.Antlr.antlr) + implementation(Deps.Antlr.runtime) +} + +open class GenerateGrammarExtension(project: Project) { + var packageName: String = "hu.bme.mit.${project.name.replace("-",".")}.dsl.gen" +} + +tasks { + val grammar = extensions.create("grammar", project) + + named("generateGrammarSource", AntlrTask::class) { + val packageName = grammar.packageName + val directoryName = packageName.replace(".", File.separator) + val pacakgeQualifiedOutputDirectory = outputDirectory.resolve(directoryName) + outputDirectory = pacakgeQualifiedOutputDirectory + + arguments.addAll(listOf("-package", packageName, "-Werror", "-visitor")) + } +} diff --git a/buildSrc/src/main/kotlin/cli-tool.gradle.kts b/buildSrc/src/main/kotlin/cli-tool.gradle.kts new file mode 100644 index 0000000000..ea8954f798 --- /dev/null +++ b/buildSrc/src/main/kotlin/cli-tool.gradle.kts @@ -0,0 +1,8 @@ +apply(plugin = "tool-common") + +dependencies { + val implementation: Configuration by configurations + + implementation(Deps.jcommander) +} + diff --git a/buildSrc/src/main/kotlin/java-common.gradle.kts b/buildSrc/src/main/kotlin/java-common.gradle.kts new file mode 100644 index 0000000000..bc21ded5f4 --- /dev/null +++ b/buildSrc/src/main/kotlin/java-common.gradle.kts @@ -0,0 +1,30 @@ +apply() +apply() + +dependencies { + val implementation: Configuration by configurations + val testImplementation: Configuration by configurations + + implementation(Deps.guava) + testImplementation(Deps.junit4) + testImplementation(Deps.Mockito.core) +} + +tasks { + withType() { + sourceCompatibility = Versions.java + targetCompatibility = Versions.java + } + + val libPath: String by rootProject.extra + val execPath: String by rootProject.extra + + withType() { + environment["PATH"] = execPath + environment["LD_LIBRARY_PATH"] = libPath + } +} + +extensions.configure { + toolVersion = Versions.jacoco +} diff --git a/buildSrc/src/main/kotlin/tool-common.gradle.kts b/buildSrc/src/main/kotlin/tool-common.gradle.kts new file mode 100644 index 0000000000..25ba37e2b5 --- /dev/null +++ b/buildSrc/src/main/kotlin/tool-common.gradle.kts @@ -0,0 +1,17 @@ +import com.github.jengelman.gradle.plugins.shadow.ShadowPlugin + +apply() +apply() + +tasks { + val libPath: String by rootProject.extra + val execPath: String by rootProject.extra + + fun JavaExec.setupEnvironment() { + environment["PATH"] = execPath + environment["LD_LIBRARY_PATH"] = libPath + } + + named("run", JavaExec::class).configure { setupEnvironment() } + named("runShadow", JavaExec::class).configure { setupEnvironment() } +} diff --git a/common-methods.gradle b/common-methods.gradle deleted file mode 100644 index 371d9b73a4..0000000000 --- a/common-methods.gradle +++ /dev/null @@ -1,34 +0,0 @@ -def getCommitId() { - def commit = new ByteArrayOutputStream() - def branch = new ByteArrayOutputStream() - exec { - commandLine 'git', 'rev-parse', '--short', 'HEAD' - standardOutput = commit - } - exec { - commandLine 'git', 'rev-parse', '--abbrev-ref', 'HEAD' - standardOutput = branch - } - def id = branch.toString() + "-" + commit.toString() - - return id.replace("\n", "").replaceAll("[^a-zA-Z0-9._]", "-") -} - -def createJarTask(def taskName, def mainClass, def jarBaseName) { - return tasks.create(taskName, Jar) { - manifest { - attributes 'Implementation-Version': getCommitId(), - 'Main-Class': mainClass - } - baseName = jarBaseName - classifier = null - version = null - from { configurations.compile.collect { it.isDirectory() ? it : zipTree(it) } } - with jar - } -} - -ext { - getCommitId = this.&getCommitId - createJarTask = this.&createJarTask -} \ No newline at end of file diff --git a/gradle/shared-with-buildSrc/mirrors.gradle.kts b/gradle/shared-with-buildSrc/mirrors.gradle.kts new file mode 100644 index 0000000000..214635c871 --- /dev/null +++ b/gradle/shared-with-buildSrc/mirrors.gradle.kts @@ -0,0 +1,6 @@ +repositories { + mavenCentral() + maven { + setUrl("https://dl.bintray.com/ftsrg/maven") + } +} diff --git a/settings.gradle b/settings.gradle deleted file mode 100644 index 90bc2ef858..0000000000 --- a/settings.gradle +++ /dev/null @@ -1,16 +0,0 @@ -rootProject.name = 'theta' - -include 'analysis' -include 'cfa' -include 'common' -include 'core' -include 'solver' -include 'solver-z3' -include 'sts' -include 'xta' - -for (project in rootProject.children) { - project.projectDir = file("subprojects/${project.name}") - project.name = "${rootProject.name}-${project.name}" -} - diff --git a/settings.gradle.kts b/settings.gradle.kts new file mode 100644 index 0000000000..04bc815e4b --- /dev/null +++ b/settings.gradle.kts @@ -0,0 +1,26 @@ +rootProject.name = "theta" + +include( + "analysis", + "cfa", + "cfa2dot", + "cfa-analysis", + "cfa-cli", + "cfa-metrics", + "common", + "core", + "solver", + "solver-z3", + "sts", + "sts-analysis", + "sts-cli", + "xta", + "xta-analysis", + "xta-cli" +) + +for (project in rootProject.children) { + val projectName = project.name + project.projectDir = file("subprojects/$projectName") + project.name = "${rootProject.name}-$projectName" +} diff --git a/subprojects/analysis/.gitignore b/subprojects/analysis/.gitignore deleted file mode 100644 index 65776c32fc..0000000000 --- a/subprojects/analysis/.gitignore +++ /dev/null @@ -1 +0,0 @@ -/bin/ \ No newline at end of file diff --git a/subprojects/analysis/build.gradle b/subprojects/analysis/build.gradle deleted file mode 100644 index c77fd18c6f..0000000000 --- a/subprojects/analysis/build.gradle +++ /dev/null @@ -1,9 +0,0 @@ -dependencies { - compile project(':theta-common') - compile project(':theta-core') - compile project(':theta-solver') - compile group: 'com.google.guava', name: 'guava', version: guavaVersion - testCompile project(':theta-solver-z3') - testCompile group: 'junit', name: 'junit', version: junitVersion - testCompile group: 'org.mockito', name: 'mockito-core', version: mockitoVersion -} diff --git a/subprojects/analysis/build.gradle.kts b/subprojects/analysis/build.gradle.kts new file mode 100644 index 0000000000..81c79e1a20 --- /dev/null +++ b/subprojects/analysis/build.gradle.kts @@ -0,0 +1,10 @@ +plugins { + id("java-common") +} + +dependencies { + compile(project(":theta-common")) + compile(project(":theta-core")) + compile(project(":theta-solver")) + testImplementation(project(":theta-solver-z3")) +} diff --git a/subprojects/cfa-analysis/build.gradle.kts b/subprojects/cfa-analysis/build.gradle.kts new file mode 100644 index 0000000000..fbfc58a323 --- /dev/null +++ b/subprojects/cfa-analysis/build.gradle.kts @@ -0,0 +1,11 @@ +plugins { + id("java-common") +} + +dependencies { + compile(project(":theta-analysis")) + compile(project(":theta-cfa")) + compile(project(":theta-common")) + compile(project(":theta-core")) + testImplementation(project(":theta-solver-z3")) +} diff --git a/subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/analysis/CfaAction.java b/subprojects/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/CfaAction.java similarity index 100% rename from subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/analysis/CfaAction.java rename to subprojects/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/CfaAction.java diff --git a/subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/analysis/CfaAnalysis.java b/subprojects/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/CfaAnalysis.java similarity index 100% rename from subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/analysis/CfaAnalysis.java rename to subprojects/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/CfaAnalysis.java diff --git a/subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/analysis/CfaInitFunc.java b/subprojects/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/CfaInitFunc.java similarity index 100% rename from subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/analysis/CfaInitFunc.java rename to subprojects/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/CfaInitFunc.java diff --git a/subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/analysis/CfaOrd.java b/subprojects/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/CfaOrd.java similarity index 100% rename from subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/analysis/CfaOrd.java rename to subprojects/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/CfaOrd.java diff --git a/subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/analysis/CfaPrec.java b/subprojects/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/CfaPrec.java similarity index 100% rename from subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/analysis/CfaPrec.java rename to subprojects/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/CfaPrec.java diff --git a/subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/analysis/CfaState.java b/subprojects/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/CfaState.java similarity index 100% rename from subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/analysis/CfaState.java rename to subprojects/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/CfaState.java diff --git a/subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/analysis/CfaTraceConcretizer.java b/subprojects/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/CfaTraceConcretizer.java similarity index 92% rename from subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/analysis/CfaTraceConcretizer.java rename to subprojects/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/CfaTraceConcretizer.java index b5e1571061..ccd9e0c07a 100644 --- a/subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/analysis/CfaTraceConcretizer.java +++ b/subprojects/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/CfaTraceConcretizer.java @@ -29,16 +29,17 @@ import hu.bme.mit.theta.analysis.expr.refinement.ItpRefutation; import hu.bme.mit.theta.core.model.Valuation; import hu.bme.mit.theta.core.type.booltype.BoolExprs; -import hu.bme.mit.theta.solver.z3.Z3SolverFactory; +import hu.bme.mit.theta.solver.*; public final class CfaTraceConcretizer { private CfaTraceConcretizer() { } - public static Trace, CfaAction> concretize(final Trace, CfaAction> trace) { + public static Trace, CfaAction> concretize( + final Trace, CfaAction> trace, SolverFactory solverFactory) { final ExprTraceChecker checker = ExprTraceFwBinItpChecker.create(BoolExprs.True(), - BoolExprs.True(), Z3SolverFactory.getInstace().createItpSolver()); + BoolExprs.True(), solverFactory.createItpSolver()); final ExprTraceStatus status = checker.check(trace); checkArgument(status.isFeasible(), "Infeasible trace."); final Trace valuations = status.asFeasible().getValuations(); diff --git a/subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/analysis/CfaTransFunc.java b/subprojects/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/CfaTransFunc.java similarity index 100% rename from subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/analysis/CfaTransFunc.java rename to subprojects/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/CfaTransFunc.java diff --git a/subprojects/cfa/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 similarity index 100% rename from subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/analysis/DistToErrComparator.java rename to subprojects/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/DistToErrComparator.java diff --git a/subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/tool/Config.java b/subprojects/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/config/CfaConfig.java similarity index 81% rename from subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/tool/Config.java rename to subprojects/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/config/CfaConfig.java index 2e3d86119b..3ab1ad60b6 100644 --- a/subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/tool/Config.java +++ b/subprojects/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/config/CfaConfig.java @@ -13,7 +13,7 @@ * See the License for the specific language governing permissions and * limitations under the License. */ -package hu.bme.mit.theta.cfa.tool; +package hu.bme.mit.theta.cfa.analysis.config; import hu.bme.mit.theta.analysis.Action; import hu.bme.mit.theta.analysis.Prec; @@ -21,18 +21,18 @@ import hu.bme.mit.theta.analysis.algorithm.SafetyChecker; import hu.bme.mit.theta.analysis.algorithm.SafetyResult; -public final class Config { +public final class CfaConfig { private final SafetyChecker checker; private final P initPrec; - private Config(final SafetyChecker checker, final P initPrec) { + private CfaConfig(final SafetyChecker checker, final P initPrec) { this.checker = checker; this.initPrec = initPrec; } - public static Config create( + public static CfaConfig create( final SafetyChecker checker, final P initPrec) { - return new Config<>(checker, initPrec); + return new CfaConfig<>(checker, initPrec); } public SafetyResult check() { diff --git a/subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/tool/CfaConfigBuilder.java b/subprojects/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/config/CfaConfigBuilder.java similarity index 94% rename from subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/tool/CfaConfigBuilder.java rename to subprojects/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/config/CfaConfigBuilder.java index 89d4974405..3b39a8f740 100644 --- a/subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/tool/CfaConfigBuilder.java +++ b/subprojects/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/config/CfaConfigBuilder.java @@ -13,7 +13,7 @@ * See the License for the specific language governing permissions and * limitations under the License. */ -package hu.bme.mit.theta.cfa.tool; +package hu.bme.mit.theta.cfa.analysis.config; import static hu.bme.mit.theta.core.type.booltype.BoolExprs.True; @@ -55,11 +55,7 @@ import hu.bme.mit.theta.analysis.pred.PredState; import hu.bme.mit.theta.analysis.waitlist.PriorityWaitlist; import hu.bme.mit.theta.cfa.CFA; -import hu.bme.mit.theta.cfa.analysis.CfaAction; -import hu.bme.mit.theta.cfa.analysis.CfaAnalysis; -import hu.bme.mit.theta.cfa.analysis.CfaPrec; -import hu.bme.mit.theta.cfa.analysis.CfaState; -import hu.bme.mit.theta.cfa.analysis.DistToErrComparator; +import hu.bme.mit.theta.cfa.analysis.*; import hu.bme.mit.theta.cfa.analysis.initprec.CfaAllVarsInitPrec; import hu.bme.mit.theta.cfa.analysis.initprec.CfaEmptyInitPrec; import hu.bme.mit.theta.cfa.analysis.initprec.CfaInitPrec; @@ -75,7 +71,6 @@ import hu.bme.mit.theta.common.logging.NullLogger; import hu.bme.mit.theta.solver.ItpSolver; import hu.bme.mit.theta.solver.SolverFactory; -import hu.bme.mit.theta.solver.z3.Z3SolverFactory; public class CfaConfigBuilder { public enum Domain { @@ -188,7 +183,7 @@ private InitPrec(final CfaInitPrec builder) { } private Logger logger = NullLogger.getInstance(); - private SolverFactory solverFactory = Z3SolverFactory.getInstace(); + private final SolverFactory solverFactory; private final Domain domain; private final Refinement refinement; private Search search = Search.BFS; @@ -198,9 +193,10 @@ private InitPrec(final CfaInitPrec builder) { private int maxEnum = 0; private InitPrec initPrec = InitPrec.EMPTY; - public CfaConfigBuilder(final Domain domain, final Refinement refinement) { + public CfaConfigBuilder(final Domain domain, final Refinement refinement, final SolverFactory solverFactory) { this.domain = domain; this.refinement = refinement; + this.solverFactory = solverFactory; } public CfaConfigBuilder logger(final Logger logger) { @@ -208,11 +204,6 @@ public CfaConfigBuilder logger(final Logger logger) { return this; } - public CfaConfigBuilder solverFactory(final SolverFactory solverFactory) { - this.solverFactory = solverFactory; - return this; - } - public CfaConfigBuilder search(final Search search) { this.search = search; return this; @@ -243,7 +234,7 @@ public CfaConfigBuilder initPrec(final InitPrec initPrec) { return this; } - public Config build(final CFA cfa) { + public CfaConfig build(final CFA cfa) { final ItpSolver solver = solverFactory.createItpSolver(); final CfaLts lts = encoding.getLts(); @@ -285,7 +276,7 @@ public CfaConfigBuilder initPrec(final InitPrec initPrec) { final CfaPrec prec = precGranularity.createPrec(initPrec.builder.createExpl(cfa)); - return Config.create(checker, prec); + return CfaConfig.create(checker, prec); } else if (domain == Domain.PRED_BOOL || domain == Domain.PRED_CART || domain == Domain.PRED_SPLIT) { PredAbstractor predAbstractor = null; @@ -334,7 +325,7 @@ public CfaConfigBuilder initPrec(final InitPrec initPrec) { final CfaPrec prec = precGranularity.createPrec(initPrec.builder.createPred(cfa)); - return Config.create(checker, prec); + return CfaConfig.create(checker, prec); } else { throw new UnsupportedOperationException(domain + " domain is not supported."); diff --git a/subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/analysis/impact/ImpactChecker.java b/subprojects/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/impact/ImpactChecker.java similarity index 97% rename from subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/analysis/impact/ImpactChecker.java rename to subprojects/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/impact/ImpactChecker.java index eace87ccc3..0d73036e27 100644 --- a/subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/analysis/impact/ImpactChecker.java +++ b/subprojects/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/impact/ImpactChecker.java @@ -33,7 +33,6 @@ import hu.bme.mit.theta.analysis.reachedset.ReachedSet; import hu.bme.mit.theta.analysis.waitlist.FifoWaitlist; import hu.bme.mit.theta.analysis.waitlist.Waitlist; -import hu.bme.mit.theta.cfa.analysis.impact.ImpactRefiner.RefinementResult; public final class ImpactChecker implements SafetyChecker { @@ -155,7 +154,7 @@ private void refine(final ArgNode v) { final ArgTrace argTrace = ArgTrace.to(v); final Trace trace = argTrace.toTrace(); - final RefinementResult refinementResult = refiner.refine(trace); + final ImpactRefiner.RefinementResult refinementResult = refiner.refine(trace); if (refinementResult.isSuccesful()) { final Trace refinedTrace = refinementResult.asSuccesful().getTrace(); diff --git a/subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/analysis/impact/ImpactReachedSet.java b/subprojects/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/impact/ImpactReachedSet.java similarity index 100% rename from subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/analysis/impact/ImpactReachedSet.java rename to subprojects/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/impact/ImpactReachedSet.java diff --git a/subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/analysis/impact/ImpactRefiner.java b/subprojects/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/impact/ImpactRefiner.java similarity index 100% rename from subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/analysis/impact/ImpactRefiner.java rename to subprojects/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/impact/ImpactRefiner.java diff --git a/subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/analysis/impact/PredImpactChecker.java b/subprojects/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/impact/PredImpactChecker.java similarity index 100% rename from subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/analysis/impact/PredImpactChecker.java rename to subprojects/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/impact/PredImpactChecker.java diff --git a/subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/analysis/impact/PredImpactRefiner.java b/subprojects/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/impact/PredImpactRefiner.java similarity index 100% rename from subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/analysis/impact/PredImpactRefiner.java rename to subprojects/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/impact/PredImpactRefiner.java diff --git a/subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/analysis/initprec/CfaAllVarsInitPrec.java b/subprojects/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/initprec/CfaAllVarsInitPrec.java similarity index 100% rename from subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/analysis/initprec/CfaAllVarsInitPrec.java rename to subprojects/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/initprec/CfaAllVarsInitPrec.java diff --git a/subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/analysis/initprec/CfaEmptyInitPrec.java b/subprojects/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/initprec/CfaEmptyInitPrec.java similarity index 100% rename from subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/analysis/initprec/CfaEmptyInitPrec.java rename to subprojects/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/initprec/CfaEmptyInitPrec.java diff --git a/subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/analysis/initprec/CfaInitPrec.java b/subprojects/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/initprec/CfaInitPrec.java similarity index 100% rename from subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/analysis/initprec/CfaInitPrec.java rename to subprojects/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/initprec/CfaInitPrec.java diff --git a/subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/analysis/lts/CfaCachedLts.java b/subprojects/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/lts/CfaCachedLts.java similarity index 100% rename from subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/analysis/lts/CfaCachedLts.java rename to subprojects/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/lts/CfaCachedLts.java diff --git a/subprojects/cfa/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 similarity index 100% rename from subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/analysis/lts/CfaLbeLts.java rename to subprojects/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/lts/CfaLbeLts.java diff --git a/subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/analysis/lts/CfaLts.java b/subprojects/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/lts/CfaLts.java similarity index 100% rename from subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/analysis/lts/CfaLts.java rename to subprojects/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/lts/CfaLts.java diff --git a/subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/analysis/lts/CfaSbeLts.java b/subprojects/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/lts/CfaSbeLts.java similarity index 100% rename from subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/analysis/lts/CfaSbeLts.java rename to subprojects/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/lts/CfaSbeLts.java diff --git a/subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/analysis/lts/package-info.java b/subprojects/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/lts/package-info.java similarity index 100% rename from subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/analysis/lts/package-info.java rename to subprojects/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/lts/package-info.java diff --git a/subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/analysis/package-info.java b/subprojects/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/package-info.java similarity index 100% rename from subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/analysis/package-info.java rename to subprojects/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/package-info.java diff --git a/subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/analysis/prec/GlobalCfaPrec.java b/subprojects/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/prec/GlobalCfaPrec.java similarity index 100% rename from subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/analysis/prec/GlobalCfaPrec.java rename to subprojects/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/prec/GlobalCfaPrec.java diff --git a/subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/analysis/prec/GlobalCfaPrecRefiner.java b/subprojects/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/prec/GlobalCfaPrecRefiner.java similarity index 100% rename from subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/analysis/prec/GlobalCfaPrecRefiner.java rename to subprojects/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/prec/GlobalCfaPrecRefiner.java diff --git a/subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/analysis/prec/LocalCfaPrec.java b/subprojects/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/prec/LocalCfaPrec.java similarity index 100% rename from subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/analysis/prec/LocalCfaPrec.java rename to subprojects/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/prec/LocalCfaPrec.java diff --git a/subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/analysis/prec/LocalCfaPrecRefiner.java b/subprojects/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/prec/LocalCfaPrecRefiner.java similarity index 100% rename from subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/analysis/prec/LocalCfaPrecRefiner.java rename to subprojects/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/prec/LocalCfaPrecRefiner.java diff --git a/subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/analysis/prec/package-info.java b/subprojects/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/prec/package-info.java similarity index 100% rename from subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/analysis/prec/package-info.java rename to subprojects/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/prec/package-info.java diff --git a/subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/utils/CfaVisualizer.java b/subprojects/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/utils/CfaVisualizer.java similarity index 99% rename from subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/utils/CfaVisualizer.java rename to subprojects/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/utils/CfaVisualizer.java index 381bddf49d..94e27f7e15 100644 --- a/subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/utils/CfaVisualizer.java +++ b/subprojects/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/utils/CfaVisualizer.java @@ -13,7 +13,7 @@ * See the License for the specific language governing permissions and * limitations under the License. */ -package hu.bme.mit.theta.cfa.utils; +package hu.bme.mit.theta.cfa.analysis.utils; import java.awt.Color; import java.util.HashMap; diff --git a/subprojects/cfa/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 similarity index 97% rename from subprojects/cfa/src/test/java/hu/bme/mit/theta/cfa/analysis/DistanceToErrorLocComparatorTest.java rename to subprojects/cfa-analysis/src/test/java/hu/bme/mit/theta/cfa/analysis/DistanceToErrorLocComparatorTest.java index dc261ef933..9035765ecf 100644 --- a/subprojects/cfa/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 @@ -23,7 +23,6 @@ import hu.bme.mit.theta.cfa.CFA; import hu.bme.mit.theta.cfa.CFA.Builder; import hu.bme.mit.theta.cfa.CFA.Loc; -import hu.bme.mit.theta.cfa.analysis.DistToErrComparator; import hu.bme.mit.theta.core.stmt.Stmt; import hu.bme.mit.theta.core.stmt.Stmts; import hu.bme.mit.theta.core.type.booltype.BoolExprs; diff --git a/subprojects/cfa/src/test/java/hu/bme/mit/theta/cfa/analysis/LocPrecTest.java b/subprojects/cfa-analysis/src/test/java/hu/bme/mit/theta/cfa/analysis/LocPrecTest.java similarity index 100% rename from subprojects/cfa/src/test/java/hu/bme/mit/theta/cfa/analysis/LocPrecTest.java rename to subprojects/cfa-analysis/src/test/java/hu/bme/mit/theta/cfa/analysis/LocPrecTest.java diff --git a/subprojects/cfa/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 similarity index 100% rename from subprojects/cfa/src/test/java/hu/bme/mit/theta/cfa/analysis/impact/CfaPredImpactCheckerTest.java rename to subprojects/cfa-analysis/src/test/java/hu/bme/mit/theta/cfa/analysis/impact/CfaPredImpactCheckerTest.java diff --git a/subprojects/cfa-analysis/src/test/resources/counter5_true.cfa b/subprojects/cfa-analysis/src/test/resources/counter5_true.cfa new file mode 100644 index 0000000000..05bfaee0ca --- /dev/null +++ b/subprojects/cfa-analysis/src/test/resources/counter5_true.cfa @@ -0,0 +1,17 @@ +main process cfa { + var x : int + + init loc L0 + loc L1 + loc L2 + loc L3 + final loc END + error loc ERR + + L0 -> L1 { x := 0 } + L1 -> L2 { assume x < 5 } + L1 -> L3 { assume not (x < 5) } + L2 -> L1 { x := x + 1 } + L3 -> END { assume x <= 5 } + L3 -> ERR { assume not (x <= 5) } +} \ No newline at end of file diff --git a/subprojects/cfa-cli/build.gradle.kts b/subprojects/cfa-cli/build.gradle.kts new file mode 100644 index 0000000000..2d7a900bde --- /dev/null +++ b/subprojects/cfa-cli/build.gradle.kts @@ -0,0 +1,14 @@ +plugins { + id("java-common") + id("cli-tool") +} + +dependencies { + compile(project(":theta-cfa")) + compile(project(":theta-cfa-analysis")) + compile(project(":theta-solver-z3")) +} + +application { + mainClassName = "hu.bme.mit.theta.cfa.cli.CfaCli" +} diff --git a/subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/tool/CfaCli.java b/subprojects/cfa-cli/src/main/java/hu/bme/mit/theta/cfa/cli/CfaCli.java similarity index 85% rename from subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/tool/CfaCli.java rename to subprojects/cfa-cli/src/main/java/hu/bme/mit/theta/cfa/cli/CfaCli.java index 6ee1c21ab8..611a8f878d 100644 --- a/subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/tool/CfaCli.java +++ b/subprojects/cfa-cli/src/main/java/hu/bme/mit/theta/cfa/cli/CfaCli.java @@ -13,7 +13,7 @@ * See the License for the specific language governing permissions and * limitations under the License. */ -package hu.bme.mit.theta.cfa.tool; +package hu.bme.mit.theta.cfa.cli; import java.io.FileInputStream; import java.io.IOException; @@ -36,26 +36,31 @@ import hu.bme.mit.theta.cfa.analysis.CfaAction; import hu.bme.mit.theta.cfa.analysis.CfaState; import hu.bme.mit.theta.cfa.analysis.CfaTraceConcretizer; +import hu.bme.mit.theta.cfa.analysis.config.CfaConfig; +import hu.bme.mit.theta.cfa.analysis.config.CfaConfigBuilder; +import hu.bme.mit.theta.cfa.analysis.config.CfaConfigBuilder.Domain; +import hu.bme.mit.theta.cfa.analysis.config.CfaConfigBuilder.Encoding; +import hu.bme.mit.theta.cfa.analysis.config.CfaConfigBuilder.InitPrec; +import hu.bme.mit.theta.cfa.analysis.config.CfaConfigBuilder.PrecGranularity; +import hu.bme.mit.theta.cfa.analysis.config.CfaConfigBuilder.PredSplit; +import hu.bme.mit.theta.cfa.analysis.config.CfaConfigBuilder.Refinement; +import hu.bme.mit.theta.cfa.analysis.config.CfaConfigBuilder.Search; import hu.bme.mit.theta.cfa.dsl.CfaDslManager; -import hu.bme.mit.theta.cfa.tool.CfaConfigBuilder.Domain; -import hu.bme.mit.theta.cfa.tool.CfaConfigBuilder.Encoding; -import hu.bme.mit.theta.cfa.tool.CfaConfigBuilder.InitPrec; -import hu.bme.mit.theta.cfa.tool.CfaConfigBuilder.PrecGranularity; -import hu.bme.mit.theta.cfa.tool.CfaConfigBuilder.PredSplit; -import hu.bme.mit.theta.cfa.tool.CfaConfigBuilder.Refinement; -import hu.bme.mit.theta.cfa.tool.CfaConfigBuilder.Search; import hu.bme.mit.theta.common.logging.ConsoleLogger; import hu.bme.mit.theta.common.logging.Logger; import hu.bme.mit.theta.common.logging.Logger.Level; 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.solver.*; +import hu.bme.mit.theta.solver.z3.*; /** * A command line interface for running a CEGAR configuration on a CFA. */ public class CfaCli { - private static final String JAR_NAME = "theta-cfa.jar"; + private static final String JAR_NAME = "theta-cfa-cli.jar"; + private final SolverFactory solverFactory = Z3SolverFactory.getInstace(); private final String[] args; private final TableWriter writer; @@ -129,7 +134,7 @@ private void run() { try { final Stopwatch sw = Stopwatch.createStarted(); final CFA cfa = loadModel(); - final Config configuration = buildConfiguration(cfa); + final CfaConfig configuration = buildConfiguration(cfa); final SafetyResult status = configuration.check(); sw.stop(); printResult(status, cfa, sw.elapsed(TimeUnit.MILLISECONDS)); @@ -160,8 +165,8 @@ private CFA loadModel() throws IOException { } } - private Config buildConfiguration(final CFA cfa) { - return new CfaConfigBuilder(domain, refinement).precGranularity(precGranularity).search(search) + private CfaConfig buildConfiguration(final CFA cfa) { + return new CfaConfigBuilder(domain, refinement, solverFactory).precGranularity(precGranularity).search(search) .predSplit(predSplit).encoding(encoding).maxEnum(maxEnum).initPrec(initPrec).logger(logger).build(cfa); } @@ -201,7 +206,7 @@ private void printError(final Throwable ex) { private void writeCex(final Unsafe status) { @SuppressWarnings("unchecked") final Trace, CfaAction> trace = (Trace, CfaAction>) status.getTrace(); - final Trace, CfaAction> concrTrace = CfaTraceConcretizer.concretize(trace); + final Trace, CfaAction> concrTrace = CfaTraceConcretizer.concretize(trace, solverFactory); logger.write(Level.RESULT, "%s", concrTrace); } } diff --git a/subprojects/cfa-metrics/build.gradle.kts b/subprojects/cfa-metrics/build.gradle.kts new file mode 100644 index 0000000000..bfa75701f8 --- /dev/null +++ b/subprojects/cfa-metrics/build.gradle.kts @@ -0,0 +1,12 @@ +plugins { + id("java-common") + id("cli-tool") +} + +dependencies { + compile(project(":theta-cfa")) +} + +application { + mainClassName = "hu.bme.mit.theta.cfa.metrics.CfaMetrics" +} diff --git a/subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/tool/CfaMetrics.java b/subprojects/cfa-metrics/src/main/java/hu/bme/mit/theta/cfa/metrics/CfaMetrics.java similarity index 98% rename from subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/tool/CfaMetrics.java rename to subprojects/cfa-metrics/src/main/java/hu/bme/mit/theta/cfa/metrics/CfaMetrics.java index 5f10b1465d..219c538ebd 100644 --- a/subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/tool/CfaMetrics.java +++ b/subprojects/cfa-metrics/src/main/java/hu/bme/mit/theta/cfa/metrics/CfaMetrics.java @@ -1,4 +1,4 @@ -package hu.bme.mit.theta.cfa.tool; +package hu.bme.mit.theta.cfa.metrics; import java.io.FileInputStream; import java.io.IOException; diff --git a/subprojects/cfa/.gitignore b/subprojects/cfa/.gitignore deleted file mode 100644 index 65776c32fc..0000000000 --- a/subprojects/cfa/.gitignore +++ /dev/null @@ -1 +0,0 @@ -/bin/ \ No newline at end of file diff --git a/subprojects/cfa/build.gradle b/subprojects/cfa/build.gradle deleted file mode 100644 index 7b48c9f37d..0000000000 --- a/subprojects/cfa/build.gradle +++ /dev/null @@ -1,36 +0,0 @@ -apply plugin: 'antlr' -apply from: "${rootDir}/common-methods.gradle" - -dependencies { - compile project(':theta-common') - compile project(':theta-core') - compile project(':theta-analysis') - compile project(':theta-solver-z3') - antlr group: 'org.antlr', name: 'antlr4', version: antlrVersion - compile group: 'com.beust', name: 'jcommander', version: jcommanderVersion - compile group: 'com.google.guava', name: 'guava', version: guavaVersion - testCompile group: 'junit', name: 'junit', version: junitVersion -} - -generateGrammarSource { - arguments += ['-package', 'hu.bme.mit.theta.cfa.dsl.gen'] - arguments += ['-Werror', '-visitor'] - doLast { - copy { - from outputDirectory - into 'src/main/java/hu/bme/mit/theta/cfa/dsl/gen' - } - } -} - -sourceSets { - main { - java { - srcDirs = ['src/main/java'] - } - } -} - -createJarTask('theta-cfa-cli', 'hu.bme.mit.theta.cfa.tool.CfaCli', 'theta-cfa-cli') -createJarTask('cfa2dot', 'hu.bme.mit.theta.cfa.tool.CfaToDotMain', 'cfa2dot') -createJarTask('cfa-metrics', 'hu.bme.mit.theta.cfa.tool.CfaMetrics', 'cfa-metrics') diff --git a/subprojects/cfa/build.gradle.kts b/subprojects/cfa/build.gradle.kts new file mode 100644 index 0000000000..52019ac21a --- /dev/null +++ b/subprojects/cfa/build.gradle.kts @@ -0,0 +1,9 @@ +plugins { + id("java-common") + id("antlr-grammar") +} + +dependencies { + compile(project(":theta-common")) + compile(project(":theta-core")) +} diff --git a/subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/dsl/gen/.gitignore b/subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/dsl/gen/.gitignore deleted file mode 100644 index d6b7ef32c8..0000000000 --- a/subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/dsl/gen/.gitignore +++ /dev/null @@ -1,2 +0,0 @@ -* -!.gitignore diff --git a/subprojects/cfa2dot/build.gradle.kts b/subprojects/cfa2dot/build.gradle.kts new file mode 100644 index 0000000000..fa9570823c --- /dev/null +++ b/subprojects/cfa2dot/build.gradle.kts @@ -0,0 +1,12 @@ +plugins { + id("java-common") + id("cli-tool") +} + +dependencies { + compile(project(":theta-cfa-analysis")) +} + +application { + mainClassName = "hu.bme.mit.theta.cfa.cfa2dot.CfaToDotMain" +} diff --git a/subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/tool/CfaToDotMain.java b/subprojects/cfa2dot/src/main/java/hu/bme/mit/theta/cfa/cfa2dot/CfaToDotMain.java similarity index 94% rename from subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/tool/CfaToDotMain.java rename to subprojects/cfa2dot/src/main/java/hu/bme/mit/theta/cfa/cfa2dot/CfaToDotMain.java index 66a0402765..4d8e96c8bb 100644 --- a/subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/tool/CfaToDotMain.java +++ b/subprojects/cfa2dot/src/main/java/hu/bme/mit/theta/cfa/cfa2dot/CfaToDotMain.java @@ -13,7 +13,7 @@ * See the License for the specific language governing permissions and * limitations under the License. */ -package hu.bme.mit.theta.cfa.tool; +package hu.bme.mit.theta.cfa.cfa2dot; import java.io.FileInputStream; import java.io.IOException; @@ -25,12 +25,12 @@ import hu.bme.mit.theta.cfa.CFA; import hu.bme.mit.theta.cfa.dsl.CfaDslManager; -import hu.bme.mit.theta.cfa.utils.CfaVisualizer; +import hu.bme.mit.theta.cfa.analysis.utils.CfaVisualizer; import hu.bme.mit.theta.common.visualization.Graph; import hu.bme.mit.theta.common.visualization.writer.GraphvizWriter; public final class CfaToDotMain { - private static final String JAR_NAME = "cfa2dot.jar"; + private static final String JAR_NAME = "theta-cfa2dot.jar"; private final String[] args; @Parameter(names = { "-c", "--cfa" }, description = "Path of the input cfa", required = true) diff --git a/subprojects/common/.gitignore b/subprojects/common/.gitignore deleted file mode 100644 index 65776c32fc..0000000000 --- a/subprojects/common/.gitignore +++ /dev/null @@ -1 +0,0 @@ -/bin/ \ No newline at end of file diff --git a/subprojects/common/build.gradle b/subprojects/common/build.gradle deleted file mode 100644 index f849a26fa6..0000000000 --- a/subprojects/common/build.gradle +++ /dev/null @@ -1,4 +0,0 @@ -dependencies { - compile group: 'com.google.guava', name: 'guava', version: guavaVersion - testCompile group: 'junit', name: 'junit', version: junitVersion -} diff --git a/subprojects/common/build.gradle.kts b/subprojects/common/build.gradle.kts new file mode 100644 index 0000000000..6e1ca82ef9 --- /dev/null +++ b/subprojects/common/build.gradle.kts @@ -0,0 +1,3 @@ +plugins { + id("java-common") +} diff --git a/subprojects/core/.gitignore b/subprojects/core/.gitignore deleted file mode 100644 index 65776c32fc..0000000000 --- a/subprojects/core/.gitignore +++ /dev/null @@ -1 +0,0 @@ -/bin/ \ No newline at end of file diff --git a/subprojects/core/build.gradle b/subprojects/core/build.gradle deleted file mode 100644 index 9032dc2baf..0000000000 --- a/subprojects/core/build.gradle +++ /dev/null @@ -1,29 +0,0 @@ -apply plugin: 'antlr' -apply plugin: 'jacoco' - -dependencies { - compile project(':theta-common') - antlr group: 'org.antlr', name: 'antlr4', version: antlrVersion - compile group: 'org.antlr', name: 'antlr4-runtime', version: antlrVersion - compile group: 'com.google.guava', name: 'guava', version: guavaVersion - testCompile group: 'junit', name: 'junit', version: junitVersion -} - -generateGrammarSource { - arguments += ['-package', 'hu.bme.mit.theta.core.dsl.gen'] - arguments += ['-Werror', '-visitor'] - doLast { - copy { - from outputDirectory - into 'src/main/java/hu/bme/mit/theta/core/dsl/gen' - } - } -} - -sourceSets { - main { - java { - srcDirs = ['src/main/java'] - } - } -} diff --git a/subprojects/core/build.gradle.kts b/subprojects/core/build.gradle.kts new file mode 100644 index 0000000000..b7330c6d78 --- /dev/null +++ b/subprojects/core/build.gradle.kts @@ -0,0 +1,8 @@ +plugins { + id("java-common") + id("antlr-grammar") +} + +dependencies { + compile(project(":theta-common")) +} diff --git a/subprojects/core/src/main/java/hu/bme/mit/theta/core/dsl/gen/.gitignore b/subprojects/core/src/main/java/hu/bme/mit/theta/core/dsl/gen/.gitignore deleted file mode 100644 index d6b7ef32c8..0000000000 --- a/subprojects/core/src/main/java/hu/bme/mit/theta/core/dsl/gen/.gitignore +++ /dev/null @@ -1,2 +0,0 @@ -* -!.gitignore diff --git a/subprojects/solver-z3/.gitignore b/subprojects/solver-z3/.gitignore deleted file mode 100644 index 65776c32fc..0000000000 --- a/subprojects/solver-z3/.gitignore +++ /dev/null @@ -1 +0,0 @@ -/bin/ \ No newline at end of file diff --git a/subprojects/solver-z3/build.gradle b/subprojects/solver-z3/build.gradle deleted file mode 100644 index 699c41cbce..0000000000 --- a/subprojects/solver-z3/build.gradle +++ /dev/null @@ -1,8 +0,0 @@ -dependencies { - compile project(':theta-common') - compile project(':theta-core') - compile project(':theta-solver') - compile group: 'z3', name: 'com.microsoft.z3', version: z3Version - compile group: 'com.google.guava', name: 'guava', version: guavaVersion - testCompile group: 'junit', name: 'junit', version: junitVersion -} diff --git a/subprojects/solver-z3/build.gradle.kts b/subprojects/solver-z3/build.gradle.kts new file mode 100644 index 0000000000..aea13bc5a4 --- /dev/null +++ b/subprojects/solver-z3/build.gradle.kts @@ -0,0 +1,10 @@ +plugins { + id("java-common") +} + +dependencies { + compile(project(":theta-common")) + compile(project(":theta-core")) + compile(project(":theta-solver")) + implementation(Deps.z3) +} diff --git a/subprojects/solver/.gitignore b/subprojects/solver/.gitignore deleted file mode 100644 index 65776c32fc..0000000000 --- a/subprojects/solver/.gitignore +++ /dev/null @@ -1 +0,0 @@ -/bin/ \ No newline at end of file diff --git a/subprojects/solver/build.gradle b/subprojects/solver/build.gradle deleted file mode 100644 index 79dcee43ef..0000000000 --- a/subprojects/solver/build.gradle +++ /dev/null @@ -1,6 +0,0 @@ -dependencies { - compile project(':theta-common') - compile project(':theta-core') - compile group: 'com.google.guava', name: 'guava', version: guavaVersion - testCompile group: 'junit', name: 'junit', version: junitVersion -} diff --git a/subprojects/solver/build.gradle.kts b/subprojects/solver/build.gradle.kts new file mode 100644 index 0000000000..4dea6f74cd --- /dev/null +++ b/subprojects/solver/build.gradle.kts @@ -0,0 +1,8 @@ +plugins { + id("java-common") +} + +dependencies { + compile(project(":theta-common")) + compile(project(":theta-core")) +} diff --git a/subprojects/sts-analysis/build.gradle.kts b/subprojects/sts-analysis/build.gradle.kts new file mode 100644 index 0000000000..8305c06389 --- /dev/null +++ b/subprojects/sts-analysis/build.gradle.kts @@ -0,0 +1,11 @@ +plugins { + id("java-common") +} + +dependencies { + compile(project(":theta-analysis")) + compile(project(":theta-common")) + compile(project(":theta-core")) + compile(project(":theta-sts")) + testImplementation(project(":theta-solver-z3")) +} diff --git a/subprojects/sts/src/main/java/hu/bme/mit/theta/sts/analysis/StsAction.java b/subprojects/sts-analysis/src/main/java/hu.bme.mit.theta.sts/analysis/StsAction.java similarity index 100% rename from subprojects/sts/src/main/java/hu/bme/mit/theta/sts/analysis/StsAction.java rename to subprojects/sts-analysis/src/main/java/hu.bme.mit.theta.sts/analysis/StsAction.java diff --git a/subprojects/sts/src/main/java/hu/bme/mit/theta/sts/analysis/StsLts.java b/subprojects/sts-analysis/src/main/java/hu.bme.mit.theta.sts/analysis/StsLts.java similarity index 100% rename from subprojects/sts/src/main/java/hu/bme/mit/theta/sts/analysis/StsLts.java rename to subprojects/sts-analysis/src/main/java/hu.bme.mit.theta.sts/analysis/StsLts.java diff --git a/subprojects/sts/src/main/java/hu/bme/mit/theta/sts/analysis/StsTraceConcretizer.java b/subprojects/sts-analysis/src/main/java/hu.bme.mit.theta.sts/analysis/StsTraceConcretizer.java similarity index 87% rename from subprojects/sts/src/main/java/hu/bme/mit/theta/sts/analysis/StsTraceConcretizer.java rename to subprojects/sts-analysis/src/main/java/hu.bme.mit.theta.sts/analysis/StsTraceConcretizer.java index f34e52288c..bd641e2c3b 100644 --- a/subprojects/sts/src/main/java/hu/bme/mit/theta/sts/analysis/StsTraceConcretizer.java +++ b/subprojects/sts-analysis/src/main/java/hu.bme.mit.theta.sts/analysis/StsTraceConcretizer.java @@ -26,16 +26,17 @@ import hu.bme.mit.theta.analysis.expr.refinement.ItpRefutation; import hu.bme.mit.theta.core.model.Valuation; import hu.bme.mit.theta.core.type.booltype.BoolExprs; -import hu.bme.mit.theta.solver.z3.Z3SolverFactory; +import hu.bme.mit.theta.solver.*; import hu.bme.mit.theta.sts.STS; public final class StsTraceConcretizer { private StsTraceConcretizer() { } - public static Trace concretize(final STS sts, final Trace trace) { + public static Trace concretize( + final STS sts, final Trace trace, final SolverFactory solverFactory) { final ExprTraceChecker checker = ExprTraceFwBinItpChecker.create(sts.getInit(), - BoolExprs.Not(sts.getProp()), Z3SolverFactory.getInstace().createItpSolver()); + BoolExprs.Not(sts.getProp()), solverFactory.createItpSolver()); final ExprTraceStatus status = checker.check(trace); checkArgument(status.isFeasible(), "Infeasible trace."); final Trace valuations = status.asFeasible().getValuations(); diff --git a/subprojects/sts/src/main/java/hu/bme/mit/theta/sts/tool/Config.java b/subprojects/sts-analysis/src/main/java/hu.bme.mit.theta.sts/analysis/config/StsConfig.java similarity index 81% rename from subprojects/sts/src/main/java/hu/bme/mit/theta/sts/tool/Config.java rename to subprojects/sts-analysis/src/main/java/hu.bme.mit.theta.sts/analysis/config/StsConfig.java index 2f424a0bde..7c72f00770 100644 --- a/subprojects/sts/src/main/java/hu/bme/mit/theta/sts/tool/Config.java +++ b/subprojects/sts-analysis/src/main/java/hu.bme.mit.theta.sts/analysis/config/StsConfig.java @@ -13,7 +13,7 @@ * See the License for the specific language governing permissions and * limitations under the License. */ -package hu.bme.mit.theta.sts.tool; +package hu.bme.mit.theta.sts.analysis.config; import hu.bme.mit.theta.analysis.Action; import hu.bme.mit.theta.analysis.Prec; @@ -21,18 +21,18 @@ import hu.bme.mit.theta.analysis.algorithm.SafetyChecker; import hu.bme.mit.theta.analysis.algorithm.SafetyResult; -public final class Config { +public final class StsConfig { private final SafetyChecker checker; private final P initPrec; - private Config(final SafetyChecker checker, final P initPrec) { + private StsConfig(final SafetyChecker checker, final P initPrec) { this.checker = checker; this.initPrec = initPrec; } - public static Config create( + public static StsConfig create( final SafetyChecker checker, final P initPrec) { - return new Config<>(checker, initPrec); + return new StsConfig<>(checker, initPrec); } public SafetyResult check() { diff --git a/subprojects/sts/src/main/java/hu/bme/mit/theta/sts/tool/StsConfigBuilder.java b/subprojects/sts-analysis/src/main/java/hu.bme.mit.theta.sts/analysis/config/StsConfigBuilder.java similarity index 95% rename from subprojects/sts/src/main/java/hu/bme/mit/theta/sts/tool/StsConfigBuilder.java rename to subprojects/sts-analysis/src/main/java/hu.bme.mit.theta.sts/analysis/config/StsConfigBuilder.java index cbda17029d..54c03fa15e 100644 --- a/subprojects/sts/src/main/java/hu/bme/mit/theta/sts/tool/StsConfigBuilder.java +++ b/subprojects/sts-analysis/src/main/java/hu.bme.mit.theta.sts/analysis/config/StsConfigBuilder.java @@ -13,7 +13,7 @@ * See the License for the specific language governing permissions and * limitations under the License. */ -package hu.bme.mit.theta.sts.tool; +package hu.bme.mit.theta.sts.analysis.config; import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Not; @@ -64,7 +64,6 @@ import hu.bme.mit.theta.core.type.booltype.BoolType; import hu.bme.mit.theta.solver.ItpSolver; import hu.bme.mit.theta.solver.SolverFactory; -import hu.bme.mit.theta.solver.z3.Z3SolverFactory; import hu.bme.mit.theta.sts.STS; import hu.bme.mit.theta.sts.analysis.StsAction; import hu.bme.mit.theta.sts.analysis.StsLts; @@ -121,16 +120,17 @@ private InitPrec(final StsInitPrec builder) { }; private Logger logger = NullLogger.getInstance(); - private SolverFactory solverFactory = Z3SolverFactory.getInstace(); + private final SolverFactory solverFactory; private final Domain domain; private final Refinement refinement; private Search search = Search.BFS; private PredSplit predSplit = PredSplit.WHOLE; private InitPrec initPrec = InitPrec.EMPTY; - public StsConfigBuilder(final Domain domain, final Refinement refinement) { + public StsConfigBuilder(final Domain domain, final Refinement refinement, final SolverFactory solverFactory) { this.domain = domain; this.refinement = refinement; + this.solverFactory = solverFactory; } public StsConfigBuilder logger(final Logger logger) { @@ -138,11 +138,6 @@ public StsConfigBuilder logger(final Logger logger) { return this; } - public StsConfigBuilder solverFactory(final SolverFactory solverFactory) { - this.solverFactory = solverFactory; - return this; - } - public StsConfigBuilder search(final Search search) { this.search = search; return this; @@ -162,7 +157,7 @@ public InitPrec getInitPrec() { return initPrec; } - public Config build(final STS sts) { + public StsConfig build(final STS sts) { final ItpSolver solver = solverFactory.createItpSolver(); final LTS lts = StsLts.create(sts); final Expr init = sts.getInit(); @@ -203,7 +198,7 @@ public InitPrec getInitPrec() { final SafetyChecker checker = CegarChecker.create(abstractor, refiner, logger); final ExplPrec prec = initPrec.builder.createExpl(sts); - return Config.create(checker, prec); + return StsConfig.create(checker, prec); } else if (domain == Domain.PRED_BOOL || domain == Domain.PRED_CART || domain == Domain.PRED_SPLIT) { PredAbstractor predAbstractor = null; @@ -250,7 +245,7 @@ public InitPrec getInitPrec() { logger); final PredPrec prec = initPrec.builder.createPred(sts); - return Config.create(checker, prec); + return StsConfig.create(checker, prec); } else { throw new UnsupportedOperationException(domain + " domain is not supported."); } diff --git a/subprojects/sts/src/main/java/hu/bme/mit/theta/sts/analysis/initprec/StsEmptyInitPrec.java b/subprojects/sts-analysis/src/main/java/hu.bme.mit.theta.sts/analysis/initprec/StsEmptyInitPrec.java similarity index 100% rename from subprojects/sts/src/main/java/hu/bme/mit/theta/sts/analysis/initprec/StsEmptyInitPrec.java rename to subprojects/sts-analysis/src/main/java/hu.bme.mit.theta.sts/analysis/initprec/StsEmptyInitPrec.java diff --git a/subprojects/sts/src/main/java/hu/bme/mit/theta/sts/analysis/initprec/StsInitPrec.java b/subprojects/sts-analysis/src/main/java/hu.bme.mit.theta.sts/analysis/initprec/StsInitPrec.java similarity index 100% rename from subprojects/sts/src/main/java/hu/bme/mit/theta/sts/analysis/initprec/StsInitPrec.java rename to subprojects/sts-analysis/src/main/java/hu.bme.mit.theta.sts/analysis/initprec/StsInitPrec.java diff --git a/subprojects/sts/src/main/java/hu/bme/mit/theta/sts/analysis/initprec/StsPropInitPrec.java b/subprojects/sts-analysis/src/main/java/hu.bme.mit.theta.sts/analysis/initprec/StsPropInitPrec.java similarity index 100% rename from subprojects/sts/src/main/java/hu/bme/mit/theta/sts/analysis/initprec/StsPropInitPrec.java rename to subprojects/sts-analysis/src/main/java/hu.bme.mit.theta.sts/analysis/initprec/StsPropInitPrec.java diff --git a/subprojects/sts/src/main/java/hu/bme/mit/theta/sts/analysis/package-info.java b/subprojects/sts-analysis/src/main/java/hu.bme.mit.theta.sts/analysis/package-info.java similarity index 100% rename from subprojects/sts/src/main/java/hu/bme/mit/theta/sts/analysis/package-info.java rename to subprojects/sts-analysis/src/main/java/hu.bme.mit.theta.sts/analysis/package-info.java diff --git a/subprojects/sts/src/main/java/hu/bme/mit/theta/sts/utils/StsTraceVisualizer.java b/subprojects/sts-analysis/src/main/java/hu.bme.mit.theta.sts/analysis/utils/StsTraceVisualizer.java similarity index 95% rename from subprojects/sts/src/main/java/hu/bme/mit/theta/sts/utils/StsTraceVisualizer.java rename to subprojects/sts-analysis/src/main/java/hu.bme.mit.theta.sts/analysis/utils/StsTraceVisualizer.java index 51189a6a4e..76d121b720 100644 --- a/subprojects/sts/src/main/java/hu/bme/mit/theta/sts/utils/StsTraceVisualizer.java +++ b/subprojects/sts-analysis/src/main/java/hu.bme.mit.theta.sts/analysis/utils/StsTraceVisualizer.java @@ -1,4 +1,4 @@ -package hu.bme.mit.theta.sts.utils; +package hu.bme.mit.theta.sts.analysis.utils; import java.util.LinkedHashSet; import java.util.Optional; diff --git a/subprojects/sts/src/test/java/hu/bme/mit/theta/sts/analysis/StsExplTest.java b/subprojects/sts-analysis/src/test/java/hu/bme/mit/theta/sts/analysis/StsExplTest.java similarity index 100% rename from subprojects/sts/src/test/java/hu/bme/mit/theta/sts/analysis/StsExplTest.java rename to subprojects/sts-analysis/src/test/java/hu/bme/mit/theta/sts/analysis/StsExplTest.java diff --git a/subprojects/sts/src/test/java/hu/bme/mit/theta/sts/analysis/StsPredTest.java b/subprojects/sts-analysis/src/test/java/hu/bme/mit/theta/sts/analysis/StsPredTest.java similarity index 100% rename from subprojects/sts/src/test/java/hu/bme/mit/theta/sts/analysis/StsPredTest.java rename to subprojects/sts-analysis/src/test/java/hu/bme/mit/theta/sts/analysis/StsPredTest.java diff --git a/subprojects/sts-cli/build.gradle.kts b/subprojects/sts-cli/build.gradle.kts new file mode 100644 index 0000000000..2f8e5d4000 --- /dev/null +++ b/subprojects/sts-cli/build.gradle.kts @@ -0,0 +1,14 @@ +plugins { + id("java-common") + id("cli-tool") +} + +dependencies { + compile(project(":theta-sts")) + compile(project(":theta-sts-analysis")) + compile(project(":theta-solver-z3")) +} + +application { + mainClassName = "hu.bme.mit.theta.sts.cli.StsCli" +} diff --git a/subprojects/sts/src/main/java/hu/bme/mit/theta/sts/tool/StsCli.java b/subprojects/sts-cli/src/main/java/hu/bme/mit/theta/sts/cli/StsCli.java similarity index 88% rename from subprojects/sts/src/main/java/hu/bme/mit/theta/sts/tool/StsCli.java rename to subprojects/sts-cli/src/main/java/hu/bme/mit/theta/sts/cli/StsCli.java index f801638207..2ac77e0a2a 100644 --- a/subprojects/sts/src/main/java/hu/bme/mit/theta/sts/tool/StsCli.java +++ b/subprojects/sts-cli/src/main/java/hu/bme/mit/theta/sts/cli/StsCli.java @@ -13,7 +13,7 @@ * See the License for the specific language governing permissions and * limitations under the License. */ -package hu.bme.mit.theta.sts.tool; +package hu.bme.mit.theta.sts.cli; import java.io.FileInputStream; import java.io.FileNotFoundException; @@ -44,6 +44,8 @@ import hu.bme.mit.theta.common.visualization.writer.GraphvizWriter; import hu.bme.mit.theta.core.type.booltype.BoolExprs; import hu.bme.mit.theta.core.utils.ExprUtils; +import hu.bme.mit.theta.solver.*; +import hu.bme.mit.theta.solver.z3.*; import hu.bme.mit.theta.sts.STS; import hu.bme.mit.theta.sts.StsUtils; import hu.bme.mit.theta.sts.aiger.AigerParser; @@ -52,17 +54,20 @@ import hu.bme.mit.theta.sts.aiger.utils.AigerCoi; import hu.bme.mit.theta.sts.dsl.StsDslManager; import hu.bme.mit.theta.sts.dsl.StsSpec; -import hu.bme.mit.theta.sts.tool.StsConfigBuilder.Domain; -import hu.bme.mit.theta.sts.tool.StsConfigBuilder.InitPrec; -import hu.bme.mit.theta.sts.tool.StsConfigBuilder.PredSplit; -import hu.bme.mit.theta.sts.tool.StsConfigBuilder.Refinement; -import hu.bme.mit.theta.sts.tool.StsConfigBuilder.Search; +import hu.bme.mit.theta.sts.analysis.config.StsConfig; +import hu.bme.mit.theta.sts.analysis.config.StsConfigBuilder; +import hu.bme.mit.theta.sts.analysis.config.StsConfigBuilder.Domain; +import hu.bme.mit.theta.sts.analysis.config.StsConfigBuilder.InitPrec; +import hu.bme.mit.theta.sts.analysis.config.StsConfigBuilder.PredSplit; +import hu.bme.mit.theta.sts.analysis.config.StsConfigBuilder.Refinement; +import hu.bme.mit.theta.sts.analysis.config.StsConfigBuilder.Search; /** * A command line interface for running a CEGAR configuration on an STS. */ public class StsCli { - private static final String JAR_NAME = "theta-sts.jar"; + private static final String JAR_NAME = "theta-sts-cli.jar"; + private final SolverFactory solverFactory = Z3SolverFactory.getInstace(); private final String[] args; private final TableWriter writer; @@ -127,7 +132,7 @@ private void run() { try { final Stopwatch sw = Stopwatch.createStarted(); final STS sts = loadModel(); - final Config configuration = buildConfiguration(sts); + final StsConfig configuration = buildConfiguration(sts); final SafetyResult status = configuration.check(); sw.stop(); printResult(status, sts, sw.elapsed(TimeUnit.MILLISECONDS)); @@ -169,9 +174,9 @@ private STS loadModel() throws IOException { } } - private Config buildConfiguration(final STS sts) { - return new StsConfigBuilder(domain, refinement).initPrec(initPrec).search(search).predSplit(predSplit) - .logger(logger).build(sts); + private StsConfig buildConfiguration(final STS sts) { + return new StsConfigBuilder(domain, refinement, solverFactory).initPrec(initPrec).search(search) + .predSplit(predSplit).logger(logger).build(sts); } private void printResult(final SafetyResult status, final STS sts, final long totalTimeMs) { diff --git a/subprojects/sts/.gitignore b/subprojects/sts/.gitignore deleted file mode 100644 index 65776c32fc..0000000000 --- a/subprojects/sts/.gitignore +++ /dev/null @@ -1 +0,0 @@ -/bin/ \ No newline at end of file diff --git a/subprojects/sts/build.gradle b/subprojects/sts/build.gradle deleted file mode 100644 index 4936342159..0000000000 --- a/subprojects/sts/build.gradle +++ /dev/null @@ -1,34 +0,0 @@ -apply plugin: 'antlr' -apply from: "$rootDir/common-methods.gradle" - -dependencies { - compile project(':theta-common') - compile project(':theta-core') - compile project(':theta-analysis') - compile project(':theta-solver-z3') - antlr group: 'org.antlr', name: 'antlr4', version: antlrVersion - compile group: 'com.beust', name: 'jcommander', version: jcommanderVersion - compile group: 'com.google.guava', name: 'guava', version: guavaVersion - testCompile group: 'junit', name: 'junit', version: junitVersion -} - -generateGrammarSource { - arguments += ["-package", "hu.bme.mit.theta.sts.dsl.gen"] - arguments += ["-Werror", "-visitor"] - doLast { - copy { - from "${buildDir}/generated-src/antlr/main" - into "src/gen/java/hu/bme/mit/theta/sts/dsl/gen" - } - } -} - -sourceSets { - main { - java { - srcDirs = [ "src/main/java", "src/gen/java" ] - } - } -} - -createJarTask("theta-sts-cli", 'hu.bme.mit.theta.sts.tool.StsCli', 'theta-sts-cli') diff --git a/subprojects/sts/build.gradle.kts b/subprojects/sts/build.gradle.kts new file mode 100644 index 0000000000..52019ac21a --- /dev/null +++ b/subprojects/sts/build.gradle.kts @@ -0,0 +1,9 @@ +plugins { + id("java-common") + id("antlr-grammar") +} + +dependencies { + compile(project(":theta-common")) + compile(project(":theta-core")) +} diff --git a/subprojects/sts/src/gen/java/.gitignore b/subprojects/sts/src/gen/java/.gitignore deleted file mode 100644 index d6b7ef32c8..0000000000 --- a/subprojects/sts/src/gen/java/.gitignore +++ /dev/null @@ -1,2 +0,0 @@ -* -!.gitignore diff --git a/subprojects/xta-analysis/build.gradle.kts b/subprojects/xta-analysis/build.gradle.kts new file mode 100644 index 0000000000..7d26311be1 --- /dev/null +++ b/subprojects/xta-analysis/build.gradle.kts @@ -0,0 +1,11 @@ +plugins { + id("java-common") +} + +dependencies { + compile(project(":theta-analysis")) + compile(project(":theta-common")) + compile(project(":theta-core")) + compile(project(":theta-xta")) + testImplementation(project(":theta-solver-z3")) +} diff --git a/subprojects/xta/src/main/java/hu/bme/mit/theta/xta/analysis/XtaAction.java b/subprojects/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/XtaAction.java similarity index 100% rename from subprojects/xta/src/main/java/hu/bme/mit/theta/xta/analysis/XtaAction.java rename to subprojects/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/XtaAction.java diff --git a/subprojects/xta/src/main/java/hu/bme/mit/theta/xta/analysis/XtaAnalysis.java b/subprojects/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/XtaAnalysis.java similarity index 100% rename from subprojects/xta/src/main/java/hu/bme/mit/theta/xta/analysis/XtaAnalysis.java rename to subprojects/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/XtaAnalysis.java diff --git a/subprojects/xta/src/main/java/hu/bme/mit/theta/xta/analysis/XtaInitFunc.java b/subprojects/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/XtaInitFunc.java similarity index 100% rename from subprojects/xta/src/main/java/hu/bme/mit/theta/xta/analysis/XtaInitFunc.java rename to subprojects/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/XtaInitFunc.java diff --git a/subprojects/xta/src/main/java/hu/bme/mit/theta/xta/analysis/XtaLts.java b/subprojects/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/XtaLts.java similarity index 100% rename from subprojects/xta/src/main/java/hu/bme/mit/theta/xta/analysis/XtaLts.java rename to subprojects/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/XtaLts.java diff --git a/subprojects/xta/src/main/java/hu/bme/mit/theta/xta/analysis/XtaOrd.java b/subprojects/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/XtaOrd.java similarity index 100% rename from subprojects/xta/src/main/java/hu/bme/mit/theta/xta/analysis/XtaOrd.java rename to subprojects/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/XtaOrd.java diff --git a/subprojects/xta/src/main/java/hu/bme/mit/theta/xta/analysis/XtaState.java b/subprojects/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/XtaState.java similarity index 100% rename from subprojects/xta/src/main/java/hu/bme/mit/theta/xta/analysis/XtaState.java rename to subprojects/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/XtaState.java diff --git a/subprojects/xta/src/main/java/hu/bme/mit/theta/xta/analysis/XtaTransFunc.java b/subprojects/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/XtaTransFunc.java similarity index 100% rename from subprojects/xta/src/main/java/hu/bme/mit/theta/xta/analysis/XtaTransFunc.java rename to subprojects/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/XtaTransFunc.java diff --git a/subprojects/xta/src/main/java/hu/bme/mit/theta/xta/analysis/expl/XtaExplAnalysis.java b/subprojects/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/expl/XtaExplAnalysis.java similarity index 100% rename from subprojects/xta/src/main/java/hu/bme/mit/theta/xta/analysis/expl/XtaExplAnalysis.java rename to subprojects/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/expl/XtaExplAnalysis.java diff --git a/subprojects/xta/src/main/java/hu/bme/mit/theta/xta/analysis/expl/XtaExplInitFunc.java b/subprojects/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/expl/XtaExplInitFunc.java similarity index 100% rename from subprojects/xta/src/main/java/hu/bme/mit/theta/xta/analysis/expl/XtaExplInitFunc.java rename to subprojects/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/expl/XtaExplInitFunc.java diff --git a/subprojects/xta/src/main/java/hu/bme/mit/theta/xta/analysis/expl/XtaExplTransFunc.java b/subprojects/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/expl/XtaExplTransFunc.java similarity index 100% rename from subprojects/xta/src/main/java/hu/bme/mit/theta/xta/analysis/expl/XtaExplTransFunc.java rename to subprojects/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/expl/XtaExplTransFunc.java diff --git a/subprojects/xta/src/main/java/hu/bme/mit/theta/xta/analysis/expl/XtaExplUtils.java b/subprojects/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/expl/XtaExplUtils.java similarity index 100% rename from subprojects/xta/src/main/java/hu/bme/mit/theta/xta/analysis/expl/XtaExplUtils.java rename to subprojects/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/expl/XtaExplUtils.java diff --git a/subprojects/xta/src/main/java/hu/bme/mit/theta/xta/analysis/expl/itp/ItpExplAnalysis.java b/subprojects/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/expl/itp/ItpExplAnalysis.java similarity index 100% rename from subprojects/xta/src/main/java/hu/bme/mit/theta/xta/analysis/expl/itp/ItpExplAnalysis.java rename to subprojects/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/expl/itp/ItpExplAnalysis.java diff --git a/subprojects/xta/src/main/java/hu/bme/mit/theta/xta/analysis/expl/itp/ItpExplInitFunc.java b/subprojects/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/expl/itp/ItpExplInitFunc.java similarity index 100% rename from subprojects/xta/src/main/java/hu/bme/mit/theta/xta/analysis/expl/itp/ItpExplInitFunc.java rename to subprojects/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/expl/itp/ItpExplInitFunc.java diff --git a/subprojects/xta/src/main/java/hu/bme/mit/theta/xta/analysis/expl/itp/ItpExplOrd.java b/subprojects/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/expl/itp/ItpExplOrd.java similarity index 100% rename from subprojects/xta/src/main/java/hu/bme/mit/theta/xta/analysis/expl/itp/ItpExplOrd.java rename to subprojects/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/expl/itp/ItpExplOrd.java diff --git a/subprojects/xta/src/main/java/hu/bme/mit/theta/xta/analysis/expl/itp/ItpExplState.java b/subprojects/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/expl/itp/ItpExplState.java similarity index 100% rename from subprojects/xta/src/main/java/hu/bme/mit/theta/xta/analysis/expl/itp/ItpExplState.java rename to subprojects/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/expl/itp/ItpExplState.java diff --git a/subprojects/xta/src/main/java/hu/bme/mit/theta/xta/analysis/expl/itp/ItpExplTransFunc.java b/subprojects/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/expl/itp/ItpExplTransFunc.java similarity index 100% rename from subprojects/xta/src/main/java/hu/bme/mit/theta/xta/analysis/expl/itp/ItpExplTransFunc.java rename to subprojects/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/expl/itp/ItpExplTransFunc.java diff --git a/subprojects/xta/src/main/java/hu/bme/mit/theta/xta/analysis/lazy/AlgorithmStrategy.java b/subprojects/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/lazy/AlgorithmStrategy.java similarity index 100% rename from subprojects/xta/src/main/java/hu/bme/mit/theta/xta/analysis/lazy/AlgorithmStrategy.java rename to subprojects/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/lazy/AlgorithmStrategy.java diff --git a/subprojects/xta/src/main/java/hu/bme/mit/theta/xta/analysis/lazy/BwItpExplStrategy.java b/subprojects/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/lazy/BwItpExplStrategy.java similarity index 100% rename from subprojects/xta/src/main/java/hu/bme/mit/theta/xta/analysis/lazy/BwItpExplStrategy.java rename to subprojects/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/lazy/BwItpExplStrategy.java diff --git a/subprojects/xta/src/main/java/hu/bme/mit/theta/xta/analysis/lazy/BwItpZoneStrategy.java b/subprojects/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/lazy/BwItpZoneStrategy.java similarity index 100% rename from subprojects/xta/src/main/java/hu/bme/mit/theta/xta/analysis/lazy/BwItpZoneStrategy.java rename to subprojects/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/lazy/BwItpZoneStrategy.java diff --git a/subprojects/xta/src/main/java/hu/bme/mit/theta/xta/analysis/lazy/ClockStrategies.java b/subprojects/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/lazy/ClockStrategies.java similarity index 100% rename from subprojects/xta/src/main/java/hu/bme/mit/theta/xta/analysis/lazy/ClockStrategies.java rename to subprojects/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/lazy/ClockStrategies.java diff --git a/subprojects/xta/src/main/java/hu/bme/mit/theta/xta/analysis/lazy/ClockStrategy.java b/subprojects/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/lazy/ClockStrategy.java similarity index 100% rename from subprojects/xta/src/main/java/hu/bme/mit/theta/xta/analysis/lazy/ClockStrategy.java rename to subprojects/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/lazy/ClockStrategy.java diff --git a/subprojects/xta/src/main/java/hu/bme/mit/theta/xta/analysis/lazy/CombinedStrategy.java b/subprojects/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/lazy/CombinedStrategy.java similarity index 100% rename from subprojects/xta/src/main/java/hu/bme/mit/theta/xta/analysis/lazy/CombinedStrategy.java rename to subprojects/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/lazy/CombinedStrategy.java diff --git a/subprojects/xta/src/main/java/hu/bme/mit/theta/xta/analysis/lazy/DataStrategies.java b/subprojects/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/lazy/DataStrategies.java similarity index 100% rename from subprojects/xta/src/main/java/hu/bme/mit/theta/xta/analysis/lazy/DataStrategies.java rename to subprojects/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/lazy/DataStrategies.java diff --git a/subprojects/xta/src/main/java/hu/bme/mit/theta/xta/analysis/lazy/DataStrategy.java b/subprojects/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/lazy/DataStrategy.java similarity index 100% rename from subprojects/xta/src/main/java/hu/bme/mit/theta/xta/analysis/lazy/DataStrategy.java rename to subprojects/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/lazy/DataStrategy.java diff --git a/subprojects/xta/src/main/java/hu/bme/mit/theta/xta/analysis/lazy/ExplStrategy.java b/subprojects/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/lazy/ExplStrategy.java similarity index 100% rename from subprojects/xta/src/main/java/hu/bme/mit/theta/xta/analysis/lazy/ExplStrategy.java rename to subprojects/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/lazy/ExplStrategy.java diff --git a/subprojects/xta/src/main/java/hu/bme/mit/theta/xta/analysis/lazy/FwItpExplStrategy.java b/subprojects/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/lazy/FwItpExplStrategy.java similarity index 100% rename from subprojects/xta/src/main/java/hu/bme/mit/theta/xta/analysis/lazy/FwItpExplStrategy.java rename to subprojects/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/lazy/FwItpExplStrategy.java diff --git a/subprojects/xta/src/main/java/hu/bme/mit/theta/xta/analysis/lazy/FwItpZoneStrategy.java b/subprojects/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/lazy/FwItpZoneStrategy.java similarity index 100% rename from subprojects/xta/src/main/java/hu/bme/mit/theta/xta/analysis/lazy/FwItpZoneStrategy.java rename to subprojects/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/lazy/FwItpZoneStrategy.java diff --git a/subprojects/xta/src/main/java/hu/bme/mit/theta/xta/analysis/lazy/ItpExplStrategy.java b/subprojects/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/lazy/ItpExplStrategy.java similarity index 100% rename from subprojects/xta/src/main/java/hu/bme/mit/theta/xta/analysis/lazy/ItpExplStrategy.java rename to subprojects/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/lazy/ItpExplStrategy.java diff --git a/subprojects/xta/src/main/java/hu/bme/mit/theta/xta/analysis/lazy/ItpZoneStrategy.java b/subprojects/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/lazy/ItpZoneStrategy.java similarity index 100% rename from subprojects/xta/src/main/java/hu/bme/mit/theta/xta/analysis/lazy/ItpZoneStrategy.java rename to subprojects/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/lazy/ItpZoneStrategy.java diff --git a/subprojects/xta/src/main/java/hu/bme/mit/theta/xta/analysis/lazy/LazyXtaChecker.java b/subprojects/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/lazy/LazyXtaChecker.java similarity index 100% rename from subprojects/xta/src/main/java/hu/bme/mit/theta/xta/analysis/lazy/LazyXtaChecker.java rename to subprojects/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/lazy/LazyXtaChecker.java diff --git a/subprojects/xta/src/main/java/hu/bme/mit/theta/xta/analysis/lazy/LazyXtaCheckerFactory.java b/subprojects/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/lazy/LazyXtaCheckerFactory.java similarity index 100% rename from subprojects/xta/src/main/java/hu/bme/mit/theta/xta/analysis/lazy/LazyXtaCheckerFactory.java rename to subprojects/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/lazy/LazyXtaCheckerFactory.java diff --git a/subprojects/xta/src/main/java/hu/bme/mit/theta/xta/analysis/lazy/LazyXtaStatistics.java b/subprojects/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/lazy/LazyXtaStatistics.java similarity index 100% rename from subprojects/xta/src/main/java/hu/bme/mit/theta/xta/analysis/lazy/LazyXtaStatistics.java rename to subprojects/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/lazy/LazyXtaStatistics.java diff --git a/subprojects/xta/src/main/java/hu/bme/mit/theta/xta/analysis/lazy/Lens.java b/subprojects/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/lazy/Lens.java similarity index 100% rename from subprojects/xta/src/main/java/hu/bme/mit/theta/xta/analysis/lazy/Lens.java rename to subprojects/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/lazy/Lens.java diff --git a/subprojects/xta/src/main/java/hu/bme/mit/theta/xta/analysis/lazy/LuZoneStrategy.java b/subprojects/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/lazy/LuZoneStrategy.java similarity index 100% rename from subprojects/xta/src/main/java/hu/bme/mit/theta/xta/analysis/lazy/LuZoneStrategy.java rename to subprojects/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/lazy/LuZoneStrategy.java diff --git a/subprojects/xta/src/main/java/hu/bme/mit/theta/xta/analysis/zone/XtaActZoneUtils.java b/subprojects/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/zone/XtaActZoneUtils.java similarity index 100% rename from subprojects/xta/src/main/java/hu/bme/mit/theta/xta/analysis/zone/XtaActZoneUtils.java rename to subprojects/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/zone/XtaActZoneUtils.java diff --git a/subprojects/xta/src/main/java/hu/bme/mit/theta/xta/analysis/zone/XtaLuZoneUtils.java b/subprojects/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/zone/XtaLuZoneUtils.java similarity index 100% rename from subprojects/xta/src/main/java/hu/bme/mit/theta/xta/analysis/zone/XtaLuZoneUtils.java rename to subprojects/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/zone/XtaLuZoneUtils.java diff --git a/subprojects/xta/src/main/java/hu/bme/mit/theta/xta/analysis/zone/XtaZoneAnalysis.java b/subprojects/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/zone/XtaZoneAnalysis.java similarity index 100% rename from subprojects/xta/src/main/java/hu/bme/mit/theta/xta/analysis/zone/XtaZoneAnalysis.java rename to subprojects/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/zone/XtaZoneAnalysis.java diff --git a/subprojects/xta/src/main/java/hu/bme/mit/theta/xta/analysis/zone/XtaZoneInitFunc.java b/subprojects/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/zone/XtaZoneInitFunc.java similarity index 100% rename from subprojects/xta/src/main/java/hu/bme/mit/theta/xta/analysis/zone/XtaZoneInitFunc.java rename to subprojects/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/zone/XtaZoneInitFunc.java diff --git a/subprojects/xta/src/main/java/hu/bme/mit/theta/xta/analysis/zone/XtaZoneTransFunc.java b/subprojects/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/zone/XtaZoneTransFunc.java similarity index 100% rename from subprojects/xta/src/main/java/hu/bme/mit/theta/xta/analysis/zone/XtaZoneTransFunc.java rename to subprojects/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/zone/XtaZoneTransFunc.java diff --git a/subprojects/xta/src/main/java/hu/bme/mit/theta/xta/analysis/zone/XtaZoneUtils.java b/subprojects/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/zone/XtaZoneUtils.java similarity index 100% rename from subprojects/xta/src/main/java/hu/bme/mit/theta/xta/analysis/zone/XtaZoneUtils.java rename to subprojects/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/zone/XtaZoneUtils.java diff --git a/subprojects/xta/src/main/java/hu/bme/mit/theta/xta/analysis/zone/itp/ItpZoneAnalysis.java b/subprojects/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/zone/itp/ItpZoneAnalysis.java similarity index 100% rename from subprojects/xta/src/main/java/hu/bme/mit/theta/xta/analysis/zone/itp/ItpZoneAnalysis.java rename to subprojects/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/zone/itp/ItpZoneAnalysis.java diff --git a/subprojects/xta/src/main/java/hu/bme/mit/theta/xta/analysis/zone/itp/ItpZoneInitFunc.java b/subprojects/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/zone/itp/ItpZoneInitFunc.java similarity index 100% rename from subprojects/xta/src/main/java/hu/bme/mit/theta/xta/analysis/zone/itp/ItpZoneInitFunc.java rename to subprojects/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/zone/itp/ItpZoneInitFunc.java diff --git a/subprojects/xta/src/main/java/hu/bme/mit/theta/xta/analysis/zone/itp/ItpZoneOrd.java b/subprojects/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/zone/itp/ItpZoneOrd.java similarity index 100% rename from subprojects/xta/src/main/java/hu/bme/mit/theta/xta/analysis/zone/itp/ItpZoneOrd.java rename to subprojects/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/zone/itp/ItpZoneOrd.java diff --git a/subprojects/xta/src/main/java/hu/bme/mit/theta/xta/analysis/zone/itp/ItpZoneState.java b/subprojects/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/zone/itp/ItpZoneState.java similarity index 100% rename from subprojects/xta/src/main/java/hu/bme/mit/theta/xta/analysis/zone/itp/ItpZoneState.java rename to subprojects/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/zone/itp/ItpZoneState.java diff --git a/subprojects/xta/src/main/java/hu/bme/mit/theta/xta/analysis/zone/itp/ItpZoneTransFunc.java b/subprojects/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/zone/itp/ItpZoneTransFunc.java similarity index 100% rename from subprojects/xta/src/main/java/hu/bme/mit/theta/xta/analysis/zone/itp/ItpZoneTransFunc.java rename to subprojects/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/zone/itp/ItpZoneTransFunc.java diff --git a/subprojects/xta/src/main/java/hu/bme/mit/theta/xta/analysis/zone/lu/LuZoneAnalysis.java b/subprojects/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/zone/lu/LuZoneAnalysis.java similarity index 100% rename from subprojects/xta/src/main/java/hu/bme/mit/theta/xta/analysis/zone/lu/LuZoneAnalysis.java rename to subprojects/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/zone/lu/LuZoneAnalysis.java diff --git a/subprojects/xta/src/main/java/hu/bme/mit/theta/xta/analysis/zone/lu/LuZoneInitFunc.java b/subprojects/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/zone/lu/LuZoneInitFunc.java similarity index 100% rename from subprojects/xta/src/main/java/hu/bme/mit/theta/xta/analysis/zone/lu/LuZoneInitFunc.java rename to subprojects/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/zone/lu/LuZoneInitFunc.java diff --git a/subprojects/xta/src/main/java/hu/bme/mit/theta/xta/analysis/zone/lu/LuZoneOrd.java b/subprojects/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/zone/lu/LuZoneOrd.java similarity index 100% rename from subprojects/xta/src/main/java/hu/bme/mit/theta/xta/analysis/zone/lu/LuZoneOrd.java rename to subprojects/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/zone/lu/LuZoneOrd.java diff --git a/subprojects/xta/src/main/java/hu/bme/mit/theta/xta/analysis/zone/lu/LuZoneState.java b/subprojects/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/zone/lu/LuZoneState.java similarity index 100% rename from subprojects/xta/src/main/java/hu/bme/mit/theta/xta/analysis/zone/lu/LuZoneState.java rename to subprojects/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/zone/lu/LuZoneState.java diff --git a/subprojects/xta/src/main/java/hu/bme/mit/theta/xta/analysis/zone/lu/LuZoneTransFunc.java b/subprojects/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/zone/lu/LuZoneTransFunc.java similarity index 100% rename from subprojects/xta/src/main/java/hu/bme/mit/theta/xta/analysis/zone/lu/LuZoneTransFunc.java rename to subprojects/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/zone/lu/LuZoneTransFunc.java diff --git a/subprojects/xta/src/test/java/hu/bme/mit/theta/xta/analysis/LazyXtaCheckerTest.java b/subprojects/xta-analysis/src/test/java/hu/bme/mit/theta/xta/analysis/LazyXtaCheckerTest.java similarity index 100% rename from subprojects/xta/src/test/java/hu/bme/mit/theta/xta/analysis/LazyXtaCheckerTest.java rename to subprojects/xta-analysis/src/test/java/hu/bme/mit/theta/xta/analysis/LazyXtaCheckerTest.java diff --git a/subprojects/xta/src/test/java/hu/bme/mit/theta/xta/analysis/XtaAnalysisTest.java b/subprojects/xta-analysis/src/test/java/hu/bme/mit/theta/xta/analysis/XtaAnalysisTest.java similarity index 100% rename from subprojects/xta/src/test/java/hu/bme/mit/theta/xta/analysis/XtaAnalysisTest.java rename to subprojects/xta-analysis/src/test/java/hu/bme/mit/theta/xta/analysis/XtaAnalysisTest.java diff --git a/subprojects/xta/src/test/java/hu/bme/mit/theta/xta/analysis/XtaZoneAnalysisTest.java b/subprojects/xta-analysis/src/test/java/hu/bme/mit/theta/xta/analysis/XtaZoneAnalysisTest.java similarity index 100% rename from subprojects/xta/src/test/java/hu/bme/mit/theta/xta/analysis/XtaZoneAnalysisTest.java rename to subprojects/xta-analysis/src/test/java/hu/bme/mit/theta/xta/analysis/XtaZoneAnalysisTest.java diff --git a/subprojects/xta-analysis/src/test/resources/critical-2-25-50.xta b/subprojects/xta-analysis/src/test/resources/critical-2-25-50.xta new file mode 100644 index 0000000000..d44cecbdc4 --- /dev/null +++ b/subprojects/xta-analysis/src/test/resources/critical-2-25-50.xta @@ -0,0 +1,61 @@ +const int N = 2; + +const int A = 25; +const int B = 50; + +typedef int[1, N] id_t; +int id; + +chan cellenter[N + 1], cellexit[N + 1]; + +process Counter() { + state + initCount, + initial; + + init initial; + + trans + initCount -> initCount { guard id >= N; assign id = 1; }, + initCount -> initCount { guard id < N; assign id = id + 1; }, + initial -> initCount { guard id == 0; assign id = 1; }; +} + +process Arbiter(const id_t i) { + state + S0, + S1; + + init S1; + + trans + S0 -> S1 { sync cellexit[i]!; assign id = i; }, + S1 -> S0 { guard id == i; sync cellenter[i]!; assign id = 0; }; +} + +process ProdCell(const id_t i) { + clock x; + + state + safe, + testing2 { x <= A }, + error, + critical { x <= B }, + requesting, + testing { x <= A }, + notready; + + init notready; + + trans + testing2 -> safe { guard x <= A - 1; }, + testing2 -> error { guard x >= A; }, + critical -> error { guard x >= B; }, + critical -> testing2 { guard x <= A - 1; sync cellexit[i]?; assign x = 0; }, + requesting -> critical { sync cellenter[i]?; assign x = 0; }, + testing -> requesting { guard x <= A - 1; }, + testing -> notready { guard x >= A; assign x = 0; }, + notready -> testing { guard x <= B; assign x = 0; }; +} + +system Counter, Arbiter, ProdCell; \ No newline at end of file diff --git a/subprojects/xta-analysis/src/test/resources/csma-2.xta b/subprojects/xta-analysis/src/test/resources/csma-2.xta new file mode 100644 index 0000000000..3de64a751a --- /dev/null +++ b/subprojects/xta-analysis/src/test/resources/csma-2.xta @@ -0,0 +1,57 @@ +const int N = 2; + +const int LAMDA = 404; +const int SIGMA = 13; + +typedef int[0, N - 1] id_t; +int j; + +chan begin, end, busy; +chan cd[N]; + +process Bus() { + clock x; + + state + idle, + active, + collision { x < SIGMA }, + transmit; + + urgent + transmit; + + init idle; + + trans + transmit -> transmit { guard j < N-1; sync cd[j]!; assign x = 0, j = j + 1; }, + transmit -> idle { guard j == N - 1; sync cd[j]!; assign j = 0, x = 0; }, + idle -> active { sync begin?; assign x = 0; }, + active -> idle { sync end?; assign x = 0; }, + active -> active { guard x >= SIGMA; sync busy!; }, + active -> collision { guard x < SIGMA; sync begin?; assign x = 0; }, + collision -> transmit { guard x < SIGMA; sync cd[j]!; assign x = 0, j = j + 1; }; +} + +process Station(const id_t id) { + clock x; + + state + wait, + transm { x <= LAMDA }, + retry { x <= 2 * SIGMA }; + + init wait; + + trans + wait -> transm { sync begin!; assign x = 0; }, + wait -> wait { sync cd[id]?; assign x = 0; }, + wait -> retry { sync cd[id]?; assign x = 0; }, + wait -> retry { sync busy?; assign x = 0; }, + transm -> wait { guard x >= LAMDA; sync end!; assign x = 0; }, + transm -> retry { guard x <= 2 * SIGMA; sync cd[id]?; assign x = 0; }, + retry -> transm { guard x <= 2 * SIGMA; sync begin!; assign x = 0; }, + retry -> retry { guard x <= 2 * SIGMA; sync cd[id]?; assign x = 0; }; +} + +system Bus, Station; \ No newline at end of file diff --git a/subprojects/xta-analysis/src/test/resources/engine-classic.xta b/subprojects/xta-analysis/src/test/resources/engine-classic.xta new file mode 100644 index 0000000000..6ecf3ae5f1 --- /dev/null +++ b/subprojects/xta-analysis/src/test/resources/engine-classic.xta @@ -0,0 +1,233 @@ +// 1996-11-20, 1997-02-20, and 1997-07-31 +// @ Uppsala University. +// Paul Pettersson, DoCS & Magnus Lindahl, Mecel AB + +// Engine +int UseCase; +chan ReqZeroTorque, TorqueZero, ReqSpeed; +chan SpeedSet, ReqTorque; + +// Clutch +chan OpenClutch, CloseClutch, ClutchIsOpen, ClutchIsClosed; + +// GearBox +chan ReqNeu, GearNeu, ReqSet, GearSet; + +// Gear +int FromGear, ToGear; +chan ReqNewGear, NewGear; + +// System Decoration +int ErrStat; +clock CTimer, ETimer, GBTimer, GCTimer, SysTimer; + +process Clutch() { + + state + Closed, + Closing { CTimer <= 150 }, + ErrorClose, + ErrorOpen, + Open, + Opening { CTimer <= 150 }; + + init Closed; + + trans + Closed -> Opening { sync OpenClutch?; assign CTimer = 0; }, + Closing -> Closed { guard CTimer >= 100; sync ClutchIsClosed!; }, + Closing -> ErrorClose { guard CTimer == 150; assign ErrStat = 1; }, + Open -> Closing { sync CloseClutch?; assign CTimer = 0; }, + Opening -> ErrorOpen { guard CTimer == 150; assign ErrStat = 2; }, + Opening -> Open { guard CTimer >= 100; sync ClutchIsOpen!; }; +} + +process GearBox() { + + state + Closing { GBTimer <= 300 }, + ErrorIdle, + ErrorNeu, + Idle, + Neutral, + Opening { GBTimer <= 200 }; + + init Neutral; + + trans + Closing -> ErrorIdle { guard GBTimer == 300; assign ErrStat = 3; }, + Closing -> Idle { guard GBTimer >= 100; sync GearSet!; }, + Idle -> Opening { sync ReqNeu?; assign GBTimer = 0; }, + Neutral -> Closing { sync ReqSet?; assign GBTimer = 0; }, + Opening -> ErrorNeu { guard GBTimer > 200; assign ErrStat = 4; }, + Opening -> Neutral { guard GBTimer >= 100; sync GearNeu!; }; +} + +process GearControl() { + + state + CCloseError, + COpenError, + CheckClutch { GCTimer <= 200 }, + CheckClutch2 { GCTimer<=200 }, + CheckClutchClosed { GCTimer <= 200 }, + CheckClutchClosed2 { GCTimer <= 200}, + CheckGearNeu { GCTimer <= 250 }, + CheckGearNeu2 { GCTimer <= 250 }, + CheckGearSet1 { GCTimer <= 350 }, + CheckGearSet2 { GCTimer <= 350 }, + CheckSyncSpeed { GCTimer <= 155 }, + CheckTorque { GCTimer <= 255 }, + ClutchClose, + ClutchOpen, + ClutchOpen2, + GNeuError, + GSetError, + Gear, + GearChanged, + Initiate, + ReqNeuGear, + ReqSetGear, + ReqSetGear2, + ReqSyncSpeed, + ReqTorqueC; + + commit + ClutchClose, + ClutchOpen, + ClutchOpen2, + GearChanged, + Initiate, + ReqNeuGear, + ReqSetGear, + ReqSetGear2, + ReqSyncSpeed, + ReqTorqueC; + + init Gear; + + trans + CheckClutch -> COpenError { guard GCTimer > 150 && GCTimer <= 200; }, + CheckClutch -> ClutchOpen { sync ClutchIsOpen?; }, + CheckClutch2 -> COpenError { guard GCTimer > 150 && GCTimer <= 200; }, + CheckClutch2 -> ClutchOpen2 { sync ClutchIsOpen?; }, + CheckClutchClosed -> CCloseError { guard GCTimer > 150 && GCTimer <= 200; }, + CheckClutchClosed -> ReqTorqueC { sync ClutchIsClosed?; }, + CheckClutchClosed2 -> CCloseError { guard GCTimer > 150 && GCTimer <= 200; }, + CheckClutchClosed2 -> GearChanged { sync ClutchIsClosed?; }, + CheckGearNeu -> GNeuError { guard GCTimer > 200 && GCTimer <= 250; }, + CheckGearNeu -> ReqSyncSpeed { sync GearNeu?; }, + CheckGearNeu2 -> GNeuError { guard GCTimer > 200 && GCTimer <= 250; }, + CheckGearNeu2 -> ReqSetGear2 { sync GearNeu?; }, + CheckGearSet1 -> GSetError { guard GCTimer > 300 && GCTimer <= 350; }, + CheckGearSet1 -> ReqTorqueC { sync GearSet?; }, + CheckGearSet2 -> ClutchClose { sync GearSet?; }, + CheckGearSet2 -> GSetError { guard GCTimer > 300 && GCTimer <= 350; }, + CheckSyncSpeed -> CheckClutch { guard GCTimer >= 150; sync OpenClutch!; assign GCTimer = 0; }, + CheckSyncSpeed -> ReqSetGear { guard GCTimer < 150; sync SpeedSet?; }, + CheckTorque -> CheckClutch2 { guard GCTimer >= 250; sync OpenClutch!; assign GCTimer = 0; }, + CheckTorque -> ReqNeuGear { guard GCTimer < 250; sync TorqueZero?; }, + ClutchClose -> CheckClutchClosed { sync CloseClutch!; assign GCTimer = 0; }, + ClutchOpen -> CheckGearSet2 { sync ReqSet!; assign GCTimer = 0; }, + ClutchOpen2 -> CheckGearNeu2 { sync ReqNeu!; assign GCTimer = 0; }, + Gear -> Initiate { sync ReqNewGear?; assign SysTimer = 0; }, + GearChanged -> Gear { sync NewGear!; }, + Initiate -> CheckTorque { guard FromGear > 0; sync ReqZeroTorque!; assign GCTimer = 0; }, + Initiate -> ReqSyncSpeed { guard FromGear <= 0; }, + ReqNeuGear -> CheckGearNeu { sync ReqNeu!; assign GCTimer = 0; }, + ReqSetGear -> CheckGearSet1 { sync ReqSet!; assign GCTimer = 0; }, + ReqSetGear2 -> CheckClutchClosed2 { guard ToGear == 0; sync CloseClutch!; assign GCTimer = 0; }, + ReqSetGear2 -> CheckGearSet2 { guard ToGear>0; sync ReqSet!; assign GCTimer = 0; }, + ReqSyncSpeed -> CheckSyncSpeed { guard ToGear > 0; sync ReqSpeed!; assign GCTimer = 0; }, + ReqSyncSpeed -> GearChanged { guard ToGear <= 0; }, + ReqTorqueC -> GearChanged { sync ReqTorque!; }; +} + +process Interface() { + + state + Gear1, + Gear2, + Gear3, + Gear4, + Gear5, + GearN, + GearR, + chkGear12, + chkGear1N, + chkGear21, + chkGear23, + chkGear32, + chkGear34, + chkGear43, + chkGear45, + chkGear54, + chkGearN1, + chkGearNR, + chkGearRN; + + init GearN; + + trans + Gear1 -> chkGear12 { sync ReqNewGear!; assign FromGear = 1, ToGear = 2; }, + Gear1 -> chkGear1N { sync ReqNewGear!; assign FromGear = 1, ToGear = 0; }, + Gear2 -> chkGear21 { sync ReqNewGear!; assign FromGear = 2, ToGear = 1; }, + Gear2 -> chkGear23 { sync ReqNewGear!; assign FromGear = 2, ToGear = 3; }, + Gear3 -> chkGear32 { sync ReqNewGear!; assign FromGear = 3, ToGear = 2; }, + Gear3 -> chkGear34 { sync ReqNewGear!; assign FromGear = 3, ToGear = 4; }, + Gear4 -> chkGear43 { sync ReqNewGear!; assign FromGear = 4, ToGear = 3; }, + Gear4 -> chkGear45 { sync ReqNewGear!; assign FromGear = 4, ToGear = 5; }, + Gear5 -> chkGear54 { sync ReqNewGear!; assign FromGear = 5, ToGear = 4; }, + GearN -> chkGearN1 { sync ReqNewGear!; assign FromGear = 0, ToGear = 1; }, + GearN -> chkGearNR { sync ReqNewGear!; assign FromGear = 0, ToGear = 6; }, + GearR -> chkGearRN { sync ReqNewGear!; assign FromGear = 6, ToGear = 0; }, + chkGear12 -> Gear2 { sync NewGear?; }, + chkGear1N -> GearN { sync NewGear?; }, + chkGear21 -> Gear1 { sync NewGear?; }, + chkGear23 -> Gear3 { sync NewGear?; }, + chkGear32 -> Gear2 { sync NewGear?; }, + chkGear34 -> Gear4 { sync NewGear?; }, + chkGear43 -> Gear3 { sync NewGear?; }, + chkGear45 -> Gear5 { sync NewGear?; }, + chkGear54 -> Gear4 { sync NewGear?; }, + chkGearN1 -> Gear1 { sync NewGear?; }, + chkGearNR -> GearR { sync NewGear?; }, + chkGearRN -> GearN { sync NewGear?; }; +} + +process Engine() { + + state + ClutchClose { ETimer <= 900}, + ClutchOpen, + DecTorque { ETimer <= 400}, + ErrorSpeed, + FindSpeed { ETimer <= 200}, + Initial, + Speed { ETimer <= 500}, + Torque, + Zero; + + commit + ClutchOpen; + + init Initial; + + trans + ClutchClose -> ErrorSpeed { guard ETimer == 900; }, + ClutchClose -> Torque { guard ETimer >= 50; sync ReqTorque?; }, + ClutchOpen -> ClutchClose { guard ToGear > 0; assign ETimer = 0; }, + ClutchOpen -> Initial { guard ToGear == 0; }, + DecTorque -> ClutchOpen { guard ETimer == 400; assign UseCase = 1; }, + DecTorque -> Zero { guard ETimer >= 150; sync TorqueZero!; }, + FindSpeed -> ClutchOpen { guard ETimer == 200; assign UseCase = 2; }, + FindSpeed -> Speed { guard ETimer >= 50; sync SpeedSet!; assign ETimer = 0; }, + Initial -> FindSpeed { sync ReqSpeed?; assign ETimer = 0, UseCase = 0; }, + Speed -> ErrorSpeed { guard ETimer == 500; }, + Speed -> Torque { guard ETimer < 500; sync ReqTorque?; }, + Torque -> DecTorque { sync ReqZeroTorque?; assign ETimer = 0,UseCase = 0; }, + Zero -> FindSpeed { guard ToGear > 0; sync ReqSpeed?; assign ETimer = 0; }, + Zero -> Initial { guard ToGear == 0; }; +} + +system GearControl, Interface, Engine, GearBox, Clutch; diff --git a/subprojects/xta-analysis/src/test/resources/fddi-2.xta b/subprojects/xta-analysis/src/test/resources/fddi-2.xta new file mode 100644 index 0000000000..6e9fa67d8e --- /dev/null +++ b/subprojects/xta-analysis/src/test/resources/fddi-2.xta @@ -0,0 +1,58 @@ +const int N = 2; + +const int TTRT = 50 * N; +const int SA = 20; +const int TD = 0; + +typedef int[1, N] id_t; + +chan TT[id_t]; +chan RT[id_t]; + +process Station(const id_t pid) { + clock trt, xA, xB; + + state + q7 { xB <= TTRT + SA }, + q6 { trt <= SA }, + q5 { trt <= SA }, + q4, + q3 { xA <= TTRT + SA }, + q2 { trt <= SA }, + q1 { trt <= SA }, + q0; + + init q0; + + trans + q0 -> q1 { guard trt >= TTRT; sync TT[pid]?; assign trt = 0, xB = 0; }, + q0 -> q2 { guard trt < TTRT; sync TT[pid]?; assign trt = 0, xB = 0; }, + q1 -> q4 { guard trt >= SA; sync RT[pid]!; }, + q2 -> q3 { guard trt >= SA; }, + q3 -> q4 { sync RT[pid]!; }, + q4 -> q5 { guard trt >= TTRT; sync TT[pid]?; assign trt = 0, xA = 0; }, + q4 -> q6 { guard trt < TTRT; sync TT[pid]?; assign trt = 0,xA = 0; }, + q5 -> q0 { guard trt >= SA; sync RT[pid]!; }, + q6 -> q7 { guard trt >= SA; }, + q7 -> q0 { sync RT[pid]!; }; +} + +process Ring() { + clock t; + int id; + + state + S0, + S1 { t <= TD }, + S2; + + init S0; + + trans + S0 -> S1 { assign id = 1; }, + S1 -> S2 { guard t >= TD; sync TT[id]!; }, + S2 -> S1 { sync RT[id]?; assign t = 0, id = (id % N) + 1; }; +} + +system Station, Ring; + \ No newline at end of file diff --git a/subprojects/xta-analysis/src/test/resources/fischer-2-32-64.xta b/subprojects/xta-analysis/src/test/resources/fischer-2-32-64.xta new file mode 100644 index 0000000000..ca0c4388be --- /dev/null +++ b/subprojects/xta-analysis/src/test/resources/fischer-2-32-64.xta @@ -0,0 +1,27 @@ +const int N = 2; + +typedef int[1, N] id_t; +int id; + +process P(const id_t pid) { + clock x; + const int a = 32; + const int b = 64; + + state + wait, + req { x <= a }, + A, + cs; + + init A; + + trans + A -> req { guard id == 0; assign x = 0; }, + req -> wait { assign x = 0, id = pid; }, + wait -> req { guard id == 0; assign x = 0; }, + wait -> cs { guard x >= b && id == pid; }, + cs -> A { assign id = 0; }; +} + +system P; \ No newline at end of file diff --git a/subprojects/xta-analysis/src/test/resources/lynch-2-16.xta b/subprojects/xta-analysis/src/test/resources/lynch-2-16.xta new file mode 100644 index 0000000000..6b8e03b33f --- /dev/null +++ b/subprojects/xta-analysis/src/test/resources/lynch-2-16.xta @@ -0,0 +1,39 @@ +const int N = 2; + +typedef int[1, N] Pid; +int v1; +bool v2; +const int T = 16; + +process P(const Pid i) { + clock c; + + state + L9 { c <= T }, + L8 { c <= T }, + CS7, + L6, + L5 { c <= T }, + L4, + L3, + L2 { c <= T }, + L1; + + init L1; + + trans + L9 -> L1 { assign v1 = 0; }, + L8 -> L9 { assign v2 = false, c = 0; }, + CS7 -> L8 { assign c = 0; }, + L4 -> L1 { guard v2; }, + L6 -> L1 { guard v1 != i; }, + L3 -> L1 { guard v1 != i; }, + L6 -> CS7 { guard v1 == i; }, + L5 -> L6 { assign v2 = true, c = 0; }, + L4 -> L5 { guard !v2; assign c = 0; }, + L3 -> L4 { guard v1 == i && c > T; }, + L2 -> L3 { assign v1 = i, c = 0; }, + L1 -> L2 { guard v1 == 0; assign c = 0; }; +} + +system P; \ No newline at end of file diff --git a/subprojects/xta-cli/build.gradle.kts b/subprojects/xta-cli/build.gradle.kts new file mode 100644 index 0000000000..9aa42a0bef --- /dev/null +++ b/subprojects/xta-cli/build.gradle.kts @@ -0,0 +1,14 @@ +plugins { + id("java-common") + id("cli-tool") +} + +dependencies { + compile(project(":theta-xta")) + compile(project(":theta-xta-analysis")) + compile(project(":theta-solver-z3")) +} + +application { + mainClassName = "hu.bme.mit.theta.xta.cli.XtaCli" +} diff --git a/subprojects/xta/src/main/java/hu/bme/mit/theta/xta/tool/XtaCli.java b/subprojects/xta-cli/src/main/java/hu/bme/mit/theta/xta/cli/XtaCli.java similarity index 99% rename from subprojects/xta/src/main/java/hu/bme/mit/theta/xta/tool/XtaCli.java rename to subprojects/xta-cli/src/main/java/hu/bme/mit/theta/xta/cli/XtaCli.java index dbc4527046..673b8bf165 100644 --- a/subprojects/xta/src/main/java/hu/bme/mit/theta/xta/tool/XtaCli.java +++ b/subprojects/xta-cli/src/main/java/hu/bme/mit/theta/xta/cli/XtaCli.java @@ -13,7 +13,7 @@ * See the License for the specific language governing permissions and * limitations under the License. */ -package hu.bme.mit.theta.xta.tool; +package hu.bme.mit.theta.xta.cli; import java.io.FileInputStream; import java.io.FileNotFoundException; diff --git a/subprojects/xta/.gitignore b/subprojects/xta/.gitignore deleted file mode 100644 index 65776c32fc..0000000000 --- a/subprojects/xta/.gitignore +++ /dev/null @@ -1 +0,0 @@ -/bin/ \ No newline at end of file diff --git a/subprojects/xta/build.gradle b/subprojects/xta/build.gradle deleted file mode 100644 index f0094a7fb3..0000000000 --- a/subprojects/xta/build.gradle +++ /dev/null @@ -1,35 +0,0 @@ -apply plugin: 'antlr' -apply from: "${rootDir}/common-methods.gradle" - -dependencies { - compile project(':theta-common') - compile project(':theta-core') - compile project(':theta-analysis') - antlr group: 'org.antlr', name: 'antlr4', version: antlrVersion - compile group: 'com.beust', name: 'jcommander', version: jcommanderVersion - compile group: 'com.google.guava', name: 'guava', version: guavaVersion - testCompile project(':theta-solver') - testCompile project(':theta-solver-z3') - testCompile group: 'junit', name: 'junit', version: junitVersion -} - -generateGrammarSource { - arguments += ['-package', 'hu.bme.mit.theta.xta.dsl.gen'] - arguments += ['-Werror', '-visitor'] - doLast { - copy { - from outputDirectory - into 'src/main/java/hu/bme/mit/theta/xta/dsl/gen' - } - } -} - -sourceSets { - main { - java { - srcDirs = ['src/main/java'] - } - } -} - -createJarTask('theta-xta-cli', 'hu.bme.mit.theta.xta.tool.XtaCli', 'theta-xta-cli') diff --git a/subprojects/xta/build.gradle.kts b/subprojects/xta/build.gradle.kts new file mode 100644 index 0000000000..52019ac21a --- /dev/null +++ b/subprojects/xta/build.gradle.kts @@ -0,0 +1,9 @@ +plugins { + id("java-common") + id("antlr-grammar") +} + +dependencies { + compile(project(":theta-common")) + compile(project(":theta-core")) +} diff --git a/subprojects/xta/src/main/java/hu/bme/mit/theta/xta/dsl/gen/.gitignore b/subprojects/xta/src/main/java/hu/bme/mit/theta/xta/dsl/gen/.gitignore deleted file mode 100644 index d6b7ef32c8..0000000000 --- a/subprojects/xta/src/main/java/hu/bme/mit/theta/xta/dsl/gen/.gitignore +++ /dev/null @@ -1,2 +0,0 @@ -* -!.gitignore