Put program into a single module
Build state generation information
Build state generation information
Put program into a single module
[1]:
>>> import stormpy
->>> import stormpy.examples
->>> import stormpy.examples.files
->>> path = stormpy.examples.files.prism_dtmc_die
->>> prism_program = stormpy.parse_prism_program(path)
->>> formula_str = "P=? [F s=7 & d=2]"
->>> properties = stormpy.parse_properties(formula_str, prism_program)
+import stormpy
+import stormpy.examples
+import stormpy.examples.files
+
+path = stormpy.examples.files.prism_dtmc_die
+prism_program = stormpy.parse_prism_program(path)
+formula_str = "P=? [F s=7 & d=2]"
+properties = stormpy.parse_properties(formula_str, prism_program)
[2]:
>>> model = stormpy.build_symbolic_model(prism_program, properties)
->>> result = stormpy.model_checking(model, properties[0])
+model = stormpy.build_symbolic_model(prism_program, properties)
+result = stormpy.model_checking(model, properties[0])
[3]:
>>> filter = stormpy.create_filter_initial_states_symbolic(model)
->>> result.filter(filter)
->>> assert result.min == result.max
+filter = stormpy.create_filter_initial_states_symbolic(model)
+result.filter(filter)
+assert result.min == result.max
[4]:
>>> model = stormpy.build_model(prism_program, properties)
->>> result = stormpy.model_checking(model, properties[0])
+model = stormpy.build_model(prism_program, properties)
+result = stormpy.model_checking(model, properties[0])
[5]:
>>> env = stormpy.Environment()
->>> env.solver_environment.set_linear_equation_solver_type(stormpy.EquationSolverType.native)
->>> env.solver_environment.native_solver_environment.method = stormpy.NativeLinearEquationSolverMethod.power_iteration
->>> result = stormpy.model_checking(model, properties[0], environment=env)
+env = stormpy.Environment()
+env.solver_environment.set_linear_equation_solver_type(stormpy.EquationSolverType.native)
+env.solver_environment.native_solver_environment.method = stormpy.NativeLinearEquationSolverMethod.power_iteration
+result = stormpy.model_checking(model, properties[0], environment=env)
[6]:
>>> env.solver_environment.native_solver_environment.maximum_iterations = 3
->>> result = stormpy.model_checking(model, properties[0])
+env.solver_environment.native_solver_environment.maximum_iterations = 3
+result = stormpy.model_checking(model, properties[0])
[1]:
>>> import stormpy.examples
->>> import stormpy.examples.files
+import stormpy.examples
+import stormpy.examples.files
[2]:
>>> path = stormpy.examples.files.drn_ctmc_dft
->>> model = stormpy.build_model_from_drn(path)
->>> print(model.model_type)
+path = stormpy.examples.files.drn_ctmc_dft
+model = stormpy.build_model_from_drn(path)
+print(model.model_type)
[3]:
>>> path = stormpy.examples.files.drn_pdtmc_die
->>> model = stormpy.build_parametric_model_from_drn(path)
->>> print(model.model_type)
+path = stormpy.examples.files.drn_pdtmc_die
+model = stormpy.build_parametric_model_from_drn(path)
+print(model.model_type)
[4]:
>>> path = stormpy.examples.files.jani_dtmc_die
->>> jani_program, properties = stormpy.parse_jani_model(path)
->>> model = stormpy.build_model(jani_program)
->>> print(model.model_type)
+path = stormpy.examples.files.jani_dtmc_die
+jani_program, properties = stormpy.parse_jani_model(path)
+model = stormpy.build_model(jani_program)
+print(model.model_type)
[1]:
>>> import stormpy
->>> import stormpy.dft
->>> import stormpy.examples
->>> import stormpy.examples.files
->>> path_json = stormpy.examples.files.dft_json_and
->>> dft_small = stormpy.dft.load_dft_json_file(path_json)
->>> print(dft_small)
+import stormpy
+import stormpy.dft
+import stormpy.examples
+import stormpy.examples.files
+
+path_json = stormpy.examples.files.dft_json_and
+dft_small = stormpy.dft.load_dft_json_file(path_json)
+print(dft_small)
[2]:
>>> path_galileo = stormpy.examples.files.dft_galileo_hecs
->>> dft = stormpy.dft.load_dft_galileo_file(path_galileo)
+path_galileo = stormpy.examples.files.dft_galileo_hecs
+dft = stormpy.dft.load_dft_galileo_file(path_galileo)
[3]:
>>> print("DFT with {} elements.".format(dft.nr_elements()))
->>> print("DFT has {} BEs and {} dynamic elements.".format(dft.nr_be(), dft.nr_dynamic()))
+print("DFT with {} elements.".format(dft.nr_elements()))
+print("DFT has {} BEs and {} dynamic elements.".format(dft.nr_be(), dft.nr_dynamic()))
[4]:
>>> formula_str = "T=? [ F \"failed\" ]"
->>> formulas = stormpy.parse_properties(formula_str)
->>> results = stormpy.dft.analyze_dft(dft, [formulas[0].raw_formula])
->>> result = results[0]
->>> print("MTTF: {:.2f}".format(result))
+formula_str = 'T=? [ F "failed" ]'
+formulas = stormpy.parse_properties(formula_str)
+results = stormpy.dft.analyze_dft(dft, [formulas[0].raw_formula])
+result = results[0]
+print("MTTF: {:.2f}".format(result))
[1]:
>>> import stormpy.examples
->>> import stormpy.examples.files
->>> prism_program = stormpy.parse_prism_program(stormpy.examples.files.prism_dtmc_die)
->>> properties = stormpy.parse_properties('P=? [F "one"]', prism_program)
->>> sparse_model = stormpy.build_sparse_model(prism_program, properties)
->>> print(type(sparse_model))
-
import stormpy.examples
+import stormpy.examples.files
+
+prism_program = stormpy.parse_prism_program(stormpy.examples.files.prism_dtmc_die)
+properties = stormpy.parse_properties('P=? [F "one"]', prism_program)
+sparse_model = stormpy.build_sparse_model(prism_program, properties)
+print(type(sparse_model))
+[3]:
>>> print("Number of transitions: {}".format(sparse_model.nr_transitions))
+print("Number of transitions: {}".format(sparse_model.nr_transitions))
[4]:
>>> sparse_result = stormpy.check_model_sparse(sparse_model, properties[0])
->>> initial_state = sparse_model.initial_states[0]
->>> print(sparse_result.at(initial_state))
+sparse_result = stormpy.check_model_sparse(sparse_model, properties[0])
+initial_state = sparse_model.initial_states[0]
+print(sparse_result.at(initial_state))
[5]:
>>> symbolic_model = stormpy.build_symbolic_model(prism_program, properties)
->>> print(type(symbolic_model))
+symbolic_model = stormpy.build_symbolic_model(prism_program, properties)
+print(type(symbolic_model))
[6]:
>>> print("Number of states: {}".format(symbolic_model.nr_states))
+print("Number of states: {}".format(symbolic_model.nr_states))
[7]:
>>> print("Number of transitions: {}".format(symbolic_model.nr_transitions))
+print("Number of transitions: {}".format(symbolic_model.nr_transitions))
[8]:
>>> symbolic_result = stormpy.check_model_dd(symbolic_model, properties[0])
->>> print(symbolic_result)
+symbolic_result = stormpy.check_model_dd(symbolic_model, properties[0])
+print(symbolic_result)
[9]:
>>> filter = stormpy.create_filter_initial_states_symbolic(symbolic_model)
->>> symbolic_result.filter(filter)
->>> print(symbolic_result.min)
+filter = stormpy.create_filter_initial_states_symbolic(symbolic_model)
+symbolic_result.filter(filter)
+print(symbolic_result.min)
[10]:
>>> print(type(symbolic_model))
+print(type(symbolic_model))
[11]:
>>> transformed_model = stormpy.transform_to_sparse_model(symbolic_model)
->>> print(type(transformed_model))
+transformed_model = stormpy.transform_to_sparse_model(symbolic_model)
+print(type(transformed_model))
[12]:
>>> print(type(symbolic_model))
+print(type(symbolic_model))
[13]:
>>> hybrid_result = stormpy.check_model_hybrid(symbolic_model, properties[0])
->>> filter = stormpy.create_filter_initial_states_symbolic(symbolic_model)
->>> hybrid_result.filter(filter)
->>> print(hybrid_result)
+hybrid_result = stormpy.check_model_hybrid(symbolic_model, properties[0])
+filter = stormpy.create_filter_initial_states_symbolic(symbolic_model)
+hybrid_result.filter(filter)
+print(hybrid_result)
[1]:
>>> import doctest
->>> doctest.ELLIPSIS_MARKER = '-etc-'
->>> import stormpy
->>> import stormpy.examples
->>> import stormpy.examples.files
->>> program = stormpy.parse_prism_program(stormpy.examples.files.prism_mdp_maze)
->>> prop = "R=? [F \"goal\"]"
+import doctest
->>> properties = stormpy.parse_properties_for_prism_program(prop, program, None)
->>> model = stormpy.build_model(program, properties)
+doctest.ELLIPSIS_MARKER = "-etc-"
+import stormpy
+import stormpy.examples
+import stormpy.examples.files
+
+program = stormpy.parse_prism_program(stormpy.examples.files.prism_mdp_maze)
+prop = 'R=? [F "goal"]'
+
+properties = stormpy.parse_properties_for_prism_program(prop, program, None)
+model = stormpy.build_model(program, properties)
[2]:
>>> for state in model.states:
-... if state.id in model.initial_states:
-... print("State {} is initial".format(state.id))
-... for action in state.actions:
-... for transition in action.transitions:
-... print("From state {} by action {}, with probability {}, go to state {}".format(state, action, transition.value(), transition.column))
+for state in model.states:
+ if state.id in model.initial_states:
+ print("State {} is initial".format(state.id))
+ for action in state.actions:
+ for transition in action.transitions:
+ print("From state {} by action {}, with probability {}, go to state {}".format(state, action, transition.value(), transition.column))
[3]:
>>> import stormpy
->>> import stormpy.examples
->>> import stormpy.examples.files
->>> program = stormpy.parse_prism_program(stormpy.examples.files.prism_pomdp_maze)
->>> prop = "R=? [F \"goal\"]"
->>> properties = stormpy.parse_properties_for_prism_program(prop, program, None)
->>> model = stormpy.build_model(program, properties)
+import stormpy
+import stormpy.examples
+import stormpy.examples.files
+
+program = stormpy.parse_prism_program(stormpy.examples.files.prism_pomdp_maze)
+prop = 'R=? [F "goal"]'
+properties = stormpy.parse_properties_for_prism_program(prop, program, None)
+model = stormpy.build_model(program, properties)
[4]:
>>> print(model.model_type)
+print(model.model_type)
[5]:
>>> print(model.nr_observations)
->>> for state in model.states:
-... print("State {} has observation id {}".format(state.id, model.observations[state.id]))
+print(model.nr_observations)
+for state in model.states:
+ print("State {} has observation id {}".format(state.id, model.observations[state.id]))
[1]:
>>> import stormpy
->>> import stormpy.gspn
->>> import stormpy.examples
->>> import stormpy.examples.files
+import stormpy
+import stormpy.gspn
+import stormpy.examples
+import stormpy.examples.files
->>> import_path = stormpy.examples.files.gspn_pnml_simple
->>> gspn_parser = stormpy.gspn.GSPNParser()
->>> gspn = gspn_parser.parse(import_path)
+import_path = stormpy.examples.files.gspn_pnml_simple
+gspn_parser = stormpy.gspn.GSPNParser()
+gspn = gspn_parser.parse(import_path)
[2]:
>>> print("Name of GSPN: {}.".format(gspn.get_name()))
+print("Name of GSPN: {}.".format(gspn.get_name()))
[3]:
>>> print("Number of places: {}.".format(gspn.get_number_of_places()))
+print("Number of places: {}.".format(gspn.get_number_of_places()))
[4]:
>>> print("Number of immediate transitions: {}.".format(gspn.get_number_of_immediate_transitions()))
+print("Number of immediate transitions: {}.".format(gspn.get_number_of_immediate_transitions()))
[5]:
>>> print("Number of timed transitions: {}.".format(gspn.get_number_of_timed_transitions()))
+print("Number of timed transitions: {}.".format(gspn.get_number_of_timed_transitions()))
[6]:
>>> builder = stormpy.gspn.GSPNBuilder()
->>> builder.set_name("my_gspn")
+builder = stormpy.gspn.GSPNBuilder()
+builder.set_name("my_gspn")
[7]:
>>> it_1 = builder.add_immediate_transition(1, 0.0, "it_1")
->>> it_layout = stormpy.gspn.LayoutInfo(1.5, 2.0)
->>> builder.set_transition_layout_info(it_1, it_layout)
+it_1 = builder.add_immediate_transition(1, 0.0, "it_1")
+it_layout = stormpy.gspn.LayoutInfo(1.5, 2.0)
+builder.set_transition_layout_info(it_1, it_layout)
[8]:
>>> tt_1 = builder.add_timed_transition(0, 0.4, "tt_1")
->>> tt_layout = stormpy.gspn.LayoutInfo(12.5, 2.0)
->>> builder.set_transition_layout_info(tt_1, tt_layout)
+tt_1 = builder.add_timed_transition(0, 0.4, "tt_1")
+tt_layout = stormpy.gspn.LayoutInfo(12.5, 2.0)
+builder.set_transition_layout_info(tt_1, tt_layout)
[9]:
>>> place_1 = builder.add_place(1, 1, "place_1")
->>> p1_layout = stormpy.gspn.LayoutInfo(6.5, 2.0)
->>> builder.set_place_layout_info(place_1, p1_layout)
+place_1 = builder.add_place(1, 1, "place_1")
+p1_layout = stormpy.gspn.LayoutInfo(6.5, 2.0)
+builder.set_place_layout_info(place_1, p1_layout)
->>> place_2 = builder.add_place(1, 0, "place_2")
->>> p2_layout = stormpy.gspn.LayoutInfo(18.5, 2.0)
->>> builder.set_place_layout_info(place_2, p2_layout)
+place_2 = builder.add_place(1, 0, "place_2")
+p2_layout = stormpy.gspn.LayoutInfo(18.5, 2.0)
+builder.set_place_layout_info(place_2, p2_layout)
[10]:
>>> builder.add_output_arc(it_1, place_1)
->>> builder.add_inhibition_arc(place_1, it_1)
->>> builder.add_input_arc(place_1, tt_1)
->>> builder.add_output_arc(tt_1, place_2)
+builder.add_output_arc(it_1, place_1)
+builder.add_inhibition_arc(place_1, it_1)
+builder.add_input_arc(place_1, tt_1)
+builder.add_output_arc(tt_1, place_2)
[11]:
>>> gspn = builder.build_gspn()
+gspn = builder.build_gspn()
[12]:
>>> export_path = stormpy.examples.files.gspn_pnpro_simple
->>> gspn.export_gspn_pnpro_file(export_path)
+export_path = stormpy.examples.files.gspn_pnpro_simple
+gspn.export_gspn_pnpro_file(export_path)
[1]:
>>> import stormpy
+import stormpy
[2]:
>>> import numpy as np
->>> transitions = np.array([
-... [0, 1.5, 0, 0],
-... [3, 0, 1.5, 0],
-... [0, 3, 0, 1.5],
-... [0, 0, 3, 0], ], dtype='float64')
+import numpy as np
+
+transitions = np.array(
+ [
+ [0, 1.5, 0, 0],
+ [3, 0, 1.5, 0],
+ [0, 3, 0, 1.5],
+ [0, 0, 3, 0],
+ ],
+ dtype="float64",
+)
[3]:
>>> transition_matrix = stormpy.build_sparse_matrix(transitions)
->>> print(transition_matrix)
+transition_matrix = stormpy.build_sparse_matrix(transitions)
+print(transition_matrix)
[4]:
>>> state_labeling = stormpy.storage.StateLabeling(4)
->>> state_labels = {'empty', 'init', 'deadlock', 'full'}
->>> for label in state_labels:
-... state_labeling.add_label(label)
->>> state_labeling.add_label_to_state('init', 0)
->>> state_labeling.add_label_to_state('empty', 0)
->>> state_labeling.add_label_to_state('full', 3)
+state_labeling = stormpy.storage.StateLabeling(4)
+state_labels = {"empty", "init", "deadlock", "full"}
+for label in state_labels:
+ state_labeling.add_label(label)
+state_labeling.add_label_to_state("init", 0)
+state_labeling.add_label_to_state("empty", 0)
+state_labeling.add_label_to_state("full", 3)
[5]:
>>> components = stormpy.SparseModelComponents(transition_matrix=transition_matrix, state_labeling=state_labeling, rate_transitions=True)
-
components = stormpy.SparseModelComponents(transition_matrix=transition_matrix, state_labeling=state_labeling, rate_transitions=True)
+And finally, we can build the model:
@@ -931,8 +936,8 @@[6]:
>>> ctmc = stormpy.storage.SparseCtmc(components)
->>> print(ctmc)
+ctmc = stormpy.storage.SparseCtmc(components)
+print(ctmc)
[1]:
>>> import stormpy
+import stormpy
[2]:
>>> builder = stormpy.SparseMatrixBuilder(rows = 0, columns = 0, entries = 0, force_dimensions = False, has_custom_row_grouping = False)
+builder = stormpy.SparseMatrixBuilder(rows=0, columns=0, entries=0, force_dimensions=False, has_custom_row_grouping=False)
[3]:
>>> 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)
+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)
[4]:
>>> for s in range(7,13):
-... builder.add_next_value(s, s, 1)
+for s in range(7, 13):
+ builder.add_next_value(s, s, 1)
[5]:
>>> transition_matrix = builder.build()
+transition_matrix = builder.build()
[6]:
>>> state_labeling = stormpy.storage.StateLabeling(13)
+state_labeling = stormpy.storage.StateLabeling(13)
->>> labels = {'init', 'one', 'two', 'three', 'four', 'five', 'six', 'done', 'deadlock'}
->>> for label in labels:
-... state_labeling.add_label(label)
+labels = {"init", "one", "two", "three", "four", "five", "six", "done", "deadlock"}
+for label in labels:
+ state_labeling.add_label(label)
[7]:
>>> state_labeling.add_label_to_state('init', 0)
->>> print(state_labeling.get_states('init'))
+state_labeling.add_label_to_state("init", 0)
+print(state_labeling.get_states("init"))
[8]:
>>> 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)
+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)
[9]:
>>> state_labeling.set_states('done', stormpy.BitVector(13, [7, 8, 9, 10, 11, 12]))
->>> print(state_labeling)
+state_labeling.set_states("done", stormpy.BitVector(13, [7, 8, 9, 10, 11, 12]))
+print(state_labeling)
9 labels
+ * three -> 1 item(s)
* five -> 1 item(s)
* deadlock -> 0 item(s)
- * two -> 1 item(s)
- * one -> 1 item(s)
- * six -> 1 item(s)
* init -> 1 item(s)
+ * one -> 1 item(s)
* four -> 1 item(s)
* done -> 6 item(s)
- * three -> 1 item(s)
+ * six -> 1 item(s)
+ * two -> 1 item(s)
[10]:
>>> reward_models = {}
->>> 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)
+reward_models = {}
+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)
[11]:
>>> components = stormpy.SparseModelComponents(transition_matrix=transition_matrix, state_labeling=state_labeling, reward_models=reward_models)
+components = stormpy.SparseModelComponents(transition_matrix=transition_matrix, state_labeling=state_labeling, reward_models=reward_models)
[12]:
>>> dtmc = stormpy.storage.SparseDtmc(components)
->>> print(dtmc)
+dtmc = stormpy.storage.SparseDtmc(components)
+print(dtmc)
[1]:
>>> import stormpy
+import stormpy
[2]:
>>> import numpy as np
->>> transitions = np.array([
-... [0, 1, 0, 0, 0],
-... [0.8, 0, 0.2, 0, 0],
-... [0.9, 0, 0, 0.1, 0],
-... [0, 0, 0, 0, 1],
-... [0, 0, 0, 1, 0],
-... [0, 0, 0, 0, 1]], dtype='float64')
+import numpy as np
+
+transitions = np.array([[0, 1, 0, 0, 0], [0.8, 0, 0.2, 0, 0], [0.9, 0, 0, 0.1, 0], [0, 0, 0, 0, 1], [0, 0, 0, 1, 0], [0, 0, 0, 0, 1]], dtype="float64")
[3]:
>>> transition_matrix = stormpy.build_sparse_matrix(transitions, [0, 2, 3, 4, 5])
->>> print(transition_matrix)
+transition_matrix = stormpy.build_sparse_matrix(transitions, [0, 2, 3, 4, 5])
+print(transition_matrix)
[5]:
>>> markovian_states = stormpy.BitVector(5, [1, 2, 3, 4])
+markovian_states = stormpy.BitVector(5, [1, 2, 3, 4])
[7]:
>>> components = stormpy.SparseModelComponents(transition_matrix=transition_matrix, state_labeling=state_labeling, markovian_states=markovian_states)
->>> components.choice_labeling = choice_labeling
->>> components.exit_rates = exit_rates
+components = stormpy.SparseModelComponents(transition_matrix=transition_matrix, state_labeling=state_labeling, markovian_states=markovian_states)
+components.choice_labeling = choice_labeling
+components.exit_rates = exit_rates
[8]:
>>> ma = stormpy.storage.SparseMA(components)
->>> print(ma)
+ma = stormpy.storage.SparseMA(components)
+print(ma)
[1]:
>>> import stormpy
+import stormpy
[2]:
>>> builder = stormpy.SparseMatrixBuilder(rows=0, columns=0, entries=0, force_dimensions=False, has_custom_row_grouping=True, row_groups=0)
+builder = stormpy.SparseMatrixBuilder(rows=0, columns=0, entries=0, force_dimensions=False, has_custom_row_grouping=True, row_groups=0)
[3]:
>>> builder.new_row_group(0)
->>> builder.add_next_value(0, 1, 0.5)
->>> builder.add_next_value(0, 2, 0.5)
->>> builder.add_next_value(1, 1, 0.2)
->>> builder.add_next_value(1, 2, 0.8)
+builder.new_row_group(0)
+builder.add_next_value(0, 1, 0.5)
+builder.add_next_value(0, 2, 0.5)
+builder.add_next_value(1, 1, 0.2)
+builder.add_next_value(1, 2, 0.8)
[4]:
>>> builder.new_row_group(2)
->>> builder.add_next_value(2, 3, 0.5)
->>> builder.add_next_value(2, 4, 0.5)
->>> builder.new_row_group(3)
->>> builder.add_next_value(3, 5, 0.5)
->>> builder.add_next_value(3, 6, 0.5)
->>> builder.new_row_group(4)
->>> builder.add_next_value(4, 7, 0.5)
->>> builder.add_next_value(4, 1, 0.5)
->>> builder.new_row_group(5)
->>> builder.add_next_value(5, 8, 0.5)
->>> builder.add_next_value(5, 9, 0.5)
->>> builder.new_row_group(6)
->>> builder.add_next_value(6, 10, 0.5)
->>> builder.add_next_value(6, 11, 0.5)
->>> builder.new_row_group(7)
->>> builder.add_next_value(7, 2, 0.5)
->>> builder.add_next_value(7, 12, 0.5)
+builder.new_row_group(2)
+builder.add_next_value(2, 3, 0.5)
+builder.add_next_value(2, 4, 0.5)
+builder.new_row_group(3)
+builder.add_next_value(3, 5, 0.5)
+builder.add_next_value(3, 6, 0.5)
+builder.new_row_group(4)
+builder.add_next_value(4, 7, 0.5)
+builder.add_next_value(4, 1, 0.5)
+builder.new_row_group(5)
+builder.add_next_value(5, 8, 0.5)
+builder.add_next_value(5, 9, 0.5)
+builder.new_row_group(6)
+builder.add_next_value(6, 10, 0.5)
+builder.add_next_value(6, 11, 0.5)
+builder.new_row_group(7)
+builder.add_next_value(7, 2, 0.5)
+builder.add_next_value(7, 12, 0.5)
->>> for s in range(8, 14):
-... builder.new_row_group(s)
-... builder.add_next_value(s, s - 1, 1)
+for s in range(8, 14):
+ builder.new_row_group(s)
+ builder.add_next_value(s, s - 1, 1)
[5]:
>>> transition_matrix = builder.build()
+transition_matrix = builder.build()
[7]:
>>> choice_labeling = stormpy.storage.ChoiceLabeling(14)
->>> choice_labels = {'a', 'b'}
+choice_labeling = stormpy.storage.ChoiceLabeling(14)
+choice_labels = {"a", "b"}
->>> for label in choice_labels:
-... choice_labeling.add_label(label)
+for label in choice_labels:
+ choice_labeling.add_label(label)
[8]:
>>> choice_labeling.add_label_to_choice('a', 0)
->>> choice_labeling.add_label_to_choice('b', 1)
->>> print(choice_labeling)
+choice_labeling.add_label_to_choice("a", 0)
+choice_labeling.add_label_to_choice("b", 1)
+print(choice_labeling)
[9]:
>>> reward_models = {}
->>> action_reward = [0.0, 0.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)
+reward_models = {}
+action_reward = [0.0, 0.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)
[10]:
>>> components = stormpy.SparseModelComponents(transition_matrix=transition_matrix, state_labeling=state_labeling, reward_models=reward_models, rate_transitions=False)
->>> components.choice_labeling = choice_labeling
+components = stormpy.SparseModelComponents(
+ transition_matrix=transition_matrix, state_labeling=state_labeling, reward_models=reward_models, rate_transitions=False
+)
+components.choice_labeling = choice_labeling
[11]:
>>> mdp = stormpy.storage.SparseMdp(components)
->>> print(mdp)
+mdp = stormpy.storage.SparseMdp(components)
+print(mdp)
[1]:
>>> import stormpy
->>> import stormpy.examples
->>> import stormpy.examples.files
->>> path = stormpy.examples.files.prism_pdtmc_die
->>> prism_program = stormpy.parse_prism_program(path)
->>> formula_str = "P=? [F s=7 & d=2]"
->>> properties = stormpy.parse_properties(formula_str, prism_program)
->>> model = stormpy.build_parametric_model(prism_program, properties)
->>> parameters = model.collect_probability_parameters()
->>> for x in parameters:
-... print(x)
+import stormpy
+import stormpy.examples
+import stormpy.examples.files
+
+path = stormpy.examples.files.prism_pdtmc_die
+prism_program = stormpy.parse_prism_program(path)
+formula_str = "P=? [F s=7 & d=2]"
+properties = stormpy.parse_properties(formula_str, prism_program)
+model = stormpy.build_parametric_model(prism_program, properties)
+parameters = model.collect_probability_parameters()
+for x in parameters:
+ print(x)
[2]:
>>> import stormpy.pars
->>> instantiator = stormpy.pars.PDtmcInstantiator(model)
+import stormpy.pars
+
+instantiator = stormpy.pars.PDtmcInstantiator(model)
[3]:
>>> point = dict()
->>> for x in parameters:
-... print(x.name)
-... point[x] = stormpy.RationalRF(0.4)
->>> instantiated_model = instantiator.instantiate(point)
->>> result = stormpy.model_checking(instantiated_model, properties[0])
+point = dict()
+for x in parameters:
+ print(x.name)
+ point[x] = stormpy.RationalRF(0.4)
+instantiated_model = instantiator.instantiate(point)
+result = stormpy.model_checking(instantiated_model, properties[0])
[4]:
>>> result = stormpy.model_checking(model, properties[0])
->>> initial_state = model.initial_states[0]
->>> func = result.at(initial_state)
+result = stormpy.model_checking(model, properties[0])
+initial_state = model.initial_states[0]
+func = result.at(initial_state)
[5]:
>>> import stormpy.info
->>> if stormpy.info.storm_ratfunc_use_cln():
-... import pycarl.cln.formula
->>> else:
-... import pycarl.gmp.formula
->>> collector = stormpy.ConstraintCollector(model)
->>> for formula in collector.wellformed_constraints:
-... print(formula)
->>> for formula in collector.graph_preserving_constraints:
-... print(formula)
+import stormpy.info
+
+if stormpy.info.storm_ratfunc_use_cln():
+ import pycarl.cln.formula
+else:
+ import pycarl.gmp.formula
+collector = stormpy.ConstraintCollector(model)
+for formula in collector.wellformed_constraints:
+ print(formula)
+for formula in collector.graph_preserving_constraints:
+ print(formula)
-(<= (* (- 1) p) 0)
-(<= (* (- 1) q) 0)
(<= (+ p (- 1)) 0)
+(<= (* (- 1) q) 0)
+(<= (* (- 1) p) 0)
(<= (+ q (- 1)) 0)
(!= q 0)
(!= p 0)
-(!= (+ q (- 1)) 0)
(!= (+ p (- 1)) 0)
+(!= (+ q (- 1)) 0)
[1]:
>>> import stormpy
->>> import stormpy.examples
->>> import stormpy.examples.files
->>> program = stormpy.parse_prism_program(stormpy.examples.files.prism_dtmc_die)
->>> prop = "R=? [F \"done\"]"
+import stormpy
+import stormpy.examples
+import stormpy.examples.files
->>> properties = stormpy.parse_properties(prop, program, None)
->>> model = stormpy.build_model(program, properties)
->>> assert len(model.reward_models) == 1
+program = stormpy.parse_prism_program(stormpy.examples.files.prism_dtmc_die)
+prop = 'R=? [F "done"]'
+
+properties = stormpy.parse_properties(prop, program, None)
+model = stormpy.build_model(program, properties)
+assert len(model.reward_models) == 1
[2]:
>>> initial_state = model.initial_states[0]
->>> result = stormpy.model_checking(model, properties[0])
->>> print("Result: {}".format(round(result.at(initial_state), 6)))
+initial_state = model.initial_states[0]
+result = stormpy.model_checking(model, properties[0])
+print("Result: {}".format(round(result.at(initial_state), 6)))
[3]:
>>> reward_model_name = list(model.reward_models.keys())[0]
->>> print(reward_model_name)
+reward_model_name = list(model.reward_models.keys())[0]
+print(reward_model_name)
[4]:
>>> assert not model.reward_models[reward_model_name].has_state_rewards
->>> assert model.reward_models[reward_model_name].has_state_action_rewards
->>> assert not model.reward_models[reward_model_name].has_transition_rewards
->>> for reward in model.reward_models[reward_model_name].state_action_rewards:
-... print(reward)
+assert not model.reward_models[reward_model_name].has_state_rewards
+assert model.reward_models[reward_model_name].has_state_action_rewards
+assert not model.reward_models[reward_model_name].has_transition_rewards
+for reward in model.reward_models[reward_model_name].state_action_rewards:
+ print(reward)
[1]:
>>> import stormpy
->>> import stormpy.examples
->>> import stormpy.examples.files
+import stormpy
+import stormpy.examples
+import stormpy.examples.files
->>> path = stormpy.examples.files.prism_mdp_coin_2_2
->>> formula_str = "Pmin=? [F \"finished\" & \"all_coins_equal_1\"]"
->>> program = stormpy.parse_prism_program(path)
->>> formulas = stormpy.parse_properties(formula_str, program)
->>> options = stormpy.BuilderOptions(True, True)
->>> options.set_build_state_valuations()
->>> options.set_build_choice_labels()
->>> options.set_build_with_choice_origins()
->>> model = stormpy.build_sparse_model_with_options(program, options)
+path = stormpy.examples.files.prism_mdp_coin_2_2
+formula_str = 'Pmin=? [F "finished" & "all_coins_equal_1"]'
+program = stormpy.parse_prism_program(path)
+formulas = stormpy.parse_properties(formula_str, program)
+options = stormpy.BuilderOptions(True, True)
+options.set_build_state_valuations()
+options.set_build_choice_labels()
+options.set_build_with_choice_origins()
+model = stormpy.build_sparse_model_with_options(program, options)
[2]:
>>> result = stormpy.model_checking(model, formulas[0], extract_scheduler=True)
+result = stormpy.model_checking(model, formulas[0], extract_scheduler=True)
[3]:
>>> assert result.has_scheduler
->>> scheduler = result.scheduler
->>> assert scheduler.memoryless
->>> assert scheduler.deterministic
->>> print(scheduler)
+assert result.has_scheduler
+scheduler = result.scheduler
+assert scheduler.memoryless
+assert scheduler.deterministic
+print(scheduler)
[4]:
>>> for state in model.states:
-... choice = scheduler.get_choice(state)
-... action_index = choice.get_deterministic_choice()
-... action = state.actions[action_index]
-... print("In state {} ({}) choose action {} ({})".format(state, ", ".join(state.labels), action, ", ".join(action.labels)))
-... print(state.valuations)
+for state in model.states:
+ choice = scheduler.get_choice(state)
+ action_index = choice.get_deterministic_choice()
+ action = state.actions[action_index]
+ print("In state {} ({}) choose action {} ({})".format(state, ", ".join(state.labels), action, ", ".join(action.labels)))
+ print(state.valuations)
[5]:
>>> path = stormpy.examples.files.prism_ma_simple
->>> formula_str = "Tmin=? [ F s=4 ]"
+path = stormpy.examples.files.prism_ma_simple
+formula_str = "Tmin=? [ F s=4 ]"
->>> program = stormpy.parse_prism_program(path, False, True)
->>> formulas = stormpy.parse_properties_for_prism_program(formula_str, program)
->>> ma = stormpy.build_model(program, formulas)
+program = stormpy.parse_prism_program(path, False, True)
+formulas = stormpy.parse_properties_for_prism_program(formula_str, program)
+ma = stormpy.build_model(program, formulas)
[6]:
>>> mdp, mdp_formulas = stormpy.transform_to_discrete_time_model(ma, formulas)
->>> assert mdp.model_type == stormpy.ModelType.MDP
+mdp, mdp_formulas = stormpy.transform_to_discrete_time_model(ma, formulas)
+assert mdp.model_type == stormpy.ModelType.MDP
[7]:
>>> result = stormpy.model_checking(mdp, mdp_formulas[0], extract_scheduler=True)
->>> scheduler = result.scheduler
->>> print(scheduler)
-
result = stormpy.model_checking(mdp, mdp_formulas[0], extract_scheduler=True)
+scheduler = result.scheduler
+print(scheduler)
+[1]:
>>> import stormpy.examples
->>> import stormpy.examples.files
->>> path = stormpy.examples.files.prism_dtmc_die
->>> prism_program = stormpy.parse_prism_program(path)
->>> model = stormpy.build_model(prism_program)
+import stormpy.examples
+import stormpy.examples.files
+
+path = stormpy.examples.files.prism_dtmc_die
+prism_program = stormpy.parse_prism_program(path)
+model = stormpy.build_model(prism_program)
[2]:
>>> from stormpy.utility import ShortestPathsGenerator
+from stormpy.utility import ShortestPathsGenerator
[3]:
>>> state_id = 8
+state_id = 8
[4]:
>>> spg = ShortestPathsGenerator(model, state_id)
+spg = ShortestPathsGenerator(model, state_id)
[5]:
>>> for k in range(1, 4):
-... path = spg.get_path_as_list(k)
-... distance = spg.get_distance(k)
-... print("{}-shortest path to state #{}: {}, with distance {}".format(k, state_id, path, distance))
+for k in range(1, 4):
+ path = spg.get_path_as_list(k)
+ distance = spg.get_distance(k)
+ print("{}-shortest path to state #{}: {}, with distance {}".format(k, state_id, path, distance))
import random
+
random.seed(23)
path = stormpy.examples.files.prism_mdp_slipgrid
prism_program = stormpy.parse_prism_program(path)
@@ -1175,7 +1176,7 @@ Explicit representationspath = [f"{state}"]
for n in range(20):
actions = simulator.available_actions()
- select_action = random.randint(0,len(actions)-1)
+ select_action = random.randint(0, len(actions) - 1)
path.append(f"--act={actions[select_action]}-->")
state, reward, labels = simulator.step(actions[select_action])
path.append(f"{state}")
@@ -1221,7 +1222,7 @@ Explicit representationspath = [f"({state['x']},{state['y']})"]
for n in range(20):
actions = simulator.available_actions()
- select_action = random.randint(0,len(actions)-1)
+ select_action = random.randint(0, len(actions) - 1)
path.append(f"--{actions[select_action]}-->")
state, reward, labels = simulator.step(actions[select_action])
path.append(f"({state['x']},{state['y']})")
@@ -1269,7 +1270,7 @@ Program-level simulatorpath = [f"({state['x']},{state['y']})"]
for n in range(20):
actions = simulator.available_actions()
- select_action = random.randint(0,len(actions)-1)
+ select_action = random.randint(0, len(actions) - 1)
path.append(f"--{actions[select_action]}-->")
state, reward, labels = simulator.step(actions[select_action])
path.append(f"({state['x']},{state['y']})")
diff --git a/doc/simulator.ipynb b/doc/simulator.ipynb
index 8de0ed56b..c0af024e0 100644
--- a/doc/simulator.ipynb
+++ b/doc/simulator.ipynb
@@ -400,8 +400,8 @@
" final_outcomes[observation] = 1\n",
" else:\n",
" final_outcomes[observation] += 1\n",
- " simulator.restart() \n",
- "print(\", \".join([f\"{str(k)}: {v}\" for k,v in final_outcomes.items()]))"
+ " simulator.restart()\n",
+ "print(\", \".join([f\"{str(k)}: {v}\" for k, v in final_outcomes.items()]))"
]
},
{
@@ -447,6 +447,7 @@
],
"source": [
"import random\n",
+ "\n",
"random.seed(23)\n",
"path = stormpy.examples.files.prism_mdp_slipgrid\n",
"prism_program = stormpy.parse_prism_program(path)\n",
@@ -461,7 +462,7 @@
" path = [f\"{state}\"]\n",
" for n in range(20):\n",
" actions = simulator.available_actions()\n",
- " select_action = random.randint(0,len(actions)-1)\n",
+ " select_action = random.randint(0, len(actions) - 1)\n",
" path.append(f\"--act={actions[select_action]}-->\")\n",
" state, reward, labels = simulator.step(actions[select_action])\n",
" path.append(f\"{state}\")\n",
@@ -513,7 +514,7 @@
" path = [f\"({state['x']},{state['y']})\"]\n",
" for n in range(20):\n",
" actions = simulator.available_actions()\n",
- " select_action = random.randint(0,len(actions)-1)\n",
+ " select_action = random.randint(0, len(actions) - 1)\n",
" path.append(f\"--{actions[select_action]}-->\")\n",
" state, reward, labels = simulator.step(actions[select_action])\n",
" path.append(f\"({state['x']},{state['y']})\")\n",
@@ -571,7 +572,7 @@
" path = [f\"({state['x']},{state['y']})\"]\n",
" for n in range(20):\n",
" actions = simulator.available_actions()\n",
- " select_action = random.randint(0,len(actions)-1)\n",
+ " select_action = random.randint(0, len(actions) - 1)\n",
" path.append(f\"--{actions[select_action]}-->\")\n",
" state, reward, labels = simulator.step(actions[select_action])\n",
" path.append(f\"({state['x']},{state['y']})\")\n",
diff --git a/getting_started.html b/getting_started.html
index 442d78b9c..b0790cc98 100644
--- a/getting_started.html
+++ b/getting_started.html
@@ -865,7 +865,7 @@ A Quick Tour through Stormpy[1]:
>>> import stormpy
+import stormpy
[2]:
>>> import stormpy.examples
->>> import stormpy.examples.files
+import stormpy.examples
+import stormpy.examples.files
[3]:
>>> path = stormpy.examples.files.prism_dtmc_die
->>> prism_program = stormpy.parse_prism_program(path)
+path = stormpy.examples.files.prism_dtmc_die
+prism_program = stormpy.parse_prism_program(path)
[4]:
>>> model = stormpy.build_model(prism_program)
->>> print("Number of states: {}".format(model.nr_states))
+model = stormpy.build_model(prism_program)
+print("Number of states: {}".format(model.nr_states))
[5]:
>>> print("Number of transitions: {}".format(model.nr_transitions))
+print("Number of transitions: {}".format(model.nr_transitions))
[6]:
>>> print("Labels: {}".format(model.labeling.get_labels()))
+print("Labels: {}".format(model.labeling.get_labels()))
-Labels: {'three', 'six', 'five', 'two', 'one', 'init', 'deadlock', 'four', 'done'}
+Labels: {'done', 'two', 'five', 'four', 'three', 'one', 'deadlock', 'six', 'init'}
We will investigate ways to examine the model in more detail later in Investigating the model.
@@ -959,8 +959,8 @@[7]:
>>> formula_str = "P=? [F s=2]"
->>> properties = stormpy.parse_properties(formula_str, prism_program)
+formula_str = "P=? [F s=2]"
+properties = stormpy.parse_properties(formula_str, prism_program)
[8]:
>>> model = stormpy.build_model(prism_program, properties)
->>> print("Labels in the model: {}".format(sorted(model.labeling.get_labels())))
+model = stormpy.build_model(prism_program, properties)
+print("Labels in the model: {}".format(sorted(model.labeling.get_labels())))
[9]:
>>> print("Number of states: {}".format(model.nr_states))
+print("Number of states: {}".format(model.nr_states))
[10]:
>>> properties = stormpy.parse_properties(formula_str, prism_program)
->>> model = stormpy.build_model(prism_program, properties)
->>> result = stormpy.model_checking(model, properties[0])
+properties = stormpy.parse_properties(formula_str, prism_program)
+model = stormpy.build_model(prism_program, properties)
+result = stormpy.model_checking(model, properties[0])
[11]:
>>> assert result.result_for_all_states
->>> for x in result.get_values():
-... pass # do something with x
+assert result.result_for_all_states
+for x in result.get_values():
+ pass # do something with x
[12]:
>>> initial_state = model.initial_states[0]
->>> print(result.at(initial_state))
+initial_state = model.initial_states[0]
+print(result.at(initial_state))
[13]:
>>> path = stormpy.examples.files.prism_dtmc_die
->>> prism_program = stormpy.parse_prism_program(path)
->>> model = stormpy.build_model(prism_program)
+path = stormpy.examples.files.prism_dtmc_die
+prism_program = stormpy.parse_prism_program(path)
+model = stormpy.build_model(prism_program)
[14]:
>>> print(model.model_type)
+print(model.model_type)
[15]:
>>> for state in model.states:
-... for action in state.actions:
-... for transition in action.transitions:
-... print("From state {}, with probability {}, go to state {}".format(state, transition.value(), transition.column))
+for state in model.states:
+ for action in state.actions:
+ for transition in action.transitions:
+ print("From state {}, with probability {}, go to state {}".format(state, transition.value(), transition.column))
[16]:
>>> for state in model.states:
-... assert len(state.actions) <= 1
+for state in model.states:
+ assert len(state.actions) <= 1
[17]:
>>> for state in model.states:
-... if state.id in model.initial_states:
-... pass
+for state in model.states:
+ if state.id in model.initial_states:
+ pass