Problem Statement
#bmc and #kind print the input at each depth but not the state it produces, so the state that violates the invariant never appears. #kind names a state only at depth 0, #bmc names none at any depth, and since the model is reported per declared constant, an inlined term has no name for a value to attach to.
import Blaster.StateMachine
open Blaster.StateMachine
structure S where
x : Int
structure I where
y : Int
instance sm : StateMachine I S where
init _ := { x := 0 }
next i s := { x := s.x + i.y }
assumptions i _ := 0 ≤ i.y ∧ i.y ≤ 1
invariants _ s := s.x ≤ 2
#kind (max-depth: 3) [sm]Current output:
❌ Falsified
Counterexample detected at Depth 3:
- «sm.state@0»: (S.mk 0)
- «sm.input@0»: (I.mk 1)
- «sm.input@1»: (I.mk 1)
- «sm.input@2»: (I.mk 1)
- «sm.input@3»: (I.mk 1)
The invariant fails at depth 3, so the reader needs state@3. To get it from this trace they have to know that the state at depth d is built from the input at depth d, that input@0 contributes nothing because init ignores its argument, and then sum the remaining three. None of that is shown. Four identical values are printed, one is a decoy, and the value the verdict turns on is absent.
Which inputs contribute is not inferable from the trace either. In this run the encoding below shows that input@0 is genuinely absent from the depth-3 invariant, but nothing in the printed output says so.
Alternatives Considered
-
Reconstruct the states by hand from the inputs. That is the burden itself rather than a way around it, and it grows with the number of steps, since every state depends on the whole prefix once next reads the previous state. All the machines in Tests/StateMachine are of that kind.
-
dump-smt-lib. This shows why the value cannot be reported rather than providing it. Running the same machine with (dump-smt-lib: 1), the problem declares one state constant and four input constants:
(declare-const $0 @S)
(declare-const $1 @I)
(declare-const $2 @I)
(declare-const $3 @I)
(declare-const $4 @I)
and the depth-0 and depth-3 invariants are encoded as:
(define-fun _inv@0 () Bool (not (< 2 (S.mk.0 $0))))
(define-fun _inv@3 () Bool (not (< 2 (+ (+ (+ (S.mk.0 $0) (I.mk.0 $2)) (I.mk.0 $3)) (I.mk.0 $4)))))
Depth 0 refers to $0, a declared constant, which is why state@0 is reported. Depth 3 is a nested sum with no constant of its own, so there is nothing for the model to attach a value to. The dump gives the reader that expression to evaluate by hand rather than the value.
-
verbose, and the Translate.expr and Translate.optExpr trace classes. As far as we could tell these are pre-solve and echo symbolic expressions rather than model values.
We found no existing setting that reports intermediate states.
Use Case
The same machine, with the states present. This is the requested output, not current behaviour:
❌ Falsified
Counterexample detected at Depth 3:
- «sm.state@0»: (S.mk 0)
- «sm.input@0»: (I.mk 1)
- «sm.input@1»: (I.mk 1)
- «sm.state@1»: (S.mk 1)
- «sm.input@2»: (I.mk 1)
- «sm.state@2»: (S.mk 2)
- «sm.input@3»: (I.mk 1)
- «sm.state@3»: (S.mk 3)
The counter walks 0, 1, 2, 3 and the invariant s.x ≤ 2 visibly breaks at the last step. Nothing has to be reconstructed, and there is no way to pair a state with the wrong input.
Priority
Medium - Would be beneficial
Additional Context
#kind already declares a state at depth 0 and asserts it equal to init, so there is precedent for the shape.
Naming intermediate states would change counterexample text, so goldens that pin traces would need regenerating. It may also overlap with any future temporal operators for inspecting past steps, since those would presumably want per-depth state addressable as well.
Problem Statement
#bmcand#kindprint the input at each depth but not the state it produces, so the state that violates the invariant never appears.#kindnames a state only at depth 0,#bmcnames none at any depth, and since the model is reported per declared constant, an inlined term has no name for a value to attach to.Current output:
The invariant fails at depth 3, so the reader needs
state@3. To get it from this trace they have to know that the state at depth d is built from the input at depth d, thatinput@0contributes nothing becauseinitignores its argument, and then sum the remaining three. None of that is shown. Four identical values are printed, one is a decoy, and the value the verdict turns on is absent.Which inputs contribute is not inferable from the trace either. In this run the encoding below shows that
input@0is genuinely absent from the depth-3 invariant, but nothing in the printed output says so.Alternatives Considered
Reconstruct the states by hand from the inputs. That is the burden itself rather than a way around it, and it grows with the number of steps, since every state depends on the whole prefix once
nextreads the previous state. All the machines inTests/StateMachineare of that kind.dump-smt-lib. This shows why the value cannot be reported rather than providing it. Running the same machine with(dump-smt-lib: 1), the problem declares one state constant and four input constants:and the depth-0 and depth-3 invariants are encoded as:
Depth 0 refers to
$0, a declared constant, which is whystate@0is reported. Depth 3 is a nested sum with no constant of its own, so there is nothing for the model to attach a value to. The dump gives the reader that expression to evaluate by hand rather than the value.verbose, and theTranslate.exprandTranslate.optExprtrace classes. As far as we could tell these are pre-solve and echo symbolic expressions rather than model values.We found no existing setting that reports intermediate states.
Use Case
The same machine, with the states present. This is the requested output, not current behaviour:
The counter walks 0, 1, 2, 3 and the invariant
s.x ≤ 2visibly breaks at the last step. Nothing has to be reconstructed, and there is no way to pair a state with the wrong input.Priority
Medium - Would be beneficial
Additional Context
#kindalready declares a state at depth 0 and asserts it equal toinit, so there is precedent for the shape.Naming intermediate states would change counterexample text, so goldens that pin traces would need regenerating. It may also overlap with any future temporal operators for inspecting past steps, since those would presumably want per-depth state addressable as well.