Web-based version of the SCOOP tool

To experiment with the SCOOP tool without having to actually download it, you can use this web-based version. Just provide a prCRL or MAPA specification in the text area (look here for the syntax of the input language), select the appropriate mode (prCRL or MAPA mode), check the actions you want the tool to take (look here for an explanation), and click 'Generate with SCOOP'. It is also possible to provide the XML specification in PNML format of a GSPN. Then, the GEMMA tool, developed by Rob Bamberg at the University of Twente, is called first to translate this GSPN to a MAPA specification. Details of this translation are explained here.

To compute probabilities or timings of certain events, we provide a direct link to a web-based version of the IMCA tool, developed by Dennis Guck at the RWTH Aachen. This tool can compute unbounded reachability, expected time to reach and long run average for sets of states of Markov Automata (and therefore also of Probabilistic Automata). To apply these methods, use the options on the bottom of the form below and click 'Verify with IMCA'.

To prevent the server from being too busy with one client, it aborts each request after 30 seconds. So, with the web-based version only relatively small state spaces can be generated. To generate state spaces requiring more time, please download the stand-alone version.

(Some example specifications can be found on the page explaining the input language; they can also be loaded automatically by using the drop-down box below.)