Replace Vector and Stack classes in tla2sany.utilities package with their java.util equivalents

[tautomaton]

Fixed #86

[tautomaton]

I think this line is just saying that there was no line break after this closing brace previously and my editor added it automatically. I'm trying to keep a clean diff on this PR, but I'm inclined not to revert this change. Let me know if you disagree.

[lemmy]

We are currently putting the finish touches on the 1.6.0 release. I will look into this afterwards.
@tautomaton Do you have specifics for why you consider the java.util classes superior?

[tautomaton]

Sure. I figured I could pick off some easy issues as a way to learn more about the implementation of the TLAToolbox.

In general, I figure using the standard library is (almost) always superior. In detail, my rationale for standardizing on the java.util implementations:

• Richer API that java.util.Vector inherits from it superclasses, and which will be updated to make use of new language features. E.g. range-based iteration, forEach and Consumers, etc.
• Better documentation. https://docs.oracle.com/javase/10/docs/api/java/util/Vector.html would be pretty hard to top for any hand-rolled class.
• Allows the removal of a duplicate, and therefore reduction of cognitive load. If the problem is that tla2sany.utilities.Vector and java.util.Vector both exists and serve similar purposes, the only permanent fix is to remove the custom one, since java.util.Vector isn't going away. Even if we remove its use now it can always creep back in.
• java.util.Vector is synchronized. This may actually be a drawback or a plus, depending on how concurrency is handled. In some cases, ArrayList or even an immutable/unmodifiable list implementation may be better for performance and resource use.

[tautomaton]

Any updates on the readiness of this PR?

[lemmy]

Will look into it once https://github.com/tlaplus/tlaplus/milestone/6 is out of the door.

[lemmy]

Related #86

[tautomaton]

Sure, I'll follow along. Would you like me to rebase this branch once that milestone is finished?

[lemmy]

@tautomaton Have you considered that java.util.Vector is synchronized whereas tla2sany.utilities.Vector is not?

[tautomaton]

Yeah, that's called out in the fourth bullet of my comment on June 16.

My thinking is

1. Some fraction of the Vectors in use are already the synchronized java.util.Vector, and this didn't seem to cause any issue
2. If the synchronization is deemed to be too big a performance hit, https://docs.oracle.com/javase/10/docs/api/java/util/Vector.html recommends using ArrayList instead. ArrayList also enjoys the same benefits as the first three bullets my comment above.

[tautomaton]

Any remaining concerns?

[tautomaton]

Friendly ping. I've got work based on this which I can create PRs for.

If the synchronization is a concern, I can replace java.util.Vector (which is rather old) with java.util.ArrayList. Just let me know.

[lemmy]

@tautomaton What is it you are working on? As per the guide it is best to first discuss contributions.

[tautomaton]

Sure thing, just other cleanups from the list of FRs. Nothing big, if that's a concern.

[tautomaton]

Eventually, once I get some familiarity with the code and the process of submitting to this project, I'd like to tackle "Improved runtime API for TLC (difficulty: moderate) (skills: Java)" listed on the contributions page you link.

[tautomaton]

But please do let me know if this particular PR has any changes that are needed.

[alygin]

@tautomaton , beware of the difference in semantics of the contains() implementations. The toolbox Vector uses reference comparison, while the standard Vector uses equals(). So, such mechanical substitution of one implementation to another may change the program behaviour.

BTW, such difference might also be a source of some subtle bugs in places where Vector.contains() and Vector.appendNoRepeats() are used at the moment. No proof of existence of such bugs, though, just my thoughts. cc @lemmy