forklift

The program FORKLIFT is an inclusion checker for Büchi automata. The input format of the automata is described here: http://languageinclusion.org/doku.php?id=tools#the_ba_format

https://github.com/mazzocchi/forklift

Science Score: 54.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
✓
Academic publication links
Links to: arxiv.org
○
Academic email domains
○
Institutional organization owner
○
JOSS paper metadata
○
Scientific vocabulary similarity
Low similarity (6.5%) to scientific vocabulary

Last synced: 6 months ago · JSON representation ·

Repository

The program FORKLIFT is an inclusion checker for Büchi automata. The input format of the automata is described here: http://languageinclusion.org/doku.php?id=tools#the_ba_format

Basic Info

Host: GitHub
Owner: Mazzocchi
License: gpl-3.0
Language: Java
Default Branch: master
Homepage:
Size: 705 KB

Statistics

Stars: 9
Watchers: 1
Forks: 3
Open Issues: 0
Releases: 1

Created almost 4 years ago · Last pushed almost 2 years ago

Metadata Files

Readme License Citation

ABOUT

FORKLIFT is an inclusion checker for Büchi automata. The input comprises two automata A and B and FORKLIFT decides whether L(A) ⊆ L(B) holds.

The input format for the automata is described here.

Upon termination, FORKLIFT returns one of the following value:

0 if L(A) ⊆ L(B)
1 if L(A) ⊈ L(B) and a counterexample u cycle {v} such that u v^ω ∈ L(A) but u v^ω ∉ L(B)
127 when something goes wrong

COMPILATION

Run make to compile. Running make in the root directory compiles the source code (using javac), then constructs the java archive (using jar), and finally prints the usage of FORKLIFT.

RUNNING

Run FORKLIFT as follows: java -jar forklift.jar sub.ba sup.ba checks whether L(A) ⊆ L(B) holds for the input Büchi automata A given by sub.ba and B given by sup.ba.

OPTIONS ####

Insert options anywhere after forklift.jar. For instance, running java -jar forklift.jar -t sub.ba -o sup.ba -v uses the options optimization (-o), verbose (-v) and time (-t). Use -h to know more about the options: java -jar forklift.jar -h

EXAMPLES

The folder samples contains examples of Büchi automata. For instance, running java -jar forklift.jar ./samples/example_SUPERSET.ba ./samples/example_SUBSET.ba checks the inclusion given at Figure 1 in our CAV'22 paper. In this case the inclusion does not hold and FORKLIFT provides the counterexample u cycle {v} to the inclusion.

Owner

Login: Mazzocchi
Kind: user

Repositories: 2
Profile: https://github.com/Mazzocchi

Citation (CITATION.cff)

cff-version: 1.2.0
message: "Please cite this work as below."
preferred-citation:
  type: conference-paper
  authors:
  - family-names: "Doveri"
    given-names: "Kyveli"
    orcid: "https://orcid.org/0000-0001-9403-2860"
  - family-names: "Ganty"
    given-names: "Pierre"
    orcid: "https://orcid.org/0000-0002-3625-6003"
  - family-names: "Mazzocchi"
    given-names: "Nicolas"
    orcid: "https://orcid.org/0000-0001-6425-5369"
  title: "FORKLIFT: FORQ-based Language Inclusion Formal Testing"
#  doi: ""
  journal: "34th International Conference on Computer Aided Verification, {CAV} 2022, August 7-10, 2022, The Technion, Haifa, Israel, Proceedings"
#  month: 7
#  start: 1 # First page number
#  end: 10 # Last page number
#  issue: 1
#  volume: 1
  year: 2022

ecosyste.ms

Data

Tools

Indexes

Applications

Experiments

Open Source Science