[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] Sets and arrays

    while exists v in {v: (u,v) in e, u in r, v not in r}:
      r := r + {v}
I've translated the "exists" by comparing the set S with {}, extracting an element
x using CHOOSE and removing it  using S := S \ { x }
It worked perfectly well and I've completed my algorithm. Thanks to you, Stephan and Leslie.