Merge pull request #8 from benkeks/zenodo-fixes

Zenodo fixes

Updates the readme for the current version.
Also sightly improves presentation.

README.md

@@ -1,12 +1,12 @@
-# Linear-time–Branching-time Spectroscope
+# Linear-Time–Branching-Time Spectroscope
 
-This is a tool for finding the best ways of equating / preordering / distinguishing finite process models as described in [Bisping & Nestmann, TACAS 2021](https://link.springer.com/chapter/10.1007%2F978-3-030-72016-2_1).
+The “Linear-time–Branching-time Spectroscope” is a web app to find all preorders, equivalences and inequivalences from the (strong) linear-time–branching-time spectrum for small processes as described in [Bisping, Jansen, Nestmann, arXiv 2022](https://doi.org/10.48550/arXiv.2109.15295).
 
 It runs online on https://concurrency-theory.org/ltbt-spectroscope/ .
 
 ![](doc/usage-illustration.gif)
 
-Just input CSS-style processes, give the two processes you want to compare with `@compare "P1,P2"` and click on the gutter next to the compare-statement!
+Just input CCS-style processes, give the two processes you want to compare with `@compare "P1,P2"` and click on the gutter next to the compare-statement!
 
 ## How to build
 
@@ -24,17 +24,18 @@ In order to test that the algorithm determines the expected (in-)equivaences for
 sbt "shared/test"
 ```
 
-To generate distinguishing formulas displayed in Table 2 of the [paper](https://link.springer.com/chapter/10.1007%2F978-3-030-72016-2_1):
+To generate distinguishing formulas displayed in Table 2 of the [TACAS 2021 paper](https://doi.org/10.1007/978-3-030-72016-2_1):
 
 ```
 sbt "shared/run"
 ```
 
+## Theoretical background
+
+The algorithm uses a generalization of the bisimulation game to find all relevant distinguishing Hennessy–Milner logic formulas for two compared finite-state processes. Using these, we can give a precise characterization of how much distinguishing power is needed to tell two processes apart—and thus also determine the best fit of equivalences to equate them.
 
 ## Developed by
 
 The LTBT Spectroscope is developed at [MTV TU Berlin](https://www.mtv.tu-berlin.de) by Benjamin Bisping (benjamin.bisping@tu-berlin.de).
 
-The code is subject to the MIT License to be found in `LICENSE`. The full source can be obtained from <https://concurrency-theory.org/ltbt-spectroscope/code/>.
-
-The frontend is derived from our [HDES Tool](http://hdes.mtv.tu-berlin.de/) for higher-order dynamic-causality event structures.
+The code is subject to the MIT License to be found in `LICENSE`. The full source can be obtained from <https://concurrency-theory.org/ltbt-spectroscope/code/>.

js-api/src/main/notebooks/spectroscopy-1.ipynb

@@ -11,29 +11,38 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 5,
+   "execution_count": 2,
    "metadata": {},
    "outputs": [
     {
-     "ename": "TypeError",
-     "evalue": "eqSpectro.LTBTS is not a function",
-     "output_type": "error",
-     "traceback": [
-      "evalmachine.<anonymous>:1",
-      "eqSpectro.LTBTS()",
-      "          ^",
-      "",
-      "TypeError: eqSpectro.LTBTS is not a function",
-      "    at evalmachine.<anonymous>:1:11",
-      "    at Script.runInThisContext (node:vm:129:12)",
-      "    at Object.runInThisContext (node:vm:305:38)",
-      "    at run ([eval]:1020:15)",
-      "    at onRunRequest ([eval]:864:18)",
-      "    at onMessage ([eval]:828:13)",
-      "    at process.emit (node:events:390:28)",
-      "    at emit (node:internal/child_process:917:12)",
-      "    at processTicksAndRejections (node:internal/process/task_queues:84:21)"
-     ]
+     "data": {
+      "text/plain": [
+       "{\n",
+       "  bisimulation: [\n",
+       "    2147483647,\n",
+       "    2147483647,\n",
+       "    2147483647,\n",
+       "    2147483647,\n",
+       "    2147483647,\n",
+       "    2147483647\n",
+       "  ],\n",
+       "  failure: [ 2147483647, 1, 0, 0, 1, 1 ],\n",
+       "  enabledness: [ 1, 0, 0, 0, 0, 0 ],\n",
+       "  traces: [ 2147483647, 0, 0, 0, 0, 0 ],\n",
+       "  'ready-trace': [ 2147483647, 2147483647, 1, 2147483647, 1, 1 ],\n",
+       "  'ready-simulation': [ 2147483647, 2147483647, 2147483647, 2147483647, 1, 1 ],\n",
+       "  'impossible-future': [ 2147483647, 1, 0, 0, 1, 2147483647 ],\n",
+       "  readiness: [ 2147483647, 1, 0, 2147483647, 1, 1 ],\n",
+       "  simulation: [ 2147483647, 2147483647, 2147483647, 2147483647, 0, 0 ],\n",
+       "  'failure-trace': [ 2147483647, 2147483647, 1, 1, 1, 1 ],\n",
+       "  '2-nested-simulation': [ 2147483647, 2147483647, 2147483647, 2147483647, 1, 2147483647 ],\n",
+       "  'possible-future': [ 2147483647, 1, 2147483647, 2147483647, 1, 2147483647 ]\n",
+       "}"
+      ]
+     },
+     "execution_count": 2,
+     "metadata": {},
+     "output_type": "execute_result"
     }
    ],
    "source": [
@@ -42,7 +51,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 2,
+   "execution_count": 3,
    "metadata": {},
    "outputs": [
     {
@@ -162,7 +171,7 @@
        "}"
       ]
      },
-     "execution_count": 2,
+     "execution_count": 3,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -251,7 +260,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 3,
+   "execution_count": 4,
    "metadata": {},
    "outputs": [
     {
@@ -273,7 +282,7 @@
        "]"
       ]
      },
-     "execution_count": 3,
+     "execution_count": 4,
      "metadata": {},
      "output_type": "execute_result"
     }

shared/src/main/scala-2.12/de/bbisping/eqfiddle/spectroscopy/AbstractSpectroscopy.scala

@@ -151,7 +151,7 @@ object AbstractSpectroscopy {
         p = orderedPair(0)
         q = orderedPair(1)
         eq <- findEqs(p, q)
-      } yield (p, eq._1, q)
+      } yield (p, eq._1 + " eq", q)
       new LabeledRelation(relTuples.toSet)
     }