Skip to content

Commit 96a46eb

Browse files
linushecklinusheck
authored
Merge pull request #7 from stormchecker/examples
Examples
2 parents f55affc + 68f63d2 commit 96a46eb

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

54 files changed

+3974
-1209
lines changed

‎.github/workflows/playwright.yml‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -79,6 +79,11 @@ jobs:
7979
run: |
8080
echo "Downloading stormvogel image..."
8181
docker pull stormvogel/stormvogel
82+
83+
- name: Generate secret key
84+
run: |
85+
python3 -c "import secrets; print(f'FLASK_SECRET_KEY=\"{secrets.token_urlsafe(32)}\"')" > .env
86+
working-directory: ./backend
8287

8388
- name: Run Playwright tests
8489
run: npx playwright test

‎README.md‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -123,5 +123,5 @@ This project is licensed under the [GPL-3.0 license](LICENSE).
123123
124124
## 🔗 Links
125125
- Storm model checker: [Storm](https://www.stormchecker.org/)
126-
- Stormpy python bindings: [Stormpy](https://github.com/moves-rwth/stormpy)
127-
- Stormvogel: [Stormvogel](https://github.com/moves-rwth/stormvogel)
126+
- Stormpy python bindings: [Stormpy](https://github.com/stormchecker/stormpy)
127+
- Stormvogel: [Stormvogel](https://github.com/stormchecker/stormvogel)

‎backend/resources/playground.py‎

Lines changed: 48 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,48 @@
1+
# Playground utility functions
2+
import stormvogel
3+
import base64
4+
import os
5+
import io
6+
import matplotlib.figure
7+
8+
def show(something: any, something_other: any = None) -> str:
9+
"""
10+
Convert the input to HTML for display in the playground.
11+
"""
12+
def add_doctype(html: str) -> str:
13+
"""Add a doctype to the HTML string."""
14+
return f"<!DOCTYPE html>\n<html>{html}</html>"
15+
16+
if isinstance(something, stormvogel.Model):
17+
vis = stormvogel.show(something, something_other, do_init_server=False)
18+
print(vis.generate_html())
19+
elif str(type(something)).startswith("<class 'stormpy.storage.storage.Sparse"):
20+
import stormvogel.stormpy_utils.mapping as mapping
21+
import stormvogel.stormpy_utils.convert_results as convert_results
22+
23+
stormvogel_model = mapping.stormpy_to_stormvogel(something)
24+
stormvogel_result = None
25+
if something_other is not None:
26+
stormvogel_result = convert_results.convert_model_checking_result(stormvogel_model, something_other)
27+
vis = stormvogel.show(stormvogel_model, stormvogel_result, do_init_server=False)
28+
print(vis.generate_html())
29+
elif isinstance(something, str) and os.path.isfile(something):
30+
ext = os.path.splitext(something)[1].lower()
31+
if ext in [".png", ".gif", ".jpg", ".jpeg"]:
32+
with open(something, "rb") as img_file:
33+
encoded = base64.b64encode(img_file.read()).decode("utf-8")
34+
mime = "image/png" if ext == ".png" else "image/gif" if ext == ".gif" else "image/jpeg"
35+
html = f'<img src="data:{mime};base64,{encoded}" />'
36+
print(add_doctype(html))
37+
elif (hasattr(something, "figure") and callable(getattr(something, "figure", None))) or isinstance(something, matplotlib.figure.Figure):
38+
import matplotlib.pyplot as plt
39+
fig = something.figure if hasattr(something, "figure") else something
40+
buf = io.BytesIO()
41+
fig.savefig(buf, format="png", bbox_inches="tight")
42+
buf.seek(0)
43+
encoded = base64.b64encode(buf.read()).decode("utf-8")
44+
html = f'<img src="data:image/png;base64,{encoded}" />'
45+
print(add_doctype(html))
46+
plt.close(fig)
47+
else:
48+
raise RuntimeError(f"I don't know how to display {something} of type {type(something)}.")

‎backend/sandbox.py‎

Lines changed: 8 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -97,10 +97,10 @@ def separate_html(text):
9797
return html_content, non_html_content
9898

9999
# Write code to a temporary file and send that to the container
100-
def write_to_file(code, container):
100+
def write_to_file(filename, code, container):
101101
tarstream = io.BytesIO()
102102
with tarfile.TarFile(fileobj=tarstream, mode="w") as tar:
103-
tarinfo = tarfile.TarInfo("script.py")
103+
tarinfo = tarfile.TarInfo(filename)
104104
tarinfo.size = len(code.encode())
105105
tar.addfile(tarinfo, io.BytesIO(code.encode()))
106106

@@ -130,7 +130,12 @@ def execute_code(user_id, code):
130130

131131
logger.debug(f"Executing code for {user_id}: {repr(code)}")
132132

133-
write_to_file(code, container)
133+
write_to_file("script.py", code, container)
134+
135+
# Read the content from resources/playground.py and write it into the container
136+
with open("resources/playground.py", "r", encoding="utf-8") as f:
137+
playground_code = f.read()
138+
write_to_file("playground.py", playground_code, container)
134139

135140
# Container.exec_run does not have an timeout, so we use subprocess here
136141
# exec_result = container.exec_run(

0 commit comments

Comments
 (0)