FOXAssert(FOXForAll(FOXTuple(FOXInteger(), FOXInteger()), ^BOOL(NSArray *values){
    NSInteger x = [tuple[0] integerValue];
    NSInteger y = [tuple[1] integerValue];
    return x + y > x;
});

// define a state machine. Model state is the state of your application and
// can be represented with any object you want -- Fox does not interpret it.
FOXFiniteStateMachine *stateMachine = [[FOXFiniteStateMachine alloc] initWithInitialModelState:@[]];

// Adds a transition to the state machine:
// - The API to test is -[addObject:]
// - The generator for the argument is a random integer in an NSNumber
// - A block indicating how to update the model state. This should not mutate the original model state.
[stateMachine addTransition:[FOXTransition byCallingSelector:@selector(addObject:)
                                               withGenerator:FOXInteger()
                                              nextModelState:^id(NSArray *modelState, id generatedValue) {
    return [modelState arrayByAddingObject:generatedValue];
}]];
// Add a custom transition (see FOXStateTransition protocol)
[stateMachine addTransition:[[QueueRemoveTransition alloc] init]];

// Generate a sequence of commands executed on the given subject. Since
// this will generate multiple tests, you also give a block of a subject.
id<FOXGenerator> executedCommands = FOXExecuteCommands(stateMachine, ^id {
    return [FOXQueue new];
});

// Verify if the executed commands validated the API conformed to the state machine.
FOXRunnerResult *result = [FOXSpecHelper resultForAll:executedCommands
                                                 then:^BOOL(NSArray *commands) {
    return FOXExecutedSuccessfully(commands);
}];
// result will shrinking to the small sequence of API calls to trigger the
// failure if there is one