Convert TLC counterexample traces into Gherkin acceptance scenarios.
npx skills add https://github.com/Hakkadaikon/hymme --skill loopeng-gherkin-hakkadaikon
Please help me install this Agent Skill. Skill: loopeng-gherkin Source: https://github.com/Hakkadaikon/hymme/tree/main/skills/loopeng-gherkin Command: npx skills add https://github.com/Hakkadaikon/hymme --skill loopeng-gherkin-hakkadaikon
.feature files so design-level bugs become executable acceptance specifications that bridge into implementation testing. ## Core Features & Use Cases - Counterexample Conversion: Transform TLC error traces into Gherkin Scenarios where the initial state becomes Given, each action becomes When, and changed variables become Then becomes ... assertions. - Acceptance Scenario Authoring: Once the design stabilizes, add positive EARS-based acceptance scenarios to the .feature file and wire them into implementation acceptance tests. - Runner Wiring Guidance: Reference documentation covers language-native Cucumber runners (pytest-bdd, cucumber-js, godog, and others) plus a C conversion path for freestanding environments, with green/red verification of the wiring. - Use Case: After loopeng-modelcheck finds an invariant violation, run the inner loop to generate a .feature capturing the failing behavior, fix the design until the counterexample disappears, then hand the scenarios to test-extract for ledger registration before writing implementation tests. ## Quick Start Convert the TLC counterexample trace from my last model check into a Gherkin feature file and add positive acceptance scenarios for the stabilized design.High-intent search queries and answers about installing and using this skill.
Run the inner loop command with the spec name, which invokes trace_to_gherkin.py to mechanically convert the TLC error trace. The initial state becomes Given steps, each action becomes a When step, and changed variables become Then becomes assertions.
Use language-native Cucumber OSS runners: pytest-bdd or behave for Python, cucumber-js for JS/TS, godog for Go, cucumber-rs for Rust, and cucumber-jvm for Java/Kotlin. You write one thin glue layer mapping When actions to implementation calls and Then steps to state comparisons.
Yes, but no off-the-shelf runner exists for that environment. Use feature_to_c.py with a project-specific JSON mapping file to convert machine-format features into C CHECK sequences, then link the generated code into your own test harness as a single translation unit.
No. Generated features must never be hand-edited; fix the source spec or EARS requirements and regenerate instead. The generators also only accept machine-format output from trace_to_gherkin.py, not hand-written prose scenarios.
Writing implementation tests without transferring scenarios to test-extract is blocked by the test-design-extract-gate hook. Each scenario must become one T-ID row in the test design ledger with the feature file recorded as its source.
dtsongGenerate TLA+ specifications and TLC configurations for formal security verification.
laraxotGenerate failing acceptance tests before implementation using the TDD cycle.
santosomarGenerate TLA+ specifications from natural language or pseudocode descriptions.
StudentCristianFormalize system behavior in TLA+ to validate invariants and prove design correctness.