Detailed Code Metrics
To demonstrate the reusability and versatility of owl we show LoC metrics. In particular, these metrics indicate the total lines of code that could be saved by re-using for a new algorithm. These numbers are based on the 18.06 release.
| Package | LoC |
|---|---|
automaton |
9028 |
ltl |
7493 |
factories |
1479 |
run |
2999 |
| JBDD | 4732 |
| Other utility | 3445 |
| Total | 29176 |
This table presents the total lines of code (including import statements, comments, etc.) currently in together with the respective share of each major package, namely ltl (LTL syntax, simplifications, etc.), automaton (Automaton representation, acceptance, etc.), factories (symbolic data structure abstraction), and run (CLI and I/O infrastructure).
| Tool | LoC | Percentage |
|---|---|---|
| Delag | 1381 | 5% |
| Rabinizer | 8502 | 29% |
dra2dpa |
717 | 2% |
ldba2dpa |
500 | 2% |
ltl2ldba |
3891 | 13% |
ltl2dpa |
475 | 2% |
ltl2dgra |
2919 | 10% |
| Seminator reimpl. | 309 | 1% |
The second table includes the total size of some translations together with their relative size compared to owl. We did not include MoChiBa (model checking based on ltl2ldba, integrated in PRISM) and Strix (LTL synthesis tool, implemented in C++), since their architecture complicates a comprehensive comparison.
Many constructions only need a few hundred lines of code for their implementation, demonstrating the significant aid provided by owl.