Model Checking, Tla Plus, TLC, Java, Concurrency.
nondeterministically: some thread is removed from the wait set, but we don’t specify which one (and neither does the Java Language Specification). Using these Java-like operators, the module continues with a formalization of the put and get methods. The TLA+ formulation mimics the Java code and is