Description

Stochastic models are usually specified in a high-level language such as JANI
https://link.springer.com/chapter/10.1007%2F978-3-662-54580-5_9
http://www-i2.informatik.rwth-aachen.de/pub/index.php?type=download&pub_id=1435
Before being able to analyse properties of such models, they have to be explored. That is, they must be transformed to a low-level description suitable for further analysis. An efficient method to do so is to transform the model to code of a programming language such as C++ or C#. This code can then be compiled and linked. Doing so then allows to compute successors of model states by calling a procedure generated this way.

A recent trend is to enable applications which would traditionally be realised as desktop applications to run in a web browser. This way, end users can use applications without the need to install them first. Being able to do so would also be useful for the area of stochastic model checking. Within others, being able to do so would be useful
- for reviewing purposes, as reviewers would no longer have to download the tool and in the worst case fight with annoying technical difficulties before being able to review a tool, and
- for demonstration of new technologies to colleagues or the general public,
- to avoid having to implement a server backend which requires specific server capabilities (PHP, MySQL, etc.), is sometimes difficult to set up, is often time-consuming to maintain, fragile in case of server configuration changes, and often subject to security issues.

An obstacle here is that it is not practically feasible to compile C++ or similar code in a web browser. This project targets at transforming JANI to AssemblyScript
https://www.assemblyscript.org/
which in turn can be compiled to WebAssembly, which can be run in a browser. The compiler for AssemblyScript can indeed easily be run in a browser.

The exact content of the project could, within others, consist of
- transform JANI models to AssemblyScript and compile to WebAssembly,
- efficient interaction of parts of the application written in Emscripten,
- efficiently storing explored states in data structures (hash tables) even if the size of a state representation is not known until the model exploration starts,
- interactively explore and visualise the low-level state space,
- implement a simple model checker on top of the state space exploration for demonstration purposes.

The default technical setting is such that the tool would be implemented
- in (the already working subset of) C++20,
- using OpenGL/WebGL and the Dear ImGui graphical user interface,
- in a way that both usual C++ compilers can be used to produce a desktop version for Windows, macOS, or Linux,
- as well as Emscripten so as to produce a version of the tool which can run in a browser.
For this setting, the supervisor has already checked the principle feasibility. However, he is also fine if other technical solutions are used, as long as the student is aware that the support might not be as good as for the proposed solution.