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

137 state builder #173

Merged
merged 10 commits into from
Dec 22, 2024
Merged

137 state builder #173

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
10 commits
Select commit Hold shift + click to select a range
2a2bc90
pgc works for the simple example
PimLeerkes Nov 30, 2024
17a443c
wrote first test for mdp pgc
PimLeerkes Nov 30, 2024
efd58f9
it works for dtmcs + changed how labels and features work in pgc
PimLeerkes Nov 30, 2024
9a5d267
pgc state object can now contain arbitrary attributes
PimLeerkes Dec 8, 2024
072c6cb
model builder now also uses reward function
PimLeerkes Dec 8, 2024
c339a8d
model builder can now also use a labels function
PimLeerkes Dec 8, 2024
ddd0342
model builder supports multiple reward models
PimLeerkes Dec 8, 2024
b441cd2
small changes
PimLeerkes Dec 22, 2024
214f724
merge main
PimLeerkes Dec 22, 2024
081efbe
commented out pgc tests
PimLeerkes Dec 22, 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
80 changes: 62 additions & 18 deletions docs/getting_started/04_mdp.ipynb
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@
},
{
"cell_type": "code",
"execution_count": 2,
"execution_count": 1,
"metadata": {},
"outputs": [],
"source": [
Expand All @@ -19,16 +19,16 @@
},
{
"cell_type": "code",
"execution_count": 3,
"execution_count": 2,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"<stormpy.storage.storage.PrismProgram at 0x7f70bcd3d530>"
"<stormpy.storage.storage.PrismProgram at 0x7f6c38d21f70>"
]
},
"execution_count": 3,
"execution_count": 2,
"metadata": {},
"output_type": "execute_result"
}
Expand Down Expand Up @@ -132,7 +132,7 @@
},
{
"cell_type": "code",
"execution_count": 4,
"execution_count": 3,
"metadata": {},
"outputs": [],
"source": [
Expand All @@ -142,7 +142,7 @@
},
{
"cell_type": "code",
"execution_count": 5,
"execution_count": 4,
"metadata": {},
"outputs": [
{
Expand Down Expand Up @@ -174,7 +174,7 @@
},
{
"cell_type": "code",
"execution_count": 6,
"execution_count": 5,
"metadata": {},
"outputs": [],
"source": [
Expand All @@ -183,7 +183,7 @@
},
{
"cell_type": "code",
"execution_count": 7,
"execution_count": 6,
"metadata": {},
"outputs": [],
"source": [
Expand All @@ -192,7 +192,7 @@
},
{
"cell_type": "code",
"execution_count": 8,
"execution_count": 7,
"metadata": {},
"outputs": [
{
Expand All @@ -209,7 +209,7 @@
},
{
"cell_type": "code",
"execution_count": 9,
"execution_count": 8,
"metadata": {},
"outputs": [
{
Expand Down Expand Up @@ -239,7 +239,7 @@
},
{
"cell_type": "code",
"execution_count": 10,
"execution_count": 9,
"metadata": {},
"outputs": [
{
Expand All @@ -261,7 +261,7 @@
},
{
"cell_type": "code",
"execution_count": 11,
"execution_count": 10,
"metadata": {
"scrolled": true
},
Expand All @@ -274,7 +274,7 @@
},
{
"cell_type": "code",
"execution_count": 12,
"execution_count": 11,
"metadata": {
"scrolled": true
},
Expand All @@ -284,7 +284,7 @@
"text/html": [
"\n",
" <iframe\n",
" id=\"modelclDGBmFPaZ\"\n",
" id=\"modelZzRAPaKtcw\"\n",
" width=\"820\"\n",
" height=\"620\"\n",
" frameborder=\"0\"\n",
Expand Down Expand Up @@ -2141,7 +2141,7 @@
},
{
"cell_type": "code",
"execution_count": 13,
"execution_count": 12,
"metadata": {},
"outputs": [],
"source": [
Expand All @@ -2150,15 +2150,17 @@
},
{
"cell_type": "code",
"execution_count": 14,
"metadata": {},
"execution_count": 13,
"metadata": {
"scrolled": true
},
"outputs": [
{
"data": {
"text/html": [
"\n",
" <iframe\n",
" id=\"modelhYRVZOxBne\"\n",
" id=\"modeleXgJiypsxN\"\n",
" width=\"820\"\n",
" height=\"620\"\n",
" frameborder=\"0\"\n",
Expand Down Expand Up @@ -2514,6 +2516,48 @@
"vis2 = show.show(induced_dtmc, layout=stormvogel.layout.EXPLORE(), show_editor=False, save_and_embed=True)"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": []
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": []
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": []
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": []
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": []
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": []
},
{
"cell_type": "code",
"execution_count": null,
Expand Down
2 changes: 1 addition & 1 deletion docs/getting_started/model.html
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@

<iframe
id="modelhYRVZOxBne"
id="modeleXgJiypsxN"
width="820"
height="620"
frameborder="0"
Expand Down
11 changes: 7 additions & 4 deletions stormvogel/model.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -205,7 +205,7 @@ class Action:
labels: The labels of this action. Corresponds to Storm labels.
"""

name: str
name: str # TODO name is stormpy choice label or we don't need a name at all?
labels: frozenset[str]

def __str__(self):
Expand Down Expand Up @@ -862,6 +862,8 @@ def get_action(self, name: str) -> Action:
)
assert self.actions is not None
if name not in self.actions:
print(name)
print(self.actions)
raise RuntimeError(
f"Tried to get action {name} but that action does not exist"
)
Expand All @@ -883,15 +885,16 @@ def new_state(
self,
labels: list[str] | str | None = None,
features: dict[str, int] | None = None,
name: str | None = None,
) -> State:
"""Creates a new state and returns it."""
state_id = self.__free_state_id()
if isinstance(labels, list):
state = State(labels, features or {}, state_id, self)
state = State(labels, features or {}, state_id, self, name=name)
elif isinstance(labels, str):
state = State([labels], features or {}, state_id, self)
state = State([labels], features or {}, state_id, self, name=name)
elif labels is None:
state = State([], features or {}, state_id, self)
state = State([], features or {}, state_id, self, name=name)

self.states[state_id] = state

Expand Down
Loading