Allow running the action sequence from a user supplied initial state

[geo2a]

The runActionsFrom allows specifying an initial annotated state, giving some control to the user of what state to start the execution from.

Motivation

I have a model, in which the initial state depends on some input parameters. As quickcheck-dynamic does not provide a way to specify static configuration, I have to put the parameters into the model state:

data Model = Model {
    mParam :: Maybe Param,
    ...
    mState :: Maybe ModelState -- depends on mParam
    }

As the initialState method of the StateModel class has no parameters, I have to create an explicit InitState action, which will forward the parameter into the model:

data Action Model a where
  InitState :: Param -> QD.Action Model GSM.GsmState

Finally, in the property, I need to:

• either somehow cons an InitState action to the sequence of actions, which I do not think is possible with the current interface of quickcheck-dynamic,
• or run the InitState action separately, obtaining the desired initialised state as output, and then somehow inject it back, which I can only do if I have the runActionFrom function:

prop_model :: Param -> QD.Actions Model -> QC.PropertyM m QC.Property
prop_model param actions = do


  let initStateAction = InitState param
  -- run an 'InitState' action in both the model and system-under-test (SUT)
  (initStateCheck, expected) <- do
    actual <- lift $ QD.perform model initStateAction undefined
    let expected = QD.nextState model initStateAction undefined
    pure (QC.counterexample "initStateCheck (initial model state == initial SUT state)" $
          (mState $ expected) QC.=== actual)

  -- we must use the the model state after executing the `InitState param` action here,
  -- otherwise, if we used `runActions`, the execution will start from
  --   `annotedInitialState`.
  runActionsFrom (QD.Annotated mempty expected) actions

  ...

Discussion

Please let me know if there is a way to achieve what I want using the current interface of quickcheck-dynamic.

I see that there is a PR #83 that solves a similar problem in a more principled way. I would be very happy to use this functionality instead of the runActionsFrom back-door! Are there any plans to merge #83

[ch1bo]

I think we have a similar situation in hydra here:

https://github.com/cardano-scaling/hydra/blob/a53f9d5e1a97f8da2fa03e971ceb280b66ca12a5/hydra-node/test/Hydra/Model.hs#L149-L155

IIRC this model always would generate Seed as the first action of any generated sequence of Actions Model. This is achieved through a Start model state on which we also case in arbitraryAction.

Maybe #83 would address our situation and your situation here.

[geo2a]

Thanks @ch1bo! Yes, #83 would definitely work for me.

[geo2a]

Update: I have noticed that the generateActionsWithOptions function, which is used to generate sequences of actions, unconditionally uses initialAnnotatedState as the state for generating actions. This means that the generated actions will ignore the result of any ad-hoc InitState-style actions, unless the actions generator is invoked explicitly and supplied with the initialised model state. @ch1bo do you know how the Hydra tests you linked above deal with this problem?

[ch1bo]

This means that the generated actions will ignore the result of any ad-hoc InitState-style actions, unless the actions generator is invoked explicitly and supplied with the initialised model state. @ch1bo do you know how the Hydra tests you linked above deal with this problem?

I'm not sure what you mean by "ad-hoc InitState-style actions"? The example I provided works because the generateActionsWithOptions you linked would invoke arbitraryAction using the initialState. In the example model I linked the initialState = Start and it would generate Seed actions while in state Start. This allows us to practically initialize the model using such arbitrary Seed parameters.

I understood your idea to make this first, arguably common step, more easily available by changing initialState :: s to initialState :: Gen s?

[geo2a]

Right, thanks for the explanation @ch1bo! Indeed, I see that in the example you're linking too the scenario I described indeed does not create problems. I was too attached to the example I'm working on, where states are a record type, and some of the record components are initialised by a dedicated action, similar to the Seed one in your example.