Thanks for your reply. I have solve the problem. With the help of Java, things become more convenient.
But unfortunately, I encountered some difficulties again, and I don’t know if there is a solution. Could you give me some advice?
As I mentioned before, I want to enumerate all possible event structure satisfying partial order.
But the raw method by enumerating all subsets and judging them is of a great time complexity.
Everything seemed to be going well, however, something unexpected happened.
What bad news ! I understand that this design makes a certain sense, but a question raises that as follows.
Suppose a set s = {1,2,3,4,5,6,7,8} and we calculate subset SUBSET (s \X s), what is the behavior of TLA+? Out of bound too? Or there is an iterator-like operation?
I know my question is a bit strange. But if you are interested, looking forward to your early relpy.
Sincerely
Ouyang