Formula negation

[owickstrom]

Adds a not(...) function and .not() method for formula. Negation is pushed down into NNF, through thunks as they're evaluated.

Also adds a time bound on always to make it dual with eventually, and both those bounds are now optional.

Closes #13.

[Copilot]

Pull request overview

This PR adds first-class formula negation support (via not(...) and .not()) by introducing a syntactic formula layer (ltl::Syntax) and pushing negation into negation-normal-form (NNF), including through thunks during evaluation. It also makes eventually bounds optional and adds optional time bounds to always to restore dualities.

Changes:

• Introduces ltl::Syntax parsing from JS values and converts formulas to NNF (Syntax::nnf()), tracking thunk polarity with Formula::Thunk { negated }.
• Extends temporal operators so always and eventually accept optional bounds, and updates evaluation/residual/violation structures accordingly.
• Adds verifier tests for .not(), bounded always, unbounded eventually, and bounded eventually, plus updates rendering for bounded-always violations.

Reviewed changes

Copilot reviewed 5 out of 5 changed files in this pull request and generated 5 comments.

Show a summary per file

File	Description
src/specification/verifier.rs	Switches property initialization to Syntax::from_value(...).nnf() and adds tests for negation and bounded/unbounded temporal operators.
src/specification/render.rs	Updates formula/violation rendering for new Formula shape and bounded Always violations.
src/specification/ltl.rs	Adds Syntax + NNF conversion, updates Formula representation, and extends evaluation logic to support optional bounds and thunk negation.
src/specification/index.ts	Adds .not() method and updates always/eventually API to support optional time bounds with .within(...).
src/specification/bombadil_exports.rs	Exposes the new Not runtime class export to Rust.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.