Skip to content
Snippets Groups Projects
Commit d4c28859 authored by dgelessus's avatar dgelessus
Browse files

Merge branch 'develop'

parents e257275c 086d3258
Branches
Tags 1.2.0
No related merge requests found
Pipeline #145600 passed
Stage: test
Expand all Show whitespace changes
Inline Side-by-side
Showing
with 746 additions and 790 deletions
.gitlab-ci.yml
+ 14
− 10
View file @ d4c28859
image: openjdk:8-jdk-slim
image: eclipse-temurin:8
stages:
- test
......@@ -6,14 +6,14 @@ stages:
variables:
GRADLE_OPTIONS: --no-daemon --info --stacktrace --warning-mode=all
GRADLE_USER_HOME: "$CI_PROJECT_DIR/.gradle"
cache:
paths:
- .gradle/wrapper
- .gradle/caches
before_script:
- export GRADLE_USER_HOME=`pwd`/.gradle
- .gradle/native
- .gradle/notifications
- .gradle/wrapper
tests:
stage: test
......@@ -21,18 +21,22 @@ tests:
tests:jdk-11:
extends: tests
image: openjdk:11-jdk-slim
image: eclipse-temurin:11
tests:jdk-17:
extends: tests
image: openjdk:17-jdk-slim
image: eclipse-temurin:17
tests:jdk-21:
extends: tests
image: eclipse-temurin:21
publish:
stage: deploy
script:
- openssl aes-256-cbc -pass "env:ENCRYPTION_PASSWORD" -d -a -md md5 -in secring.gpg.enc -out secring.gpg
- openssl aes-256-cbc -pass "env:ENCRYPTION_PASSWORD" -d -a -md md5 -in pubring.gpg.enc -out pubring.gpg
- openssl aes-256-cbc -pass "env:ENCRYPTION_PASSWORD" -d -a -md md5 -in gradle.properties.enc -out gradle.properties
- openssl aes-256-cbc -d -base64 -pbkdf2 -pass "env:ENCRYPTION_PASSWORD" -in gradle.properties.enc -out gradle.properties
- openssl aes-256-cbc -d -base64 -pbkdf2 -pass "env:ENCRYPTION_PASSWORD" -in pubring.gpg.enc -out pubring.gpg
- openssl aes-256-cbc -d -base64 -pbkdf2 -pass "env:ENCRYPTION_PASSWORD" -in secring.gpg.enc -out secring.gpg
- ./gradlew ${GRADLE_OPTIONS} publish
only:
- master@general/stups/tlc4b
......
README.md
+ 13
− 0
View file @ d4c28859
TLC4B
=====
This project contains a translator from B to TLA+ with the purpose of applying the
TLC model checker on B models within the ProB validation tool.
TLC is an efficient model checker for TLA+ specifications, which can check LTL properties with fairness. It is particularly good for lower level specifications, where it can be substantially faster than ProB's own model checker
The following article describes the translation:
Dominik Hansen and Michael Leuschel.
Translating B to TLA+ for validation with TLC.
Sci. Comput. Program. 131, pages 109-125. 2016.
[Link](https://doi.org/10.1016/j.scico.2016.04.014)
More details about using TLC4B can be found on the [ProB web pages](https://prob.hhu.de/w/index.php?title=TLC).
[![GitLab CI](https://gitlab.cs.uni-duesseldorf.de/general/stups/tlc4b/badges/develop/pipeline.svg)](https://gitlab.cs.uni-duesseldorf.de/general/stups/tlc4b/pipelines)
build.gradle
+ 13
− 11
View file @ d4c28859
......@@ -4,11 +4,11 @@ plugins {
id 'jacoco'
id "maven-publish"
id "signing"
id "de.undercouch.download" version "5.4.0"
id "de.undercouch.download" version "5.6.0"
}
project.version = '1.1.0'
project.group = 'de.hhu.stups'
project.version = "1.2.0"
final isSnapshot = project.version.endsWith("-SNAPSHOT")
......@@ -26,31 +26,30 @@ configurations.all {
resolutionStrategy.cacheChangingModulesFor 0, 'seconds'
}
def parser_version = '2.12.4'
def parser_version = '2.13.5'
dependencies {
//implementation(group: 'com.microsoft', name: 'tla2tools', version: '1.4.6')
implementation(group: 'commons-cli', name: 'commons-cli', version: '1.5.0')
implementation(group: 'de.hhu.stups', name: 'tlatools', version: '1.0.2')
implementation(group: 'commons-cli', name: 'commons-cli', version: '1.8.0')
implementation(group: 'de.hhu.stups', name: 'tlatools', version: '1.1.0')
implementation(group: 'de.hhu.stups', name: 'bparser', version: parser_version)
implementation(group: 'de.hhu.stups', name: 'ltlparser', version: parser_version)
testImplementation(group: 'junit', name: 'junit', version: '4.13.2')
testImplementation(group: 'de.hhu.stups', name: 'tla2bAST', version: '1.1.5')
testImplementation(group: 'de.hhu.stups', name: 'tla2bAST', version: '1.4.0')
}
java {
project.sourceCompatibility = JavaVersion.VERSION_1_8
project.targetCompatibility = JavaVersion.VERSION_1_8
sourceCompatibility = JavaVersion.VERSION_1_8
targetCompatibility = JavaVersion.VERSION_1_8
withSourcesJar()
withJavadocJar()
}
jacoco {
toolVersion = "0.8.7"
reportsDirectory = file("$buildDir/JacocoReports")
toolVersion = "0.8.12"
}
......@@ -58,7 +57,7 @@ jacocoTestReport {
reports {
xml.required = false
csv.required = false
html.destination file("${buildDir}/jacocoHtml")
html.outputLocation = layout.buildDirectory.dir('jacocoHtml')
}
}
......@@ -93,6 +92,9 @@ clean {
}
task regressionTests(dependsOn: extractPublicExamples, type: Test) {
testClassesDirs = testing.suites.test.sources.output.classesDirs
classpath = testing.suites.test.sources.runtimeClasspath
include('de/tlc4b/tlc/integration/probprivate/**')
}
check.dependsOn(regressionTests)
......
gradle.properties.enc
+ 4
− 5
View file @ d4c28859
U2FsdGVkX18nOHLNyyzYk3lwSF0IGgXp8ubFJuMWOPaMbTBmgRPWS/jQT4LO17HP
W5yqIb+NzcYqzLBohg9s9r4XFyoS5ic3TIyPp87IXzgWNh3gKV+F+DfbggwMjiyJ
0gZI+90cmkWXBDW7c3JijLOX2f0NATwuiwHFPau3FCKC0cp7uOArtqkbfZau2how
oP8hzzAue50fahPuBfg8h3OtofJW9x9UCUxxD/NXzD8VZFQabICUjI8mcjEcvaea
MqQn9JuoekIRPDUsUwZ9Er07OkzKXHB5c968S3DUP3w=
U2FsdGVkX1+BEAbjRIB+mXtm8SXf7JkI+WHnEimPW4vLHWrbGs8PY7u+B9BCqO+3
vmUhdJFfnwJglivtRmt3ecLUpSSG3pZFXrdtnR/eHdLIkbGIIjZRcRTokF66Z2CQ
sWdDhhu2gsRxXOiKSQ/d5MknWHd+zlLoMiWJv3u+EQ3desH/cadBC1RAod7L6Kul
UtSAw5pmAJFaBrRFoOJVvw7hi5ZkpcMB3JTZL2+1Tsxs50m7XAqc5PVdCHpMqVMb
gradle/wrapper/gradle-wrapper.jar
+ 0
− 0
View file @ d4c28859
No preview for this file type
gradle/wrapper/gradle-wrapper.properties
+ 2
− 1
View file @ d4c28859
distributionBase=GRADLE_USER_HOME
distributionPath=wrapper/dists
distributionUrl=https\://services.gradle.org/distributions/gradle-8.1.1-bin.zip
distributionUrl=https\://services.gradle.org/distributions/gradle-8.10.2-bin.zip
networkTimeout=10000
validateDistributionUrl=true
zipStoreBase=GRADLE_USER_HOME
zipStorePath=wrapper/dists
gradlew
+ 17
− 10
View file @ d4c28859
......@@ -15,6 +15,8 @@
# See the License for the specific language governing permissions and
# limitations under the License.
#
# SPDX-License-Identifier: Apache-2.0
#
##############################################################################
#
......@@ -55,7 +57,7 @@
# Darwin, MinGW, and NonStop.
#
# (3) This script is generated from the Groovy template
# https://github.com/gradle/gradle/blob/HEAD/subprojects/plugins/src/main/resources/org/gradle/api/internal/plugins/unixStartScript.txt
# https://github.com/gradle/gradle/blob/HEAD/platforms/jvm/plugins-application/src/main/resources/org/gradle/api/internal/plugins/unixStartScript.txt
# within the Gradle project.
#
# You can find Gradle at https://github.com/gradle/gradle/.
......@@ -83,7 +85,9 @@ done
# This is normally unused
# shellcheck disable=SC2034
APP_BASE_NAME=${0##*/}
APP_HOME=$( cd "${APP_HOME:-./}" && pwd -P ) || exit
# Discard cd standard output in case $CDPATH is set (https://github.com/gradle/gradle/issues/25036)
APP_HOME=$( cd -P "${APP_HOME:-./}" > /dev/null && printf '%s
' "$PWD" ) || exit
# Use the maximum available, or set MAX_FD != -1 to use that value.
MAX_FD=maximum
......@@ -130,18 +134,21 @@ location of your Java installation."
fi
else
JAVACMD=java
which java >/dev/null 2>&1 || die "ERROR: JAVA_HOME is not set and no 'java' command could be found in your PATH.
if ! command -v java >/dev/null 2>&1
then
die "ERROR: JAVA_HOME is not set and no 'java' command could be found in your PATH.
Please set the JAVA_HOME variable in your environment to match the
location of your Java installation."
fi
fi
# Increase the maximum file descriptors if we can.
if ! "$cygwin" && ! "$darwin" && ! "$nonstop" ; then
case $MAX_FD in #(
max*)
# In POSIX sh, ulimit -H is undefined. That's why the result is checked to see if it worked.
# shellcheck disable=SC3045
# shellcheck disable=SC2039,SC3045
MAX_FD=$( ulimit -H -n ) ||
warn "Could not query maximum file descriptor limit"
esac
......@@ -149,7 +156,7 @@ if ! "$cygwin" && ! "$darwin" && ! "$nonstop" ; then
'' | soft) :;; #(
*)
# In POSIX sh, ulimit -n is undefined. That's why the result is checked to see if it worked.
# shellcheck disable=SC3045
# shellcheck disable=SC2039,SC3045
ulimit -n "$MAX_FD" ||
warn "Could not set maximum file descriptor limit to $MAX_FD"
esac
......@@ -198,11 +205,11 @@ fi
# Add default JVM options here. You can also use JAVA_OPTS and GRADLE_OPTS to pass JVM options to this script.
DEFAULT_JVM_OPTS='"-Xmx64m" "-Xms64m"'
# Collect all arguments for the java command;
# * $DEFAULT_JVM_OPTS, $JAVA_OPTS, and $GRADLE_OPTS can contain fragments of
# shell script including quotes and variable substitutions, so put them in
# double quotes to make sure that they get re-expanded; and
# * put everything else in single quotes, so that it's not re-expanded.
# Collect all arguments for the java command:
# * DEFAULT_JVM_OPTS, JAVA_OPTS, JAVA_OPTS, and optsEnvironmentVar are not allowed to contain shell fragments,
# and any embedded shellness will be escaped.
# * For example: A user cannot expect ${Hostname} to be expanded, as it is an environment variable and will be
# treated as '${Hostname}' itself on the command line.
set -- \
"-Dorg.gradle.appname=$APP_BASE_NAME" \
......
gradlew.bat
+ 12
− 10
View file @ d4c28859
......@@ -13,6 +13,8 @@
@rem See the License for the specific language governing permissions and
@rem limitations under the License.
@rem
@rem SPDX-License-Identifier: Apache-2.0
@rem
@if "%DEBUG%"=="" @echo off
@rem ##########################################################################
......@@ -43,11 +45,11 @@ set JAVA_EXE=java.exe
%JAVA_EXE% -version >NUL 2>&1
if %ERRORLEVEL% equ 0 goto execute
echo.
echo ERROR: JAVA_HOME is not set and no 'java' command could be found in your PATH.
echo.
echo Please set the JAVA_HOME variable in your environment to match the
echo location of your Java installation.
echo. 1>&2
echo ERROR: JAVA_HOME is not set and no 'java' command could be found in your PATH. 1>&2
echo. 1>&2
echo Please set the JAVA_HOME variable in your environment to match the 1>&2
echo location of your Java installation. 1>&2
goto fail
......@@ -57,11 +59,11 @@ set JAVA_EXE=%JAVA_HOME%/bin/java.exe
if exist "%JAVA_EXE%" goto execute
echo.
echo ERROR: JAVA_HOME is set to an invalid directory: %JAVA_HOME%
echo.
echo Please set the JAVA_HOME variable in your environment to match the
echo location of your Java installation.
echo. 1>&2
echo ERROR: JAVA_HOME is set to an invalid directory: %JAVA_HOME% 1>&2
echo. 1>&2
echo Please set the JAVA_HOME variable in your environment to match the 1>&2
echo location of your Java installation. 1>&2
goto fail
......
pubring.gpg.enc
+ 26
− 26
View file @ d4c28859
U2FsdGVkX1/MdPD8TmHygEYUS49v1M2eqrSgZK0x8pZ/mIO51EnU4UUelrxxyGN5
NvnLUPVhm63e2EtzQ3Yhq8f5rb7+2rZ/vwlL6SteBhxH5G0bwb0gCdA2rUiyWKJw
tKwAjizS1TYs1AgU4LpUIQ1iGmvg1WDmuyWpZvJ/2vR/v6rT/5OxHAKzk5MclbDq
a7HfR3XiRmH0zZKMk38zD7id04pDstDO6jfLE1OOay9Rg8qIfUbenHzBlQLiqqz+
lDsJtzT9UZmtKK0X89TQ7dfS7cmbgpJB11ibLAi+EEJqqkEP2U5BT5qRFsehTp/X
Xh07xOnyMbQXo67cAZ6GkGhw3Wy/71JRRK2ynLg8NmxgTsTqxhcJX4bZ0gCKLome
1QR5B1fhmo2IMpWE8shgk8gm3AKtlo7v8eGzVFmpchrog5HBFclupLUVD5rLj6ei
dncq8jsJ0AlcjFsW+Cyg8/2Tncdi/uwiwsKJdligvXKECAcvuNhFBFPrlPB4Z1KY
f6SQG2LAu5746zCQ29Hpkj5UKiCqCXqdYnG6PCx2ZNkbDSR31GeqK+GbYoahKGxb
VDuBw033g5bvAIeRUuGYC5ua3LhW7Fs5ElUx3feAVjJALtA1FB9mtK2vVwVU/bmS
2f02VBKvYVfZ2asILQJ2HuC157TBbAPEJAu4M+0YR5T9fUiDGLbhDHq4E4vZp+LJ
7WKMecy+zXkvuF13TkxbzmAdh/pQvq8uhLvu24fPbHvzudasZA0n+VwRqg8whzxX
2rodf86Zk3aVPwYPq/o/j1aXRE1zPZHIeZv7mmp+dNvhqS0sjr8fPziUS/MnwzJz
J/K9Z7cXGE1wQIIHnTZGbAa6LI0keV/Ba5IgKLR0CifugjwU4vxHdHEzvo2YZIJI
AVR9oVQMcAx73GWEYlO3SG9IktHamfo76U3FAUtthRZ2D46Us0+LuNsPL92OC7o8
2+rdgtzulCuYbcVaAFJTrpg4NTHU5uJf8CsDrQKt+1frmV/+lFye7P1OJcREPuQ4
RA7+1V3A2x8hOiDBo1BBr0MskLu+01l+Lh4YzPd8jTcngn6T7WO5P6689O6Nk4QS
Dg9ubHo3BWdGdJ4nK44qGMa/GfZKG9pShn3Zoq2+1Y5jYCmyjs5/jtV0Zw7NDCTz
5ZBqBU7lxrc0gAUy3dH5IYTmOBNUieZKDYG/sILtBs363am7tQ3sfqgIJEA2nRxI
PnlYAy+JEYKz80zY1c4CFC2gfZzed8499pPMsSjRc8TX8wpe+iE/fL7rjpBdSRi1
xBSK4BiSOQOLp5Rw5SHDzBpdK9aobNQECCUhkejYEfTi0Xw6v1QZ8U6tNjZQ9+M2
56VH4wuvYXE++L3SUVEYTJPi3yYC8v+fo80hkm3KF/wIWmeZqmjsRVDHatHxEfld
vzRhO0Lb1CsJo9aq+FAd5E/Ek9skQE1dXoQLRXgFkEJGbmo9hysxz2CB89CaaREW
l/hRW/v3Zqw6giQfe8hOEpyg7yj6xGgEuCuv5Uiz3gLg4NAg8Wvbq0K40ne7ukIO
DrbAkG2+0+TyIBv/ocZJykQ974SD+w0t3qIBeW0q9cxqTtKAX8OAaJhdXx5IiCcW
KpRBcAzZBCC0hKdBTVp/50+ySfcBzHJDnxVzGaWx/DA=
U2FsdGVkX1/ecmzt62K2yKsVlvmQKkfzExhaIo9Zm8/ZobX4Q9asbrssdDbfAdpX
lyIp3wY65EPLcROlrNZqLTjAbcZrPnQyKgCYRr0+s5/0iy6noTWa52EZyPvmP3fw
vsIM/MqFjZCBUhFfvvIb2qNz5+d84lvsOojzeYm+9xSKCx8k24XupcsWuMgfiNla
vmpeUUCPHAYB1clTNn66YdChrQJCcrbnHUmBWms3lSU5waZ5i1dnteaLCLo6M58O
H/7YKOb5cg/0WFE6/l28xFk49ACcAH6i3q3pf99XyPGk+/kvG/Zx+8HvaoG26MkM
HrV60kJgh1t4LBtvadvHk0UyODZJzrH/4ka1XVJv18ZQ5pcLTI6sNEwkM9XjxaU0
Ik7DIxf6onEaBlk1nRnhXi97gKa7+XjVR82pLXgPEn5HrAe+ObX1UL0VqfJw7EXs
Nb2ZVciC/ugfi3UiHuOtFmImo+MRLXvvqkpW49VfO5GwBBpmjM9PcXdRzdtU8USp
Z+KXXBoUPfZupCpty+ZCq8uBEMW93ifeqOLOqcr8B496LrPOC+T4D/MOh+1Pdpy+
3YmzdfwttqKXNULhiW/loljKoKOBOjO6DDWwyEH+4LEuZYgXdC6nfedchU+F5ZQw
ORtyrkznV7baoNR/UDT33qz0c3fEtoWmPtiuiClHN12CoXWamK7dwBKP64aPL5Xy
UaYsrbjhMhW3/miVx6NgIv0iq8B/aUrJIXVdGWycVJVciRbgk1Px6z1lo3GOaZad
APqExffMHUOQZCjv8AC9tKsy2heog97Q4jUwOCHdghfmKK16ksy4plDaVN322uOG
S3mkfJLxw/2oUeAA8IFARCZ1FoCINPKxiRevPXhoizRNa7WzmQ4jT9C+BWDJeitn
LrA7fMmTpW0z7oaQez2VTSFg5liDtozp7Dp+d5MBA9Rg4B69F121FIt3MXWACHFl
5YW2+Sa6czh8P7eZQ4lRGOl8Y56NAE72n5l15HUdxrnEowwREuHAmWVdWCi16oTJ
JUqcSv3vu4WZQo3XhoB36ll0gvYZezlzoxpSqekBwlDkKCqevhncyu0UefG9fApu
g/2gDmQIVeAMfKytEyAomXCNiFriesqPBAyt3ZRivbWCMeBGT3KuMO2BIigfW7na
+BdpdeCF8KIEiOq69Ulaw6wo2lTOlP+utuD6D3iB0ATsvr18Bj9CXN7lloQD4tmw
DTUxrYBFjjtK6/SINHq0CwCgY968QdL+muk1A1xIiOK4ELNSLK16qIHUKYN5G7pr
eGNRD0KGeg64u42o+R1bZaYOWEqDHw9gWP9uuDp+M31T2uz3+NZS7JOmqpwh1VRy
4hW7BEhLO+C/A+feWeuXq5PXlMaeEE0+L8QE0nvto3N3HqsiwXIgg54AsQEkRCxp
uybDyfvAc4ni+GTd+8g0oUilzxa/oHGGzD386/aZDVWXhNiFZNXfr2LJljMW+lRT
7A5z/IIegoN5lSNy4IwbJY4WSRMaZ3jX7zM/t5IAyeB2/BXuiKspJ+XKhNwib5Mo
NKuwogypLpPux7968PkRHiOk3ndizKTUQj4RF52dWqW7ekbYelK1fcJXxILXDYi7
8i/H7c7cUzvYvmnHe+2PArs2yVUL+fBrrsdXSaaswMs=
secring.gpg.enc
+ 55
− 55
View file @ d4c28859
U2FsdGVkX1+qD9zNt5PsTWUNPv0+h3MZr3LMQniTSXNJ70iaxTv8TOQ2EFQM42X0
IKPutnofk+e17tRWJch3XTzTI95sU7s8NgtrorS9cNJQMMpZrMSNGt6jHbLGC6jL
F4AWjk3fNg4s0OVPvVD4ZXbdLm1BJaNuz094kRGNNTYPrFapxkPr6WVDjnZsh3bh
S5xhQ84hSAyfXKShs8HidN6Mf6XZvRgVsXg87SeCNQlTtyU+k8o5/COXZ35XhNjY
NUEOSaSaBbhC16fNC8rWYTqcOsrypiikuZAT+qo2ZfMw3/SYUyc9q9qPfQvITJqb
YtfQsdfQEarI0skRBZLuNs8OOWMh473YaMqicaNfOUTtPm3NPElZNAIVyM6wp3lh
36Ovib377R0IAvsSg5ktSHWbkPOY1MqDusHRHW5s5jjrjAtKyi3iWjQ4L4Mf67lj
ZJ9b2YQpdqQQOpZg8nRghk/Dqw2XGWc/84LgnaTCdSTsYSyZbDkYvLbyNzoNbcx1
i2BOUqDaA9N3lGdgSqrHLjVdH3LegpCaEBsi3I8ZdDVfZMHckujYI7+/rDqzDxQ2
btbHt9LKcciOpWZvrD83R5Uq4WewWrkx6vKUYwQAklKu4SkKUz/Q+P4esWWfgMcy
XXhhzMhvhx9Hsham5AznWU5oXDhCxdrdpXtI56Jepa444M9e7JaoszaQ5V0rHFhA
F2Ko7vDlk1LRjJ1f27T3Uaj26jspyCiaAi7kVBTriCVGp7yEoAJ5EBeOOPKSzzOa
pxyzYuKQlf+nQoo5t8TPpgLIPJbip70n0HNkKDc2cj8102ZeKgGWkpnNawrtgkjs
b5DK3f+SjuZCWGnXZ2pcM01NIAXOCnw7hCH06z5hXmzK/jDDbckWL/F7sVtO4n7Z
yICynW0m2EkzMpU4yPC5f5h9iNpNgV1xirjZ5F2QbiguvtAZOo0YSGtE6lO/22uI
jgXW5uMzkh3doBatbEsJYh8dGzrCqq1leC8b+MBOM8Xby4wkCgSSCOzclF9AIRe6
axHGfFtO/wOv0Z/6CeuREvw38MIjozVIZomjddEj9KLW1/30ljksvhDnv2pS0vVm
nAvYiXvtuvMwDzmFEpsAqinyFbzS3lCMzlqRoATFbjUGAh29Xz9PHsLHb0B9KjRD
1/rz3BVhzNaYEvCMX8J0M5mzjAzTaB8eWkQnZ+wLfmUJlvt6XFxDuLbcNGmCZ2th
8NNfvly6Awbkln2R3wism0oIDUnO8KrUJmVtCcbOIiEkrsOEq62oF3Ndof5jKHUx
2KcjuzSrKiXoYoVH4uTh2HiKHVB71yZ8Fpwrbda16AMrmpA35urKeEmAjTsmT0iT
Plxnd4cPfqSxAesGOpz5jhRjPc/3FqIYvewf1eINUHteduDwLqeA0SqBcDgW6YIO
LRPQhJdsDnpmV5NKXbSHChRAsk+4CrCS68WNJ/RrY1NhuFktjHQ+mHyg886YMnmg
bYRd9CKmlYDBVsgpFJFT7wDMoCWZ132flqegu8ojsdjXD/2i18kcyZgFx/YFimz9
u2NRVOJnU0ec5tTk0HNi3q5wG/pgIWj8et2HDSDBr2dhBc5s+s9EhL3JXDr3SoEp
bW41GA+G7l+FPKakOgDgiw2VBi5MmIPMwDRzhi/VD3mrI8SfKFDQxq1Ro91dy0sO
cQ4Ku1esMojqNJO+sPUOm0LYj3BgL+bUQdc4Vj4gvo/uDEk7SrPloDaMPjzbQsQ4
wJ+NRuF82NvagdA25vEMxLD3O3aD7wsQA/Fsbh04GLwbGkH+Kl9QGmMVMHJU2Dn/
1owCuIvNRYZU587HQXDitM5Be7+EixE/90PLuAioe8iNDiCHUPwiYMHge5ZNZlbk
agN4KjmkEpCh0XwOLvD9F5PDji8dAp6AOmZhQK+y0XTGGQCWD2k6tBFD94Ux4wOi
J18zIEDeRJWZA/WiyqEihVIRNcq7NZQRfv3PsSbU8wFbVg379yJftfIdXj8fJFcI
7gKK7gYv2A6K9kS6pNSN8kSWBsukiz0/njiPZH1wjyeSrONueacJ9guk9hzTeN68
iD00zcdtukC6ZtxXRB9XOAbXTGhbyWrdb5ATCmJLFG8riUTJVo5DIyHzCg4rCRef
2yq5Pe1MVsV8960AnkE1iyin2lMebzJJL8ridlHmzhaNIRSSGxstv1tnaZL1xVWV
c2pLWkch6uEzdyC5Zyd5Xi56zyxUxxCYPEPA9lortKgW7KdYULUvTBHfRoGAUqjZ
6yHl37DF1MWFHmV4Dk1yHNP7uVazF+7c1hJTvqop/ytFkgIEhLq8SHWBEHG/sGVi
R11UfpoVHdkT3KJm6Y/tml9SLxES65ENzLGPTKVUAaHKImADXrMI9slU+lUMHDr8
MwKx3+4xSgUUYWL2+YfayURNK6LIUskmsOlGy212z1B/pJc8DvrH9rqj6NtBaQlZ
lR6A9eiG3i88N2PvibxMuHW+ye0zlbiktqArWQAhNgt9mM05BQSb2Ce55cl8yLCD
+3eSAIFUKQhn4aHNaEutGD7q02bjX1pcUymM9NV2WxHtG5dQPa8eWRXKwJca3V6w
WKC/ve1HXsCunjW5mc2FvtsqqKUANzRjTV2fkbQlMdVfdThy+MIxJs0P8XMbyxT7
tjwt4tuq42ZAQkj8dLL2j1z+/otzH3LtfYjl3CjDjWPlfVFJn+1lISQDBdzWPYe/
xnhNn2Gsx0jWv1vX0dbxD8gyXP68yS3KLPTBb6DoTbjW+0LraTLlHSw2rNJ/zTsM
5hcf7PnuEr3c34bVjP2XLjrZ6qT0+TEXJ8vR6ptuUL/GFREG8ByfBG4SFphR1Nkr
iuySq+4awgKwmXrfiVdBQPrn+UWfH/UQh6Jt2J0xvRwcs7/COO5LcWqjD4bSCw9a
CfSkivrrEDmeE4aruA1eOeauVbRcqwtMuzCV7Gq282LKambmnKiWvrk9wJnF2IaQ
wV8rjmBM08sf+93/P+TbYhY4e/z27+ml844HwoNsivuvmo70z8nYNnFXKKOewZby
Vw0I3JX/2vkHllMFtLcJqnQLD8zJR2SclkUnWv4S519qR0sg9kzFvggTvB740KDu
Ohu1wIeHkTv9ZnCfu/7gK3lxNobyV2+2UhgBB4/njI/9mb4BnOJkaTG7HvJA+Pks
BpSL7jOrmTixSLzt6rsLeYpp8J+A2+uKL5Q1t97My/yhIKjC67LuWVfKovB+5/Bk
/C/FuDqeKDeLOl/lBs1ntQM4TDtb8uVNSmKKdlj4h+dp7J5ZIzHuKDRRw7HcWIPw
3ThPVLFQUoDUsnRxTkenqWA4yUov0UPwpwOBswZQFqFwoX9BQ8hqk13c9P2AhVMZ
2wR5J5cbH3sum2Np/cZUOXuqvcoQGQNyKb1t8PXsvGc3LaMraxRNUcIVJJzUr/eC
oja8ldCr68ZwD/M+CZgQNGr1/5+78tzKdD5432/pZ6W5ZOM36xzyI71b/tZkB4S6
ATF+WE2brPM5g2Wr4T+xKA==
U2FsdGVkX1/uZ2q881m1pVQtzJ0DILJqtO2ZEJOotiBebJg4SmSM4TkLeSgTDFoD
m3fsZdrdbTrOqpNjdCySadS2IwibzJjG8cRFxnetJNUdfpWGFb67kKx/Han4QaIY
d9bvEAkg02nL3suJTa4WKVl70gjiXSheOXgWHi+L3mEGzJewORIIYBv1BE60zxjB
72SvpfrboYxFBCahZJ/GAiNvw4aqD0Wj9G5CJlM6xY0gGTn3dXuWkUC+sciQp9UI
rRSF+r/RMRvbUAPZY3F2S07wMSzIBct9INyhc9kQptRwhuy9BAAdfxVaMxEK3a2P
cM7mHacEmE242/4a28unvcDnsuyV3NW74pt7f2v+LFlPvM8Cw9tpeKtFCRXfREJR
g32dDJBo+4zSa3qLx7n4gsUFaKTDJWPtAPe0pkMLa7GrdoEVIkaIl4m1ET8+M6t4
sKrBKP7neVnjjkSPRroxpiSQ7MLECeyj3MNUB/r/hsLg1ZLc8n90b1vPKqd4DIpJ
PtiIcamt6K8gvAIOwUZQqdpJNNTqCLV9DnKyj5I/U8RpHAXsBe5eawX2WDxA/Ywf
INzBibO9yUpg25OtlsHRqdcyHNmDRMAVUOWtzqa+5lGWIF3h0qWOY8BEqHf7TkjO
O/2qPBqLSmpRcOdgUg9G/5Snpb1xo4NXEZ2kj8GC+Rf61stI38QVScLTsPSR+QKK
9VgCSg1cQTmhQnwZLQw5pB7SdsFPtwwq62YM5E2xzZwr9f9eJVXTfIQlwjM+t7cH
nFbyC+3ywLnvlec/NEeA4DOH5QfJ2vRUQmcXuzmuBi0vGSriVd3U4CKiRKsq7umo
nFpo6y8i7qr4Vj3oIgRIj3yyzYEnaSyJXRJ2mhp3e4fqrMMD7MFrAZ4syKgAJ1Xh
qFbfovebhPbA4NtLrehmZ0r9F1ovowo1X8fwqpoqaKO1LVYQkWC1N/Tkg0ASUlTh
pF0O94r7sMv6pD7vvBvwsfZWxt6qWHVD4H6JU4ySwWHOFiFs7YWPbQIcqaw1Y9R+
sZncQ7Aul/8HGhYhQvklsrK2Yt5nKAQCibST8UinICyAbEWnHnRLaLleB45BiAUy
injdzUjwy2PO7sOnUa7Nf37QuxZGMIMqETapc5ONIz+CAqGjfOC1BGSB6vZmUCNn
W3kpFHbznGTe0zAoPYFhsfnwOWc/m2xUJRRwovVYGQc+PLGEUsMa9JhxwEyb6EUg
bXMsyfk2RBZYEV7bWqML2Nyv71nBuMDjCkAju3gUCaWeG4OVjLTjvvTTNsKWqzKt
vevEgTteynQrUi+CvsqY1fcwyZcmqTBIen+pUYz8mK+JXfL5ppafvuRGZBWMtJW0
Q+3x7HLGtbNO6MNoaK+dPfp5ekQ7eztRFEwTPRTuvqnVBGmgot4HkkxB3noASlCb
xEXEjSYmQJA8Y+B0OGG8CNyKnS/ZeHgqA0K9+xPLuWmJBSEGAgpe6knBdE2+5Qqp
/OgfTKnrCjaVZPeWUG+EwbnUriUKJfTM0SIixJwla9ml+8pzTU1qkRLgD1aychM7
91mxducI9ZsbGAa9aH4SZWU8PC3EPoMOxqN88kZNcfb7AjWMLOdCcgHUm+zRZ/46
zJaS3MAXDdxLmTweT/seL/7VhKvfMSo+qKX1ALSneXpYtAT/XjrIOidhCr9et9eu
SzPdQt24lwcyuGQPIBDYt9NuMBqjFmOE6X3O3CMr4G5d0YmDJuWDZvvCEtGrQjc1
2fREnWTzgkIvOxlYlrR0cczUpzRiAgCfU3ujHRXV+Fqch3RpxmwWz4FGsoJfJ9+a
LNRGtMn+X9Tt/Vx9J1RlPwHJ6U3gS853MXGLXzXFKobqZL3XrMhT00kN0sONCxvc
L17s62zThzeENKZPQxSuA2GVeR3ucip4AhPgFsCCB3m/aIPNZ45/PpRMIFVbijIz
u3XTxv6DN2tp7rDyerRvhfNkVxdu0G8AZ18immyT2wkxnuM4SZODBFK32C6iY2Sx
LU5GgTCSvy/ze5/DRXFhG6mcC9iUWALpfYvCGGwpwdK0MM/Xqd4t7X/kVhcEGljF
UPN09Ja6OqYO47yZUdTUp4L+0FkHnl3wqQaL23e92mb+LpqBYUsdH9PBMAHZ6YA6
OlDNP9n0xwoPHSz4od/6lNA93AmpVOfcrJ2N9J4GMPX44AATDLbr3Hwd8lSxvVD8
oITXp1lZcLzpDo8AHEF/t/MkahaIxTeyjX6jAy2HB5IIXFn5IopAO5gNLS1jmT0I
4d+9u1JxArjQRCjV0c5103SLzVFrYbTVMT7iegCAXjQ0CR3RjGQNna0KMA7Yteoy
gTb7lNDrBjfVk3LkqsBH7bpCQik9lqmcWhYP+ry7wbAK99v/FtzhHqBjyQYHmEBC
Zepft6grJ1JiNOwhTs0/uLQNamuMD1qNGZfta/7CQYzLARvy78DXXyfiM0vc9HeI
cdBwm0nmn2mL3xpKZbQFUNJtzTZTUM4K+H+4Ua166Plil4Gmb2p8BM/Ulby27xDM
OvKgofUrWorPny3kPgjlNXpWAaxGPgcrC6/Zx2mwdUBSmsGAe9aGVMk1wIN/KKdz
uvpAYnlQu26JK39BVVO3OR9v7S3kALxGlN9TCxszWfHiq9wR/BHrZzud1XoCuzZA
+YNDLIWIkie5B7WkF6o+7HnO6/G7arl2gmTBK/i5f/vfZsnj077kQz6TPxt+/k6I
RLWVzUvUDtqSlAO9Wnbi0gajRcsjREVrGiS0kh120x4JRJfEdVmDs/MDPK+iM7ov
mEOgGTIa73SxZZnwqG9j6uggY6M9m/ZO0uPNTEt+jsbQ0NZ9prpI+2/6A8QAX6RE
ug7x+98jjXf7vboTEJLTHJxbuBxJLhJjOqY1Nq0I7GahpPGZMo9yo4Ty78bF4E57
OpT/Q0/wTVSyK9fHPQrRr5zFjvwHmCCs2wWpc76Mv2OThmzVudgyJAoUPENxLSrA
RylkDiihi4PacfjaClbKJJ7K7cgU7KqJQgwS9AM4H8sRqQsZZX/f5UMAVXPRj6u0
qnoH9gxIYAzvm6ceVklagTk09IWCiWqY0NGELL6+plxzjkJuXX2LstfXiHY7g29P
FLnneZ0kNWog2ynKUVBFkdEVdS6K0aQ0xqUFXAwbNvrcpiJeY9RufQcBUlZm/fPb
m26i9V+sL3CcHRbX4qa/QRsQ7DdjdSpOJAt0GQUco3AGfW6Z1koIjSswr0IA41no
1A35JdElJm+lt0pHA9QWBTewNfJkXPR/GHvqUdc1sTDDXa2binNHFWhb+ydX2aQ6
z8ceydjxEt6I3mdK89GZsc/839ctCkeevrjLIC+wAxOviGNJanfyt25BirCgntpi
sLyqYz1nesHZeheyKQBw6y5oYI0EAtVX1ifwSvYgAjbFb1rUmeZl+NWgU14eskyT
+0SdoUgo7WNuJelmyRRoIwTgaV5p3boreRWmdA0oiIKowo6dFE+PzU/cy0dBZtL+
xkXQZ8J6POdTEt4A9Vw6BQ==
settings.gradle 0 → 100644
+ 1
− 0
View file @ d4c28859
rootProject.name = "tlc4b"
src/main/java/de/tlc4b/Log.java deleted 100644 → 0
+ 0
− 63
View file @ e257275c
package de.tlc4b;
import static de.tlc4b.util.StopWatch.Watches.PARSING_TIME;
import java.util.ArrayList;
import de.tlc4b.tlc.TLCResults;
import de.tlc4b.util.StopWatch;
import de.tlc4b.util.StopWatch.Watches;
public class Log {
private ArrayList<String> fieldNames = new ArrayList<>();
private ArrayList<String> fieldValues = new ArrayList<>();
public Log(TLC4B tlc4b, TLCResults tlcResults) {
fieldNames.add("Machine File");
String machineFile = tlc4b.getMainFile().getAbsolutePath();
fieldValues.add(machineFile);
fieldNames.add("TLC Model Checking Time (s)");
int tlcModelCheckingTime = tlcResults.getModelCheckingTime();
fieldValues.add(String.valueOf(tlcModelCheckingTime));
fieldNames.add("Parsing Time Of B machine (ms)");
long parseTime = StopWatch.getRunTime(PARSING_TIME);
fieldValues.add(String.valueOf(parseTime));
fieldNames.add("Translation Time (ms)");
long translationTime = StopWatch.getRunTime(Watches.TRANSLATION_TIME);
fieldValues.add(String.valueOf(translationTime));
fieldNames.add("Model Checking Time (ms)");
long modelCheckingTime = StopWatch
.getRunTime(Watches.MODEL_CHECKING_TIME);
fieldValues.add(String.valueOf(modelCheckingTime));
fieldNames.add("TLC Result");
fieldValues.add(tlcResults.getResultString());
}
public String getCSVValueLine() {
return getCSVLine(fieldValues);
}
public String getCSVFieldNamesLine() {
return getCSVLine(fieldNames);
}
private String getCSVLine(ArrayList<String> list) {
StringBuilder sb = new StringBuilder();
for (int i = 0; i < list.size(); i++) {
sb.append(list.get(i));
if (i < list.size() - 1) {
sb.append(";");
}
}
sb.append("\n");
return sb.toString();
}
}
src/main/java/de/tlc4b/MP.java
+ 33
− 4
View file @ d4c28859
......@@ -4,8 +4,8 @@ import java.io.OutputStream;
import java.io.PrintStream;
public class MP {
private static PrintStream out = System.out;
private static PrintStream err = System.err;
private static final PrintStream out = System.out;
private static final PrintStream err = System.err;
private MP() {
}
......@@ -15,6 +15,26 @@ public class MP {
err.println(errorMessage);
}
public static void printlnSilent(String message) {
if (!TLC4BGlobals.isSilent() || TLC4BGlobals.isVerbose())
out.println(message);
}
public static void printSilent(String message) {
if (!TLC4BGlobals.isSilent() || TLC4BGlobals.isVerbose())
out.print(message);
}
public static void printlnVerbose(String message) {
if (TLC4BGlobals.isVerbose())
out.println(message);
}
public static void printVerbose(String message) {
if (TLC4BGlobals.isVerbose())
out.print(message);
}
public static void println(String message) {
out.println(message);
}
......@@ -27,8 +47,17 @@ public class MP {
static final PrintStream origOut = System.out;
public static void changeOutputStream() {
MP.TLCOutputStream tlcOutputStream = new TLCOutputStream(origOut);
System.setOut(tlcOutputStream);
if (TLC4BGlobals.isSilent()) {
origOut.println("Run TLC...");
System.setOut(new PrintStream(new OutputStream() {
@Override
public void write(int b) {
// ignore
}
}));
return;
}
System.setOut(new TLCOutputStream(origOut));
}
public static void resetOutputStream() {
......
src/main/java/de/tlc4b/TLC4B.java
+ 325
− 338
View file @ d4c28859
This diff is collapsed.
src/main/java/de/tlc4b/TLC4BGlobals.java
+ 35
− 61
View file @ d4c28859
......@@ -15,25 +15,19 @@ public class TLC4BGlobals {
private static boolean partialInvariantEvaluation;
private static boolean useSymmetry;
private static boolean printCoverage;
private static boolean checkOnlyMainAssertions;
private static boolean verbose;
private static boolean silent;
private static boolean deleteFilesOnExit;
private static boolean runTLC;
private static boolean translate;
private static boolean hideTLCConsoleOutput;
private static boolean createTraceFile;
private static boolean testingMode;
private static boolean cleanup;
private static boolean forceTLCToEvalConstants;
private static int workers;
private static boolean runTestscript;
private static int dfid_initial_depth;
static {
resetGlobals();
......@@ -54,25 +48,19 @@ public class TLC4BGlobals {
useSymmetry = false;
printCoverage = false;
forceTLCToEvalConstants = false;
checkOnlyMainAssertions = false;
verbose = false;
silent = false;
proBconstantsSetup = false;
cleanup = true;
workers = 1;
dfid_initial_depth = -1; // option not selected
// for debugging purposes
runTLC = true;
translate = true;
hideTLCConsoleOutput = false; // is mapped to TOOLIO.tool
deleteFilesOnExit = false; // if enabled: deletes all created '.tla',
// '.cfg' files on exit of the JVM. This
// includes
// the created B2TLA standard modules (e.g.
// Relation, but not Naturals etc.).
runTestscript = false;
testingMode = false;
deleteFilesOnExit = false; // if enabled: deletes all created '.tla', '.cfg' files on exit of the JVM.
// This includes the created B2TLA standard modules (e.g. Relation, but not Naturals etc.).
createTraceFile = true;
}
......@@ -84,14 +72,6 @@ public class TLC4BGlobals {
TLC4BGlobals.createTraceFile = createTraceFile;
}
public static boolean isRunTestscript() {
return runTestscript;
}
public static void setRunTestscript(boolean runTestscript) {
TLC4BGlobals.runTestscript = runTestscript;
}
public static int getDEFERRED_SET_SIZE() {
return DEFERRED_SET_SIZE;
}
......@@ -132,10 +112,6 @@ public class TLC4BGlobals {
return checkLTL;
}
public static boolean isTool() {
return hideTLCConsoleOutput;
}
public static boolean isDeleteOnExit() {
return deleteFilesOnExit;
}
......@@ -148,20 +124,20 @@ public class TLC4BGlobals {
partialInvariantEvaluation = b;
}
public static void setDEFERRED_SET_SIZE(int dEFERRED_SET_SIZE) {
DEFERRED_SET_SIZE = dEFERRED_SET_SIZE;
public static void setDEFERRED_SET_SIZE(int deferredSetSize) {
TLC4BGlobals.DEFERRED_SET_SIZE = deferredSetSize;
}
public static void setMAX_INT(int mAX_INT) {
MAX_INT = mAX_INT;
public static void setMAX_INT(int maxInt) {
TLC4BGlobals.MAX_INT = maxInt;
}
public static void setMIN_INT(int mIN_INT) {
MIN_INT = mIN_INT;
public static void setMIN_INT(int minInt) {
TLC4BGlobals.MIN_INT = minInt;
}
public static void setGOAL(boolean gOAL) {
checkGOAL = gOAL;
public static void setGOAL(boolean goal) {
TLC4BGlobals.checkGOAL = goal;
}
public static void setDeadlockCheck(boolean deadlockCheck) {
......@@ -188,10 +164,6 @@ public class TLC4BGlobals {
TLC4BGlobals.checkLTL = checkltl;
}
public static void setTool(boolean tool) {
TLC4BGlobals.hideTLCConsoleOutput = tool;
}
public static void setDeleteOnExit(boolean deleteOnExit) {
TLC4BGlobals.deleteFilesOnExit = deleteOnExit;
}
......@@ -204,12 +176,12 @@ public class TLC4BGlobals {
return TLC4BGlobals.workers;
}
public static boolean isCleanup() {
return cleanup;
public static void setDfidInitialDepth(int depth) {
TLC4BGlobals.dfid_initial_depth = depth;
}
public static void setCleanup(boolean cleanup) {
TLC4BGlobals.cleanup = cleanup;
public static int getDfidInitialDepth() {
return TLC4BGlobals.dfid_initial_depth;
}
public static boolean isProBconstantsSetup() {
......@@ -220,14 +192,6 @@ public class TLC4BGlobals {
TLC4BGlobals.proBconstantsSetup = proBconstantsSetup;
}
public static void setTestingMode(boolean b) {
TLC4BGlobals.testingMode = b;
}
public static boolean getTestingMode() {
return TLC4BGlobals.testingMode;
}
public static void setWelldefinednessCheck(boolean b) {
TLC4BGlobals.checkWD = b;
}
......@@ -240,8 +204,7 @@ public class TLC4BGlobals {
return forceTLCToEvalConstants;
}
public static void setForceTLCToEvalConstants(
boolean forceTLCToEvalConstants) {
public static void setForceTLCToEvalConstants(boolean forceTLCToEvalConstants) {
TLC4BGlobals.forceTLCToEvalConstants = forceTLCToEvalConstants;
}
......@@ -261,8 +224,19 @@ public class TLC4BGlobals {
return printCoverage;
}
public static boolean isCheckOnlyMainAssertions(){
return checkOnlyMainAssertions;
public static void setVerbose(boolean b) {
verbose = b;
}
public static boolean isVerbose() {
return verbose;
}
public static void setSilent(boolean b) {
silent = b;
}
public static boolean isSilent() {
return silent;
}
}
src/main/java/de/tlc4b/TLC4BOption.java 0 → 100644
+ 55
− 0
View file @ d4c28859
package de.tlc4b;
public enum TLC4BOption {
NODEAD("nodead", "do not look for deadlocks", null),
NOTLC("notlc", "do not run TLC", null),
NOTRANSLATION("notranslation", "proceed without machine translation", null),
NOGOAL("nogoal", "do not look for GOAL predicate", null),
NOINV("noinv", "do not look for invariant violations", null),
NOASS("noass", "do not look for ASSERTION violations", null),
WDCHECK("wdcheck", "", null),
SYMMETRY("symmetry", "", null),
TMP("tmp", "", null),
NOLTL("noltl", "no checking of LTL assertions", null),
LAZYCONSTANTS("lazyconstants", "", null),
NOTRACE("notrace", "do not generate counter example trace", null),
DEL("del", "", null),
PARINVEVAL("parinveval", "", null),
LOG("log", "write statistics to CSV file", String.class),
MAXINT("maxint", "set value of MAXINT", Integer.class),
DEFAULT_SETSIZE("default_setsize", "", Integer.class),
MININT("minint", "set value of MININT", Integer.class),
WORKERS("workers", "specify number of workers", Integer.class),
DFID("dfid", "depth-first model checking with iterative deepening, specify initial depth", Integer.class),
CONSTANTSSETUP("constantssetup", "use constants found by ProB for TLC model checking", String.class),
LTLFORMULA("ltlformula", "provide an additional LTL formula", String.class),
VERBOSE("verbose", "put TLC4B in verbose mode", null),
SILENT("silent", "put TLC4B in silent mode", null),
OUTPUT("output", "provide path for output directory", String.class),
COVERAGE("coverage", "print operation coverage", null);
private final String arg, desc;
private final Class<?> expectsArg;
TLC4BOption(String arg, String desc, Class<?> expectsArg) {
this.arg = arg;
this.desc = desc;
this.expectsArg = expectsArg;
}
public String arg() {
return arg;
}
public String cliArg() {
return "-" + arg;
}
public String desc() {
return desc;
}
public Class<?> expectsArg() {
return expectsArg;
}
}
src/main/java/de/tlc4b/TLCRunner.java
+ 43
− 30
View file @ d4c28859
......@@ -9,19 +9,29 @@ import java.io.IOException;
import java.io.InputStream;
import java.io.InputStreamReader;
import java.net.UnknownHostException;
import java.nio.charset.StandardCharsets;
import java.nio.file.FileSystems;
import java.util.ArrayList;
import java.util.Arrays;
import java.util.HashSet;
import java.util.List;
import java.util.Set;
import de.tlc4b.tlc.TLCMessageListener;
import de.tlc4b.util.StopWatch;
import tlc2.TLCGlobals;
import util.SimpleFilenameToStream;
import util.ToolIO;
import tlc2.TLC;
public class TLCRunner {
public static TLCMessageListener listener = null;
public static void addTLCMessageListener(final TLCMessageListener listener) {
TLCRunner.listener = listener;
}
public static void main(String[] args) {
// this method will be executed in a separate JVM
System.setProperty("apple.awt.UIElement", "true");
......@@ -29,15 +39,11 @@ public class TLCRunner {
String path = args[0];
ToolIO.setUserDir(path);
String[] parameters = new String[args.length - 1];
for (int i = 0; i < parameters.length; i++) {
parameters[i] = args[i + 1];
}
System.arraycopy(args, 1, parameters, 0, parameters.length);
try {
TLC.main(parameters);
} catch (UnknownHostException e) {
e.printStackTrace();
} catch (FileNotFoundException e) {
e.printStackTrace();
} catch (Exception e) {
throw new RuntimeException(e);
}
}
......@@ -45,27 +51,22 @@ public class TLCRunner {
final String mainClass, final String[] arguments)
throws IOException {
String separator = System.getProperty("file.separator");
String separator = FileSystems.getDefault().getSeparator();
String jvm = System.getProperty("java.home") + separator + "bin"
+ separator + "java";
String classpath = System.getProperty("java.class.path");
List<String> command = new ArrayList<String>();
command.add(jvm);
command.add("-cp");
command.add(classpath);
command.add(mainClass);
List<String> command = Arrays.asList(jvm, "-cp", classpath, mainClass);
command.addAll(Arrays.asList(arguments));
ProcessBuilder processBuilder = new ProcessBuilder(command);
Process process = processBuilder.start();
return process;
return processBuilder.start();
}
public static ArrayList<String> runTLCInANewJVM(String machineName,
String path) throws IOException {
ArrayList<String> list = new ArrayList<String>();
ArrayList<String> list = new ArrayList<>();
list.add(path);
list.add(machineName);
if (!TLC4BGlobals.isDeadlockCheck()) {
......@@ -78,7 +79,7 @@ public class TLCRunner {
// list.add("-coverage");
// list.add("1");
String[] args = list.toArray(new String[list.size()]);
String[] args = list.toArray(new String[0]);
final Process p = startJVM("", TLCRunner.class.getCanonicalName(), args);
StreamGobbler stdOut = new StreamGobbler(p.getInputStream());
stdOut.start();
......@@ -94,17 +95,29 @@ public class TLCRunner {
public static void runTLC(String machineName, File path) {
StopWatch.start(MODEL_CHECKING_TIME);
MP.println("--------------------------------");
MP.printlnSilent("--------------------------------");
MP.TLCOutputStream.changeOutputStream();
ToolIO.setMode(ToolIO.SYSTEM);
ArrayList<String> list = new ArrayList<String>();
ArrayList<String> list = new ArrayList<>();
if (!TLC4BGlobals.isDeadlockCheck()) {
list.add("-deadlock");
}
if (TLC4BGlobals.getWorkers() > 1) {
list.add("-workers");
list.add("" + TLC4BGlobals.getWorkers());
} else {
// When running multiple model checks from ProB2, the global state is not reset.
// Reset number of workers manually here, are there any other problematic options?!
TLCGlobals.setNumWorkers(1);
}
if (TLC4BGlobals.getDfidInitialDepth() >= 0) {
list.add("-dfid");
list.add("" + TLC4BGlobals.getDfidInitialDepth());
} else {
// When running multiple model checks from ProB2, the global state is not reset.
// Reset DFID manually here if not selected, are there any other problematic options?!
TLCGlobals.DFIDMax = -1;
}
if (TLC4BGlobals.isPrintCoverage()) {
......@@ -121,14 +134,16 @@ public class TLCRunner {
// list.add(machineName + ".cfg");
list.add(machineName);
ToolIO.setUserDir(path.getPath());
String[] args = list.toArray(new String[list.size()]);
String[] args = list.toArray(new String[0]);
TLC tlc = new TLC();
// handle parameters
if (tlc.handleParameters(args)) {
tlc.setResolver(new SimpleFilenameToStream());
// call the actual processing method
try {
if (listener != null) listener.start();
tlc.process();
if (listener != null) listener.finish();
} catch (Exception e) {
}
}
......@@ -142,11 +157,9 @@ public class TLCRunner {
}
private static void closeThreads() {
Set<Thread> threadSet = new HashSet<Thread>(Thread.getAllStackTraces()
.keySet());
Thread[] threadArray = threadSet.toArray(new Thread[threadSet.size()]);
for (int i = 0; i < threadArray.length; i++) {
Thread t = threadArray[i];
Set<Thread> threadSet = new HashSet<>(Thread.getAllStackTraces().keySet());
Thread[] threadArray = threadSet.toArray(new Thread[0]);
for (Thread t : threadArray) {
// System.out.println(t.getId()+ " "+t.getThreadGroup());
if (t.getName().equals("RMI Reaper")) {
t.interrupt();
......@@ -157,8 +170,8 @@ public class TLCRunner {
}
class StreamGobbler extends Thread {
private InputStream is;
private ArrayList<String> log;
private final InputStream is;
private final ArrayList<String> log;
public ArrayList<String> getLog() {
return log;
......@@ -166,14 +179,14 @@ class StreamGobbler extends Thread {
StreamGobbler(InputStream is) {
this.is = is;
this.log = new ArrayList<String>();
this.log = new ArrayList<>();
}
public void run() {
try {
InputStreamReader isr = new InputStreamReader(is, "UTF-8");
InputStreamReader isr = new InputStreamReader(is, StandardCharsets.UTF_8);
BufferedReader br = new BufferedReader(isr);
String line = null;
String line;
while ((line = br.readLine()) != null) {
System.out.println("> " + line);
log.add(line);
......
src/main/java/de/tlc4b/Translator.java
+ 20
− 36
View file @ d4c28859
package de.tlc4b;
import java.io.File;
import java.io.IOException;
import java.util.HashSet;
import java.util.Map;
import java.util.Set;
import de.be4.classicalb.core.parser.BParser;
import de.be4.classicalb.core.parser.analysis.prolog.RecursiveMachineLoader;
......@@ -21,14 +20,13 @@ import de.tlc4b.analysis.Renamer;
import de.tlc4b.analysis.Typechecker;
import de.tlc4b.analysis.UnsupportedConstructsFinder;
import de.tlc4b.analysis.UsedStandardModules;
import de.tlc4b.analysis.UsedStandardModules.STANDARD_MODULES;
import de.tlc4b.analysis.transformation.DefinitionsEliminator;
import de.tlc4b.analysis.transformation.SeesEliminator;
import de.tlc4b.analysis.transformation.SequenceSubstitutionsEliminator;
import de.tlc4b.analysis.transformation.SetComprehensionOptimizer;
import de.tlc4b.analysis.typerestriction.TypeRestrictor;
import de.tlc4b.analysis.unchangedvariables.InvariantPreservationAnalysis;
import de.tlc4b.analysis.unchangedvariables.UnchangedVariablesFinder;
import de.tlc4b.exceptions.TLC4BIOException;
import de.tlc4b.prettyprint.TLAPrinter;
import de.tlc4b.tla.Generator;
import de.tlc4b.tlc.TLCOutputInfo;
......@@ -36,41 +34,35 @@ import de.tlc4b.tlc.TLCOutputInfo;
public class Translator {
private String machineString;
private Start start;
private final Start start;
private Map<String, Start> parsedMachines;
private String moduleString;
private String configString;
private String machineName;
private String ltlFormula;
private PPredicate constantsSetup;
private HashSet<STANDARD_MODULES> standardModulesToBeCreated;
private Set<String> standardModulesToBeCreated;
private TLCOutputInfo tlcOutputInfo;
private String translatedLTLFormula;
public Translator(String machineString) throws BCompoundException {
this.machineString = machineString;
BParser parser = new BParser("Testing");
start = parser.parse(machineString, false);
start = parser.parseMachine(machineString);
}
public Translator(String machineString, String ltlFormula) throws BCompoundException {
this.machineString = machineString;
this.ltlFormula = ltlFormula;
BParser parser = new BParser("Testing");
start = parser.parse(machineString, false);
start = parser.parseMachine(machineString);
}
public Translator(String machineName, File machineFile, String ltlFormula, String constantSetup)
throws BCompoundException, IOException {
public Translator(String machineName, File machineFile, String ltlFormula, String constantSetup) throws BCompoundException {
this.machineName = machineName;
this.ltlFormula = ltlFormula;
BParser parser = new BParser(machineName);
try {
start = parser.parseFile(machineFile, false);
} catch (NoClassDefFoundError e) {
throw new TLC4BIOException("Definitions file cannot be found.");
}
start = parser.parseFile(machineFile);
// Definitions of definitions files are injected in the ast of the main
// machine
......@@ -82,11 +74,11 @@ public class Translator {
if (constantSetup != null) {
BParser con = new BParser();
Start start2 = null;
Start start2;
try {
start2 = con.parse("#FORMULA " + constantSetup, false);
start2 = con.parseFormula(constantSetup);
} catch (BCompoundException e) {
System.err.println("An error occured while parsing the constants setup predicate.");
System.err.println("An error occurred while parsing the constants setup predicate.");
throw e;
}
......@@ -96,20 +88,21 @@ public class Translator {
}
public void translate() {
UnsupportedConstructsFinder unsupportedConstructsFinder = new UnsupportedConstructsFinder(start);
unsupportedConstructsFinder.find();
start.apply(new UnsupportedConstructsFinder());
// ast transformation
SeesEliminator.eliminateSeesClauses(start, parsedMachines);
DefinitionsEliminator.eliminateDefinitions(start);
SequenceSubstitutionsEliminator sequenceSubstitutionsEliminator = new SequenceSubstitutionsEliminator(start);
// TODO move set comprehension optimizer behind the type checker
SetComprehensionOptimizer.optimizeSetComprehensions(start);
MachineContext machineContext = new MachineContext(machineName, start);
if (ltlFormula != null) {
machineContext.addLTLFromula(this.ltlFormula);
machineContext.addLTLFormula(this.ltlFormula);
}
if (this.constantsSetup != null) {
machineContext.setConstantSetupPredicate(constantsSetup);
......@@ -117,8 +110,9 @@ public class Translator {
machineContext.analyseMachine();
this.machineName = machineContext.getMachineName();
if (machineContext.machineContainsOperations()) {
TLC4BGlobals.setPrintCoverage(true);
// ignore coverage option if machine contains no operations
if (!machineContext.machineContainsOperations()) {
TLC4BGlobals.setPrintCoverage(false);
}
Typechecker typechecker = new Typechecker(machineContext);
......@@ -149,7 +143,7 @@ public class Translator {
standardModulesToBeCreated = usedModules.getStandardModulesToBeCreated();
PrimedNodesMarker primedNodesMarker = new PrimedNodesMarker(generator.getTlaModule().getOperations(),
machineContext);
machineContext, sequenceSubstitutionsEliminator.getPrimeNodes());
primedNodesMarker.start();
Renamer renamer = new Renamer(machineContext);
......@@ -159,7 +153,6 @@ public class Translator {
printer.start();
moduleString = printer.getStringbuilder().toString();
configString = printer.getConfigString().toString();
translatedLTLFormula = printer.geTranslatedLTLFormula();
tlcOutputInfo = new TLCOutputInfo(machineContext, renamer, typechecker, generator.getTlaModule(),
generator.getConfigFile());
......@@ -189,16 +182,7 @@ public class Translator {
return tlcOutputInfo;
}
public boolean containsUsedStandardModule(STANDARD_MODULES module) {
return standardModulesToBeCreated.contains(module);
}
public HashSet<UsedStandardModules.STANDARD_MODULES> getStandardModuleToBeCreated() {
public Set<String> getStandardModuleToBeCreated() {
return standardModulesToBeCreated;
}
public String getTranslatedLTLFormula() {
return translatedLTLFormula;
}
}
src/main/java/de/tlc4b/analysis/ConstantsEliminator.java
+ 32
− 53
View file @ d4c28859
......@@ -4,7 +4,6 @@ import java.util.Collection;
import java.util.HashMap;
import java.util.HashSet;
import java.util.Hashtable;
import java.util.Iterator;
import java.util.LinkedHashMap;
import java.util.LinkedList;
import java.util.Map.Entry;
......@@ -25,12 +24,11 @@ import de.be4.classicalb.core.parser.node.Node;
import de.be4.classicalb.core.parser.node.PDefinition;
import de.be4.classicalb.core.parser.node.PExpression;
import de.be4.classicalb.core.parser.node.PPredicate;
import de.be4.classicalb.core.parser.node.TIdentifierLiteral;
public class ConstantsEliminator extends DepthFirstAdapter {
private final Hashtable<Node, HashSet<Node>> dependsOnIdentifierTable;
private MachineContext machineContext;
private final MachineContext machineContext;
private ValuesOfIdentifierFinder valuesOfConstantsFinder;
private final HashMap<Node, Integer> integerValueTable;
......@@ -49,8 +47,8 @@ public class ConstantsEliminator extends DepthFirstAdapter {
}
public ConstantsEliminator(MachineContext machineContext) {
this.dependsOnIdentifierTable = new Hashtable<Node, HashSet<Node>>();
this.integerValueTable = new HashMap<Node, Integer>();
this.dependsOnIdentifierTable = new Hashtable<>();
this.integerValueTable = new HashMap<>();
this.machineContext = machineContext;
}
......@@ -71,12 +69,12 @@ public class ConstantsEliminator extends DepthFirstAdapter {
this.valuesOfConstantsFinder = new ValuesOfIdentifierFinder();
this.valueOfIdentifier = new LinkedHashMap<Node, Node>();
this.valueOfIdentifier = new LinkedHashMap<>();
// creating a new list of the constants, because constants will be
// removed from the original list
LinkedList<Node> oldConstants = new LinkedList<Node>(machineContext.getConstantArrayList());
if (oldConstants.size() > 0) {
LinkedList<Node> oldConstants = new LinkedList<>(machineContext.getConstantArrayList());
if (!oldConstants.isEmpty()) {
evalIdentifier(oldConstants);
}
......@@ -85,27 +83,24 @@ public class ConstantsEliminator extends DepthFirstAdapter {
}
private void evalIdentifier(Collection<Node> ids) {
LinkedList<PDefinition> defsList = new LinkedList<PDefinition>();
LinkedList<PDefinition> defsList = new LinkedList<>();
boolean newRun = true;
while (newRun) {
newRun = false;
Iterator<Node> itr = ids.iterator();
while (itr.hasNext()) {
AIdentifierExpression id = (AIdentifierExpression) itr.next();
for (Node node : ids) {
AIdentifierExpression id = (AIdentifierExpression) node;
if (valueOfIdentifier.containsKey(id))
continue;
HashSet<Node> idValues = valuesOfConstantsFinder.valuesOfIdentifierTable
.get(id);
HashSet<Node> idValues = valuesOfConstantsFinder.valuesOfIdentifierTable.get(id);
for (Node val : idValues) {
HashSet<Node> idsInVal = dependsOnIdentifierTable.get(val);
if (idsInVal.size() == 0) {
if (idsInVal.isEmpty()) {
// remove constants assignment of the properties clause
removeAssignmentInPropertiesClause(val);
removeConstant(id);
AExpressionDefinitionDefinition def = new AExpressionDefinitionDefinition(
(TIdentifierLiteral) id.getIdentifier().get(0)
.clone(),
new LinkedList<PExpression>(),
id.getIdentifier().get(0).clone(),
new LinkedList<>(),
(PExpression) val);
machineContext.getReferences().put(def, id);
machineContext.getReferences().put(id, def);
......@@ -120,9 +115,8 @@ public class ConstantsEliminator extends DepthFirstAdapter {
}
}
if (defsList.size() > 0) {
ADefinitionsMachineClause clause = machineContext
.getDefinitionMachineClause();
if (!defsList.isEmpty()) {
ADefinitionsMachineClause clause = machineContext.getDefinitionMachineClause();
if (null == clause) {
clause = new ADefinitionsMachineClause(defsList);
machineContext.getAbstractMachineParseUnit()
......@@ -168,19 +162,14 @@ public class ConstantsEliminator extends DepthFirstAdapter {
}
} else if (parent instanceof APropertiesMachineClause) {
machineContext.setPropertiesMachineClaus(null);
machineContext.getAbstractMachineParseUnit().getMachineClauses()
.remove(parent);
machineContext.getAbstractMachineParseUnit().getMachineClauses().remove(parent);
}
}
private void removeIdentifier(Collection<Node> collection,
Node identifierToRemove) {
Iterator<Node> itr = collection.iterator();
while (itr.hasNext()) {
Node id = itr.next();
HashSet<Node> idValues = valuesOfConstantsFinder.valuesOfIdentifierTable
.get(id);
for (Node id : collection) {
HashSet<Node> idValues = valuesOfConstantsFinder.valuesOfIdentifierTable.get(id);
for (Node val : idValues) {
HashSet<Node> idsInVal = dependsOnIdentifierTable.get(val);
idsInVal.remove(identifierToRemove);
......@@ -191,7 +180,7 @@ public class ConstantsEliminator extends DepthFirstAdapter {
class ConstantsInTreeFinder extends DepthFirstAdapter {
@Override
public void defaultIn(Node node) {
dependsOnIdentifierTable.put(node, new HashSet<Node>());
dependsOnIdentifierTable.put(node, new HashSet<>());
}
@Override
......@@ -228,39 +217,33 @@ public class ConstantsEliminator extends DepthFirstAdapter {
}
class ValuesOfIdentifierFinder extends DepthFirstAdapter {
private Hashtable<Node, HashSet<Node>> valuesOfIdentifierTable;
private HashSet<Node> identifiers;
private final Hashtable<Node, HashSet<Node>> valuesOfIdentifierTable;
private final HashSet<Node> identifiers;
public ValuesOfIdentifierFinder() {
valuesOfIdentifierTable = new Hashtable<Node, HashSet<Node>>();
valuesOfIdentifierTable = new Hashtable<>();
this.identifiers = new HashSet<Node>();
this.identifiers = new HashSet<>();
identifiers.addAll(machineContext.getConstants().values());
identifiers.addAll(machineContext.getScalarParameter().values());
Iterator<Node> itr = identifiers.iterator();
while (itr.hasNext()) {
Node id = itr.next();
valuesOfIdentifierTable.put(id, new HashSet<Node>());
for (Node id : identifiers) {
valuesOfIdentifierTable.put(id, new HashSet<>());
}
Node constraints = machineContext.getConstraintMachineClause();
AConstraintsMachineClause constraints = machineContext.getConstraintMachineClause();
if (constraints != null) {
analysePredicate(((AConstraintsMachineClause) constraints)
.getPredicates());
analysePredicate(constraints.getPredicates());
}
Node properties = machineContext.getPropertiesMachineClause();
APropertiesMachineClause properties = machineContext.getPropertiesMachineClause();
if (properties != null) {
analysePredicate(((APropertiesMachineClause) properties)
.getPredicates());
analysePredicate(properties.getPredicates());
}
}
private void analysePredicate(Node n) {
if (n instanceof AEqualPredicate) {
analyseEqualsPredicate((AEqualPredicate) n);
return;
} else if (n instanceof AGreaterPredicate) {
// analyseGreaterPredicate((AGreaterPredicate) n);
} else if (n instanceof ALessEqualPredicate) {
......@@ -268,7 +251,6 @@ public class ConstantsEliminator extends DepthFirstAdapter {
} else if (n instanceof AConjunctPredicate) {
analysePredicate(((AConjunctPredicate) n).getLeft());
analysePredicate(((AConjunctPredicate) n).getRight());
return;
}
}
......@@ -280,8 +262,7 @@ public class ConstantsEliminator extends DepthFirstAdapter {
Node right_ref = machineContext.getReferences().get(right);
if (left instanceof ACardExpression) {
Node ref = machineContext.getReferences().get(
((ACardExpression) left).getExpression());
Node ref = machineContext.getReferences().get(((ACardExpression) left).getExpression());
try {
AIntegerExpression intExpr = (AIntegerExpression) right;
int size = Integer.parseInt(intExpr.getLiteral().getText());
......@@ -297,7 +278,7 @@ public class ConstantsEliminator extends DepthFirstAdapter {
AIntegerExpression intExpr = (AIntegerExpression) left;
int size = Integer.parseInt(intExpr.getLiteral().getText());
integerValueTable.put(ref, size);
} catch (ClassCastException e) {
} catch (ClassCastException ignored) {
}
}
......@@ -308,8 +289,6 @@ public class ConstantsEliminator extends DepthFirstAdapter {
if (identifiers.contains(right_ref)) {
valuesOfIdentifierTable.get(right_ref).add(left);
}
return;
}
}
......
src/main/java/de/tlc4b/analysis/ConstantsEvaluator.java
+ 46
− 77
View file @ d4c28859
......@@ -5,7 +5,6 @@ import java.util.Collection;
import java.util.HashMap;
import java.util.HashSet;
import java.util.Hashtable;
import java.util.Iterator;
import java.util.LinkedHashMap;
import de.be4.classicalb.core.parser.analysis.DepthFirstAdapter;
......@@ -31,14 +30,14 @@ import de.be4.classicalb.core.parser.node.PPredicate;
*
*/
public class ConstantsEvaluator extends DepthFirstAdapter {
private LinkedHashMap<Node, HashSet<Node>> dependsOnIdentifierTable;
private MachineContext machineContext;
private ValuesOfIdentifierFinder valuesOfConstantsFinder;
private HashMap<Node, Integer> integerValueTable;
private final LinkedHashMap<Node, HashSet<Node>> dependsOnIdentifierTable;
private final MachineContext machineContext;
private final ValuesOfIdentifierFinder valuesOfConstantsFinder;
private final HashMap<Node, Integer> integerValueTable;
private final ArrayList<Node> propertiesList;
private final ArrayList<Node> invariantList;
private LinkedHashMap<Node, Node> valueOfIdentifier;
private final LinkedHashMap<Node, Node> valueOfIdentifier;
public Node getValueOfConstant(Node con) {
return valueOfIdentifier.get(con);
......@@ -65,11 +64,11 @@ public class ConstantsEvaluator extends DepthFirstAdapter {
}
public ConstantsEvaluator(MachineContext machineContext) {
this.dependsOnIdentifierTable = new LinkedHashMap<Node, HashSet<Node>>();
this.integerValueTable = new HashMap<Node, Integer>();
this.dependsOnIdentifierTable = new LinkedHashMap<>();
this.integerValueTable = new HashMap<>();
this.machineContext = machineContext;
this.propertiesList = new ArrayList<Node>();
this.invariantList = new ArrayList<Node>();
this.propertiesList = new ArrayList<>();
this.invariantList = new ArrayList<>();
ConstantsInTreeFinder constantInTreeFinder = new ConstantsInTreeFinder();
......@@ -77,21 +76,19 @@ public class ConstantsEvaluator extends DepthFirstAdapter {
machineContext.getConstantsSetup().apply(constantInTreeFinder);
}
APropertiesMachineClause properties = machineContext
.getPropertiesMachineClause();
APropertiesMachineClause properties = machineContext.getPropertiesMachineClause();
if (null != properties) {
properties.apply(constantInTreeFinder);
}
AConstraintsMachineClause constraints = machineContext
.getConstraintMachineClause();
AConstraintsMachineClause constraints = machineContext.getConstraintMachineClause();
if (null != constraints) {
constraints.apply(constantInTreeFinder);
}
this.valuesOfConstantsFinder = new ValuesOfIdentifierFinder();
this.valueOfIdentifier = new LinkedHashMap<Node, Node>();
this.valueOfIdentifier = new LinkedHashMap<>();
evalIdentifier(machineContext.getConstants().values());
evalIdentifier(machineContext.getScalarParameter().values());
......@@ -101,18 +98,15 @@ public class ConstantsEvaluator extends DepthFirstAdapter {
boolean newRun = true;
while (newRun) {
newRun = false;
Iterator<Node> itr = ids.iterator();
while (itr.hasNext()) {
Node id = itr.next();
for (Node id : ids) {
if (valueOfIdentifier.containsKey(id))
continue;
HashSet<Node> idValues = valuesOfConstantsFinder.valuesOfIdentifierTable
.get(id);
HashSet<Node> idValues = valuesOfConstantsFinder.valuesOfIdentifierTable.get(id);
for (Node val : idValues) {
HashSet<Node> idsInVal = dependsOnIdentifierTable.get(val);
idsInVal.remove(id);
if (idsInVal.size() == 0) {
if (idsInVal.isEmpty()) {
valueOfIdentifier.put(id, val);
removeIdentifier(ids, id);
newRun = true;
......@@ -123,13 +117,9 @@ public class ConstantsEvaluator extends DepthFirstAdapter {
}
}
private void removeIdentifier(Collection<Node> collection,
Node identifierToRemove) {
Iterator<Node> itr = collection.iterator();
while (itr.hasNext()) {
Node id = itr.next();
HashSet<Node> idValues = valuesOfConstantsFinder.valuesOfIdentifierTable
.get(id);
private void removeIdentifier(Collection<Node> collection, Node identifierToRemove) {
for (Node id : collection) {
HashSet<Node> idValues = valuesOfConstantsFinder.valuesOfIdentifierTable.get(id);
for (Node val : idValues) {
HashSet<Node> idsInVal = dependsOnIdentifierTable.get(val);
idsInVal.remove(identifierToRemove);
......@@ -140,7 +130,7 @@ public class ConstantsEvaluator extends DepthFirstAdapter {
class ConstantsInTreeFinder extends DepthFirstAdapter {
@Override
public void defaultIn(Node node) {
dependsOnIdentifierTable.put(node, new HashSet<Node>());
dependsOnIdentifierTable.put(node, new HashSet<>());
}
@Override
......@@ -151,7 +141,6 @@ public class ConstantsEvaluator extends DepthFirstAdapter {
if (parentSet != null) {
parentSet.addAll(set);
}
}
@Override
......@@ -186,41 +175,33 @@ public class ConstantsEvaluator extends DepthFirstAdapter {
}
class ValuesOfIdentifierFinder extends DepthFirstAdapter {
private Hashtable<Node, HashSet<Node>> valuesOfIdentifierTable;
private Hashtable<Node, ArrayList<PExpression>> rangeOfIdentifierTable;
private HashSet<Node> identifiers;
private final Hashtable<Node, HashSet<Node>> valuesOfIdentifierTable;
private final Hashtable<Node, ArrayList<PExpression>> rangeOfIdentifierTable;
private final HashSet<Node> identifiers;
public ValuesOfIdentifierFinder() {
this.valuesOfIdentifierTable = new Hashtable<Node, HashSet<Node>>();
this.rangeOfIdentifierTable = new Hashtable<Node, ArrayList<PExpression>>();
this.valuesOfIdentifierTable = new Hashtable<>();
this.rangeOfIdentifierTable = new Hashtable<>();
this.identifiers = new HashSet<Node>();
this.identifiers = new HashSet<>();
this.identifiers.addAll(machineContext.getConstants().values());
this.identifiers.addAll(machineContext.getScalarParameter()
.values());
this.identifiers.addAll(machineContext.getScalarParameter().values());
Iterator<Node> itr = identifiers.iterator();
while (itr.hasNext()) {
Node id = itr.next();
valuesOfIdentifierTable.put(id, new HashSet<Node>());
rangeOfIdentifierTable.put(id, new ArrayList<PExpression>());
for (Node id : identifiers) {
valuesOfIdentifierTable.put(id, new HashSet<>());
rangeOfIdentifierTable.put(id, new ArrayList<>());
}
Node constraints = machineContext.getConstraintMachineClause();
AConstraintsMachineClause constraints = machineContext.getConstraintMachineClause();
if (constraints != null) {
analysePredicate(
((AConstraintsMachineClause) constraints)
.getPredicates(),
false);
analysePredicate(constraints.getPredicates(), false);
}
if (machineContext.getConstantsSetup() != null) {
if (machineContext.getConstantsSetup() instanceof ADisjunctPredicate) {
analyseConstantSetupPredicate(machineContext
.getConstantsSetup());
analyseConstantSetupPredicate(machineContext.getConstantsSetup());
for (Node con : this.identifiers) {
ArrayList<PExpression> list = rangeOfIdentifierTable
.get(con);
ArrayList<PExpression> list = rangeOfIdentifierTable.get(con);
if (list.size() == 1) {
// there only one value for the constant con, hence
// con remains a constant
......@@ -230,21 +211,17 @@ public class ConstantsEvaluator extends DepthFirstAdapter {
} else {
analysePredicate(machineContext.getConstantsSetup(), true);
}
}
Node properties = machineContext.getPropertiesMachineClause();
APropertiesMachineClause properties = machineContext.getPropertiesMachineClause();
if (properties != null) {
PPredicate predicate = (PPredicate) ((APropertiesMachineClause) properties)
.getPredicates();
PPredicate predicate = properties.getPredicates();
analysePredicate(predicate, true);
}
Node invariantClause = machineContext.getInvariantMachineClause();
AInvariantMachineClause invariantClause = machineContext.getInvariantMachineClause();
if (invariantClause != null) {
analyseInvariantPredicate(((AInvariantMachineClause) invariantClause)
.getPredicates());
analyseInvariantPredicate(invariantClause.getPredicates());
}
}
......@@ -273,12 +250,10 @@ public class ConstantsEvaluator extends DepthFirstAdapter {
found = true;
}
}
if (found == false) {
currentRange.add((PExpression) equals.getRight());
if (!found) {
currentRange.add(equals.getRight());
}
}
}
private void analyseInvariantPredicate(Node node) {
......@@ -303,7 +278,7 @@ public class ConstantsEvaluator extends DepthFirstAdapter {
}
if (isProperties) {
propertiesList.add((PPredicate) node);
propertiesList.add(node);
}
}
......@@ -314,13 +289,11 @@ public class ConstantsEvaluator extends DepthFirstAdapter {
Node right_ref = machineContext.getReferences().get(right);
if (left instanceof ACardExpression) {
Node ref = machineContext.getReferences().get(
((ACardExpression) left).getExpression());
Node ref = machineContext.getReferences().get(((ACardExpression) left).getExpression());
if (!machineContext.getConstants().containsValue(ref)) {
try {
AIntegerExpression intExpr = (AIntegerExpression) right;
int size = Integer.parseInt(intExpr.getLiteral()
.getText());
int size = Integer.parseInt(intExpr.getLiteral().getText());
integerValueTable.put(ref, size);
} catch (ClassCastException e) {
}
......@@ -328,15 +301,13 @@ public class ConstantsEvaluator extends DepthFirstAdapter {
}
if (right instanceof ACardExpression) {
Node ref = machineContext.getReferences().get(
((ACardExpression) right).getExpression());
Node ref = machineContext.getReferences().get(((ACardExpression) right).getExpression());
if (!machineContext.getConstants().containsValue(ref)) {
try {
AIntegerExpression intExpr = (AIntegerExpression) left;
int size = Integer.parseInt(intExpr.getLiteral()
.getText());
int size = Integer.parseInt(intExpr.getLiteral().getText());
integerValueTable.put(ref, size);
} catch (ClassCastException e) {
} catch (ClassCastException ignored) {
}
}
}
......@@ -348,8 +319,6 @@ public class ConstantsEvaluator extends DepthFirstAdapter {
if (identifiers.contains(right_ref)) {
valuesOfIdentifierTable.get(right_ref).add(left);
}
return;
}
}
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment