Hello Jevitha,
you need to indicate the specification that you want to verify as one TLA+ formula, and the property to be verified by another one. You appear to include the property F ~> G in the specification, hence the model checker will consider all executions that satisfy Spec. Since there are no such executions, Spec => Prop holds for whatever property Prop you may define.
Presumably you meant to define
Spec == Init /\ [][Next]_hr /\ WF_hr(Next)
then enter F ~> G as the (temporal) formula to be verified by TLC.
Regards,
Stephan