The monad for writing test scenarios. It supports non-deterministic choice through Alternative, failure with MonadFail, and access to the model state through GetModelState. It is lazy, so scenarios can be potentially infinite, although the probability of termination needs to be high enough that concrete test cases are always finite. See stopping for more information on termination.

Generate a random action using arbitraryAction. The generated action is guaranteed to satisfy its precondition. Fails with Stuck if no action satisfying the precondition can be found after 100 attempts.

Generate a sequence of random actions using arbitraryAction. All actions satisfy their preconditions. The argument is the expected number of actions in the sequence chosen from a geometric distribution, unless in the stopping stage, in which case as few actions as possible are generated.

Generate a sequence of random actions using arbitraryAction. All actions satisfy their preconditions. Actions may be generated until the stopping stage is reached; the expected length is size/2.

Test case generation from DL scenarios have a target length of the action sequence to be generated that is based on the QuickCheck size parameter (see sized). However, given that scenarios can contain explicit actions it might not be possible to stop the scenario once the target length has been reached.

Instead, once the target number of actions have been reached, generation goes into the stopping phase. In this phase branches starting with stopping are preferred, if possible. Conversely, before the stopping phase, branches starting with stopping are avoided unless there are no other possible choices.

For example, here is the definition of anyActions:

anyActions n = stopping <|> pure ()
                       <|> (weight (fromIntegral n) >> anyAction >> anyActions n)

The effect of this definition is that the second or third branch will be taken until the desired number of actions have been generated, at which point the stopping branch will be taken and generation stops (or continues with whatever comes after the anyActions call).

Now, it might not be possible, or too hard, to find a way to terminate a scenario. For instance, this scenario has no finite test cases:

looping = anyAction >> looping

To prevent test case generation from looping, if a scenario has not terminated after generating 2 * n + 20 actions, where n is when the stopping phase kicks in, generation fails with a Looping error.

By default, Alternative choice (<|>) picks among the next actions with equal probability. So, for instance, this code chooses between the actions a, b and c, with a probability 1/3 of choosing each:

unbiasedChoice a b c = action a <|> action b <|> action c

To change this you can use weight, which multiplies the relative probability of picking a branch by the given number.

For instance, the following scenario picks the action a with probability 2/3 and the action b with probability 1/3:

biasedChoice a b = weight 2 (action a) <|> weight (action b)

Calls to weight need to appear at the top-level after a choice, preceding any actions (action/anyAction) or random generation (forAllQ), or they will have no effect.

Sometimes test case generation should depend on QuickCheck's size parameter. This can be accessed using getSize. For example, anyActions_ is defined by

anyActions_ = do n <- getSize
                 anyActions (n div 2 + 1)

so that we generate a random number of actions, but on average half the size (which is about the same as the average random positive integer, or length of a list).

The monitor function allows you to collect statistics of your testing using QuickCheck functions like label, collect, classify, and tabulate. See also the monitoring method of ContractModel which is called for all actions in a test case (regardless of whether they are generated by an explicit action or an anyAction).

Fail unless the given predicate holds of the model state.

Equivalent to

assertModel msg p = do
  s <- getModelState
  assert msg (p s)

Turn a DL scenario into a QuickCheck property. Generates a random Actions matching the scenario and feeds it to the given property. The property can be a full property running the emulator and checking the results, defined using propRunActions_, propRunActions, or propRunActionsWithOptions. Assuming a model for an auction contract and DL scenario that checks that you can always complete the auction, you can write:

finishAuction :: DL AuctionState ()
prop_Auction  = propRunActions_ handles
  where handles = ...
prop_Finish = forAllDL finishAuction prop_Auction

However, there is also value in a property that does not run the emulator at all:

prop_FinishModel = forAllDL finishAuction $ const True

This will check all the assertions and other failure conditions of the DL scenario very quickly. Once this property passes a large number of tests, you can run the full property checking that the model agrees with reality.