diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index da4ca559ba54fcf96a9650b3cbd7c5609e848397..64adccc29dc93299a116f351f0c99e4509288eeb 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -30,3 +30,27 @@ test:
paths:
- build/distributions
- build/libs
+
+deploy:
+ stage: deploy
+ only:
+ - master@general/stups/prob2-jupyter-kernel
+ needs:
+ - test
+ image: alpine:3
+ before_script:
+ - apk update
+ - apk add lftp openssh-client
+ script:
+ - |
+ filename="$(echo build/libs/prob2-jupyter-kernel-*-all.jar)"
+ case "${filename}" in
+ (*-SNAPSHOT-all.jar)
+ # Don't upload SNAPSHOT builds
+ ;;
+
+ (*-all.jar)
+ # Do upload release builds
+ LFTP_PASSWORD="${DEPLOY_PASSWORD}" lftp -c "set cmd:fail-exit true; set sftp:auto-confirm true; open --user ${DEPLOY_USERNAME} --env-password sftp://${DEPLOY_HOST}/${DEPLOY_REMOTE_BASEDIR}/downloads/prob2-jupyter/; mput build/libs/prob2-jupyter-kernel-*-all.jar"
+ ;;
+ esac
diff --git a/CHANGELOG.md b/CHANGELOG.md
index a41a539ce922a104a6ae0c0088ce9652d134e88d..7aa262a0be397f2bcae4fa27dfcc03af6c8ddcaa 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,8 +1,16 @@
# Changelog
-## [(next version)](https://gitlab.cs.uni-duesseldorf.de/api/v4/projects/848/jobs/artifacts/master/raw/build/libs/prob2-jupyter-kernel-1.3.1-SNAPSHOT-all.jar?job=test)
+## [(next version)](https://gitlab.cs.uni-duesseldorf.de/api/v4/projects/848/jobs/artifacts/master/raw/build/libs/prob2-jupyter-kernel-1.4.2-SNAPSHOT-all.jar?job=test)
-* Updated ProB 2 to version 4.0.0-SNAPSHOT.
+* (no changes yet)
+
+## [1.4.1](https://stups.hhu-hosting.de/downloads/prob2-jupyter/prob2-jupyter-kernel-1.4.1-all.jar)
+
+* Updated to ProB 1.12.1 (ProB Java API version 4.12.1).
+
+## [1.4.0](https://stups.hhu-hosting.de/downloads/prob2-jupyter/prob2-jupyter-kernel-1.4.0-all.jar)
+
+* Updated to ProB 1.12.0 (ProB Java API version 4.12.0).
* Added position information to formula evaluation errors (e. g. type or well-definedness errors).
* Changed `:exec` and `:init` to automatically set up constants and initialize the machine if necessary. Previously this caused an error "Machine is not initialised".
* Rewrote the kernel installation code in Python. This is mostly an internal change and shouldn't affect most users. As a side effect, uninstalling the kernel is now simpler and requires no extra steps after `jupyter kernelspec remove`.
diff --git a/README.md b/README.md
index 6b656381f0ec73756be8bdf4b9658d2bc89f3461..b80d0738380e89dae162065841f9674cca01ec16 100644
--- a/README.md
+++ b/README.md
@@ -8,9 +8,9 @@ This is a [Jupyter](https://jupyter.org/) kernel for the [ProB animator and mode
## Downloads
-* **[Download the latest version of the ProB2 Jupyter kernel here](https://stups.hhu-hosting.de/downloads/prob2-jupyter/prob2-jupyter-kernel-1.3.0-all.jar).**
+* **[Download the latest version of the ProB2 Jupyter kernel here](https://stups.hhu-hosting.de/downloads/prob2-jupyter/prob2-jupyter-kernel-1.4.1-all.jar).**
* Download links for previous versions can be found in the [changelog].
-* A [snapshot build](https://gitlab.cs.uni-duesseldorf.de/api/v4/projects/848/jobs/artifacts/master/raw/build/libs/prob2-jupyter-kernel-1.3.1-SNAPSHOT-all.jar?job=test) of the latest development version is also available. **Warning:** this is an unstable version that can contain bugs or breaking changes.
+* A [snapshot build](https://gitlab.cs.uni-duesseldorf.de/api/v4/projects/848/jobs/artifacts/master/raw/build/libs/prob2-jupyter-kernel-1.4.2-SNAPSHOT-all.jar?job=test) of the latest development version is also available. **Warning:** this is an unstable version that can contain bugs or breaking changes.
See the [requirements](#requirements) and [installation instructions](#installation) for information on how to install and use the downloaded jar file.
@@ -31,17 +31,10 @@ See the [requirements](#requirements) and [installation instructions](#installat
1. Ensure that all [requirements](#requirements) are installed.
2. [Download the latest version of the kernel](#downloads).
3. If Jupyter is installed in a virtual environment, activate it.
-4. Run `java -jar <jarfile> install` to install the kernel. (`<jarfile>` is the name of the jar file that you just downloaded.)
- * If you get a permission error when installing the kernel spec, add the option `--user` after `install`. This will install the kernel spec into your user home instead of the Python install directory (which may not be writable).
- * This assumes that Jupyter can be called using the command `jupyter`. To use a different command in place of `jupyter`, pass it as an argument after `install`, e. g. `java -jar <jarfile> install /path/to/jupyter`.
- * To use a different ProB home directory than the default, pass `-Dprob.home=/path/to/prob/home` before the `-jar` option. (The path must be absolute.)
-5. (Optional) The jar file can be deleted after installation.
-<!--
-New instructions once the next version is released:
4. Run `python3 <jarfile> install` to install the kernel. (`<jarfile>` is the name of the jar file that you just downloaded. Yes, you need to run the jar file using Python.)
* If you get a permission error when installing the kernel spec, add the option `--user` after `install`. This will install the kernel spec into your user home instead of the Python install directory (which may not be writable).
* To use a different ProB home directory than the default, set the environment variable `PROB_HOME` to the desired path. (The path must be absolute.)
--->
+5. (Optional) The jar file can be deleted after installation.
### For developers
diff --git a/build.gradle b/build.gradle
index 8313c6ddf1ebcf4c015c3e221526dc93e828dbf1..d0b2b41372c463277317abe3bfd831ee3370527e 100644
--- a/build.gradle
+++ b/build.gradle
@@ -8,16 +8,12 @@ plugins {
id("com.github.johnrengelman.shadow").version("7.1.2")
}
-version = "1.3.1-SNAPSHOT"
+version = "1.4.2-SNAPSHOT"
final isSnapshot = project.version.endsWith("-SNAPSHOT")
final SOURCE_ENCODING = "UTF-8"
-wrapper {
- gradleVersion = "7.6"
-}
-
repositories {
mavenCentral()
if (isSnapshot) {
@@ -35,11 +31,11 @@ configurations.all {
}
dependencies {
- implementation(group: "ch.qos.logback", name: "logback-classic", version: "1.3.5")
+ implementation(group: "ch.qos.logback", name: "logback-classic", version: "1.3.7")
implementation(group: "com.google.guava", name: "guava", version: "31.1-jre")
- implementation(group: "de.hhu.stups", name: "de.prob2.kernel", version: "4.0.0-SNAPSHOT")
+ implementation(group: "de.hhu.stups", name: "de.prob2.kernel", version: "4.12.1")
implementation(group: "io.github.spencerpark", name: "jupyter-jvm-basekernel", version: "2.3.0")
- implementation(group: "org.jetbrains", name: "annotations", version: "23.1.0")
+ implementation(group: "org.jetbrains", name: "annotations", version: "24.0.1")
implementation(group: "se.sawano.java", name: "alphanumeric-comparator", version: "1.4.1")
}
@@ -79,6 +75,6 @@ task installKernelSpec(type: Exec) {
executable = project.hasProperty("pythonCommand") ? project.pythonCommand : "python3"
args = [shadowJar.archiveFile.get().asFile, "--jar-path=" + shadowJar.archiveFile.get().asFile, "install"]
if (project.hasProperty("kernelspecUserInstall") && project.kernelspecUserInstall == "true") {
- args << "--user"
+ args("--user")
}
}
diff --git a/gradle/wrapper/gradle-wrapper.jar b/gradle/wrapper/gradle-wrapper.jar
index 943f0cbfa754578e88a3dae77fce6e3dea56edbf..c1962a79e29d3e0ab67b14947c167a862655af9b 100644
Binary files a/gradle/wrapper/gradle-wrapper.jar and b/gradle/wrapper/gradle-wrapper.jar differ
diff --git a/gradle/wrapper/gradle-wrapper.properties b/gradle/wrapper/gradle-wrapper.properties
index f398c33c4b08dabb3f1275e57706c2de4effb50c..37aef8d3f0c9fffa920a8290320a6c78095e1591 100644
--- a/gradle/wrapper/gradle-wrapper.properties
+++ b/gradle/wrapper/gradle-wrapper.properties
@@ -1,6 +1,6 @@
distributionBase=GRADLE_USER_HOME
distributionPath=wrapper/dists
-distributionUrl=https\://services.gradle.org/distributions/gradle-7.6-bin.zip
+distributionUrl=https\://services.gradle.org/distributions/gradle-8.1.1-bin.zip
networkTimeout=10000
zipStoreBase=GRADLE_USER_HOME
zipStorePath=wrapper/dists
diff --git a/gradlew b/gradlew
index 65dcd68d65c82f2a5338fded4af852f9caf93b93..aeb74cbb43e3931a2455a838345c3f6b8131aaa2 100755
--- a/gradlew
+++ b/gradlew
@@ -85,9 +85,6 @@ done
APP_BASE_NAME=${0##*/}
APP_HOME=$( cd "${APP_HOME:-./}" && pwd -P ) || exit
-# 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"'
-
# Use the maximum available, or set MAX_FD != -1 to use that value.
MAX_FD=maximum
@@ -144,7 +141,7 @@ 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=SC3045
MAX_FD=$( ulimit -H -n ) ||
warn "Could not query maximum file descriptor limit"
esac
@@ -152,7 +149,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=SC3045
ulimit -n "$MAX_FD" ||
warn "Could not set maximum file descriptor limit to $MAX_FD"
esac
@@ -197,6 +194,10 @@ if "$cygwin" || "$msys" ; then
done
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
diff --git a/notebooks/experiments/SMT_Translation_Experiments.ipynb b/notebooks/experiments/SMT_Translation_Experiments.ipynb
index 36751390c3963ac242cce07026426ea19a692307..ba6a80cadc917c0a0a98d0c0f01992cfe2421687 100644
--- a/notebooks/experiments/SMT_Translation_Experiments.ipynb
+++ b/notebooks/experiments/SMT_Translation_Experiments.ipynb
@@ -15,12 +15,25 @@
"metadata": {},
"outputs": [
{
- "ename": "CommandExecutionException",
- "evalue": ":solve: Computation not completed: no solution found (but one might exist), reason: solver_not_available",
- "output_type": "error",
- "traceback": [
- "\u001b[1m\u001b[31m:solve: Computation not completed: no solution found (but one might exist), reason: solver_not_available\u001b[0m"
- ]
+ "data": {
+ "text/markdown": [
+ "$\\mathit{TRUE}$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $\\mathit{r} = \\{2\\}$\n",
+ "* $\\mathit{f} = \\{(1\\mapsto 3),(2\\mapsto 6)\\}$"
+ ],
+ "text/plain": [
+ "TRUE\n",
+ "\n",
+ "Solution:\n",
+ "\tr = {2}\n",
+ "\tf = {(1↦3),(2↦6)}"
+ ]
+ },
+ "execution_count": 1,
+ "metadata": {},
+ "output_type": "execute_result"
}
],
"source": [
@@ -33,12 +46,17 @@
"metadata": {},
"outputs": [
{
- "ename": "CommandExecutionException",
- "evalue": ":solve: Computation not completed: no solution found (but one might exist), reason: solver_not_available",
- "output_type": "error",
- "traceback": [
- "\u001b[1m\u001b[31m:solve: Computation not completed: no solution found (but one might exist), reason: solver_not_available\u001b[0m"
- ]
+ "data": {
+ "text/markdown": [
+ "$\\mathit{FALSE}$"
+ ],
+ "text/plain": [
+ "FALSE"
+ ]
+ },
+ "execution_count": 2,
+ "metadata": {},
+ "output_type": "execute_result"
}
],
"source": [
@@ -104,10 +122,10 @@
{
"data": {
"text/markdown": [
- "Execution time: 0.359755436 seconds"
+ "Execution time: 0.453966125 seconds"
],
"text/plain": [
- "Execution time: 0.359755436 seconds"
+ "Execution time: 0.453966125 seconds"
]
},
"metadata": {},
@@ -210,11 +228,12 @@
"metadata": {},
"outputs": [
{
- "ename": "CommandExecutionException",
- "evalue": ":solve: Computation not completed: no solution found (but one might exist), reason: solver_not_available",
+ "ename": "WithSourceCodeException",
+ "evalue": "de.prob.exception.ProBError: Computation not completed\nProB returned error messages:\nError: no solution found (but one might exist), reason: solver_answered_unknown",
"output_type": "error",
"traceback": [
- "\u001b[1m\u001b[31m:solve: Computation not completed: no solution found (but one might exist), reason: solver_not_available\u001b[0m"
+ "\u001b[1m\u001b[30mError from ProB: \u001b[0m\u001b[1m\u001b[31mComputation not completed\u001b[0m",
+ "\u001b[1m\u001b[31mError: no solution found (but one might exist), reason: solver_answered_unknown\u001b[0m"
]
}
],
@@ -238,11 +257,12 @@
"metadata": {},
"outputs": [
{
- "ename": "CommandExecutionException",
- "evalue": ":solve: Computation not completed: no solution found (but one might exist), reason: solver_not_available",
+ "ename": "WithSourceCodeException",
+ "evalue": "de.prob.exception.ProBError: Computation not completed\nProB returned error messages:\nError: no solution found (but one might exist), reason: solver_answered_unknown",
"output_type": "error",
"traceback": [
- "\u001b[1m\u001b[31m:solve: Computation not completed: no solution found (but one might exist), reason: solver_not_available\u001b[0m"
+ "\u001b[1m\u001b[30mError from ProB: \u001b[0m\u001b[1m\u001b[31mComputation not completed\u001b[0m",
+ "\u001b[1m\u001b[31mError: no solution found (but one might exist), reason: solver_answered_unknown\u001b[0m"
]
}
],
diff --git a/notebooks/manual/ExternalFunctions.ipynb b/notebooks/manual/ExternalFunctions.ipynb
index faa876f364d5ed10ec65fabe45c22a9fb9920753..6ac06ec5d81e8f3aa7db3e840a39938b004a5c0f 100644
--- a/notebooks/manual/ExternalFunctions.ipynb
+++ b/notebooks/manual/ExternalFunctions.ipynb
@@ -416,7 +416,7 @@
{
"data": {
"text/markdown": [
- "$\\renewcommand{\\emptyset}{\\mathord\\varnothing}\\emptyset$"
+ "$\\def\\emptyset{\\mathord\\varnothing}\\emptyset$"
],
"text/plain": [
"∅"
@@ -498,7 +498,7 @@
{
"data": {
"text/markdown": [
- "$\\renewcommand{\\emptyset}{\\mathord\\varnothing}\\emptyset$"
+ "$\\def\\emptyset{\\mathord\\varnothing}\\emptyset$"
],
"text/plain": [
"∅"
@@ -2391,14 +2391,14 @@
"<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
"<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
" \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
- "<!-- Generated by graphviz version 2.50.0 (20211204.2007)\n",
+ "<!-- Generated by graphviz version 8.0.3 (20230416.2022)\n",
" -->\n",
"<!-- Title: state Pages: 1 -->\n",
"<svg width=\"176pt\" height=\"131pt\"\n",
" viewBox=\"0.00 0.00 176.00 131.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
"<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 127)\">\n",
"<title>state</title>\n",
- "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-127 172,-127 172,4 -4,4\"/>\n",
+ "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-127 172,-127 172,4 -4,4\"/>\n",
"<!-- 4 -->\n",
"<g id=\"node1\" class=\"node\">\n",
"<title>4</title>\n",
@@ -2414,15 +2414,15 @@
"<!-- 4->3 -->\n",
"<g id=\"edge1\" class=\"edge\">\n",
"<title>4->3</title>\n",
- "<path fill=\"none\" stroke=\"firebrick\" d=\"M14.23,-86.67C8.69,-76.96 4.4,-64.68 9,-54 10.57,-50.36 12.72,-46.92 15.21,-43.72\"/>\n",
- "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"17.81,-46.06 21.93,-36.3 12.62,-41.36 17.81,-46.06\"/>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M14.23,-86.67C8.69,-76.96 4.4,-64.68 9,-54 10.48,-50.57 12.48,-47.31 14.79,-44.27\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"16.86,-47.08 20.93,-37.3 11.65,-42.41 16.86,-47.08\"/>\n",
"<text text-anchor=\"middle\" x=\"16.5\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\">rel</text>\n",
"</g>\n",
"<!-- 3->4 -->\n",
"<g id=\"edge2\" class=\"edge\">\n",
"<title>3->4</title>\n",
- "<path fill=\"none\" stroke=\"firebrick\" d=\"M42.16,-36.18C39.56,-47.81 36.07,-63.42 33.09,-76.73\"/>\n",
- "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"29.61,-76.28 30.84,-86.8 36.44,-77.8 29.61,-76.28\"/>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M42.1,-36.47C39.52,-47.97 36.1,-63.28 33.17,-76.41\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"29.61,-75.28 30.84,-85.8 36.44,-76.8 29.61,-75.28\"/>\n",
"<text text-anchor=\"middle\" x=\"45.5\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\">rel</text>\n",
"</g>\n",
"<!-- 2 -->\n",
@@ -2434,8 +2434,8 @@
"<!-- 2->3 -->\n",
"<g id=\"edge3\" class=\"edge\">\n",
"<title>2->3</title>\n",
- "<path fill=\"none\" stroke=\"firebrick\" d=\"M106.62,-86.8C95.6,-74.47 80.58,-57.68 68.25,-43.89\"/>\n",
- "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"70.63,-41.3 61.36,-36.18 65.41,-45.96 70.63,-41.3\"/>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M106.62,-86.8C95.77,-74.67 81.06,-58.21 68.84,-44.55\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"71.89,-42.59 62.62,-37.47 66.67,-47.25 71.89,-42.59\"/>\n",
"<text text-anchor=\"middle\" x=\"95.5\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\">rel</text>\n",
"</g>\n",
"<!-- 1 -->\n",
@@ -2447,15 +2447,15 @@
"<!-- 2->1 -->\n",
"<g id=\"edge4\" class=\"edge\">\n",
"<title>2->1</title>\n",
- "<path fill=\"none\" stroke=\"firebrick\" d=\"M120.44,-86.62C120.04,-76.88 120.32,-64.61 123,-54 123.72,-51.14 124.71,-48.26 125.86,-45.43\"/>\n",
- "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"129.12,-46.72 130.2,-36.18 122.78,-43.75 129.12,-46.72\"/>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M120.44,-86.62C120.04,-76.88 120.32,-64.61 123,-54 123.67,-51.33 124.58,-48.64 125.63,-45.99\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"129.15,-47.73 130.2,-37.18 122.8,-44.77 129.15,-47.73\"/>\n",
"<text text-anchor=\"middle\" x=\"130.5\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\">rel</text>\n",
"</g>\n",
"<!-- 1->2 -->\n",
"<g id=\"edge5\" class=\"edge\">\n",
"<title>1->2</title>\n",
- "<path fill=\"none\" stroke=\"firebrick\" d=\"M141.52,-36.36C141.42,-46.09 140.65,-58.37 138,-69 137.33,-71.7 136.45,-74.45 135.45,-77.16\"/>\n",
- "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"132.11,-76.08 131.46,-86.65 138.56,-78.8 132.11,-76.08\"/>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M141.52,-36.36C141.42,-46.09 140.65,-58.37 138,-69 137.37,-71.52 136.57,-74.07 135.65,-76.6\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"132.08,-75.08 131.46,-85.65 138.54,-77.78 132.08,-75.08\"/>\n",
"<text text-anchor=\"middle\" x=\"147.5\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\">rel</text>\n",
"</g>\n",
"</g>\n",
@@ -2550,10 +2550,10 @@
{
"data": {
"text/markdown": [
- "$\\text{\"1.11.1-final\"}$"
+ "$\\text{\"1.12.0-final\"}$"
],
"text/plain": [
- "\"1.11.1-final\""
+ "\"1.12.0-final\""
]
},
"execution_count": 90,
@@ -2573,10 +2573,10 @@
{
"data": {
"text/markdown": [
- "$\\text{\"1125ea39af78125a39093c65a0af783b7636b362\"}$"
+ "$\\text{\"fef4b935b59d76e353ab67230f6206b15f903f4b\"}$"
],
"text/plain": [
- "\"1125ea39af78125a39093c65a0af783b7636b362\""
+ "\"fef4b935b59d76e353ab67230f6206b15f903f4b\""
]
},
"execution_count": 91,
@@ -2596,10 +2596,10 @@
{
"data": {
"text/markdown": [
- "$\\text{\"Wed Dec 29 13:14:39 2021 +0100\"}$"
+ "$\\text{\"Wed Apr 5 14:57:01 2023 +0200\"}$"
],
"text/plain": [
- "\"Wed Dec 29 13:14:39 2021 +0100\""
+ "\"Wed Apr 5 14:57:01 2023 +0200\""
]
},
"execution_count": 92,
@@ -2619,10 +2619,10 @@
{
"data": {
"text/markdown": [
- "$\\text{\"1.17.35\\\"\\n\"}$"
+ "$\\text{\"1.17.0.6+10\"}$"
],
"text/plain": [
- "\"1.17.35\\\"\\n\""
+ "\"1.17.0.6+10\""
]
},
"execution_count": 93,
@@ -2665,10 +2665,10 @@
{
"data": {
"text/markdown": [
- "$\\text{\"6/1/2022 - 13h37 50s\"}$"
+ "$\\text{\"25/4/2023 - 11h23 27s\"}$"
],
"text/plain": [
- "\"6/1/2022 - 13h37 50s\""
+ "\"25/4/2023 - 11h23 27s\""
]
},
"execution_count": 95,
@@ -2704,10 +2704,10 @@
{
"data": {
"text/markdown": [
- "$166651936$"
+ "$168811280$"
],
"text/plain": [
- "166651936"
+ "168811280"
]
},
"execution_count": 96,
@@ -2819,10 +2819,10 @@
{
"data": {
"text/markdown": [
- "$1641472670$"
+ "$1682414607$"
],
"text/plain": [
- "1641472670"
+ "1682414607"
]
},
"execution_count": 101,
@@ -2842,10 +2842,10 @@
{
"data": {
"text/markdown": [
- "$2295$"
+ "$4273$"
],
"text/plain": [
- "2295"
+ "4273"
]
},
"execution_count": 102,
@@ -2865,10 +2865,10 @@
{
"data": {
"text/markdown": [
- "$18724$"
+ "$18128$"
],
"text/plain": [
- "18724"
+ "18128"
]
},
"execution_count": 103,
@@ -3130,7 +3130,7 @@
{
"data": {
"text/markdown": [
- "$\\renewcommand{\\emptyset}{\\mathord\\varnothing}\\emptyset$"
+ "$\\def\\emptyset{\\mathord\\varnothing}\\emptyset$"
],
"text/plain": [
"∅"
@@ -3153,7 +3153,7 @@
{
"data": {
"text/markdown": [
- "$\\renewcommand{\\emptyset}{\\mathord\\varnothing}\\emptyset$"
+ "$\\def\\emptyset{\\mathord\\varnothing}\\emptyset$"
],
"text/plain": [
"∅"
@@ -3176,7 +3176,7 @@
{
"data": {
"text/markdown": [
- "$\\renewcommand{\\emptyset}{\\mathord\\varnothing}\\emptyset$"
+ "$\\def\\emptyset{\\mathord\\varnothing}\\emptyset$"
],
"text/plain": [
"∅"
@@ -3199,7 +3199,7 @@
{
"data": {
"text/markdown": [
- "$\\renewcommand{\\emptyset}{\\mathord\\varnothing}\\emptyset$"
+ "$\\def\\emptyset{\\mathord\\varnothing}\\emptyset$"
],
"text/plain": [
"∅"
@@ -3222,7 +3222,7 @@
{
"data": {
"text/markdown": [
- "$\\renewcommand{\\emptyset}{\\mathord\\varnothing}\\emptyset$"
+ "$\\def\\emptyset{\\mathord\\varnothing}\\emptyset$"
],
"text/plain": [
"∅"
@@ -3245,7 +3245,7 @@
{
"data": {
"text/markdown": [
- "$\\renewcommand{\\emptyset}{\\mathord\\varnothing}\\emptyset$"
+ "$\\def\\emptyset{\\mathord\\varnothing}\\emptyset$"
],
"text/plain": [
"∅"
@@ -3268,10 +3268,10 @@
{
"data": {
"text/markdown": [
- "$\\{\\text{\"9541282a9b1c250d7244201817fbc6f332a22940\"}\\}$"
+ "$\\{\\text{\"1e2334f66e80dac4a856a360e3e9add2c7fd9e58\"}\\}$"
],
"text/plain": [
- "{\"9541282a9b1c250d7244201817fbc6f332a22940\"}"
+ "{\"1e2334f66e80dac4a856a360e3e9add2c7fd9e58\"}"
]
},
"execution_count": 119,
@@ -4415,7 +4415,7 @@
{
"data": {
"text/markdown": [
- "$\\renewcommand{\\emptyset}{\\mathord\\varnothing}\\mathit{rec}(\\mathit{length}\\in 6,\\mathit{position}\\in 1,\\mathit{string}\\in\\text{\"abcdef\"},\\mathit{submatches}\\in\\emptyset)$"
+ "$\\def\\emptyset{\\mathord\\varnothing}\\mathit{rec}(\\mathit{length}\\in 6,\\mathit{position}\\in 1,\\mathit{string}\\in\\text{\"abcdef\"},\\mathit{submatches}\\in\\emptyset)$"
],
"text/plain": [
"rec(length∈6,position∈1,string∈\"abcdef\",submatches∈∅)"
@@ -4438,7 +4438,7 @@
{
"data": {
"text/markdown": [
- "$\\renewcommand{\\emptyset}{\\mathord\\varnothing}\\mathit{rec}(\\mathit{length}\\in 3,\\mathit{position}\\in 13,\\mathit{string}\\in\\text{\"daf\"},\\mathit{submatches}\\in\\emptyset)$"
+ "$\\def\\emptyset{\\mathord\\varnothing}\\mathit{rec}(\\mathit{length}\\in 3,\\mathit{position}\\in 13,\\mathit{string}\\in\\text{\"daf\"},\\mathit{submatches}\\in\\emptyset)$"
],
"text/plain": [
"rec(length∈3,position∈13,string∈\"daf\",submatches∈∅)"
@@ -4491,7 +4491,7 @@
{
"data": {
"text/markdown": [
- "$\\renewcommand{\\emptyset}{\\mathord\\varnothing}\\mathit{rec}(\\mathit{length}\\in-1,\\mathit{position}\\in-1,\\mathit{string}\\in\\text{\"\"},\\mathit{submatches}\\in\\emptyset)$"
+ "$\\def\\emptyset{\\mathord\\varnothing}\\mathit{rec}(\\mathit{length}\\in-1,\\mathit{position}\\in-1,\\mathit{string}\\in\\text{\"\"},\\mathit{submatches}\\in\\emptyset)$"
],
"text/plain": [
"rec(length∈−1,position∈−1,string∈\"\",submatches∈∅)"
@@ -4578,7 +4578,7 @@
{
"data": {
"text/markdown": [
- "$\\renewcommand{\\emptyset}{\\mathord\\varnothing}\\emptyset$"
+ "$\\def\\emptyset{\\mathord\\varnothing}\\emptyset$"
],
"text/plain": [
"∅"
@@ -4656,7 +4656,7 @@
{
"data": {
"text/markdown": [
- "$\\renewcommand{\\emptyset}{\\mathord\\varnothing}\\mathit{rec}(\\mathit{length}\\in 3,\\mathit{position}\\in 5,\\mathit{string}\\in\\text{\"äéà\"},\\mathit{submatches}\\in\\emptyset)$"
+ "$\\def\\emptyset{\\mathord\\varnothing}\\mathit{rec}(\\mathit{length}\\in 3,\\mathit{position}\\in 5,\\mathit{string}\\in\\text{\"äéà\"},\\mathit{submatches}\\in\\emptyset)$"
],
"text/plain": [
"rec(length∈3,position∈5,string∈\"äéà\",submatches∈∅)"
@@ -5043,15 +5043,15 @@
"metadata": {},
"outputs": [
{
- "ename": "CommandExecutionException",
- "evalue": ":eval: UNKNOWN: \n### Exception occurred while calling external function: 'REGEX_SEARCH':regex_exception('One of *?+{ was not preceded by a valid regular expression.')\n ### File: /Users/Shared/Uni/SHK/ProB2/prob_prolog/stdlib/LibraryRegex.def\n ### Line: 34, Column: 1 until 88\n ### within: DEFINITION call of REGEX_SEARCH at Line: 1 Column: 0 until Line: 1 Column: 54\n\n",
+ "ename": "WithSourceCodeException",
+ "evalue": "de.prob.exception.ProBError: UNKNOWN\nProB returned error messages:\nError: Exception occurred while calling external function REGEX_SEARCH: regex_exception('One of *?+{ was not preceded by a valid regular expression.') (/Users/dgelessus/.prob/prob2-4.12.0/stdlib/LibraryRegex.def:45:1 to 45:88)",
"output_type": "error",
"traceback": [
- "\u001b[1m\u001b[31m:eval: UNKNOWN: \u001b[0m",
- "\u001b[1m\u001b[31m### Exception occurred while calling external function: 'REGEX_SEARCH':regex_exception('One of *?+{ was not preceded by a valid regular expression.')\u001b[0m",
- "\u001b[1m\u001b[31m ### File: /Users/Shared/Uni/SHK/ProB2/prob_prolog/stdlib/LibraryRegex.def\u001b[0m",
- "\u001b[1m\u001b[31m ### Line: 34, Column: 1 until 88\u001b[0m",
- "\u001b[1m\u001b[31m ### within: DEFINITION call of REGEX_SEARCH at Line: 1 Column: 0 until Line: 1 Column: 54\u001b[0m"
+ "\u001b[1m\u001b[30mError from ProB: \u001b[0m\u001b[1m\u001b[31mUNKNOWN\u001b[0m",
+ "\u001b[1m\u001b[31mError: Exception occurred while calling external function REGEX_SEARCH: regex_exception('One of *?+{ was not preceded by a valid regular expression.') (/Users/dgelessus/.prob/prob2-4.12.0/stdlib/LibraryRegex.def:45:1 to 45:88)\u001b[0m",
+ "\u001b[1m\u001b[30m string:STRING, submatches:seq(STRING)));\u001b[0m",
+ "\u001b[1m\u001b[30m \u001b[0m\u001b[1m\u001b[30m\u001b[41mREGEX_SEARCH(re_str,re_from,re_pat) == rec(length:0,position:0,string:\"\",submatches:[])\u001b[0m\u001b[1m\u001b[30m;\u001b[0m",
+ "\u001b[1m\u001b[30m // a version which ignores case (icase option)\u001b[0m"
]
}
],
@@ -5506,14 +5506,13 @@
"metadata": {},
"outputs": [
{
- "ename": "CommandExecutionException",
- "evalue": ":eval: NOT-WELL-DEFINED: \narg not positive x > 0\n ### Line: 1, Column: 27 until 30\n ### within: DEFINITION call of ASSERT_EXPR at Line: 1 Column: 10 until Line: 1 Column: 56\n\n",
+ "ename": "WithSourceCodeException",
+ "evalue": "de.prob.exception.ProBError: NOT-WELL-DEFINED\nProB returned error messages:\nError: arg not positive x > 0 (:1:27 to 1:30)",
"output_type": "error",
"traceback": [
- "\u001b[1m\u001b[31m:eval: NOT-WELL-DEFINED: \u001b[0m",
- "\u001b[1m\u001b[31marg not positive x > 0\u001b[0m",
- "\u001b[1m\u001b[31m ### Line: 1, Column: 27 until 30\u001b[0m",
- "\u001b[1m\u001b[31m ### within: DEFINITION call of ASSERT_EXPR at Line: 1 Column: 10 until Line: 1 Column: 56\u001b[0m"
+ "\u001b[1m\u001b[30mError from ProB: \u001b[0m\u001b[1m\u001b[31mNOT-WELL-DEFINED\u001b[0m",
+ "\u001b[1m\u001b[31mError: arg not positive x > 0 (:1:27 to 1:30)\u001b[0m",
+ "\u001b[1m\u001b[30mx=0 & res=ASSERT_EXPR(bool(\u001b[0m\u001b[1m\u001b[30m\u001b[41mx>0\u001b[0m\u001b[1m\u001b[30m),\"arg not positive\",10+x)\u001b[0m"
]
}
],
@@ -5609,13 +5608,13 @@
{
"data": {
"text/plain": [
- "ProB 2 Jupyter kernel: 1.2.1-SNAPSHOT (2aaa99bab781d6eca5a2b3388cca76b412fd52f6)\n",
- "ProB 2: 3.15.0 (6ee6df4eab62d20df40c36cd42108b62962ec41b)\n",
- "ProB B parser: 2.9.32 (7306d13499ba281a6e336c006d9fb23204624daa)\n",
+ "ProB 2 Jupyter kernel: 1.3.1-SNAPSHOT (b960640e155fc1441104e499894acd14e8f0fc07)\n",
+ "ProB 2: 4.12.0 (0356aaca15fde27915b8ab15c35a198fd381c9cd)\n",
+ "ProB B parser: 2.12.3 (99a64151f3bc82f987258619161831a8b9a7df01)\n",
"ProB CLI:\n",
- "\t1.11.1-final (1125ea39af78125a39093c65a0af783b7636b362)\n",
- "\tLast changed: Wed Dec 29 13:14:39 2021 +0100\n",
- "\tProlog: SICStus 4.7.0 (x86_64-darwin-18.7.0): Wed Jul 7 17:07:32 CEST 2021"
+ "\t1.12.0-final (fef4b935b59d76e353ab67230f6206b15f903f4b)\n",
+ "\tLast changed: Wed Apr 5 14:57:01 2023 +0200\n",
+ "\tProlog: SICStus 4.7.1 (x86_64-darwin-18.7.0): Fri Jan 21 19:45:28 CET 2022"
]
},
"execution_count": 194,
diff --git a/notebooks/manual/FloatsReals.ipynb b/notebooks/manual/FloatsReals.ipynb
index c781695306c3b4d5c50c30ee96133eed7f927770..2b7c9165a9c72e9327bbabe796ee003130e0e9e8 100644
--- a/notebooks/manual/FloatsReals.ipynb
+++ b/notebooks/manual/FloatsReals.ipynb
@@ -30,7 +30,7 @@
},
{
"cell_type": "code",
- "execution_count": 12,
+ "execution_count": 1,
"id": "cf76baf3",
"metadata": {
"vscode": {
@@ -47,7 +47,7 @@
"2.0"
]
},
- "execution_count": 12,
+ "execution_count": 1,
"metadata": {},
"output_type": "execute_result"
}
@@ -58,7 +58,7 @@
},
{
"cell_type": "code",
- "execution_count": 6,
+ "execution_count": 2,
"id": "941433ba",
"metadata": {
"vscode": {
@@ -75,7 +75,7 @@
"TRUE"
]
},
- "execution_count": 6,
+ "execution_count": 2,
"metadata": {},
"output_type": "execute_result"
}
@@ -98,7 +98,7 @@
},
{
"cell_type": "code",
- "execution_count": 22,
+ "execution_count": 3,
"id": "8925f6fe",
"metadata": {
"vscode": {
@@ -115,7 +115,7 @@
"2.0"
]
},
- "execution_count": 22,
+ "execution_count": 3,
"metadata": {},
"output_type": "execute_result"
}
@@ -126,7 +126,7 @@
},
{
"cell_type": "code",
- "execution_count": 23,
+ "execution_count": 4,
"id": "bbd73954",
"metadata": {
"vscode": {
@@ -143,7 +143,7 @@
"2"
]
},
- "execution_count": 23,
+ "execution_count": 4,
"metadata": {},
"output_type": "execute_result"
}
@@ -154,7 +154,7 @@
},
{
"cell_type": "code",
- "execution_count": 24,
+ "execution_count": 5,
"id": "838ea786",
"metadata": {
"vscode": {
@@ -171,7 +171,7 @@
"3"
]
},
- "execution_count": 24,
+ "execution_count": 5,
"metadata": {},
"output_type": "execute_result"
}
@@ -182,7 +182,7 @@
},
{
"cell_type": "code",
- "execution_count": 25,
+ "execution_count": 6,
"id": "ee31f934",
"metadata": {
"vscode": {
@@ -199,7 +199,7 @@
"−2"
]
},
- "execution_count": 25,
+ "execution_count": 6,
"metadata": {},
"output_type": "execute_result"
}
@@ -223,7 +223,7 @@
},
{
"cell_type": "code",
- "execution_count": 1,
+ "execution_count": 7,
"id": "65a66ec9",
"metadata": {
"vscode": {
@@ -240,7 +240,7 @@
"2.0"
]
},
- "execution_count": 1,
+ "execution_count": 7,
"metadata": {},
"output_type": "execute_result"
}
@@ -251,7 +251,7 @@
},
{
"cell_type": "code",
- "execution_count": 2,
+ "execution_count": 8,
"id": "35ce95d5",
"metadata": {
"vscode": {
@@ -268,7 +268,7 @@
"FALSE"
]
},
- "execution_count": 2,
+ "execution_count": 8,
"metadata": {},
"output_type": "execute_result"
}
@@ -279,7 +279,7 @@
},
{
"cell_type": "code",
- "execution_count": 3,
+ "execution_count": 9,
"id": "531aa72d",
"metadata": {
"vscode": {
@@ -296,7 +296,7 @@
"FALSE"
]
},
- "execution_count": 3,
+ "execution_count": 9,
"metadata": {},
"output_type": "execute_result"
}
@@ -320,7 +320,7 @@
},
{
"cell_type": "code",
- "execution_count": 4,
+ "execution_count": 10,
"id": "528e647d",
"metadata": {
"vscode": {
@@ -345,7 +345,7 @@
"\ty = 0"
]
},
- "execution_count": 4,
+ "execution_count": 10,
"metadata": {},
"output_type": "execute_result"
}
@@ -369,7 +369,7 @@
},
{
"cell_type": "code",
- "execution_count": 7,
+ "execution_count": 11,
"id": "9356ea2c",
"metadata": {
"vscode": {
@@ -392,7 +392,7 @@
"\tx = 0.0"
]
},
- "execution_count": 7,
+ "execution_count": 11,
"metadata": {},
"output_type": "execute_result"
}
@@ -403,7 +403,7 @@
},
{
"cell_type": "code",
- "execution_count": 14,
+ "execution_count": 12,
"id": "b6d8671d",
"metadata": {
"vscode": {
@@ -426,7 +426,7 @@
"\tx = 1.0"
]
},
- "execution_count": 14,
+ "execution_count": 12,
"metadata": {},
"output_type": "execute_result"
}
@@ -451,7 +451,7 @@
},
{
"cell_type": "code",
- "execution_count": 9,
+ "execution_count": 13,
"id": "df6d2cd0",
"metadata": {
"vscode": {
@@ -468,7 +468,7 @@
"1.4142135623730951"
]
},
- "execution_count": 9,
+ "execution_count": 13,
"metadata": {},
"output_type": "execute_result"
}
@@ -479,7 +479,7 @@
},
{
"cell_type": "code",
- "execution_count": 16,
+ "execution_count": 14,
"id": "d2daab50",
"metadata": {
"vscode": {
@@ -496,7 +496,7 @@
"−2.4492935982947064E-16"
]
},
- "execution_count": 16,
+ "execution_count": 14,
"metadata": {},
"output_type": "execute_result"
}
@@ -507,7 +507,7 @@
},
{
"cell_type": "code",
- "execution_count": 11,
+ "execution_count": 15,
"id": "481e4f68",
"metadata": {
"vscode": {
@@ -532,7 +532,7 @@
"\tx = 0.5"
]
},
- "execution_count": 11,
+ "execution_count": 15,
"metadata": {},
"output_type": "execute_result"
}
@@ -543,7 +543,7 @@
},
{
"cell_type": "code",
- "execution_count": 12,
+ "execution_count": 16,
"id": "bfd74a24",
"metadata": {
"vscode": {
@@ -568,7 +568,7 @@
"\tx = 10.5"
]
},
- "execution_count": 12,
+ "execution_count": 16,
"metadata": {},
"output_type": "execute_result"
}
@@ -579,7 +579,7 @@
},
{
"cell_type": "code",
- "execution_count": 13,
+ "execution_count": 17,
"id": "34ca2773",
"metadata": {
"vscode": {
@@ -596,7 +596,7 @@
"2.718281828459045"
]
},
- "execution_count": 13,
+ "execution_count": 17,
"metadata": {},
"output_type": "execute_result"
}
@@ -607,7 +607,7 @@
},
{
"cell_type": "code",
- "execution_count": 14,
+ "execution_count": 18,
"id": "4b24407f",
"metadata": {
"vscode": {
@@ -624,7 +624,7 @@
"−1.0"
]
},
- "execution_count": 14,
+ "execution_count": 18,
"metadata": {},
"output_type": "execute_result"
}
@@ -635,7 +635,7 @@
},
{
"cell_type": "code",
- "execution_count": 21,
+ "execution_count": 19,
"id": "ec855071",
"metadata": {
"vscode": {
@@ -652,7 +652,7 @@
"2.2"
]
},
- "execution_count": 21,
+ "execution_count": 19,
"metadata": {},
"output_type": "execute_result"
}
@@ -663,7 +663,7 @@
},
{
"cell_type": "code",
- "execution_count": 17,
+ "execution_count": 20,
"id": "c0bf9060",
"metadata": {
"vscode": {
@@ -680,7 +680,7 @@
"10.0"
]
},
- "execution_count": 17,
+ "execution_count": 20,
"metadata": {},
"output_type": "execute_result"
}
@@ -691,7 +691,7 @@
},
{
"cell_type": "code",
- "execution_count": 18,
+ "execution_count": 21,
"id": "152d2052",
"metadata": {
"vscode": {
@@ -708,7 +708,7 @@
"1.0"
]
},
- "execution_count": 18,
+ "execution_count": 21,
"metadata": {},
"output_type": "execute_result"
}
@@ -719,7 +719,7 @@
},
{
"cell_type": "code",
- "execution_count": 19,
+ "execution_count": 22,
"id": "0a81f12f",
"metadata": {
"vscode": {
@@ -736,7 +736,7 @@
"1.4142135623730951"
]
},
- "execution_count": 19,
+ "execution_count": 22,
"metadata": {},
"output_type": "execute_result"
}
@@ -747,7 +747,7 @@
},
{
"cell_type": "code",
- "execution_count": 20,
+ "execution_count": 23,
"id": "4669fcd2",
"metadata": {
"vscode": {
@@ -764,7 +764,7 @@
"1.0"
]
},
- "execution_count": 20,
+ "execution_count": 23,
"metadata": {},
"output_type": "execute_result"
}
diff --git a/notebooks/models/Jars_DieHard_Puzzle.ipynb b/notebooks/models/Jars_DieHard_Puzzle.ipynb
index f2386e6b6734c4ab958ea54f29c166ebcf28648b..3d01b202b00125b5df1c1eb967607f10f33a0e68 100644
--- a/notebooks/models/Jars_DieHard_Puzzle.ipynb
+++ b/notebooks/models/Jars_DieHard_Puzzle.ipynb
@@ -654,14 +654,14 @@
"<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
"<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
" \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
- "<!-- Generated by graphviz version 2.50.0 (20211204.2007)\n",
+ "<!-- Generated by graphviz version 8.0.3 (20230416.2022)\n",
" -->\n",
"<!-- Title: g Pages: 1 -->\n",
- "<svg width=\"303pt\" height=\"110pt\"\n",
- " viewBox=\"0.00 0.00 303.00 110.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+ "<svg width=\"291pt\" height=\"110pt\"\n",
+ " viewBox=\"0.00 0.00 291.00 110.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
"<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 106)\">\n",
"<title>g</title>\n",
- "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-106 299,-106 299,4 -4,4\"/>\n",
+ "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-106 287,-106 287,4 -4,4\"/>\n",
"<!-- Noderoot -->\n",
"<g id=\"node1\" class=\"node\">\n",
"<title>Noderoot</title>\n",
@@ -678,36 +678,36 @@
"<!-- Node1->Noderoot -->\n",
"<g id=\"edge1\" class=\"edge\">\n",
"<title>Node1->Noderoot</title>\n",
- "<path fill=\"none\" stroke=\"black\" d=\"M89.6,-74.5C81.43,-71.72 72.3,-68.6 63.62,-65.64\"/>\n",
- "<polygon fill=\"black\" stroke=\"black\" points=\"64.68,-62.31 54.08,-62.39 62.42,-68.93 64.68,-62.31\"/>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M90.07,-74.66C82.07,-71.93 73.1,-68.88 64.53,-65.95\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"65.95,-62.4 55.35,-62.48 63.69,-69.02 65.95,-62.4\"/>\n",
"</g>\n",
"<!-- Node2 -->\n",
"<g id=\"node3\" class=\"node\">\n",
"<title>Node2</title>\n",
"<polygon fill=\"white\" stroke=\"black\" points=\"90,-0.5 90,-46.5 144,-46.5 144,-0.5 90,-0.5\"/>\n",
"<text text-anchor=\"middle\" x=\"117\" y=\"-31.3\" font-family=\"Times,serif\" font-size=\"14.00\">ran</text>\n",
- "<polyline fill=\"none\" stroke=\"black\" points=\"90,-23.5 144,-23.5 \"/>\n",
+ "<polyline fill=\"none\" stroke=\"black\" points=\"90,-23.5 144,-23.5\"/>\n",
"<text text-anchor=\"middle\" x=\"117\" y=\"-8.3\" font-family=\"Times,serif\" font-size=\"14.00\">{3,4}</text>\n",
"</g>\n",
"<!-- Node2->Noderoot -->\n",
"<g id=\"edge2\" class=\"edge\">\n",
"<title>Node2->Noderoot</title>\n",
- "<path fill=\"none\" stroke=\"black\" d=\"M89.6,-32.5C81.43,-35.28 72.3,-38.4 63.62,-41.36\"/>\n",
- "<polygon fill=\"black\" stroke=\"black\" points=\"62.42,-38.07 54.08,-44.61 64.68,-44.69 62.42,-38.07\"/>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M90.07,-32.34C82.07,-35.07 73.1,-38.12 64.53,-41.05\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"63.69,-37.98 55.35,-44.52 65.95,-44.6 63.69,-37.98\"/>\n",
"</g>\n",
"<!-- Node3 -->\n",
"<g id=\"node4\" class=\"node\">\n",
"<title>Node3</title>\n",
- "<polygon fill=\"white\" stroke=\"black\" points=\"180,-0.5 180,-46.5 295,-46.5 295,-0.5 180,-0.5\"/>\n",
- "<text text-anchor=\"middle\" x=\"237.5\" y=\"-31.3\" font-family=\"Times,serif\" font-size=\"14.00\">level</text>\n",
- "<polyline fill=\"none\" stroke=\"black\" points=\"180,-23.5 295,-23.5 \"/>\n",
- "<text text-anchor=\"middle\" x=\"237.5\" y=\"-8.3\" font-family=\"Times,serif\" font-size=\"14.00\">{(j3↦3),(j5↦4)}</text>\n",
+ "<polygon fill=\"white\" stroke=\"black\" points=\"180,-0.5 180,-46.5 283,-46.5 283,-0.5 180,-0.5\"/>\n",
+ "<text text-anchor=\"middle\" x=\"231.5\" y=\"-31.3\" font-family=\"Times,serif\" font-size=\"14.00\">level</text>\n",
+ "<polyline fill=\"none\" stroke=\"black\" points=\"180,-23.5 283,-23.5\"/>\n",
+ "<text text-anchor=\"middle\" x=\"231.5\" y=\"-8.3\" font-family=\"Times,serif\" font-size=\"14.00\">{(j3↦3),(j5↦4)}</text>\n",
"</g>\n",
"<!-- Node3->Node2 -->\n",
"<g id=\"edge3\" class=\"edge\">\n",
"<title>Node3->Node2</title>\n",
- "<path fill=\"none\" stroke=\"black\" d=\"M179.68,-23.5C171.01,-23.5 162.26,-23.5 154.2,-23.5\"/>\n",
- "<polygon fill=\"black\" stroke=\"black\" points=\"154.04,-20 144.04,-23.5 154.04,-27 154.04,-20\"/>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M180.17,-23.5C171.66,-23.5 162.97,-23.5 154.89,-23.5\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"154.94,-20 144.94,-23.5 154.94,-27 154.94,-20\"/>\n",
"</g>\n",
"</g>\n",
"</svg>\n"
diff --git a/notebooks/models/NFA_to_DFA.ipynb b/notebooks/models/NFA_to_DFA.ipynb
index f57b2a025c6d6f008d6d5f04ef3fe954a742bf93..a2fae6b34f13642bd2cd12f040686e045749a29e 100644
--- a/notebooks/models/NFA_to_DFA.ipynb
+++ b/notebooks/models/NFA_to_DFA.ipynb
@@ -8,7 +8,7 @@
{
"data": {
"text/markdown": [
- "$\\newcommand{\\Inter}{\\bigcap\\nolimits}\\newcommand{\\bfalse}{\\mathord\\bot}\\newcommand{\\qdot}{\\mathord{\\mkern1mu\\cdot\\mkern1mu}}\\newcommand{\\binter}{\\mathbin{\\mkern1mu\\cap\\mkern1mu}}\\newcommand{\\dprod}{\\mathbin\\otimes}\\newcommand{\\usucc}{\\mathop{\\mathrm{succ}}\\nolimits}\\newcommand{\\trel}{\\mathbin{<\\mkern-6mu<\\mkern-10mu-\\mkern-10mu>}}\\newcommand{\\strel}{\\mathbin{<\\mkern-6mu<\\mkern-10mu-\\mkern-10mu>\\mkern-6mu>}}\\newcommand{\\Bool}{\\mathord{\\mathrm{BOOL}}}\\newcommand{\\rel}{\\mathbin{<\\mkern-10mu-\\mkern-10mu>}}\\newcommand{\\pprod}{\\mathbin\\mid}\\newcommand{\\id}{\\mathop{\\mathrm{id}}\\nolimits}\\newcommand{\\cprod}{\\mathbin\\times}\\newcommand{\\ran}{\\mathop{\\mathrm{ran}}\\nolimits}\\newcommand{\\nat}{\\mathord{\\mathbb N}}\\newcommand{\\pown}{\\mathop{\\mathbb P_1}\\nolimits}\\newcommand{\\finite}{\\mathop{\\mathrm{finite}}\\nolimits}\\newcommand{\\inter}{\\mathop{\\mathrm{inter}}\\nolimits}\\newcommand{\\prjone}{\\mathop{\\mathrm{prj}_1}\\nolimits}\\newcommand{\\defi}{\\mathrel{≙}}\\newcommand{\\ranres}{\\mathbin▷}\\newcommand{\\prjtwo}{\\mathop{\\mathrm{prj}_2}\\nolimits}\\newcommand{\\upred}{\\mathop{\\mathrm{pred}}\\nolimits}\\newcommand{\\fcomp}{\\mathbin;}\\newcommand{\\tbij}{\\mathbin⤖}\\newcommand{\\pfun}{\\mathbin↦}\\newcommand{\\tfun}{\\mathbin→}\\newcommand{\\card}{\\mathop{\\mathrm{card}}\\nolimits}\\newcommand{\\pinj}{\\mathbin⤔}\\newcommand{\\dom}{\\mathop{\\mathrm{dom}}\\nolimits}\\newcommand{\\bool}{\\mathop{\\mathrm{bool}}\\nolimits}\\newcommand{\\tinj}{\\mathbin↣}\\newcommand{\\domsub}{\\mathbin⩤}\\newcommand{\\Union}{\\bigcup\\nolimits}\\newcommand{\\limp}{\\mathbin\\Rightarrow}\\newcommand{\\ransub}{\\mathbin⩥}\\newcommand{\\psur}{\\mathbin⤅}\\newcommand{\\pow}{\\mathop{\\mathbb P\\hbox{}}\\nolimits}\\newcommand{\\bcmsuch}{\\mathrel{:\\mkern1mu\\mid}}\\newcommand{\\natn}{\\mathord{\\mathbb N_1}}\\newcommand{\\expn}{\\mathbin{\\widehat{\\mkern1em}}}\\newcommand{\\upto}{\\mathbin{.\\mkern1mu.}}\\newcommand{\\bcomp}{\\circ}\\newcommand{\\bcmin}{\\mathrel{:\\mkern1mu\\in}}\\newcommand{\\ovl}{\\mathbin{<\\mkern-11mu+}}\\newcommand{\\intg}{\\mathord{\\mathbb Z}}\\newcommand{\\domres}{\\mathbin◁}\\newcommand{\\tsur}{\\mathbin↠}\\newcommand{\\btrue}{\\mathord\\top}\\newcommand{\\union}{\\mathop{\\mathrm{union}}\\nolimits}\\newcommand{\\bcmeq}{\\mathrel{:\\mkern1mu=}}\\newcommand{\\leqv}{\\mathbin\\Leftrightarrow}\\renewcommand{\\emptyset}{\\mathord\\varnothing}\\newcommand{\\bunion}{\\mathbin{\\mkern1mu\\cup\\mkern1mu}}\\newcommand{\\srel}{\\mathbin{<\\mkern-10mu-\\mkern-10mu>\\mkern-6mu>}}\\text{All bsymb.sty definitions have been loaded.}$"
+ "$\\def\\Inter{\\bigcap\\nolimits}\\def\\bfalse{\\mathord\\bot}\\def\\qdot{\\mathord{\\mkern1mu\\cdot\\mkern1mu}}\\def\\binter{\\mathbin{\\mkern1mu\\cap\\mkern1mu}}\\def\\dprod{\\mathbin\\otimes}\\def\\usucc{\\mathop{\\mathrm{succ}}\\nolimits}\\def\\trel{\\mathbin{<\\mkern-6mu<\\mkern-10mu-\\mkern-10mu>}}\\def\\strel{\\mathbin{<\\mkern-6mu<\\mkern-10mu-\\mkern-10mu>\\mkern-6mu>}}\\def\\Bool{\\mathord{\\mathrm{BOOL}}}\\def\\rel{\\mathbin{<\\mkern-10mu-\\mkern-10mu>}}\\def\\pprod{\\mathbin\\mid}\\def\\id{\\mathop{\\mathrm{id}}\\nolimits}\\def\\cprod{\\mathbin\\times}\\def\\ran{\\mathop{\\mathrm{ran}}\\nolimits}\\def\\nat{\\mathord{\\mathbb N}}\\def\\pown{\\mathop{\\mathbb P_1}\\nolimits}\\def\\finite{\\mathop{\\mathrm{finite}}\\nolimits}\\def\\inter{\\mathop{\\mathrm{inter}}\\nolimits}\\def\\prjone{\\mathop{\\mathrm{prj}_1}\\nolimits}\\def\\defi{\\mathrel{≙}}\\def\\ranres{\\mathbin▷}\\def\\prjtwo{\\mathop{\\mathrm{prj}_2}\\nolimits}\\def\\upred{\\mathop{\\mathrm{pred}}\\nolimits}\\def\\fcomp{\\mathbin;}\\def\\tbij{\\mathbin⤖}\\def\\pfun{\\mathbin↦}\\def\\tfun{\\mathbin→}\\def\\card{\\mathop{\\mathrm{card}}\\nolimits}\\def\\pinj{\\mathbin⤔}\\def\\dom{\\mathop{\\mathrm{dom}}\\nolimits}\\def\\bool{\\mathop{\\mathrm{bool}}\\nolimits}\\def\\tinj{\\mathbin↣}\\def\\domsub{\\mathbin⩤}\\def\\Union{\\bigcup\\nolimits}\\def\\limp{\\mathbin\\Rightarrow}\\def\\ransub{\\mathbin⩥}\\def\\psur{\\mathbin⤅}\\def\\pow{\\mathop{\\mathbb P\\hbox{}}\\nolimits}\\def\\bcmsuch{\\mathrel{:\\mkern1mu\\mid}}\\def\\natn{\\mathord{\\mathbb N_1}}\\def\\expn{\\mathbin{\\widehat{\\mkern1em}}}\\def\\upto{\\mathbin{.\\mkern1mu.}}\\def\\bcomp{\\circ}\\def\\bcmin{\\mathrel{:\\mkern1mu\\in}}\\def\\ovl{\\mathbin{<\\mkern-11mu+}}\\def\\intg{\\mathord{\\mathbb Z}}\\def\\domres{\\mathbin◁}\\def\\tsur{\\mathbin↠}\\def\\btrue{\\mathord\\top}\\def\\union{\\mathop{\\mathrm{union}}\\nolimits}\\def\\bcmeq{\\mathrel{:\\mkern1mu=}}\\def\\leqv{\\mathbin\\Leftrightarrow}\\def\\emptyset{\\mathord\\varnothing}\\def\\bunion{\\mathbin{\\mkern1mu\\cup\\mkern1mu}}\\def\\srel{\\mathbin{<\\mkern-10mu-\\mkern-10mu>\\mkern-6mu>}}\\text{All bsymb.sty definitions have been loaded.}$"
],
"text/plain": [
"Your current environment uses plain text output; the bsymb.sty LaTeX commands will not be loaded."
@@ -252,14 +252,14 @@
"<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
"<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
" \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
- "<!-- Generated by graphviz version 2.50.0 (20211204.2007)\n",
+ "<!-- Generated by graphviz version 8.0.3 (20230416.2022)\n",
" -->\n",
"<!-- Title: state Pages: 1 -->\n",
"<svg width=\"144pt\" height=\"358pt\"\n",
" viewBox=\"0.00 0.00 144.00 358.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
"<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 354)\">\n",
"<title>state</title>\n",
- "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-354 140,-354 140,4 -4,4\"/>\n",
+ "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-354 140,-354 140,4 -4,4\"/>\n",
"<g id=\"clust1\" class=\"cluster\">\n",
"<title>cluster_Z</title>\n",
"<polygon fill=\"lightgrey\" stroke=\"lightgrey\" points=\"8,-8 8,-342 128,-342 128,-8 8,-8\"/>\n",
@@ -274,15 +274,15 @@
"<!-- z0->z0 -->\n",
"<g id=\"edge2\" class=\"edge\">\n",
"<title>z0->z0</title>\n",
- "<path fill=\"none\" stroke=\"firebrick\" d=\"M70.24,-298.93C80.02,-299.02 88,-297.71 88,-295 88,-293.35 85.04,-292.22 80.51,-291.61\"/>\n",
- "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"80.41,-288.1 70.24,-291.07 80.04,-295.09 80.41,-288.1\"/>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M70.24,-299.07C80.02,-299.16 88,-297.8 88,-295 88,-293.38 85.33,-292.24 81.19,-291.59\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"81.43,-288.03 71.24,-290.93 81.01,-295.02 81.43,-288.03\"/>\n",
"<text text-anchor=\"middle\" x=\"91.5\" y=\"-291.3\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
"</g>\n",
"<!-- z0->z0 -->\n",
"<g id=\"edge6\" class=\"edge\">\n",
"<title>z0->z0</title>\n",
- "<path fill=\"none\" stroke=\"sienna\" d=\"M70.2,-302.18C88.34,-304.2 106,-301.81 106,-295 106,-289.47 94.34,-286.85 80.24,-287.15\"/>\n",
- "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"79.94,-283.66 70.2,-287.82 80.41,-290.64 79.94,-283.66\"/>\n",
+ "<path fill=\"none\" stroke=\"sienna\" d=\"M70.2,-302.44C88.34,-304.53 106,-302.05 106,-295 106,-289.38 94.79,-286.66 81.05,-286.85\"/>\n",
+ "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"80.95,-283.42 71.2,-287.56 81.4,-290.4 80.95,-283.42\"/>\n",
"<text text-anchor=\"middle\" x=\"109.5\" y=\"-291.3\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
"</g>\n",
"<!-- z1 -->\n",
@@ -294,8 +294,8 @@
"<!-- z0->z1 -->\n",
"<g id=\"edge1\" class=\"edge\">\n",
"<title>z0->z1</title>\n",
- "<path fill=\"none\" stroke=\"firebrick\" d=\"M43,-276.8C43,-265.16 43,-249.55 43,-236.24\"/>\n",
- "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"46.5,-236.18 43,-226.18 39.5,-236.18 46.5,-236.18\"/>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M43,-276.8C43,-265.47 43,-250.36 43,-237.29\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"46.5,-237.47 43,-227.47 39.5,-237.47 46.5,-237.47\"/>\n",
"<text text-anchor=\"middle\" x=\"46.5\" y=\"-247.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
"</g>\n",
"<!-- z2 -->\n",
@@ -307,8 +307,8 @@
"<!-- z1->z2 -->\n",
"<g id=\"edge5\" class=\"edge\">\n",
"<title>z1->z2</title>\n",
- "<path fill=\"none\" stroke=\"sienna\" d=\"M43,-189.8C43,-178.16 43,-162.55 43,-149.24\"/>\n",
- "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"46.5,-149.18 43,-139.18 39.5,-149.18 46.5,-149.18\"/>\n",
+ "<path fill=\"none\" stroke=\"sienna\" d=\"M43,-189.8C43,-178.47 43,-163.36 43,-150.29\"/>\n",
+ "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"46.5,-150.47 43,-140.47 39.5,-150.47 46.5,-150.47\"/>\n",
"<text text-anchor=\"middle\" x=\"46.5\" y=\"-160.8\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
"</g>\n",
"<!-- z3 -->\n",
@@ -320,15 +320,15 @@
"<!-- z3->z3 -->\n",
"<g id=\"edge3\" class=\"edge\">\n",
"<title>z3->z3</title>\n",
- "<path fill=\"none\" stroke=\"sienna\" d=\"M70.24,-41.87C80.02,-42.04 88,-39.41 88,-34 88,-30.7 85.04,-28.44 80.51,-27.21\"/>\n",
- "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"80.55,-23.7 70.24,-26.13 79.82,-30.66 80.55,-23.7\"/>\n",
+ "<path fill=\"none\" stroke=\"sienna\" d=\"M70.24,-42.15C80.02,-42.32 88,-39.61 88,-34 88,-30.67 85.19,-28.36 80.86,-27.07\"/>\n",
+ "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"81.57,-23.51 71.24,-25.85 80.78,-30.47 81.57,-23.51\"/>\n",
"<text text-anchor=\"middle\" x=\"91.5\" y=\"-30.3\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
"</g>\n",
"<!-- z2->z3 -->\n",
"<g id=\"edge4\" class=\"edge\">\n",
"<title>z2->z3</title>\n",
- "<path fill=\"none\" stroke=\"sienna\" d=\"M43,-102.8C43,-91.16 43,-75.55 43,-62.24\"/>\n",
- "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"46.5,-62.18 43,-52.18 39.5,-62.18 46.5,-62.18\"/>\n",
+ "<path fill=\"none\" stroke=\"sienna\" d=\"M43,-102.8C43,-91.47 43,-76.36 43,-63.29\"/>\n",
+ "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"46.5,-63.47 43,-53.47 39.5,-63.47 46.5,-63.47\"/>\n",
"<text text-anchor=\"middle\" x=\"46.5\" y=\"-73.8\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
"</g>\n",
"</g>\n",
@@ -527,7 +527,7 @@
{
"data": {
"text/markdown": [
- "$\\renewcommand{\\emptyset}{\\mathord\\varnothing}\\{\\emptyset,\\{\\mathit{z0}\\},\\{\\mathit{z0},\\mathit{z1}\\},\\{\\mathit{z0},\\mathit{z2}\\},\\{\\mathit{z0},\\mathit{z3}\\},\\{\\mathit{z1}\\},\\{\\mathit{z0},\\mathit{z1},\\mathit{z2}\\},\\{\\mathit{z0},\\mathit{z1},\\mathit{z3}\\},\\{\\mathit{z1},\\mathit{z2}\\},\\{\\mathit{z1},\\mathit{z3}\\},\\{\\mathit{z0},\\mathit{z1},\\mathit{z2},\\mathit{z3}\\},\\{\\mathit{z2}\\},\\{\\mathit{z0},\\mathit{z2},\\mathit{z3}\\},\\{\\mathit{z1},\\mathit{z2},\\mathit{z3}\\},\\{\\mathit{z2},\\mathit{z3}\\},\\{\\mathit{z3}\\}\\}$"
+ "$\\def\\emptyset{\\mathord\\varnothing}\\{\\emptyset,\\{\\mathit{z0}\\},\\{\\mathit{z0},\\mathit{z1}\\},\\{\\mathit{z0},\\mathit{z2}\\},\\{\\mathit{z0},\\mathit{z3}\\},\\{\\mathit{z1}\\},\\{\\mathit{z0},\\mathit{z1},\\mathit{z2}\\},\\{\\mathit{z0},\\mathit{z1},\\mathit{z3}\\},\\{\\mathit{z1},\\mathit{z2}\\},\\{\\mathit{z1},\\mathit{z3}\\},\\{\\mathit{z0},\\mathit{z1},\\mathit{z2},\\mathit{z3}\\},\\{\\mathit{z2}\\},\\{\\mathit{z0},\\mathit{z2},\\mathit{z3}\\},\\{\\mathit{z1},\\mathit{z2},\\mathit{z3}\\},\\{\\mathit{z2},\\mathit{z3}\\},\\{\\mathit{z3}\\}\\}$"
],
"text/plain": [
"{∅,{z0},{z0,z1},{z0,z2},{z0,z3},{z1},{z0,z1,z2},{z0,z1,z3},{z1,z2},{z1,z3},{z0,z1,z2,z3},{z2},{z0,z2,z3},{z1,z2,z3},{z2,z3},{z3}}"
@@ -675,14 +675,14 @@
"<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
"<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
" \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
- "<!-- Generated by graphviz version 2.50.0 (20211204.2007)\n",
+ "<!-- Generated by graphviz version 8.0.3 (20230416.2022)\n",
" -->\n",
"<!-- Title: state Pages: 1 -->\n",
"<svg width=\"654pt\" height=\"566pt\"\n",
" viewBox=\"0.00 0.00 654.00 566.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
"<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 562)\">\n",
"<title>state</title>\n",
- "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-562 650,-562 650,4 -4,4\"/>\n",
+ "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-562 650,-562 650,4 -4,4\"/>\n",
"<!-- \\{z2,z3\\} -->\n",
"<g id=\"node1\" class=\"node\">\n",
"<title>\\{z2,z3\\}</title>\n",
@@ -692,8 +692,8 @@
"<!-- \\{z2,z3\\}->\\{z2,z3\\} -->\n",
"<g id=\"edge1\" class=\"edge\">\n",
"<title>\\{z2,z3\\}->\\{z2,z3\\}</title>\n",
- "<path fill=\"none\" stroke=\"firebrick\" d=\"M223.69,-460.88C233.58,-460.88 241.5,-458.25 241.5,-453 241.5,-449.72 238.41,-447.46 233.67,-446.23\"/>\n",
- "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"234.01,-442.75 223.69,-445.12 233.24,-449.71 234.01,-442.75\"/>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M223.69,-461.16C233.58,-461.16 241.5,-458.44 241.5,-453 241.5,-449.77 238.71,-447.5 234.37,-446.19\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"235.05,-442.62 224.69,-444.84 234.17,-449.57 235.05,-442.62\"/>\n",
"<text text-anchor=\"middle\" x=\"251.5\" y=\"-449.3\" font-family=\"Times,serif\" font-size=\"14.00\">end</text>\n",
"</g>\n",
"<!-- \\{z3\\} -->\n",
@@ -705,15 +705,15 @@
"<!-- \\{z2,z3\\}->\\{z3\\} -->\n",
"<g id=\"edge11\" class=\"edge\">\n",
"<title>\\{z2,z3\\}->\\{z3\\}</title>\n",
- "<path fill=\"none\" stroke=\"#473c8b\" d=\"M174.14,-434.79C169.36,-429.57 164.82,-423.49 162,-417 158.98,-410.05 157.55,-402.05 156.98,-394.52\"/>\n",
- "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"160.47,-394.22 156.67,-384.33 153.47,-394.44 160.47,-394.22\"/>\n",
+ "<path fill=\"none\" stroke=\"#473c8b\" d=\"M174.14,-434.79C169.36,-429.57 164.82,-423.49 162,-417 159.08,-410.29 157.65,-402.6 157.04,-395.3\"/>\n",
+ "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"160.5,-395.21 156.67,-385.33 153.51,-395.45 160.5,-395.21\"/>\n",
"<text text-anchor=\"middle\" x=\"165.5\" y=\"-405.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
"</g>\n",
"<!-- \\{z2,z3\\}->\\{z3\\} -->\n",
"<g id=\"edge27\" class=\"edge\">\n",
"<title>\\{z2,z3\\}->\\{z3\\}</title>\n",
- "<path fill=\"none\" stroke=\"black\" d=\"M186.71,-434.8C181.69,-422.93 174.91,-406.93 169.2,-393.45\"/>\n",
- "<polygon fill=\"black\" stroke=\"black\" points=\"172.4,-392.02 165.27,-384.18 165.95,-394.75 172.4,-392.02\"/>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M186.71,-434.8C181.82,-423.24 175.26,-407.75 169.65,-394.5\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"172.52,-393.31 165.4,-385.47 166.07,-396.04 172.52,-393.31\"/>\n",
"<text text-anchor=\"middle\" x=\"182.5\" y=\"-405.8\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
"</g>\n",
"<!-- \\{z1,z2,z3\\} -->\n",
@@ -725,22 +725,22 @@
"<!-- \\{z1,z2,z3\\}->\\{z2,z3\\} -->\n",
"<g id=\"edge12\" class=\"edge\">\n",
"<title>\\{z1,z2,z3\\}->\\{z2,z3\\}</title>\n",
- "<path fill=\"none\" stroke=\"#473c8b\" d=\"M110.93,-521.63C112.3,-511.19 115.52,-498.18 123,-489 131.29,-478.83 143.27,-471.37 155.04,-466.03\"/>\n",
- "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"156.45,-469.23 164.35,-462.18 153.77,-462.76 156.45,-469.23\"/>\n",
+ "<path fill=\"none\" stroke=\"#473c8b\" d=\"M110.93,-521.63C112.3,-511.19 115.52,-498.18 123,-489 131.12,-479.03 142.8,-471.67 154.34,-466.35\"/>\n",
+ "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"155.47,-469.25 163.35,-462.18 152.78,-462.79 155.47,-469.25\"/>\n",
"<text text-anchor=\"middle\" x=\"126.5\" y=\"-492.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
"</g>\n",
"<!-- \\{z1,z2,z3\\}->\\{z2,z3\\} -->\n",
"<g id=\"edge28\" class=\"edge\">\n",
"<title>\\{z1,z2,z3\\}->\\{z2,z3\\}</title>\n",
- "<path fill=\"none\" stroke=\"black\" d=\"M127,-521.8C139.3,-509.36 156.09,-492.36 169.78,-478.5\"/>\n",
- "<polygon fill=\"black\" stroke=\"black\" points=\"172.49,-480.75 177.03,-471.18 167.51,-475.83 172.49,-480.75\"/>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M127,-521.8C139.1,-509.55 155.56,-492.9 169.13,-479.16\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"171.2,-482.04 175.74,-472.47 166.22,-477.12 171.2,-482.04\"/>\n",
"<text text-anchor=\"middle\" x=\"161.5\" y=\"-492.8\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
"</g>\n",
"<!-- \\{z1,z2,z3\\}->\\{z1,z2,z3\\} -->\n",
"<g id=\"edge2\" class=\"edge\">\n",
"<title>\\{z1,z2,z3\\}->\\{z1,z2,z3\\}</title>\n",
- "<path fill=\"none\" stroke=\"firebrick\" d=\"M148.21,-547.81C158.33,-547.36 166,-544.76 166,-540 166,-537.03 163.01,-534.89 158.29,-533.61\"/>\n",
- "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"158.6,-530.12 148.21,-532.19 157.63,-537.05 158.6,-530.12\"/>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M148.48,-548.07C158.47,-547.58 166,-544.89 166,-540 166,-537.1 163.34,-534.97 159.09,-533.62\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"159.9,-530.04 149.48,-531.93 158.8,-536.96 159.9,-530.04\"/>\n",
"<text text-anchor=\"middle\" x=\"176\" y=\"-536.3\" font-family=\"Times,serif\" font-size=\"14.00\">end</text>\n",
"</g>\n",
"<!-- \\{z0,z2,z3\\} -->\n",
@@ -752,8 +752,8 @@
"<!-- \\{z0,z2,z3\\}->\\{z0,z2,z3\\} -->\n",
"<g id=\"edge3\" class=\"edge\">\n",
"<title>\\{z0,z2,z3\\}->\\{z0,z2,z3\\}</title>\n",
- "<path fill=\"none\" stroke=\"firebrick\" d=\"M347.21,-286.81C357.33,-286.36 365,-283.76 365,-279 365,-276.03 362.01,-273.89 357.29,-272.61\"/>\n",
- "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"357.6,-269.12 347.21,-271.19 356.63,-276.05 357.6,-269.12\"/>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M347.48,-287.07C357.47,-286.58 365,-283.89 365,-279 365,-276.1 362.34,-273.97 358.09,-272.62\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"358.9,-269.04 348.48,-270.93 357.8,-275.96 358.9,-269.04\"/>\n",
"<text text-anchor=\"middle\" x=\"375\" y=\"-275.3\" font-family=\"Times,serif\" font-size=\"14.00\">end</text>\n",
"</g>\n",
"<!-- \\{z0,z1,z3\\} -->\n",
@@ -765,8 +765,8 @@
"<!-- \\{z0,z2,z3\\}->\\{z0,z1,z3\\} -->\n",
"<g id=\"edge13\" class=\"edge\">\n",
"<title>\\{z0,z2,z3\\}->\\{z0,z1,z3\\}</title>\n",
- "<path fill=\"none\" stroke=\"#473c8b\" d=\"M309.9,-260.79C311.31,-239.93 314.78,-203.86 323,-174 326.9,-159.84 333.1,-144.76 338.77,-132.4\"/>\n",
- "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"342.04,-133.68 343.16,-123.15 335.71,-130.69 342.04,-133.68\"/>\n",
+ "<path fill=\"none\" stroke=\"#473c8b\" d=\"M309.9,-260.79C311.31,-239.93 314.78,-203.86 323,-174 326.83,-160.08 332.89,-145.26 338.49,-133.02\"/>\n",
+ "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"341.92,-134.96 343.02,-124.43 335.59,-131.97 341.92,-134.96\"/>\n",
"<text text-anchor=\"middle\" x=\"326.5\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
"</g>\n",
"<!-- \\{z0,z3\\} -->\n",
@@ -778,8 +778,8 @@
"<!-- \\{z0,z2,z3\\}->\\{z0,z3\\} -->\n",
"<g id=\"edge29\" class=\"edge\">\n",
"<title>\\{z0,z2,z3\\}->\\{z0,z3\\}</title>\n",
- "<path fill=\"none\" stroke=\"black\" d=\"M337.94,-260.8C359.94,-247.72 390.39,-229.62 414.29,-215.41\"/>\n",
- "<polygon fill=\"black\" stroke=\"black\" points=\"416.3,-218.29 423.1,-210.18 412.72,-212.28 416.3,-218.29\"/>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M338.28,-260.59C359.97,-247.7 389.74,-230.01 413.37,-215.96\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"414.95,-218.5 421.76,-210.38 411.37,-212.48 414.95,-218.5\"/>\n",
"<text text-anchor=\"middle\" x=\"392.5\" y=\"-231.8\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
"</g>\n",
"<!-- \\{z2\\} -->\n",
@@ -791,22 +791,22 @@
"<!-- \\{z2\\}->\\{z2\\} -->\n",
"<g id=\"edge4\" class=\"edge\">\n",
"<title>\\{z2\\}->\\{z2\\}</title>\n",
- "<path fill=\"none\" stroke=\"firebrick\" d=\"M91.24,-460.87C101.02,-461.04 109,-458.41 109,-453 109,-449.7 106.04,-447.44 101.51,-446.21\"/>\n",
- "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"101.55,-442.7 91.24,-445.13 100.82,-449.66 101.55,-442.7\"/>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M91.24,-461.15C101.02,-461.32 109,-458.61 109,-453 109,-449.67 106.19,-447.36 101.86,-446.07\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"102.57,-442.51 92.24,-444.85 101.78,-449.47 102.57,-442.51\"/>\n",
"<text text-anchor=\"middle\" x=\"119\" y=\"-449.3\" font-family=\"Times,serif\" font-size=\"14.00\">end</text>\n",
"</g>\n",
"<!-- \\{z2\\}->\\{z3\\} -->\n",
"<g id=\"edge14\" class=\"edge\">\n",
"<title>\\{z2\\}->\\{z3\\}</title>\n",
- "<path fill=\"none\" stroke=\"#473c8b\" d=\"M69.95,-434.59C74.22,-424.12 80.85,-411.11 90,-402 98.89,-393.14 110.49,-386.06 121.58,-380.64\"/>\n",
- "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"123.06,-383.81 130.71,-376.48 120.16,-377.44 123.06,-383.81\"/>\n",
+ "<path fill=\"none\" stroke=\"#473c8b\" d=\"M69.95,-434.59C74.22,-424.12 80.85,-411.11 90,-402 98.72,-393.32 110.03,-386.34 120.92,-380.96\"/>\n",
+ "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"122.08,-383.82 129.71,-376.48 119.16,-377.46 122.08,-383.82\"/>\n",
"<text text-anchor=\"middle\" x=\"93.5\" y=\"-405.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
"</g>\n",
"<!-- \\{z2\\}->\\{z3\\} -->\n",
"<g id=\"edge30\" class=\"edge\">\n",
"<title>\\{z2\\}->\\{z3\\}</title>\n",
- "<path fill=\"none\" stroke=\"black\" d=\"M83.02,-434.8C96.91,-422.24 115.92,-405.05 131.33,-391.12\"/>\n",
- "<polygon fill=\"black\" stroke=\"black\" points=\"133.94,-393.48 139.01,-384.18 129.24,-388.29 133.94,-393.48\"/>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M83.02,-434.8C96.69,-422.44 115.33,-405.59 130.6,-391.78\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"132.61,-394.77 137.68,-385.47 127.92,-389.58 132.61,-394.77\"/>\n",
"<text text-anchor=\"middle\" x=\"120.5\" y=\"-405.8\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
"</g>\n",
"<!-- \\{z0,z1,z2,z3\\} -->\n",
@@ -818,22 +818,22 @@
"<!-- \\{z0,z1,z2,z3\\}->\\{z0,z2,z3\\} -->\n",
"<g id=\"edge31\" class=\"edge\">\n",
"<title>\\{z0,z1,z2,z3\\}->\\{z0,z2,z3\\}</title>\n",
- "<path fill=\"none\" stroke=\"black\" d=\"M266.08,-36.32C273.9,-80.38 294.62,-197.01 304.11,-250.49\"/>\n",
- "<polygon fill=\"black\" stroke=\"black\" points=\"300.72,-251.37 305.91,-260.6 307.61,-250.15 300.72,-251.37\"/>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M266.08,-36.32C273.87,-80.19 294.44,-196.03 304,-249.82\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"300.72,-250.37 305.91,-259.6 307.61,-249.15 300.72,-250.37\"/>\n",
"<text text-anchor=\"middle\" x=\"291.5\" y=\"-144.8\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
"</g>\n",
"<!-- \\{z0,z1,z2,z3\\}->\\{z0,z1,z2,z3\\} -->\n",
"<g id=\"edge5\" class=\"edge\">\n",
"<title>\\{z0,z1,z2,z3\\}->\\{z0,z1,z2,z3\\}</title>\n",
- "<path fill=\"none\" stroke=\"firebrick\" d=\"M309.02,-21.84C319.41,-21.5 327,-20.21 327,-18 327,-16.62 324.03,-15.6 319.27,-14.94\"/>\n",
- "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"319.26,-11.43 309.02,-14.16 318.73,-18.41 319.26,-11.43\"/>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M309.31,-21.97C319.55,-21.6 327,-20.27 327,-18 327,-16.65 324.37,-15.64 320.09,-14.96\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"320.57,-11.4 310.31,-14.03 319.98,-18.37 320.57,-11.4\"/>\n",
"<text text-anchor=\"middle\" x=\"337\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\">end</text>\n",
"</g>\n",
"<!-- \\{z0,z1,z2,z3\\}->\\{z0,z1,z2,z3\\} -->\n",
"<g id=\"edge15\" class=\"edge\">\n",
"<title>\\{z0,z1,z2,z3\\}->\\{z0,z1,z2,z3\\}</title>\n",
- "<path fill=\"none\" stroke=\"#473c8b\" d=\"M309.37,-25.78C329.56,-26.42 347,-23.82 347,-18 347,-13.18 335.04,-10.57 319.46,-10.18\"/>\n",
- "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"319.36,-6.68 309.37,-10.22 319.39,-13.68 319.36,-6.68\"/>\n",
+ "<path fill=\"none\" stroke=\"#473c8b\" d=\"M309.37,-26.06C329.56,-26.72 347,-24.03 347,-18 347,-13.1 335.49,-10.41 320.34,-9.92\"/>\n",
+ "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"320.37,-6.42 310.37,-9.94 320.38,-13.42 320.37,-6.42\"/>\n",
"<text text-anchor=\"middle\" x=\"350.5\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
"</g>\n",
"<!-- \\{z1,z2\\} -->\n",
@@ -845,22 +845,22 @@
"<!-- \\{z1,z2\\}->\\{z2,z3\\} -->\n",
"<g id=\"edge17\" class=\"edge\">\n",
"<title>\\{z1,z2\\}->\\{z2,z3\\}</title>\n",
- "<path fill=\"none\" stroke=\"#473c8b\" d=\"M211.3,-521.81C206.06,-516.67 201.12,-510.63 198,-504 194.78,-497.14 193.28,-489.17 192.71,-481.64\"/>\n",
- "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"196.21,-481.34 192.44,-471.44 189.21,-481.52 196.21,-481.34\"/>\n",
+ "<path fill=\"none\" stroke=\"#473c8b\" d=\"M211.3,-521.81C206.06,-516.67 201.12,-510.63 198,-504 194.89,-497.38 193.39,-489.72 192.77,-482.42\"/>\n",
+ "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"196.24,-482.32 192.44,-472.44 189.25,-482.54 196.24,-482.32\"/>\n",
"<text text-anchor=\"middle\" x=\"201.5\" y=\"-492.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
"</g>\n",
"<!-- \\{z1,z2\\}->\\{z2,z3\\} -->\n",
"<g id=\"edge33\" class=\"edge\">\n",
"<title>\\{z1,z2\\}->\\{z2,z3\\}</title>\n",
- "<path fill=\"none\" stroke=\"black\" d=\"M225.91,-521.8C220.32,-509.93 212.79,-493.93 206.45,-480.45\"/>\n",
- "<polygon fill=\"black\" stroke=\"black\" points=\"209.51,-478.73 202.08,-471.18 203.17,-481.71 209.51,-478.73\"/>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M225.91,-521.8C220.41,-510.12 213.03,-494.45 206.76,-481.11\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"209.64,-480.03 202.22,-472.47 203.31,-483.01 209.64,-480.03\"/>\n",
"<text text-anchor=\"middle\" x=\"220.5\" y=\"-492.8\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
"</g>\n",
"<!-- \\{z1,z2\\}->\\{z1,z2\\} -->\n",
"<g id=\"edge6\" class=\"edge\">\n",
"<title>\\{z1,z2\\}->\\{z1,z2\\}</title>\n",
- "<path fill=\"none\" stroke=\"firebrick\" d=\"M263.69,-547.88C273.58,-547.88 281.5,-545.25 281.5,-540 281.5,-536.72 278.41,-534.46 273.67,-533.23\"/>\n",
- "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"274.01,-529.75 263.69,-532.12 273.24,-536.71 274.01,-529.75\"/>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M263.69,-548.16C273.58,-548.16 281.5,-545.44 281.5,-540 281.5,-536.77 278.71,-534.5 274.37,-533.19\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"275.05,-529.62 264.69,-531.84 274.17,-536.57 275.05,-529.62\"/>\n",
"<text text-anchor=\"middle\" x=\"291.5\" y=\"-536.3\" font-family=\"Times,serif\" font-size=\"14.00\">end</text>\n",
"</g>\n",
"<!-- \\{z0,z1,z2\\} -->\n",
@@ -872,22 +872,22 @@
"<!-- \\{z0,z1,z2\\}->\\{z0,z2,z3\\} -->\n",
"<g id=\"edge35\" class=\"edge\">\n",
"<title>\\{z0,z1,z2\\}->\\{z0,z2,z3\\}</title>\n",
- "<path fill=\"none\" stroke=\"black\" d=\"M309,-347.8C309,-336.16 309,-320.55 309,-307.24\"/>\n",
- "<polygon fill=\"black\" stroke=\"black\" points=\"312.5,-307.18 309,-297.18 305.5,-307.18 312.5,-307.18\"/>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M309,-347.8C309,-336.47 309,-321.36 309,-308.29\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"312.5,-308.47 309,-298.47 305.5,-308.47 312.5,-308.47\"/>\n",
"<text text-anchor=\"middle\" x=\"312.5\" y=\"-318.8\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
"</g>\n",
"<!-- \\{z0,z1,z2\\}->\\{z0,z1,z2,z3\\} -->\n",
"<g id=\"edge19\" class=\"edge\">\n",
"<title>\\{z0,z1,z2\\}->\\{z0,z1,z2,z3\\}</title>\n",
- "<path fill=\"none\" stroke=\"#473c8b\" d=\"M275.32,-347.88C251.95,-333.36 225,-310.08 225,-280 225,-280 225,-280 225,-104 225,-82.92 234.86,-61.26 244.54,-45.08\"/>\n",
- "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"247.74,-46.56 250.13,-36.23 241.83,-42.81 247.74,-46.56\"/>\n",
+ "<path fill=\"none\" stroke=\"#473c8b\" d=\"M274.83,-347.58C251.58,-333.04 225,-309.88 225,-280 225,-280 225,-280 225,-104 225,-83.12 234.68,-61.67 244.26,-45.54\"/>\n",
+ "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"247.76,-47.56 250.13,-37.23 241.84,-43.82 247.76,-47.56\"/>\n",
"<text text-anchor=\"middle\" x=\"228.5\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
"</g>\n",
"<!-- \\{z0,z1,z2\\}->\\{z0,z1,z2\\} -->\n",
"<g id=\"edge7\" class=\"edge\">\n",
"<title>\\{z0,z1,z2\\}->\\{z0,z1,z2\\}</title>\n",
- "<path fill=\"none\" stroke=\"firebrick\" d=\"M347.21,-373.81C357.33,-373.36 365,-370.76 365,-366 365,-363.03 362.01,-360.89 357.29,-359.61\"/>\n",
- "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"357.6,-356.12 347.21,-358.19 356.63,-363.05 357.6,-356.12\"/>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M347.48,-374.07C357.47,-373.58 365,-370.89 365,-366 365,-363.1 362.34,-360.97 358.09,-359.62\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"358.9,-356.04 348.48,-357.93 357.8,-362.96 358.9,-356.04\"/>\n",
"<text text-anchor=\"middle\" x=\"375\" y=\"-362.3\" font-family=\"Times,serif\" font-size=\"14.00\">end</text>\n",
"</g>\n",
"<!-- \\{z0,z2\\} -->\n",
@@ -899,22 +899,22 @@
"<!-- \\{z0,z2\\}->\\{z0,z2\\} -->\n",
"<g id=\"edge8\" class=\"edge\">\n",
"<title>\\{z0,z2\\}->\\{z0,z2\\}</title>\n",
- "<path fill=\"none\" stroke=\"firebrick\" d=\"M462.69,-286.88C472.58,-286.88 480.5,-284.25 480.5,-279 480.5,-275.72 477.41,-273.46 472.67,-272.23\"/>\n",
- "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"473.01,-268.75 462.69,-271.12 472.24,-275.71 473.01,-268.75\"/>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M462.69,-287.16C472.58,-287.16 480.5,-284.44 480.5,-279 480.5,-275.77 477.71,-273.5 473.37,-272.19\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"474.05,-268.62 463.69,-270.84 473.17,-275.57 474.05,-268.62\"/>\n",
"<text text-anchor=\"middle\" x=\"490.5\" y=\"-275.3\" font-family=\"Times,serif\" font-size=\"14.00\">end</text>\n",
"</g>\n",
"<!-- \\{z0,z2\\}->\\{z0,z1,z3\\} -->\n",
"<g id=\"edge22\" class=\"edge\">\n",
"<title>\\{z0,z2\\}->\\{z0,z1,z3\\}</title>\n",
- "<path fill=\"none\" stroke=\"#473c8b\" d=\"M424.94,-260.88C410.75,-230.74 381.22,-168.04 364.41,-132.35\"/>\n",
- "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"367.46,-130.61 360.03,-123.05 361.12,-133.59 367.46,-130.61\"/>\n",
+ "<path fill=\"none\" stroke=\"#473c8b\" d=\"M424.79,-260.56C410.66,-230.56 381.65,-168.96 364.83,-133.25\"/>\n",
+ "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"367.66,-132.04 360.23,-124.48 361.33,-135.02 367.66,-132.04\"/>\n",
"<text text-anchor=\"middle\" x=\"403.5\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
"</g>\n",
"<!-- \\{z0,z2\\}->\\{z0,z3\\} -->\n",
"<g id=\"edge38\" class=\"edge\">\n",
"<title>\\{z0,z2\\}->\\{z0,z3\\}</title>\n",
- "<path fill=\"none\" stroke=\"black\" d=\"M436.84,-260.8C439.45,-249.16 442.94,-233.55 445.91,-220.24\"/>\n",
- "<polygon fill=\"black\" stroke=\"black\" points=\"449.39,-220.7 448.16,-210.18 442.56,-219.17 449.39,-220.7\"/>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M436.84,-260.8C439.4,-249.35 442.82,-234.06 445.76,-220.89\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"449.33,-221.99 448.1,-211.47 442.5,-220.46 449.33,-221.99\"/>\n",
"<text text-anchor=\"middle\" x=\"446.5\" y=\"-231.8\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
"</g>\n",
"<!-- \\{z0\\} -->\n",
@@ -926,15 +926,15 @@
"<!-- \\{z0\\}->\\{z0\\} -->\n",
"<g id=\"edge9\" class=\"edge\">\n",
"<title>\\{z0\\}->\\{z0\\}</title>\n",
- "<path fill=\"none\" stroke=\"sienna\" d=\"M457.24,-543.93C467.02,-544.02 475,-542.71 475,-540 475,-538.35 472.04,-537.22 467.51,-536.61\"/>\n",
- "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"467.41,-533.1 457.24,-536.07 467.04,-540.09 467.41,-533.1\"/>\n",
+ "<path fill=\"none\" stroke=\"sienna\" d=\"M457.24,-544.07C467.02,-544.16 475,-542.8 475,-540 475,-538.38 472.33,-537.24 468.19,-536.59\"/>\n",
+ "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"468.43,-533.03 458.24,-535.93 468.01,-540.02 468.43,-533.03\"/>\n",
"<text text-anchor=\"middle\" x=\"487\" y=\"-536.3\" font-family=\"Times,serif\" font-size=\"14.00\">start</text>\n",
"</g>\n",
"<!-- \\{z0\\}->\\{z0\\} -->\n",
"<g id=\"edge40\" class=\"edge\">\n",
"<title>\\{z0\\}->\\{z0\\}</title>\n",
- "<path fill=\"none\" stroke=\"black\" d=\"M457.1,-546.99C477.58,-549.34 499,-547.01 499,-540 499,-534.14 484.03,-531.55 467.16,-532.23\"/>\n",
- "<polygon fill=\"black\" stroke=\"black\" points=\"466.8,-528.75 457.1,-533.01 467.34,-535.73 466.8,-528.75\"/>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M457.46,-547.28C477.83,-549.65 499,-547.22 499,-540 499,-534.08 484.76,-531.38 468.39,-531.91\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"468.17,-528.49 458.46,-532.72 468.69,-535.47 468.17,-528.49\"/>\n",
"<text text-anchor=\"middle\" x=\"502.5\" y=\"-536.3\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
"</g>\n",
"<!-- \\{z0,z1\\} -->\n",
@@ -946,36 +946,36 @@
"<!-- \\{z0\\}->\\{z0,z1\\} -->\n",
"<g id=\"edge24\" class=\"edge\">\n",
"<title>\\{z0\\}->\\{z0,z1\\}</title>\n",
- "<path fill=\"none\" stroke=\"#473c8b\" d=\"M430,-521.8C430,-510.16 430,-494.55 430,-481.24\"/>\n",
- "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"433.5,-481.18 430,-471.18 426.5,-481.18 433.5,-481.18\"/>\n",
+ "<path fill=\"none\" stroke=\"#473c8b\" d=\"M430,-521.8C430,-510.47 430,-495.36 430,-482.29\"/>\n",
+ "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"433.5,-482.47 430,-472.47 426.5,-482.47 433.5,-482.47\"/>\n",
"<text text-anchor=\"middle\" x=\"433.5\" y=\"-492.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
"</g>\n",
"<!-- \\{z3\\}->\\{z3\\} -->\n",
"<g id=\"edge10\" class=\"edge\">\n",
"<title>\\{z3\\}->\\{z3\\}</title>\n",
- "<path fill=\"none\" stroke=\"#473c8b\" d=\"M185.24,-369.93C195.02,-370.02 203,-368.71 203,-366 203,-364.35 200.04,-363.22 195.51,-362.61\"/>\n",
- "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"195.41,-359.1 185.24,-362.07 195.04,-366.09 195.41,-359.1\"/>\n",
+ "<path fill=\"none\" stroke=\"#473c8b\" d=\"M185.24,-370.07C195.02,-370.16 203,-368.8 203,-366 203,-364.38 200.33,-363.24 196.19,-362.59\"/>\n",
+ "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"196.43,-359.03 186.24,-361.93 196.01,-366.02 196.43,-359.03\"/>\n",
"<text text-anchor=\"middle\" x=\"206.5\" y=\"-362.3\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
"</g>\n",
"<!-- \\{z3\\}->\\{z3\\} -->\n",
"<g id=\"edge26\" class=\"edge\">\n",
"<title>\\{z3\\}->\\{z3\\}</title>\n",
- "<path fill=\"none\" stroke=\"black\" d=\"M185.2,-373.18C203.34,-375.2 221,-372.81 221,-366 221,-360.47 209.34,-357.85 195.24,-358.15\"/>\n",
- "<polygon fill=\"black\" stroke=\"black\" points=\"194.94,-354.66 185.2,-358.82 195.41,-361.64 194.94,-354.66\"/>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M185.2,-373.44C203.34,-375.53 221,-373.05 221,-366 221,-360.38 209.79,-357.66 196.05,-357.85\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"195.95,-354.42 186.2,-358.56 196.4,-361.4 195.95,-354.42\"/>\n",
"<text text-anchor=\"middle\" x=\"224.5\" y=\"-362.3\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
"</g>\n",
"<!-- \\{z0,z1,z3\\}->\\{z0,z2,z3\\} -->\n",
"<g id=\"edge34\" class=\"edge\">\n",
"<title>\\{z0,z1,z3\\}->\\{z0,z2,z3\\}</title>\n",
- "<path fill=\"none\" stroke=\"black\" d=\"M350.49,-123.28C347.83,-149.67 341.17,-201.34 327,-243 326,-245.95 324.78,-248.95 323.46,-251.9\"/>\n",
- "<polygon fill=\"black\" stroke=\"black\" points=\"320.26,-250.48 319.02,-261 326.55,-253.55 320.26,-250.48\"/>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M350.49,-123.28C347.83,-149.67 341.17,-201.34 327,-243 326.11,-245.6 325.06,-248.25 323.92,-250.87\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"320.4,-249.11 319.21,-259.64 326.7,-252.15 320.4,-249.11\"/>\n",
"<text text-anchor=\"middle\" x=\"347.5\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
"</g>\n",
"<!-- \\{z0,z1,z3\\}->\\{z0,z1,z2,z3\\} -->\n",
"<g id=\"edge18\" class=\"edge\">\n",
"<title>\\{z0,z1,z3\\}->\\{z0,z1,z2,z3\\}</title>\n",
- "<path fill=\"none\" stroke=\"#473c8b\" d=\"M333.99,-86.8C320.84,-74.24 302.84,-57.05 288.26,-43.12\"/>\n",
- "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"290.63,-40.55 280.98,-36.18 285.8,-45.61 290.63,-40.55\"/>\n",
+ "<path fill=\"none\" stroke=\"#473c8b\" d=\"M333.99,-86.8C321.05,-74.44 303.4,-57.59 288.94,-43.78\"/>\n",
+ "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"291.94,-41.84 282.29,-37.47 287.1,-46.91 291.94,-41.84\"/>\n",
"<text text-anchor=\"middle\" x=\"316.5\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
"</g>\n",
"<!-- \\{z1,z3\\} -->\n",
@@ -987,15 +987,15 @@
"<!-- \\{z1,z3\\}->\\{z2,z3\\} -->\n",
"<g id=\"edge16\" class=\"edge\">\n",
"<title>\\{z1,z3\\}->\\{z2,z3\\}</title>\n",
- "<path fill=\"none\" stroke=\"#473c8b\" d=\"M319.48,-522.81C294.78,-509.27 259.36,-489.84 232.45,-475.08\"/>\n",
- "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"234.12,-472.01 223.67,-470.27 230.76,-478.15 234.12,-472.01\"/>\n",
+ "<path fill=\"none\" stroke=\"#473c8b\" d=\"M319.11,-522.61C294.67,-509.21 259.91,-490.14 233.22,-475.51\"/>\n",
+ "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"235.24,-472.08 224.79,-470.34 231.88,-478.22 235.24,-472.08\"/>\n",
"<text text-anchor=\"middle\" x=\"284.5\" y=\"-492.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
"</g>\n",
"<!-- \\{z1,z3\\}->\\{z2,z3\\} -->\n",
"<g id=\"edge32\" class=\"edge\">\n",
"<title>\\{z1,z3\\}->\\{z2,z3\\}</title>\n",
- "<path fill=\"none\" stroke=\"black\" d=\"M332.86,-521.85C322.11,-511.22 307.21,-497.94 292,-489 273.78,-478.29 251.75,-470.06 233.2,-464.28\"/>\n",
- "<polygon fill=\"black\" stroke=\"black\" points=\"234.15,-460.91 223.57,-461.4 232.15,-467.62 234.15,-460.91\"/>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M332.86,-521.85C322.11,-511.22 307.21,-497.94 292,-489 274.03,-478.44 252.36,-470.29 233.97,-464.52\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"235.15,-460.92 224.57,-461.4 233.14,-467.63 235.15,-460.92\"/>\n",
"<text text-anchor=\"middle\" x=\"316.5\" y=\"-492.8\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
"</g>\n",
"<!-- \\{z1\\} -->\n",
@@ -1007,43 +1007,43 @@
"<!-- \\{z1\\}->\\{z2\\} -->\n",
"<g id=\"edge20\" class=\"edge\">\n",
"<title>\\{z1\\}->\\{z2\\}</title>\n",
- "<path fill=\"none\" stroke=\"#473c8b\" d=\"M27.04,-521.67C27.64,-511.73 29.39,-499.23 34,-489 35.54,-485.59 37.52,-482.26 39.72,-479.09\"/>\n",
- "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"42.53,-481.17 45.94,-471.14 37.02,-476.86 42.53,-481.17\"/>\n",
+ "<path fill=\"none\" stroke=\"#473c8b\" d=\"M27.04,-521.67C27.64,-511.73 29.39,-499.23 34,-489 35.45,-485.79 37.28,-482.65 39.33,-479.65\"/>\n",
+ "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"42.57,-482.19 45.94,-472.14 37.04,-477.89 42.57,-482.19\"/>\n",
"<text text-anchor=\"middle\" x=\"37.5\" y=\"-492.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
"</g>\n",
"<!-- \\{z1\\}->\\{z2\\} -->\n",
"<g id=\"edge36\" class=\"edge\">\n",
"<title>\\{z1\\}->\\{z2\\}</title>\n",
- "<path fill=\"none\" stroke=\"black\" d=\"M34.49,-521.8C39.65,-509.93 46.62,-493.93 52.49,-480.45\"/>\n",
- "<polygon fill=\"black\" stroke=\"black\" points=\"55.74,-481.74 56.52,-471.18 49.32,-478.95 55.74,-481.74\"/>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M34.49,-521.8C39.52,-510.24 46.26,-494.75 52.03,-481.5\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"55.61,-483.03 56.4,-472.47 49.2,-480.24 55.61,-483.03\"/>\n",
"<text text-anchor=\"middle\" x=\"51.5\" y=\"-492.8\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
"</g>\n",
"<!-- \\{z0,z3\\}->\\{z0,z1,z3\\} -->\n",
"<g id=\"edge21\" class=\"edge\">\n",
"<title>\\{z0,z3\\}->\\{z0,z1,z3\\}</title>\n",
- "<path fill=\"none\" stroke=\"#473c8b\" d=\"M440.37,-173.97C432.79,-163.65 422.24,-150.66 411,-141 405.84,-136.57 400.05,-132.37 394.16,-128.53\"/>\n",
- "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"395.87,-125.47 385.53,-123.16 392.17,-131.41 395.87,-125.47\"/>\n",
+ "<path fill=\"none\" stroke=\"#473c8b\" d=\"M440.37,-173.97C432.79,-163.65 422.24,-150.66 411,-141 406.02,-136.72 400.45,-132.66 394.77,-128.93\"/>\n",
+ "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"397.17,-125.67 386.83,-123.34 393.46,-131.61 397.17,-125.67\"/>\n",
"<text text-anchor=\"middle\" x=\"427.5\" y=\"-144.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
"</g>\n",
"<!-- \\{z0,z3\\}->\\{z0,z3\\} -->\n",
"<g id=\"edge37\" class=\"edge\">\n",
"<title>\\{z0,z3\\}->\\{z0,z3\\}</title>\n",
- "<path fill=\"none\" stroke=\"black\" d=\"M481.69,-199.88C491.58,-199.88 499.5,-197.25 499.5,-192 499.5,-188.72 496.41,-186.46 491.67,-185.23\"/>\n",
- "<polygon fill=\"black\" stroke=\"black\" points=\"492.01,-181.75 481.69,-184.12 491.24,-188.71 492.01,-181.75\"/>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M481.69,-200.16C491.58,-200.16 499.5,-197.44 499.5,-192 499.5,-188.77 496.71,-186.5 492.37,-185.19\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"493.05,-181.62 482.69,-183.84 492.17,-188.57 493.05,-181.62\"/>\n",
"<text text-anchor=\"middle\" x=\"503\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
"</g>\n",
"<!-- \\{z0,z1\\}->\\{z0,z1,z2\\} -->\n",
"<g id=\"edge23\" class=\"edge\">\n",
"<title>\\{z0,z1\\}->\\{z0,z1,z2\\}</title>\n",
- "<path fill=\"none\" stroke=\"#473c8b\" d=\"M405.51,-434.8C387.15,-421.9 361.81,-404.1 341.71,-389.98\"/>\n",
- "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"343.64,-387.06 333.45,-384.18 339.62,-392.79 343.64,-387.06\"/>\n",
+ "<path fill=\"none\" stroke=\"#473c8b\" d=\"M405.22,-434.59C387.11,-421.87 362.36,-404.48 342.49,-390.52\"/>\n",
+ "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"344.94,-387.27 334.75,-384.38 340.92,-393 344.94,-387.27\"/>\n",
"<text text-anchor=\"middle\" x=\"379.5\" y=\"-405.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
"</g>\n",
"<!-- \\{z0,z1\\}->\\{z0,z2\\} -->\n",
"<g id=\"edge39\" class=\"edge\">\n",
"<title>\\{z0,z1\\}->\\{z0,z2\\}</title>\n",
- "<path fill=\"none\" stroke=\"black\" d=\"M430.3,-434.88C430.82,-405 431.9,-343.11 432.52,-307.27\"/>\n",
- "<polygon fill=\"black\" stroke=\"black\" points=\"436.03,-307.11 432.7,-297.05 429.03,-306.99 436.03,-307.11\"/>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M430.3,-434.56C430.82,-404.81 431.88,-344.01 432.51,-308.17\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"436.02,-308.54 432.7,-298.48 429.02,-308.42 436.02,-308.54\"/>\n",
"<text text-anchor=\"middle\" x=\"434.5\" y=\"-362.3\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
"</g>\n",
"<!-- \\{\\} -->\n",
@@ -1055,15 +1055,15 @@
"<!-- \\{\\}->\\{\\} -->\n",
"<g id=\"edge25\" class=\"edge\">\n",
"<title>\\{\\}->\\{\\}</title>\n",
- "<path fill=\"none\" stroke=\"#473c8b\" d=\"M596.24,-543.93C606.02,-544.02 614,-542.71 614,-540 614,-538.35 611.04,-537.22 606.51,-536.61\"/>\n",
- "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"606.41,-533.1 596.24,-536.07 606.04,-540.09 606.41,-533.1\"/>\n",
+ "<path fill=\"none\" stroke=\"#473c8b\" d=\"M596.24,-544.07C606.02,-544.16 614,-542.8 614,-540 614,-538.38 611.33,-537.24 607.19,-536.59\"/>\n",
+ "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"607.43,-533.03 597.24,-535.93 607.01,-540.02 607.43,-533.03\"/>\n",
"<text text-anchor=\"middle\" x=\"617.5\" y=\"-536.3\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
"</g>\n",
"<!-- \\{\\}->\\{\\} -->\n",
"<g id=\"edge41\" class=\"edge\">\n",
"<title>\\{\\}->\\{\\}</title>\n",
- "<path fill=\"none\" stroke=\"black\" d=\"M596.2,-547.18C614.34,-549.2 632,-546.81 632,-540 632,-534.47 620.34,-531.85 606.24,-532.15\"/>\n",
- "<polygon fill=\"black\" stroke=\"black\" points=\"605.94,-528.66 596.2,-532.82 606.41,-535.64 605.94,-528.66\"/>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M596.2,-547.44C614.34,-549.53 632,-547.05 632,-540 632,-534.38 620.79,-531.66 607.05,-531.85\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"606.95,-528.42 597.2,-532.56 607.4,-535.4 606.95,-528.42\"/>\n",
"<text text-anchor=\"middle\" x=\"635.5\" y=\"-536.3\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
"</g>\n",
"</g>\n",
diff --git a/notebooks/models/NQueens_Puzzle.ipynb b/notebooks/models/NQueens_Puzzle.ipynb
index 7af4b65f3b57cbcbaf456c5dfc8b49568cfcb5c7..fb1f9e723e7f3b2581e6bfb7b12010a169b847ae 100644
--- a/notebooks/models/NQueens_Puzzle.ipynb
+++ b/notebooks/models/NQueens_Puzzle.ipynb
@@ -112,7 +112,7 @@
{
"data": {
"text/markdown": [
- "$\\renewcommand{\\emptyset}{\\mathord\\varnothing}(\\emptyset\\mapsto 1)$"
+ "$\\def\\emptyset{\\mathord\\varnothing}(\\emptyset\\mapsto 1)$"
],
"text/plain": [
"(∅↦1)"
diff --git a/notebooks/tests/animate.ipynb b/notebooks/tests/animate.ipynb
index 41c53bbc0781266010f227b9c99f40c61de0a74a..18ed9e29e05dea0641d6897849cdbb23c6532cf4 100644
--- a/notebooks/tests/animate.ipynb
+++ b/notebooks/tests/animate.ipynb
@@ -369,15 +369,11 @@
"metadata": {},
"outputs": [
{
- "ename": "ProBError",
- "evalue": "ProB reported Errors\nProB returned error messages:\nError: INITIALISATION FAILS (/Users/dgelessus/Uni/STUPS/ProB/ProB-2-Überprojekt/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:6:15 to 6:44)",
+ "ename": "ExecuteOperationException",
+ "evalue": "Executing operation $initialise_machine with additional predicate produced errors: Could not execute operation INITIALISATION in state 2 with additional predicate",
"output_type": "error",
"traceback": [
- "\u001b[1m\u001b[30mError from ProB: \u001b[0m\u001b[1m\u001b[31mProB reported Errors\u001b[0m",
- "\u001b[1m\u001b[31mError: INITIALISATION FAILS (/Users/dgelessus/Uni/STUPS/ProB/ProB-2-Überprojekt/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:6:15 to 6:44)\u001b[0m",
- "\u001b[1m\u001b[30mINVARIANT value : min_value..max_value\u001b[0m",
- "\u001b[1m\u001b[30mINITIALISATION \u001b[0m\u001b[1m\u001b[30m\u001b[41mvalue :: min_value..max_value\u001b[0m\u001b[1m\u001b[30m\u001b[0m",
- "\u001b[1m\u001b[30mOPERATIONS\u001b[0m"
+ "\u001b[1m\u001b[31mde.prob.animator.command.ExecuteOperationException: Executing operation $initialise_machine with additional predicate produced errors: Could not execute operation INITIALISATION in state 2 with additional predicate\u001b[0m"
]
}
],
@@ -682,15 +678,11 @@
"metadata": {},
"outputs": [
{
- "ename": "ProBError",
- "evalue": "ProB reported Errors\nProB returned error messages:\nError: INITIALISATION FAILS (/Users/dgelessus/Uni/STUPS/ProB/ProB-2-Überprojekt/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:4:15 to 4:26)",
+ "ename": "ExecuteOperationException",
+ "evalue": "Executing operation $initialise_machine with additional predicate produced errors: Could not execute operation INITIALISATION in state root with additional predicate",
"output_type": "error",
"traceback": [
- "\u001b[1m\u001b[30mError from ProB: \u001b[0m\u001b[1m\u001b[31mProB reported Errors\u001b[0m",
- "\u001b[1m\u001b[31mError: INITIALISATION FAILS (/Users/dgelessus/Uni/STUPS/ProB/ProB-2-Überprojekt/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:4:15 to 4:26)\u001b[0m",
- "\u001b[1m\u001b[30mINVARIANT z : MININT..MAXINT\u001b[0m",
- "\u001b[1m\u001b[30mINITIALISATION \u001b[0m\u001b[1m\u001b[30m\u001b[41mz :: {0, 1}\u001b[0m\u001b[1m\u001b[30m\u001b[0m",
- "\u001b[1m\u001b[30mOPERATIONS\u001b[0m"
+ "\u001b[1m\u001b[31mde.prob.animator.command.ExecuteOperationException: Executing operation $initialise_machine with additional predicate produced errors: Could not execute operation INITIALISATION in state root with additional predicate\u001b[0m"
]
}
],
diff --git a/notebooks/tests/assert.ipynb b/notebooks/tests/assert.ipynb
index a6b39cfeaefd4f8f000de42e77f68ec453e1c4c2..662bcc08a4591853b1a40cff2eb15c064f7b5b10 100644
--- a/notebooks/tests/assert.ipynb
+++ b/notebooks/tests/assert.ipynb
@@ -223,10 +223,10 @@
"outputs": [
{
"ename": "CommandExecutionException",
- "evalue": ":assert: Error while evaluating assertion: (ERROR: Type mismatch: Expected INTEGER, but was POW(_A) in '{}')",
+ "evalue": ":assert: Error while evaluating assertion: (ERROR: Type mismatch: Expected INTEGER, but was POW(_A) in 'empty_set')",
"output_type": "error",
"traceback": [
- "\u001b[1m\u001b[31m:assert: Error while evaluating assertion: (ERROR: Type mismatch: Expected INTEGER, but was POW(_A) in '{}')\u001b[0m"
+ "\u001b[1m\u001b[31m:assert: Error while evaluating assertion: (ERROR: Type mismatch: Expected INTEGER, but was POW(_A) in 'empty_set')\u001b[0m"
]
}
],
diff --git a/notebooks/tests/chr_tests.ipynb b/notebooks/tests/chr_tests.ipynb
index 1fa46fbdcc27ef1bb15efce19ba64fc784fd9fa9..3b4b00c4dabf0ed4f6b00e56da3b87ab67bb76d2 100644
--- a/notebooks/tests/chr_tests.ipynb
+++ b/notebooks/tests/chr_tests.ipynb
@@ -111,17 +111,13 @@
},
"outputs": [
{
- "data": {
- "text/markdown": [
- "$\\mathit{time\\_out}$"
- ],
- "text/plain": [
- "time_out"
- ]
- },
- "execution_count": 6,
- "metadata": {},
- "output_type": "execute_result"
+ "ename": "WithSourceCodeException",
+ "evalue": "de.prob.exception.ProBError: time_out\nProB returned error messages:\nInternal error: Unknown error type: time_out",
+ "output_type": "error",
+ "traceback": [
+ "\u001b[1m\u001b[30mError from ProB: \u001b[0m\u001b[1m\u001b[31mtime_out\u001b[0m",
+ "\u001b[1m\u001b[31mInternal error: Unknown error type: time_out\u001b[0m"
+ ]
}
],
"source": [
diff --git a/notebooks/tests/dot.ipynb b/notebooks/tests/dot.ipynb
index 07c381be902ed031dd4046fa76f3256901c8af7d..3ae2467843d226d5be7d27175e8c50b81ab01083 100644
--- a/notebooks/tests/dot.ipynb
+++ b/notebooks/tests/dot.ipynb
@@ -40,7 +40,8 @@
"* `variable_modification_graph` - Variable Read/Write Graph: Show variable modification by operations and reading in guards\n",
"* `definitions` - Definitions Graph: Show dependence graph of DEFINITIONS\n",
"* `predicate_dependency` - Predicate Dependency Graph...: Show dependence graph of conjuncts of a predicate\n",
- "* `last_error` - Last Error Formula Tree: Show last error source as a formula tree\n"
+ "* `last_error` - Last Error Formula Tree: Show last error source as a formula tree\n",
+ "* `id_value_formula_tree` - Value of Identifier as Formula Tree...: Show value of an identifier as a formula tree (mainly useful for symbolic values)\n"
],
"text/plain": [
":dot COMMAND [FORMULA]\n",
@@ -72,7 +73,8 @@
"* `variable_modification_graph` - Variable Read/Write Graph: Show variable modification by operations and reading in guards\n",
"* `definitions` - Definitions Graph: Show dependence graph of DEFINITIONS\n",
"* `predicate_dependency` - Predicate Dependency Graph...: Show dependence graph of conjuncts of a predicate\n",
- "* `last_error` - Last Error Formula Tree: Show last error source as a formula tree\n"
+ "* `last_error` - Last Error Formula Tree: Show last error source as a formula tree\n",
+ "* `id_value_formula_tree` - Value of Identifier as Formula Tree...: Show value of an identifier as a formula tree (mainly useful for symbolic values)\n"
]
},
"execution_count": 1,
@@ -95,14 +97,14 @@
"<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
"<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
" \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
- "<!-- Generated by graphviz version 2.50.0 (20211204.2007)\n",
+ "<!-- Generated by graphviz version 8.0.3 (20230416.2022)\n",
" -->\n",
"<!-- Title: visited_states Pages: 1 -->\n",
"<svg width=\"94pt\" height=\"50pt\"\n",
" viewBox=\"0.00 0.00 94.18 50.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
"<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 46)\">\n",
"<title>visited_states</title>\n",
- "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-46 90.18,-46 90.18,4 -4,4\"/>\n",
+ "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-46 90.18,-46 90.18,4 -4,4\"/>\n",
"<!-- root -->\n",
"<g id=\"node1\" class=\"node\">\n",
"<title>root</title>\n",
@@ -158,14 +160,14 @@
"<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
"<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
" \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
- "<!-- Generated by graphviz version 2.50.0 (20211204.2007)\n",
+ "<!-- Generated by graphviz version 8.0.3 (20230416.2022)\n",
" -->\n",
"<!-- Title: visited_states Pages: 1 -->\n",
"<svg width=\"143pt\" height=\"215pt\"\n",
" viewBox=\"0.00 0.00 143.09 215.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
"<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 211)\">\n",
"<title>visited_states</title>\n",
- "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-211 139.09,-211 139.09,4 -4,4\"/>\n",
+ "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-211 139.09,-211 139.09,4 -4,4\"/>\n",
"<!-- root -->\n",
"<g id=\"node1\" class=\"node\">\n",
"<title>root</title>\n",
@@ -181,8 +183,8 @@
"<!-- root->0 -->\n",
"<g id=\"edge1\" class=\"edge\">\n",
"<title>root->0</title>\n",
- "<path fill=\"none\" stroke=\"black\" stroke-dasharray=\"1,5\" d=\"M43.09,-164.81C43.09,-137.15 43.09,-87.19 43.09,-54.56\"/>\n",
- "<polygon fill=\"black\" stroke=\"black\" points=\"46.59,-54.22 43.09,-44.22 39.59,-54.22 46.59,-54.22\"/>\n",
+ "<path fill=\"none\" stroke=\"black\" stroke-dasharray=\"1,5\" d=\"M43.09,-163.82C43.09,-136.28 43.09,-87.89 43.09,-55.64\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"46.59,-55.96 43.09,-45.96 39.59,-55.96 46.59,-55.96\"/>\n",
"<text text-anchor=\"middle\" x=\"89.09\" y=\"-101.4\" font-family=\"Times,serif\" font-size=\"12.00\">INITIALISATION</text>\n",
"</g>\n",
"</g>\n",
@@ -212,14 +214,14 @@
"<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
"<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
" \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
- "<!-- Generated by graphviz version 2.50.0 (20211204.2007)\n",
+ "<!-- Generated by graphviz version 8.0.3 (20230416.2022)\n",
" -->\n",
"<!-- Title: g Pages: 1 -->\n",
"<svg width=\"62pt\" height=\"46pt\"\n",
" viewBox=\"0.00 0.00 62.00 46.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
"<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 42)\">\n",
"<title>g</title>\n",
- "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-42 58,-42 58,4 -4,4\"/>\n",
+ "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-42 58,-42 58,4 -4,4\"/>\n",
"<!-- Noderoot -->\n",
"<g id=\"node1\" class=\"node\">\n",
"<title>Noderoot</title>\n",
@@ -254,14 +256,14 @@
"<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
"<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
" \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
- "<!-- Generated by graphviz version 2.50.0 (20211204.2007)\n",
+ "<!-- Generated by graphviz version 8.0.3 (20230416.2022)\n",
" -->\n",
"<!-- Title: state Pages: 1 -->\n",
"<svg width=\"325pt\" height=\"218pt\"\n",
" viewBox=\"0.00 0.00 325.00 218.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
"<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 214)\">\n",
"<title>state</title>\n",
- "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-214 321,-214 321,4 -4,4\"/>\n",
+ "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-214 321,-214 321,4 -4,4\"/>\n",
"<!-- 3 -->\n",
"<g id=\"node1\" class=\"node\">\n",
"<title>3</title>\n",
@@ -277,8 +279,8 @@
"<!-- 3->1 -->\n",
"<g id=\"edge1\" class=\"edge\">\n",
"<title>3->1</title>\n",
- "<path fill=\"none\" stroke=\"firebrick\" d=\"M74.65,-185.62C58.14,-180.83 38.35,-171.99 28,-156 23.67,-149.31 22.32,-140.99 22.36,-133.07\"/>\n",
- "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"25.85,-133.29 23.09,-123.06 18.87,-132.77 25.85,-133.29\"/>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M74.65,-185.62C58.14,-180.83 38.35,-171.99 28,-156 23.82,-149.54 22.41,-141.55 22.36,-133.87\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"25.91,-134.27 23.09,-124.06 18.93,-133.8 25.91,-134.27\"/>\n",
"<text text-anchor=\"middle\" x=\"96\" y=\"-144.8\" font-family=\"Times,serif\" font-size=\"14.00\">{(1|->2),(2|->3),(3|->1)}</text>\n",
"</g>\n",
"<!-- 2 -->\n",
@@ -290,15 +292,15 @@
"<!-- 1->2 -->\n",
"<g id=\"edge3\" class=\"edge\">\n",
"<title>1->2</title>\n",
- "<path fill=\"none\" stroke=\"firebrick\" d=\"M23.09,-86.94C21.7,-76.61 21.77,-63.62 28,-54 36.41,-41.01 51.05,-32.74 65.1,-27.52\"/>\n",
- "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"66.25,-30.83 74.65,-24.38 64.06,-24.18 66.25,-30.83\"/>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M23.09,-86.94C21.7,-76.61 21.77,-63.62 28,-54 36.25,-41.26 50.49,-33.06 64.29,-27.83\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"65.27,-30.86 73.65,-24.38 63.06,-24.22 65.27,-30.86\"/>\n",
"<text text-anchor=\"middle\" x=\"96\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\">{(1|->2),(2|->3),(3|->1)}</text>\n",
"</g>\n",
"<!-- 2->3 -->\n",
"<g id=\"edge2\" class=\"edge\">\n",
"<title>2->3</title>\n",
- "<path fill=\"none\" stroke=\"firebrick\" d=\"M129.25,-27.16C142.2,-32.56 156.46,-41.08 164,-54 186.86,-93.15 186.86,-116.85 164,-156 158.23,-165.89 148.51,-173.2 138.47,-178.51\"/>\n",
- "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"136.81,-175.42 129.25,-182.84 139.79,-181.76 136.81,-175.42\"/>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M129.25,-27.16C142.2,-32.56 156.46,-41.08 164,-54 186.86,-93.15 186.86,-116.85 164,-156 158.34,-165.69 148.91,-172.9 139.08,-178.19\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"137.79,-175.4 130.25,-182.84 140.79,-181.72 137.79,-175.4\"/>\n",
"<text text-anchor=\"middle\" x=\"249\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\">{(1|->2),(2|->3),(3|->1)}</text>\n",
"</g>\n",
"</g>\n",
@@ -328,14 +330,14 @@
"<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
"<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
" \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
- "<!-- Generated by graphviz version 2.50.0 (20211204.2007)\n",
+ "<!-- Generated by graphviz version 8.0.3 (20230416.2022)\n",
" -->\n",
"<!-- Title: state Pages: 1 -->\n",
"<svg width=\"220pt\" height=\"392pt\"\n",
" viewBox=\"0.00 0.00 220.11 392.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
"<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 388)\">\n",
"<title>state</title>\n",
- "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-388 216.11,-388 216.11,4 -4,4\"/>\n",
+ "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-388 216.11,-388 216.11,4 -4,4\"/>\n",
"<!-- 4 -->\n",
"<g id=\"node1\" class=\"node\">\n",
"<title>4</title>\n",
@@ -351,15 +353,15 @@
"<!-- 4->2 -->\n",
"<g id=\"edge1\" class=\"edge\">\n",
"<title>4->2</title>\n",
- "<path fill=\"none\" stroke=\"firebrick\" d=\"M79.4,-260.77C66.39,-248.14 50.29,-229.79 42.11,-210 31.98,-185.5 30.49,-155.04 31.07,-133.43\"/>\n",
- "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"34.57,-133.45 31.51,-123.31 27.58,-133.15 34.57,-133.45\"/>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M79.4,-260.77C66.39,-248.14 50.29,-229.79 42.11,-210 32.07,-185.72 30.52,-155.6 31.05,-134.03\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"34.58,-134.45 31.51,-124.31 27.59,-134.15 34.58,-134.45\"/>\n",
"<text text-anchor=\"middle\" x=\"53.11\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\">half</text>\n",
"</g>\n",
"<!-- 4->2 -->\n",
"<g id=\"edge8\" class=\"edge\">\n",
"<title>4->2</title>\n",
- "<path fill=\"none\" stroke=\"sienna\" d=\"M72.04,-264.74C52.42,-253.35 27.71,-234.83 18.11,-210 8.4,-184.88 14.87,-154.15 22.1,-132.63\"/>\n",
- "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"25.41,-133.75 25.52,-123.16 18.83,-131.37 25.41,-133.75\"/>\n",
+ "<path fill=\"none\" stroke=\"sienna\" d=\"M71.64,-264.5C52.08,-253.09 27.64,-234.66 18.11,-210 8.49,-185.11 14.76,-154.71 21.9,-133.22\"/>\n",
+ "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"25.43,-134.75 25.52,-124.16 18.84,-132.38 25.43,-134.75\"/>\n",
"<text text-anchor=\"middle\" x=\"23.61\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\">gt</text>\n",
"</g>\n",
"<!-- 1 -->\n",
@@ -371,8 +373,8 @@
"<!-- 4->1 -->\n",
"<g id=\"edge9\" class=\"edge\">\n",
"<title>4->1</title>\n",
- "<path fill=\"none\" stroke=\"sienna\" d=\"M111.6,-260.84C120.38,-247.66 131.37,-228.63 136.11,-210 150.81,-152.22 129.79,-82.84 115.48,-45.66\"/>\n",
- "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"118.61,-44.06 111.66,-36.06 112.11,-46.64 118.61,-44.06\"/>\n",
+ "<path fill=\"none\" stroke=\"sienna\" d=\"M111.79,-260.56C120.53,-247.39 131.4,-228.5 136.11,-210 150.71,-152.62 130.08,-83.79 115.78,-46.42\"/>\n",
+ "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"118.71,-45.32 111.77,-37.32 112.2,-47.91 118.71,-45.32\"/>\n",
"<text text-anchor=\"middle\" x=\"145.61\" y=\"-144.8\" font-family=\"Times,serif\" font-size=\"14.00\">gt</text>\n",
"</g>\n",
"<!-- 3 -->\n",
@@ -384,22 +386,22 @@
"<!-- 4->3 -->\n",
"<g id=\"edge7\" class=\"edge\">\n",
"<title>4->3</title>\n",
- "<path fill=\"none\" stroke=\"sienna\" d=\"M99.31,-260.8C99.45,-249.16 99.63,-233.55 99.79,-220.24\"/>\n",
- "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"103.29,-220.22 99.91,-210.18 96.29,-220.13 103.29,-220.22\"/>\n",
+ "<path fill=\"none\" stroke=\"sienna\" d=\"M99.31,-260.8C99.44,-249.47 99.62,-234.36 99.78,-221.29\"/>\n",
+ "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"103.28,-221.51 99.9,-211.47 96.29,-221.43 103.28,-221.51\"/>\n",
"<text text-anchor=\"middle\" x=\"104.61\" y=\"-231.8\" font-family=\"Times,serif\" font-size=\"14.00\">gt</text>\n",
"</g>\n",
"<!-- 2->1 -->\n",
"<g id=\"edge2\" class=\"edge\">\n",
"<title>2->1</title>\n",
- "<path fill=\"none\" stroke=\"firebrick\" d=\"M44.02,-86.75C50.57,-76.83 59.32,-64.33 68.11,-54 71.11,-50.47 74.42,-46.89 77.78,-43.45\"/>\n",
- "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"80.48,-45.7 85.11,-36.17 75.55,-40.73 80.48,-45.7\"/>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M44.02,-86.75C50.57,-76.83 59.32,-64.33 68.11,-54 71.03,-50.56 74.24,-47.09 77.51,-43.73\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"79.49,-46.7 84.11,-37.17 74.55,-41.74 79.49,-46.7\"/>\n",
"<text text-anchor=\"middle\" x=\"79.11\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\">half</text>\n",
"</g>\n",
"<!-- 2->1 -->\n",
"<g id=\"edge12\" class=\"edge\">\n",
"<title>2->1</title>\n",
- "<path fill=\"none\" stroke=\"sienna\" d=\"M32.23,-86.86C32.53,-76.5 34.45,-63.5 41.11,-54 47.7,-44.59 57.68,-37.42 67.76,-32.1\"/>\n",
- "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"69.43,-35.19 76.95,-27.73 66.42,-28.86 69.43,-35.19\"/>\n",
+ "<path fill=\"none\" stroke=\"sienna\" d=\"M32.23,-86.86C32.53,-76.5 34.45,-63.5 41.11,-54 47.52,-44.85 57.11,-37.83 66.9,-32.56\"/>\n",
+ "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"68.15,-35.36 75.63,-27.87 65.1,-29.06 68.15,-35.36\"/>\n",
"<text text-anchor=\"middle\" x=\"46.61\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\">gt</text>\n",
"</g>\n",
"<!-- 5 -->\n",
@@ -411,43 +413,43 @@
"<!-- 5->4 -->\n",
"<g id=\"edge3\" class=\"edge\">\n",
"<title>5->4</title>\n",
- "<path fill=\"none\" stroke=\"sienna\" d=\"M136.6,-347.8C129.97,-335.82 121.01,-319.62 113.52,-306.06\"/>\n",
- "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"116.51,-304.23 108.61,-297.18 110.38,-307.62 116.51,-304.23\"/>\n",
+ "<path fill=\"none\" stroke=\"sienna\" d=\"M136.6,-347.8C130.08,-336.01 121.3,-320.14 113.88,-306.72\"/>\n",
+ "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"116.67,-305.52 108.77,-298.47 110.54,-308.91 116.67,-305.52\"/>\n",
"<text text-anchor=\"middle\" x=\"130.61\" y=\"-318.8\" font-family=\"Times,serif\" font-size=\"14.00\">gt</text>\n",
"</g>\n",
"<!-- 5->2 -->\n",
"<g id=\"edge5\" class=\"edge\">\n",
"<title>5->2</title>\n",
- "<path fill=\"none\" stroke=\"sienna\" d=\"M119.03,-349.49C87.1,-329.5 35.56,-291.48 13.11,-243 -5.95,-201.86 -1.96,-184.1 12.11,-141 13.09,-138 14.36,-134.98 15.8,-132.04\"/>\n",
- "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"19,-133.5 20.79,-123.06 12.87,-130.1 19,-133.5\"/>\n",
+ "<path fill=\"none\" stroke=\"sienna\" d=\"M118.74,-349.31C86.8,-329.27 35.5,-291.33 13.11,-243 -5.95,-201.86 -1.96,-184.1 12.11,-141 12.97,-138.35 14.07,-135.68 15.31,-133.07\"/>\n",
+ "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"18.86,-134.87 20.57,-124.42 12.71,-131.52 18.86,-134.87\"/>\n",
"<text text-anchor=\"middle\" x=\"18.61\" y=\"-231.8\" font-family=\"Times,serif\" font-size=\"14.00\">gt</text>\n",
"</g>\n",
"<!-- 5->1 -->\n",
"<g id=\"edge6\" class=\"edge\">\n",
"<title>5->1</title>\n",
- "<path fill=\"none\" stroke=\"sienna\" d=\"M165.65,-347.85C181.46,-332 201.11,-306.89 201.11,-280 201.11,-280 201.11,-280 201.11,-104 201.11,-70.4 167.79,-46.99 140.21,-33.37\"/>\n",
- "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"141.67,-30.19 131.13,-29.12 138.7,-36.53 141.67,-30.19\"/>\n",
+ "<path fill=\"none\" stroke=\"sienna\" d=\"M165.96,-347.54C181.72,-331.67 201.11,-306.72 201.11,-280 201.11,-280 201.11,-280 201.11,-104 201.11,-70.8 168.56,-47.54 141.17,-33.85\"/>\n",
+ "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"142.92,-30.33 132.39,-29.23 139.94,-36.66 142.92,-30.33\"/>\n",
"<text text-anchor=\"middle\" x=\"206.61\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\">gt</text>\n",
"</g>\n",
"<!-- 5->3 -->\n",
"<g id=\"edge4\" class=\"edge\">\n",
"<title>5->3</title>\n",
- "<path fill=\"none\" stroke=\"sienna\" d=\"M146.21,-347.69C145.9,-326.73 143.94,-290.57 135.11,-261 130.75,-246.4 123.26,-231.23 116.33,-218.93\"/>\n",
- "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"119.27,-217.01 111.2,-210.14 113.22,-220.54 119.27,-217.01\"/>\n",
+ "<path fill=\"none\" stroke=\"sienna\" d=\"M146.21,-347.69C145.9,-326.73 143.94,-290.57 135.11,-261 130.86,-246.79 123.66,-232.03 116.88,-219.91\"/>\n",
+ "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"119.42,-218.31 111.37,-211.42 113.37,-221.82 119.42,-218.31\"/>\n",
"<text text-anchor=\"middle\" x=\"147.61\" y=\"-275.3\" font-family=\"Times,serif\" font-size=\"14.00\">gt</text>\n",
"</g>\n",
"<!-- 3->2 -->\n",
"<g id=\"edge10\" class=\"edge\">\n",
"<title>3->2</title>\n",
- "<path fill=\"none\" stroke=\"sienna\" d=\"M86.55,-173.8C76.92,-161.59 63.84,-144.99 53.03,-131.28\"/>\n",
- "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"55.59,-128.86 46.65,-123.18 50.09,-133.2 55.59,-128.86\"/>\n",
+ "<path fill=\"none\" stroke=\"sienna\" d=\"M86.55,-173.8C77.08,-161.78 64.26,-145.52 53.55,-131.94\"/>\n",
+ "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"55.82,-130.15 46.88,-124.47 50.32,-134.49 55.82,-130.15\"/>\n",
"<text text-anchor=\"middle\" x=\"75.61\" y=\"-144.8\" font-family=\"Times,serif\" font-size=\"14.00\">gt</text>\n",
"</g>\n",
"<!-- 3->1 -->\n",
"<g id=\"edge11\" class=\"edge\">\n",
"<title>3->1</title>\n",
- "<path fill=\"none\" stroke=\"sienna\" d=\"M100.51,-173.88C101.2,-144 102.64,-82.11 103.47,-46.27\"/>\n",
- "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"106.98,-46.13 103.71,-36.05 99.98,-45.97 106.98,-46.13\"/>\n",
+ "<path fill=\"none\" stroke=\"sienna\" d=\"M100.51,-173.56C101.21,-143.81 102.62,-83.01 103.45,-47.17\"/>\n",
+ "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"106.97,-47.56 103.7,-37.48 99.97,-47.4 106.97,-47.56\"/>\n",
"<text text-anchor=\"middle\" x=\"107.61\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\">gt</text>\n",
"</g>\n",
"</g>\n",
@@ -497,14 +499,14 @@
"<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
"<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
" \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
- "<!-- Generated by graphviz version 2.50.0 (20211204.2007)\n",
+ "<!-- Generated by graphviz version 8.0.3 (20230416.2022)\n",
" -->\n",
"<!-- Title: state Pages: 1 -->\n",
"<svg width=\"243pt\" height=\"235pt\"\n",
" viewBox=\"0.00 0.00 243.39 234.72\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
"<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 230.72)\">\n",
"<title>state</title>\n",
- "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-230.72 239.39,-230.72 239.39,4 -4,4\"/>\n",
+ "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-230.72 239.39,-230.72 239.39,4 -4,4\"/>\n",
"<!-- 4 -->\n",
"<g id=\"node1\" class=\"node\">\n",
"<title>4</title>\n",
@@ -520,16 +522,16 @@
"<!-- 4->2 -->\n",
"<g id=\"edge1\" class=\"edge\">\n",
"<title>4->2</title>\n",
- "<path fill=\"none\" stroke=\"firebrick\" d=\"M146.1,-36.33C154.53,-50.75 168.71,-70.94 181.47,-87.06\"/>\n",
- "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"178.95,-89.51 187.97,-95.07 184.38,-85.1 178.95,-89.51\"/>\n",
- "<text text-anchor=\"middle\" x=\"152.78\" y=\"-65.49\" font-family=\"Times,serif\" font-size=\"14.00\">half</text>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M146.1,-36.33C154.46,-50.61 168.45,-70.57 181.11,-86.62\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"178.95,-88.51 187.97,-94.07 184.39,-84.1 178.95,-88.51\"/>\n",
+ "<text text-anchor=\"middle\" x=\"152.61\" y=\"-65.27\" font-family=\"Times,serif\" font-size=\"14.00\">half</text>\n",
"</g>\n",
"<!-- 4->2 -->\n",
"<g id=\"edge8\" class=\"edge\">\n",
"<title>4->2</title>\n",
- "<path fill=\"none\" stroke=\"sienna\" d=\"M159.48,-36.25C171.39,-50.48 185.9,-70.37 196.11,-86.42\"/>\n",
- "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"193.37,-88.64 201.58,-95.35 199.34,-84.99 193.37,-88.64\"/>\n",
- "<text text-anchor=\"middle\" x=\"172.3\" y=\"-65.14\" font-family=\"Times,serif\" font-size=\"14.00\">gt</text>\n",
+ "<path fill=\"none\" stroke=\"sienna\" d=\"M159.48,-36.25C171.21,-50.26 185.46,-69.76 195.64,-85.67\"/>\n",
+ "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"193.18,-87.35 201.39,-94.04 199.14,-83.68 193.18,-87.35\"/>\n",
+ "<text text-anchor=\"middle\" x=\"172.06\" y=\"-64.76\" font-family=\"Times,serif\" font-size=\"14.00\">gt</text>\n",
"</g>\n",
"<!-- 1 -->\n",
"<g id=\"node3\" class=\"node\">\n",
@@ -540,9 +542,9 @@
"<!-- 4->1 -->\n",
"<g id=\"edge9\" class=\"edge\">\n",
"<title>4->1</title>\n",
- "<path fill=\"none\" stroke=\"sienna\" d=\"M126.02,-36C106.38,-63.03 69.16,-114.27 46.36,-145.65\"/>\n",
- "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"43.39,-143.78 40.34,-153.93 49.05,-147.9 43.39,-143.78\"/>\n",
- "<text text-anchor=\"middle\" x=\"80.69\" y=\"-94.62\" font-family=\"Times,serif\" font-size=\"14.00\">gt</text>\n",
+ "<path fill=\"none\" stroke=\"sienna\" d=\"M125.8,-36.31C106.17,-63.33 69.29,-114.08 46.57,-145.36\"/>\n",
+ "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"43.33,-142.87 40.28,-153.01 48.99,-146.98 43.33,-142.87\"/>\n",
+ "<text text-anchor=\"middle\" x=\"80.69\" y=\"-94.63\" font-family=\"Times,serif\" font-size=\"14.00\">gt</text>\n",
"</g>\n",
"<!-- 3 -->\n",
"<g id=\"node5\" class=\"node\">\n",
@@ -553,23 +555,23 @@
"<!-- 4->3 -->\n",
"<g id=\"edge7\" class=\"edge\">\n",
"<title>4->3</title>\n",
- "<path fill=\"none\" stroke=\"sienna\" d=\"M111.97,-26.82C97.61,-31.48 79.78,-37.28 64.16,-42.35\"/>\n",
- "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"62.7,-39.14 54.28,-45.56 64.87,-45.8 62.7,-39.14\"/>\n",
- "<text text-anchor=\"middle\" x=\"82.56\" y=\"-38.38\" font-family=\"Times,serif\" font-size=\"14.00\">gt</text>\n",
+ "<path fill=\"none\" stroke=\"sienna\" d=\"M111.68,-26.91C97.46,-31.53 79.88,-37.24 64.43,-42.26\"/>\n",
+ "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"63.57,-39.19 55.14,-45.61 65.73,-45.84 63.57,-39.19\"/>\n",
+ "<text text-anchor=\"middle\" x=\"82.55\" y=\"-38.39\" font-family=\"Times,serif\" font-size=\"14.00\">gt</text>\n",
"</g>\n",
"<!-- 2->1 -->\n",
"<g id=\"edge2\" class=\"edge\">\n",
"<title>2->1</title>\n",
- "<path fill=\"none\" stroke=\"firebrick\" d=\"M181.28,-117.04C149.97,-124.88 98.36,-141.39 63.54,-154.51\"/>\n",
- "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"62.27,-151.25 54.19,-158.11 64.78,-157.78 62.27,-151.25\"/>\n",
- "<text text-anchor=\"middle\" x=\"111.41\" y=\"-139.58\" font-family=\"Times,serif\" font-size=\"14.00\">half</text>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M181.28,-117.04C150.33,-124.79 99.54,-141.01 64.74,-154.06\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"63.57,-151.14 55.49,-157.99 66.08,-157.67 63.57,-151.14\"/>\n",
+ "<text text-anchor=\"middle\" x=\"112.01\" y=\"-124.35\" font-family=\"Times,serif\" font-size=\"14.00\">half</text>\n",
"</g>\n",
"<!-- 2->1 -->\n",
"<g id=\"edge12\" class=\"edge\">\n",
"<title>2->1</title>\n",
- "<path fill=\"none\" stroke=\"sienna\" d=\"M181.22,-127.54C150.04,-139.85 98.76,-156.65 63.97,-166.04\"/>\n",
- "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"62.97,-162.68 54.18,-168.59 64.74,-169.46 62.97,-162.68\"/>\n",
- "<text text-anchor=\"middle\" x=\"128.09\" y=\"-150.59\" font-family=\"Times,serif\" font-size=\"14.00\">gt</text>\n",
+ "<path fill=\"none\" stroke=\"sienna\" d=\"M181.22,-127.54C150.26,-139.77 99.49,-156.41 64.72,-165.84\"/>\n",
+ "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"64.26,-162.6 55.48,-168.52 66.04,-169.37 64.26,-162.6\"/>\n",
+ "<text text-anchor=\"middle\" x=\"117.47\" y=\"-150.49\" font-family=\"Times,serif\" font-size=\"14.00\">gt</text>\n",
"</g>\n",
"<!-- 5 -->\n",
"<g id=\"node4\" class=\"node\">\n",
@@ -580,44 +582,44 @@
"<!-- 5->4 -->\n",
"<g id=\"edge3\" class=\"edge\">\n",
"<title>5->4</title>\n",
- "<path fill=\"none\" stroke=\"sienna\" d=\"M139.1,-190.43C139.1,-157.04 139.1,-85.99 139.1,-46.3\"/>\n",
- "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"142.6,-46.23 139.1,-36.23 135.6,-46.23 142.6,-46.23\"/>\n",
- "<text text-anchor=\"middle\" x=\"133.6\" y=\"-122.17\" font-family=\"Times,serif\" font-size=\"14.00\">gt</text>\n",
+ "<path fill=\"none\" stroke=\"sienna\" d=\"M139.1,-190.43C139.1,-157.25 139.1,-86.89 139.1,-47.07\"/>\n",
+ "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"142.6,-47.23 139.1,-37.23 135.6,-47.23 142.6,-47.23\"/>\n",
+ "<text text-anchor=\"middle\" x=\"133.6\" y=\"-122.55\" font-family=\"Times,serif\" font-size=\"14.00\">gt</text>\n",
"</g>\n",
"<!-- 5->2 -->\n",
"<g id=\"edge5\" class=\"edge\">\n",
"<title>5->2</title>\n",
- "<path fill=\"none\" stroke=\"sienna\" d=\"M152.46,-190.33C162.88,-175.99 177.49,-155.88 189.16,-139.82\"/>\n",
- "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"192.26,-141.51 195.3,-131.37 186.59,-137.4 192.26,-141.51\"/>\n",
- "<text text-anchor=\"middle\" x=\"165.31\" y=\"-168.87\" font-family=\"Times,serif\" font-size=\"14.00\">gt</text>\n",
+ "<path fill=\"none\" stroke=\"sienna\" d=\"M152.46,-190.33C162.72,-176.22 177.04,-156.51 188.62,-140.57\"/>\n",
+ "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"192.02,-142.84 195.07,-132.69 186.36,-138.72 192.02,-142.84\"/>\n",
+ "<text text-anchor=\"middle\" x=\"165.04\" y=\"-169.25\" font-family=\"Times,serif\" font-size=\"14.00\">gt</text>\n",
"</g>\n",
"<!-- 5->1 -->\n",
"<g id=\"edge6\" class=\"edge\">\n",
"<title>5->1</title>\n",
- "<path fill=\"none\" stroke=\"sienna\" d=\"M111.97,-199.9C97.61,-195.24 79.78,-189.44 64.16,-184.37\"/>\n",
- "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"64.87,-180.92 54.28,-181.16 62.7,-187.58 64.87,-180.92\"/>\n",
- "<text text-anchor=\"middle\" x=\"82.56\" y=\"-195.94\" font-family=\"Times,serif\" font-size=\"14.00\">gt</text>\n",
+ "<path fill=\"none\" stroke=\"sienna\" d=\"M111.68,-199.81C97.46,-195.19 79.88,-189.48 64.43,-184.46\"/>\n",
+ "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"65.73,-180.88 55.14,-181.11 63.57,-187.53 65.73,-180.88\"/>\n",
+ "<text text-anchor=\"middle\" x=\"82.55\" y=\"-195.93\" font-family=\"Times,serif\" font-size=\"14.00\">gt</text>\n",
"</g>\n",
"<!-- 5->3 -->\n",
"<g id=\"edge4\" class=\"edge\">\n",
"<title>5->3</title>\n",
- "<path fill=\"none\" stroke=\"sienna\" d=\"M126.02,-190.72C106.38,-163.69 69.16,-112.45 46.36,-81.07\"/>\n",
- "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"49.05,-78.82 40.34,-72.79 43.39,-82.94 49.05,-78.82\"/>\n",
- "<text text-anchor=\"middle\" x=\"80.69\" y=\"-139.7\" font-family=\"Times,serif\" font-size=\"14.00\">gt</text>\n",
+ "<path fill=\"none\" stroke=\"sienna\" d=\"M125.8,-190.41C106.17,-163.39 69.29,-112.64 46.57,-81.36\"/>\n",
+ "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"48.99,-79.74 40.28,-73.71 43.33,-83.85 48.99,-79.74\"/>\n",
+ "<text text-anchor=\"middle\" x=\"80.69\" y=\"-139.69\" font-family=\"Times,serif\" font-size=\"14.00\">gt</text>\n",
"</g>\n",
"<!-- 3->2 -->\n",
"<g id=\"edge10\" class=\"edge\">\n",
"<title>3->2</title>\n",
- "<path fill=\"none\" stroke=\"sienna\" d=\"M54.16,-63.25C85.37,-73.39 136.76,-90.09 171.56,-101.39\"/>\n",
- "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"170.75,-104.81 181.34,-104.57 172.91,-98.15 170.75,-104.81\"/>\n",
- "<text text-anchor=\"middle\" x=\"107.36\" y=\"-86.12\" font-family=\"Times,serif\" font-size=\"14.00\">gt</text>\n",
+ "<path fill=\"none\" stroke=\"sienna\" d=\"M54.16,-63.25C85.14,-73.32 136.02,-89.85 170.81,-101.15\"/>\n",
+ "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"169.45,-104.72 180.04,-104.48 171.62,-98.06 169.45,-104.72\"/>\n",
+ "<text text-anchor=\"middle\" x=\"106.98\" y=\"-86\" font-family=\"Times,serif\" font-size=\"14.00\">gt</text>\n",
"</g>\n",
"<!-- 3->1 -->\n",
"<g id=\"edge11\" class=\"edge\">\n",
"<title>3->1</title>\n",
- "<path fill=\"none\" stroke=\"sienna\" d=\"M27,-72.58C27,-91.56 27,-121.61 27,-143.76\"/>\n",
- "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"23.5,-143.92 27,-153.92 30.5,-143.92 23.5,-143.92\"/>\n",
- "<text text-anchor=\"middle\" x=\"21.5\" y=\"-111.97\" font-family=\"Times,serif\" font-size=\"14.00\">gt</text>\n",
+ "<path fill=\"none\" stroke=\"sienna\" d=\"M27,-72.84C27,-91.7 27,-121.28 27,-143.29\"/>\n",
+ "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"23.5,-143.01 27,-153.01 30.5,-143.01 23.5,-143.01\"/>\n",
+ "<text text-anchor=\"middle\" x=\"21.5\" y=\"-111.86\" font-family=\"Times,serif\" font-size=\"14.00\">gt</text>\n",
"</g>\n",
"</g>\n",
"</svg>\n"
@@ -666,14 +668,14 @@
"<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
"<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
" \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
- "<!-- Generated by graphviz version 2.50.0 (20211204.2007)\n",
+ "<!-- Generated by graphviz version 8.0.3 (20230416.2022)\n",
" -->\n",
"<!-- Title: g Pages: 1 -->\n",
"<svg width=\"242pt\" height=\"110pt\"\n",
" viewBox=\"0.00 0.00 242.00 110.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
"<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 106)\">\n",
"<title>g</title>\n",
- "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-106 238,-106 238,4 -4,4\"/>\n",
+ "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-106 238,-106 238,4 -4,4\"/>\n",
"<!-- Noderoot -->\n",
"<g id=\"node1\" class=\"node\">\n",
"<title>Noderoot</title>\n",
@@ -690,22 +692,22 @@
"<!-- Node1->Noderoot -->\n",
"<g id=\"edge1\" class=\"edge\">\n",
"<title>Node1->Noderoot</title>\n",
- "<path fill=\"none\" stroke=\"black\" d=\"M89.6,-74.5C81.43,-71.72 72.3,-68.6 63.62,-65.64\"/>\n",
- "<polygon fill=\"black\" stroke=\"black\" points=\"64.68,-62.31 54.08,-62.39 62.42,-68.93 64.68,-62.31\"/>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M90.07,-74.66C82.07,-71.93 73.1,-68.88 64.53,-65.95\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"65.95,-62.4 55.35,-62.48 63.69,-69.02 65.95,-62.4\"/>\n",
"</g>\n",
"<!-- Node2 -->\n",
"<g id=\"node3\" class=\"node\">\n",
"<title>Node2</title>\n",
"<polygon fill=\"white\" stroke=\"black\" points=\"90,-0.5 90,-46.5 144,-46.5 144,-0.5 90,-0.5\"/>\n",
"<text text-anchor=\"middle\" x=\"117\" y=\"-31.3\" font-family=\"Times,serif\" font-size=\"14.00\">card</text>\n",
- "<polyline fill=\"none\" stroke=\"black\" points=\"90,-23.5 144,-23.5 \"/>\n",
+ "<polyline fill=\"none\" stroke=\"black\" points=\"90,-23.5 144,-23.5\"/>\n",
"<text text-anchor=\"middle\" x=\"117\" y=\"-8.3\" font-family=\"Times,serif\" font-size=\"14.00\">2</text>\n",
"</g>\n",
"<!-- Node2->Noderoot -->\n",
"<g id=\"edge2\" class=\"edge\">\n",
"<title>Node2->Noderoot</title>\n",
- "<path fill=\"none\" stroke=\"black\" d=\"M89.6,-32.5C81.43,-35.28 72.3,-38.4 63.62,-41.36\"/>\n",
- "<polygon fill=\"black\" stroke=\"black\" points=\"62.42,-38.07 54.08,-44.61 64.68,-44.69 62.42,-38.07\"/>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M90.07,-32.34C82.07,-35.07 73.1,-38.12 64.53,-41.05\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"63.69,-37.98 55.35,-44.52 65.95,-44.6 63.69,-37.98\"/>\n",
"</g>\n",
"<!-- Node3 -->\n",
"<g id=\"node4\" class=\"node\">\n",
@@ -716,8 +718,8 @@
"<!-- Node3->Node2 -->\n",
"<g id=\"edge3\" class=\"edge\">\n",
"<title>Node3->Node2</title>\n",
- "<path fill=\"none\" stroke=\"black\" d=\"M179.6,-23.5C171.61,-23.5 162.69,-23.5 154.18,-23.5\"/>\n",
- "<polygon fill=\"black\" stroke=\"black\" points=\"154.08,-20 144.08,-23.5 154.08,-27 154.08,-20\"/>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M180.07,-23.5C172.11,-23.5 163.18,-23.5 154.64,-23.5\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"154.74,-20 144.74,-23.5 154.74,-27 154.74,-20\"/>\n",
"</g>\n",
"</g>\n",
"</svg>\n"
@@ -776,14 +778,14 @@
"<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
"<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
" \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
- "<!-- Generated by graphviz version 2.50.0 (20211204.2007)\n",
+ "<!-- Generated by graphviz version 8.0.3 (20230416.2022)\n",
" -->\n",
"<!-- Title: g Pages: 1 -->\n",
"<svg width=\"242pt\" height=\"110pt\"\n",
" viewBox=\"0.00 0.00 242.00 110.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
"<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 106)\">\n",
"<title>g</title>\n",
- "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-106 238,-106 238,4 -4,4\"/>\n",
+ "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-106 238,-106 238,4 -4,4\"/>\n",
"<!-- Noderoot -->\n",
"<g id=\"node1\" class=\"node\">\n",
"<title>Noderoot</title>\n",
@@ -800,22 +802,22 @@
"<!-- Node1->Noderoot -->\n",
"<g id=\"edge1\" class=\"edge\">\n",
"<title>Node1->Noderoot</title>\n",
- "<path fill=\"none\" stroke=\"black\" d=\"M89.6,-74.5C81.43,-71.72 72.3,-68.6 63.62,-65.64\"/>\n",
- "<polygon fill=\"black\" stroke=\"black\" points=\"64.68,-62.31 54.08,-62.39 62.42,-68.93 64.68,-62.31\"/>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M90.07,-74.66C82.07,-71.93 73.1,-68.88 64.53,-65.95\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"65.95,-62.4 55.35,-62.48 63.69,-69.02 65.95,-62.4\"/>\n",
"</g>\n",
"<!-- Node2 -->\n",
"<g id=\"node3\" class=\"node\">\n",
"<title>Node2</title>\n",
"<polygon fill=\"white\" stroke=\"black\" points=\"90,-0.5 90,-46.5 144,-46.5 144,-0.5 90,-0.5\"/>\n",
"<text text-anchor=\"middle\" x=\"117\" y=\"-31.3\" font-family=\"Times,serif\" font-size=\"14.00\">card</text>\n",
- "<polyline fill=\"none\" stroke=\"black\" points=\"90,-23.5 144,-23.5 \"/>\n",
+ "<polyline fill=\"none\" stroke=\"black\" points=\"90,-23.5 144,-23.5\"/>\n",
"<text text-anchor=\"middle\" x=\"117\" y=\"-8.3\" font-family=\"Times,serif\" font-size=\"14.00\">2</text>\n",
"</g>\n",
"<!-- Node2->Noderoot -->\n",
"<g id=\"edge2\" class=\"edge\">\n",
"<title>Node2->Noderoot</title>\n",
- "<path fill=\"none\" stroke=\"black\" d=\"M89.6,-32.5C81.43,-35.28 72.3,-38.4 63.62,-41.36\"/>\n",
- "<polygon fill=\"black\" stroke=\"black\" points=\"62.42,-38.07 54.08,-44.61 64.68,-44.69 62.42,-38.07\"/>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M90.07,-32.34C82.07,-35.07 73.1,-38.12 64.53,-41.05\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"63.69,-37.98 55.35,-44.52 65.95,-44.6 63.69,-37.98\"/>\n",
"</g>\n",
"<!-- Node3 -->\n",
"<g id=\"node4\" class=\"node\">\n",
@@ -826,8 +828,8 @@
"<!-- Node3->Node2 -->\n",
"<g id=\"edge3\" class=\"edge\">\n",
"<title>Node3->Node2</title>\n",
- "<path fill=\"none\" stroke=\"black\" d=\"M179.6,-23.5C171.61,-23.5 162.69,-23.5 154.18,-23.5\"/>\n",
- "<polygon fill=\"black\" stroke=\"black\" points=\"154.08,-20 144.08,-23.5 154.08,-27 154.08,-20\"/>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M180.07,-23.5C172.11,-23.5 163.18,-23.5 154.64,-23.5\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"154.74,-20 144.74,-23.5 154.74,-27 154.74,-20\"/>\n",
"</g>\n",
"</g>\n",
"</svg>\n"
diff --git a/notebooks/tests/external_functions.ipynb b/notebooks/tests/external_functions.ipynb
index 99c63904ebd8b917caac8851b92611599722ebc0..3997880b68f03823556ed24240aa1fe5f1890099 100644
--- a/notebooks/tests/external_functions.ipynb
+++ b/notebooks/tests/external_functions.ipynb
@@ -31,10 +31,10 @@
{
"data": {
"text/markdown": [
- "$\\text{\"1.11.1-final\"}$"
+ "$\\text{\"1.12.0-final\"}$"
],
"text/plain": [
- "\"1.11.1-final\""
+ "\"1.12.0-final\""
]
},
"execution_count": 2,
@@ -54,10 +54,10 @@
{
"data": {
"text/markdown": [
- "$\\text{\"1.17.35\\\"\\n\"}$"
+ "$\\text{\"1.17.0.6+10\"}$"
],
"text/plain": [
- "\"1.17.35\\\"\\n\""
+ "\"1.17.0.6+10\""
]
},
"execution_count": 3,
@@ -77,10 +77,10 @@
{
"data": {
"text/markdown": [
- "$\\text{\"1125ea39af78125a39093c65a0af783b7636b362\"}$"
+ "$\\text{\"fef4b935b59d76e353ab67230f6206b15f903f4b\"}$"
],
"text/plain": [
- "\"1125ea39af78125a39093c65a0af783b7636b362\""
+ "\"fef4b935b59d76e353ab67230f6206b15f903f4b\""
]
},
"execution_count": 4,
@@ -123,10 +123,10 @@
{
"data": {
"text/markdown": [
- "$164878528$"
+ "$166963568$"
],
"text/plain": [
- "164878528"
+ "166963568"
]
},
"execution_count": 6,
@@ -151,19 +151,17 @@
"metadata": {},
"outputs": [
{
- "ename": "CommandExecutionException",
- "evalue": ":eval: UNKNOWN: \nUnexpected error while parsing machine: \n\n\nAdditional information: Fehler: Hauptklasse de.prob.cliparser.CliBParser konnte nicht gefunden oder geladen werden\nUrsache: java.lang.ClassNotFoundException: de.prob.cliparser.CliBParser\n\n\nJava B parser (probcliparser.jar) is missing from lib directory in: /Users/Shared/Uni/SHK/ProB2/prob_prolog/\n\n",
+ "ename": "WithSourceCodeException",
+ "evalue": "de.prob.exception.ProBError: UNKNOWN\nProB returned error messages:\nError: Unexpected error while parsing machine: \nError: Additional information: Fehler: Hauptklasse de.prob.cliparser.CliBParser konnte nicht gefunden oder geladen werden\nUrsache: java.lang.ClassNotFoundException: de.prob.cliparser.CliBParser\nInternal error: Java B parser (probcliparser.jar) is missing from lib directory in: /Users/dgelessus/.prob/prob2-4.12.0/\nError: Unknown info field, known fields: prob-version prolog-version prob-revision prob-last-changed-date java-version java-command-path current-time",
"output_type": "error",
"traceback": [
- "\u001b[1m\u001b[31m:eval: UNKNOWN: \u001b[0m",
- "\u001b[1m\u001b[31mUnexpected error while parsing machine: \u001b[0m",
- "\u001b[1m\u001b[31m\u001b[0m",
- "\u001b[1m\u001b[31m\u001b[0m",
- "\u001b[1m\u001b[31mAdditional information: Fehler: Hauptklasse de.prob.cliparser.CliBParser konnte nicht gefunden oder geladen werden\u001b[0m",
+ "\u001b[1m\u001b[30mError from ProB: \u001b[0m\u001b[1m\u001b[31mUNKNOWN\u001b[0m",
+ "\u001b[1m\u001b[30m4 errors:\u001b[0m",
+ "\u001b[1m\u001b[31mError: Unexpected error while parsing machine: \u001b[0m",
+ "\u001b[1m\u001b[31mError: Additional information: Fehler: Hauptklasse de.prob.cliparser.CliBParser konnte nicht gefunden oder geladen werden\u001b[0m",
"\u001b[1m\u001b[31mUrsache: java.lang.ClassNotFoundException: de.prob.cliparser.CliBParser\u001b[0m",
- "\u001b[1m\u001b[31m\u001b[0m",
- "\u001b[1m\u001b[31m\u001b[0m",
- "\u001b[1m\u001b[31mJava B parser (probcliparser.jar) is missing from lib directory in: /Users/Shared/Uni/SHK/ProB2/prob_prolog/\u001b[0m"
+ "\u001b[1m\u001b[31mInternal error: Java B parser (probcliparser.jar) is missing from lib directory in: /Users/dgelessus/.prob/prob2-4.12.0/\u001b[0m",
+ "\u001b[1m\u001b[31mError: Unknown info field, known fields: prob-version prolog-version prob-revision prob-last-changed-date java-version java-command-path current-time\u001b[0m"
]
}
],
diff --git a/notebooks/tests/load_cell.ipynb b/notebooks/tests/load_cell.ipynb
index 786594324b89f6327f25c1f3e69a61c8eafa250b..c6c26a6ec458c0b5e38e1c540e0514bf50003060 100644
--- a/notebooks/tests/load_cell.ipynb
+++ b/notebooks/tests/load_cell.ipynb
@@ -252,16 +252,16 @@
"outputs": [
{
"ename": "ProBError",
- "evalue": "Prolog said no.\nProB returned error messages:\nError: Could not infer type of x (/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:2:17 to 2:18)\nError: Identifier 'x' (local from duplicate) already declared at (Line:2 Col:14) (local from duplicate) (/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:2:17 to 2:18)",
+ "evalue": "Prolog said no.\nProB returned error messages:\nError: Could not infer type of x (/Users/dgelessus/Uni/STUPS/ProB/ProB-2-Überprojekt/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:2:17 to 2:18)\nError: Identifier 'x' (local from duplicate) already declared at (Line:2 Col:14) (local from duplicate) (/Users/dgelessus/Uni/STUPS/ProB/ProB-2-Überprojekt/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:2:17 to 2:18)",
"output_type": "error",
"traceback": [
"\u001b[1m\u001b[30mError from ProB: \u001b[0m\u001b[1m\u001b[31mProlog said no.\u001b[0m",
"\u001b[1m\u001b[30m2 errors:\u001b[0m",
- "\u001b[1m\u001b[31mError: Could not infer type of x (/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:2:17 to 2:18)\u001b[0m",
+ "\u001b[1m\u001b[31mError: Could not infer type of x (/Users/dgelessus/Uni/STUPS/ProB/ProB-2-Überprojekt/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:2:17 to 2:18)\u001b[0m",
"\u001b[1m\u001b[30mMACHINE duplicate\u001b[0m",
"\u001b[1m\u001b[30m CONSTANTS x, \u001b[0m\u001b[1m\u001b[30m\u001b[41mx\u001b[0m\u001b[1m\u001b[30m\u001b[0m",
"\u001b[1m\u001b[30m PROPERTIES x : INT\u001b[0m",
- "\u001b[1m\u001b[31mError: Identifier 'x' (local from duplicate) already declared at (Line:2 Col:14) (local from duplicate) (/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:2:17 to 2:18)\u001b[0m",
+ "\u001b[1m\u001b[31mError: Identifier 'x' (local from duplicate) already declared at (Line:2 Col:14) (local from duplicate) (/Users/dgelessus/Uni/STUPS/ProB/ProB-2-Überprojekt/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:2:17 to 2:18)\u001b[0m",
"\u001b[1m\u001b[30mMACHINE duplicate\u001b[0m",
"\u001b[1m\u001b[30m CONSTANTS x, \u001b[0m\u001b[1m\u001b[30m\u001b[41mx\u001b[0m\u001b[1m\u001b[30m\u001b[0m",
"\u001b[1m\u001b[30m PROPERTIES x : INT\u001b[0m"
@@ -283,22 +283,22 @@
"outputs": [
{
"ename": "ProBError",
- "evalue": "Prolog said no.\nProB returned error messages:\nError: Could not infer type of x (/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:2:14 to 2:15)\nError: Type mismatch: Expected INTEGER, but was STRING in '\"string\" ^ \"string\" ^ \"string\"' (/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:3:35 to 5:18)\nError: Type mismatch: Expected INTEGER, but was STRING in '\"string\"' (/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:3:19 to 3:27)",
+ "evalue": "Prolog said no.\nProB returned error messages:\nError: Could not infer type of x (/Users/dgelessus/Uni/STUPS/ProB/ProB-2-Überprojekt/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:2:14 to 2:15)\nError: Type mismatch: Expected INTEGER, but was STRING in '\"string\" ^ \"string\" ^ \"string\"' (/Users/dgelessus/Uni/STUPS/ProB/ProB-2-Überprojekt/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:3:35 to 5:18)\nError: Type mismatch: Expected INTEGER, but was STRING in '\"string\"' (/Users/dgelessus/Uni/STUPS/ProB/ProB-2-Überprojekt/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:3:19 to 3:27)",
"output_type": "error",
"traceback": [
"\u001b[1m\u001b[30mError from ProB: \u001b[0m\u001b[1m\u001b[31mProlog said no.\u001b[0m",
"\u001b[1m\u001b[30m3 errors:\u001b[0m",
- "\u001b[1m\u001b[31mError: Could not infer type of x (/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:2:14 to 2:15)\u001b[0m",
+ "\u001b[1m\u001b[31mError: Could not infer type of x (/Users/dgelessus/Uni/STUPS/ProB/ProB-2-Überprojekt/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:2:14 to 2:15)\u001b[0m",
"\u001b[1m\u001b[30mMACHINE typeerrors\u001b[0m",
"\u001b[1m\u001b[30m CONSTANTS \u001b[0m\u001b[1m\u001b[30m\u001b[41mx\u001b[0m\u001b[1m\u001b[30m\u001b[0m",
"\u001b[1m\u001b[30m PROPERTIES 1 = \"string\" & 1 = (\"string\"\u001b[0m",
- "\u001b[1m\u001b[31mError: Type mismatch: Expected INTEGER, but was STRING in '\"string\" ^ \"string\" ^ \"string\"' (/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:3:35 to 5:18)\u001b[0m",
+ "\u001b[1m\u001b[31mError: Type mismatch: Expected INTEGER, but was STRING in '\"string\" ^ \"string\" ^ \"string\"' (/Users/dgelessus/Uni/STUPS/ProB/ProB-2-Überprojekt/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:3:35 to 5:18)\u001b[0m",
"\u001b[1m\u001b[30m CONSTANTS x\u001b[0m",
"\u001b[1m\u001b[30m PROPERTIES 1 = \"string\" & 1 = (\u001b[0m\u001b[1m\u001b[30m\u001b[41m\"string\"\u001b[0m",
"\u001b[1m\u001b[30m\u001b[41m ^ \"string\"\u001b[0m",
"\u001b[1m\u001b[30m\u001b[41m ^ \"string\"\u001b[0m\u001b[1m\u001b[30m)\u001b[0m",
"\u001b[1m\u001b[30mEND\u001b[0m",
- "\u001b[1m\u001b[31mError: Type mismatch: Expected INTEGER, but was STRING in '\"string\"' (/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:3:19 to 3:27)\u001b[0m",
+ "\u001b[1m\u001b[31mError: Type mismatch: Expected INTEGER, but was STRING in '\"string\"' (/Users/dgelessus/Uni/STUPS/ProB/ProB-2-Überprojekt/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:3:19 to 3:27)\u001b[0m",
"\u001b[1m\u001b[30m CONSTANTS x\u001b[0m",
"\u001b[1m\u001b[30m PROPERTIES 1 = \u001b[0m\u001b[1m\u001b[30m\u001b[41m\"string\"\u001b[0m\u001b[1m\u001b[30m & 1 = (\"string\"\u001b[0m",
"\u001b[1m\u001b[30m ^ \"string\"\u001b[0m"
diff --git a/notebooks/tests/modelcheck.ipynb b/notebooks/tests/modelcheck.ipynb
index 6f0e71ebbdd9fd0dce321d7626e5bcf49ea8c1ae..21958a1bb3c702fe04f0a45d331e72dd3d03fd94 100644
--- a/notebooks/tests/modelcheck.ipynb
+++ b/notebooks/tests/modelcheck.ipynb
@@ -60,7 +60,7 @@
{
"data": {
"text/plain": [
- "0.300 sec, 36 of 36 states processed, 156 transitions"
+ "0.678 sec, 36 of 36 states processed, 156 transitions"
]
},
"metadata": {},
@@ -109,7 +109,7 @@
{
"data": {
"text/plain": [
- "0.268 sec, 57 of 316 states processed, 416 transitions"
+ "0.827 sec, 65 of 360 states processed, 478 transitions"
]
},
"metadata": {},
@@ -166,7 +166,7 @@
{
"data": {
"text/plain": [
- "21.538 sec, 17753 of 17753 states processed, 185145 transitions"
+ "44.633 sec, 17753 of 17753 states processed, 185145 transitions"
]
},
"metadata": {},
diff --git a/notebooks/tests/pref.ipynb b/notebooks/tests/pref.ipynb
index 416a27b4eb60148e196086f334c9fbab4df77890..06d7ad524e798b211728befd158efd6aefaf19d9 100644
--- a/notebooks/tests/pref.ipynb
+++ b/notebooks/tests/pref.ipynb
@@ -71,6 +71,7 @@
"ALLOY_USE_IMPLEMENTABLE_INTEGERS = false\n",
"ASSERT_CHECKING = true\n",
"ATELIERB_KRT_PATH = krt\n",
+ "AUTO_DETECT_THEORY_MAPPING = false\n",
"BBRESULTS = false\n",
"BOOL_AS_PREDICATE = false\n",
"BUGLY = false\n",
@@ -135,11 +136,13 @@
"DOT_PROJECTION_LABEL_LIMIT = 75\n",
"DOT_PROJECTION_NON_DEF_COL = dashed\n",
"DOT_PROJECTION_NON_DET_COL = #806040\n",
+ "DOT_PROJECTION_ONLY_EXPLORED_NODES = false\n",
"DOT_PROP = false\n",
"DOT_ROOT = true\n",
"DOT_ROOT_SHAPE = invtriangle\n",
"DOT_SCOPE_LIMIT_COL = gray\n",
"DOT_SHOW_OP_READ_WRITES = true\n",
+ "DOT_TRANS_IDS = false\n",
"DOT_USE_CONSTANTS = true\n",
"DOT_USE_UNICODE = true\n",
"DOT_VARIABLE_MODIFICATION_HIDE_ONLY_WRITTEN = false\n",
@@ -174,6 +177,7 @@
"MAX_DISPLAY_SET = 100\n",
"MAX_INITIALISATIONS = 4\n",
"MAX_OPERATIONS = 10\n",
+ "MAX_TRACES = 100\n",
"MC_DC_Level = 2\n",
"MEMO = false\n",
"MEMOIZE_FUNCTIONS = false\n",
@@ -194,9 +198,9 @@
"PP_SEQUENCES = false\n",
"PROB2_TRACE_FILE = \n",
"PROB2_TRACE_FILE_UNIQUE = false\n",
- "PROB_LASTCHANGED_INFO = Wed Dec 29 13:14:39 2021 +0100\n",
- "PROB_REVISION_INFO = 1125ea39af78125a39093c65a0af783b7636b362\n",
- "PROB_VERSION_INFO = 1.11.1-final\n",
+ "PROB_LASTCHANGED_INFO = Wed Apr 5 14:57:01 2023 +0200\n",
+ "PROB_REVISION_INFO = fef4b935b59d76e353ab67230f6206b15f903f4b\n",
+ "PROB_VERSION_INFO = 1.12.0-final\n",
"PROOF_INFO = true\n",
"RAISE_ABORT_IMMEDIATELY = false\n",
"RANDOMISED_RESTART_INIT = false\n",
@@ -227,6 +231,7 @@
"SYMBOLIC_MC_TRY_OTHER_SOLVERS = false\n",
"SYMMETRY_MODE = off\n",
"SYNTAX_HIGHLIGHT = true\n",
+ "TABLE_COLUMN_LIMIT = 100\n",
"TIME_OUT = 2500\n",
"TK_CUSTOM_STATE_VIEW_FONT_NAME = \n",
"TK_CUSTOM_STATE_VIEW_FONT_SIZE = 0\n",
@@ -234,6 +239,7 @@
"TK_CUSTOM_STATE_VIEW_STRING_PADDING = 10\n",
"TK_CUSTOM_STATE_VIEW_VISIBLE = true\n",
"TLC_WORKERS = 2\n",
+ "TRACES_TIME_OUT = 2147483646\n",
"TRACE_INFO = false\n",
"TRACE_UPON_ERROR = false\n",
"TRY_ATELIERB_PROVERS = false\n",
@@ -246,7 +252,9 @@
"WARN_IF_DEFINITION_HIDES_VARIABLE = true\n",
"WD_ANALYSIS_FOR_ANIMATION = true\n",
"WD_IGNORE_EXTERNAL = false\n",
- "XML_ENCODING = auto\n"
+ "WD_IGNORE_FINITE_POS = false\n",
+ "XML_ENCODING = auto\n",
+ "Z3_SOLVE_FOR_ANIMATION = true\n"
]
},
"execution_count": 2,
diff --git a/notebooks/tests/solve.ipynb b/notebooks/tests/solve.ipynb
index 1f1f91baacfcf6f28d4cba907111078d22afd073..75afa36ef8404da3ac7e720e86c20709a701e796 100644
--- a/notebooks/tests/solve.ipynb
+++ b/notebooks/tests/solve.ipynb
@@ -16,8 +16,8 @@
"\n",
"The following solvers are currently available:\n",
"\n",
+ "* `cdclt`\n",
"* `cvc4`\n",
- "* `dpllt`\n",
"* `kodkod`\n",
"* `prob`\n",
"* `smt_supported_interpreter`\n",
@@ -31,8 +31,8 @@
"\n",
"The following solvers are currently available:\n",
"\n",
+ "* `cdclt`\n",
"* `cvc4`\n",
- "* `dpllt`\n",
"* `kodkod`\n",
"* `prob`\n",
"* `smt_supported_interpreter`\n",
@@ -125,13 +125,25 @@
"metadata": {},
"outputs": [
{
- "ename": "WithSourceCodeException",
- "evalue": "de.prob.exception.PrologException: Unhandled exception thrown from Prolog: (error(existence_error(procedure,:(z3interface,/(pop_frame,0))),existence_error($@(:(z3interface,pop_frame),4545727948),0,procedure,:(z3interface,/(pop_frame,0)),0)))\n",
- "output_type": "error",
- "traceback": [
- "\u001b[1m\u001b[30mError from ProB: \u001b[0m\u001b[1m\u001b[31mUnhandled exception thrown from Prolog: (error(existence_error(procedure,:(z3interface,/(pop_frame,0))),existence_error($@(:(z3interface,pop_frame),4545727948),0,procedure,:(z3interface,/(pop_frame,0)),0)))",
- "\u001b[0m"
- ]
+ "data": {
+ "text/markdown": [
+ "$\\mathit{TRUE}$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $\\mathit{xx} = 3$\n",
+ "* $\\mathit{yy} = 4$"
+ ],
+ "text/plain": [
+ "TRUE\n",
+ "\n",
+ "Solution:\n",
+ "\txx = 3\n",
+ "\tyy = 4"
+ ]
+ },
+ "execution_count": 4,
+ "metadata": {},
+ "output_type": "execute_result"
}
],
"source": [
@@ -144,13 +156,25 @@
"metadata": {},
"outputs": [
{
- "ename": "WithSourceCodeException",
- "evalue": "de.prob.exception.ProBError: ProB reported Errors\nProB returned error messages:\nInternal error: Call for event start_solving failed. init_smt_supported_interpreter",
- "output_type": "error",
- "traceback": [
- "\u001b[1m\u001b[30mError from ProB: \u001b[0m\u001b[1m\u001b[31mProB reported Errors\u001b[0m",
- "\u001b[1m\u001b[31mInternal error: Call for event start_solving failed. init_smt_supported_interpreter\u001b[0m"
- ]
+ "data": {
+ "text/markdown": [
+ "$\\mathit{TRUE}$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $\\mathit{xx} = 3$\n",
+ "* $\\mathit{yy} = 4$"
+ ],
+ "text/plain": [
+ "TRUE\n",
+ "\n",
+ "Solution:\n",
+ "\txx = 3\n",
+ "\tyy = 4"
+ ]
+ },
+ "execution_count": 5,
+ "metadata": {},
+ "output_type": "execute_result"
}
],
"source": [
@@ -196,11 +220,10 @@
"outputs": [
{
"ename": "WithSourceCodeException",
- "evalue": "de.prob.exception.ProBError: NOT-INITIALISED\nProB returned no error messages.",
+ "evalue": "de.prob.exception.ProBError: NOT-INITIALISED",
"output_type": "error",
"traceback": [
- "\u001b[1m\u001b[30mError from ProB: \u001b[0m\u001b[1m\u001b[31mNOT-INITIALISED\u001b[0m",
- "\u001b[1m\u001b[30mProB returned no error messages.\u001b[0m"
+ "\u001b[1m\u001b[30mError from ProB: \u001b[0m\u001b[1m\u001b[31mNOT-INITIALISED\u001b[0m"
]
}
],
diff --git a/notebooks/tests/time.ipynb b/notebooks/tests/time.ipynb
index be735ee74169e7ba48882c54ec27d836e913429c..d574fda1d312842dcbfc3372c67a483f926c0f76 100644
--- a/notebooks/tests/time.ipynb
+++ b/notebooks/tests/time.ipynb
@@ -51,10 +51,10 @@
{
"data": {
"text/markdown": [
- "Execution time: 1.056192286 seconds"
+ "Execution time: 1.024570750 seconds"
],
"text/plain": [
- "Execution time: 1.056192286 seconds"
+ "Execution time: 1.024570750 seconds"
]
},
"metadata": {},
@@ -90,10 +90,10 @@
{
"data": {
"text/markdown": [
- "Execution time: 0.378675290 seconds"
+ "Execution time: 0.419384167 seconds"
],
"text/plain": [
- "Execution time: 0.378675290 seconds"
+ "Execution time: 0.419384167 seconds"
]
},
"metadata": {},
diff --git a/notebooks/tests/type.ipynb b/notebooks/tests/type.ipynb
index 3684dc13d9a25291fa0d2a9c18a1f92613c29db2..86e8bc657f98e9202a8612806ce4cf5fca2f958a 100644
--- a/notebooks/tests/type.ipynb
+++ b/notebooks/tests/type.ipynb
@@ -245,11 +245,11 @@
"outputs": [
{
"ename": "WithSourceCodeException",
- "evalue": "de.prob.exception.ProBError: Type errors in formula\nProB returned error messages:\nError: Type mismatch: Expected INTEGER, but was POW(_A) in '{}' (:1:4 to 1:6)",
+ "evalue": "de.prob.exception.ProBError: Type errors in formula\nProB returned error messages:\nError: Type mismatch: Expected INTEGER, but was POW(_A) in 'empty_set' (:1:4 to 1:6)",
"output_type": "error",
"traceback": [
"\u001b[1m\u001b[30mError from ProB: \u001b[0m\u001b[1m\u001b[31mType errors in formula\u001b[0m",
- "\u001b[1m\u001b[31mError: Type mismatch: Expected INTEGER, but was POW(_A) in '{}' (:1:4 to 1:6)\u001b[0m",
+ "\u001b[1m\u001b[31mError: Type mismatch: Expected INTEGER, but was POW(_A) in 'empty_set' (:1:4 to 1:6)\u001b[0m",
"\u001b[1m\u001b[30m1 + \u001b[0m\u001b[1m\u001b[30m\u001b[41m{}\u001b[0m\u001b[1m\u001b[30m\u001b[0m"
]
}
diff --git a/notebooks/tests/version.ipynb b/notebooks/tests/version.ipynb
index fc15096cd61dccea3c120db1743d7e0bd76b6742..212f4baa94f0e7f0f33ecbc5dfbca4c0934b2d43 100644
--- a/notebooks/tests/version.ipynb
+++ b/notebooks/tests/version.ipynb
@@ -36,13 +36,13 @@
{
"data": {
"text/plain": [
- "ProB 2 Jupyter kernel: 1.2.1-SNAPSHOT (2aaa99bab781d6eca5a2b3388cca76b412fd52f6)\n",
- "ProB 2: 3.15.0 (6ee6df4eab62d20df40c36cd42108b62962ec41b)\n",
- "ProB B parser: 2.9.32 (7306d13499ba281a6e336c006d9fb23204624daa)\n",
+ "ProB 2 Jupyter kernel: 1.3.1-SNAPSHOT (b960640e155fc1441104e499894acd14e8f0fc07)\n",
+ "ProB 2: 4.12.0 (0356aaca15fde27915b8ab15c35a198fd381c9cd)\n",
+ "ProB B parser: 2.12.3 (99a64151f3bc82f987258619161831a8b9a7df01)\n",
"ProB CLI:\n",
- "\t1.11.1-final (1125ea39af78125a39093c65a0af783b7636b362)\n",
- "\tLast changed: Wed Dec 29 13:14:39 2021 +0100\n",
- "\tProlog: SICStus 4.7.0 (x86_64-darwin-18.7.0): Wed Jul 7 17:07:32 CEST 2021"
+ "\t1.12.0-final (fef4b935b59d76e353ab67230f6206b15f903f4b)\n",
+ "\tLast changed: Wed Apr 5 14:57:01 2023 +0200\n",
+ "\tProlog: SICStus 4.7.1 (x86_64-darwin-18.7.0): Fri Jan 21 19:45:28 CET 2022"
]
},
"execution_count": 2,