counterexample-to-test-generator
Automatically generates executable test cases from model checking counterexample traces. Translates abstract counterexample states and transitions into concrete test inputs, execution steps, and assertions that reproduce property violations. Use when working with model checker outputs (SPIN, CBMC, NuSMV, TLA+, Java PathFinder, etc.) and needing to create regression tests, validate bug fixes, or reproduce verification failures in executable test suites.
90
85%
Does it follow best practices?
Impact
99%
1.16xAverage score across 3 eval scenarios
Passed
No known issues
Quality
Discovery
100%Based on the skill's description, can an agent find and select it at the right time? Clear, specific descriptions lead to better discovery.
This is an excellent skill description that clearly defines a specialized capability in the model checking and formal verification domain. It provides specific actions, comprehensive trigger terms including tool names, explicit 'Use when...' guidance, and occupies a distinct niche that won't conflict with other skills. The description is appropriately detailed without being verbose.
| Dimension | Reasoning | Score |
|---|---|---|
Specificity | Lists multiple specific concrete actions: 'generates executable test cases', 'translates abstract counterexample states and transitions into concrete test inputs, execution steps, and assertions', 'reproduce property violations'. Very detailed about what it does. | 3 / 3 |
Completeness | Clearly answers both what ('generates executable test cases from model checking counterexample traces', 'translates abstract counterexample states...') AND when with explicit 'Use when...' clause covering multiple trigger scenarios (model checker outputs, regression tests, validate bug fixes, reproduce verification failures). | 3 / 3 |
Trigger Term Quality | Excellent coverage of natural terms including specific tool names (SPIN, CBMC, NuSMV, TLA+, Java PathFinder), domain terms (model checker, counterexample traces, property violations), and use case terms (regression tests, bug fixes, verification failures). | 3 / 3 |
Distinctiveness Conflict Risk | Highly distinctive niche focusing specifically on model checking counterexamples and test generation. The specific tool names and domain terminology (counterexample traces, property violations, verification failures) make it very unlikely to conflict with general testing or code generation skills. | 3 / 3 |
Total | 12 / 12 Passed |
Implementation
70%Reviews the quality of instructions and guidance provided to agents. Good implementation is clear, handles edge cases, and produces reliable results.
This skill provides a solid workflow for a complex task with good structure and clear references to supporting materials. However, it could be more concise by removing explanatory content Claude already knows, and the actionability suffers from incomplete code examples that aren't fully executable. The workflow clarity and progressive disclosure are strengths.
Suggestions
Remove the Overview section and explanatory text that restates the skill's purpose - start directly with the workflow
Complete the code example with all necessary includes, variable declarations, and the missing thread2_func to make it truly executable
Replace pseudocode placeholders in Step 4 with actual executable code snippets for at least one target language
| Dimension | Reasoning | Score |
|---|---|---|
Conciseness | The content is reasonably efficient but includes some unnecessary explanation (e.g., the Overview section restates what the skill does, and some workflow steps explain concepts Claude would understand). The example and best practices sections add value but could be tighter. | 2 / 3 |
Actionability | Provides a clear workflow structure and includes a concrete code example, but the step-by-step instructions use pseudocode placeholders rather than fully executable code. The example is illustrative but incomplete (missing lock_b, thread2_func, includes). | 2 / 3 |
Workflow Clarity | The 5-step workflow is clearly sequenced with logical progression from analysis through output generation. Each step has numbered sub-steps, and the process includes validation through 'Test the test' in best practices. The workflow handles the complexity of the task well. | 3 / 3 |
Progressive Disclosure | Well-structured with clear sections, appropriate use of references to external files (model_checker_formats.md, test_templates/), and content is organized for easy navigation. References are one level deep and clearly signaled. | 3 / 3 |
Total | 10 / 12 Passed |
Validation
100%Checks the skill against the spec for correct structure and formatting. All validation checks must pass before discovery and implementation can be scored.
Validation — 11 / 11 Passed
Validation for skill structure
No warnings or errors.
- Repository
- ArabelaTso/Skills-4-SE
- Commit
0f00a4f
- Reviewed
Table of Contents
Is this your skill?
If you maintain this skill, you can claim it as your own. Once claimed, you can manage eval scenarios, bundle related skills, attach documentation or rules, and ensure cross-agent compatibility.