Make dependent actions shrink

[MaximilianAlgehed]

In situations like this:

do var0 <- action $ Deploy
   var1 <- action $ Step var0
   var2 <- action $ Step var1
   var3 <- action $ Step var2

Where Step varX makes X unuseable in a future action (it consumes the input) you run into trouble when trying to shrink away Step var0, Step var1 because shrinking var3 to var0 is not valid.

To get around this one could shrink the sequence to something like this:

do var0 <- action $ Deploy
   var1 <- action $ Step var0
   var2 <- pure var1
   var3 <- action $ Step var2

which would allow two-step shrinking of var3 to var0 via var2 and var1.

[MaximilianAlgehed]

I tried this out today and it unfortunately doesn't work as well as one would like. The model can have a precondition like "the variable is the output of the last action that modified the state" - which would mean that var2 would be invalid in the final step. Here is a model that demonstrates that problem:

data Resource = MyResource
  deriving Generic
data State = State { theResource :: Maybe (Var Resource) }
  deriving (Show, Eq, Generic)

instance HasVariables (Action State a) where
  getAllVariables Init = mempty
  getAllVariables (UseLinearly v) = getAllVariables v
  getAllVariables (UseLinearlyBadly v) = getAllVariables v

deriving instance Eq (Action State a)
deriving instance Show (Action State a)

instance StateModel State where
  data Action State a where
    Init :: Action State Resource
    UseLinearly :: Var Resource -> Action State Resource
    UseLinearlyBadly :: Var Resource -> Action State Resource

  precondition s Init                 = isNothing (theResource s)
  precondition s (UseLinearly v)      = theResource s == Just v
  precondition s (UseLinearlyBadly v) = theResource s == Just v

  arbitraryAction _ (State Nothing) = pure $ Some Init
  arbitraryAction _ (State (Just r)) =
    elements [Some $ UseLinearly r, Some $ UseLinearlyBadly r ]

  initialState = State Nothing

  nextState _ Init v               = State (Just v)
  nextState _ UseLinearly{} v      = State (Just v)
  nextState _ UseLinearlyBadly{} v = State (Just v)

instance RunModel State Identity where
  perform _ Init _               = pure MyResource
  perform _ UseLinearly{} _      = pure MyResource
  perform _ UseLinearlyBadly{} _ = pure MyResource

  postcondition _ UseLinearlyBadly{} _ _ = pure False
  postcondition _ _ _ _ = pure True

prop_State :: Actions State -> Property
prop_State s =
  monadic runIdentity $ do
    runActions s
    assert True

Here you get counterexamples like:

var1 <- action $ Init
var2 <- action $ UseLinearly var1
var3 <- action $ UseLinearly var2
action $ UseLinearlyBadly var3

That fail to shrink. You would think that by adding UseLinearly var1 -> pure var1 as a shrinking step you would be able to shrink it down to:

var1 <- action $ Init
var2 <- pure var1
var3 <- pure var2
action $ UseLinearlyBadly var3

Which in turn would shrink down to action Init >>= action . UseLinearlyBadly. But this doesn't work because the variable var3 is not equal to var1 so the precondition for UseLinearlyBadly fails - meaning we never go via the intermediary step of replacing UseLinearly with pure.

[MaximilianAlgehed]

The other solution to this problem is to shrink var1 <- SomeAction var0; trace to trace[var0/var1], basically getting rid of the action and the variable at the same time. However, to implement this one would need substitution for the actions.

Two ways of doing substitution that we've discussed in the last couple of days:

class HasVariables a where
  subst :: Var b -> Var b -> a -> a
  getAllVariables :: a-> Set (Some Var)

and

class HasVariables a where
  getAllVariables :: a -> Set (Some (VarLens a))

newtype VarLens a b = VarLens (Lens' a (Var b))

The second option has the benefit that the user doesn't need to implement the substitution themselves for many types, but the downside is that one needs to make lenses for all the variables instead. Either way I don't like any of these solutions very much...