v0.2.0

This release fixes several soundness bugs in the core LTL model checker, substantially improving the reliability of verification results.

🔴 Correctness fixes (model checking)

• Fix operand transposition in the NNF negation of Until / WeakUntil. Formulas involving Until / Eventually / WeakUntil could return wrong results — e.g. p U r was incorrectly reported as HOLDS. (#16)
• Fix the Release tableau-expansion branches, which assigned the operands incorrectly. (#17)
• Fix check()'s not(.atomic) special case to use universal (not existential) quantification over the initial states. (#18)
• Unify Büchi emptiness checking on a single standard Nested DFS (Holzmann–Peled–Yannakakis / CVWY), removing the non-standard pre-order implementation and the redundant SCC-based fallback. (#21)

⚠️ Robustness

• Tableau construction now throws an error when the GBA state-count limit is exceeded, instead of silently truncating (which could yield an incorrect HOLDS). (#20)

🧹 Maintenance

• Remove debug cruft and dead code (−368 lines in #23; −227 net from the NestedDFS unification in #21). (#21, #23)
• Add the MIT LICENSE file. (#25)
• Add an Apple-platform (macOS) CI job. (#26)

⚠️ Breaking changes

• Removed the unused LTLModelCheckerError.algorithmsNotImplemented case.
• Due to the correctness fixes above, some formulas that previously (incorrectly) returned HOLDS/FAILS now return the correct verdict.

Full Changelog: v0.1.0...v0.2.0

v0.1.0 - Initial Release

This is the initial public release of TemporalKit, a Swift library for expressing, evaluating, and model-checking Linear Temporal Logic (LTL) formulas.

Key Features:

• Type-safe LTL Representation: Define LTL formulas using a Swift-native enum structure.
• Expressive DSL: Construct formulas intuitively with an idiomatic Swift DSL (.globally, .eventually, .until, etc.).
• Trace Evaluation: Check if an LTL formula holds for a given execution trace (sequence of states) using LTLFormulaTraceEvaluator.
• LTL Model Checking: Verify LTL formulas against finite-state system models (KripkeStructure) using advanced algorithms:
  • Translation of LTL formulas to Generalized Büchi Automata (GBA).
  • Optimized GBA acceptance condition generation, including special handling for the Release operator.
  • Efficient Büchi Automaton emptiness checking using an enhanced Nested DFS algorithm.
• Formula Normalization: Automatic simplification of formulas (e.g., double negation elimination, constant propagation).
• Extensible Design: Core protocols (TemporalProposition, EvaluationContext, KripkeStructure) allow for customization and extension.
• Comprehensive Testing: Includes unit tests, integration tests, edge case handling tests, performance benchmarks, and random tests for robustness.
• Demo Application: See Sources/TemporalKitDemo for practical usage examples.

This release provides a solid foundation for working with LTL in Swift projects, particularly for formal verification and analysis tasks.