equivalence-fiddle
Tool for finding the best ways of equating / preordering / distinguishing finite process models.
Science Score: 67.0%
This score indicates how likely this project is to be science-related based on various indicators:
-
✓CITATION.cff file
Found CITATION.cff file -
✓codemeta.json file
Found codemeta.json file -
✓.zenodo.json file
Found .zenodo.json file -
✓DOI references
Found 7 DOI reference(s) in README -
✓Academic publication links
Links to: zenodo.org -
○Academic email domains
-
○Institutional organization owner
-
○JOSS paper metadata
-
○Scientific vocabulary similarity
Low similarity (13.5%) to scientific vocabulary
Keywords
Repository
Tool for finding the best ways of equating / preordering / distinguishing finite process models.
Basic Info
- Host: GitHub
- Owner: benkeks
- License: mit
- Language: Scala
- Default Branch: main
- Homepage: https://equiv.io
- Size: 11.5 MB
Statistics
- Stars: 4
- Watchers: 1
- Forks: 1
- Open Issues: 0
- Releases: 2
Topics
Metadata Files
README.md
Linear-Time–Branching-Time Spectroscope
The “Linear-time–Branching-time Spectroscope” is a web app to find all preorders, equivalences and inequivalences from the linear-time–branching-time spectrum for small processes as described in Bisping, CAV 2023 and Bisping & Jansen, EXPRESS/SOS 2024.
It runs online on https://equiv.io/ .
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!
It's also possible to enter processes with internal behavior, either by tau.P actions or due to communication, (a.0 | a!0) \ {a}. To compare with respect to the weak spectrum, use @compareSilent P1, P2.
How to build
The project can be built using sbt on Java 17 by:
sbt webStage
This will download all dependencies and output a website under web/target/web/stage/index.html that can be run locally in any modern browser.
In order to test that the algorithm determines the expected (in-)equivaences for the example processes from https://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.36.8596, run:
sbt "shared/test"
To perform benchmarks, run:
sbt "shared/run benchmark"
Docker image
To build a docker image that bundles the Scala dependencies and the fiddle (and export it to tgz), run:
docker build . -t equivalence-fiddle
docker save equivalence-fiddle | gzip > doc/artifact/equivalence-fiddle-docker.tar.gz
By default, the docker image starts up a small webserver serving the fiddle on 8080, which can be made live on http://127.0.0.1:8080 like this:
docker run -p 127.0.0.1:8080:8080 --name equivalence-fiddle -d equivalence-fiddle
To reproduce benchmarks from the container, you then can (for instance) run:
docker exec -it equivalence-fiddle sbt "shared/run benchmark"
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 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/ and via 
.
Owner
- Name: Benjamin Bisping
- Login: benkeks
- Kind: user
- Location: Berlin
- Company: TU Berlin
- Website: https://bbisping.de
- Twitter: benkeks
- Repositories: 20
- Profile: https://github.com/benkeks
Computer scientist in the field of analysis and theory of distributed systems. (And sometimes game dev.)
Citation (CITATION.cff)
cff-version: 1.2.0
message: "If you use this software, please cite it as below."
title: Linear-Time—Branching-Time Spectroscope
authors:
- family-names: Bisping
given-names: Benjamin
orcid: https://orcid.org/0000-0002-0637-0171
version: v0.3.0
date-released: 2023-05-04
identifiers:
- description: "Snapshot of the Linear-Time–Branching-Time Spectroscope"
type: doi
value: "10.5281/zenodo.6726493"
license: MIT
repository-code: "https://github.com/benkeks/equivalence-fiddle"
GitHub Events
Total
- Watch event: 1
- Push event: 64
- Pull request event: 12
- Create event: 8
Last Year
- Watch event: 1
- Push event: 64
- Pull request event: 12
- Create event: 8
Issues and Pull Requests
Last synced: 6 months ago
All Time
- Total issues: 0
- Total pull requests: 6
- Average time to close issues: N/A
- Average time to close pull requests: 11 days
- Total issue authors: 0
- Total pull request authors: 1
- Average comments per issue: 0
- Average comments per pull request: 0.0
- Merged pull requests: 5
- Bot issues: 0
- Bot pull requests: 0
Past Year
- Issues: 0
- Pull requests: 6
- Average time to close issues: N/A
- Average time to close pull requests: 11 days
- Issue authors: 0
- Pull request authors: 1
- Average comments per issue: 0
- Average comments per pull request: 0.0
- Merged pull requests: 5
- Bot issues: 0
- Bot pull requests: 0
Top Authors
Issue Authors
Pull Request Authors
- benkeks (11)
- Gobbel2000 (1)
Top Labels
Issue Labels
Pull Request Labels
Dependencies
- actions/checkout v2 composite
- actions/setup-java v2 composite
- actions/upload-artifact v3 composite
- burnett01/rsync-deployments 5.2 composite
- coursier/cache-action v6 composite
- cytoscape 3.21.1
- heap 0.2.7
- lodash.debounce 4.0.8
- lodash.get 4.4.2
- lodash.set 4.3.2
- lodash.topath 4.5.2
- cytoscape ^3.21.1
- sbtscala/scala-sbt eclipse-temurin-jammy-11.0.17_8_1.8.2_2.12.17 build