Model-based Testing With Quickcheck-Dynamic #391

KtorZ · 2022-06-09T10:20:30Z

No description provided.

github-actions · 2022-06-09T11:21:12Z

Transactions Costs

Sizes and execution budgets for Hydra protocol transactions. Note that unlisted parameters are currently using arbitrary values and results are not fully deterministic and comparable to previous runs.

Metadata
Generated at	2022-06-28 07:40:59.361073594 UTC
Max. memory units	14000000.00
Max. CPU units	10000000000.00
Max. tx size (kB)	16384

Cost of Init Transaction

Parties	Tx size	% max Mem	% max CPU
1	4737	11.58	6.31
2	4937	13.71	7.41
3	5138	13.06	6.80
5	5538	18.44	9.66
10	6537	27.15	13.92
30	10539	65.48	33.11
47	13938	98.36	49.61

Cost of Commit Transaction

Currently only one UTxO per commit allowed (this is about to change soon)

UTxO	Tx size	% max Mem	% max CPU
1	6233	19.55	9.67

Cost of CollectCom Transaction

Parties	Tx size	% max Mem	% max CPU
1	14181	21.09	11.41
2	14482	37.00	20.23
3	14697	53.86	29.50
4	14995	75.40	41.48

Cost of Close Transaction

Parties	Tx size	% max Mem	% max CPU
1	9827	7.77	4.11
2	9992	8.69	4.61
3	10157	9.59	5.09
5	10520	11.80	6.27
10	11345	16.19	8.60
30	14710	34.77	18.48
62	15899	36.41	18.36

Cost of Contest Transaction

Parties	Tx size	% max Mem	% max CPU
1	9859	8.18	4.33
2	9991	8.66	4.59
3	10187	9.91	5.25
5	10517	11.73	6.22
10	11342	16.17	8.58
30	14712	35.28	18.79
40	16359	43.61	23.19

Cost of Abort Transaction

Parties	Tx size	% max Mem	% max CPU

Cost of FanOut Transaction

Involves spending head output and burning head tokens. Uses ada-only UTxO for better comparability.

UTxO	Tx size	% max Mem	% max CPU
10	14133	22.13	12.72
50	15585	82.94	47.64
496	14032	12.46	7.16

…ent)

…d insane

and spawns a thread to run the nodes

Also distinct ctors for each action type and increase success to increase coverage

also provide correct Eq and Show instances for Actions

Question: how do we get a handle on the test nodes from within the property execution?

Need to accumulate observed outputs

Now we can write moar!

Also adapt generators to reduce the number of discarded actions

* Use tabulate instead of label for better classification * Improve generators to reduce the number of discards * Tweak frequencies to increase the number of Initial -> Open transitions which are more interesting

Implementing actionName allows us to provide sensible names for actions and remove the need for dedicated constructors.

So far, we only send to addresses owned by participants of the head. We may want to change that later, but that is tricky because, if there's no longer any utxo owned by participants, they can't spend anything.

We realise we need to make our model more abstract as we don't have access to the details of the snapshots easily.

We model payments, and only within the inner-circle of the head participants. This is analogous to an account-based system. Kind of.

This removes the Typable constraint on the model and was needed to explore ideas on how we could use DynLogic stuff with the ActionMonad being over IOSim

Still puzzling how to get it to work with (forall s. IOSim s)

github-actions · 2022-06-23T10:37:04Z

Unit Test Results

229 tests +4 227 ✔️ +4 7m 50s ⏱️ +21s
  83 suites +1     2 💤 ±0
    5 files ±0     0 ❌ ±0

Results for commit 1161107. ± Comparison against base commit 68024d5.

♻️ This comment has been updated with latest results.

This is stashed in another branch we'll be working on soonish

abailly-iohk · 2022-06-23T12:42:34Z

Fix #375

abailly-iohk · 2022-06-23T12:44:56Z

@ch1bo @KtorZ If you are happy with my latest changes, I think we can merge this and move on.

ch1bo

These things need addressing:

api changed -> update api.yaml and changelog (why are we seeing no CI errors?)
Take a Proxy log instead of a Proxy tx in printTrace

hydra-node/src/Hydra/Crypto.hs

hydra-node/src/Hydra/ServerOutput.hs

hydra-node/test/Hydra/Model.hs

hydra-node/test/Test/Util.hs

Oddly enough this did not break our tests, we probably need to strengthen our property check here

ch1bo · 2022-06-24T06:37:24Z

hydra-node/test/Test/Util.hs

 printTrace _ tr =
  unlines . map (decodeUtf8 . Aeson.encode) $
-    selectTraceEventsDynamic' @_ @(HydraNodeLog tx) tr
+    selectTraceEventsDynamic' @_ @log tr


abailly-iohk · 2022-06-28T08:31:17Z

This is a first shot of MBT approach using Quviq's framework, I think we should merge it as-is. We have a follow-up meeting with Quviq end of the week which will provide some insights on what to do next.

KtorZ requested review from ch1bo and abailly-iohk June 9, 2022 10:20

KtorZ force-pushed the qd-model branch from bf34aef to d6becb4 Compare June 17, 2022 07:56

abailly-iohk and others added 26 commits June 22, 2022 14:31

[wip] Write a simple QD model for HeadLogic

b5ea26b

[wip] Making some progress on model, now trygin to execute test

99caa35

WIP: make StateModel play nicely with IOSim

2a00ca1

WIP: fixing shrinking so that it does something (not ideal at the mom…

ba6136f

…ent)

WIP: unsafeCoerce hack to get arund QuickCheck's PropertyM being a ta…

1a796a8

…d insane

Try to get rid of some Typeable constraints but still having troubles

754d70f

Fix Model so that it can run in hspec 🎉

6d7a16e

Add Commits to the model

7718d00

and spawns a thread to run the nodes

Add Commit and Abort actions

cbc36ed

Also distinct ctors for each action type and increase success to increase coverage

Wait for Init to perform Commit

41473c0

also provide correct Eq and Show instances for Actions

Write first assertion on the model: assert commits consistency.

d340bec

Question: how do we get a handle on the test nodes from within the property execution?

Correctly compare node's state with model

b305048

Need to accumulate observed outputs

Improve error message on failed assertion

139da3a

Fix recording of server outputs in TestHydraNode

1cb03f8

Move state-model assertion in separate function

a5495d5

Now we can write moar!

Assert Head is opened with the right commits

1d71b90

Try labelling transitions to enrich the model output.

e741258

Add more labels for transitions and generate more tests

1c5fc8c

Simplify testing machinery for StateModel

e3d12fd

Unify Model to have a single consensus state

63a9606

Also adapt generators to reduce the number of discarded actions

Improvements to model-based test output

07f1290

* Use tabulate instead of label for better classification * Improve generators to reduce the number of discards * Tweak frequencies to increase the number of Initial -> Open transitions which are more interesting

Simplify Action type as a wrapper around ClientInput

6b65a48

Implementing actionName allows us to provide sensible names for actions and remove the need for dedicated constructors.

Reject transition by default

9dd5959

Work towards generating transaction on Open

d7a387c

So far, we only send to addresses owned by participants of the head. We may want to change that later, but that is tricky because, if there's no longer any utxo owned by participants, they can't spend anything.

[wip] Implement perform on NewTx

a98d6ea

We realise we need to make our model more abstract as we don't have access to the details of the snapshots easily.

Rework model to use abstract representation of Ledger/UTxO

9ffe210

We model payments, and only within the inner-circle of the head participants. This is analogous to an account-based system. Kind of.

ch1bo and others added 8 commits June 23, 2022 09:10

Remove empty quickcheck directory artifact (former submodule?)

30c2d46

Fix quickcheck-dynamic package reference to remote one

08c5735

Rename property checking balances

9001d23

Rephrase liveness property

4b47bf9

genPayment instead of genNewTx (an Action)

89cf064

This removes the Typable constraint on the model and was needed to explore ideas on how we could use DynLogic stuff with the ActionMonad being over IOSim

Draft a property using the DynamicLogic

74b7d2a

Use a branched quickcheck-dynamic to make it compile

324448f

Still puzzling how to get it to work with (forall s. IOSim s)

Make Model-based tests pass

c27dcce

abailly-iohk added 3 commits June 23, 2022 11:26

Missing golden files

99d0600

Clean-up and document Model

360ebbf

Remove dynamic logic stuff

af3d6f7

This is stashed in another branch we'll be working on soonish

abailly-iohk approved these changes Jun 23, 2022

View reviewed changes

ch1bo requested changes Jun 23, 2022

View reviewed changes

abailly-iohk added 4 commits June 23, 2022 14:04

Remove Ord instance for SigningKey

54ff20a

Update YAML for logs following change in API

4ca43bb

Oddly enough this did not break our tests, we probably need to strengthen our property check here

Rename performs -> sendsInput

db7a68e

Make printTrace more generic

7153cc5

ch1bo reviewed Jun 24, 2022

View reviewed changes

ch1bo approved these changes Jun 24, 2022

View reviewed changes

abailly-iohk requested a review from ch1bo June 24, 2022 06:46

abailly-iohk added 2 commits June 28, 2022 07:15

Dedup parties list when generating HeadParameters

e0e87f6

Fix API schema for CommandFailed server output

1161107

ch1bo approved these changes Jun 28, 2022

View reviewed changes

abailly-iohk merged commit 1b9992a into master Jun 28, 2022

abailly-iohk deleted the qd-model branch June 28, 2022 13:32

ch1bo mentioned this pull request Jul 1, 2022

Spike: Model-based testing of Hydra protocol using quickcheck-dynamic #375

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Model-based Testing With Quickcheck-Dynamic #391

Model-based Testing With Quickcheck-Dynamic #391

KtorZ commented Jun 9, 2022

github-actions bot commented Jun 9, 2022 •

edited

Loading

github-actions bot commented Jun 23, 2022 •

edited

Loading

abailly-iohk commented Jun 23, 2022

abailly-iohk commented Jun 23, 2022

ch1bo left a comment

ch1bo Jun 24, 2022

abailly-iohk commented Jun 28, 2022

Model-based Testing With Quickcheck-Dynamic #391

Model-based Testing With Quickcheck-Dynamic #391

Conversation

KtorZ commented Jun 9, 2022

github-actions bot commented Jun 9, 2022 • edited Loading

Transactions Costs

Cost of Init Transaction

Cost of Commit Transaction

Cost of CollectCom Transaction

Cost of Close Transaction

Cost of Contest Transaction

Cost of Abort Transaction

Cost of FanOut Transaction

github-actions bot commented Jun 23, 2022 • edited Loading

Unit Test Results

abailly-iohk commented Jun 23, 2022

abailly-iohk commented Jun 23, 2022

ch1bo left a comment

Choose a reason for hiding this comment

ch1bo Jun 24, 2022

Choose a reason for hiding this comment

abailly-iohk commented Jun 28, 2022

github-actions bot commented Jun 9, 2022 •

edited

Loading

github-actions bot commented Jun 23, 2022 •

edited

Loading