Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

ModelSpec is failing on a precondition because of incorrect generator #1239

Closed
abailly-iohk opened this issue Jan 8, 2024 · 1 comment · Fixed by #1248
Closed

ModelSpec is failing on a precondition because of incorrect generator #1239

abailly-iohk opened this issue Jan 8, 2024 · 1 comment · Fixed by #1248
Assignees
Labels
bug 🐛 Something isn't working

Comments

@abailly-iohk
Copy link
Contributor

When running

cabal test hydra-node --test-options="-m conflict-free --seed=358692224"

there test fails because of a failed precondition

...
            action $ NewTx (Party {vkey = HydraVerificationKey (VerKeyEd25519DSIGN "db3a50408fbf6f16ba253f3844e1838f51ba4232cd93281fcc24e9e9284911f2")}) Payment { from = AddressInEra (ShelleyAddressInEra ShelleyBasedEraBabbage) (ShelleyAddress Testnet (KeyHashObj (KeyHash "976c076f698e510fb27c892d97aeef5498b2ed30f8d0fa331f4c1d35")) StakeRefNull), to = AddressInEra (ShelleyAddressInEra ShelleyBasedEraBabbage) (ShelleyAddress Testnet (KeyHashObj (KeyHash "f79ad7a19a558d236efdbe3d409613e4ae3d4f84271e849ca3839930")) StakeRefNull), value = valueFromList [(AdaAssetId,745869)] }  -- Failed precondition

This is caused by the use of withGenQ which is defined in such a way that the "filtering" part of the quantification it defines accepts any generated value meaning the use of this function while shrinking a trace can lead to this situation where an action is selected even though the precondition fails.

@abailly-iohk abailly-iohk self-assigned this Jan 8, 2024
@abailly-iohk abailly-iohk changed the title Create issue / clarify on quickcheck-dynamic about preconditions while shrinking ModelSpec is failing on a precondition because of incorrect generator Jan 8, 2024
@abailly-iohk abailly-iohk added the bug 🐛 Something isn't working label Jan 8, 2024
@abailly-iohk
Copy link
Contributor Author

After a long discussion with @MaximilianAlgehed it seems that withGenQ is not the only issue here. There's also a problem with the generator which can produce TxOut below the minimal value accepted by ledger, which is fine in the model but fails in the execution. However this problem is masked by shrinking: Because there's no dependency between the various actions after we enter the Open state, the shrinker will try to remove any of them. If it removes the NewTx then the ObserveTx will fail because the transaction would not have been submitted and therefore cannot be observed, if it removes transactions before NewTx it can render it invalid because withGenQ does not filter anything.
There's therefore a couple of small fixes to be made to solve the issue, and also some modification to q-d to deprecate the use of withGenQ which does not really make sense.

@abailly-iohk abailly-iohk mentioned this issue Jan 13, 2024
4 tasks
@ch1bo ch1bo modified the milestone: 0.16.0 Apr 3, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug 🐛 Something isn't working
Projects
None yet
Development

Successfully merging a pull request may close this issue.

2 participants