Data

Tools

Indexes

Applications

Experiments

Open Source Science

ltl2dfa

A series of programs that can create LTL formulas or take user provided ones, converts them to a DFA and can generate Traces

https://github.com/jkomp/ltl2dfa

Science Score: 44.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
  • ○
    Academic email domains
  • ○
    Institutional organization owner
  • ○
    JOSS paper metadata
  • ○
    Scientific vocabulary similarity
    Low similarity (12.2%) to scientific vocabulary
Last synced: 6 months ago · JSON representation ·

Repository

A series of programs that can create LTL formulas or take user provided ones, converts them to a DFA and can generate Traces

Basic Info
  • Host: GitHub
  • Owner: JKomp
  • License: mit
  • Language: Jupyter Notebook
  • Default Branch: main
  • Size: 1.42 MB
Statistics
  • Stars: 4
  • Watchers: 1
  • Forks: 0
  • Open Issues: 0
  • Releases: 0
Created about 2 years ago · Last pushed over 1 year ago
Metadata Files
Readme License Citation

README.md

LTL2DFA

This is a tool for creating DFAs from LTL source formulas. It provides the following capabilities: * Create DFA from given LTL formula * Generate traces through DFA * Show coverage of all states and edges

Formulas used can come from one of three sources: * Specifically given * Selected from a table of existing formulas * Auto generated by Spot

This tool is currently only available as a Jupyter Notebook. It is an alternate front end for Spot that uses the LTL formula manipulation and DFA generation capabilities to create a test generation tool for working with DFAs.

Spot can be obtained from: https://spot.lre.epita.fr

How to use this tool

To control the execution of this generator, there are the option parameters to set:

Specification Related Parameters

formulaType This defines where the specification comes from. The options are: * 'Fixed' Used a fixed formula found in the Formula class. * 'Random' Ask Spot for a random formula * 'Given' Give the formula directly

fixedFormulaNum If using a fixed formula, this parameter specifies which one. Currently allows selection 0-15
rndNumFormulas If Spot is generating the formula, define how many to generate. The code will attempt to select an interesting one
startFormula The specific formula to use

dOptions All the formulas are sent to Spot to generate an automaton. This paramenter defines what type of automaton to create. The options are Complete, Unambiguous, tgba. See the Spot documentation for more info.

rndSeed=True For repeatability, set this to false. when set to True, the seed used is defined in getSeed().

Trace Related Parameters

runLen Length of each trace genrated
numRuns Number of traces to generate

Graph Display Control

path Defines where saved files will go

graphPrint Print the original automaton graph
graphSourceSave the graph source in dot format
graphFile A dictionary of graph file output control

tracePrint Display a detail log of each trace showing predicates along with stating and ending states for each trace step
traceGraphPrint Display the automaton graph color coded for coverate. Green = path or state seen in at least one trace
traceSource Save the graph source in dot format traceGraphFile A dictionary of graph file output control

Owner

  • Login: JKomp
  • Kind: user
  • Location: University of Colorado, Boulder

Citation (CITATION.cff) 

cff-version: 1.2.0
message: "If you use this software, please cite it as below."
authors:
- family-names: "Komp"
  given-names: "John"
  orcid: "https://orcid.org/0009-0009-7856-8433"
title: "LTL2DFA Trace Generation Tool"
version: 1.0.0
date-released: 2024-01-31
url: "https://github.com/JKomp/LTL2DFA"

GitHub Events

Total
  • Watch event: 1
Last Year
  • Watch event: 1