search

freespek / solarkraft

Solakraft: a runtime monitoring tool for Soroban, powered by TLA+ and Apalache
Apache License 2.0
10 stars 0 forks source link

Correctness fix in default status #105

Closed Kukovec closed 2 weeks ago

Kukovec commented 2 weeks ago

Found this while doing the demo, since VerificationStatus::Unknown absorbs NoViolation, the initial fold-value must be a NoViolation, since otherwise Unknown (initial) + NoViolation (actual result) give an Unknown, instead of a NoViolation

thpani commented 2 weeks ago

I think you'll have to rebase on main to get the tests working