LiveSC is web-based live sequence chart editor that can check for realizability, given a set of charts with environment and system instance lines.
Realizability is checking using symbolic model checking with JTLV running as a Java applet. This currently causes LiveSC to be fairly slow, and due to the poor integration of Java in modern browsers occationally requires the user to kill a few process.
In its current state the code is still fairly unpolished, and this merly serves as a proof of concept. An online test version of LiveSC can be found here.
LiveSC is written in coffeescript, and a Cakefile
for building can be located in the repository root.
To build the applet you'll need a Scala compiler, Java compiler and GNU Make.
The relevant makefile
can be located in the applet/
folder of the repository.
- LiveSC is licensed under GNU GPL.
- Rapheal icons by Dmitry Baranovskiy are MIT.
- JTLV is GNU (L)GPL.
- JavaBDD is also GNU (L)GPL.
- ANTLR is under the ANTLR 3 License.
- IcedTea-Web is GNU GPL.
- Raphael.Export by Elbert Foo is MIT licensed.
- Raphaël is also MIT.
- jquery-json is MIT.
- jquery.base64 is GNU GPL.
- jquery is MIT.
- JDD is zlib license.
- Jonas Finnemann Jensen
- Lars Kærlund Østergaard
- Lisa Fontani
- Daniel Ejsing-Duun