Please wait while the Java applet for checking your model is being loaded.
Be advised that this may take a while, and can render your browser unstable.
But other than that, enjoy :)
By the way, you'll probably need a Java plugin to run this part.
Alternatively, you can export the SMV file and download a console
appliation to check realizability from github.com/jopsen/LiveSC
LiveSC is a web application for drawing and checking realizability of live sequence chart specifications. For more information on LiveSC have a look at our github project, where you will also find links to our paper on the subject, which formally presents the subset of live sequence charts consider here.
Below you will find a brief introduction to this application.