Op-based counter (op_counter.tla), Observed-Remove Set (or_set.tla) and Last-Writer-Wins Register (lww_register.tla) from the Research Report A comprehensive study of Convergent and Commutative Replicated Data Types. by Marc Shapiro, Nuno Preguiça, Carlos Baquero and Marek Zawirski.
To execute this specification is necessary the TLA+ Toolbok, available in http://lamport.azurewebsites.net/tla/toolbox.html.