Skip to content

Commit

Permalink
Merge pull request #172 from moves-rwth/158-make-functions-that-help-…
Browse files Browse the repository at this point in the history 
…create-the-property-strings

158 make functions that help create the property strings
  • Loading branch information
@PimLeerkes
PimLeerkes authored Dec 22, 2024
2 parents dcd1051 + bb69719 commit a6d8cac
Show file tree
Hide file tree
Showing 7 changed files with 326 additions and 58 deletions.
49 changes: 28 additions & 21 deletions docs/getting_started/04_mdp.ipynb
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@
},
{
"cell_type": "code",
"execution_count": 1,
"execution_count": 2,
"metadata": {},
"outputs": [],
"source": [
Expand All @@ -19,16 +19,16 @@
},
{
"cell_type": "code",
"execution_count": 2,
"execution_count": 3,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"<stormpy.storage.storage.PrismProgram at 0x10827a1f0>"
"<stormpy.storage.storage.PrismProgram at 0x7f70bcd3d530>"
]
},
"execution_count": 2,
"execution_count": 3,
"metadata": {},
"output_type": "execute_result"
}
Expand Down Expand Up @@ -132,7 +132,7 @@
},
{
"cell_type": "code",
"execution_count": 3,
"execution_count": 4,
"metadata": {},
"outputs": [],
"source": [
Expand All @@ -142,7 +142,7 @@
},
{
"cell_type": "code",
"execution_count": 4,
"execution_count": 5,
"metadata": {},
"outputs": [
{
Expand All @@ -162,7 +162,7 @@
"Choice Labels: \tnone\n",
"-------------------------------------------------------------- \n",
"\n",
"['__class__', '__delattr__', '__dir__', '__doc__', '__eq__', '__format__', '__ge__', '__getattribute__', '__getstate__', '__gt__', '__hash__', '__init__', '__init_subclass__', '__le__', '__lt__', '__module__', '__ne__', '__new__', '__reduce__', '__reduce_ex__', '__repr__', '__setattr__', '__sizeof__', '__str__', '__subclasshook__', '_as_sparse_ctmc', '_as_sparse_dtmc', '_as_sparse_exact_dtmc', '_as_sparse_exact_mdp', '_as_sparse_imdp', '_as_sparse_ma', '_as_sparse_mdp', '_as_sparse_pctmc', '_as_sparse_pdtmc', '_as_sparse_pma', '_as_sparse_pmdp', '_as_sparse_pomdp', '_as_sparse_ppomdp', '_as_sparse_smg', '_as_symbolic_ctmc', '_as_symbolic_dtmc', '_as_symbolic_ma', '_as_symbolic_mdp', '_as_symbolic_pctmc', '_as_symbolic_pdtmc', '_as_symbolic_pma', '_as_symbolic_pmdp', 'add_reward_model', 'apply_scheduler', 'backward_transition_matrix', 'choice_labeling', 'choice_origins', 'get_choice_index', 'get_nr_available_actions', 'get_reward_model', 'has_choice_labeling', 'has_choice_origins', 'has_parameters', 'has_reward_model', 'has_state_valuations', 'initial_states', 'initial_states_as_bitvector', 'is_discrete_time_model', 'is_exact', 'is_nondeterministic_model', 'is_partially_observable', 'is_sink_state', 'is_sparse_model', 'is_symbolic_model', 'labeling', 'labels_state', 'model_type', 'nondeterministic_choice_indices', 'nr_choices', 'nr_states', 'nr_transitions', 'reduce_to_state_based_rewards', 'reward_models', 'set_initial_states', 'state_valuations', 'states', 'supports_parameters', 'supports_uncertainty', 'to_dot', 'transition_matrix']\n"
"['__class__', '__delattr__', '__dir__', '__doc__', '__eq__', '__format__', '__ge__', '__getattribute__', '__getstate__', '__gt__', '__hash__', '__init__', '__init_subclass__', '__le__', '__lt__', '__module__', '__ne__', '__new__', '__reduce__', '__reduce_ex__', '__repr__', '__setattr__', '__sizeof__', '__str__', '__subclasshook__', '_as_sparse_ctmc', '_as_sparse_dtmc', '_as_sparse_exact_dtmc', '_as_sparse_exact_mdp', '_as_sparse_imdp', '_as_sparse_ma', '_as_sparse_mdp', '_as_sparse_pctmc', '_as_sparse_pdtmc', '_as_sparse_pma', '_as_sparse_pmdp', '_as_sparse_pomdp', '_as_sparse_ppomdp', '_as_symbolic_ctmc', '_as_symbolic_dtmc', '_as_symbolic_ma', '_as_symbolic_mdp', '_as_symbolic_pctmc', '_as_symbolic_pdtmc', '_as_symbolic_pma', '_as_symbolic_pmdp', 'add_reward_model', 'apply_scheduler', 'backward_transition_matrix', 'choice_labeling', 'choice_origins', 'get_choice_index', 'get_nr_available_actions', 'get_reward_model', 'has_choice_labeling', 'has_choice_origins', 'has_parameters', 'has_reward_model', 'has_state_valuations', 'initial_states', 'initial_states_as_bitvector', 'is_discrete_time_model', 'is_exact', 'is_nondeterministic_model', 'is_partially_observable', 'is_sink_state', 'is_sparse_model', 'is_symbolic_model', 'labeling', 'labels_state', 'model_type', 'nondeterministic_choice_indices', 'nr_choices', 'nr_states', 'nr_transitions', 'reduce_to_state_based_rewards', 'reward_models', 'set_initial_states', 'state_valuations', 'states', 'supports_parameters', 'supports_uncertainty', 'to_dot', 'transition_matrix']\n"
]
}
],
Expand All @@ -174,7 +174,7 @@
},
{
"cell_type": "code",
"execution_count": 5,
"execution_count": 6,
"metadata": {},
"outputs": [],
"source": [
Expand All @@ -183,7 +183,7 @@
},
{
"cell_type": "code",
"execution_count": 6,
"execution_count": 7,
"metadata": {},
"outputs": [],
"source": [
Expand All @@ -192,7 +192,7 @@
},
{
"cell_type": "code",
"execution_count": 7,
"execution_count": 8,
"metadata": {},
"outputs": [
{
Expand All @@ -209,7 +209,7 @@
},
{
"cell_type": "code",
"execution_count": 8,
"execution_count": 9,
"metadata": {},
"outputs": [
{
Expand All @@ -222,9 +222,9 @@
"Transitions: \t56\n",
"Reward Models: rounds\n",
"State Labels: \t3 labels\n",
" * deadlock -> 3 item(s)\n",
" * init -> 1 item(s)\n",
" * elected -> 0 item(s)\n",
" * init -> 1 item(s)\n",
" * deadlock -> 3 item(s)\n",
"Choice Labels: \tnone\n",
"-------------------------------------------------------------- \n",
"\n"
Expand All @@ -239,7 +239,7 @@
},
{
"cell_type": "code",
"execution_count": 9,
"execution_count": 10,
"metadata": {},
"outputs": [
{
Expand All @@ -261,7 +261,7 @@
},
{
"cell_type": "code",
"execution_count": 10,
"execution_count": 11,
"metadata": {
"scrolled": true
},
Expand All @@ -274,7 +274,7 @@
},
{
"cell_type": "code",
"execution_count": 11,
"execution_count": 12,
"metadata": {
"scrolled": true
},
Expand All @@ -284,7 +284,7 @@
"text/html": [
"\n",
" <iframe\n",
" id=\"modelOjoDulqviS\"\n",
" id=\"modelclDGBmFPaZ\"\n",
" width=\"820\"\n",
" height=\"620\"\n",
" frameborder=\"0\"\n",
Expand Down Expand Up @@ -2141,7 +2141,7 @@
},
{
"cell_type": "code",
"execution_count": 12,
"execution_count": 13,
"metadata": {},
"outputs": [],
"source": [
Expand All @@ -2150,15 +2150,15 @@
},
{
"cell_type": "code",
"execution_count": 13,
"execution_count": 14,
"metadata": {},
"outputs": [
{
"data": {
"text/html": [
"\n",
" <iframe\n",
" id=\"modelIQGBHetHwx\"\n",
" id=\"modelhYRVZOxBne\"\n",
" width=\"820\"\n",
" height=\"620\"\n",
" frameborder=\"0\"\n",
Expand Down Expand Up @@ -2513,6 +2513,13 @@
"source": [
"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": []
}
],
"metadata": {
Expand All @@ -2531,7 +2538,7 @@
"name": "python",
"nbconvert_exporter": "python",
"pygments_lexer": "ipython3",
"version": "3.12.6"
"version": "3.12.7"
}
},
"nbformat": 4,
Expand Down
188 changes: 156 additions & 32 deletions docs/getting_started/model.html
View file
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@

<iframe
id="modelZVKCIZVJVv"
id="modelhYRVZOxBne"
width="820"
height="620"
frameborder="0"
Expand All @@ -27,37 +27,161 @@
&lt;div id=&quot;mynetwork&quot;&gt;&lt;/div&gt;
&lt;script type=&quot;text/javascript&quot;&gt;
var nodes = new vis.DataSet([{ id: 0, label: `nijmegen`, group: &quot;states&quot; },
{ id: 1, label: `eindhoven`, group: &quot;states&quot; },
{ id: 2, label: `aachen`, group: &quot;states&quot; },
{ id: 3, label: `saw nijmegen
ʘ 3`, group: &quot;states&quot; },
{ id: 4, label: `saw eindhoven
ʘ 4`, group: &quot;states&quot; },
{ id: 5, label: `saw aachen
ʘ 5`, group: &quot;states&quot; },
{ id: 10000000000, label: `walk`, group: &quot;actions&quot; },
{ id: 10000000001, label: `stay put`, group: &quot;actions&quot; },
{ id: 10000000002, label: `walk`, group: &quot;actions&quot; },
{ id: 10000000003, label: `stay put`, group: &quot;actions&quot; },
{ id: 10000000004, label: `walk`, group: &quot;actions&quot; },
{ id: 10000000005, label: `stay put`, group: &quot;actions&quot; },
var nodes = new vis.DataSet([{ id: 0, label: `init
€ rounds: 0.0`, group: &quot;states&quot; },
{ id: 1, label: `
€ rounds: 0.0`, group: &quot;states&quot;, hidden: true },
{ id: 2, label: `
€ rounds: 0.0`, group: &quot;states&quot;, hidden: true },
{ id: 3, label: `
€ rounds: 0.0`, group: &quot;states&quot;, hidden: true },
{ id: 4, label: `
€ rounds: 0.0`, group: &quot;states&quot;, hidden: true },
{ id: 5, label: `
€ rounds: 0.0`, group: &quot;states&quot;, hidden: true },
{ id: 6, label: `
€ rounds: 0.0`, group: &quot;states&quot;, hidden: true },
{ id: 7, label: `
€ rounds: 0.0`, group: &quot;states&quot;, hidden: true },
{ id: 8, label: `
€ rounds: 0.0`, group: &quot;states&quot;, hidden: true },
{ id: 9, label: `
€ rounds: 0.0`, group: &quot;states&quot;, hidden: true },
{ id: 10, label: `
€ rounds: 0.0`, group: &quot;states&quot;, hidden: true },
{ id: 11, label: `
€ rounds: 0.0`, group: &quot;states&quot;, hidden: true },
{ id: 12, label: `
€ rounds: 0.0`, group: &quot;states&quot;, hidden: true },
{ id: 13, label: `
€ rounds: 0.0`, group: &quot;states&quot;, hidden: true },
{ id: 14, label: `
€ rounds: 0.0`, group: &quot;states&quot;, hidden: true },
{ id: 15, label: `
€ rounds: 0.0`, group: &quot;states&quot;, hidden: true },
{ id: 16, label: `
€ rounds: 0.0`, group: &quot;states&quot;, hidden: true },
{ id: 17, label: `
€ rounds: 1.0`, group: &quot;states&quot;, hidden: true },
{ id: 18, label: `
€ rounds: 0.0`, group: &quot;states&quot;, hidden: true },
{ id: 19, label: `
€ rounds: 1.0`, group: &quot;states&quot;, hidden: true },
{ id: 20, label: `
€ rounds: 0.0`, group: &quot;states&quot;, hidden: true },
{ id: 21, label: `
€ rounds: 1.0`, group: &quot;states&quot;, hidden: true },
{ id: 22, label: `
€ rounds: 1.0`, group: &quot;states&quot;, hidden: true },
{ id: 23, label: `
€ rounds: 1.0`, group: &quot;states&quot;, hidden: true },
{ id: 24, label: `
€ rounds: 1.0`, group: &quot;states&quot;, hidden: true },
{ id: 25, label: `
€ rounds: 0.0`, group: &quot;states&quot;, hidden: true },
{ id: 26, label: `
€ rounds: 0.0`, group: &quot;states&quot;, hidden: true },
{ id: 27, label: `
€ rounds: 0.0`, group: &quot;states&quot;, hidden: true },
{ id: 28, label: `
€ rounds: 0.0`, group: &quot;states&quot;, hidden: true },
{ id: 29, label: `
€ rounds: 0.0`, group: &quot;states&quot;, hidden: true },
{ id: 30, label: `
€ rounds: 0.0`, group: &quot;states&quot;, hidden: true },
{ id: 31, label: `
€ rounds: 0.0`, group: &quot;states&quot;, hidden: true },
{ id: 32, label: `
€ rounds: 0.0`, group: &quot;states&quot;, hidden: true },
{ id: 33, label: `
€ rounds: 1.0`, group: &quot;states&quot;, hidden: true },
{ id: 34, label: `
€ rounds: 0.0`, group: &quot;states&quot;, hidden: true },
{ id: 35, label: `
€ rounds: 0.0`, group: &quot;states&quot;, hidden: true },
{ id: 36, label: `
€ rounds: 0.0`, group: &quot;states&quot;, hidden: true },
{ id: 37, label: `
€ rounds: 0.0`, group: &quot;states&quot;, hidden: true },
{ id: 38, label: `
€ rounds: 0.0`, group: &quot;states&quot;, hidden: true },
{ id: 39, label: `
€ rounds: 0.0`, group: &quot;states&quot;, hidden: true },
{ id: 40, label: `
€ rounds: 0.0`, group: &quot;states&quot;, hidden: true },
{ id: 41, label: `
€ rounds: 0.0`, group: &quot;states&quot;, hidden: true },
{ id: 42, label: `
€ rounds: 0.0`, group: &quot;states&quot;, hidden: true },
{ id: 43, label: `
€ rounds: 0.0`, group: &quot;states&quot;, hidden: true },
{ id: 44, label: `
€ rounds: 0.0`, group: &quot;states&quot;, hidden: true },
{ id: 45, label: `
€ rounds: 0.0`, group: &quot;states&quot;, hidden: true },
{ id: 46, label: `deadlock
€ rounds: 0.0`, group: &quot;states&quot;, hidden: true },
{ id: 47, label: `deadlock
€ rounds: 0.0`, group: &quot;states&quot;, hidden: true },
{ id: 48, label: `deadlock
€ rounds: 0.0`, group: &quot;states&quot;, hidden: true },
]);
var edges = new vis.DataSet([{ from: 0, to: 10000000000 },
{ from: 10000000000, to: 3, label: &quot;1&quot; },
{ from: 0, to: 10000000001 },
{ from: 10000000001, to: 0, label: &quot;1&quot; },
{ from: 3, to: 0, label: &quot;1&quot; },
{ from: 1, to: 10000000002 },
{ from: 10000000002, to: 4, label: &quot;1&quot; },
{ from: 1, to: 10000000003 },
{ from: 10000000003, to: 1, label: &quot;1&quot; },
{ from: 4, to: 1, label: &quot;1&quot; },
{ from: 2, to: 10000000004 },
{ from: 10000000004, to: 5, label: &quot;1&quot; },
{ from: 2, to: 10000000005 },
{ from: 10000000005, to: 2, label: &quot;1&quot; },
{ from: 5, to: 2, label: &quot;1&quot; },
var edges = new vis.DataSet([{ from: 0, to: 1, label: &quot;1/8&quot; },
{ from: 0, to: 2, label: &quot;1/8&quot; },
{ from: 0, to: 3, label: &quot;1/8&quot; },
{ from: 0, to: 4, label: &quot;1/8&quot; },
{ from: 0, to: 5, label: &quot;1/8&quot; },
{ from: 0, to: 6, label: &quot;1/8&quot; },
{ from: 0, to: 7, label: &quot;1/8&quot; },
{ from: 0, to: 8, label: &quot;1/8&quot; },
{ from: 1, to: 9, label: &quot;1&quot; },
{ from: 2, to: 10, label: &quot;1&quot; },
{ from: 3, to: 11, label: &quot;1&quot; },
{ from: 4, to: 12, label: &quot;1&quot; },
{ from: 5, to: 13, label: &quot;1&quot; },
{ from: 6, to: 14, label: &quot;1&quot; },
{ from: 7, to: 15, label: &quot;1&quot; },
{ from: 8, to: 16, label: &quot;1&quot; },
{ from: 9, to: 17, label: &quot;1&quot; },
{ from: 10, to: 18, label: &quot;1&quot; },
{ from: 11, to: 19, label: &quot;1&quot; },
{ from: 12, to: 20, label: &quot;1&quot; },
{ from: 13, to: 21, label: &quot;1&quot; },
{ from: 14, to: 22, label: &quot;1&quot; },
{ from: 15, to: 23, label: &quot;1&quot; },
{ from: 16, to: 24, label: &quot;1&quot; },
{ from: 17, to: 25, label: &quot;1&quot; },
{ from: 18, to: 26, label: &quot;1&quot; },
{ from: 19, to: 27, label: &quot;1&quot; },
{ from: 20, to: 26, label: &quot;1&quot; },
{ from: 21, to: 28, label: &quot;1&quot; },
{ from: 22, to: 29, label: &quot;1&quot; },
{ from: 23, to: 30, label: &quot;1&quot; },
{ from: 24, to: 31, label: &quot;1&quot; },
{ from: 25, to: 32, label: &quot;1&quot; },
{ from: 26, to: 33, label: &quot;1&quot; },
{ from: 27, to: 34, label: &quot;1&quot; },
{ from: 28, to: 35, label: &quot;1&quot; },
{ from: 29, to: 36, label: &quot;1&quot; },
{ from: 30, to: 37, label: &quot;1&quot; },
{ from: 31, to: 38, label: &quot;1&quot; },
{ from: 32, to: 39, label: &quot;1&quot; },
{ from: 33, to: 40, label: &quot;1&quot; },
{ from: 34, to: 41, label: &quot;1&quot; },
{ from: 35, to: 42, label: &quot;1&quot; },
{ from: 36, to: 43, label: &quot;1&quot; },
{ from: 37, to: 44, label: &quot;1&quot; },
{ from: 38, to: 45, label: &quot;1&quot; },
{ from: 39, to: 0, label: &quot;1&quot; },
{ from: 40, to: 46, label: &quot;1&quot; },
{ from: 41, to: 47, label: &quot;1&quot; },
{ from: 42, to: 48, label: &quot;1&quot; },
{ from: 43, to: 48, label: &quot;1&quot; },
{ from: 44, to: 47, label: &quot;1&quot; },
{ from: 45, to: 0, label: &quot;1&quot; },
{ from: 46, to: 46, label: &quot;1&quot; },
{ from: 47, to: 47, label: &quot;1&quot; },
{ from: 48, to: 48, label: &quot;1&quot; },
]);
var options = {
&quot;__fake_macros&quot;: {
Expand Down Expand Up @@ -164,7 +288,7 @@
&quot;enable_physics&quot;: true,
&quot;width&quot;: 800,
&quot;height&quot;: 600,
&quot;explore&quot;: false
&quot;explore&quot;: true
},
&quot;saving&quot;: {
&quot;relative_path&quot;: true,
Expand Down
Loading

0 comments on commit a6d8cac

Please sign in to comment.