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
To control the execution of this generator, there are the option parameters to set:
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().
runLen Length of each trace genrated
numRuns Number of traces to generate
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