In addressing the problem of the (in)compatibility of divine foreknowledge and human freedom, philosophers of religion encounter problems regarding the metaphysics and structure of time. Some models of temporal logic developed for completely independent reasons have proved especially appropriate for representing the temporal structure of the world as Molinism conceives it. In particular, some models of the Thin Red Line (TRL) seem to imply that some conditionals of freedom are true or false, as Molinists maintain. Noting the resemblance between Molinism and TRL models, Restall (2011) has advanced some criticisms of Molinism that have also been leveled against TRL models. In particular, Restall believes that the implication p implies PFp is not true in TRL models. Because Molinists must also accept that this implication is not true, this is a problem for them. I will show that Restall's criticism is wide of the mark. Firstly, it will be demonstrated that in most open future models (not just TRL) the problematic implication p implies PFp is invalid. Secondly, while it is possible to account for this implication, some modifications are required in respect of the branching time semantics. In proposing one such modification, I show that this new semantics can be adopted by advocates of the TRL and, as a consequence, by Molinists as well. I conclude that the principle stated by Restall is either a problem for many open future models (not just for Molinists) or can be accounted for by these models and so is not a problem for Molinists either.