Random generation of initial states

[MaximilianAlgehed]

This introduces two changes:

initialState :: Gen state instead of initialState :: state and a new callback setup :: state -> m () to RunModel.

Checklist:

• Check source-code formatting is consistent

[rjmh]

An alternative way to do this is to let the state be a Maybe type, initially Nothing, and define a Setup action (with appropriate parameters) whose precondition is that the state is Nothing. The cost is that all other preconditions have to check for Just, as do nextState, postcondition etc. This is a recurring need, so I'm sure people would use it, but it does make the API a bit more complex, for something that is easy to do already. My inclination would probably be not to add this, although I can see arguments in favour too.

[MaximilianAlgehed]

This PR is precisely meant to address this clunkyness in the current design. Almost everyone ends up needing to do what you describe and it's always ugly one way or another.

The API in the PR on the other hand imposes minimal overhead if you don't use it (just write pure MyState{..} instead of MyState{..} in one place) and avoids all this clunkyness of having to encode the "have I gone through the setup stage yet" in the precondition and nextState for every action in the model.

[ghost]

The proposal makes sense, just have a couple of comments on possible improvements to the code

[MaximilianAlgehed]

There is one design decision left here that we need to discuss and that's how to deal with initial states in DL. Currently the low-level DL functionality punts on this and has you provide an initial state in your property while the monadic forAllDL interface generates an initial state for you from the initialState generator in the state model. Ideally we would change the interface to require you to provide an initial state everywhere, but at the same time that seems clunky. Should we have the "use the built-in generator" and the "run in this particular state" interfaces side-by-side perhaps?

[ghost]

we would change the interface to require you to provide an initial state everywhere

If one defines an initialState generator then why would you want to use a specific initial state for some DL formula and not all? What would be the use case?

[MaximilianAlgehed]

The best example would be "when the initial state is drawn from this distribution, I expect this property to hold". E.g. when the protocol parameter for some delay is 0, we expect something to always happen immediately. That would be nice to express as a DL property I think?

[ghost]

But then, it seems to me I could rather express that directly in the DL formula and have a special action initialising the system with some specific values.

[MaximilianAlgehed]

Indeed, but mixing that with a random initialState would be messy!

[ghost]

Hence why I am starting to have doubts about the value of this change. WDYT @bwbush?

[MaximilianAlgehed]

The initializing action is clunky in one direction, this is clunky in a different direction. I tend to prefer this design but let's think more carefully about what we want to be able to do on the DL side.

You're saying that you want to be able to say action $ Init ... but what if there was something like init :: state -> DL state () that only worked in the beginning of a DL run (i.e. implementing what you would have to implement by hand in Init's precondition)?

[ghost]

Would you need to construct and pass explicitly state to init? Or is init not a combinator from the DL language? How would that look like? I think we came here because of some need that surfaced from Peras project, hence why I would be interested in @bwbush's insights

[MaximilianAlgehed]

Yes, you would. However, you would turn:

instance StateModel (Maybe MyState)
  initialState = Nothing

someDLThing :: DL (Maybe MyState) ()
someDLThing = do
  action $ Init ExplicitlyConstructedState{...}
  ...

into

instance StateModel MyState
  initialState = myStateGenerator

someDLThing :: DL MyState ()
someDLThing = do
  init ExplicitlyConstructedState{...}
  ...

Or some variant of this where the original model doesn't have the explicit Maybe part that John is talking about.

Anyway, note that the de# the PR can incorporate both of these techniques (given that we implement init) while the old design forces the clunky Init action way of doing things.

This is not a Peras-only problem. It appears in Peras, but the Init :: MyState -> Action MyState () pattern of variants of it have appeared in lots of places before.

[ghost]

I agree the pattern of having an Init :: ... specific action appeared elsewhere. Actually, I myself have used it in 100% of the q-d models I have written :) However, is this really a problem? Having initialState :: Gen State is symmetric to data Actions State a where Init :: State -> Action State () and for the user to recover control when they want, we need to introduce an additional init combinator to DL language.
I am not sure what we really gain, hence why I would be interested in having more users chime in.
That said, if you think there's value in moving in that direction, please go ahead :)

[MaximilianAlgehed]

It's not quite symmetric for two reasons:

1. With the Gen State approach you can still recover the old approach if you want to, while the opposite is not quite true because
2. The Init approach requires your state to have some flag for "I have not yet been initialised" that you either have to check in every actions precondition or generator, which you don't need to check in the Gen State approach because that's taken care of for you.

[ghost]

Fair enough. But while argument 2. is true, it seems to me most (all?) interesting generators and preconditions would require pattern matching or checking the state anyway. Removing one check for one specific, albeit arguably important, state does not seem to bring that much value.
But like I said, I trust your judgment.