specification-to-temporal-logic-generator
Installation
SKILL.md
Specification → Temporal Logic Generator
Three logics, one job: saying precisely what "always" and "eventually" mean. The choice of logic is mostly dictated by your checker; the choice of formula is the craft.
Which logic?
| Logic | Time model | Checker | When it's the right fit |
|---|---|---|---|
| LTL | Linear — one future | Spin, NuSMV, most | "On every execution, X eventually holds" |
| CTL | Branching — many futures | NuSMV, nuXmv | "There exists an execution where..." / "on all branches..." |
| TLA | Linear + actions | TLC, TLAPS | Distributed systems; → requirement-to-tlaplus-property-generator |
LTL vs CTL: LTL quantifies over paths implicitly (every path). CTL quantifies explicitly (A = all paths, E = some path). The formula AG EF reset ("from any state, it's possible to reach reset") is CTL-only — LTL can't say "possible."