Model Checking, Tla Plus, TLC, Java, Concurrency.
programming language like Java. In particular, one can write nondeterministic actions (like the last two above for which, given x, there are several possible values of x'), which are very useful in modeling concurrent systems. With this in mind, it is now possible to decipher the TLA+ formulations