In this note, we present the first version of the Mona tool to be released in its entirety. The tool now offers decision procedures for both WS1S and WS2S and a completely rewritten front-end. Here, we present some of our techniques, which make calculations couched in WS1S run up to five times faster than with our pre-release tool based on M2L(Str). This suggests that WS1S---with its better semantic properties---is preferable to M2L(Str).
[postscript | BibTeX]