Different commands with different errors (or none!)

[jasagredo]

Say I have some actions which might throw some different errors, or none.

performFoo :: ArgsFoo -> m (Either FooError FooResult)
performBar :: ArgsBar -> m (Either BarError BarResult)
performBaz :: ArgsBaz -> m BazResult

From what I can see in the documentation of q-d, if some actions might return errors, we should define a different type Error instance. I imagine that error should be a combination of all the errors possible in all the commands?

instance StateModel Model where
  type Error Model = Either FooError BarError
  ...

I want to see if my current understanding of how this would be implemented seems correct. Most of the functions here carry a question on how to implement them. It would be nice if the intended usage could be clarified:

instance StateModel Model where
    -- here we don't specify what errors might the actions throw 
    -- as the return of `perform` will be the one declaring those errors
    data Action Model a where
      Foo :: ArgsFoo -> Action Model FooResult
      Bar :: ArgsBar -> Action Model BarResult
      Baz :: ArgsBaz -> Action Model BazResult

  type Error Model = Either FooError BarError

  arbitraryAction = ...

  nextState state (Foo args) _res = -- here we should assume that Foo succeeded?
  nextState state (Bar args) _res = -- same
  nextState state (Baz args) _res = -- as Baz cannot fail, with Baz we will only arrive here, not to `failureNextState`? But _we_ know that, there is nothing in the test that prevents this...

  failureNextState state _ = state -- we don't change the model on failures (this could be defaulted I think?)

  precondition state (Foo args) = -- here we should *ONLY* accept Foo iff it will succeed?
  precondition state (Bar args) = -- same
  precondition state (Baz args) = -- this will always be the case when we run `Baz`? but as said above, _we_ know that, but the test doesn't.

  validFailingAction state (Foo args) = -- here we should *ONLY* accept Foo iff it will fail? or is it fine to accept it regardless of whether it will fail or not?
  validFailingAction state (Bar args) = -- same
  validFailingAction state (Baz args) = -- we know this will never be executed, right?

instance RunModel State m where
   perform = ...

   postcondition (a, b) (Foo args) lookup realized = -- here we should check the postcondition considering that Foo succeeded?
   -- same with Bar, understandable for Baz

   postconditionOnFailure states act lookup (Right v) = postcondition states act lookup v -- is this reasonable?
   postconditionOnFailure (a, b) (Foo args) lookup (Left (Left FooError)) = -- ok I know what to do here, but what about
   postconditionOnFailure (a, b) (Foo args) lookup (Left (Left BarError)) == -- here I should just throw an `error "impossible combination of action+result"`?
   ... -- same for Bar
   postconditionOnFailure (a, b) (Baz args) lookup (Left _) = -- _we_ know baz cannot fail, so what should this do? throw an error?

Disclaimer: I have not tried what is after this line, it might not even be doable.

I wonder if Error could insted be determined by the action that is run, such as:

data Error Model action where
  FooError :: Error Model (Action Model FooResult)
  BarError :: Error Model (Action Model BarResult)

This way, we could define:

postconditionOnFailure :: 
     (state, state) 
  -> Action state a 
  -> Lookup m 
  -> Either (Error state (Action state a)) (Realized m a) 
  -> PostconditionM m Bool

and in the case of Baz, this could not be defined as there exists no BazError :: Error Model (Action Model BazResult). And also for Foo and Bar we know precisely which is the error that could be thrown on each case.

[ghost]

instance StateModel Model where
    -- here we don't specify what errors might the actions throw 
    -- as the return of `perform` will be the one declaring those errors

Yes, the Actions in the model only carry type information about the expected result of the action.
Thus by default, q-d won't generate "erroring" actions

    data Action Model a where
        ....
  type Error Model = Either FooError BarError

Minor comment but I think an actual sum type would be more suited here

  arbitraryAction = ...

  nextState state (Foo args) _res = -- here we should assume that Foo succeeded?
  nextState state (Bar args) _res = -- same

Yes, this expresses the "natural" state transition in the model when the action succeed

  -- as Baz cannot fail, with Baz we will only arrive here, 
  -- not to `failureNextState`? But _we_ know that, there is nothing in the test that prevents this...
  nextState state (Baz args) _res = 

  failureNextState state _ = state -- we don't change the model on failures (this could be defaulted I think?)

Indeed. The logic is that failureNextState is only called when validFailingAction returns true, and the default implementation does not change the state.

  precondition state (Foo args) = -- here we should *ONLY* accept Foo iff it will succeed?
  precondition state (Bar args) = -- same

Yes

  precondition state (Baz args) = -- this will always be the case when we run `Baz`? 
                                                        -- but as said above, _we_ know that, but the test doesn't.

precondition will be called for any Positive action, there's really no concept of errors here. Note that precondition by definition does not depend on the result of the action itself, which should be quite obvious.

  validFailingAction state (Foo args) = -- here we should *ONLY* accept Foo iff it will fail? or is it fine 
                                                                -- to accept it regardless of whether it will fail or not?
  validFailingAction state (Bar args) = -- same
  validFailingAction state (Baz args) = -- we know this will never be executed, right?

validFailingAction will be called iff precondition is false and if true will turn the action into a Negative action, eg. an Action that's expected to trigger an Error in the SUT.

Perhaps things are clearer in the code?

instance RunModel State m where
   perform = ...

   postcondition (a, b) (Foo args) lookup realized = -- here we should check the postcondition considering that Foo succeeded?
   -- same with Bar, understandable for Baz

Same logic than before: postcondition will be called iff the action is Positive and then will be given the result which must not be an error.

   postconditionOnFailure states act lookup (Right v) = postcondition states act lookup v -- is this reasonable?

It might be in your particular case but that seems indicative of a hole in the model. postconditionOnFailure is called iff the action is Negative and is given the actual result of the RunModel execution whether it's an error or not. In general, if you have a Negative action in your model then you should expect and error in the SUT.

   postconditionOnFailure (a, b) (Foo args) lookup (Left (Left FooError)) = -- ok I know what to do here, but what about
   postconditionOnFailure (a, b) (Foo args) lookup (Left (Left BarError)) == -- here I should just throw an `error "impossible combination of action+result"`?
   ... -- same for Bar

Yes, there's no direct link between the Actions defined and the Errors thrown, but that's because the errors are supposed to be errors from the model representing some invalid state which may be triggered by different actions.

   postconditionOnFailure (a, b) (Baz args) lookup (Left _) = -- _we_ know baz cannot fail, so what should this do? throw an error?

Yes, there's no provision to prevent this match as the types are not linked. If your Baz never comes in Negative position, this won't ever be reached. Perhaps we could find a way to express that at the type level to prune matches but I am not sure this is worth the effort.

[ghost]

I think your question highlights the fact we did not do a good job at explaining how this "negative testing" works, I will write some documentation and hopefully examples to better illustrate the ideas behind it.