Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

merge main into my branch #12

Merged
merged 6 commits into from
Jul 2, 2024
Merged

merge main into my branch #12

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
1472ac7
Added action visualization
YouGuessedMyName Jun 28, 2024
9957257
Improved action visualization
YouGuessedMyName Jul 1, 2024
be0793e
Add study MDP example.
YouGuessedMyName Jul 1, 2024
9df743e
Add study MDP example comments.
YouGuessedMyName Jul 1, 2024
35c8782
Add test for stormpy to stormvogel
glatteis Jul 2, 2024
23071c9
Merge branch 'main' of github.com:moves-rwth/stormvogel
glatteis Jul 2, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
82 changes: 82 additions & 0 deletions examples/stormpy_to_stormvogel.py
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,82 @@
import stormpy # type: ignore


def example_building_dtmcs_01():
# Use the SparseMatrixBuilder for constructing the transition matrix
builder = stormpy.SparseMatrixBuilder(
rows=0,
columns=0,
entries=0,
force_dimensions=False,
has_custom_row_grouping=False,
)

# New Transition from state 0 to target state 1 with probability 0.5
builder.add_next_value(row=0, column=1, value=0.5)
builder.add_next_value(0, 2, 0.5)
builder.add_next_value(1, 3, 0.5)
builder.add_next_value(1, 4, 0.5)
builder.add_next_value(2, 5, 0.5)
builder.add_next_value(2, 6, 0.5)
builder.add_next_value(3, 7, 0.5)
builder.add_next_value(3, 1, 0.5)
builder.add_next_value(4, 8, 0.5)
builder.add_next_value(4, 9, 0.5)
builder.add_next_value(5, 10, 0.5)
builder.add_next_value(5, 11, 0.5)
builder.add_next_value(6, 2, 0.5)
builder.add_next_value(6, 12, 0.5)

# Add transitions for the final states
for s in range(7, 13):
builder.add_next_value(s, s, 1)

# Build matrix
transition_matrix = builder.build()
print(transition_matrix)

# State labeling
state_labeling = stormpy.storage.StateLabeling(13)

# Add labels
labels = {"init", "one", "two", "three", "four", "five", "six", "done", "deadlock"}
for label in labels:
state_labeling.add_label(label)

# Set label of state 0
state_labeling.add_label_to_state("init", 0)
print(state_labeling.get_states("init"))

# Set remaining labels
state_labeling.add_label_to_state("one", 7)
state_labeling.add_label_to_state("two", 8)
state_labeling.add_label_to_state("three", 9)
state_labeling.add_label_to_state("four", 10)
state_labeling.add_label_to_state("five", 11)
state_labeling.add_label_to_state("six", 12)

# Set label 'done' for multiple states
state_labeling.set_states("done", stormpy.BitVector(13, [7, 8, 9, 10, 11, 12]))
print(state_labeling)

# Reward models:
reward_models = {}
# Create a vector representing the state-action rewards
action_reward = [1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0]
reward_models["coin_flips"] = stormpy.SparseRewardModel(
optional_state_action_reward_vector=action_reward
)

components = stormpy.SparseModelComponents(
transition_matrix=transition_matrix,
state_labeling=state_labeling,
reward_models=reward_models,
)

dtmc = stormpy.storage.SparseDtmc(components)

print(dtmc)


if __name__ == "__main__":
example_building_dtmcs_01()
223 changes: 90 additions & 133 deletions notebooks/die.ipynb
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,145 +1,102 @@
{
"cells": [
{
"cell_type": "code",
"execution_count": 1,
"metadata": {},
"outputs": [],
"source": [
"import stormvogel.model\n",
"import stormvogel.visualization"
]
},
{
"cell_type": "code",
"execution_count": 2,
"metadata": {},
"outputs": [],
"source": [
"# Create a new model with the name \"Die\"\n",
"dtmc = stormvogel.model.new_dtmc(\"Die\")\n",
"\n",
"init = dtmc.get_initial_state()\n",
"\n",
"# From the initial state, add the transition to 6 new states with probability 1/6th.\n",
"init.set_transitions(\n",
" [(1 / 6, dtmc.new_state(f\"rolled{i}\", {\"rolled\": i})) for i in range(6)]\n",
")\n",
"\n",
"# Print the resulting model in dot format.\n",
"# print(dtmc.to_dot())"
]
},
{
"cell_type": "code",
"execution_count": 3,
"metadata": {
"scrolled": true
},
"outputs": [
"cells": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"diegraph.html\n"
]
"cell_type": "code",
"execution_count": 1,
"metadata": {},
"outputs": [],
"source": [
"import stormvogel.model\n",
"import stormvogel.visualization"
]
},
{
"data": {
"text/html": [
"\n",
" <iframe\n",
" width=\"100%\"\n",
" height=\"600px\"\n",
" src=\"diegraph.html\"\n",
" frameborder=\"0\"\n",
" allowfullscreen\n",
" \n",
" ></iframe>\n",
" "
],
"text/plain": [
"<IPython.lib.display.IFrame at 0x7ff90d17b510>"
"cell_type": "code",
"execution_count": 2,
"metadata": {},
"outputs": [],
"source": [
"# Create a new model with the name \"Die\"\n",
"dtmc = stormvogel.model.new_dtmc(\"Die\")\n",
"\n",
"init = dtmc.get_initial_state()\n",
"\n",
"# From the initial state, add the transition to 6 new states with probability 1/6th.\n",
"init.set_transitions(\n",
" [(1 / 6, dtmc.new_state(f\"rolled{i}\", {\"rolled\": i})) for i in range(6)]\n",
")\n",
"\n",
"# Print the resulting model in dot format.\n",
"# print(dtmc.to_dot())"
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"stormvogel.visualization.show(model=dtmc, name=\"diegraph\")"
]
},
{
"cell_type": "code",
"execution_count": 4,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"hi.html\n"
]
},
{
"data": {
"text/html": [
"\n",
" <iframe\n",
" width=\"100%\"\n",
" height=\"600px\"\n",
" src=\"hi.html\"\n",
" frameborder=\"0\"\n",
" allowfullscreen\n",
" \n",
" ></iframe>\n",
" "
"cell_type": "code",
"execution_count": 3,
"metadata": {
"scrolled": true
},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"diegraph.html\n"
]
},
{
"data": {
"text/html": [
"\n",
" <iframe\n",
" width=\"100%\"\n",
" height=\"600px\"\n",
" src=\"diegraph.html\"\n",
" frameborder=\"0\"\n",
" allowfullscreen\n",
" \n",
" ></iframe>\n",
" "
],
"text/plain": [
"<IPython.lib.display.IFrame at 0x7efdc3cc9010>"
]
},
"metadata": {},
"output_type": "display_data"
}
],
"text/plain": [
"<IPython.lib.display.IFrame at 0x7ff90ec3a110>"
"source": [
"stormvogel.visualization.show(model=dtmc, name=\"diegraph\")"
]
},
"execution_count": 4,
"metadata": {},
"output_type": "execute_result"
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": []
}
],
"metadata": {
"kernelspec": {
"display_name": "Python 3 (ipykernel)",
"language": "python",
"name": "python3"
},
"language_info": {
"codemirror_mode": {
"name": "ipython",
"version": 3
},
"file_extension": ".py",
"mimetype": "text/x-python",
"name": "python",
"nbconvert_exporter": "python",
"pygments_lexer": "ipython3",
"version": "3.11.2"
}
],
"source": [
"from pyvis.network import Network\n",
"\n",
"g = Network(notebook=True,cdn_resources=\"remote\")\n",
"g.show_buttons()\n",
"g.show(\"hi.html\")"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": []
}
],
"metadata": {
"kernelspec": {
"display_name": "Python 3 (ipykernel)",
"language": "python",
"name": "python3"
},
"language_info": {
"codemirror_mode": {
"name": "ipython",
"version": 3
},
"file_extension": ".py",
"mimetype": "text/x-python",
"name": "python",
"nbconvert_exporter": "python",
"pygments_lexer": "ipython3",
"version": "3.11.2"
}
},
"nbformat": 4,
"nbformat_minor": 4
"nbformat": 4,
"nbformat_minor": 4
}
Loading
Loading