{- reachability problems -}

data RVal = RVal { rch :: Bool } deriving (Eq, Show)

reAll g =
  let init v = RVal (vid v == 1) ;
      step v prev curr =
        let newrch = prev v .^ rch || or [ prev u .^ rch | (e,u) <- is v ]
        in RVal newrch
  in fregel init step Fix g

re3 g =
  let init v = RVal (vid v == 1) ;
      step v prev curr =
        let newrch = prev v .^ rch || or [ prev u .^ rch | (e,u) <- is v ]
        in RVal newrch
  in fregel init
            step
            (Until (\g -> sum [ 1 | u <- g, val u .^ rch ] > 3))
            g