[nprescott]

While I haven't used DSLabs, I did suffer a similar bit of indecision recently trying to decide between Alloy[0] and TLA+[1]. In the end I don't think there is a correct answer, and there are probably more similarities than differences between any two specification languages. In my case I read both Software Abstractions and Specifying Systems (part 1 at least). Each took about a week; which is probably less time than I spent trying to decide between them.

I happen to agree with the argument made by proponents of both TLA+ and Alloy that model checking and specification is better accomplished when detached from an implementation language, but I think you would benefit most from simply starting with one of them (DSLabs or TLA+) and decide later if you'd like to learn the other.

[0]: http://alloytools.org/

[1]: https://lamport.azurewebsites.net/tla/tla.html

[RBerenguel]

I started learning TLA+ in October (or so), and after getting reasonably acceptable (as in, can write PlusCal without many issues, and can write and read basic plain TLA+) I'm starting to learn Alloy now. It offers a different approach that seems to suit different domains (say, less "temporal" focus)