satStatesAF :: Model -> CtlFormula -> Set State
satStatesAF m f = satStatesAF' (satStates m f)
  where
    satStatesAF' :: Set State -> Set State
    satStatesAF' s = let new_s = s `union` preAll m s in
                             if Set.size s == Set.size new_s
                             then new_s
                             else satStatesAF' new_s

satStatesEU :: Model -> CtlFormula -> CtlFormula -> Set State
satStatesEU m f1 f2 = satStatesEU' (satStates m f2)
  where
    x = (satStates m f1)
    satStatesEU' :: Set State -> Set State
    satStatesEU' y = let new_y = y `union` preEx m (y `intersection` x)  in
                             if Set.size y == Set.size new_y
                             then new_y
                             else satStatesEU' new_y