NEGATIVE SPECIFICATION PRESERVED
Unreachable in bounded behavioral exploration — depth ≤ 10, 6 states explored
A refunded order must never be shipped
Context-aware behavior graph
6 states · 5 transitions · forbidden when state = SHIPPED ∧ refundedAt = true
Minimum counterexample
NO COUNTEREXAMPLE
The bounded search explored 6 states without reaching a state that satisfies the forbidden condition.
Transition table
The behavior extracted from the repository as it currently ships
- tr-001cancelOrderPAID → CANCELLEDsrc/services/order-service.ts:64
- tr-002cancelOrderREFUNDED → CANCELLEDsrc/services/order-service.ts:64
- tr-003payOrderCREATED → PAIDsrc/services/order-service.ts:26
- tr-004refundOrderPAID → REFUNDEDsrc/services/order-service.ts:39
- tr-005shipOrderPAID → SHIPPEDsrc/services/order-service.ts:77
No transition constrains refundedAt — the rule holds here because no path re-enters a shippable state after a refund.
Context-aware states
1 lifecycle status splits into multiple graph states by fact context
| status | cancelledAt | paidAt | refundedAt | shippedAt | verdict |
|---|---|---|---|---|---|
| CANCELLED | ✓ | ✓ | ✓ | — | allowed |
| ↳ CANCELLED | ✓ | ✓ | — | — | allowed |
| CREATED | — | — | — | — | allowed |
| PAID | — | ✓ | — | — | allowed |
| REFUNDED | — | ✓ | ✓ | — | allowed |
| SHIPPED | — | ✓ | — | ✓ | allowed |
Graph nodes are (status, facts) tuples. Rows sharing a status are distinct states — identical lifecycle status, different history. Collapsing them to the status string alone is exactly what hides this class of violation.