From 534f29c9e329007d67428da3ef7be84141140fe2 Mon Sep 17 00:00:00 2001 From: Auto Format Date: Tue, 19 Nov 2024 09:38:50 +0000 Subject: [PATCH 1/2] Applied code formatting --- doc/source/conf.py | 99 ++--- doc/source/doc/analysis.ipynb | 41 +- doc/source/doc/building_models.ipynb | 24 +- doc/source/doc/dfts.ipynb | 33 +- doc/source/doc/engines.ipynb | 55 +-- doc/source/doc/exploration.ipynb | 55 +-- doc/source/doc/gspns.ipynb | 64 +-- doc/source/doc/models/building_ctmcs.ipynb | 43 +- doc/source/doc/models/building_dtmcs.ipynb | 78 ++-- doc/source/doc/models/building_mas.ipynb | 29 +- doc/source/doc/models/building_mdps.ipynb | 112 ++--- doc/source/doc/parametric_models.ipynb | 67 +-- doc/source/doc/reward_models.ipynb | 37 +- doc/source/doc/schedulers.ipynb | 68 +-- doc/source/doc/shortest_paths.ipynb | 25 +- doc/source/doc/simulator.ipynb | 11 +- doc/source/getting_started.ipynb | 70 +-- examples/01-getting-started.py | 2 +- examples/02-getting-started.py | 2 +- examples/03-getting-started.py | 2 +- examples/04-getting-started.py | 5 +- examples/analysis/01-analysis.py | 3 +- examples/analysis/02-analysis.py | 19 +- examples/analysis/03-analysis.py | 5 +- examples/analysis/04-analysis.py | 11 +- examples/building_ctmcs/01-building-ctmcs.py | 25 +- examples/building_dtmcs/01-building-dtmcs.py | 30 +- examples/building_mas/01-building-mas.py | 25 +- examples/building_mdps/01-building-mdps.py | 36 +- .../building_models/01-building-models.py | 4 +- .../building_models/02-building-models.py | 12 +- .../building_models/03-building-models.py | 3 +- .../building_models/04-building-models.py | 9 +- examples/dfts/01-dfts.py | 4 +- examples/dfts/02-dfts.py | 5 +- examples/dfts/interactive_simulator.py | 16 +- examples/exploration/01-exploration.py | 8 +- examples/exploration/02-exploration.py | 8 +- examples/exploration/03-exploration.py | 3 +- examples/gspns/01-gspns.py | 2 +- examples/gspns/02-gspns.py | 3 +- .../highlevel_models/01-highlevel-models.py | 2 +- .../highlevel_models/02-highlevel-models.py | 17 +- .../parametric_models/01-parametric-models.py | 3 +- .../parametric_models/02-parametric-models.py | 3 +- .../parametric_models/03-parametric-models.py | 10 +- .../parametric_models/04-parametric-models.py | 4 +- examples/pomdp/01-pomdps.py | 8 +- examples/pomdp/high-level-observations.py | 5 +- examples/reward_models/01-reward-models.py | 5 +- examples/schedulers/01-schedulers.py | 5 +- examples/schedulers/02-schedulers.py | 4 +- examples/shortest_paths/01-shortest-paths.py | 2 +- examples/simulator/01-simulator.py | 9 +- examples/simulator/02-simulator.py | 21 +- examples/simulator/03-simulator.py | 5 +- examples/simulator/04-simulator.py | 7 +- lib/stormpy/__init__.py | 29 +- lib/stormpy/dft/modules.py | 10 +- lib/stormpy/pomdp/__init__.py | 6 +- lib/stormpy/simulator.py | 36 +- .../utility/multiobjective_plotting.py | 13 +- setup.py | 133 +++--- setup/__init__.py | 2 +- setup/config.py | 4 +- setup/helper.py | 5 +- tests/configurations.py | 3 + tests/conftest.py | 2 +- tests/core/test_bisimulation.py | 6 +- tests/core/test_building.py | 10 +- tests/core/test_core.py | 1 + tests/core/test_environment.py | 1 + tests/core/test_modelchecking.py | 37 +- tests/core/test_multiobjective.py | 21 +- tests/core/test_parse.py | 10 +- tests/core/test_transformation.py | 11 +- tests/dft/test_analysis.py | 18 +- tests/dft/test_dft.py | 4 +- tests/dft/test_dft_simulator.py | 2 +- tests/dft/test_io.py | 3 +- tests/dft/test_module.py | 14 +- tests/dft/test_transformations.py | 1 - tests/gspn/test_gspn_io.py | 4 +- tests/info/test_info.py | 3 +- tests/logic/test_formulas.py | 22 +- tests/pars/test_model_instantiator.py | 6 +- tests/pars/test_parametric.py | 5 +- tests/pars/test_parametric_model.py | 12 +- .../pomdp/test_pomdp_quantitative_analysis.py | 9 +- tests/simulator/test_simulator.py | 4 +- tests/storage/test_labeling.py | 3 +- tests/storage/test_matrix.py | 24 +- tests/storage/test_matrix_builder.py | 47 +- tests/storage/test_model.py | 25 +- tests/storage/test_model_components.py | 413 +++++++++--------- tests/storage/test_prism.py | 9 +- tests/storage/test_scheduler.py | 6 +- tests/storage/test_state.py | 100 +++-- tests/storage/test_state_generation.py | 6 +- tests/utility/test_shortestpaths.py | 3 +- tests/utility/test_smtsolver.py | 5 +- 101 files changed, 1212 insertions(+), 1139 deletions(-) diff --git a/doc/source/conf.py b/doc/source/conf.py index 883ed19e6..52b1d3649 100644 --- a/doc/source/conf.py +++ b/doc/source/conf.py @@ -25,7 +25,6 @@ import sphinx_bootstrap_theme - # -- General configuration ------------------------------------------------ # If your documentation needs a minimal Sphinx version, state it here. @@ -36,33 +35,33 @@ # extensions coming with Sphinx (named 'sphinx.ext.*') or your custom # ones. extensions = [ - 'sphinx.ext.autodoc', - 'sphinx.ext.doctest', + "sphinx.ext.autodoc", + "sphinx.ext.doctest", #'sphinx.ext.intersphinx', - 'sphinx.ext.coverage', - 'sphinx.ext.githubpages', - 'sphinx.ext.autosectionlabel', - 'nbsphinx' + "sphinx.ext.coverage", + "sphinx.ext.githubpages", + "sphinx.ext.autosectionlabel", + "nbsphinx", ] autosectionlabel_prefix_document = True -#autosectionlabel_maxdepth = 10 +# autosectionlabel_maxdepth = 10 # Add any paths that contain templates here, relative to this directory. -templates_path = ['_templates'] +templates_path = ["_templates"] # The suffix(es) of source filenames. # You can specify multiple suffix as a list of string: # # source_suffix = ['.rst', '.md'] -source_suffix = '.rst' +source_suffix = ".rst" # The master toctree document. -master_doc = 'index' +master_doc = "index" # General information about the project. -project = 'stormpy' -copyright = '2016-2022 Moves RWTH Aachen' -author = 'Sebastian Junges, Matthias Volk' +project = "stormpy" +copyright = "2016-2022 Moves RWTH Aachen" +author = "Sebastian Junges, Matthias Volk" # The version info for the project you're documenting, acts as replacement for # |version| and |release|, also used in various other places throughout the @@ -78,7 +77,7 @@ # # This is also used if you do content translation via gettext catalogs. # Usually you set "language" from the command line for these cases. -language = 'en' +language = "en" # List of patterns, relative to source directory, that match files and # directories to ignore when looking for source files. @@ -86,7 +85,7 @@ exclude_patterns = [] # The name of the Pygments (syntax highlighting) style to use. -pygments_style = 'sphinx' +pygments_style = "sphinx" # If true, `todo` and `todoList` produce output, else they produce nothing. todo_include_todos = False @@ -100,7 +99,7 @@ # The theme to use for HTML and HTML Help pages. See the documentation for # a list of builtin themes. # -html_theme = 'fixedbootstrap' +html_theme = "fixedbootstrap" html_theme_path = ["themes"] + sphinx_bootstrap_theme.get_html_theme_path() @@ -111,11 +110,9 @@ html_theme_options = { # Navigation bar title. (Default: ``project`` value) - 'navbar_title': "Stormpy", - + "navbar_title": "Stormpy", # Tab name for entire site. (Default: "Site") - 'navbar_site_name': "Stormpy", - + "navbar_site_name": "Stormpy", # A list of tuples containing pages or urls to link to. # Valid tuples should be in the following forms: # (name, page) # a link to a page @@ -123,24 +120,16 @@ # (name, "http://example.com", True) # arbitrary absolute url # Note the "1" or "True" value above as the third argument to indicate # an arbitrary url. - 'navbar_links': [ - ("Storm", "https://www.stormchecker.org", True), - ("Github", "https://github.com/moves-rwth/stormpy", True) - ], - + "navbar_links": [("Storm", "https://www.stormchecker.org", True), ("Github", "https://github.com/moves-rwth/stormpy", True)], # Render the next and previous page links in navbar. (Default: true) - 'navbar_sidebarrel': True, - + "navbar_sidebarrel": True, # Render the current pages TOC in the navbar. (Default: true) - 'navbar_pagenav': True, - + "navbar_pagenav": True, # Tab name for the current pages TOC. (Default: "Page") - 'navbar_pagenav_name': "Page", - + "navbar_pagenav_name": "Page", # Global TOC depth for "site" navbar tab. (Default: 1) # Switching to -1 shows all levels. - 'globaltoc_depth': 2, - + "globaltoc_depth": 2, # Include hidden TOCs in Site navbar? # # Note: If this is "false", you cannot have mixed ``:hidden:`` and @@ -148,43 +137,38 @@ # will break. # # Values: "true" (default) or "false" - 'globaltoc_includehidden': "true", - + "globaltoc_includehidden": "true", # HTML navbar class (Default: "navbar") to attach to
element. # For black navbar, do "navbar navbar-inverse" - 'navbar_class': "navbar navbar-inverse", - + "navbar_class": "navbar navbar-inverse", # Fix navigation bar to top of page? # Values: "true" (default) or "false" - 'navbar_fixed_top': "true", - + "navbar_fixed_top": "true", # Location of link to source. # Options are "nav" (default), "footer" or anything else to exclude. - 'source_link_position': "footer", - + "source_link_position": "footer", # Bootswatch (http://bootswatch.com/) theme. # # Options are nothing (default) or the name of a valid theme # such as "cosmo" or "sandstone". - 'bootswatch_theme': "united", - + "bootswatch_theme": "united", # Choose Bootstrap version. # Values: "3" (default) or "2" (in quotes) - 'bootstrap_version': "3", + "bootstrap_version": "3", } -html_sidebars = {'**': ['localtoc.html']} +html_sidebars = {"**": ["localtoc.html"]} # Add any paths that contain custom static files (such as style sheets) here, # relative to this directory. They are copied after the builtin static files, # so a file named "default.css" will overwrite the builtin "default.css". -html_static_path = ['_static'] +html_static_path = ["_static"] # -- Options for HTMLHelp output ------------------------------------------ # Output file base name for HTML help builder. -htmlhelp_basename = 'stormpydoc' +htmlhelp_basename = "stormpydoc" # -- Options for LaTeX output --------------------------------------------- @@ -193,15 +177,12 @@ # The paper size ('letterpaper' or 'a4paper'). # # 'papersize': 'letterpaper', - # The font size ('10pt', '11pt' or '12pt'). # # 'pointsize': '10pt', - # Additional stuff for the LaTeX preamble. # # 'preamble': '', - # Latex figure (float) alignment # # 'figure_align': 'htbp', @@ -211,8 +192,7 @@ # (source start file, target name, title, # author, documentclass [howto, manual, or own class]). latex_documents = [ - (master_doc, 'stormpy.tex', 'stormpy Documentation', - 'Sebastian Junges, Matthias Volk', 'manual'), + (master_doc, "stormpy.tex", "stormpy Documentation", "Sebastian Junges, Matthias Volk", "manual"), ] @@ -220,10 +200,7 @@ # One entry per manual page. List of tuples # (source start file, name, description, authors, manual section). -man_pages = [ - (master_doc, 'stormpy', 'stormpy Documentation', - [author], 1) -] +man_pages = [(master_doc, "stormpy", "stormpy Documentation", [author], 1)] # -- Options for Texinfo output ------------------------------------------- @@ -232,16 +209,12 @@ # (source start file, target name, title, author, # dir menu entry, description, category) texinfo_documents = [ - (master_doc, 'stormpy', 'stormpy Documentation', - author, 'stormpy', 'Python bindings for Storm.', - 'Miscellaneous'), + (master_doc, "stormpy", "stormpy Documentation", author, "stormpy", "Python bindings for Storm.", "Miscellaneous"), ] - - # Example configuration for intersphinx: refer to the Python standard library. -intersphinx_mapping = {'https://docs.python.org/': None} +intersphinx_mapping = {"https://docs.python.org/": None} nbsphinx_prolog = """ {% set docname = env.doc2path(env.docname, base=False) %} diff --git a/doc/source/doc/analysis.ipynb b/doc/source/doc/analysis.ipynb index 151d82632..380cad415 100644 --- a/doc/source/doc/analysis.ipynb +++ b/doc/source/doc/analysis.ipynb @@ -26,13 +26,14 @@ }, "outputs": [], "source": [ - ">>> import stormpy\n", - ">>> import stormpy.examples\n", - ">>> import stormpy.examples.files\n", - ">>> path = stormpy.examples.files.prism_dtmc_die\n", - ">>> prism_program = stormpy.parse_prism_program(path)\n", - ">>> formula_str = \"P=? [F s=7 & d=2]\"\n", - ">>> properties = stormpy.parse_properties(formula_str, prism_program)" + "import stormpy\n", + "import stormpy.examples\n", + "import stormpy.examples.files\n", + "\n", + "path = stormpy.examples.files.prism_dtmc_die\n", + "prism_program = stormpy.parse_prism_program(path)\n", + "formula_str = \"P=? [F s=7 & d=2]\"\n", + "properties = stormpy.parse_properties(formula_str, prism_program)" ] }, { @@ -61,8 +62,8 @@ }, "outputs": [], "source": [ - ">>> model = stormpy.build_symbolic_model(prism_program, properties)\n", - ">>> result = stormpy.model_checking(model, properties[0])" + "model = stormpy.build_symbolic_model(prism_program, properties)\n", + "result = stormpy.model_checking(model, properties[0])" ] }, { @@ -80,9 +81,9 @@ }, "outputs": [], "source": [ - ">>> filter = stormpy.create_filter_initial_states_symbolic(model)\n", - ">>> result.filter(filter)\n", - ">>> assert result.min == result.max" + "filter = stormpy.create_filter_initial_states_symbolic(model)\n", + "result.filter(filter)\n", + "assert result.min == result.max" ] }, { @@ -114,8 +115,8 @@ }, "outputs": [], "source": [ - ">>> model = stormpy.build_model(prism_program, properties)\n", - ">>> result = stormpy.model_checking(model, properties[0])" + "model = stormpy.build_model(prism_program, properties)\n", + "result = stormpy.model_checking(model, properties[0])" ] }, { @@ -133,10 +134,10 @@ }, "outputs": [], "source": [ - ">>> env = stormpy.Environment()\n", - ">>> env.solver_environment.set_linear_equation_solver_type(stormpy.EquationSolverType.native)\n", - ">>> env.solver_environment.native_solver_environment.method = stormpy.NativeLinearEquationSolverMethod.power_iteration\n", - ">>> result = stormpy.model_checking(model, properties[0], environment=env)" + "env = stormpy.Environment()\n", + "env.solver_environment.set_linear_equation_solver_type(stormpy.EquationSolverType.native)\n", + "env.solver_environment.native_solver_environment.method = stormpy.NativeLinearEquationSolverMethod.power_iteration\n", + "result = stormpy.model_checking(model, properties[0], environment=env)" ] }, { @@ -155,8 +156,8 @@ }, "outputs": [], "source": [ - ">>> env.solver_environment.native_solver_environment.maximum_iterations = 3\n", - ">>> result = stormpy.model_checking(model, properties[0])" + "env.solver_environment.native_solver_environment.maximum_iterations = 3\n", + "result = stormpy.model_checking(model, properties[0])" ] }, { diff --git a/doc/source/doc/building_models.ipynb b/doc/source/doc/building_models.ipynb index 8ce6c116b..9b21f9451 100644 --- a/doc/source/doc/building_models.ipynb +++ b/doc/source/doc/building_models.ipynb @@ -34,8 +34,8 @@ }, "outputs": [], "source": [ - ">>> import stormpy.examples\n", - ">>> import stormpy.examples.files" + "import stormpy.examples\n", + "import stormpy.examples.files" ] }, { @@ -54,9 +54,9 @@ }, "outputs": [], "source": [ - ">>> path = stormpy.examples.files.drn_ctmc_dft\n", - ">>> model = stormpy.build_model_from_drn(path)\n", - ">>> print(model.model_type)" + "path = stormpy.examples.files.drn_ctmc_dft\n", + "model = stormpy.build_model_from_drn(path)\n", + "print(model.model_type)" ] }, { @@ -74,9 +74,9 @@ }, "outputs": [], "source": [ - ">>> path = stormpy.examples.files.drn_pdtmc_die\n", - ">>> model = stormpy.build_parametric_model_from_drn(path)\n", - ">>> print(model.model_type)" + "path = stormpy.examples.files.drn_pdtmc_die\n", + "model = stormpy.build_parametric_model_from_drn(path)\n", + "print(model.model_type)" ] }, { @@ -95,10 +95,10 @@ }, "outputs": [], "source": [ - ">>> path = stormpy.examples.files.jani_dtmc_die\n", - ">>> jani_program, properties = stormpy.parse_jani_model(path)\n", - ">>> model = stormpy.build_model(jani_program)\n", - ">>> print(model.model_type)" + "path = stormpy.examples.files.jani_dtmc_die\n", + "jani_program, properties = stormpy.parse_jani_model(path)\n", + "model = stormpy.build_model(jani_program)\n", + "print(model.model_type)" ] }, { diff --git a/doc/source/doc/dfts.ipynb b/doc/source/doc/dfts.ipynb index e1e253f61..0b7d3697c 100644 --- a/doc/source/doc/dfts.ipynb +++ b/doc/source/doc/dfts.ipynb @@ -29,13 +29,14 @@ }, "outputs": [], "source": [ - ">>> import stormpy\n", - ">>> import stormpy.dft\n", - ">>> import stormpy.examples\n", - ">>> import stormpy.examples.files\n", - ">>> path_json = stormpy.examples.files.dft_json_and\n", - ">>> dft_small = stormpy.dft.load_dft_json_file(path_json)\n", - ">>> print(dft_small)" + "import stormpy\n", + "import stormpy.dft\n", + "import stormpy.examples\n", + "import stormpy.examples.files\n", + "\n", + "path_json = stormpy.examples.files.dft_json_and\n", + "dft_small = stormpy.dft.load_dft_json_file(path_json)\n", + "print(dft_small)" ] }, { @@ -53,8 +54,8 @@ }, "outputs": [], "source": [ - ">>> path_galileo = stormpy.examples.files.dft_galileo_hecs\n", - ">>> dft = stormpy.dft.load_dft_galileo_file(path_galileo)" + "path_galileo = stormpy.examples.files.dft_galileo_hecs\n", + "dft = stormpy.dft.load_dft_galileo_file(path_galileo)" ] }, { @@ -72,8 +73,8 @@ }, "outputs": [], "source": [ - ">>> print(\"DFT with {} elements.\".format(dft.nr_elements()))\n", - ">>> print(\"DFT has {} BEs and {} dynamic elements.\".format(dft.nr_be(), dft.nr_dynamic()))" + "print(\"DFT with {} elements.\".format(dft.nr_elements()))\n", + "print(\"DFT has {} BEs and {} dynamic elements.\".format(dft.nr_be(), dft.nr_dynamic()))" ] }, { @@ -97,11 +98,11 @@ }, "outputs": [], "source": [ - ">>> formula_str = \"T=? [ F \\\"failed\\\" ]\"\n", - ">>> formulas = stormpy.parse_properties(formula_str)\n", - ">>> results = stormpy.dft.analyze_dft(dft, [formulas[0].raw_formula])\n", - ">>> result = results[0]\n", - ">>> print(\"MTTF: {:.2f}\".format(result))" + "formula_str = 'T=? [ F \"failed\" ]'\n", + "formulas = stormpy.parse_properties(formula_str)\n", + "results = stormpy.dft.analyze_dft(dft, [formulas[0].raw_formula])\n", + "result = results[0]\n", + "print(\"MTTF: {:.2f}\".format(result))" ] } ], diff --git a/doc/source/doc/engines.ipynb b/doc/source/doc/engines.ipynb index 861feef8f..29ce14b3d 100644 --- a/doc/source/doc/engines.ipynb +++ b/doc/source/doc/engines.ipynb @@ -31,12 +31,13 @@ "metadata": {}, "outputs": [], "source": [ - ">>> import stormpy.examples\n", - ">>> import stormpy.examples.files\n", - ">>> prism_program = stormpy.parse_prism_program(stormpy.examples.files.prism_dtmc_die)\n", - ">>> properties = stormpy.parse_properties('P=? [F \"one\"]', prism_program)\n", - ">>> sparse_model = stormpy.build_sparse_model(prism_program, properties)\n", - ">>> print(type(sparse_model))\n" + "import stormpy.examples\n", + "import stormpy.examples.files\n", + "\n", + "prism_program = stormpy.parse_prism_program(stormpy.examples.files.prism_dtmc_die)\n", + "properties = stormpy.parse_properties('P=? [F \"one\"]', prism_program)\n", + "sparse_model = stormpy.build_sparse_model(prism_program, properties)\n", + "print(type(sparse_model))" ] }, { @@ -55,7 +56,7 @@ "metadata": {}, "outputs": [], "source": [ - ">>> print(\"Number of transitions: {}\".format(sparse_model.nr_transitions))" + "print(\"Number of transitions: {}\".format(sparse_model.nr_transitions))" ] }, { @@ -64,9 +65,9 @@ "metadata": {}, "outputs": [], "source": [ - ">>> sparse_result = stormpy.check_model_sparse(sparse_model, properties[0])\n", - ">>> initial_state = sparse_model.initial_states[0]\n", - ">>> print(sparse_result.at(initial_state))" + "sparse_result = stormpy.check_model_sparse(sparse_model, properties[0])\n", + "initial_state = sparse_model.initial_states[0]\n", + "print(sparse_result.at(initial_state))" ] }, { @@ -85,8 +86,8 @@ "metadata": {}, "outputs": [], "source": [ - ">>> symbolic_model = stormpy.build_symbolic_model(prism_program, properties)\n", - ">>> print(type(symbolic_model))" + "symbolic_model = stormpy.build_symbolic_model(prism_program, properties)\n", + "print(type(symbolic_model))" ] }, { @@ -95,7 +96,7 @@ "metadata": {}, "outputs": [], "source": [ - ">>> print(\"Number of states: {}\".format(symbolic_model.nr_states))" + "print(\"Number of states: {}\".format(symbolic_model.nr_states))" ] }, { @@ -104,7 +105,7 @@ "metadata": {}, "outputs": [], "source": [ - ">>> print(\"Number of transitions: {}\".format(symbolic_model.nr_transitions))" + "print(\"Number of transitions: {}\".format(symbolic_model.nr_transitions))" ] }, { @@ -113,8 +114,8 @@ "metadata": {}, "outputs": [], "source": [ - ">>> symbolic_result = stormpy.check_model_dd(symbolic_model, properties[0])\n", - ">>> print(symbolic_result)" + "symbolic_result = stormpy.check_model_dd(symbolic_model, properties[0])\n", + "print(symbolic_result)" ] }, { @@ -130,9 +131,9 @@ "metadata": {}, "outputs": [], "source": [ - ">>> filter = stormpy.create_filter_initial_states_symbolic(symbolic_model)\n", - ">>> symbolic_result.filter(filter)\n", - ">>> print(symbolic_result.min)" + "filter = stormpy.create_filter_initial_states_symbolic(symbolic_model)\n", + "symbolic_result.filter(filter)\n", + "print(symbolic_result.min)" ] }, { @@ -148,7 +149,7 @@ "metadata": {}, "outputs": [], "source": [ - ">>> print(type(symbolic_model))" + "print(type(symbolic_model))" ] }, { @@ -157,8 +158,8 @@ "metadata": {}, "outputs": [], "source": [ - ">>> transformed_model = stormpy.transform_to_sparse_model(symbolic_model)\n", - ">>> print(type(transformed_model))" + "transformed_model = stormpy.transform_to_sparse_model(symbolic_model)\n", + "print(type(transformed_model))" ] }, { @@ -178,7 +179,7 @@ "metadata": {}, "outputs": [], "source": [ - ">>> print(type(symbolic_model))" + "print(type(symbolic_model))" ] }, { @@ -187,10 +188,10 @@ "metadata": {}, "outputs": [], "source": [ - ">>> hybrid_result = stormpy.check_model_hybrid(symbolic_model, properties[0])\n", - ">>> filter = stormpy.create_filter_initial_states_symbolic(symbolic_model)\n", - ">>> hybrid_result.filter(filter)\n", - ">>> print(hybrid_result)" + "hybrid_result = stormpy.check_model_hybrid(symbolic_model, properties[0])\n", + "filter = stormpy.create_filter_initial_states_symbolic(symbolic_model)\n", + "hybrid_result.filter(filter)\n", + "print(hybrid_result)" ] } ], diff --git a/doc/source/doc/exploration.ipynb b/doc/source/doc/exploration.ipynb index 57378d84d..39e231195 100644 --- a/doc/source/doc/exploration.ipynb +++ b/doc/source/doc/exploration.ipynb @@ -38,16 +38,18 @@ }, "outputs": [], "source": [ - ">>> import doctest\n", - ">>> doctest.ELLIPSIS_MARKER = '-etc-' \n", - ">>> import stormpy\n", - ">>> import stormpy.examples\n", - ">>> import stormpy.examples.files\n", - ">>> program = stormpy.parse_prism_program(stormpy.examples.files.prism_mdp_maze)\n", - ">>> prop = \"R=? [F \\\"goal\\\"]\"\n", + "import doctest\n", "\n", - ">>> properties = stormpy.parse_properties_for_prism_program(prop, program, None)\n", - ">>> model = stormpy.build_model(program, properties)" + "doctest.ELLIPSIS_MARKER = \"-etc-\"\n", + "import stormpy\n", + "import stormpy.examples\n", + "import stormpy.examples.files\n", + "\n", + "program = stormpy.parse_prism_program(stormpy.examples.files.prism_mdp_maze)\n", + "prop = 'R=? [F \"goal\"]'\n", + "\n", + "properties = stormpy.parse_properties_for_prism_program(prop, program, None)\n", + "model = stormpy.build_model(program, properties)" ] }, { @@ -66,12 +68,12 @@ }, "outputs": [], "source": [ - ">>> for state in model.states:\n", - "... if state.id in model.initial_states:\n", - "... print(\"State {} is initial\".format(state.id))\n", - "... for action in state.actions:\n", - "... for transition in action.transitions:\n", - "... print(\"From state {} by action {}, with probability {}, go to state {}\".format(state, action, transition.value(), transition.column))" + "for state in model.states:\n", + " if state.id in model.initial_states:\n", + " print(\"State {} is initial\".format(state.id))\n", + " for action in state.actions:\n", + " for transition in action.transitions:\n", + " print(\"From state {} by action {}, with probability {}, go to state {}\".format(state, action, transition.value(), transition.column))" ] }, { @@ -104,13 +106,14 @@ }, "outputs": [], "source": [ - ">>> import stormpy\n", - ">>> import stormpy.examples\n", - ">>> import stormpy.examples.files\n", - ">>> program = stormpy.parse_prism_program(stormpy.examples.files.prism_pomdp_maze)\n", - ">>> prop = \"R=? [F \\\"goal\\\"]\"\n", - ">>> properties = stormpy.parse_properties_for_prism_program(prop, program, None)\n", - ">>> model = stormpy.build_model(program, properties)" + "import stormpy\n", + "import stormpy.examples\n", + "import stormpy.examples.files\n", + "\n", + "program = stormpy.parse_prism_program(stormpy.examples.files.prism_pomdp_maze)\n", + "prop = 'R=? [F \"goal\"]'\n", + "properties = stormpy.parse_properties_for_prism_program(prop, program, None)\n", + "model = stormpy.build_model(program, properties)" ] }, { @@ -130,7 +133,7 @@ }, "outputs": [], "source": [ - ">>> print(model.model_type)" + "print(model.model_type)" ] }, { @@ -149,9 +152,9 @@ }, "outputs": [], "source": [ - ">>> print(model.nr_observations)\n", - ">>> for state in model.states:\n", - "... print(\"State {} has observation id {}\".format(state.id, model.observations[state.id]))" + "print(model.nr_observations)\n", + "for state in model.states:\n", + " print(\"State {} has observation id {}\".format(state.id, model.observations[state.id]))" ] }, { diff --git a/doc/source/doc/gspns.ipynb b/doc/source/doc/gspns.ipynb index d7fa99d2c..c24fc3199 100644 --- a/doc/source/doc/gspns.ipynb +++ b/doc/source/doc/gspns.ipynb @@ -27,14 +27,14 @@ }, "outputs": [], "source": [ - ">>> import stormpy\n", - ">>> import stormpy.gspn\n", - ">>> import stormpy.examples\n", - ">>> import stormpy.examples.files\n", + "import stormpy\n", + "import stormpy.gspn\n", + "import stormpy.examples\n", + "import stormpy.examples.files\n", "\n", - ">>> import_path = stormpy.examples.files.gspn_pnml_simple\n", - ">>> gspn_parser = stormpy.gspn.GSPNParser()\n", - ">>> gspn = gspn_parser.parse(import_path)" + "import_path = stormpy.examples.files.gspn_pnml_simple\n", + "gspn_parser = stormpy.gspn.GSPNParser()\n", + "gspn = gspn_parser.parse(import_path)" ] }, { @@ -52,7 +52,7 @@ }, "outputs": [], "source": [ - ">>> print(\"Name of GSPN: {}.\".format(gspn.get_name()))" + "print(\"Name of GSPN: {}.\".format(gspn.get_name()))" ] }, { @@ -61,7 +61,7 @@ "metadata": {}, "outputs": [], "source": [ - ">>> print(\"Number of places: {}.\".format(gspn.get_number_of_places()))" + "print(\"Number of places: {}.\".format(gspn.get_number_of_places()))" ] }, { @@ -70,7 +70,7 @@ "metadata": {}, "outputs": [], "source": [ - ">>> print(\"Number of immediate transitions: {}.\".format(gspn.get_number_of_immediate_transitions()))" + "print(\"Number of immediate transitions: {}.\".format(gspn.get_number_of_immediate_transitions()))" ] }, { @@ -79,7 +79,7 @@ "metadata": {}, "outputs": [], "source": [ - ">>> print(\"Number of timed transitions: {}.\".format(gspn.get_number_of_timed_transitions()))" + "print(\"Number of timed transitions: {}.\".format(gspn.get_number_of_timed_transitions()))" ] }, { @@ -102,8 +102,8 @@ }, "outputs": [], "source": [ - ">>> builder = stormpy.gspn.GSPNBuilder()\n", - ">>> builder.set_name(\"my_gspn\")" + "builder = stormpy.gspn.GSPNBuilder()\n", + "builder.set_name(\"my_gspn\")" ] }, { @@ -122,9 +122,9 @@ }, "outputs": [], "source": [ - ">>> it_1 = builder.add_immediate_transition(1, 0.0, \"it_1\")\n", - ">>> it_layout = stormpy.gspn.LayoutInfo(1.5, 2.0)\n", - ">>> builder.set_transition_layout_info(it_1, it_layout)" + "it_1 = builder.add_immediate_transition(1, 0.0, \"it_1\")\n", + "it_layout = stormpy.gspn.LayoutInfo(1.5, 2.0)\n", + "builder.set_transition_layout_info(it_1, it_layout)" ] }, { @@ -142,9 +142,9 @@ }, "outputs": [], "source": [ - ">>> tt_1 = builder.add_timed_transition(0, 0.4, \"tt_1\")\n", - ">>> tt_layout = stormpy.gspn.LayoutInfo(12.5, 2.0)\n", - ">>> builder.set_transition_layout_info(tt_1, tt_layout)" + "tt_1 = builder.add_timed_transition(0, 0.4, \"tt_1\")\n", + "tt_layout = stormpy.gspn.LayoutInfo(12.5, 2.0)\n", + "builder.set_transition_layout_info(tt_1, tt_layout)" ] }, { @@ -162,13 +162,13 @@ }, "outputs": [], "source": [ - ">>> place_1 = builder.add_place(1, 1, \"place_1\")\n", - ">>> p1_layout = stormpy.gspn.LayoutInfo(6.5, 2.0)\n", - ">>> builder.set_place_layout_info(place_1, p1_layout)\n", + "place_1 = builder.add_place(1, 1, \"place_1\")\n", + "p1_layout = stormpy.gspn.LayoutInfo(6.5, 2.0)\n", + "builder.set_place_layout_info(place_1, p1_layout)\n", "\n", - ">>> place_2 = builder.add_place(1, 0, \"place_2\")\n", - ">>> p2_layout = stormpy.gspn.LayoutInfo(18.5, 2.0)\n", - ">>> builder.set_place_layout_info(place_2, p2_layout)" + "place_2 = builder.add_place(1, 0, \"place_2\")\n", + "p2_layout = stormpy.gspn.LayoutInfo(18.5, 2.0)\n", + "builder.set_place_layout_info(place_2, p2_layout)" ] }, { @@ -187,10 +187,10 @@ }, "outputs": [], "source": [ - ">>> builder.add_output_arc(it_1, place_1)\n", - ">>> builder.add_inhibition_arc(place_1, it_1)\n", - ">>> builder.add_input_arc(place_1, tt_1)\n", - ">>> builder.add_output_arc(tt_1, place_2)" + "builder.add_output_arc(it_1, place_1)\n", + "builder.add_inhibition_arc(place_1, it_1)\n", + "builder.add_input_arc(place_1, tt_1)\n", + "builder.add_output_arc(tt_1, place_2)" ] }, { @@ -208,7 +208,7 @@ }, "outputs": [], "source": [ - ">>> gspn = builder.build_gspn()" + "gspn = builder.build_gspn()" ] }, { @@ -228,8 +228,8 @@ }, "outputs": [], "source": [ - ">>> export_path = stormpy.examples.files.gspn_pnpro_simple\n", - ">>> gspn.export_gspn_pnpro_file(export_path)" + "export_path = stormpy.examples.files.gspn_pnpro_simple\n", + "gspn.export_gspn_pnpro_file(export_path)" ] } ], diff --git a/doc/source/doc/models/building_ctmcs.ipynb b/doc/source/doc/models/building_ctmcs.ipynb index 50a0e180d..001980440 100644 --- a/doc/source/doc/models/building_ctmcs.ipynb +++ b/doc/source/doc/models/building_ctmcs.ipynb @@ -29,7 +29,7 @@ }, "outputs": [], "source": [ - ">>> import stormpy" + "import stormpy" ] }, { @@ -47,12 +47,17 @@ "metadata": {}, "outputs": [], "source": [ - ">>> import numpy as np\n", - ">>> transitions = np.array([\n", - "... [0, 1.5, 0, 0],\n", - "... [3, 0, 1.5, 0],\n", - "... [0, 3, 0, 1.5],\n", - "... [0, 0, 3, 0], ], dtype='float64')" + "import numpy as np\n", + "\n", + "transitions = np.array(\n", + " [\n", + " [0, 1.5, 0, 0],\n", + " [3, 0, 1.5, 0],\n", + " [0, 3, 0, 1.5],\n", + " [0, 0, 3, 0],\n", + " ],\n", + " dtype=\"float64\",\n", + ")" ] }, { @@ -70,8 +75,8 @@ }, "outputs": [], "source": [ - ">>> transition_matrix = stormpy.build_sparse_matrix(transitions)\n", - ">>> print(transition_matrix) " + "transition_matrix = stormpy.build_sparse_matrix(transitions)\n", + "print(transition_matrix)" ] }, { @@ -91,13 +96,13 @@ }, "outputs": [], "source": [ - ">>> state_labeling = stormpy.storage.StateLabeling(4)\n", - ">>> state_labels = {'empty', 'init', 'deadlock', 'full'}\n", - ">>> for label in state_labels:\n", - "... state_labeling.add_label(label)\n", - ">>> state_labeling.add_label_to_state('init', 0)\n", - ">>> state_labeling.add_label_to_state('empty', 0)\n", - ">>> state_labeling.add_label_to_state('full', 3)" + "state_labeling = stormpy.storage.StateLabeling(4)\n", + "state_labels = {\"empty\", \"init\", \"deadlock\", \"full\"}\n", + "for label in state_labels:\n", + " state_labeling.add_label(label)\n", + "state_labeling.add_label_to_state(\"init\", 0)\n", + "state_labeling.add_label_to_state(\"empty\", 0)\n", + "state_labeling.add_label_to_state(\"full\", 3)" ] }, { @@ -118,7 +123,7 @@ }, "outputs": [], "source": [ - ">>> components = stormpy.SparseModelComponents(transition_matrix=transition_matrix, state_labeling=state_labeling, rate_transitions=True)\n" + "components = stormpy.SparseModelComponents(transition_matrix=transition_matrix, state_labeling=state_labeling, rate_transitions=True)" ] }, { @@ -136,8 +141,8 @@ }, "outputs": [], "source": [ - ">>> ctmc = stormpy.storage.SparseCtmc(components)\n", - ">>> print(ctmc) " + "ctmc = stormpy.storage.SparseCtmc(components)\n", + "print(ctmc)" ] } ], diff --git a/doc/source/doc/models/building_dtmcs.ipynb b/doc/source/doc/models/building_dtmcs.ipynb index aa4f95ee0..4efb9acb4 100644 --- a/doc/source/doc/models/building_dtmcs.ipynb +++ b/doc/source/doc/models/building_dtmcs.ipynb @@ -33,7 +33,7 @@ }, "outputs": [], "source": [ - ">>> import stormpy" + "import stormpy" ] }, { @@ -54,7 +54,7 @@ }, "outputs": [], "source": [ - ">>> 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)" ] }, { @@ -80,20 +80,20 @@ }, "outputs": [], "source": [ - ">>> builder.add_next_value(row = 0, column = 1, value = 0.5)\n", - ">>> builder.add_next_value(0, 2, 0.5)\n", - ">>> builder.add_next_value(1, 3, 0.5)\n", - ">>> builder.add_next_value(1, 4, 0.5)\n", - ">>> builder.add_next_value(2, 5, 0.5)\n", - ">>> builder.add_next_value(2, 6, 0.5)\n", - ">>> builder.add_next_value(3, 7, 0.5)\n", - ">>> builder.add_next_value(3, 1, 0.5)\n", - ">>> builder.add_next_value(4, 8, 0.5)\n", - ">>> builder.add_next_value(4, 9, 0.5)\n", - ">>> builder.add_next_value(5, 10, 0.5)\n", - ">>> builder.add_next_value(5, 11, 0.5)\n", - ">>> builder.add_next_value(6, 2, 0.5)\n", - ">>> builder.add_next_value(6, 12, 0.5)" + "builder.add_next_value(row=0, column=1, value=0.5)\n", + "builder.add_next_value(0, 2, 0.5)\n", + "builder.add_next_value(1, 3, 0.5)\n", + "builder.add_next_value(1, 4, 0.5)\n", + "builder.add_next_value(2, 5, 0.5)\n", + "builder.add_next_value(2, 6, 0.5)\n", + "builder.add_next_value(3, 7, 0.5)\n", + "builder.add_next_value(3, 1, 0.5)\n", + "builder.add_next_value(4, 8, 0.5)\n", + "builder.add_next_value(4, 9, 0.5)\n", + "builder.add_next_value(5, 10, 0.5)\n", + "builder.add_next_value(5, 11, 0.5)\n", + "builder.add_next_value(6, 2, 0.5)\n", + "builder.add_next_value(6, 12, 0.5)" ] }, { @@ -111,8 +111,8 @@ }, "outputs": [], "source": [ - ">>> for s in range(7,13):\n", - "... builder.add_next_value(s, s, 1)" + "for s in range(7, 13):\n", + " builder.add_next_value(s, s, 1)" ] }, { @@ -130,7 +130,7 @@ }, "outputs": [], "source": [ - ">>> transition_matrix = builder.build()" + "transition_matrix = builder.build()" ] }, { @@ -161,11 +161,11 @@ }, "outputs": [], "source": [ - ">>> state_labeling = stormpy.storage.StateLabeling(13)\n", + "state_labeling = stormpy.storage.StateLabeling(13)\n", "\n", - ">>> labels = {'init', 'one', 'two', 'three', 'four', 'five', 'six', 'done', 'deadlock'}\n", - ">>> for label in labels:\n", - "... state_labeling.add_label(label)" + "labels = {\"init\", \"one\", \"two\", \"three\", \"four\", \"five\", \"six\", \"done\", \"deadlock\"}\n", + "for label in labels:\n", + " state_labeling.add_label(label)" ] }, { @@ -183,8 +183,8 @@ }, "outputs": [], "source": [ - ">>> state_labeling.add_label_to_state('init', 0)\n", - ">>> print(state_labeling.get_states('init'))" + "state_labeling.add_label_to_state(\"init\", 0)\n", + "print(state_labeling.get_states(\"init\"))" ] }, { @@ -202,12 +202,12 @@ }, "outputs": [], "source": [ - ">>> state_labeling.add_label_to_state('one', 7)\n", - ">>> state_labeling.add_label_to_state('two', 8)\n", - ">>> state_labeling.add_label_to_state('three', 9)\n", - ">>> state_labeling.add_label_to_state('four', 10)\n", - ">>> state_labeling.add_label_to_state('five', 11)\n", - ">>> state_labeling.add_label_to_state('six', 12)" + "state_labeling.add_label_to_state(\"one\", 7)\n", + "state_labeling.add_label_to_state(\"two\", 8)\n", + "state_labeling.add_label_to_state(\"three\", 9)\n", + "state_labeling.add_label_to_state(\"four\", 10)\n", + "state_labeling.add_label_to_state(\"five\", 11)\n", + "state_labeling.add_label_to_state(\"six\", 12)" ] }, { @@ -225,8 +225,8 @@ }, "outputs": [], "source": [ - ">>> state_labeling.set_states('done', stormpy.BitVector(13, [7, 8, 9, 10, 11, 12]))\n", - ">>> print(state_labeling) " + "state_labeling.set_states(\"done\", stormpy.BitVector(13, [7, 8, 9, 10, 11, 12]))\n", + "print(state_labeling)" ] }, { @@ -256,9 +256,9 @@ }, "outputs": [], "source": [ - ">>> reward_models = {}\n", - ">>> 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]\n", - ">>> reward_models['coin_flips'] = stormpy.SparseRewardModel(optional_state_action_reward_vector = action_reward)" + "reward_models = {}\n", + "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]\n", + "reward_models[\"coin_flips\"] = stormpy.SparseRewardModel(optional_state_action_reward_vector=action_reward)" ] }, { @@ -278,7 +278,7 @@ }, "outputs": [], "source": [ - ">>> 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)" ] }, { @@ -296,8 +296,8 @@ }, "outputs": [], "source": [ - ">>> dtmc = stormpy.storage.SparseDtmc(components)\n", - ">>> print(dtmc) " + "dtmc = stormpy.storage.SparseDtmc(components)\n", + "print(dtmc)" ] } ], diff --git a/doc/source/doc/models/building_mas.ipynb b/doc/source/doc/models/building_mas.ipynb index 5d0a2377e..3f9aad2a0 100644 --- a/doc/source/doc/models/building_mas.ipynb +++ b/doc/source/doc/models/building_mas.ipynb @@ -34,7 +34,7 @@ }, "outputs": [], "source": [ - ">>> import stormpy" + "import stormpy" ] }, { @@ -57,14 +57,9 @@ }, "outputs": [], "source": [ - ">>> import numpy as np\n", - ">>> transitions = np.array([\n", - "... [0, 1, 0, 0, 0],\n", - "... [0.8, 0, 0.2, 0, 0],\n", - "... [0.9, 0, 0, 0.1, 0],\n", - "... [0, 0, 0, 0, 1],\n", - "... [0, 0, 0, 1, 0],\n", - "... [0, 0, 0, 0, 1]], dtype='float64')" + "import numpy as np\n", + "\n", + "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\")" ] }, { @@ -82,8 +77,8 @@ }, "outputs": [], "source": [ - ">>> transition_matrix = stormpy.build_sparse_matrix(transitions, [0, 2, 3, 4, 5])\n", - ">>> print(transition_matrix) " + "transition_matrix = stormpy.build_sparse_matrix(transitions, [0, 2, 3, 4, 5])\n", + "print(transition_matrix)" ] }, { @@ -136,7 +131,7 @@ }, "outputs": [], "source": [ - ">>> markovian_states = stormpy.BitVector(5, [1, 2, 3, 4])" + "markovian_states = stormpy.BitVector(5, [1, 2, 3, 4])" ] }, { @@ -179,9 +174,9 @@ }, "outputs": [], "source": [ - ">>> components = stormpy.SparseModelComponents(transition_matrix=transition_matrix, state_labeling=state_labeling, markovian_states=markovian_states)\n", - ">>> components.choice_labeling = choice_labeling\n", - ">>> components.exit_rates = exit_rates" + "components = stormpy.SparseModelComponents(transition_matrix=transition_matrix, state_labeling=state_labeling, markovian_states=markovian_states)\n", + "components.choice_labeling = choice_labeling\n", + "components.exit_rates = exit_rates" ] }, { @@ -199,8 +194,8 @@ }, "outputs": [], "source": [ - ">>> ma = stormpy.storage.SparseMA(components)\n", - ">>> print(ma) " + "ma = stormpy.storage.SparseMA(components)\n", + "print(ma)" ] } ], diff --git a/doc/source/doc/models/building_mdps.ipynb b/doc/source/doc/models/building_mdps.ipynb index 5ebf2e1a7..3919e322f 100644 --- a/doc/source/doc/models/building_mdps.ipynb +++ b/doc/source/doc/models/building_mdps.ipynb @@ -29,7 +29,7 @@ }, "outputs": [], "source": [ - ">>> import stormpy" + "import stormpy" ] }, { @@ -49,7 +49,7 @@ }, "outputs": [], "source": [ - ">>> 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)" ] }, { @@ -69,11 +69,11 @@ }, "outputs": [], "source": [ - ">>> builder.new_row_group(0)\n", - ">>> builder.add_next_value(0, 1, 0.5)\n", - ">>> builder.add_next_value(0, 2, 0.5)\n", - ">>> builder.add_next_value(1, 1, 0.2)\n", - ">>> builder.add_next_value(1, 2, 0.8)" + "builder.new_row_group(0)\n", + "builder.add_next_value(0, 1, 0.5)\n", + "builder.add_next_value(0, 2, 0.5)\n", + "builder.add_next_value(1, 1, 0.2)\n", + "builder.add_next_value(1, 2, 0.8)" ] }, { @@ -95,28 +95,28 @@ }, "outputs": [], "source": [ - ">>> builder.new_row_group(2)\n", - ">>> builder.add_next_value(2, 3, 0.5)\n", - ">>> builder.add_next_value(2, 4, 0.5)\n", - ">>> builder.new_row_group(3)\n", - ">>> builder.add_next_value(3, 5, 0.5)\n", - ">>> builder.add_next_value(3, 6, 0.5)\n", - ">>> builder.new_row_group(4)\n", - ">>> builder.add_next_value(4, 7, 0.5)\n", - ">>> builder.add_next_value(4, 1, 0.5)\n", - ">>> builder.new_row_group(5)\n", - ">>> builder.add_next_value(5, 8, 0.5)\n", - ">>> builder.add_next_value(5, 9, 0.5)\n", - ">>> builder.new_row_group(6)\n", - ">>> builder.add_next_value(6, 10, 0.5)\n", - ">>> builder.add_next_value(6, 11, 0.5)\n", - ">>> builder.new_row_group(7)\n", - ">>> builder.add_next_value(7, 2, 0.5)\n", - ">>> builder.add_next_value(7, 12, 0.5)\n", + "builder.new_row_group(2)\n", + "builder.add_next_value(2, 3, 0.5)\n", + "builder.add_next_value(2, 4, 0.5)\n", + "builder.new_row_group(3)\n", + "builder.add_next_value(3, 5, 0.5)\n", + "builder.add_next_value(3, 6, 0.5)\n", + "builder.new_row_group(4)\n", + "builder.add_next_value(4, 7, 0.5)\n", + "builder.add_next_value(4, 1, 0.5)\n", + "builder.new_row_group(5)\n", + "builder.add_next_value(5, 8, 0.5)\n", + "builder.add_next_value(5, 9, 0.5)\n", + "builder.new_row_group(6)\n", + "builder.add_next_value(6, 10, 0.5)\n", + "builder.add_next_value(6, 11, 0.5)\n", + "builder.new_row_group(7)\n", + "builder.add_next_value(7, 2, 0.5)\n", + "builder.add_next_value(7, 12, 0.5)\n", "\n", - ">>> for s in range(8, 14):\n", - "... builder.new_row_group(s)\n", - "... builder.add_next_value(s, s - 1, 1)" + "for s in range(8, 14):\n", + " builder.new_row_group(s)\n", + " builder.add_next_value(s, s - 1, 1)" ] }, { @@ -134,7 +134,7 @@ }, "outputs": [], "source": [ - ">>> transition_matrix = builder.build()" + "transition_matrix = builder.build()" ] }, { @@ -157,19 +157,19 @@ }, "outputs": [], "source": [ - ">>> state_labeling = stormpy.storage.StateLabeling(13)\n", - ">>> labels = {'init', 'one', 'two', 'three', 'four', 'five', 'six', 'done', 'deadlock'}\n", - ">>> for label in labels:\n", - "... state_labeling.add_label(label)\n", + "state_labeling = stormpy.storage.StateLabeling(13)\n", + "labels = {\"init\", \"one\", \"two\", \"three\", \"four\", \"five\", \"six\", \"done\", \"deadlock\"}\n", + "for label in labels:\n", + " state_labeling.add_label(label)\n", "\n", - ">>> state_labeling.add_label_to_state('init', 0)\n", - ">>> state_labeling.add_label_to_state('one', 7)\n", - ">>> state_labeling.add_label_to_state('two', 8)\n", - ">>> state_labeling.add_label_to_state('three', 9)\n", - ">>> state_labeling.add_label_to_state('four', 10)\n", - ">>> state_labeling.add_label_to_state('five', 11)\n", - ">>> state_labeling.add_label_to_state('six', 12)\n", - ">>> state_labeling.set_states('done', stormpy.BitVector(13, [7, 8, 9, 10, 11, 12]))" + "state_labeling.add_label_to_state(\"init\", 0)\n", + "state_labeling.add_label_to_state(\"one\", 7)\n", + "state_labeling.add_label_to_state(\"two\", 8)\n", + "state_labeling.add_label_to_state(\"three\", 9)\n", + "state_labeling.add_label_to_state(\"four\", 10)\n", + "state_labeling.add_label_to_state(\"five\", 11)\n", + "state_labeling.add_label_to_state(\"six\", 12)\n", + "state_labeling.set_states(\"done\", stormpy.BitVector(13, [7, 8, 9, 10, 11, 12]))" ] }, { @@ -180,11 +180,11 @@ }, "outputs": [], "source": [ - ">>> choice_labeling = stormpy.storage.ChoiceLabeling(14)\n", - ">>> choice_labels = {'a', 'b'}\n", + "choice_labeling = stormpy.storage.ChoiceLabeling(14)\n", + "choice_labels = {\"a\", \"b\"}\n", "\n", - ">>> for label in choice_labels:\n", - "... choice_labeling.add_label(label)" + "for label in choice_labels:\n", + " choice_labeling.add_label(label)" ] }, { @@ -203,9 +203,9 @@ }, "outputs": [], "source": [ - ">>> choice_labeling.add_label_to_choice('a', 0)\n", - ">>> choice_labeling.add_label_to_choice('b', 1)\n", - ">>> print(choice_labeling) " + "choice_labeling.add_label_to_choice(\"a\", 0)\n", + "choice_labeling.add_label_to_choice(\"b\", 1)\n", + "print(choice_labeling)" ] }, { @@ -225,9 +225,9 @@ }, "outputs": [], "source": [ - ">>> reward_models = {}\n", - ">>> 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]\n", - ">>> reward_models['coin_flips'] = stormpy.SparseRewardModel(optional_state_action_reward_vector=action_reward)" + "reward_models = {}\n", + "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]\n", + "reward_models[\"coin_flips\"] = stormpy.SparseRewardModel(optional_state_action_reward_vector=action_reward)" ] }, { @@ -247,8 +247,10 @@ }, "outputs": [], "source": [ - ">>> components = stormpy.SparseModelComponents(transition_matrix=transition_matrix, state_labeling=state_labeling, reward_models=reward_models, rate_transitions=False)\n", - ">>> components.choice_labeling = choice_labeling" + "components = stormpy.SparseModelComponents(\n", + " transition_matrix=transition_matrix, state_labeling=state_labeling, reward_models=reward_models, rate_transitions=False\n", + ")\n", + "components.choice_labeling = choice_labeling" ] }, { @@ -266,8 +268,8 @@ }, "outputs": [], "source": [ - ">>> mdp = stormpy.storage.SparseMdp(components)\n", - ">>> print(mdp) " + "mdp = stormpy.storage.SparseMdp(components)\n", + "print(mdp)" ] }, { diff --git a/doc/source/doc/parametric_models.ipynb b/doc/source/doc/parametric_models.ipynb index 1c0e5ec5b..1998fddfe 100644 --- a/doc/source/doc/parametric_models.ipynb +++ b/doc/source/doc/parametric_models.ipynb @@ -27,17 +27,18 @@ }, "outputs": [], "source": [ - ">>> import stormpy\n", - ">>> import stormpy.examples\n", - ">>> import stormpy.examples.files\n", - ">>> path = stormpy.examples.files.prism_pdtmc_die\n", - ">>> prism_program = stormpy.parse_prism_program(path)\n", - ">>> formula_str = \"P=? [F s=7 & d=2]\"\n", - ">>> properties = stormpy.parse_properties(formula_str, prism_program)\n", - ">>> model = stormpy.build_parametric_model(prism_program, properties)\n", - ">>> parameters = model.collect_probability_parameters()\n", - ">>> for x in parameters:\n", - "... print(x)" + "import stormpy\n", + "import stormpy.examples\n", + "import stormpy.examples.files\n", + "\n", + "path = stormpy.examples.files.prism_pdtmc_die\n", + "prism_program = stormpy.parse_prism_program(path)\n", + "formula_str = \"P=? [F s=7 & d=2]\"\n", + "properties = stormpy.parse_properties(formula_str, prism_program)\n", + "model = stormpy.build_parametric_model(prism_program, properties)\n", + "parameters = model.collect_probability_parameters()\n", + "for x in parameters:\n", + " print(x)" ] }, { @@ -55,8 +56,9 @@ }, "outputs": [], "source": [ - ">>> import stormpy.pars\n", - ">>> instantiator = stormpy.pars.PDtmcInstantiator(model)" + "import stormpy.pars\n", + "\n", + "instantiator = stormpy.pars.PDtmcInstantiator(model)" ] }, { @@ -74,12 +76,12 @@ }, "outputs": [], "source": [ - ">>> point = dict()\n", - ">>> for x in parameters:\n", - "... print(x.name)\n", - "... point[x] = stormpy.RationalRF(0.4)\n", - ">>> instantiated_model = instantiator.instantiate(point)\n", - ">>> result = stormpy.model_checking(instantiated_model, properties[0])" + "point = dict()\n", + "for x in parameters:\n", + " print(x.name)\n", + " point[x] = stormpy.RationalRF(0.4)\n", + "instantiated_model = instantiator.instantiate(point)\n", + "result = stormpy.model_checking(instantiated_model, properties[0])" ] }, { @@ -108,9 +110,9 @@ }, "outputs": [], "source": [ - ">>> result = stormpy.model_checking(model, properties[0])\n", - ">>> initial_state = model.initial_states[0]\n", - ">>> func = result.at(initial_state)" + "result = stormpy.model_checking(model, properties[0])\n", + "initial_state = model.initial_states[0]\n", + "func = result.at(initial_state)" ] }, { @@ -128,16 +130,17 @@ }, "outputs": [], "source": [ - ">>> import stormpy.info\n", - ">>> if stormpy.info.storm_ratfunc_use_cln():\n", - "... import pycarl.cln.formula\n", - ">>> else:\n", - "... import pycarl.gmp.formula\n", - ">>> collector = stormpy.ConstraintCollector(model)\n", - ">>> for formula in collector.wellformed_constraints:\n", - "... print(formula)\n", - ">>> for formula in collector.graph_preserving_constraints:\n", - "... print(formula)" + "import stormpy.info\n", + "\n", + "if stormpy.info.storm_ratfunc_use_cln():\n", + " import pycarl.cln.formula\n", + "else:\n", + " import pycarl.gmp.formula\n", + "collector = stormpy.ConstraintCollector(model)\n", + "for formula in collector.wellformed_constraints:\n", + " print(formula)\n", + "for formula in collector.graph_preserving_constraints:\n", + " print(formula)" ] }, { diff --git a/doc/source/doc/reward_models.ipynb b/doc/source/doc/reward_models.ipynb index 6c438d301..af10c3080 100644 --- a/doc/source/doc/reward_models.ipynb +++ b/doc/source/doc/reward_models.ipynb @@ -29,15 +29,16 @@ }, "outputs": [], "source": [ - ">>> import stormpy\n", - ">>> import stormpy.examples\n", - ">>> import stormpy.examples.files\n", - ">>> program = stormpy.parse_prism_program(stormpy.examples.files.prism_dtmc_die)\n", - ">>> prop = \"R=? [F \\\"done\\\"]\"\n", + "import stormpy\n", + "import stormpy.examples\n", + "import stormpy.examples.files\n", "\n", - ">>> properties = stormpy.parse_properties(prop, program, None)\n", - ">>> model = stormpy.build_model(program, properties)\n", - ">>> assert len(model.reward_models) == 1" + "program = stormpy.parse_prism_program(stormpy.examples.files.prism_dtmc_die)\n", + "prop = 'R=? [F \"done\"]'\n", + "\n", + "properties = stormpy.parse_properties(prop, program, None)\n", + "model = stormpy.build_model(program, properties)\n", + "assert len(model.reward_models) == 1" ] }, { @@ -57,9 +58,9 @@ }, "outputs": [], "source": [ - ">>> initial_state = model.initial_states[0]\n", - ">>> result = stormpy.model_checking(model, properties[0])\n", - ">>> print(\"Result: {}\".format(round(result.at(initial_state), 6)))" + "initial_state = model.initial_states[0]\n", + "result = stormpy.model_checking(model, properties[0])\n", + "print(\"Result: {}\".format(round(result.at(initial_state), 6)))" ] }, { @@ -77,8 +78,8 @@ }, "outputs": [], "source": [ - ">>> reward_model_name = list(model.reward_models.keys())[0]\n", - ">>> print(reward_model_name)" + "reward_model_name = list(model.reward_models.keys())[0]\n", + "print(reward_model_name)" ] }, { @@ -98,11 +99,11 @@ }, "outputs": [], "source": [ - ">>> assert not model.reward_models[reward_model_name].has_state_rewards\n", - ">>> assert model.reward_models[reward_model_name].has_state_action_rewards\n", - ">>> assert not model.reward_models[reward_model_name].has_transition_rewards\n", - ">>> for reward in model.reward_models[reward_model_name].state_action_rewards:\n", - "... print(reward)" + "assert not model.reward_models[reward_model_name].has_state_rewards\n", + "assert model.reward_models[reward_model_name].has_state_action_rewards\n", + "assert not model.reward_models[reward_model_name].has_transition_rewards\n", + "for reward in model.reward_models[reward_model_name].state_action_rewards:\n", + " print(reward)" ] } ], diff --git a/doc/source/doc/schedulers.ipynb b/doc/source/doc/schedulers.ipynb index 652467d38..e5483a794 100644 --- a/doc/source/doc/schedulers.ipynb +++ b/doc/source/doc/schedulers.ipynb @@ -31,19 +31,19 @@ }, "outputs": [], "source": [ - ">>> import stormpy\n", - ">>> import stormpy.examples\n", - ">>> import stormpy.examples.files\n", + "import stormpy\n", + "import stormpy.examples\n", + "import stormpy.examples.files\n", "\n", - ">>> path = stormpy.examples.files.prism_mdp_coin_2_2\n", - ">>> formula_str = \"Pmin=? [F \\\"finished\\\" & \\\"all_coins_equal_1\\\"]\"\n", - ">>> program = stormpy.parse_prism_program(path)\n", - ">>> formulas = stormpy.parse_properties(formula_str, program)\n", - ">>> options = stormpy.BuilderOptions(True, True)\n", - ">>> options.set_build_state_valuations()\n", - ">>> options.set_build_choice_labels()\n", - ">>> options.set_build_with_choice_origins()\n", - ">>> model = stormpy.build_sparse_model_with_options(program, options)" + "path = stormpy.examples.files.prism_mdp_coin_2_2\n", + "formula_str = 'Pmin=? [F \"finished\" & \"all_coins_equal_1\"]'\n", + "program = stormpy.parse_prism_program(path)\n", + "formulas = stormpy.parse_properties(formula_str, program)\n", + "options = stormpy.BuilderOptions(True, True)\n", + "options.set_build_state_valuations()\n", + "options.set_build_choice_labels()\n", + "options.set_build_with_choice_origins()\n", + "model = stormpy.build_sparse_model_with_options(program, options)" ] }, { @@ -61,7 +61,7 @@ }, "outputs": [], "source": [ - ">>> result = stormpy.model_checking(model, formulas[0], extract_scheduler=True)" + "result = stormpy.model_checking(model, formulas[0], extract_scheduler=True)" ] }, { @@ -79,11 +79,11 @@ }, "outputs": [], "source": [ - ">>> assert result.has_scheduler\n", - ">>> scheduler = result.scheduler\n", - ">>> assert scheduler.memoryless\n", - ">>> assert scheduler.deterministic\n", - ">>> print(scheduler)" + "assert result.has_scheduler\n", + "scheduler = result.scheduler\n", + "assert scheduler.memoryless\n", + "assert scheduler.deterministic\n", + "print(scheduler)" ] }, { @@ -101,12 +101,12 @@ }, "outputs": [], "source": [ - ">>> for state in model.states:\n", - "... choice = scheduler.get_choice(state)\n", - "... action_index = choice.get_deterministic_choice()\n", - "... action = state.actions[action_index]\n", - "... print(\"In state {} ({}) choose action {} ({})\".format(state, \", \".join(state.labels), action, \", \".join(action.labels)))\n", - "... print(state.valuations)" + "for state in model.states:\n", + " choice = scheduler.get_choice(state)\n", + " action_index = choice.get_deterministic_choice()\n", + " action = state.actions[action_index]\n", + " print(\"In state {} ({}) choose action {} ({})\".format(state, \", \".join(state.labels), action, \", \".join(action.labels)))\n", + " print(state.valuations)" ] }, { @@ -131,12 +131,12 @@ }, "outputs": [], "source": [ - ">>> path = stormpy.examples.files.prism_ma_simple\n", - ">>> formula_str = \"Tmin=? [ F s=4 ]\"\n", + "path = stormpy.examples.files.prism_ma_simple\n", + "formula_str = \"Tmin=? [ F s=4 ]\"\n", "\n", - ">>> program = stormpy.parse_prism_program(path, False, True)\n", - ">>> formulas = stormpy.parse_properties_for_prism_program(formula_str, program)\n", - ">>> ma = stormpy.build_model(program, formulas)" + "program = stormpy.parse_prism_program(path, False, True)\n", + "formulas = stormpy.parse_properties_for_prism_program(formula_str, program)\n", + "ma = stormpy.build_model(program, formulas)" ] }, { @@ -155,8 +155,8 @@ }, "outputs": [], "source": [ - ">>> mdp, mdp_formulas = stormpy.transform_to_discrete_time_model(ma, formulas)\n", - ">>> assert mdp.model_type == stormpy.ModelType.MDP" + "mdp, mdp_formulas = stormpy.transform_to_discrete_time_model(ma, formulas)\n", + "assert mdp.model_type == stormpy.ModelType.MDP" ] }, { @@ -174,9 +174,9 @@ }, "outputs": [], "source": [ - ">>> result = stormpy.model_checking(mdp, mdp_formulas[0], extract_scheduler=True)\n", - ">>> scheduler = result.scheduler\n", - ">>> print(scheduler)\n" + "result = stormpy.model_checking(mdp, mdp_formulas[0], extract_scheduler=True)\n", + "scheduler = result.scheduler\n", + "print(scheduler)" ] } ], diff --git a/doc/source/doc/shortest_paths.ipynb b/doc/source/doc/shortest_paths.ipynb index e9076bf78..575f3d1f8 100644 --- a/doc/source/doc/shortest_paths.ipynb +++ b/doc/source/doc/shortest_paths.ipynb @@ -42,11 +42,12 @@ }, "outputs": [], "source": [ - ">>> import stormpy.examples\n", - ">>> import stormpy.examples.files\n", - ">>> path = stormpy.examples.files.prism_dtmc_die\n", - ">>> prism_program = stormpy.parse_prism_program(path)\n", - ">>> model = stormpy.build_model(prism_program)" + "import stormpy.examples\n", + "import stormpy.examples.files\n", + "\n", + "path = stormpy.examples.files.prism_dtmc_die\n", + "prism_program = stormpy.parse_prism_program(path)\n", + "model = stormpy.build_model(prism_program)" ] }, { @@ -64,7 +65,7 @@ }, "outputs": [], "source": [ - ">>> from stormpy.utility import ShortestPathsGenerator" + "from stormpy.utility import ShortestPathsGenerator" ] }, { @@ -82,7 +83,7 @@ }, "outputs": [], "source": [ - ">>> state_id = 8" + "state_id = 8" ] }, { @@ -103,7 +104,7 @@ }, "outputs": [], "source": [ - ">>> spg = ShortestPathsGenerator(model, state_id)" + "spg = ShortestPathsGenerator(model, state_id)" ] }, { @@ -122,10 +123,10 @@ }, "outputs": [], "source": [ - ">>> for k in range(1, 4):\n", - "... path = spg.get_path_as_list(k)\n", - "... distance = spg.get_distance(k)\n", - "... print(\"{}-shortest path to state #{}: {}, with distance {}\".format(k, state_id, path, distance))" + "for k in range(1, 4):\n", + " path = spg.get_path_as_list(k)\n", + " distance = spg.get_distance(k)\n", + " print(\"{}-shortest path to state #{}: {}, with distance {}\".format(k, state_id, path, distance))" ] }, { diff --git a/doc/source/doc/simulator.ipynb b/doc/source/doc/simulator.ipynb index 8de0ed56b..c0af024e0 100644 --- a/doc/source/doc/simulator.ipynb +++ b/doc/source/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/doc/source/getting_started.ipynb b/doc/source/getting_started.ipynb index fd5f77b76..4a34700d9 100644 --- a/doc/source/getting_started.ipynb +++ b/doc/source/getting_started.ipynb @@ -52,7 +52,7 @@ }, "outputs": [], "source": [ - ">>> import stormpy" + "import stormpy" ] }, { @@ -78,8 +78,8 @@ }, "outputs": [], "source": [ - ">>> import stormpy.examples\n", - ">>> import stormpy.examples.files" + "import stormpy.examples\n", + "import stormpy.examples.files" ] }, { @@ -97,8 +97,8 @@ }, "outputs": [], "source": [ - ">>> path = stormpy.examples.files.prism_dtmc_die\n", - ">>> prism_program = stormpy.parse_prism_program(path)" + "path = stormpy.examples.files.prism_dtmc_die\n", + "prism_program = stormpy.parse_prism_program(path)" ] }, { @@ -116,8 +116,8 @@ }, "outputs": [], "source": [ - ">>> model = stormpy.build_model(prism_program)\n", - ">>> print(\"Number of states: {}\".format(model.nr_states))" + "model = stormpy.build_model(prism_program)\n", + "print(\"Number of states: {}\".format(model.nr_states))" ] }, { @@ -126,7 +126,7 @@ "metadata": {}, "outputs": [], "source": [ - ">>> print(\"Number of transitions: {}\".format(model.nr_transitions))" + "print(\"Number of transitions: {}\".format(model.nr_transitions))" ] }, { @@ -146,7 +146,7 @@ }, "outputs": [], "source": [ - ">>> print(\"Labels: {}\".format(model.labeling.get_labels()))" + "print(\"Labels: {}\".format(model.labeling.get_labels()))" ] }, { @@ -196,8 +196,8 @@ }, "outputs": [], "source": [ - ">>> formula_str = \"P=? [F s=2]\"\n", - ">>> properties = stormpy.parse_properties(formula_str, prism_program)" + "formula_str = \"P=? [F s=2]\"\n", + "properties = stormpy.parse_properties(formula_str, prism_program)" ] }, { @@ -219,8 +219,8 @@ }, "outputs": [], "source": [ - ">>> model = stormpy.build_model(prism_program, properties)\n", - ">>> print(\"Labels in the model: {}\".format(sorted(model.labeling.get_labels())))" + "model = stormpy.build_model(prism_program, properties)\n", + "print(\"Labels in the model: {}\".format(sorted(model.labeling.get_labels())))" ] }, { @@ -239,7 +239,7 @@ }, "outputs": [], "source": [ - ">>> print(\"Number of states: {}\".format(model.nr_states))" + "print(\"Number of states: {}\".format(model.nr_states))" ] }, { @@ -290,9 +290,9 @@ }, "outputs": [], "source": [ - ">>> properties = stormpy.parse_properties(formula_str, prism_program)\n", - ">>> model = stormpy.build_model(prism_program, properties)\n", - ">>> result = stormpy.model_checking(model, properties[0])" + "properties = stormpy.parse_properties(formula_str, prism_program)\n", + "model = stormpy.build_model(prism_program, properties)\n", + "result = stormpy.model_checking(model, properties[0])" ] }, { @@ -311,9 +311,9 @@ }, "outputs": [], "source": [ - ">>> assert result.result_for_all_states\n", - ">>> for x in result.get_values():\n", - "... pass # do something with x" + "assert result.result_for_all_states\n", + "for x in result.get_values():\n", + " pass # do something with x" ] }, { @@ -335,8 +335,8 @@ }, "outputs": [], "source": [ - ">>> initial_state = model.initial_states[0]\n", - ">>> print(result.at(initial_state))" + "initial_state = model.initial_states[0]\n", + "print(result.at(initial_state))" ] }, { @@ -366,9 +366,9 @@ }, "outputs": [], "source": [ - ">>> path = stormpy.examples.files.prism_dtmc_die\n", - ">>> prism_program = stormpy.parse_prism_program(path)\n", - ">>> model = stormpy.build_model(prism_program)" + "path = stormpy.examples.files.prism_dtmc_die\n", + "prism_program = stormpy.parse_prism_program(path)\n", + "model = stormpy.build_model(prism_program)" ] }, { @@ -387,7 +387,7 @@ }, "outputs": [], "source": [ - ">>> print(model.model_type)" + "print(model.model_type)" ] }, { @@ -406,10 +406,10 @@ }, "outputs": [], "source": [ - ">>> for state in model.states:\n", - "... for action in state.actions:\n", - "... for transition in action.transitions:\n", - "... print(\"From state {}, with probability {}, go to state {}\".format(state, transition.value(), transition.column))" + "for state in model.states:\n", + " for action in state.actions:\n", + " for transition in action.transitions:\n", + " print(\"From state {}, with probability {}, go to state {}\".format(state, transition.value(), transition.column))" ] }, { @@ -428,8 +428,8 @@ }, "outputs": [], "source": [ - ">>> for state in model.states:\n", - "... assert len(state.actions) <= 1" + "for state in model.states:\n", + " assert len(state.actions) <= 1" ] }, { @@ -447,9 +447,9 @@ }, "outputs": [], "source": [ - ">>> for state in model.states:\n", - "... if state.id in model.initial_states:\n", - "... pass" + "for state in model.states:\n", + " if state.id in model.initial_states:\n", + " pass" ] } ], diff --git a/examples/01-getting-started.py b/examples/01-getting-started.py index 1d1aacc95..04606527c 100644 --- a/examples/01-getting-started.py +++ b/examples/01-getting-started.py @@ -14,5 +14,5 @@ def example_getting_started_01(): print("Labels: {}".format(model.labeling.get_labels())) -if __name__ == '__main__': +if __name__ == "__main__": example_getting_started_01() diff --git a/examples/02-getting-started.py b/examples/02-getting-started.py index fa64b206a..8b7195c6e 100644 --- a/examples/02-getting-started.py +++ b/examples/02-getting-started.py @@ -28,5 +28,5 @@ def example_getting_started_02(): print("Labels in the model: {}".format(model_for_formula_2.labeling.get_labels())) -if __name__ == '__main__': +if __name__ == "__main__": example_getting_started_02() diff --git a/examples/03-getting-started.py b/examples/03-getting-started.py index 2bf64a4ef..e7bf8319a 100644 --- a/examples/03-getting-started.py +++ b/examples/03-getting-started.py @@ -20,5 +20,5 @@ def example_getting_started_03(): print(result.at(initial_state)) -if __name__ == '__main__': +if __name__ == "__main__": example_getting_started_03() diff --git a/examples/04-getting-started.py b/examples/04-getting-started.py index dc0d55955..f1008ba84 100644 --- a/examples/04-getting-started.py +++ b/examples/04-getting-started.py @@ -19,9 +19,8 @@ def example_getting_started_04(): print(state) for action in state.actions: for transition in action.transitions: - print("From state {}, with probability {}, go to state {}".format(state, transition.value(), - transition.column)) + print("From state {}, with probability {}, go to state {}".format(state, transition.value(), transition.column)) -if __name__ == '__main__': +if __name__ == "__main__": example_getting_started_04() diff --git a/examples/analysis/01-analysis.py b/examples/analysis/01-analysis.py index a307d795f..689ed4b4e 100644 --- a/examples/analysis/01-analysis.py +++ b/examples/analysis/01-analysis.py @@ -15,5 +15,6 @@ def example_analysis_01(): print(prob0E) print(prob1A) -if __name__ == '__main__': + +if __name__ == "__main__": example_analysis_01() diff --git a/examples/analysis/02-analysis.py b/examples/analysis/02-analysis.py index db02ef0bb..ec7b459a3 100644 --- a/examples/analysis/02-analysis.py +++ b/examples/analysis/02-analysis.py @@ -6,6 +6,7 @@ from stormpy.storage import Expression + def example_analysis_02(): path = stormpy.examples.files.prism_dtmc_die prism_program = stormpy.parse_prism_program(path) @@ -19,7 +20,6 @@ def example_analysis_02(): assert result.min == result.max print(result.min) - # Create an auxiliary mapping to build expressions that matches some state. variables = dict() for m in prism_program.modules: @@ -27,20 +27,21 @@ def example_analysis_02(): variables[v.name] = v.expression_variable.get_expression() expr_manager = prism_program.expression_manager - expr_for_state_1 = Expression.Conjunction([Expression.Eq(variables["s"],expr_manager.create_integer(1)), - Expression.Eq(variables["d"],expr_manager.create_integer(0))]) - expr_for_state_2 = Expression.And(Expression.Eq(variables["s"],expr_manager.create_integer(4)), - Expression.Eq(variables["d"],expr_manager.create_integer(0))) + expr_for_state_1 = Expression.Conjunction( + [Expression.Eq(variables["s"], expr_manager.create_integer(1)), Expression.Eq(variables["d"], expr_manager.create_integer(0))] + ) + expr_for_state_2 = Expression.And( + Expression.Eq(variables["s"], expr_manager.create_integer(4)), Expression.Eq(variables["d"], expr_manager.create_integer(0)) + ) result = stormpy.model_checking(model, properties[0]) cached_res = result.clone() - cached_res.filter(stormpy.create_filter_symbolic(model,expr_for_state_1)) + cached_res.filter(stormpy.create_filter_symbolic(model, expr_for_state_1)) print(cached_res.min) - result.filter(stormpy.create_filter_symbolic(model,expr_for_state_2)) + result.filter(stormpy.create_filter_symbolic(model, expr_for_state_2)) assert result.min == result.max print(result.min) - -if __name__ == '__main__': +if __name__ == "__main__": example_analysis_02() diff --git a/examples/analysis/03-analysis.py b/examples/analysis/03-analysis.py index 260d5234d..f7411913f 100644 --- a/examples/analysis/03-analysis.py +++ b/examples/analysis/03-analysis.py @@ -15,7 +15,7 @@ def example_analysis_03(): env.solver_environment.set_linear_equation_solver_type(stormpy.EquationSolverType.native) env.solver_environment.native_solver_environment.method = stormpy.NativeLinearEquationSolverMethod.optimistic_value_iteration env.solver_environment.native_solver_environment.precision = stormpy.Rational("0.9") - #env.solver_environment.native_solver_environment.maximum_iterations = 2 + # env.solver_environment.native_solver_environment.maximum_iterations = 2 result = stormpy.model_checking(model, properties[0], environment=env) print(result.at(model.initial_states[0])) @@ -27,6 +27,5 @@ def example_analysis_03(): print(result.min) - -if __name__ == '__main__': +if __name__ == "__main__": example_analysis_03() diff --git a/examples/analysis/04-analysis.py b/examples/analysis/04-analysis.py index 88a5d2996..d46916e52 100644 --- a/examples/analysis/04-analysis.py +++ b/examples/analysis/04-analysis.py @@ -14,14 +14,15 @@ def example_analysis_04(): options = stormpy.BuilderOptions([p.raw_formula for p in properties]) options.set_build_state_valuations() model = stormpy.build_sparse_model_with_options(prism_program, options) - + result = stormpy.model_checking(model, properties[0]) # Print the model checking result for all states - + print("Model checking results:") for i in range(len(model.states)): - print("\tstate #{}\t {}:\t {}".format(i,model.state_valuations.get_string(i),result.at(i))) - -if __name__ == '__main__': + print("\tstate #{}\t {}:\t {}".format(i, model.state_valuations.get_string(i), result.at(i))) + + +if __name__ == "__main__": example_analysis_04() diff --git a/examples/building_ctmcs/01-building-ctmcs.py b/examples/building_ctmcs/01-building-ctmcs.py index c2603a1c1..12fe19afa 100644 --- a/examples/building_ctmcs/01-building-ctmcs.py +++ b/examples/building_ctmcs/01-building-ctmcs.py @@ -3,6 +3,7 @@ # Check if numpy is available try: import numpy as np + numpy_found = True except ModuleNotFoundError: numpy_found = False @@ -14,11 +15,15 @@ def example_building_ctmcs_01(): return # Building the transition matrix using numpy - transitions = np.array([ - [0, 1.5, 0, 0], - [3, 0, 1.5, 0], - [0, 3, 0, 1.5], - [0, 0, 3, 0], ], dtype='float64') + transitions = np.array( + [ + [0, 1.5, 0, 0], + [3, 0, 1.5, 0], + [0, 3, 0, 1.5], + [0, 0, 3, 0], + ], + dtype="float64", + ) # Default row groups: [0,1,2,3] transition_matrix = stormpy.build_sparse_matrix(transitions) @@ -26,14 +31,14 @@ def example_building_ctmcs_01(): # State labeling state_labeling = stormpy.storage.StateLabeling(4) - state_labels = {'empty', 'init', 'deadlock', 'full'} + state_labels = {"empty", "init", "deadlock", "full"} for label in state_labels: state_labeling.add_label(label) # Adding label to states - 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.add_label_to_state("init", 0) + state_labeling.add_label_to_state("empty", 0) + state_labeling.add_label_to_state("full", 3) # Collect components # rate_transitions = True, because the transition values are interpreted as rates @@ -45,5 +50,5 @@ def example_building_ctmcs_01(): print(ctmc) -if __name__ == '__main__': +if __name__ == "__main__": example_building_ctmcs_01() diff --git a/examples/building_dtmcs/01-building-dtmcs.py b/examples/building_dtmcs/01-building-dtmcs.py index d7d22da73..e4b64dfbd 100644 --- a/examples/building_dtmcs/01-building-dtmcs.py +++ b/examples/building_dtmcs/01-building-dtmcs.py @@ -3,8 +3,7 @@ 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) + 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) @@ -34,39 +33,38 @@ def example_building_dtmcs_01(): state_labeling = stormpy.storage.StateLabeling(13) # Add labels - labels = {'init', 'one', 'two', 'three', 'four', 'five', 'six', 'done', 'deadlock'} + 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')) + 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) + 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])) + 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) + 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) + 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__': +if __name__ == "__main__": example_building_dtmcs_01() diff --git a/examples/building_mas/01-building-mas.py b/examples/building_mas/01-building-mas.py index a7e4bcc27..fea7e4779 100644 --- a/examples/building_mas/01-building-mas.py +++ b/examples/building_mas/01-building-mas.py @@ -3,6 +3,7 @@ # Check if numpy is available try: import numpy as np + numpy_found = True except ModuleNotFoundError: numpy_found = False @@ -14,14 +15,7 @@ def example_building_mas_01(): return # Building the transition matrix using numpy - 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') + 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") # Build matrix and define indices of row groups (ascending order) transition_matrix = stormpy.build_sparse_matrix(transitions, [0, 2, 3, 4, 5]) @@ -30,21 +24,21 @@ def example_building_mas_01(): # StateLabeling state_labeling = stormpy.storage.StateLabeling(5) # Add labels - state_labels = {'init', 'deadlock'} + state_labels = {"init", "deadlock"} # Set labeling of states for label in state_labels: state_labeling.add_label(label) - state_labeling.add_label_to_state('init', 0) + state_labeling.add_label_to_state("init", 0) # Choice labeling choice_labeling = stormpy.storage.ChoiceLabeling(6) # Add labels - choice_labels = {'alpha', 'beta'} + choice_labels = {"alpha", "beta"} # Set labeling of choices for label in choice_labels: choice_labeling.add_label(label) - choice_labeling.add_label_to_choice('alpha', 0) - choice_labeling.add_label_to_choice('beta', 1) + choice_labeling.add_label_to_choice("alpha", 0) + choice_labeling.add_label_to_choice("beta", 1) # Provide exit rates (for Markovian states) exit_rates = [0.0, 10.0, 12.0, 1.0, 1.0] @@ -52,8 +46,7 @@ def example_building_mas_01(): markovian_states = stormpy.BitVector(5, [1, 2, 3, 4]) # Collect components - components = stormpy.SparseModelComponents(transition_matrix=transition_matrix, state_labeling=state_labeling, - markovian_states=markovian_states) + 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 @@ -62,5 +55,5 @@ def example_building_mas_01(): print(ma) -if __name__ == '__main__': +if __name__ == "__main__": example_building_mas_01() diff --git a/examples/building_mdps/01-building-mdps.py b/examples/building_mdps/01-building-mdps.py index 60d61d6a6..cc862de27 100644 --- a/examples/building_mdps/01-building-mdps.py +++ b/examples/building_mdps/01-building-mdps.py @@ -7,8 +7,7 @@ def example_building_mdps_01(): nr_choices = 14 # Transition matrix with custom row grouping: nondeterministic choice over the actions available in states - 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) # New row group, for actions of state 0 builder.new_row_group(0) @@ -51,43 +50,44 @@ def example_building_mdps_01(): # State labeling state_labeling = stormpy.storage.StateLabeling(nr_states) # Add labels - labels = {'init', 'one', 'two', 'three', 'four', 'five', 'six', 'done', 'deadlock'} + labels = {"init", "one", "two", "three", "four", "five", "six", "done", "deadlock"} for label in labels: state_labeling.add_label(label) # Set labeling of states - state_labeling.add_label_to_state('init', 0) - 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("init", 0) + 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(nr_states, [7, 8, 9, 10, 11, 12])) + state_labeling.set_states("done", stormpy.BitVector(nr_states, [7, 8, 9, 10, 11, 12])) # Choice labeling choice_labeling = stormpy.storage.ChoiceLabeling(nr_choices) - choice_labels = {'a', 'b'} + choice_labels = {"a", "b"} # Add labels for label in choice_labels: choice_labeling.add_label(label) # Set labels - choice_labeling.add_label_to_choice('a', 0) - choice_labeling.add_label_to_choice('b', 1) + choice_labeling.add_label_to_choice("a", 0) + choice_labeling.add_label_to_choice("b", 1) print(choice_labeling) # Reward models reward_models = {} # Create a vector representing the state-action rewards 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["coin_flips"] = stormpy.SparseRewardModel(optional_state_action_reward_vector=action_reward) # Collect components - components = stormpy.SparseModelComponents(transition_matrix=transition_matrix, state_labeling=state_labeling, - reward_models=reward_models, rate_transitions=False) + components = stormpy.SparseModelComponents( + transition_matrix=transition_matrix, state_labeling=state_labeling, reward_models=reward_models, rate_transitions=False + ) components.choice_labeling = choice_labeling # Build the model @@ -95,5 +95,5 @@ def example_building_mdps_01(): print(mdp) -if __name__ == '__main__': +if __name__ == "__main__": example_building_mdps_01() diff --git a/examples/building_models/01-building-models.py b/examples/building_models/01-building-models.py index 5edfe2919..7a50d43a6 100644 --- a/examples/building_models/01-building-models.py +++ b/examples/building_models/01-building-models.py @@ -5,7 +5,6 @@ import stormpy.pomdp - def example_building_models_01(): path = stormpy.examples.files.drn_ctmc_dft model = stormpy.build_model_from_drn(path) @@ -32,5 +31,6 @@ def example_building_models_01(): # POMDPs need to be in a canonic representation pomdp = stormpy.pomdp.make_canonic(pomdp) -if __name__ == '__main__': + +if __name__ == "__main__": example_building_models_01() diff --git a/examples/building_models/02-building-models.py b/examples/building_models/02-building-models.py index 6b29199c6..dbeea8af2 100644 --- a/examples/building_models/02-building-models.py +++ b/examples/building_models/02-building-models.py @@ -6,10 +6,11 @@ import stormpy.info import pycarl -def example_building_models_02(): +def example_building_models_02(): import stormpy.pars + if stormpy.info.storm_ratfunc_use_cln(): import pycarl.cln as pc else: @@ -21,12 +22,10 @@ def make_factorized_rf(var, cache): return pc.FactorizedRationalFunction(num, denom) # And the parametric + path = stormpy.examples.files.drn_pdtmc_die model = stormpy.build_parametric_model_from_drn(path) - - - parameters = model.collect_probability_parameters() bar_parameters = dict() for p in parameters: @@ -48,8 +47,9 @@ def make_factorized_rf(var, cache): if val_pol - sub == 0: print("Found substitution") e.set_value(make_factorized_rf(repl, cache)) - break # Assume only one substitution per entry + break # Assume only one substitution per entry print(matrix) -if __name__ == '__main__': + +if __name__ == "__main__": example_building_models_02() diff --git a/examples/building_models/03-building-models.py b/examples/building_models/03-building-models.py index 6cb88c53b..fbc77c021 100644 --- a/examples/building_models/03-building-models.py +++ b/examples/building_models/03-building-models.py @@ -28,6 +28,5 @@ def example_building_models_03(): print(", ".join(["{}: {}".format(str(iv.name), valuations.get_integer_value(2, iv.expression_variable)) for iv in integer_variables])) - -if __name__ == '__main__': +if __name__ == "__main__": example_building_models_03() diff --git a/examples/building_models/04-building-models.py b/examples/building_models/04-building-models.py index 70c2858fa..cf080c492 100644 --- a/examples/building_models/04-building-models.py +++ b/examples/building_models/04-building-models.py @@ -3,9 +3,12 @@ import stormpy.examples import stormpy.examples.files import json + """ Building with a fixed (permissive) policy """ + + def example_building_models_04(): path = stormpy.examples.files.prism_mdp_firewire prism_program = stormpy.parse_prism_program(path) @@ -28,15 +31,15 @@ def permissive_policy(state_valuation, action_index): # conditions on the action cond1 = action_name.startswith("snd") # conditions on the state (efficient) - cond2 = state_valuation.get_integer_value(prism_program.get_module("node2").get_integer_variable("x2").expression_variable) <20 + cond2 = state_valuation.get_integer_value(prism_program.get_module("node2").get_integer_variable("x2").expression_variable) < 20 # conditions on the json repr of the state (inefficient, string handling, etc) cond3 = json.loads(str(state_valuation.to_json()))["x1"] < 40 - return (cond1 or (cond2 and cond3)) + return cond1 or (cond2 and cond3) constructor = stormpy.make_sparse_model_builder(prism_program, options, stormpy.StateValuationFunctionActionMaskDouble(permissive_policy)) model = constructor.build() print(model) -if __name__ == '__main__': +if __name__ == "__main__": example_building_models_04() diff --git a/examples/dfts/01-dfts.py b/examples/dfts/01-dfts.py index 160c97599..326c2300f 100644 --- a/examples/dfts/01-dfts.py +++ b/examples/dfts/01-dfts.py @@ -18,12 +18,12 @@ def example_dfts_01(): print("DFT has {} BEs and {} dynamic elements.".format(dft.nr_be(), dft.nr_dynamic())) # Analyze - formula_str = "T=? [ F \"failed\" ]" + 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(result) -if __name__ == '__main__': +if __name__ == "__main__": example_dfts_01() diff --git a/examples/dfts/02-dfts.py b/examples/dfts/02-dfts.py index ff773728b..53deef19d 100644 --- a/examples/dfts/02-dfts.py +++ b/examples/dfts/02-dfts.py @@ -16,8 +16,7 @@ def example_dft_simulator_02(): # Load DFT from Galileo path = stormpy.examples.files.dft_galileo_hecs dft = stormpy.dft.load_dft_galileo_file(path) - print("DFT with {} elements, {} BEs and {} dynamic elements.".format(dft.nr_elements(), dft.nr_be(), - dft.nr_dynamic())) + print("DFT with {} elements, {} BEs and {} dynamic elements.".format(dft.nr_elements(), dft.nr_be(), dft.nr_dynamic())) # Create simulator simulator = DftSimulator(dft, seed=42) @@ -41,5 +40,5 @@ def example_dft_simulator_02(): print("Result for time bound {}: {}".format(timebound, no_failed / no_runs)) -if __name__ == '__main__': +if __name__ == "__main__": example_dft_simulator_02() diff --git a/examples/dfts/interactive_simulator.py b/examples/dfts/interactive_simulator.py index 78e6052c6..e59296ec5 100644 --- a/examples/dfts/interactive_simulator.py +++ b/examples/dfts/interactive_simulator.py @@ -19,7 +19,7 @@ def get_status(simulator): def get_user_fail_be(candidates): while True: inp = input("Select index of BE to fail next (use 'q' to abort)\n") - if inp == 'q': + if inp == "q": return None try: inp_number = int(inp) @@ -35,21 +35,21 @@ def get_user_fail_be(candidates): def get_user_dep_success(): while True: inp = input("Should the failure due a dependency be successful? (y/n)\n") - if inp == 'y': + if inp == "y": return True - elif inp == 'n': + elif inp == "n": return False else: logging.error("Input is not valid.") def main(): - parser = argparse.ArgumentParser(description='Interactive simulator for DFTs.') - parser.add_argument('infile', help='Input Galileo file', type=str) - parser.add_argument('--verbose', '-v', help='print more output', action="store_true") + parser = argparse.ArgumentParser(description="Interactive simulator for DFTs.") + parser.add_argument("infile", help="Input Galileo file", type=str) + parser.add_argument("--verbose", "-v", help="print more output", action="store_true") args = parser.parse_args() - logging.basicConfig(format='%(levelname)s: %(message)s', level=logging.DEBUG if args.verbose else logging.INFO) + logging.basicConfig(format="%(levelname)s: %(message)s", level=logging.DEBUG if args.verbose else logging.INFO) # Load DFT from file if pathlib.Path(args.infile).suffix == ".json": @@ -60,7 +60,7 @@ def main(): dft = stormpy.dft.prepare_for_analysis(dft) # Create simulator - simulator = DftSimulator(dft, seed=42, relevant=['all']) + simulator = DftSimulator(dft, seed=42, relevant=["all"]) # Get initial state logging.info("Initial status:") diff --git a/examples/exploration/01-exploration.py b/examples/exploration/01-exploration.py index fa9d09635..325ecec92 100644 --- a/examples/exploration/01-exploration.py +++ b/examples/exploration/01-exploration.py @@ -10,20 +10,18 @@ def example_exploration_01(): :return: """ program = stormpy.parse_prism_program(stormpy.examples.files.prism_pomdp_maze) - prop = "R=? [F \"goal\"]" + prop = 'R=? [F "goal"]' properties = stormpy.parse_properties(prop, program) model = stormpy.build_model(program, properties) print(model.model_type) - for state in model.states: if state.id in model.initial_states: print(state) 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)) + print("From state {} by action {}, with probability {}, go to state {}".format(state, action, transition.value(), transition.column)) -if __name__ == '__main__': +if __name__ == "__main__": example_exploration_01() diff --git a/examples/exploration/02-exploration.py b/examples/exploration/02-exploration.py index 3adb23f5d..ee9f5a9c2 100644 --- a/examples/exploration/02-exploration.py +++ b/examples/exploration/02-exploration.py @@ -10,7 +10,7 @@ def example_exploration_02(): :return: """ program = stormpy.parse_prism_program(stormpy.examples.files.prism_pomdp_maze) - prop = "R=? [F \"goal\"]" + prop = 'R=? [F "goal"]' properties = stormpy.parse_properties(prop, program) model = stormpy.build_model(program, properties) print(model.model_type) @@ -23,8 +23,7 @@ def example_exploration_02(): print(state) 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)) + print("From state {} by action {}, with probability {}, go to state {}".format(state, action, transition.value(), transition.column)) print(model.nr_observations) @@ -32,6 +31,5 @@ def example_exploration_02(): print("State {} has observation id {}".format(state.id, model.observations[state.id])) - -if __name__ == '__main__': +if __name__ == "__main__": example_exploration_02() diff --git a/examples/exploration/03-exploration.py b/examples/exploration/03-exploration.py index 503b36659..7db1f9ef3 100644 --- a/examples/exploration/03-exploration.py +++ b/examples/exploration/03-exploration.py @@ -22,5 +22,6 @@ def example_exploration_03(): sorted = stormpy.topological_sort(model, forward=False) print(sorted) -if __name__ == '__main__': + +if __name__ == "__main__": example_exploration_03() diff --git a/examples/gspns/01-gspns.py b/examples/gspns/01-gspns.py index 9fcb32aa4..f2a6da2cb 100644 --- a/examples/gspns/01-gspns.py +++ b/examples/gspns/01-gspns.py @@ -17,5 +17,5 @@ def example_gspns_01(): print("Number of timed transitions: {}.".format(gspn.get_number_of_timed_transitions())) -if __name__ == '__main__': +if __name__ == "__main__": example_gspns_01() diff --git a/examples/gspns/02-gspns.py b/examples/gspns/02-gspns.py index f9a49adb3..be4d05c75 100644 --- a/examples/gspns/02-gspns.py +++ b/examples/gspns/02-gspns.py @@ -48,6 +48,5 @@ def example_gspns_02(): gspn.export_gspn_pnpro_file(export_path) -if __name__ == '__main__': +if __name__ == "__main__": example_gspns_02() - diff --git a/examples/highlevel_models/01-highlevel-models.py b/examples/highlevel_models/01-highlevel-models.py index cdc512f0d..2feceb945 100644 --- a/examples/highlevel_models/01-highlevel-models.py +++ b/examples/highlevel_models/01-highlevel-models.py @@ -19,5 +19,5 @@ def example_highlevel_models(): print(f"Variable {v.name} is Boolean") -if __name__ == '__main__': +if __name__ == "__main__": example_highlevel_models() diff --git a/examples/highlevel_models/02-highlevel-models.py b/examples/highlevel_models/02-highlevel-models.py index 13cdf5f9d..b6891a8ad 100644 --- a/examples/highlevel_models/02-highlevel-models.py +++ b/examples/highlevel_models/02-highlevel-models.py @@ -12,17 +12,19 @@ def example_highlevel_models(): """ path = stormpy.examples.files.prism_mdp_slipgrid_sketch prism_program = stormpy.parse_prism_program(path) - prop_string = "Rmin=? [F \"target\"]" + prop_string = 'Rmin=? [F "target"]' properties = stormpy.parse_properties(prop_string, prism_program) # Note: The following is necessary for the code to work correctly, as otherwise there will be a default initial value injected. prism_program = prism_program.replace_variable_initialization_by_init_expression() emgr = prism_program.expression_manager Vvar = prism_program.get_constant("V") - Vvalues = {2,4,6,8,10,12} + Vvalues = {2, 4, 6, 8, 10, 12} all_in_one_program = prism_program.replace_constant_by_variable(Vvar, emgr.create_integer(min(Vvalues)), emgr.create_integer(max(Vvalues))) options = [stormpy.Expression.Eq(Vvar.expression_variable.get_expression(), emgr.create_integer(val)) for val in Vvalues] - all_in_one_program.update_initial_states_expression(stormpy.Expression.And(all_in_one_program.initial_states_expression, stormpy.Expression.Disjunction(options))) + all_in_one_program.update_initial_states_expression( + stormpy.Expression.And(all_in_one_program.initial_states_expression, stormpy.Expression.Disjunction(options)) + ) print(all_in_one_program) for v in all_in_one_program.constants: @@ -34,7 +36,7 @@ def example_highlevel_models(): result = stormpy.check_model_sparse(sparse_model, properties[0], extract_scheduler=True, only_initial_states=True) filter_sparse = stormpy.create_filter_initial_states_sparse(sparse_model) result.filter(filter_sparse) - result_for_vvar = {int(sparse_model.state_valuations.get_integer_value(x, Vvar.expression_variable)) : result.at(x) for x in sparse_model.initial_states} + result_for_vvar = {int(sparse_model.state_valuations.get_integer_value(x, Vvar.expression_variable)): result.at(x) for x in sparse_model.initial_states} print(result_for_vvar) dd_model = stormpy.build_symbolic_model(all_in_one_program) @@ -45,8 +47,9 @@ def example_highlevel_models(): resultvalues = result.get_values() # Notice that the manager seems to be different than the manager for the prism program. So we solve it like this - result_for_vvar = {int(valuation.get_integer_value(valuation.expression_manager.get_variable("V"))) : mc_result for valuation, mc_result in resultvalues } + result_for_vvar = {int(valuation.get_integer_value(valuation.expression_manager.get_variable("V"))): mc_result for valuation, mc_result in resultvalues} print(result_for_vvar) -if __name__ == '__main__': - example_highlevel_models() \ No newline at end of file + +if __name__ == "__main__": + example_highlevel_models() diff --git a/examples/parametric_models/01-parametric-models.py b/examples/parametric_models/01-parametric-models.py index 8553b08ab..638d5e98b 100644 --- a/examples/parametric_models/01-parametric-models.py +++ b/examples/parametric_models/01-parametric-models.py @@ -15,6 +15,7 @@ def example_parametric_models_01(): return import stormpy.pars + path = stormpy.examples.files.prism_pdtmc_die prism_program = stormpy.parse_prism_program(path) @@ -35,5 +36,5 @@ def example_parametric_models_01(): print(result) -if __name__ == '__main__': +if __name__ == "__main__": example_parametric_models_01() diff --git a/examples/parametric_models/02-parametric-models.py b/examples/parametric_models/02-parametric-models.py index e7e4010e3..b13030828 100644 --- a/examples/parametric_models/02-parametric-models.py +++ b/examples/parametric_models/02-parametric-models.py @@ -17,6 +17,7 @@ def example_parametric_models_02(): import stormpy.pars from pycarl.formula import FormulaType, Relation + if stormpy.info.storm_ratfunc_use_cln(): import pycarl.cln.formula else: @@ -42,5 +43,5 @@ def example_parametric_models_02(): print(formula.get_constraint()) -if __name__ == '__main__': +if __name__ == "__main__": example_parametric_models_02() diff --git a/examples/parametric_models/03-parametric-models.py b/examples/parametric_models/03-parametric-models.py index cddda98ce..e9ebfb6af 100644 --- a/examples/parametric_models/03-parametric-models.py +++ b/examples/parametric_models/03-parametric-models.py @@ -7,6 +7,7 @@ import stormpy._config as config + def example_parametric_models_03(): if not config.storm_with_pars: print("Support parameters is missing. Try building storm-pars.") @@ -15,7 +16,7 @@ def example_parametric_models_03(): path = stormpy.examples.files.prism_dtmc_brp prism_program = stormpy.parse_prism_program(path) - formula_str = "P=? [F \"target\"]" + formula_str = 'P=? [F "target"]' properties = stormpy.parse_properties_for_prism_program(formula_str, prism_program) model = stormpy.build_parametric_model(prism_program, properties) @@ -29,11 +30,10 @@ def example_parametric_models_03(): for transition in action.transitions: if transition.value().constant_part() == 1: t += 1 - #print("From state {}, with probability {}, go to state {}".format(state, transition.value(), transition.column)) + # print("From state {}, with probability {}, go to state {}".format(state, transition.value(), transition.column)) print(time.time() - start) print(t) - t2 = 0 start = time.time() for row_group in range(model.nr_states): @@ -53,12 +53,12 @@ def example_parametric_models_03(): t3 = 0 start = time.time() for s in states_and_transitions: - for (v,c) in s: + for v, c in s: if v.constant_part() == 1: t3 += 1 print(time.time() - start) print(t3) -if __name__ == '__main__': +if __name__ == "__main__": example_parametric_models_03() diff --git a/examples/parametric_models/04-parametric-models.py b/examples/parametric_models/04-parametric-models.py index 5ec8bf4f5..9e06854e7 100644 --- a/examples/parametric_models/04-parametric-models.py +++ b/examples/parametric_models/04-parametric-models.py @@ -7,7 +7,6 @@ import stormpy._config as config - def example_parametric_models_04(): # Check support for parameters if not config.storm_with_pars: @@ -15,6 +14,7 @@ def example_parametric_models_04(): return import stormpy.pars + path = stormpy.examples.files.prism_pdtmc_die prism_program = stormpy.parse_prism_program(path) @@ -48,5 +48,5 @@ def example_parametric_models_04(): print("From state {}, with probability {}, go to state {}".format(state, transition.value(), transition.column)) -if __name__ == '__main__': +if __name__ == "__main__": example_parametric_models_04() diff --git a/examples/pomdp/01-pomdps.py b/examples/pomdp/01-pomdps.py index 0d08991f4..ac3b0529f 100644 --- a/examples/pomdp/01-pomdps.py +++ b/examples/pomdp/01-pomdps.py @@ -19,6 +19,7 @@ def example_parametric_models_01(): import stormpy.pars from pycarl.formula import FormulaType, Relation + if stormpy.info.storm_ratfunc_use_cln(): import pycarl.cln.formula else: @@ -53,7 +54,7 @@ def example_parametric_models_01(): path = stormpy.examples.files.prism_par_pomdp_maze prism_program = stormpy.parse_prism_program(path) - formula_str = "P=? [!\"bad\" U \"goal\"]" + formula_str = 'P=? [!"bad" U "goal"]' properties = stormpy.parse_properties_for_prism_program(formula_str, prism_program) # construct the pPOMDP options = stormpy.BuilderOptions([p.raw_formula for p in properties]) @@ -74,11 +75,12 @@ def example_parametric_models_01(): # apply the unknown FSC to obtain a pmc from the POMDP pmc = stormpy.pomdp.apply_unknown_fsc(pomdp, stormpy.pomdp.PomdpFscApplicationMode.simple_linear) - export_pmc = False # Set to True to export the pMC as drn. + export_pmc = False # Set to True to export the pMC as drn. if export_pmc: export_options = stormpy.core.DirectEncodingOptions() export_options.allow_placeholders = False stormpy.export_to_drn(pmc, "test.out", export_options) -if __name__ == '__main__': + +if __name__ == "__main__": example_parametric_models_01() diff --git a/examples/pomdp/high-level-observations.py b/examples/pomdp/high-level-observations.py index d98f7dc2d..5dc0170dc 100644 --- a/examples/pomdp/high-level-observations.py +++ b/examples/pomdp/high-level-observations.py @@ -16,7 +16,7 @@ def example_pomdp_highlevel_observations(): path = stormpy.examples.files.prism_pomdp_maze prism_program = stormpy.parse_prism_program(path) - formula_str = "P=? [!\"bad\" U \"goal\"]" + formula_str = 'P=? [!"bad" U "goal"]' properties = stormpy.parse_properties_for_prism_program(formula_str, prism_program) # construct the POMDP options = stormpy.BuilderOptions([p.raw_formula for p in properties]) @@ -29,5 +29,6 @@ def example_pomdp_highlevel_observations(): assert pomdp.has_observation_valuations assert pomdp.observation_valuations.get_json(0)["o"] == 5 -if __name__ == '__main__': + +if __name__ == "__main__": example_pomdp_highlevel_observations() diff --git a/examples/reward_models/01-reward-models.py b/examples/reward_models/01-reward-models.py index 388bb1a9c..09e13a3eb 100644 --- a/examples/reward_models/01-reward-models.py +++ b/examples/reward_models/01-reward-models.py @@ -6,7 +6,7 @@ def example_reward_models_01(): program = stormpy.parse_prism_program(stormpy.examples.files.prism_dtmc_die) - prop = "R=? [F \"done\"]" + prop = 'R=? [F "done"]' properties = stormpy.parse_properties_for_prism_program(prop, program, None) model = stormpy.build_model(program, properties) assert len(model.reward_models) == 1 @@ -27,5 +27,6 @@ def example_reward_models_01(): assert len(model.reward_models) == 1 assert reward_model_name == "coin_flips" -if __name__ == '__main__': + +if __name__ == "__main__": example_reward_models_01() diff --git a/examples/schedulers/01-schedulers.py b/examples/schedulers/01-schedulers.py index 2febc68a1..951c3f3d5 100644 --- a/examples/schedulers/01-schedulers.py +++ b/examples/schedulers/01-schedulers.py @@ -6,7 +6,7 @@ def example_schedulers_01(): path = stormpy.examples.files.prism_mdp_coin_2_2 - formula_str = "Pmin=? [F \"finished\" & \"all_coins_equal_1\"]" + formula_str = 'Pmin=? [F "finished" & "all_coins_equal_1"]' program = stormpy.parse_prism_program(path) formulas = stormpy.parse_properties_for_prism_program(formula_str, program) @@ -35,6 +35,5 @@ def example_schedulers_01(): print(dtmc) - -if __name__ == '__main__': +if __name__ == "__main__": example_schedulers_01() diff --git a/examples/schedulers/02-schedulers.py b/examples/schedulers/02-schedulers.py index 6c90e02fd..5b58c5319 100644 --- a/examples/schedulers/02-schedulers.py +++ b/examples/schedulers/02-schedulers.py @@ -33,8 +33,8 @@ def example_schedulers_02(): 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("In state {} ({}) choose action {} ({})".format(state, ", ".join(state.labels), action, ", ".join(action.labels))) -if __name__ == '__main__': +if __name__ == "__main__": example_schedulers_02() diff --git a/examples/shortest_paths/01-shortest-paths.py b/examples/shortest_paths/01-shortest-paths.py index c9ad72020..1ebddf4f3 100644 --- a/examples/shortest_paths/01-shortest-paths.py +++ b/examples/shortest_paths/01-shortest-paths.py @@ -24,5 +24,5 @@ def example_shortest_paths(): print("{}-shortest path to state #{}: {}, with distance {}".format(k, state_id, path, distance)) -if __name__ == '__main__': +if __name__ == "__main__": example_shortest_paths() diff --git a/examples/simulator/01-simulator.py b/examples/simulator/01-simulator.py index ada876aa4..679acd3c5 100644 --- a/examples/simulator/01-simulator.py +++ b/examples/simulator/01-simulator.py @@ -3,9 +3,12 @@ import stormpy.examples import stormpy.examples.files + """ Simulator for deterministic models """ + + def example_simulator_01(): path = stormpy.examples.files.prism_dtmc_die prism_program = stormpy.parse_prism_program(path) @@ -39,10 +42,8 @@ def example_simulator_01(): else: final_outcomes[observation] += 1 simulator.restart() - print(", ".join([f"{str(k)}: {v}" for k,v in final_outcomes.items()])) - - + print(", ".join([f"{str(k)}: {v}" for k, v in final_outcomes.items()])) -if __name__ == '__main__': +if __name__ == "__main__": example_simulator_01() diff --git a/examples/simulator/02-simulator.py b/examples/simulator/02-simulator.py index 56d3bd747..f956a4db2 100644 --- a/examples/simulator/02-simulator.py +++ b/examples/simulator/02-simulator.py @@ -8,6 +8,8 @@ """ Simulator for nondeterministic models """ + + def example_simulator_02(): path = stormpy.examples.files.prism_mdp_maze prism_program = stormpy.parse_prism_program(path) @@ -22,14 +24,14 @@ def example_simulator_02(): path = [f"{state}"] for n in range(20): actions = simulator.available_actions() - select_action = random.randint(0,len(actions)-1) - #print(f"Randomly select action nr: {select_action} from actions {actions}") + select_action = random.randint(0, len(actions) - 1) + # print(f"Randomly select action nr: {select_action} from actions {actions}") path.append(f"--act={actions[select_action]}-->") state, reward, labels = simulator.step(actions[select_action]) - #print(state) + # print(state) path.append(f"{state}") if simulator.is_done(): - #print("Trapped!") + # print("Trapped!") break paths.append(path) for path in paths: @@ -51,20 +53,19 @@ def example_simulator_02(): path = [f"{state}"] for n in range(20): actions = simulator.available_actions() - select_action = random.randint(0,len(actions)-1) - #print(f"Randomly select action nr: {select_action} from actions {actions}") + select_action = random.randint(0, len(actions) - 1) + # print(f"Randomly select action nr: {select_action} from actions {actions}") path.append(f"--act={actions[select_action]}-->") state, reward, labels = simulator.step(actions[select_action]) - #print(state) + # print(state) path.append(f"{state}") if simulator.is_done(): - #print("Trapped!") + # print("Trapped!") break paths.append(path) for path in paths: print(" ".join(path)) - -if __name__ == '__main__': +if __name__ == "__main__": example_simulator_02() diff --git a/examples/simulator/03-simulator.py b/examples/simulator/03-simulator.py index 1bac03765..a07b4991a 100644 --- a/examples/simulator/03-simulator.py +++ b/examples/simulator/03-simulator.py @@ -3,9 +3,12 @@ import stormpy.examples import stormpy.examples.files + """ Simulator for programs """ + + def example_simulator_03(): path = stormpy.examples.files.prism_mdp_firewire prism_program = stormpy.parse_prism_program(path) @@ -25,5 +28,5 @@ def example_simulator_03(): simulator.restart() -if __name__ == '__main__': +if __name__ == "__main__": example_simulator_03() diff --git a/examples/simulator/04-simulator.py b/examples/simulator/04-simulator.py index aa669dc0a..809f71251 100644 --- a/examples/simulator/04-simulator.py +++ b/examples/simulator/04-simulator.py @@ -3,13 +3,16 @@ import stormpy.examples import stormpy.examples.files + """ Simulator for programs """ + + def example_simulator_04(): path = stormpy.examples.files.prism_mdp_coin_2_2 prism_program = stormpy.parse_prism_program(path) - #prism_program = stormpy.preprocess_symbolic_input(prism_program, [], "delay=10,fast=0.8")[0].as_prism_program() + # prism_program = stormpy.preprocess_symbolic_input(prism_program, [], "delay=10,fast=0.8")[0].as_prism_program() new_prism_program = prism_program.label_unlabelled_commands(dict()) simulator = stormpy.simulator.create_simulator(new_prism_program, seed=42) @@ -49,5 +52,5 @@ def example_simulator_04(): simulator.restart() -if __name__ == '__main__': +if __name__ == "__main__": example_simulator_04() diff --git a/lib/stormpy/__init__.py b/lib/stormpy/__init__.py index 6df1255e1..cccb28ceb 100644 --- a/lib/stormpy/__init__.py +++ b/lib/stormpy/__init__.py @@ -1,7 +1,7 @@ import sys if sys.version_info[0] == 2: - raise ImportError('Python 2.x is not supported for stormpy.') + raise ImportError("Python 2.x is not supported for stormpy.") from ._config import * @@ -138,7 +138,7 @@ def build_sparse_model(symbolic_description, properties=None): def build_sparse_parametric_model(symbolic_description, properties=None): """ Build a parametric model in sparse representation from a symbolic description. - + :param symbolic_description: Symbolic model description to translate into a model. :param List[Property] properties: List of properties that should be preserved during the translation. If None, then all properties are preserved. :return: Parametric model in sparse representation. @@ -204,7 +204,7 @@ def build_model_from_drn(file, options=DirectEncodingParserOptions()): return _convert_sparse_model(intermediate, parametric=False) -def build_parametric_model_from_drn(file, options = DirectEncodingParserOptions()): +def build_parametric_model_from_drn(file, options=DirectEncodingParserOptions()): """ Build a parametric model in sparse representation from the explicit DRN representation. @@ -216,7 +216,7 @@ def build_parametric_model_from_drn(file, options = DirectEncodingParserOptions( return _convert_sparse_model(intermediate, parametric=True) -def build_interval_model_from_drn(file, options = DirectEncodingParserOptions()): +def build_interval_model_from_drn(file, options=DirectEncodingParserOptions()): """ Build an interval model in sparse representation from the explicit DRN representation. @@ -285,14 +285,19 @@ def model_checking(model, property, only_initial_states=False, extract_scheduler :rtype: CheckResult """ if model.is_sparse_model: - return check_model_sparse(model, property, only_initial_states=only_initial_states, - extract_scheduler=extract_scheduler, force_fully_observable=force_fully_observable, environment=environment) + return check_model_sparse( + model, + property, + only_initial_states=only_initial_states, + extract_scheduler=extract_scheduler, + force_fully_observable=force_fully_observable, + environment=environment, + ) else: - assert (model.is_symbolic_model) + assert model.is_symbolic_model if extract_scheduler: raise StormError("Model checking based on dd engine does not support extracting schedulers right now.") - return check_model_dd(model, property, only_initial_states=only_initial_states, - environment=environment) + return check_model_dd(model, property, only_initial_states=only_initial_states, environment=environment) def check_model_sparse(model, property, only_initial_states=False, extract_scheduler=False, force_fully_observable=False, hint=None, environment=Environment()): @@ -334,8 +339,6 @@ def check_model_sparse(model, property, only_initial_states=False, extract_sched else: raise RuntimeError("Model checking of partially observable models is handled via dedicated methods, unless the force fully-observable is set.") - - if model.supports_parameters: task = core.ParametricCheckTask(formula, only_initial_states) task.set_produce_schedulers(extract_scheduler) @@ -516,7 +519,7 @@ def topological_sort(model, forward=True, initial=[]): raise StormError("Unknown kind of model.") -def get_reachable_states(model, initial_states, constraint_states, target_states, maximal_steps = None, choice_filter = None ): +def get_reachable_states(model, initial_states, constraint_states, target_states, maximal_steps=None, choice_filter=None): """ Get the states that are reachable in a sparse model @@ -582,7 +585,7 @@ def construct_submodel(model, states, actions, keep_unreachable_states=True, opt return core._construct_subsystem_Double(model, states, actions, keep_unreachable_states, options) -def eliminate_ECs(matrix, subsystem, possible_ecs, add_sink_row_states, add_self_loop_at_sink_states = False): +def eliminate_ECs(matrix, subsystem, possible_ecs, add_sink_row_states, add_self_loop_at_sink_states=False): """ For each such EC (that is not contained in another EC), we add a new state and redirect all incoming and outgoing transitions of the EC to (and from) this state. diff --git a/lib/stormpy/dft/modules.py b/lib/stormpy/dft/modules.py index faf234ab8..87781b5de 100644 --- a/lib/stormpy/dft/modules.py +++ b/lib/stormpy/dft/modules.py @@ -1,5 +1,6 @@ import stormpy.dft + def _get_tuple(dft, index): """ Get json representation of element. @@ -8,7 +9,8 @@ def _get_tuple(dft, index): :param index: Index (Id). :return: Dict with 'name' and 'index'. """ - return {'id': str(index), 'name': dft.get_element(index).name} + return {"id": str(index), "name": dft.get_element(index).name} + def _modules_json(dft, module): """ @@ -19,12 +21,12 @@ def _modules_json(dft, module): :return: JSON object containing all modules in a recursive hierarchy. """ data = dict() - data['representative'] = _get_tuple(dft, module.representative()) - data['elements'] = [_get_tuple(dft, elem) for elem in module.elements()] + data["representative"] = _get_tuple(dft, module.representative()) + data["elements"] = [_get_tuple(dft, elem) for elem in module.elements()] submodules = [] for submodule in module.submodules(): submodules.append(_modules_json(dft, submodule)) - data['submodules'] = submodules + data["submodules"] = submodules return data diff --git a/lib/stormpy/pomdp/__init__.py b/lib/stormpy/pomdp/__init__.py index d490e77b4..fceb6f250 100644 --- a/lib/stormpy/pomdp/__init__.py +++ b/lib/stormpy/pomdp/__init__.py @@ -1,6 +1,7 @@ from . import pomdp from .pomdp import * + def make_canonic(model): """ Make the POMDP canonic @@ -13,6 +14,7 @@ def make_canonic(model): else: return pomdp._make_canonic_Double(model) + def make_simple(model, keep_state_valuations=False): """ Make the POMDP simple (aka alternating), i.e., each state has at most two actions, and if there is nondeterminism, then there is no probabilistic branching, @@ -25,6 +27,7 @@ def make_simple(model, keep_state_valuations=False): else: return pomdp._make_simple_Double(model, keep_state_valuations) + def unfold_memory(model, memory, add_memory_labels=False, keep_state_valuations=False): """ Unfold the memory for an FSC into the POMDP @@ -38,6 +41,7 @@ def unfold_memory(model, memory, add_memory_labels=False, keep_state_valuations= else: return pomdp._unfold_memory_Double(model, memory, add_memory_labels, keep_state_valuations) + def apply_unknown_fsc(model, mode): if model.supports_parameters: return pomdp._apply_unknown_fsc_Rf(model, mode) @@ -75,4 +79,4 @@ def create_observation_trace_unfolder(model, risk_assessment, expr_manager): if model.is_exact: return pomdp.ObservationTraceUnfolderExact(model, risk_assessment, expr_manager) else: - return pomdp.ObservationTraceUnfolderDouble(model, risk_assessment, expr_manager) \ No newline at end of file + return pomdp.ObservationTraceUnfolderDouble(model, risk_assessment, expr_manager) diff --git a/lib/stormpy/simulator.py b/lib/stormpy/simulator.py index e6b6e0e20..d8866739c 100644 --- a/lib/stormpy/simulator.py +++ b/lib/stormpy/simulator.py @@ -4,17 +4,20 @@ class SimulatorObservationMode(Enum): - STATE_LEVEL = 0, + STATE_LEVEL = (0,) PROGRAM_LEVEL = 1 + class SimulatorActionMode(Enum): - INDEX_LEVEL = 0, + INDEX_LEVEL = (0,) GLOBAL_NAMES = 1 + class Simulator: """ Abstract base class for simulators. """ + def __init__(self, seed=None): self._seed = seed self._observation_mode = SimulatorObservationMode.STATE_LEVEL @@ -47,7 +50,7 @@ def step(self, action=None): """ raise NotImplementedError("Abstract superclass") - def restart(self, state = None): + def restart(self, state=None): """ Reset the simulator to the initial state """ @@ -149,7 +152,7 @@ def _report_observation(self): """ :return: """ - #TODO this should be ensured earlier + # TODO this should be ensured earlier assert self._model.model_type == stormpy.storage.ModelType.POMDP if self._observation_mode == SimulatorObservationMode.STATE_LEVEL: return self._model.get_observation(self._engine.get_current_state()) @@ -159,9 +162,9 @@ def _report_observation(self): def _report_result(self): if self._full_observe: - return self._report_state(), self._report_rewards(), self._report_labels() + return self._report_state(), self._report_rewards(), self._report_labels() else: - return self._report_observation(), self._report_rewards(), self._report_labels() + return self._report_observation(), self._report_rewards(), self._report_labels() def _report_rewards(self): return self._engine.get_last_reward() @@ -201,7 +204,7 @@ def step(self, action=None): raise ValueError(f"Unrecognized type of action {action}") return self._report_result() - def restart(self, state = None): + def restart(self, state=None): if state is not None: raise RuntimeError("Not implemented") self._engine.reset_to_initial_state() @@ -230,7 +233,7 @@ class PrismSimulator(Simulator): def __init__(self, program, seed=None, options=stormpy.BuilderOptions()): super().__init__(seed) self._program = program - #TODO support exact arithmetic here + # TODO support exact arithmetic here self._engine = stormpy.core._DiscreteTimePrismProgramSimulatorDouble(program, options) if seed is not None: self._engine.set_seed(seed) @@ -259,9 +262,9 @@ def _report_observation(self): def _report_result(self): if self._full_observe: - return self._report_state(), self._report_rewards(), self._report_labels() + return self._report_state(), self._report_rewards(), self._report_labels() else: - return self._report_observation(), self._report_rewards(), self._report_labels() + return self._report_observation(), self._report_rewards(), self._report_labels() def _report_rewards(self): return self._engine.get_last_reward() @@ -304,13 +307,13 @@ def step(self, action=None): raise ValueError(f"Unrecognized type of action {action}") return self._report_result() - def restart(self, state = None): + def restart(self, state=None): if state is None: self._engine.reset_to_initial_state() else: - if isinstance(state,stormpy.BitVector): + if isinstance(state, stormpy.BitVector): self._engine._reset_to_state_from_compressed_state(state) - elif isinstance(state,stormpy.SimpleValuation): + elif isinstance(state, stormpy.SimpleValuation): self._engine._reset_to_state_from_valuation(state) else: raise ValueError(f"States of type {type(state)} are not supported yet.") @@ -327,7 +330,12 @@ def set_observation_mode(self, mode): def get_reward_names(self): return self._engine.get_reward_names() -def create_simulator(model, seed = None, options=None, ): + +def create_simulator( + model, + seed=None, + options=None, +): """ Factory method for creating a simulator. diff --git a/lib/stormpy/utility/multiobjective_plotting.py b/lib/stormpy/utility/multiobjective_plotting.py index a85413cc6..99beff434 100644 --- a/lib/stormpy/utility/multiobjective_plotting.py +++ b/lib/stormpy/utility/multiobjective_plotting.py @@ -1,6 +1,7 @@ import numpy as np import stormpy + def plot_convex_pareto_curve_demo(ax, underapprox_points, overapprox_points, lowerleft, upperright): """ @@ -18,9 +19,9 @@ def plot_convex_pareto_curve_demo(ax, underapprox_points, overapprox_points, low ax.grid() under_hull = ConvexHull(underapprox_points) over_hull = ConvexHull(overapprox_points) - ax.set_facecolor('r') - ax.fill(overapprox_points[over_hull.vertices,0], overapprox_points[over_hull.vertices,1], 'w', 1) - ax.fill(underapprox_points[under_hull.vertices,0], underapprox_points[under_hull.vertices,1], 'g', 1) + ax.set_facecolor("r") + ax.fill(overapprox_points[over_hull.vertices, 0], overapprox_points[over_hull.vertices, 1], "w", 1) + ax.fill(underapprox_points[under_hull.vertices, 0], underapprox_points[under_hull.vertices, 1], "g", 1) def _prepare_points_for_convex_pareto_plotting(points, lower_corner, upper_corner, multi_obj_formula): @@ -32,7 +33,8 @@ def _prepare_points_for_convex_pareto_plotting(points, lower_corner, upper_corne :param multi_obj_formula: :return: """ - def direction_as_operation(dir : stormpy.OptimizationDirection): + + def direction_as_operation(dir: stormpy.OptimizationDirection): return max if dir == stormpy.OptimizationDirection.Maximize else min if multi_obj_formula.nr_subformulas != 2: @@ -50,6 +52,7 @@ def direction_as_operation(dir : stormpy.OptimizationDirection): points = np.concatenate((np.array(points), origin, x_cut, y_cut), axis=0) return points + def prepare_multiobjective_result_for_plotting(result, lower_corner, upper_corner, formula): """ Takes a multiobjective model checking results and prepares it for plotting. @@ -61,4 +64,4 @@ def prepare_multiobjective_result_for_plotting(result, lower_corner, upper_corne :return: A tuple with two sets of points representing an under- and overapproximation of the vertices """ results = [result.get_underapproximation(), result.get_overapproximation()] - return [_prepare_points_for_convex_pareto_plotting(h.vertices, lower_corner, upper_corner, formula) for h in results] \ No newline at end of file + return [_prepare_points_for_convex_pareto_plotting(h.vertices, lower_corner, upper_corner, formula) for h in results] diff --git a/setup.py b/setup.py index c38365cd5..3a1e982c6 100755 --- a/setup.py +++ b/setup.py @@ -10,32 +10,32 @@ from setup.config import SetupConfig if sys.version_info[0] == 2: - sys.exit('Sorry, Python 2.x is not supported') + sys.exit("Sorry, Python 2.x is not supported") # Minimal storm version required storm_min_version = "1.9.1" # Get the long description from the README file -with open(os.path.join(os.path.abspath(os.path.dirname(__file__)), 'README.md'), encoding='utf-8') as f: +with open(os.path.join(os.path.abspath(os.path.dirname(__file__)), "README.md"), encoding="utf-8") as f: long_description = f.read() class CMakeExtension(Extension): - def __init__(self, name, sourcedir=''): + def __init__(self, name, sourcedir=""): Extension.__init__(self, name, sources=[]) self.sourcedir = os.path.abspath(sourcedir) class CMakeBuild(build_ext): user_options = build_ext.user_options + [ - ('storm-dir=', None, 'Path to storm root (binary) location'), - ('disable-dft', None, 'Disable support for DFTs'), - ('disable-gspn', None, 'Disable support for GSPNs'), - ('disable-pars', None, 'Disable support for parametric models'), - ('disable-pomdp', None, 'Disable support for POMDP analysis'), - ('debug', None, 'Build in Debug mode'), - ('jobs=', 'j', 'Number of jobs to use for compiling'), - ('pybind-version=', None, 'Pybind11 version to use'), + ("storm-dir=", None, "Path to storm root (binary) location"), + ("disable-dft", None, "Disable support for DFTs"), + ("disable-gspn", None, "Disable support for GSPNs"), + ("disable-pars", None, "Disable support for parametric models"), + ("disable-pomdp", None, "Disable support for POMDP analysis"), + ("debug", None, "Build in Debug mode"), + ("jobs=", "j", "Number of jobs to use for compiling"), + ("pybind-version=", None, "Pybind11 version to use"), ] config = SetupConfig() @@ -45,10 +45,9 @@ def _extdir(self, extname): def run(self): try: - _ = subprocess.check_output(['cmake', '--version']) + _ = subprocess.check_output(["cmake", "--version"]) except OSError: - raise RuntimeError("CMake must be installed to build the following extensions: " + - ", ".join(e.name for e in self.extensions)) + raise RuntimeError("CMake must be installed to build the following extensions: " + ", ".join(e.name for e in self.extensions)) # Build cmake version info print("Stormpy - Building into {}".format(self.build_temp)) @@ -62,24 +61,23 @@ def run(self): cmake_args = [] storm_dir = os.path.expanduser(self.config.get_as_string("storm_dir")) if storm_dir: - cmake_args += ['-DSTORM_DIR_HINT=' + storm_dir] - _ = subprocess.check_output(['cmake', os.path.abspath("cmake")] + cmake_args, cwd=build_temp_version) - cmake_conf = setup_helper.load_cmake_config(os.path.join(build_temp_version, 'generated/config.py')) + cmake_args += ["-DSTORM_DIR_HINT=" + storm_dir] + _ = subprocess.check_output(["cmake", os.path.abspath("cmake")] + cmake_args, cwd=build_temp_version) + cmake_conf = setup_helper.load_cmake_config(os.path.join(build_temp_version, "generated/config.py")) # Set storm directory if storm_dir == "": storm_dir = cmake_conf.STORM_DIR if storm_dir != cmake_conf.STORM_DIR: - print("Stormpy - WARNING: Using different storm directory {} instead of given {}!".format( - cmake_conf.STORM_DIR, - storm_dir)) + print("Stormpy - WARNING: Using different storm directory {} instead of given {}!".format(cmake_conf.STORM_DIR, storm_dir)) storm_dir = cmake_conf.STORM_DIR # Check version - from packaging.version import Version # Need to import here because otherwise packaging cannot be automatically installed as required dependency + from packaging.version import Version # Need to import here because otherwise packaging cannot be automatically installed as required dependency + storm_version, storm_commit = setup_helper.parse_storm_version(cmake_conf.STORM_VERSION) if Version(storm_version) < Version(storm_min_version): - print('Stormpy - Error: Storm version {} from \'{}\' is not supported anymore!'.format(storm_version, storm_dir)) + print("Stormpy - Error: Storm version {} from '{}' is not supported anymore!".format(storm_version, storm_dir)) print(" For more information, see https://moves-rwth.github.io/stormpy/installation.html#compatibility-of-stormpy-and-storm") sys.exit(42) # Custom exit code which can be used for incompatible checks @@ -91,6 +89,7 @@ def run(self): # Set pybind version from pycarl._config import PYBIND_VERSION as pycarl_pybind_version + pybind_version = self.config.get_as_string("pybind_version") if pybind_version == "": pybind_version = pycarl_pybind_version @@ -117,30 +116,30 @@ def run(self): else: print("Stormpy - WARNING: No support for POMDP analysis!") - build_type = 'Debug' if self.config.get_as_bool("debug") else 'Release' + build_type = "Debug" if self.config.get_as_bool("debug") else "Release" # Set cmake build options - cmake_args = ['-DCMAKE_LIBRARY_OUTPUT_DIRECTORY=' + self._extdir("core")] - cmake_args += ['-DPython_EXECUTABLE=' + sys.executable] - cmake_args += ['-DCMAKE_BUILD_TYPE=' + build_type] - cmake_args += ['-DPYBIND_VERSION=' + pybind_version] + cmake_args = ["-DCMAKE_LIBRARY_OUTPUT_DIRECTORY=" + self._extdir("core")] + cmake_args += ["-DPython_EXECUTABLE=" + sys.executable] + cmake_args += ["-DCMAKE_BUILD_TYPE=" + build_type] + cmake_args += ["-DPYBIND_VERSION=" + pybind_version] if storm_dir is not None: - cmake_args += ['-DSTORM_DIR_HINT=' + storm_dir] - cmake_args += ['-DUSE_STORM_DFT=' + ('ON' if use_dft else 'OFF')] - cmake_args += ['-DUSE_STORM_GSPN=' + ('ON' if use_gspn else 'OFF')] - cmake_args += ['-DUSE_STORM_PARS=' + ('ON' if use_pars else 'OFF')] - cmake_args += ['-DUSE_STORM_POMDP=' + ('ON' if use_pomdp else 'OFF')] + cmake_args += ["-DSTORM_DIR_HINT=" + storm_dir] + cmake_args += ["-DUSE_STORM_DFT=" + ("ON" if use_dft else "OFF")] + cmake_args += ["-DUSE_STORM_GSPN=" + ("ON" if use_gspn else "OFF")] + cmake_args += ["-DUSE_STORM_PARS=" + ("ON" if use_pars else "OFF")] + cmake_args += ["-DUSE_STORM_POMDP=" + ("ON" if use_pomdp else "OFF")] # Configure extensions env = os.environ.copy() - env['CXXFLAGS'] = '{} -DVERSION_INFO=\\"{}\\"'.format(env.get('CXXFLAGS', ''), self.distribution.get_version()) + env["CXXFLAGS"] = '{} -DVERSION_INFO=\\"{}\\"'.format(env.get("CXXFLAGS", ""), self.distribution.get_version()) setup_helper.ensure_dir_exists(self.build_temp) print("Stormpy - CMake args={}".format(cmake_args)) # Call cmake - subprocess.check_call(['cmake', os.path.abspath("")] + cmake_args, cwd=self.build_temp, env=env) + subprocess.check_call(["cmake", os.path.abspath("")] + cmake_args, cwd=self.build_temp, env=env) # Set build args - build_args = ['--config', build_type] - build_args += ['--', '-j{}'.format(self.config.get_as_int("jobs"))] + build_args = ["--config", build_type] + build_args += ["--", "-j{}".format(self.config.get_as_int("jobs"))] # Build extensions for ext in self.extensions: @@ -157,7 +156,7 @@ def run(self): print("Stormpy - Bindings for POMDP analysis skipped") continue # Call make - subprocess.check_call(['cmake', '--build', '.', '--target', ext.name] + build_args, cwd=self.build_temp) + subprocess.check_call(["cmake", "--build", ".", "--target", ext.name] + build_args, cwd=self.build_temp) def initialize_options(self): build_ext.initialize_options(self) @@ -197,45 +196,43 @@ def finalize_options(self): url="https://github.com/moves-rwth/stormpy/", description="stormpy - Python Bindings for Storm", long_description=long_description, - long_description_content_type='text/markdown', + long_description_content_type="text/markdown", project_urls={ - 'Documentation': 'https://moves-rwth.github.io/stormpy/', - 'Source': 'https://github.com/moves-rwth/stormpy/', - 'Bug reports': 'https://github.com/moves-rwth/stormpy/issues', + "Documentation": "https://moves-rwth.github.io/stormpy/", + "Source": "https://github.com/moves-rwth/stormpy/", + "Bug reports": "https://github.com/moves-rwth/stormpy/issues", }, classifiers=[ - 'Intended Audience :: Science/Research', - 'Topic :: Scientific/Engineering', - 'Topic :: Software Development :: Libraries :: Python Modules', + "Intended Audience :: Science/Research", + "Topic :: Scientific/Engineering", + "Topic :: Software Development :: Libraries :: Python Modules", ], - - packages=find_packages('lib'), - package_dir={'': 'lib'}, + packages=find_packages("lib"), + package_dir={"": "lib"}, include_package_data=True, - package_data={'stormpy.examples': ['examples/files/*']}, - ext_package='stormpy', - ext_modules=[CMakeExtension('core'), - CMakeExtension('info'), - CMakeExtension('logic'), - CMakeExtension('storage'), - CMakeExtension('utility'), - CMakeExtension('dft'), - CMakeExtension('gspn'), - CMakeExtension('pars'), - CMakeExtension('pomdp') - ], - cmdclass={'build_ext': CMakeBuild}, + package_data={"stormpy.examples": ["examples/files/*"]}, + ext_package="stormpy", + ext_modules=[ + CMakeExtension("core"), + CMakeExtension("info"), + CMakeExtension("logic"), + CMakeExtension("storage"), + CMakeExtension("utility"), + CMakeExtension("dft"), + CMakeExtension("gspn"), + CMakeExtension("pars"), + CMakeExtension("pomdp"), + ], + cmdclass={"build_ext": CMakeBuild}, zip_safe=False, - install_requires=['pycarl>=2.3.0'], - setup_requires=['pycarl>=2.3.0', # required to check pybind version used for pycarl - 'packaging' - ], + install_requires=["pycarl>=2.3.0"], + setup_requires=["pycarl>=2.3.0", "packaging"], # required to check pybind version used for pycarl extras_require={ - "numpy": ["numpy"], - "plot": ["matplotlib","numpy","scipy"], + "numpy": ["numpy"], + "plot": ["matplotlib", "numpy", "scipy"], "test": ["pytest", "nbval", "numpy"], - "doc": ["Sphinx", "sphinx-bootstrap-theme", "nbsphinx", "ipython", "ipykernel"], # also requires pandoc to be installed + "doc": ["Sphinx", "sphinx-bootstrap-theme", "nbsphinx", "ipython", "ipykernel"], # also requires pandoc to be installed "dev": ["black"], }, - python_requires='>=3.7', # required by packaging + python_requires=">=3.7", # required by packaging ) diff --git a/setup/__init__.py b/setup/__init__.py index e17edbb67..9a01f92a3 100644 --- a/setup/__init__.py +++ b/setup/__init__.py @@ -1 +1 @@ -# Intentionally left empty \ No newline at end of file +# Intentionally left empty diff --git a/setup/config.py b/setup/config.py index 0a8b2b519..2e6e49486 100644 --- a/setup/config.py +++ b/setup/config.py @@ -34,7 +34,7 @@ def _default_values(): "disable_pomdp": False, "debug": False, "jobs": str(no_jobs), - "pybind_version": "" + "pybind_version": "", } def load_from_file(self, path): @@ -52,7 +52,7 @@ def write_config(self, path): Save config with build settings. :param path Path to config file. """ - with open(path, 'w') as configfile: + with open(path, "w") as configfile: self.config.write(configfile) def get_as_bool(self, name): diff --git a/setup/helper.py b/setup/helper.py index 8e9288cd5..8357f2954 100755 --- a/setup/helper.py +++ b/setup/helper.py @@ -27,7 +27,7 @@ def parse_storm_version(version_string): :param version_string: String containing version information. :return: Tuple (version, commit) """ - split = version_string.split('-') + split = version_string.split("-") version = split[0] commit = "" if len(split) > 1: @@ -43,7 +43,7 @@ def obtain_version(): """ verstr = "unknown" try: - verstrline = open('lib/stormpy/_version.py', "rt").read() + verstrline = open("lib/stormpy/_version.py", "rt").read() except EnvironmentError: pass # Okay, there is no version file. else: @@ -71,4 +71,5 @@ def load_cmake_config(path): else: # Deprecated method for Python <= 3.4 from importlib.machinery import SourceFileLoader + return SourceFileLoader("genconfig", path).load_module() diff --git a/tests/configurations.py b/tests/configurations.py index 7de939a48..9b293424d 100644 --- a/tests/configurations.py +++ b/tests/configurations.py @@ -12,18 +12,21 @@ try: import numpy + has_numpy = True except ImportError: has_numpy = False try: import matplotlib + has_matplotlib = True except ImportError: has_matplotlib = False try: import scipy + has_scipy = True except ImportError: has_scipy = False diff --git a/tests/conftest.py b/tests/conftest.py index 9661c490a..0028bcfd7 100644 --- a/tests/conftest.py +++ b/tests/conftest.py @@ -1,4 +1,4 @@ import sys import os -sys.path.append(os.path.join(os.path.dirname(__file__), 'helpers')) +sys.path.append(os.path.join(os.path.dirname(__file__), "helpers")) diff --git a/tests/core/test_bisimulation.py b/tests/core/test_bisimulation.py index 9c5812003..efa9aeaa0 100644 --- a/tests/core/test_bisimulation.py +++ b/tests/core/test_bisimulation.py @@ -10,7 +10,7 @@ def test_bisimulation(self): assert program.nr_modules == 1 assert program.model_type == stormpy.PrismModelType.DTMC - prop = "P=? [F \"observe0Greater1\"]" + prop = 'P=? [F "observe0Greater1"]' properties = stormpy.parse_properties_for_prism_program(prop, program) model = stormpy.build_model(program, properties) assert model.nr_states == 7403 @@ -32,7 +32,7 @@ def test_bisimulation(self): def test_symbolic_bisimulation(self): program = stormpy.parse_prism_program(get_example_path("dtmc", "crowds5_5.pm")) - prop = "P=? [F \"observe0Greater1\"]" + prop = 'P=? [F "observe0Greater1"]' properties = stormpy.parse_properties_for_prism_program(prop, program) model = stormpy.build_symbolic_model(program, properties) assert model.nr_states == 7403 @@ -78,7 +78,7 @@ def test_parametric_bisimulation(self): def test_symbolic_parametric_bisimulation(self): program = stormpy.parse_prism_program(get_example_path("pdtmc", "brp16_2.pm")) - prop = "P=? [F \"error\"]" + prop = 'P=? [F "error"]' properties = stormpy.parse_properties_for_prism_program(prop, program) model = stormpy.build_symbolic_parametric_model(program, properties) assert model.nr_states == 613 diff --git a/tests/core/test_building.py b/tests/core/test_building.py index 135254573..90beacd2c 100644 --- a/tests/core/test_building.py +++ b/tests/core/test_building.py @@ -2,6 +2,7 @@ import stormpy.examples import stormpy.examples.files + class TestBuilding: def test_explicit_builder(self): path = stormpy.examples.files.prism_dtmc_die @@ -22,15 +23,14 @@ def test_explicit_builder(self): # and export the model from building state_mapping = model_builder.export_lookup() - #lookup 1 - state = { s_var : prism_program.expression_manager.create_integer(3), d_var : prism_program.expression_manager.create_integer(0)} + # lookup 1 + state = {s_var: prism_program.expression_manager.create_integer(3), d_var: prism_program.expression_manager.create_integer(0)} id = state_mapping.lookup(state) assert model.state_valuations.get_integer_value(id, s_var) == 3 assert model.state_valuations.get_integer_value(id, d_var) == 0 - #lookup 2 - state = { s_var : prism_program.expression_manager.create_integer(7), d_var : prism_program.expression_manager.create_integer(3)} + # lookup 2 + state = {s_var: prism_program.expression_manager.create_integer(7), d_var: prism_program.expression_manager.create_integer(3)} id = state_mapping.lookup(state) assert model.state_valuations.get_integer_value(id, s_var) == 7 assert model.state_valuations.get_integer_value(id, d_var) == 3 - diff --git a/tests/core/test_core.py b/tests/core/test_core.py index fc79932fd..13fdb6cbf 100644 --- a/tests/core/test_core.py +++ b/tests/core/test_core.py @@ -4,6 +4,7 @@ def test_init(self): def test_pycarl(self): import stormpy + rational = stormpy.Rational(0.25) assert str(rational) == "1/4" pol1 = stormpy.FactorizedPolynomial(32) diff --git a/tests/core/test_environment.py b/tests/core/test_environment.py index fa6b0ea15..ec951ef85 100644 --- a/tests/core/test_environment.py +++ b/tests/core/test_environment.py @@ -1,6 +1,7 @@ import stormpy from helpers.helper import get_example_path + class TestEnvironment: def test_environment(self): env = stormpy.Environment() diff --git a/tests/core/test_modelchecking.py b/tests/core/test_modelchecking.py index 020161fcb..cd7ba6e7b 100644 --- a/tests/core/test_modelchecking.py +++ b/tests/core/test_modelchecking.py @@ -9,7 +9,7 @@ class TestModelChecking: def test_model_checking_prism_dtmc(self): program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm")) - formulas = stormpy.parse_properties_for_prism_program("P=? [ F \"one\" ]", program) + formulas = stormpy.parse_properties_for_prism_program('P=? [ F "one" ]', program) model = stormpy.build_model(program, formulas) assert model.nr_states == 13 assert model.nr_transitions == 20 @@ -22,7 +22,7 @@ def test_model_checking_prism_dtmc(self): @spot def test_model_checking_prism_dtmc_ltl(self): program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm")) - formulas = stormpy.parse_properties_for_prism_program("P=? [ FG \"one\" ]", program) + formulas = stormpy.parse_properties_for_prism_program('P=? [ FG "one" ]', program) model = stormpy.build_model(program, formulas) assert model.nr_states == 13 assert model.nr_transitions == 20 @@ -34,7 +34,7 @@ def test_model_checking_prism_dtmc_ltl(self): def test_model_checking_prism_mdp(self): program = stormpy.parse_prism_program(get_example_path("mdp", "coin2-2.nm")) - formulas = stormpy.parse_properties_for_prism_program("Pmin=? [ F \"finished\" & \"all_coins_equal_1\"]", program) + formulas = stormpy.parse_properties_for_prism_program('Pmin=? [ F "finished" & "all_coins_equal_1"]', program) model = stormpy.build_model(program, formulas) assert model.nr_states == 272 assert model.nr_transitions == 492 @@ -46,7 +46,7 @@ def test_model_checking_prism_mdp(self): def test_model_checking_interval_mdp(self): model = stormpy.build_interval_model_from_drn(get_example_path("imdp", "tiny-01.drn")) - formulas = stormpy.parse_properties("Pmax=? [ F \"target\"];Pmin=? [ F \"target\"]") + formulas = stormpy.parse_properties('Pmax=? [ F "target"];Pmin=? [ F "target"]') initial_state = model.initial_states[0] assert initial_state == 0 @@ -75,7 +75,6 @@ def test_model_checking_interval_mdp(self): result = stormpy.check_interval_mdp(model, task, env) assert math.isclose(result.at(initial_state), 0.4, rel_tol=1e-4) - def test_model_checking_jani_dtmc(self): jani_model, formulas = stormpy.parse_jani_model(get_example_path("dtmc", "die.jani")) formulas = stormpy.eliminate_reward_accumulations(jani_model, formulas) @@ -93,7 +92,7 @@ def test_model_checking_jani_dtmc(self): def test_model_checking_dtmc_all_labels(self): program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm")) - formulas = stormpy.parse_properties_for_prism_program("P=? [ F \"one\" ]", program) + formulas = stormpy.parse_properties_for_prism_program('P=? [ F "one" ]', program) model = stormpy.build_model(program) assert model.nr_states == 13 assert model.nr_transitions == 20 @@ -102,13 +101,13 @@ def test_model_checking_dtmc_all_labels(self): assert initial_state == 0 result = stormpy.model_checking(model, formulas[0]) assert math.isclose(result.at(initial_state), 1 / 6) - formulas = stormpy.parse_properties_for_prism_program("P=? [ F \"two\" ]", program) + formulas = stormpy.parse_properties_for_prism_program('P=? [ F "two" ]', program) result = stormpy.model_checking(model, formulas[0]) assert math.isclose(result.at(initial_state), 1 / 6) def test_model_checking_all_dtmc(self): program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm")) - formulas = stormpy.parse_properties_for_prism_program("P=? [ F \"one\" ]", program) + formulas = stormpy.parse_properties_for_prism_program('P=? [ F "one" ]', program) model = stormpy.build_model(program, formulas) assert model.nr_states == 13 assert model.nr_transitions == 20 @@ -119,7 +118,7 @@ def test_model_checking_all_dtmc(self): def test_model_checking_only_initial(self): program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm")) - formulas = stormpy.parse_properties_for_prism_program("Pmax=? [F{\"coin_flips\"}<=3 \"one\"]", program) + formulas = stormpy.parse_properties_for_prism_program('Pmax=? [F{"coin_flips"}<=3 "one"]', program) model = stormpy.build_model(program, formulas) assert len(model.initial_states) == 1 initial_state = model.initial_states[0] @@ -131,7 +130,7 @@ def test_model_checking_only_initial(self): def test_model_checking_prob01(self): program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm")) formulaPhi = stormpy.parse_properties("true")[0] - formulaPsi = stormpy.parse_properties("\"six\"")[0] + formulaPsi = stormpy.parse_properties('"six"')[0] model = stormpy.build_model(program, [formulaPsi]) phiResult = stormpy.model_checking(model, formulaPhi) phiStates = phiResult.get_truth_values() @@ -154,7 +153,7 @@ def test_model_checking_prob01(self): def test_model_checking_ctmc(self): model = stormpy.build_model_from_drn(get_example_path("ctmc", "dft.drn")) - formulas = stormpy.parse_properties("T=? [ F \"failed\" ]") + formulas = stormpy.parse_properties('T=? [ F "failed" ]') assert model.nr_states == 16 assert model.nr_transitions == 33 assert len(model.initial_states) == 1 @@ -165,7 +164,7 @@ def test_model_checking_ctmc(self): def test_filter(self): program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm")) - formulas = stormpy.parse_properties_for_prism_program("P=? [ F \"one\" ]", program) + formulas = stormpy.parse_properties_for_prism_program('P=? [ F "one" ]', program) model = stormpy.build_model(program, formulas) assert model.nr_states == 13 assert model.nr_transitions == 20 @@ -181,7 +180,7 @@ def test_filter(self): def test_model_checking_prism_dd_dtmc(self): program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm")) - formulas = stormpy.parse_properties_for_prism_program("P=? [ F \"one\" ]", program) + formulas = stormpy.parse_properties_for_prism_program('P=? [ F "one" ]', program) model = stormpy.build_symbolic_model(program, formulas) assert model.nr_states == 13 assert model.nr_transitions == 20 @@ -194,7 +193,7 @@ def test_model_checking_prism_dd_dtmc(self): def test_model_checking_prism_hybrid_dtmc(self): program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm")) - formulas = stormpy.parse_properties_for_prism_program("P=? [ F \"one\" ]", program) + formulas = stormpy.parse_properties_for_prism_program('P=? [ F "one" ]', program) model = stormpy.build_symbolic_model(program, formulas) assert model.nr_states == 13 assert model.nr_transitions == 20 @@ -210,8 +209,8 @@ def test_compute_expected_number_of_visits(self): environment = stormpy.Environment() result = stormpy.compute_expected_number_of_visits(environment, model) assert result.at(0) == 1 - assert math.isclose(result.at(1),2.0/3) - + assert math.isclose(result.at(1), 2.0 / 3) + def test_compute_steady_state_distribution(self): program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm")) model = stormpy.build_model(program) @@ -220,7 +219,7 @@ def test_compute_steady_state_distribution(self): values = result.get_values() assert len(values) == 13 sorted(values) - for i in range(7): + for i in range(7): assert values[i] == 0 - for i in range(7,13): - assert math.isclose(values[i], 1.0/6) + for i in range(7, 13): + assert math.isclose(values[i], 1.0 / 6) diff --git a/tests/core/test_multiobjective.py b/tests/core/test_multiobjective.py index 10bfe3f5a..84bc2742c 100644 --- a/tests/core/test_multiobjective.py +++ b/tests/core/test_multiobjective.py @@ -3,20 +3,21 @@ from configurations import plotting, numpy_avail + class TestModelChecking: def naive_api_double_no_plotting_test(self): program = stormpy.parse_prism_program(get_example_path("mdp", "multiobjective1.nm")) - properties = stormpy.parse_properties_for_prism_program("multi(Pmax=? [ F<=3 s=2 ],R{\"rew\"}max=? [ F s=2 ])", program) + properties = stormpy.parse_properties_for_prism_program('multi(Pmax=? [ F<=3 s=2 ],R{"rew"}max=? [ F s=2 ])', program) model = stormpy.build_model(program, properties) - result = stormpy.model_checking(model,properties[0]) - expected_vertices = [[124/125, 248/2125], [97/100, 5456/425 ], [91/100, 248/17]] + result = stormpy.model_checking(model, properties[0]) + expected_vertices = [[124 / 125, 248 / 2125], [97 / 100, 5456 / 425], [91 / 100, 248 / 17]] assert len(result.get_underapproximation().vertices) >= 3 assert len(result.get_overapproximation().vertices) >= 3 # check if each under/over-approximation point is close to one of the expected vertices for p in result.get_underapproximation().vertices: - assert min([ max([ abs(pi-vi) for pi,vi in zip(p, v) ]) for v in expected_vertices]) <= 1e-4 + assert min([max([abs(pi - vi) for pi, vi in zip(p, v)]) for v in expected_vertices]) <= 1e-4 for p in result.get_overapproximation().vertices: - assert min([ max([ abs(pi-vi) for pi,vi in zip(p, v) ]) for v in expected_vertices]) <= 1e-4 + assert min([max([abs(pi - vi) for pi, vi in zip(p, v)]) for v in expected_vertices]) <= 1e-4 @plotting @numpy_avail @@ -25,15 +26,15 @@ def naive_api_double_with_plotting_test(self): from stormpy.utility.multiobjective_plotting import prepare_multiobjective_result_for_plotting, plot_convex_pareto_curve_demo program = stormpy.parse_prism_program(get_example_path("mdp", "multiobjective1.nm")) - properties = stormpy.parse_properties_for_prism_program("multi(Pmax=? [ F<=3 s=2 ],R{\"rew\"}max=? [ F s=2 ])", program) + properties = stormpy.parse_properties_for_prism_program('multi(Pmax=? [ F<=3 s=2 ],R{"rew"}max=? [ F s=2 ])', program) model = stormpy.build_model(program, properties) - result = stormpy.model_checking(model,properties[0]) - lower_left = [0,0] - upper_right = [1,20] + result = stormpy.model_checking(model, properties[0]) + lower_left = [0, 0] + upper_right = [1, 20] formula = properties[0].raw_formula underapprox_points, overapprox_points = prepare_multiobjective_result_for_plotting(result, lower_left, upper_right, formula) fig, ax = plt.subplots() plot_convex_pareto_curve_demo(ax, underapprox_points, overapprox_points, lower_left, upper_right) ax.set_xlabel(formula.subformulas[0]) ax.set_ylabel(formula.subformulas[1]) - #plt.show() + # plt.show() diff --git a/tests/core/test_parse.py b/tests/core/test_parse.py index 42ade3de6..f1a1aef3e 100644 --- a/tests/core/test_parse.py +++ b/tests/core/test_parse.py @@ -29,7 +29,7 @@ def test_parse_jani_model(self): assert description.is_jani_model def test_parse_jani_model_string(self): - with open(get_example_path("dtmc", "die.jani"), 'r') as file: + with open(get_example_path("dtmc", "die.jani"), "r") as file: json_string = file.read() jani_model, properties = stormpy.parse_jani_model_from_string(json_string) assert jani_model.name == "die.jani" @@ -40,14 +40,13 @@ def test_parse_jani_model_string(self): assert description.is_jani_model def test_parse_formula(self): - formula = "P=? [F \"one\"]" + formula = 'P=? [F "one"]' properties = stormpy.parse_properties(formula) assert len(properties) == 1 assert str(properties[0].raw_formula) == formula def test_parse_explicit_dtmc(self): - model = stormpy.build_sparse_model_from_explicit(get_example_path("dtmc", "die.tra"), - get_example_path("dtmc", "die.lab")) + model = stormpy.build_sparse_model_from_explicit(get_example_path("dtmc", "die.tra"), get_example_path("dtmc", "die.lab")) assert model.nr_states == 13 assert model.nr_transitions == 20 assert model.model_type == stormpy.ModelType.DTMC @@ -55,8 +54,7 @@ def test_parse_explicit_dtmc(self): assert type(model) is stormpy.SparseDtmc def test_parse_explicit_mdp(self): - model = stormpy.build_sparse_model_from_explicit(get_example_path("mdp", "two_dice.tra"), - get_example_path("mdp", "two_dice.lab")) + model = stormpy.build_sparse_model_from_explicit(get_example_path("mdp", "two_dice.tra"), get_example_path("mdp", "two_dice.lab")) assert model.nr_states == 169 assert model.nr_transitions == 436 assert model.model_type == stormpy.ModelType.MDP diff --git a/tests/core/test_transformation.py b/tests/core/test_transformation.py index 05dea41ed..c439b3465 100644 --- a/tests/core/test_transformation.py +++ b/tests/core/test_transformation.py @@ -38,7 +38,7 @@ def test_transform_symbolic_parametric_dtmc_to_sparse(self): def test_transform_continuous_to_discrete_time_model_ctmc(self): ctmc = stormpy.build_model_from_drn(get_example_path("ctmc", "dft.drn")) - formulas = stormpy.parse_properties("T=? [ F \"failed\" ]") + formulas = stormpy.parse_properties('T=? [ F "failed" ]') assert ctmc.nr_states == 16 assert ctmc.nr_transitions == 33 assert len(ctmc.initial_states) == 1 @@ -81,7 +81,7 @@ def test_transform_continuous_to_discrete_time_model_ma(self): def test_eliminate_non_markovian_chains(self): program = stormpy.parse_prism_program(get_example_path("ma", "stream2.ma"), False, True) - formulas = stormpy.parse_properties_for_prism_program("Pmin=? [ F \"done\"];Tmin=? [ F \"done\" ]", program) + formulas = stormpy.parse_properties_for_prism_program('Pmin=? [ F "done"];Tmin=? [ F "done" ]', program) ma = stormpy.build_model(program, formulas) assert ma.nr_states == 12 assert ma.nr_transitions == 14 @@ -129,10 +129,11 @@ def test_eliminate_non_markovian_chains(self): result = stormpy.model_checking(ma_elim, ma_formulas_elim[0]) assert math.isclose(result.at(initial_state), 1) + class TestECElimination: def test_elimination_on_two_dice(self): program = stormpy.parse_prism_program(get_example_path("mdp", "two_dice.nm")) - formulas = stormpy.parse_properties_for_prism_program("P=? [ F \"two\" ]", program) + formulas = stormpy.parse_properties_for_prism_program('P=? [ F "two" ]', program) model = stormpy.build_model(program, formulas) subsystem = stormpy.BitVector(model.nr_states, True) possible_ec_rows = stormpy.BitVector(model.nr_choices, True) @@ -144,10 +145,11 @@ def test_elimination_on_two_dice(self): assert ec_elimination_result.new_to_old_row_mapping[200] == 245 assert ec_elimination_result.sink_rows.number_of_set_bits() == 36 + class TestSubsystemCreation: def test_for_ctmc(self): program = stormpy.parse_prism_program(get_example_path("ctmc", "polling2.sm"), True) - formulas = stormpy.parse_properties_for_prism_program("P=? [ F<=3 \"target\" ]", program) + formulas = stormpy.parse_properties_for_prism_program('P=? [ F<=3 "target" ]', program) model = stormpy.build_model(program, formulas) assert model.nr_states == 12 selected_outgoing_transitions = stormpy.BitVector(model.nr_states, True) @@ -161,4 +163,3 @@ def test_for_ctmc(self): assert submodel.nr_states == 8 assert abort_label == "deadl" assert "deadl" in submodel.labeling.get_labels() - diff --git a/tests/dft/test_analysis.py b/tests/dft/test_analysis.py index 586f1425b..134c62ae6 100644 --- a/tests/dft/test_analysis.py +++ b/tests/dft/test_analysis.py @@ -10,7 +10,7 @@ class TestAnalysis: def test_analyze_mttf(self): dft = stormpy.dft.load_dft_json_file(get_example_path("dft", "and.json")) - formulas = stormpy.parse_properties("T=? [ F \"failed\" ]") + formulas = stormpy.parse_properties('T=? [ F "failed" ]') assert dft.nr_elements() == 3 results = stormpy.dft.analyze_dft(dft, [formulas[0].raw_formula]) assert math.isclose(results[0], 3) @@ -37,7 +37,7 @@ def test_explicit_model_builder(self): def test_explicit_model_builder_approximation(self): dft = stormpy.dft.load_dft_galileo_file(get_example_path("dft", "rc.dft")) - properties = stormpy.parse_properties("T=? [ F \"failed\" ]") + properties = stormpy.parse_properties('T=? [ F "failed" ]') prop = properties[0] builder = stormpy.dft.ExplicitDFTModelBuilder_double(dft) @@ -93,7 +93,7 @@ def test_explicit_model_builder_approximation(self): def test_explicit_model_builder_approximation_complete(self): dft = stormpy.dft.load_dft_galileo_file(get_example_path("dft", "rc.dft")) - properties = stormpy.parse_properties("T=? [ F \"failed\" ]") + properties = stormpy.parse_properties('T=? [ F "failed" ]') prop = properties[0] builder = stormpy.dft.ExplicitDFTModelBuilder_double(dft) @@ -123,24 +123,24 @@ def test_explicit_model_builder_approximation_complete(self): def test_relevant_events_property(self): dft = stormpy.dft.load_dft_json_file(get_example_path("dft", "and.json")) - properties = stormpy.parse_properties("P=? [ F<=1 \"A_failed\" ]") + properties = stormpy.parse_properties('P=? [ F<=1 "A_failed" ]') formulas = [p.raw_formula for p in properties] relevant_events = stormpy.dft.compute_relevant_events(formulas) assert relevant_events.is_relevant("A") assert not relevant_events.is_relevant("B") assert not relevant_events.is_relevant("C") - results = stormpy.dft.analyze_dft(dft, formulas, relevant_events = relevant_events) + results = stormpy.dft.analyze_dft(dft, formulas, relevant_events=relevant_events) assert math.isclose(results[0], 0.1548181217) def test_relevant_events_additional(self): dft = stormpy.dft.load_dft_json_file(get_example_path("dft", "and.json")) - properties = stormpy.parse_properties("P=? [ F<=1 \"failed\" ]") + properties = stormpy.parse_properties('P=? [ F<=1 "failed" ]') formulas = [p.raw_formula for p in properties] relevant_events = stormpy.dft.compute_relevant_events(formulas, ["B", "C"]) assert relevant_events.is_relevant("B") assert relevant_events.is_relevant("C") assert not relevant_events.is_relevant("A") - results = stormpy.dft.analyze_dft(dft, formulas, relevant_events = relevant_events) + results = stormpy.dft.analyze_dft(dft, formulas, relevant_events=relevant_events) assert math.isclose(results[0], 0.1548181217) def test_transformation(self): @@ -150,7 +150,7 @@ def test_transformation(self): dft = stormpy.dft.transform_dft(dft, unique_constant_be=True, binary_fdeps=True, exponential_distributions=True) valid, output = stormpy.dft.is_well_formed(dft) assert valid - formulas = stormpy.parse_properties("Tmin=? [ F \"failed\" ]") + formulas = stormpy.parse_properties('Tmin=? [ F "failed" ]') results = stormpy.dft.analyze_dft(dft, [formulas[0].raw_formula]) assert math.isclose(results[0], 6.380930905) @@ -159,6 +159,6 @@ def test_fdep_conflicts(self): dft = stormpy.dft.transform_dft(dft, unique_constant_be=True, binary_fdeps=True, exponential_distributions=True) has_conflicts = stormpy.dft.compute_dependency_conflicts(dft, use_smt=False, solver_timeout=0) assert not has_conflicts - formulas = stormpy.parse_properties("T=? [ F \"failed\" ]") + formulas = stormpy.parse_properties('T=? [ F "failed" ]') results = stormpy.dft.analyze_dft(dft, [formulas[0].raw_formula]) assert math.isclose(results[0], 6.380930905) diff --git a/tests/dft/test_dft.py b/tests/dft/test_dft.py index d95214eed..3eb6323f8 100644 --- a/tests/dft/test_dft.py +++ b/tests/dft/test_dft.py @@ -11,6 +11,7 @@ class TestDft: def test_parametric_dft(self): import pycarl + pycarl.clear_pools() dft = stormpy.dft.load_parametric_dft_galileo_file(get_example_path("dft", "symmetry_param.dft")) assert dft.nr_elements() == 7 @@ -44,6 +45,7 @@ def test_element(self): d = dft.get_element_by_name("D") assert "InvalidArgumentException" in str(exception.value) + @dft class TestDftSymmetries: def test_symmetries_none(self): @@ -73,5 +75,5 @@ def test_symmetries(self): for syms in group: assert len(syms) == 2 for elem in syms: - assert elem == i or elem == i+3 + assert elem == i or elem == i + 3 i += 1 diff --git a/tests/dft/test_dft_simulator.py b/tests/dft/test_dft_simulator.py index 836624ec0..c7df771b8 100644 --- a/tests/dft/test_dft_simulator.py +++ b/tests/dft/test_dft_simulator.py @@ -116,7 +116,7 @@ def test_steps(self): failable = state.failable() for f in failable: - assert False # no failable elements + assert False # no failable elements def test_steps_dependency(self): dft = stormpy.dft.load_dft_galileo_file(get_example_path("dft", "fdep.dft")) diff --git a/tests/dft/test_io.py b/tests/dft/test_io.py index b4ca0af02..24d9325bd 100644 --- a/tests/dft/test_io.py +++ b/tests/dft/test_io.py @@ -27,7 +27,7 @@ def test_load_dft_json_string(self): json_node_a = '{"data": {"id":"0", "name":"A", "type":"be", "rate":"1", "dorm":"1", "label":"A (1)"}, "group":"nodes", "classes":"be"}' json_node_b = '{"data": {"id":"1", "name":"B", "type":"be", "rate":"1", "dorm":"1", "label":"B (1)"}, "group":"nodes", "classes":"be"}' json_node_c = '{"data": {"id":"6", "name":"Z", "type":"pand", "children":["0", "1"], "label":"Z"}, "group":"nodes", "classes":"pand"}' - json_string = '{"toplevel": "6", "parameters": {}, "nodes": [' + json_node_a + ',' + json_node_b + ',' + json_node_c + ']}' + json_string = '{"toplevel": "6", "parameters": {}, "nodes": [' + json_node_a + "," + json_node_b + "," + json_node_c + "]}" # Load dft = stormpy.dft.load_dft_json_string(json_string) assert dft.nr_elements() == 3 @@ -35,6 +35,7 @@ def test_load_dft_json_string(self): assert dft.nr_dynamic() == 1 assert not dft.can_have_nondeterminism() + @dft class TestDftExport: def test_export_dft_json_string(self): diff --git a/tests/dft/test_module.py b/tests/dft/test_module.py index f3ff475d8..a16cbfa51 100644 --- a/tests/dft/test_module.py +++ b/tests/dft/test_module.py @@ -13,7 +13,7 @@ def test_module(self): assert dft.nr_elements() == 23 assert dft.nr_be() == 13 assert dft.nr_dynamic() == 2 - module = dft.modules(); + module = dft.modules() assert dft.get_element(module.representative()).name == "n0" assert len(module.elements()) == 1 assert len(module.submodules()) == 4 @@ -25,10 +25,10 @@ def test_module(self): def test_module_json(self): dft = stormpy.dft.load_dft_galileo_file(get_example_path("dft", "hecs.dft")) json = stormpy.dft.modules_json(dft) - assert json['representative']['name'] == "n0" - assert len(json['elements']) == 1 - assert len(json['submodules']) == 4 + assert json["representative"]["name"] == "n0" + assert len(json["elements"]) == 1 + assert len(json["submodules"]) == 4 for submodule in json["submodules"]: - assert submodule['representative']['name'] in ["n116", "n137", "n120", "n21"] - assert len(submodule['elements']) in [1, 7] - assert len(submodule['submodules']) in [0, 2, 3, 7] + assert submodule["representative"]["name"] in ["n116", "n137", "n120", "n21"] + assert len(submodule["elements"]) in [1, 7] + assert len(submodule["submodules"]) in [0, 2, 3, 7] diff --git a/tests/dft/test_transformations.py b/tests/dft/test_transformations.py index e839858a8..4969fbe31 100644 --- a/tests/dft/test_transformations.py +++ b/tests/dft/test_transformations.py @@ -26,4 +26,3 @@ def test_instantiate_dft(self): assert str(elem) == "{C} BE(exp 5, 0.05)" elem = inst_dft.get_element_by_name("D") assert str(elem) == "{D} BE(exp 0.01, 0)" - diff --git a/tests/gspn/test_gspn_io.py b/tests/gspn/test_gspn_io.py index 049a2dfa2..85df29d20 100644 --- a/tests/gspn/test_gspn_io.py +++ b/tests/gspn/test_gspn_io.py @@ -23,7 +23,7 @@ def test_custom_property(self): jani_program = jani_builder.build() # Set properties - properties = stormpy.parse_properties_for_jani_model('P=? [F<=10 eating1=1]', jani_program) + properties = stormpy.parse_properties_for_jani_model("P=? [F<=10 eating1=1]", jani_program) # Build model model = stormpy.build_model(jani_program, properties) @@ -56,7 +56,7 @@ def test_standard_properties(self): # Build model # Leads to incorrect result - #model = stormpy.build_model(jani_program, properties) + # model = stormpy.build_model(jani_program, properties) model = stormpy.build_model(jani_program) # Model checking diff --git a/tests/info/test_info.py b/tests/info/test_info.py index d715ad285..2f8eb0dfe 100644 --- a/tests/info/test_info.py +++ b/tests/info/test_info.py @@ -10,5 +10,4 @@ def test_version(self): def test_version_equal(self): assert stormpy.info.storm_version() in stormpy.info.Version.short - assert (stormpy.info.Version.development and stormpy.info.Version.short.endswith( - " (dev)")) or not stormpy.info.Version.development + assert (stormpy.info.Version.development and stormpy.info.Version.short.endswith(" (dev)")) or not stormpy.info.Version.development diff --git a/tests/logic/test_formulas.py b/tests/logic/test_formulas.py index bf9bfb5d8..51cee543d 100644 --- a/tests/logic/test_formulas.py +++ b/tests/logic/test_formulas.py @@ -4,7 +4,7 @@ class TestFormulas: def test_probability_formula(self): - formula_str = "P=? [F \"one\"]" + formula_str = 'P=? [F "one"]' properties = stormpy.parse_properties(formula_str) formula = properties[0].raw_formula assert type(formula) == stormpy.logic.ProbabilityOperator @@ -12,16 +12,16 @@ def test_probability_formula(self): assert str(formula) == formula_str def test_reward_formula(self): - formula_str = "R=? [F \"one\"]" + formula_str = 'R=? [F "one"]' properties = stormpy.parse_properties(formula_str) formula = properties[0].raw_formula assert type(formula) == stormpy.logic.RewardOperator assert len(properties) == 1 - assert str(formula) == "R=? [F \"one\"]" + assert str(formula) == 'R=? [F "one"]' def test_formula_list(self): formulas = [] - prop = "=? [F \"one\"]" + prop = '=? [F "one"]' forms = stormpy.parse_properties("P" + prop) formulas.append(forms[0].raw_formula) forms = stormpy.parse_properties("R" + prop) @@ -41,17 +41,17 @@ def test_jani_formula(self): assert prop.name == "Expected number of coin flips" def test_bounds(self): - prop = "P=? [F \"one\"]" + prop = 'P=? [F "one"]' formula = stormpy.parse_properties(prop)[0].raw_formula assert not formula.has_bound - prop = "P<0.4 [F \"one\"]" + prop = 'P<0.4 [F "one"]' formula = stormpy.parse_properties(prop)[0].raw_formula assert formula.has_bound assert formula.threshold == stormpy.Rational("0.4") assert formula.comparison_type == stormpy.logic.ComparisonType.LESS def test_set_bounds(self): - prop = "P<0.4 [F \"one\"]" + prop = 'P<0.4 [F "one"]' formula = stormpy.parse_properties(prop)[0].raw_formula expression_manager = stormpy.ExpressionManager() rational = stormpy.Rational("0.2") @@ -59,10 +59,10 @@ def test_set_bounds(self): formula.set_bound(stormpy.logic.ComparisonType.GEQ, expression) assert formula.threshold == stormpy.Rational("0.2") assert formula.comparison_type == stormpy.logic.ComparisonType.GEQ - assert str(formula) == "P>=1/5 [F \"one\"]" + assert str(formula) == 'P>=1/5 [F "one"]' def test_subformula(self): - prop = "P=? [F \"one\"]" + prop = 'P=? [F "one"]' formula = stormpy.parse_properties(prop)[0].raw_formula assert type(formula) == stormpy.logic.ProbabilityOperator pathform = formula.subformula @@ -73,7 +73,7 @@ def test_subformula(self): assert prop.raw_formula == labelform def test_game_formula(self): - formula_str = "<<0>> Pmax=? [F \"goal\"]" + formula_str = '<<0>> Pmax=? [F "goal"]' properties = stormpy.parse_properties(formula_str) formula = properties[0].raw_formula assert type(formula) == stormpy.logic.GameFormula @@ -81,4 +81,4 @@ def test_game_formula(self): assert len(properties) == 1 formula = formula.subformula assert type(formula) == stormpy.logic.ProbabilityOperator - assert str(formula) == "Pmax=? [F \"goal\"]" + assert str(formula) == 'Pmax=? [F "goal"]' diff --git a/tests/pars/test_model_instantiator.py b/tests/pars/test_model_instantiator.py index bd2656bea..87736655f 100644 --- a/tests/pars/test_model_instantiator.py +++ b/tests/pars/test_model_instantiator.py @@ -27,7 +27,7 @@ def test_instantiate_dtmc(self): def test_sample_pdtmc(self): program = stormpy.parse_prism_program(get_example_path("pdtmc", "brp16_2.pm")) - formulas = stormpy.parse_properties_for_prism_program("P=? [F \"error\"]", program) + formulas = stormpy.parse_properties_for_prism_program('P=? [F "error"]', program) model = stormpy.build_parametric_model(program, formulas) parameters = model.collect_probability_parameters() @@ -45,7 +45,7 @@ def test_sample_pdtmc(self): def test_pdtmc_instantiation_checker(self): program = stormpy.parse_prism_program(get_example_path("pdtmc", "herman5.pm")) - formulas = stormpy.parse_properties_for_prism_program("R=? [F \"stable\"]", program) + formulas = stormpy.parse_properties_for_prism_program('R=? [F "stable"]', program) model = stormpy.build_parametric_model(program, formulas) parameters = model.collect_probability_parameters() @@ -63,7 +63,7 @@ def test_pdtmc_instantiation_checker(self): def test_pdtmc_exact_instantiation_checker(self): program = stormpy.parse_prism_program(get_example_path("pdtmc", "herman5.pm")) - formulas = stormpy.parse_properties_for_prism_program("R=? [F \"stable\"]", program) + formulas = stormpy.parse_properties_for_prism_program('R=? [F "stable"]', program) model = stormpy.build_parametric_model(program, formulas) parameters = model.collect_probability_parameters() diff --git a/tests/pars/test_parametric.py b/tests/pars/test_parametric.py index f7460e12d..824cca484 100644 --- a/tests/pars/test_parametric.py +++ b/tests/pars/test_parametric.py @@ -61,7 +61,7 @@ def test_parameters(self): assert len(all_parameters) == 2 program_reward = stormpy.parse_prism_program(get_example_path("pdtmc", "brp_rewards16_2.pm")) - formulas_reward = stormpy.parse_properties_for_prism_program("Rmin=? [ F \"target\" ]", program_reward) + formulas_reward = stormpy.parse_properties_for_prism_program('Rmin=? [ F "target" ]', program_reward) model = stormpy.build_parametric_model(program_reward, formulas_reward) model_parameters = model.collect_probability_parameters() reward_parameters = model.collect_reward_parameters() @@ -78,6 +78,7 @@ def test_parameters(self): def test_constraints_collector(self): from pycarl.formula import FormulaType, Relation + if stormpy.info.storm_ratfunc_use_cln(): import pycarl.cln.formula else: @@ -126,7 +127,7 @@ def test_dtmc_simplification(self): def test_mdp_simplification(self): program = stormpy.parse_prism_program(get_example_path("pmdp", "two_dice.nm")) - formulas = stormpy.parse_properties_for_prism_program("Pmin=? [ F \"two\" ]", program) + formulas = stormpy.parse_properties_for_prism_program('Pmin=? [ F "two" ]', program) formula = formulas[0].raw_formula model = stormpy.build_parametric_model(program, formulas) assert model.nr_states == 169 diff --git a/tests/pars/test_parametric_model.py b/tests/pars/test_parametric_model.py index c9ba6c3c7..64bc5b6f8 100644 --- a/tests/pars/test_parametric_model.py +++ b/tests/pars/test_parametric_model.py @@ -20,7 +20,7 @@ def test_build_parametric_dtmc(self): def test_build_parametric_dtmc_preprocess(self): program = stormpy.parse_prism_program(get_example_path("pdtmc", "herman5.pm")) - formulas = stormpy.parse_properties_for_prism_program("R=? [ F \"stable\" ]", program) + formulas = stormpy.parse_properties_for_prism_program('R=? [ F "stable" ]', program) trans_program, trans_formulas = stormpy.preprocess_symbolic_input(program, formulas, "") trans_prism = trans_program.as_prism_program() model = stormpy.build_parametric_model(trans_prism, trans_formulas) @@ -33,7 +33,7 @@ def test_build_parametric_dtmc_preprocess(self): def test_build_dtmc_supporting_parameters(self): program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm")) - formulas = stormpy.parse_properties_for_prism_program("P=? [ F \"one\" ]", program) + formulas = stormpy.parse_properties_for_prism_program('P=? [ F "one" ]', program) model = stormpy.build_parametric_model(program, formulas) assert model.nr_states == 13 assert model.nr_transitions == 20 @@ -44,7 +44,7 @@ def test_build_dtmc_supporting_parameters(self): def test_build_parametric_mdp(self): program = stormpy.parse_prism_program(get_example_path("pmdp", "two_dice.nm")) - formulas = stormpy.parse_properties_for_prism_program("P=? [ F \"two\" ]", program) + formulas = stormpy.parse_properties_for_prism_program('P=? [ F "two" ]', program) model = stormpy.build_parametric_model(program, formulas) assert model.nr_states == 169 assert model.nr_transitions == 435 @@ -68,7 +68,7 @@ def test_build_parametric_dtmc(self): def test_build_parametric_dtmc_preprocess(self): program = stormpy.parse_prism_program(get_example_path("pdtmc", "herman5.pm")) - formulas = stormpy.parse_properties_for_prism_program("R=? [ F \"stable\" ]", program) + formulas = stormpy.parse_properties_for_prism_program('R=? [ F "stable" ]', program) trans_program, trans_formulas = stormpy.preprocess_symbolic_input(program, formulas, "") trans_prism = trans_program.as_prism_program() model = stormpy.build_symbolic_parametric_model(trans_prism, trans_formulas) @@ -81,7 +81,7 @@ def test_build_parametric_dtmc_preprocess(self): def test_build_dtmc_supporting_parameters(self): program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm")) - formulas = stormpy.parse_properties_for_prism_program("P=? [ F \"one\" ]", program) + formulas = stormpy.parse_properties_for_prism_program('P=? [ F "one" ]', program) model = stormpy.build_symbolic_parametric_model(program, formulas) assert model.nr_states == 13 assert model.nr_transitions == 20 @@ -92,7 +92,7 @@ def test_build_dtmc_supporting_parameters(self): def test_build_parametric_mdp(self): program = stormpy.parse_prism_program(get_example_path("pmdp", "two_dice.nm")) - formulas = stormpy.parse_properties_for_prism_program("P=? [ F \"two\" ]", program) + formulas = stormpy.parse_properties_for_prism_program('P=? [ F "two" ]', program) model = stormpy.build_symbolic_parametric_model(program, formulas) assert model.nr_states == 169 assert model.nr_transitions == 435 diff --git a/tests/pomdp/test_pomdp_quantitative_analysis.py b/tests/pomdp/test_pomdp_quantitative_analysis.py index d0717f08b..9116aa4e5 100644 --- a/tests/pomdp/test_pomdp_quantitative_analysis.py +++ b/tests/pomdp/test_pomdp_quantitative_analysis.py @@ -6,11 +6,12 @@ import math + @pomdp class TestPomdpQuantitative: def test_underapprox_mc_maze_pmax(self): program = stormpy.parse_prism_program(get_example_path("pomdp", "maze_2.prism")) - formulas = stormpy.parse_properties_for_prism_program("Pmax=? [ !\"bad\" U \"goal\" ]", program) + formulas = stormpy.parse_properties_for_prism_program('Pmax=? [ !"bad" U "goal" ]', program) model = stormpy.build_model(program, formulas) model = stormpy.pomdp.make_canonic(model) options = stormpy.pomdp.BeliefExplorationModelCheckerOptionsDouble(False, True) @@ -27,7 +28,7 @@ def test_underapprox_mc_maze_pmax(self): def test_underapprox_mc_maze_rmin(self): program = stormpy.parse_prism_program(get_example_path("pomdp", "maze_2.prism")) - formulas = stormpy.parse_properties_for_prism_program("Rmin=? [ F \"goal\" ]", program) + formulas = stormpy.parse_properties_for_prism_program('Rmin=? [ F "goal" ]', program) model = stormpy.build_model(program, formulas) model = stormpy.pomdp.make_canonic(model) options = stormpy.pomdp.BeliefExplorationModelCheckerOptionsDouble(False, True) @@ -44,7 +45,7 @@ def test_underapprox_mc_maze_rmin(self): def test_underapprox_mc_cmaze_rmin(self): program = stormpy.parse_prism_program(get_example_path("pomdp", "maze-concise.prism")) - formulas = stormpy.parse_properties_for_prism_program("R{\"steps\"}min=? [F ((x = 2) & (y = 0))]", program) + formulas = stormpy.parse_properties_for_prism_program('R{"steps"}min=? [F ((x = 2) & (y = 0))]', program) model = stormpy.build_model(program, formulas) model = stormpy.pomdp.make_canonic(model) options = stormpy.pomdp.BeliefExplorationModelCheckerOptionsDouble(False, True) @@ -57,4 +58,4 @@ def test_underapprox_mc_cmaze_rmin(self): assert math.isclose(result.upper_bound, 19.781437, abs_tol=10**-6) assert result.induced_mc_from_scheduler.nr_states == 9 assert result.induced_mc_from_scheduler.nr_transitions == 15 - assert len(result.cutoff_schedulers) == 3 \ No newline at end of file + assert len(result.cutoff_schedulers) == 3 diff --git a/tests/simulator/test_simulator.py b/tests/simulator/test_simulator.py index cad9586b4..2eb7b9bcc 100644 --- a/tests/simulator/test_simulator.py +++ b/tests/simulator/test_simulator.py @@ -21,6 +21,7 @@ class TestSparseSimulator: final_outcomes[observation] += 1 simulator.restart() + class TestPrismSimulator: def test_negative_values(self): @@ -30,6 +31,5 @@ def test_negative_values(self): simulator = stormpy.simulator.create_simulator(prism_program, seed=42) simulator.set_action_mode(stormpy.simulator.SimulatorActionMode.GLOBAL_NAMES) state, rew, labels = simulator.restart() - assert state["s"] == -1 + assert state["s"] == -1 assert int(state["s"]) == -1 - diff --git a/tests/storage/test_labeling.py b/tests/storage/test_labeling.py index 9fa89852a..23c23de2e 100644 --- a/tests/storage/test_labeling.py +++ b/tests/storage/test_labeling.py @@ -21,7 +21,7 @@ def test_set_labeling(self): def test_label(self): program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm")) - formulas = stormpy.parse_properties_for_prism_program("P=? [ F \"one\" ]", program) + formulas = stormpy.parse_properties_for_prism_program('P=? [ F "one" ]', program) model = stormpy.build_model(program, formulas) labeling = model.labeling labels = labeling.get_labels() @@ -48,6 +48,7 @@ def test_label_parametric(self): assert len(initial_states) == 1 assert 0 in initial_states + class TestChoiceLabeling: def test_label(self): program = stormpy.parse_prism_program(get_example_path("dtmc", "brp-16-2.pm")) diff --git a/tests/storage/test_matrix.py b/tests/storage/test_matrix.py index 02de8971b..5e3f60aae 100644 --- a/tests/storage/test_matrix.py +++ b/tests/storage/test_matrix.py @@ -6,8 +6,7 @@ class TestMatrix: def test_matrix(self): - model = stormpy.build_sparse_model_from_explicit(get_example_path("dtmc", "die.tra"), - get_example_path("dtmc", "die.lab")) + model = stormpy.build_sparse_model_from_explicit(get_example_path("dtmc", "die.tra"), get_example_path("dtmc", "die.lab")) matrix = model.transition_matrix assert type(matrix) is stormpy.storage.SparseMatrix assert matrix.nr_rows == model.nr_states @@ -18,8 +17,7 @@ def test_matrix(self): assert e.value() == 0.5 or e.value() == 0 or (e.value() == 1 and e.column > 6) def test_backward_matrix(self): - model = stormpy.build_sparse_model_from_explicit(get_example_path("dtmc", "die.tra"), - get_example_path("dtmc", "die.lab")) + model = stormpy.build_sparse_model_from_explicit(get_example_path("dtmc", "die.tra"), get_example_path("dtmc", "die.lab")) matrix = model.backward_transition_matrix assert type(matrix) is stormpy.storage.SparseMatrix assert matrix.nr_rows == model.nr_states @@ -30,8 +28,7 @@ def test_backward_matrix(self): assert e.value() == 0.5 or e.value() == 0 or (e.value() == 1 and e.column > 6) def test_matrix_row_groups(self): - model = stormpy.build_sparse_model_from_explicit(get_example_path("mdp", "two_dice.tra"), - get_example_path("mdp", "two_dice.lab")) + model = stormpy.build_sparse_model_from_explicit(get_example_path("mdp", "two_dice.tra"), get_example_path("mdp", "two_dice.lab")) matrix = model.transition_matrix assert type(matrix) is stormpy.storage.SparseMatrix assert matrix.nr_rows == 254 @@ -40,11 +37,11 @@ def test_matrix_row_groups(self): assert matrix.nr_entries == model.nr_transitions i = 0 for x in range(0, 8): - for group in range(x*12, x*12+7): + for group in range(x * 12, x * 12 + 7): for row in matrix.get_rows_for_group(group): assert row == i i += 1 - for group in range(x*12+7, x*12+12): + for group in range(x * 12 + 7, x * 12 + 12): for row in matrix.get_rows_for_group(group): assert row == i i += 1 @@ -52,8 +49,7 @@ def test_matrix_row_groups(self): assert e.value() == 0.5 or e.value() == 0 or (e.value() == 1 and e.column > 6) def test_change_matrix(self): - model = stormpy.build_sparse_model_from_explicit(get_example_path("dtmc", "die.tra"), - get_example_path("dtmc", "die.lab")) + model = stormpy.build_sparse_model_from_explicit(get_example_path("dtmc", "die.tra"), get_example_path("dtmc", "die.lab")) matrix = model.transition_matrix for e in matrix: assert e.value() == 0.5 or e.value() == 0 or e.value() == 1 @@ -67,14 +63,13 @@ def test_change_matrix(self): i += 0.1 def test_change_matrix_modelchecking(self): - model = stormpy.build_sparse_model_from_explicit(get_example_path("dtmc", "die.tra"), - get_example_path("dtmc", "die.lab")) + model = stormpy.build_sparse_model_from_explicit(get_example_path("dtmc", "die.tra"), get_example_path("dtmc", "die.lab")) matrix = model.transition_matrix # Check matrix for e in matrix: assert e.value() == 0.5 or e.value() == 0 or e.value() == 1 # First model checking - formulas = stormpy.parse_properties("P=? [ F \"one\" ]") + formulas = stormpy.parse_properties('P=? [ F "one" ]') result = stormpy.model_checking(model, formulas[0]) resValue = result.at(model.initial_states[0]) assert math.isclose(resValue, 0.16666666666666663) @@ -141,8 +136,7 @@ def test_change_parametric_matrix_modelchecking(self): assert len(ratFunc.gather_variables()) == 0 def test_submatrix(self): - model = stormpy.build_sparse_model_from_explicit(get_example_path("dtmc", "die.tra"), - get_example_path("dtmc", "die.lab")) + model = stormpy.build_sparse_model_from_explicit(get_example_path("dtmc", "die.tra"), get_example_path("dtmc", "die.lab")) matrix = model.transition_matrix assert matrix.nr_rows == 13 assert matrix.nr_columns == 13 diff --git a/tests/storage/test_matrix_builder.py b/tests/storage/test_matrix_builder.py index 54650e891..fe6923bee 100644 --- a/tests/storage/test_matrix_builder.py +++ b/tests/storage/test_matrix_builder.py @@ -63,7 +63,11 @@ def test_exact_matrix_builder(self): assert matrix_5x5.nr_entries == 7 for e in matrix_5x5: - assert (e.value() == stormpy.Rational(1) and e.column < 2) or (e.value() == stormpy.Rational(2) and e.column == 2) or (e.column > 2 and e.value() == stormpy.Rational("1/6")) + assert ( + (e.value() == stormpy.Rational(1) and e.column < 2) + or (e.value() == stormpy.Rational(2) and e.column == 2) + or (e.column > 2 and e.value() == stormpy.Rational("1/6")) + ) def test_parametric_matrix_builder(self): builder = stormpy.ParametricSparseMatrixBuilder(force_dimensions=True) @@ -127,8 +131,12 @@ def test_matrix_replace_columns(self): # Check if columns where replaced for e in matrix: - assert (e.value() == 0 and e.column == 0) or (e.value() == 3 and e.column == 1) or ( - e.value() == 2 and e.column == 2) or (e.value() == 1 and e.column == 3) + assert ( + (e.value() == 0 and e.column == 0) + or (e.value() == 3 and e.column == 1) + or (e.value() == 2 and e.column == 2) + or (e.value() == 1 and e.column == 3) + ) def test_parametric_matrix_replace_columns(self): builder = stormpy.ParametricSparseMatrixBuilder(3, 4, force_dimensions=False) @@ -161,8 +169,7 @@ def test_parametric_matrix_replace_columns(self): # Check if columns where replaced for e in matrix: - assert (e.value() == first_val and e.column == 1) or (e.value() == third_val and e.column == 2) or ( - e.value() == sec_val and e.column == 3) + assert (e.value() == first_val and e.column == 1) or (e.value() == third_val and e.column == 2) or (e.value() == sec_val and e.column == 3) def test_matrix_builder_row_grouping(self): num_rows = 5 @@ -201,10 +208,8 @@ def test_parametric_matrix_builder_row_grouping(self): @numpy_avail def test_matrix_from_numpy(self): import numpy as np - array = np.array([[0, 2], - [3, 4], - [0.1, 24], - [-0.3, -4]], dtype='float64') + + array = np.array([[0, 2], [3, 4], [0.1, 24], [-0.3, -4]], dtype="float64") matrix = stormpy.build_sparse_matrix(array) @@ -222,10 +227,8 @@ def test_matrix_from_numpy(self): @numpy_avail def test_matrix_from_numpy_zeros(self): import numpy as np - array = np.array([[0, 0, 1, 0], - [0.1, 0, 0, 0.9], - [0, 0, 0, 0], - [1, 0, 0, 0]], dtype='float64') + + array = np.array([[0, 0, 1, 0], [0.1, 0, 0, 0.9], [0, 0, 0, 0], [1, 0, 0, 0]], dtype="float64") matrix = stormpy.build_sparse_matrix(array) @@ -243,6 +246,7 @@ def test_matrix_from_numpy_zeros(self): @numpy_avail def test_parametric_matrix_from_numpy(self): import numpy as np + zero = stormpy.RationalRF(0) one_pol = stormpy.RationalRF(1) one_pol = stormpy.FactorizedPolynomial(one_pol) @@ -252,10 +256,7 @@ def test_parametric_matrix_from_numpy(self): sec_val = stormpy.FactorizedRationalFunction(two_pol, two_pol) third_val = stormpy.FactorizedRationalFunction(one_pol, two_pol) - array = np.array([[sec_val, first_val], - [first_val, zero], - [0, sec_val], - [third_val, third_val]]) + array = np.array([[sec_val, first_val], [first_val, zero], [0, sec_val], [third_val, third_val]]) matrix = stormpy.build_parametric_sparse_matrix(array) @@ -273,10 +274,8 @@ def test_parametric_matrix_from_numpy(self): @numpy_avail def test_matrix_from_numpy_row_grouping(self): import numpy as np - array = np.array([[0, 2], - [3, 4], - [0.1, 24], - [-0.3, -4]], dtype='float64') + + array = np.array([[0, 2], [3, 4], [0.1, 24], [-0.3, -4]], dtype="float64") matrix = stormpy.build_sparse_matrix(array, row_group_indices=[1, 3]) @@ -301,6 +300,7 @@ def test_matrix_from_numpy_row_grouping(self): @numpy_avail def test_parametric_matrix_from_numpy_row_grouping(self): import numpy as np + one_pol = stormpy.RationalRF(1) one_pol = stormpy.FactorizedPolynomial(one_pol) first_val = stormpy.FactorizedRationalFunction(one_pol, one_pol) @@ -309,10 +309,7 @@ def test_parametric_matrix_from_numpy_row_grouping(self): sec_val = stormpy.FactorizedRationalFunction(two_pol, two_pol) third_val = stormpy.FactorizedRationalFunction(one_pol, two_pol) - array = np.array([[sec_val, first_val], - [first_val, sec_val], - [sec_val, sec_val], - [third_val, third_val]]) + array = np.array([[sec_val, first_val], [first_val, sec_val], [sec_val, sec_val], [third_val, third_val]]) matrix = stormpy.build_parametric_sparse_matrix(array, row_group_indices=[1, 3]) diff --git a/tests/storage/test_model.py b/tests/storage/test_model.py index 015b70154..9b955aa8a 100644 --- a/tests/storage/test_model.py +++ b/tests/storage/test_model.py @@ -15,7 +15,7 @@ def test_build_dtmc_from_prism_program(self): def test_build_dtmc_from_prism_program_formulas(self): program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm")) - prop = "P=? [F \"one\"]" + prop = 'P=? [F "one"]' properties = stormpy.parse_properties_for_prism_program(prop, program, None) model = stormpy.build_model(program, properties) assert model.nr_states == 13 @@ -27,7 +27,7 @@ def test_build_dtmc_from_prism_program_formulas(self): def test_build_dtmc_from_prism_program_reward_formulas(self): program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm")) - prop = "R=? [F \"done\"]" + prop = 'R=? [F "done"]' properties = stormpy.parse_properties_for_prism_program(prop, program, None) model = stormpy.build_model(program, properties) assert model.nr_states == 13 @@ -44,7 +44,7 @@ def test_build_dtmc_from_prism_program_reward_formulas(self): def test_reduce_to_state_based_rewards(self): program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm")) - prop = "R=? [F \"done\"]" + prop = 'R=? [F "done"]' properties = stormpy.parse_properties_for_prism_program(prop, program, None) model = stormpy.build_model(program, properties) model.reduce_to_state_based_rewards() @@ -101,7 +101,7 @@ def test_build_instantiated_dtmc_jani(self): def test_build_mdp(self): program = stormpy.parse_prism_program(get_example_path("mdp", "two_dice.nm")) - formulas = stormpy.parse_properties_for_prism_program("P=? [ F \"two\" ]", program) + formulas = stormpy.parse_properties_for_prism_program('P=? [ F "two" ]', program) model = stormpy.build_model(program, formulas) assert model.nr_states == 169 assert model.nr_transitions == 435 @@ -111,7 +111,7 @@ def test_build_mdp(self): def test_build_ctmc(self): program = stormpy.parse_prism_program(get_example_path("ctmc", "polling2.sm"), True) - formulas = stormpy.parse_properties_for_prism_program("P=? [ F<=3 \"target\" ]", program) + formulas = stormpy.parse_properties_for_prism_program('P=? [ F<=3 "target" ]', program) model = stormpy.build_model(program) assert model.nr_states == 12 assert model.nr_transitions == 22 @@ -127,7 +127,7 @@ def test_build_ctmc(self): def test_build_pomdp(self): program = stormpy.parse_prism_program(get_example_path("pomdp", "maze_2.prism")) - formulas = stormpy.parse_properties_for_prism_program("P=? [F \"goal\"]", program) + formulas = stormpy.parse_properties_for_prism_program('P=? [F "goal"]', program) model = stormpy.build_model(program, formulas) assert model.nr_states == 15 assert model.nr_observations == 8 @@ -160,7 +160,7 @@ def test_convert_ma_to_ctmc(self): def test_initial_states(self): program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm")) - formulas = stormpy.parse_properties_for_prism_program("P=? [ F \"one\" ]", program) + formulas = stormpy.parse_properties_for_prism_program('P=? [ F "one" ]', program) model = stormpy.build_model(program, formulas) initial_states = model.initial_states assert len(initial_states) == 1 @@ -175,6 +175,7 @@ def test_choice_origins(self): model = stormpy.build_sparse_model_with_options(program, options) a = model.choice_origins.get_edge_index_set(3) + class TestSymbolicSylvanModel: def test_build_dtmc_from_prism_program(self): program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm")) @@ -187,7 +188,7 @@ def test_build_dtmc_from_prism_program(self): def test_build_dtmc_from_prism_program_formulas(self): program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm")) - prop = "P=? [F \"one\"]" + prop = 'P=? [F "one"]' properties = stormpy.parse_properties_for_prism_program(prop, program, None) model = stormpy.build_symbolic_model(program, properties) assert model.nr_states == 13 @@ -199,7 +200,7 @@ def test_build_dtmc_from_prism_program_formulas(self): def test_build_dtmc_from_prism_program_reward_formulas(self): program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm")) - prop = "R=? [F \"done\"]" + prop = 'R=? [F "done"]' properties = stormpy.parse_properties_for_prism_program(prop, program, None) model = stormpy.build_symbolic_model(program, properties) assert model.nr_states == 13 @@ -214,7 +215,7 @@ def test_build_dtmc_from_prism_program_reward_formulas(self): def test_reduce_to_state_based_rewards(self): program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm")) - prop = "R=? [F \"done\"]" + prop = 'R=? [F "done"]' properties = stormpy.parse_properties_for_prism_program(prop, program, None) model = stormpy.build_symbolic_model(program, properties) model.reduce_to_state_based_rewards() @@ -237,7 +238,7 @@ def test_build_dtmc_from_jani_model(self): def test_build_mdp(self): program = stormpy.parse_prism_program(get_example_path("mdp", "two_dice.nm")) - formulas = stormpy.parse_properties_for_prism_program("P=? [ F \"two\" ]", program) + formulas = stormpy.parse_properties_for_prism_program('P=? [ F "two" ]', program) model = stormpy.build_symbolic_model(program, formulas) assert model.nr_states == 169 assert model.nr_transitions == 435 @@ -247,7 +248,7 @@ def test_build_mdp(self): def test_build_ctmc(self): program = stormpy.parse_prism_program(get_example_path("ctmc", "polling2.sm"), True) - formulas = stormpy.parse_properties_for_prism_program("P=? [ F<=3 \"target\" ]", program) + formulas = stormpy.parse_properties_for_prism_program('P=? [ F<=3 "target" ]', program) model = stormpy.build_symbolic_model(program, formulas) assert model.nr_states == 12 assert model.nr_transitions == 21 diff --git a/tests/storage/test_model_components.py b/tests/storage/test_model_components.py index d8d537a09..5cfe2353f 100644 --- a/tests/storage/test_model_components.py +++ b/tests/storage/test_model_components.py @@ -20,8 +20,7 @@ def test_build_dtmc(self): nr_choices = 13 # transition_matrix - builder = stormpy.SparseMatrixBuilder(rows=0, columns=0, entries=0, force_dimensions=False, - has_custom_row_grouping=False, row_groups=0) + builder = stormpy.SparseMatrixBuilder(rows=0, columns=0, entries=0, force_dimensions=False, has_custom_row_grouping=False, row_groups=0) # Add transitions builder.add_next_value(0, 1, 0.5) @@ -45,30 +44,30 @@ def test_build_dtmc(self): # state labeling state_labeling = stormpy.storage.StateLabeling(nr_states) - state_labels = {'init', 'one', 'two', 'three', 'four', 'five', 'six', 'done', 'deadlock'} + state_labels = {"init", "one", "two", "three", "four", "five", "six", "done", "deadlock"} for label in state_labels: state_labeling.add_label(label) # Add label to one state - state_labeling.add_label_to_state('init', 0) - 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("init", 0) + 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.set_states('done', stormpy.BitVector(nr_states, [7, 8, 9, 10, 11, 12])) + state_labeling.set_states("done", stormpy.BitVector(nr_states, [7, 8, 9, 10, 11, 12])) # 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) + reward_models["coin_flips"] = stormpy.SparseRewardModel(optional_state_action_reward_vector=action_reward) # state valuations manager = stormpy.ExpressionManager() - var_s = manager.create_integer_variable(name='s') - var_d = manager.create_integer_variable(name='d') + var_s = manager.create_integer_variable(name="s") + var_d = manager.create_integer_variable(name="d") v_builder = stormpy.StateValuationsBuilder() v_builder.add_variable(var_s) @@ -88,12 +87,10 @@ def test_build_dtmc(self): for i in range(1, 8): # 0: no origin id_to_command_set_mapping[i].insert(i - 1) id_to_command_set_mapping[8].insert(7) - choice_origins = stormpy.PrismChoiceOrigins(prism_program, index_to_identifier_mapping, - id_to_command_set_mapping) + choice_origins = stormpy.PrismChoiceOrigins(prism_program, index_to_identifier_mapping, id_to_command_set_mapping) # Construct components - 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) components.choice_origins = choice_origins components.state_valuations = state_valuations @@ -114,7 +111,7 @@ def test_build_dtmc(self): assert len(state.actions) <= 1 # Test state labeling - assert dtmc.labeling.get_labels() == {'init', 'deadlock', 'done', 'one', 'two', 'three', 'four', 'five', 'six'} + assert dtmc.labeling.get_labels() == {"init", "deadlock", "done", "one", "two", "three", "four", "five", "six"} # Test reward_models assert len(dtmc.reward_models) == 1 @@ -148,8 +145,7 @@ def test_build_mdp(self): nr_choices = 14 # Build transition matrix - 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) # Row group, state 0 builder.new_row_group(0) @@ -190,37 +186,37 @@ def test_build_mdp(self): # state labeling state_labeling = stormpy.storage.StateLabeling(nr_states) - labels = {'init', 'one', 'two', 'three', 'four', 'five', 'six', 'done', 'deadlock'} + labels = {"init", "one", "two", "three", "four", "five", "six", "done", "deadlock"} for label in labels: state_labeling.add_label(label) - state_labeling.add_label_to_state('init', 0) - 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("init", 0) + 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.set_states('done', stormpy.BitVector(nr_states, [7, 8, 9, 10, 11, 12])) + state_labeling.set_states("done", stormpy.BitVector(nr_states, [7, 8, 9, 10, 11, 12])) # reward models reward_models = {} # Vector representing the state-action rewards 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["coin_flips"] = stormpy.SparseRewardModel(optional_state_action_reward_vector=action_reward) # choice labeling choice_labeling = stormpy.storage.ChoiceLabeling(nr_choices) - choice_labels = {'a', 'b'} + choice_labels = {"a", "b"} for label in choice_labels: choice_labeling.add_label(label) - choice_labeling.add_label_to_choice('a', 0) - choice_labeling.add_label_to_choice('b', 1) + choice_labeling.add_label_to_choice("a", 0) + choice_labeling.add_label_to_choice("b", 1) # state valuations manager = stormpy.ExpressionManager() - var_s = manager.create_integer_variable(name='s') - var_d = manager.create_integer_variable(name='d') + var_s = manager.create_integer_variable(name="s") + var_d = manager.create_integer_variable(name="d") v_builder = stormpy.StateValuationsBuilder() v_builder.add_variable(var_s) v_builder.add_variable(var_d) @@ -240,12 +236,12 @@ def test_build_mdp(self): # 0: no origin id_to_command_set_mapping[i].insert(i - 1) id_to_command_set_mapping[9].insert(8) - choice_origins = stormpy.PrismChoiceOrigins(prism_program, index_to_identifier_mapping, - id_to_command_set_mapping) + choice_origins = stormpy.PrismChoiceOrigins(prism_program, index_to_identifier_mapping, id_to_command_set_mapping) # Construct Components - components = stormpy.SparseModelComponents(transition_matrix=transition_matrix, state_labeling=state_labeling, - reward_models=reward_models, rate_transitions=False) + components = stormpy.SparseModelComponents( + transition_matrix=transition_matrix, state_labeling=state_labeling, reward_models=reward_models, rate_transitions=False + ) components.state_valuations = state_valuations components.choice_labeling = choice_labeling components.choice_origins = choice_origins @@ -262,13 +258,12 @@ def test_build_mdp(self): assert mdp.nr_transitions == 22 assert mdp.transition_matrix.nr_entries == mdp.nr_transitions for e in mdp.transition_matrix: - assert e.value() == 0.5 or e.value() == 0 or e.value() == 0.2 or e.value() == 0.8 or ( - e.value() == 1 and e.column > 6) + assert e.value() == 0.5 or e.value() == 0 or e.value() == 0.2 or e.value() == 0.8 or (e.value() == 1 and e.column > 6) for state in mdp.states: assert len(state.actions) <= 2 # Test state labeling - assert mdp.labeling.get_labels() == {'init', 'deadlock', 'done', 'one', 'two', 'three', 'four', 'five', 'six'} + assert mdp.labeling.get_labels() == {"init", "deadlock", "done", "one", "two", "three", "four", "five", "six"} # Test reward models assert len(mdp.reward_models) == 1 @@ -280,7 +275,7 @@ def test_build_mdp(self): # Test choice labeling assert mdp.has_choice_labeling() - assert mdp.choice_labeling.get_labels() == {'a', 'b'} + assert mdp.choice_labeling.get_labels() == {"a", "b"} # Test state valuations assert mdp.has_state_valuations() @@ -306,63 +301,67 @@ def test_build_ctmc(self): nr_choices = 12 # Build transition_matrix - transitions = np.array([ - [0, 0.5, 0.5, 200, 0, 0, 0, 0, 0, 0, 0, 0], - [0, 0, 0, 0, 0.5, 200, 0, 0, 0, 0, 0, 0], - [0, 0, 0, 0, 0.5, 0, 200, 0, 0, 0, 0, 0], - [200, 0, 0, 0, 0, 0, 0.5, 0.5, 0, 0, 0, 0], - [0, 0, 0, 0, 0, 0, 0, 0, 200, 0, 0, 0], - [0, 0, 0, 1, 0, 0, 0, 0, 0.5, 0, 0, 0], - [0, 0, 0, 0, 0, 0, 0, 0, 0, 0.5, 200, 0], - [0, 200, 0, 0, 0, 0, 0, 0, 0, 0.5, 0, 0], - [0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0], - [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 200], - [1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0.5], - [0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]], dtype='float64') + transitions = np.array( + [ + [0, 0.5, 0.5, 200, 0, 0, 0, 0, 0, 0, 0, 0], + [0, 0, 0, 0, 0.5, 200, 0, 0, 0, 0, 0, 0], + [0, 0, 0, 0, 0.5, 0, 200, 0, 0, 0, 0, 0], + [200, 0, 0, 0, 0, 0, 0.5, 0.5, 0, 0, 0, 0], + [0, 0, 0, 0, 0, 0, 0, 0, 200, 0, 0, 0], + [0, 0, 0, 1, 0, 0, 0, 0, 0.5, 0, 0, 0], + [0, 0, 0, 0, 0, 0, 0, 0, 0, 0.5, 200, 0], + [0, 200, 0, 0, 0, 0, 0, 0, 0, 0.5, 0, 0], + [0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0], + [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 200], + [1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0.5], + [0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], + ], + dtype="float64", + ) transition_matrix = stormpy.build_sparse_matrix(transitions) # state labeling state_labeling = stormpy.storage.StateLabeling(nr_states) # Add labels - state_labels = {'init', 'deadlock', 'target'} + state_labels = {"init", "deadlock", "target"} for label in state_labels: state_labeling.add_label(label) # Add labels to states - state_labeling.add_label_to_state('init', 0) - state_labeling.set_states('target', stormpy.BitVector(nr_states, [5, 8])) + state_labeling.add_label_to_state("init", 0) + state_labeling.set_states("target", stormpy.BitVector(nr_states, [5, 8])) # reward models reward_models = {} # vector representing state-action rewards action_reward = [0.0, 0.0, 0.0, 0.0, 0.0, 2 / 3, 0.0, 0.0, 1.0, 0.0, 0.0, 0.0] - reward_models['served'] = stormpy.SparseRewardModel(optional_state_action_reward_vector=action_reward) + reward_models["served"] = stormpy.SparseRewardModel(optional_state_action_reward_vector=action_reward) # vector representing state rewards state_reward = [0.0, 1.0, 0.0, 0.0, 1.0, 0.0, 0.0, 1.0, 0.0, 1.0, 0.0, 1.0] - reward_models['waiting'] = stormpy.SparseRewardModel(optional_state_reward_vector=state_reward) + reward_models["waiting"] = stormpy.SparseRewardModel(optional_state_reward_vector=state_reward) # choice labeling choice_labeling = stormpy.storage.ChoiceLabeling(nr_choices) - choice_labels = {'loop1a', 'loop1b', 'serve1', 'loop2a', 'loop2b', 'serve2'} + choice_labels = {"loop1a", "loop1b", "serve1", "loop2a", "loop2b", "serve2"} # Add labels for label in choice_labels: choice_labeling.add_label(label) - choice_labeling.set_choices('loop1a', stormpy.BitVector(nr_choices, [0, 2])) - choice_labeling.set_choices('loop1b', stormpy.BitVector(nr_choices, [1, 4])) - choice_labeling.set_choices('serve1', stormpy.BitVector(nr_choices, [5, 8])) - choice_labeling.set_choices('loop2a', stormpy.BitVector(nr_choices, [3, 7])) - choice_labeling.set_choices('loop2b', stormpy.BitVector(nr_choices, [6, 9])) - choice_labeling.set_choices('serve2', stormpy.BitVector(nr_choices, [10, 11])) + choice_labeling.set_choices("loop1a", stormpy.BitVector(nr_choices, [0, 2])) + choice_labeling.set_choices("loop1b", stormpy.BitVector(nr_choices, [1, 4])) + choice_labeling.set_choices("serve1", stormpy.BitVector(nr_choices, [5, 8])) + choice_labeling.set_choices("loop2a", stormpy.BitVector(nr_choices, [3, 7])) + choice_labeling.set_choices("loop2b", stormpy.BitVector(nr_choices, [6, 9])) + choice_labeling.set_choices("serve2", stormpy.BitVector(nr_choices, [10, 11])) # state valuations manager = stormpy.ExpressionManager() - var_s = manager.create_integer_variable(name='s') - var_a = manager.create_integer_variable(name='a') - var_s1 = manager.create_integer_variable(name='s1') - var_s2 = manager.create_integer_variable(name='s2') + var_s = manager.create_integer_variable(name="s") + var_a = manager.create_integer_variable(name="a") + var_s1 = manager.create_integer_variable(name="s1") + var_s2 = manager.create_integer_variable(name="s2") v_builder = stormpy.StateValuationsBuilder() v_builder.add_variable(var_s) v_builder.add_variable(var_a) @@ -385,8 +384,9 @@ def test_build_ctmc(self): state_valuations = v_builder.build() # set rate_transitions to True: the transition values are interpreted as rates - components = stormpy.SparseModelComponents(transition_matrix=transition_matrix, state_labeling=state_labeling, - reward_models=reward_models, rate_transitions=True) + components = stormpy.SparseModelComponents( + transition_matrix=transition_matrix, state_labeling=state_labeling, reward_models=reward_models, rate_transitions=True + ) components.choice_labeling = choice_labeling # exit_rates are not required due to using a rate matrix components.state_valuations = state_valuations @@ -408,14 +408,13 @@ def test_build_ctmc(self): assert len(state.actions) <= 1 # Test state labeling - assert ctmc.labeling.get_labels() == {'target', 'init', 'deadlock'} + assert ctmc.labeling.get_labels() == {"target", "init", "deadlock"} # Test reward models assert len(ctmc.reward_models) == 2 assert not ctmc.reward_models["served"].has_state_rewards assert ctmc.reward_models["served"].has_state_action_rewards - assert ctmc.reward_models["served"].state_action_rewards == [0.0, 0.0, 0.0, 0.0, 0.0, 0.6666666666666666, 0.0, - 0.0, 1.0, 0.0, 0.0, 0.0] + assert ctmc.reward_models["served"].state_action_rewards == [0.0, 0.0, 0.0, 0.0, 0.0, 0.6666666666666666, 0.0, 0.0, 1.0, 0.0, 0.0, 0.0] assert not ctmc.reward_models["served"].has_transition_rewards assert ctmc.reward_models["waiting"].has_state_rewards @@ -425,7 +424,7 @@ def test_build_ctmc(self): # Test choice labeling assert ctmc.has_choice_labeling() - assert ctmc.choice_labeling.get_labels() == {'loop1a', 'loop1b', 'serve1', 'loop2a', 'loop2b', 'serve2'} + assert ctmc.choice_labeling.get_labels() == {"loop1a", "loop1b", "serve1", "loop2a", "loop2b", "serve2"} # Test state valuations assert ctmc.has_state_valuations() @@ -455,8 +454,7 @@ def test_build_ma(self): nr_choices = 10 # Build transition matrix - 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) # Row group, state 0 builder.new_row_group(0) @@ -496,16 +494,16 @@ def test_build_ma(self): # state labeling state_labeling = stormpy.storage.StateLabeling(nr_states) # Add labels - state_labels = {'init', 'deadlock'} + state_labels = {"init", "deadlock"} for label in state_labels: state_labeling.add_label(label) # Add label to states - state_labeling.add_label_to_state('init', 0) + state_labeling.add_label_to_state("init", 0) # state valuations manager = stormpy.ExpressionManager() - var_s = manager.create_integer_variable(name='s') + var_s = manager.create_integer_variable(name="s") v_builder = stormpy.StateValuationsBuilder() v_builder.add_variable(var_s) @@ -519,8 +517,7 @@ def test_build_ma(self): # choice origins: prism_program = stormpy.parse_prism_program(get_example_path("ma", "hybrid_states.ma")) - index_to_identifier_mapping = [1, 2, 3, 4, 5, 6, 7, 8, 9, - 10] + index_to_identifier_mapping = [1, 2, 3, 4, 5, 6, 7, 8, 9, 10] id_to_command_set_mapping = [stormpy.FlatSet() for _ in range(11)] id_to_command_set_mapping[1].insert(2) @@ -534,16 +531,16 @@ def test_build_ma(self): id_to_command_set_mapping[9].insert(6) id_to_command_set_mapping[10].insert(5) - choice_origins = stormpy.PrismChoiceOrigins(prism_program, index_to_identifier_mapping, - id_to_command_set_mapping) + choice_origins = stormpy.PrismChoiceOrigins(prism_program, index_to_identifier_mapping, id_to_command_set_mapping) exit_rates = [3.0, 12.0, 10.0, 3.0, 4.0] markovian_states = stormpy.BitVector(5, [0, 1, 2, 3, 4]) # Build components, set rate_transitions to False - components = stormpy.SparseModelComponents(transition_matrix=transition_matrix, state_labeling=state_labeling, - rate_transitions=False, markovian_states=markovian_states) + components = stormpy.SparseModelComponents( + transition_matrix=transition_matrix, state_labeling=state_labeling, rate_transitions=False, markovian_states=markovian_states + ) components.state_valuations = state_valuations components.choice_origins = choice_origins components.exit_rates = exit_rates @@ -577,7 +574,7 @@ def test_build_ma(self): assert len(state.actions) <= 3 # Test state labeling - assert ma.labeling.get_labels() == {'deadlock', 'init'} + assert ma.labeling.get_labels() == {"deadlock", "init"} # Test reward models assert len(ma.reward_models) == 0 @@ -606,92 +603,119 @@ def test_build_ma(self): @numpy_avail def test_build_pomdp(self): import numpy as np + nr_states = 10 nr_choices = 34 # Build transition matrix - builder = stormpy.SparseMatrixBuilder(rows=0, columns=0, entries=0, force_dimensions=False, - has_custom_row_grouping=True, row_groups=0) - - transitions = np.array([ - [0, 0.125, 0.125, 0.125, 0.125, 0.125, 0.125, 0.125, 0.125, 0], - - [0, 0, 0, 0, 1, 0, 0, 0, 0, 0], - [0, 1, 0, 0, 0, 0, 0, 0, 0, 0], - [0, 0, 1, 0, 0, 0, 0, 0, 0, 0], - [0, 1, 0, 0, 0, 0, 0, 0, 0, 0], - - [0, 0, 0, 0, 0, 1, 0, 0, 0, 0], - [0, 0, 1, 0, 0, 0, 0, 0, 0, 0], - [0, 0, 0, 1, 0, 0, 0, 0, 0, 0], - [0, 1, 0, 0, 0, 0, 0, 0, 0, 0], - - [0, 0, 0, 0, 0, 0, 1, 0, 0, 0], - [0, 0, 0, 1, 0, 0, 0, 0, 0, 0], - [0, 0, 0, 1, 0, 0, 0, 0, 0, 0], - [0, 0, 1, 0, 0, 0, 0, 0, 0, 0], - - [0, 0, 0, 0, 0, 0, 0, 0, 0, 1], - [0, 1, 0, 0, 0, 0, 0, 0, 0, 0], - [0, 0, 0, 0, 0, 1, 0, 0, 0, 0], - [0, 0, 0, 0, 1, 0, 0, 0, 0, 0], - - [0, 0, 0, 0, 0, 0, 0, 1, 0, 0], - [0, 0, 1, 0, 0, 0, 0, 0, 0, 0], - [0, 0, 0, 0, 0, 0, 1, 0, 0, 0], - [0, 0, 0, 0, 1, 0, 0, 0, 0, 0], - - [0, 0, 0, 0, 0, 0, 0, 0, 1, 0], - [0, 0, 0, 1, 0, 0, 0, 0, 0, 0], - [0, 0, 0, 0, 0, 0, 1, 0, 0, 0], - [0, 0, 0, 0, 0, 1, 0, 0, 0, 0], - - [0, 0, 0, 0, 0, 0, 0, 1, 0, 0], - [0, 0, 0, 0, 0, 1, 0, 0, 0, 0], - [0, 0, 0, 0, 0, 0, 0, 0, 1, 0], - [0, 0, 0, 0, 0, 0, 0, 0, 0, 1], - - [0, 0, 0, 0, 0, 0, 0, 0, 1, 0], - [0, 0, 0, 0, 0, 0, 1, 0, 0, 0], - [0, 0, 0, 0, 0, 0, 0, 0, 1, 0], - [0, 0, 0, 0, 0, 0, 0, 1, 0, 0], - - [0, 0, 0, 0, 0, 0, 0, 0, 0, 1]]) - - transition_matrix = stormpy.build_sparse_matrix(transitions, - row_group_indices=[0, 1, 5, 9, 13, 17, 21, 25, 29, 33]) + builder = stormpy.SparseMatrixBuilder(rows=0, columns=0, entries=0, force_dimensions=False, has_custom_row_grouping=True, row_groups=0) + + transitions = np.array( + [ + [0, 0.125, 0.125, 0.125, 0.125, 0.125, 0.125, 0.125, 0.125, 0], + [0, 0, 0, 0, 1, 0, 0, 0, 0, 0], + [0, 1, 0, 0, 0, 0, 0, 0, 0, 0], + [0, 0, 1, 0, 0, 0, 0, 0, 0, 0], + [0, 1, 0, 0, 0, 0, 0, 0, 0, 0], + [0, 0, 0, 0, 0, 1, 0, 0, 0, 0], + [0, 0, 1, 0, 0, 0, 0, 0, 0, 0], + [0, 0, 0, 1, 0, 0, 0, 0, 0, 0], + [0, 1, 0, 0, 0, 0, 0, 0, 0, 0], + [0, 0, 0, 0, 0, 0, 1, 0, 0, 0], + [0, 0, 0, 1, 0, 0, 0, 0, 0, 0], + [0, 0, 0, 1, 0, 0, 0, 0, 0, 0], + [0, 0, 1, 0, 0, 0, 0, 0, 0, 0], + [0, 0, 0, 0, 0, 0, 0, 0, 0, 1], + [0, 1, 0, 0, 0, 0, 0, 0, 0, 0], + [0, 0, 0, 0, 0, 1, 0, 0, 0, 0], + [0, 0, 0, 0, 1, 0, 0, 0, 0, 0], + [0, 0, 0, 0, 0, 0, 0, 1, 0, 0], + [0, 0, 1, 0, 0, 0, 0, 0, 0, 0], + [0, 0, 0, 0, 0, 0, 1, 0, 0, 0], + [0, 0, 0, 0, 1, 0, 0, 0, 0, 0], + [0, 0, 0, 0, 0, 0, 0, 0, 1, 0], + [0, 0, 0, 1, 0, 0, 0, 0, 0, 0], + [0, 0, 0, 0, 0, 0, 1, 0, 0, 0], + [0, 0, 0, 0, 0, 1, 0, 0, 0, 0], + [0, 0, 0, 0, 0, 0, 0, 1, 0, 0], + [0, 0, 0, 0, 0, 1, 0, 0, 0, 0], + [0, 0, 0, 0, 0, 0, 0, 0, 1, 0], + [0, 0, 0, 0, 0, 0, 0, 0, 0, 1], + [0, 0, 0, 0, 0, 0, 0, 0, 1, 0], + [0, 0, 0, 0, 0, 0, 1, 0, 0, 0], + [0, 0, 0, 0, 0, 0, 0, 0, 1, 0], + [0, 0, 0, 0, 0, 0, 0, 1, 0, 0], + [0, 0, 0, 0, 0, 0, 0, 0, 0, 1], + ] + ) + + transition_matrix = stormpy.build_sparse_matrix(transitions, row_group_indices=[0, 1, 5, 9, 13, 17, 21, 25, 29, 33]) # state labeling state_labeling = stormpy.storage.StateLabeling(nr_states) - labels = {'deadlock', 'goal', 'init'} + labels = {"deadlock", "goal", "init"} for label in labels: state_labeling.add_label(label) - state_labeling.add_label_to_state('init', 0) - state_labeling.add_label_to_state('goal', 9) + state_labeling.add_label_to_state("init", 0) + state_labeling.add_label_to_state("goal", 9) # reward models reward_models = {} # Vector representing state-action rewards - action_reward = [0.0, 1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 1.0, - 1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 0.0] - reward_models[''] = stormpy.SparseRewardModel(optional_state_action_reward_vector=action_reward) + action_reward = [ + 0.0, + 1.0, + 1.0, + 1.0, + 1.0, + 1.0, + 1.0, + 1.0, + 1.0, + 1.0, + 1.0, + 1.0, + 1.0, + 1.0, + 1.0, + 1.0, + 1.0, + 1.0, + 1.0, + 1.0, + 1.0, + 1.0, + 1.0, + 1.0, + 1.0, + 1.0, + 1.0, + 1.0, + 1.0, + 1.0, + 1.0, + 1.0, + 1.0, + 0.0, + ] + reward_models[""] = stormpy.SparseRewardModel(optional_state_action_reward_vector=action_reward) # choice labeling choice_labeling = stormpy.storage.ChoiceLabeling(nr_choices) - choice_labels = {'south', 'north', 'west', 'east', 'done'} + choice_labels = {"south", "north", "west", "east", "done"} for label in choice_labels: choice_labeling.add_label(label) - choice_labeling.set_choices('south', stormpy.BitVector(nr_choices, [4, 8, 12, 16, 20, 24, 28, 32])) - choice_labeling.set_choices('north', stormpy.BitVector(nr_choices, [3, 7, 11, 15, 19, 23, 27, 31])) - choice_labeling.set_choices('west', stormpy.BitVector(nr_choices, [2, 6, 10, 14, 18, 22, 26, 30])) - choice_labeling.set_choices('east', stormpy.BitVector(nr_choices, [1, 5, 9, 13, 17, 21, 25, 29])) - choice_labeling.set_choices('done', stormpy.BitVector(nr_choices, [33])) + choice_labeling.set_choices("south", stormpy.BitVector(nr_choices, [4, 8, 12, 16, 20, 24, 28, 32])) + choice_labeling.set_choices("north", stormpy.BitVector(nr_choices, [3, 7, 11, 15, 19, 23, 27, 31])) + choice_labeling.set_choices("west", stormpy.BitVector(nr_choices, [2, 6, 10, 14, 18, 22, 26, 30])) + choice_labeling.set_choices("east", stormpy.BitVector(nr_choices, [1, 5, 9, 13, 17, 21, 25, 29])) + choice_labeling.set_choices("done", stormpy.BitVector(nr_choices, [33])) # state valuations manager = stormpy.ExpressionManager() - var_x = manager.create_integer_variable(name='x') - var_y = manager.create_integer_variable(name='y') - var_o = manager.create_integer_variable(name='o') + var_x = manager.create_integer_variable(name="x") + var_y = manager.create_integer_variable(name="y") + var_o = manager.create_integer_variable(name="o") v_builder = stormpy.StateValuationsBuilder() v_builder.add_variable(var_x) @@ -714,8 +738,9 @@ def test_build_pomdp(self): observations = [1, 0, 0, 0, 0, 0, 0, 0, 0, 2] # Build components, set rate_transitions to False - components = stormpy.SparseModelComponents(transition_matrix=transition_matrix, state_labeling=state_labeling, - reward_models=reward_models, rate_transitions=False) + components = stormpy.SparseModelComponents( + transition_matrix=transition_matrix, state_labeling=state_labeling, reward_models=reward_models, rate_transitions=False + ) components.state_valuations = state_valuations components.choice_labeling = choice_labeling # components.choice_origins=choice_origins @@ -736,19 +761,19 @@ def test_build_pomdp(self): assert len(state.actions) <= 4 # Test state labeling - assert pomdp.labeling.get_labels() == {'init', 'goal', 'deadlock'} + assert pomdp.labeling.get_labels() == {"init", "goal", "deadlock"} # Test reward models assert len(pomdp.reward_models) == 1 - assert not pomdp.reward_models[''].has_state_rewards - assert pomdp.reward_models[''].has_state_action_rewards - for reward in pomdp.reward_models[''].state_action_rewards: + assert not pomdp.reward_models[""].has_state_rewards + assert pomdp.reward_models[""].has_state_action_rewards + for reward in pomdp.reward_models[""].state_action_rewards: assert reward == 1.0 or reward == 0.0 - assert not pomdp.reward_models[''].has_transition_rewards + assert not pomdp.reward_models[""].has_transition_rewards # Test choice labeling assert pomdp.has_choice_labeling() - assert pomdp.choice_labeling.get_labels() == {'east', 'west', 'north', 'south', 'done'} + assert pomdp.choice_labeling.get_labels() == {"east", "west", "north", "south", "done"} # Test state valuations assert pomdp.has_state_valuations() @@ -773,6 +798,7 @@ def test_build_pomdp(self): def test_build_parametric_dtmc(self): import stormpy.info import stormpy.pars + if stormpy.info.storm_ratfunc_use_cln(): import pycarl.cln as pc else: @@ -787,12 +813,12 @@ def create_number(num): return pc.FactorizedRationalFunction(num) from pycarl import Variable + nr_states = 13 nr_choices = 13 # transition_matrix - builder = stormpy.ParametricSparseMatrixBuilder(rows=0, columns=0, entries=0, force_dimensions=False, - has_custom_row_grouping=False, row_groups=0) + builder = stormpy.ParametricSparseMatrixBuilder(rows=0, columns=0, entries=0, force_dimensions=False, has_custom_row_grouping=False, row_groups=0) # Create variables var_p = create_polynomial(Variable("p")) @@ -822,29 +848,28 @@ def create_number(num): # state labeling state_labeling = stormpy.storage.StateLabeling(nr_states) - state_labels = {'init', 'one', 'two', 'three', 'four', 'five', 'six', 'done', 'deadlock'} + state_labels = {"init", "one", "two", "three", "four", "five", "six", "done", "deadlock"} for label in state_labels: state_labeling.add_label(label) # Add label to one state - state_labeling.add_label_to_state('init', 0) - 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("init", 0) + 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.set_states('done', stormpy.BitVector(nr_states, [7, 8, 9, 10, 11, 12])) + state_labeling.set_states("done", stormpy.BitVector(nr_states, [7, 8, 9, 10, 11, 12])) # reward_models reward_models = {} # Create a vector representing the state-action rewards action_reward = [one, one, one, one, one, one, one, zero, zero, zero, zero, zero, zero] - reward_models['coin_flips'] = stormpy.SparseParametricRewardModel(optional_state_action_reward_vector=action_reward) + reward_models["coin_flips"] = stormpy.SparseParametricRewardModel(optional_state_action_reward_vector=action_reward) # Construct components - components = stormpy.SparseParametricModelComponents(transition_matrix=transition_matrix, state_labeling=state_labeling, - reward_models=reward_models) + components = stormpy.SparseParametricModelComponents(transition_matrix=transition_matrix, state_labeling=state_labeling, reward_models=reward_models) # Build parametric DTMC dtmc = stormpy.storage.SparseParametricDtmc(components) @@ -863,7 +888,7 @@ def create_number(num): assert len(state.actions) <= 1 # Test state labeling - assert dtmc.labeling.get_labels() == {'init', 'deadlock', 'done', 'one', 'two', 'three', 'four', 'five', 'six'} + assert dtmc.labeling.get_labels() == {"init", "deadlock", "done", "one", "two", "three", "four", "five", "six"} # Test reward_models assert len(dtmc.reward_models) == 1 @@ -876,14 +901,12 @@ def create_number(num): # Test choice labeling assert not dtmc.has_choice_labeling() - def test_build_smg(self): nr_states = 7 nr_choices = 10 # Build transition matrix - 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) # Row group, state 0 builder.new_row_group(0) @@ -918,24 +941,24 @@ def test_build_smg(self): # State labeling state_labeling = stormpy.storage.StateLabeling(nr_states) - labels = {'init_p1', 'bad', 'done'} + labels = {"init_p1", "bad", "done"} for label in labels: state_labeling.add_label(label) - state_labeling.add_label_to_state('init_p1', 0) - state_labeling.add_label_to_state('done', 5) - state_labeling.add_label_to_state('bad', 6) + state_labeling.add_label_to_state("init_p1", 0) + state_labeling.add_label_to_state("done", 5) + state_labeling.add_label_to_state("bad", 6) # Choice labeling choice_labeling = stormpy.storage.ChoiceLabeling(nr_choices) - choice_labels = {'a', 'b', 'c', 'd'} + choice_labels = {"a", "b", "c", "d"} for label in choice_labels: choice_labeling.add_label(label) - choice_labeling.add_label_to_choice('a', 0) - choice_labeling.add_label_to_choice('b', 1) - choice_labeling.add_label_to_choice('c', 2) - choice_labeling.add_label_to_choice('d', 3) - choice_labeling.add_label_to_choice('a', 4) - choice_labeling.add_label_to_choice('b', 5) + choice_labeling.add_label_to_choice("a", 0) + choice_labeling.add_label_to_choice("b", 1) + choice_labeling.add_label_to_choice("c", 2) + choice_labeling.add_label_to_choice("d", 3) + choice_labeling.add_label_to_choice("a", 4) + choice_labeling.add_label_to_choice("b", 5) # State player indications state_player_indications = [0, 1, 2, 0, 2, 1, 0] @@ -959,11 +982,11 @@ def test_build_smg(self): assert len(state.actions) <= 2 # Test state labeling - assert smg.labeling.get_labels() == {'init_p1', 'bad', 'done'} + assert smg.labeling.get_labels() == {"init_p1", "bad", "done"} # Test choice labeling assert smg.has_choice_labeling() - assert smg.choice_labeling.get_labels() == {'a', 'b', 'c', 'd'} + assert smg.choice_labeling.get_labels() == {"a", "b", "c", "d"} # Test state player indications assert smg.get_state_player_indications() == [0, 1, 2, 0, 2, 1, 0] diff --git a/tests/storage/test_prism.py b/tests/storage/test_prism.py index b8a16aaf7..f5a96caea 100644 --- a/tests/storage/test_prism.py +++ b/tests/storage/test_prism.py @@ -2,6 +2,7 @@ from helpers.helper import get_example_path import pytest + class TestPrism: def test_prism_to_jani_states(self): @@ -11,22 +12,20 @@ def test_prism_to_jani_states(self): jani_model, new_properties = program.to_jani(orig_properties) assert len(new_properties) == len(orig_properties) - def test_prism_to_jani_labels(self): program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm")) - orig_properties = stormpy.parse_properties_for_prism_program("P=? [F \"two\"]", program) + orig_properties = stormpy.parse_properties_for_prism_program('P=? [F "two"]', program) assert len(orig_properties) == 1 jani_model, new_properties = program.to_jani(orig_properties) assert len(new_properties) == len(orig_properties) - def test_prism_to_jani_repetitive(self): program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm")) - orig_properties = stormpy.parse_properties_for_prism_program("P=? [F \"two\"]", program) + orig_properties = stormpy.parse_properties_for_prism_program('P=? [F "two"]', program) jani_model, new_properties = program.to_jani(orig_properties) assert len(new_properties) == len(orig_properties) orig_properties = stormpy.parse_properties_for_prism_program("P=? [F s=7]", program) - jani_model, new_properties = program.to_jani(orig_properties, suffix = "2") + jani_model, new_properties = program.to_jani(orig_properties, suffix="2") assert len(new_properties) == len(orig_properties) def test_prism_variables(selfs): diff --git a/tests/storage/test_scheduler.py b/tests/storage/test_scheduler.py index e5f6e9c75..18125ac9e 100644 --- a/tests/storage/test_scheduler.py +++ b/tests/storage/test_scheduler.py @@ -9,7 +9,7 @@ class TestScheduler: def test_scheduler_mdp(self): program = stormpy.parse_prism_program(get_example_path("mdp", "coin2-2.nm")) - formulas = stormpy.parse_properties_for_prism_program("Pmin=? [ F \"finished\" & \"all_coins_equal_1\"]", program) + formulas = stormpy.parse_properties_for_prism_program('Pmin=? [ F "finished" & "all_coins_equal_1"]', program) options = stormpy.BuilderOptions(True, True) options.set_build_state_valuations() options.set_build_choice_labels() @@ -80,7 +80,7 @@ def test_scheduler_ma_via_mdp(self): def test_apply_scheduler_mdp(self): program = stormpy.parse_prism_program(get_example_path("mdp", "coin2-2.nm")) - formulas = stormpy.parse_properties_for_prism_program("Pmin=? [ F \"finished\" & \"all_coins_equal_1\"]", program) + formulas = stormpy.parse_properties_for_prism_program('Pmin=? [ F "finished" & "all_coins_equal_1"]', program) model = stormpy.build_model(program, formulas) assert model.nr_states == 272 assert model.nr_transitions == 492 @@ -104,7 +104,7 @@ def test_apply_scheduler_mdp(self): @spot def test_apply_scheduler_mdp_ltl(self): program = stormpy.parse_prism_program(get_example_path("mdp", "slipgrid.nm")) - properties = stormpy.parse_properties_for_prism_program("Pmax=? [ GF \"target\" & GF \"goal\" ]", program) + properties = stormpy.parse_properties_for_prism_program('Pmax=? [ GF "target" & GF "goal" ]', program) mdp = stormpy.build_model(program, properties) result = stormpy.model_checking(mdp, properties[0], extract_scheduler=True) assert result.has_scheduler diff --git a/tests/storage/test_state.py b/tests/storage/test_state.py index b0d4571a0..a691b0bfd 100644 --- a/tests/storage/test_state.py +++ b/tests/storage/test_state.py @@ -4,8 +4,7 @@ class TestState: def test_states_dtmc(self): - model = stormpy.build_sparse_model_from_explicit(get_example_path("dtmc", "die.tra"), - get_example_path("dtmc", "die.lab")) + model = stormpy.build_sparse_model_from_explicit(get_example_path("dtmc", "die.tra"), get_example_path("dtmc", "die.lab")) i = 0 states = model.states assert len(states) == 13 @@ -19,8 +18,7 @@ def test_states_dtmc(self): assert state.id == 5 def test_states_mdp(self): - model = stormpy.build_sparse_model_from_explicit(get_example_path("mdp", "two_dice.tra"), - get_example_path("mdp", "two_dice.lab")) + model = stormpy.build_sparse_model_from_explicit(get_example_path("mdp", "two_dice.tra"), get_example_path("mdp", "two_dice.lab")) i = 0 assert len(model.states) == 169 for state in model.states: @@ -34,10 +32,22 @@ def test_states_mdp(self): assert state.id == 1 def test_labels_dtmc(self): - model = stormpy.build_sparse_model_from_explicit(get_example_path("dtmc", "die.tra"), - get_example_path("dtmc", "die.lab")) - labelsOrig = [["init"], [], [], [], [], [], [], ["one", "done"], ["two", "done"], ["three", "done"], - ["four", "done"], ["five", "done"], ["six", "done"]] + model = stormpy.build_sparse_model_from_explicit(get_example_path("dtmc", "die.tra"), get_example_path("dtmc", "die.lab")) + labelsOrig = [ + ["init"], + [], + [], + [], + [], + [], + [], + ["one", "done"], + ["two", "done"], + ["three", "done"], + ["four", "done"], + ["five", "done"], + ["six", "done"], + ] i = 0 for state in model.states: labels = state.labels @@ -46,35 +56,47 @@ def test_labels_dtmc(self): i += 1 def test_actions_dtmc(self): - model = stormpy.build_sparse_model_from_explicit(get_example_path("dtmc", "die.tra"), - get_example_path("dtmc", "die.lab")) + model = stormpy.build_sparse_model_from_explicit(get_example_path("dtmc", "die.tra"), get_example_path("dtmc", "die.lab")) for state in model.states: assert len(state.actions) == 1 for action in state.actions: assert action.id == 0 def test_actions_mdp(self): - model = stormpy.build_sparse_model_from_explicit(get_example_path("mdp", "two_dice.tra"), - get_example_path("mdp", "two_dice.lab")) + model = stormpy.build_sparse_model_from_explicit(get_example_path("mdp", "two_dice.tra"), get_example_path("mdp", "two_dice.lab")) for state in model.states: assert len(state.actions) == 1 or len(state.actions) == 2 for action in state.actions: assert action.id == 0 or action.id == 1 def test_transitions_dtmc(self): - transitions_orig = [(0, 1, 0.5), (0, 2, 0.5), (1, 3, 0.5), (1, 4, 0.5), - (2, 5, 0.5), (2, 6, 0.5), (3, 1, 0.5), (3, 7, 0.5), - (4, 8, 0.5), (4, 9, 0.5), (5, 10, 0.5), (5, 11, 0.5), - (6, 2, 0.5), (6, 12, 0.5), (7, 7, 1), (8, 8, 1), - (9, 9, 1), (10, 10, 1), (11, 11, 1), (12, 12, 1) - ] - model = stormpy.build_sparse_model_from_explicit(get_example_path("dtmc", "die.tra"), - get_example_path("dtmc", "die.lab")) + transitions_orig = [ + (0, 1, 0.5), + (0, 2, 0.5), + (1, 3, 0.5), + (1, 4, 0.5), + (2, 5, 0.5), + (2, 6, 0.5), + (3, 1, 0.5), + (3, 7, 0.5), + (4, 8, 0.5), + (4, 9, 0.5), + (5, 10, 0.5), + (5, 11, 0.5), + (6, 2, 0.5), + (6, 12, 0.5), + (7, 7, 1), + (8, 8, 1), + (9, 9, 1), + (10, 10, 1), + (11, 11, 1), + (12, 12, 1), + ] + model = stormpy.build_sparse_model_from_explicit(get_example_path("dtmc", "die.tra"), get_example_path("dtmc", "die.lab")) i = 0 for state in model.states: for action in state.actions: - assert (state.id < 7 and len(action.transitions) == 2) or ( - state.id >= 7 and len(action.transitions) == 1) + assert (state.id < 7 and len(action.transitions) == 2) or (state.id >= 7 and len(action.transitions) == 1) for transition in action.transitions: transition_orig = transitions_orig[i] i += 1 @@ -83,8 +105,7 @@ def test_transitions_dtmc(self): assert transition.value() == transition_orig[2] def test_transitions_mdp(self): - model = stormpy.build_sparse_model_from_explicit(get_example_path("mdp", "two_dice.tra"), - get_example_path("mdp", "two_dice.lab")) + model = stormpy.build_sparse_model_from_explicit(get_example_path("mdp", "two_dice.tra"), get_example_path("mdp", "two_dice.lab")) assert model.states[1].id == 1 for state in model.states: i = 0 @@ -95,14 +116,29 @@ def test_transitions_mdp(self): assert i == 1 or i == 2 def test_row_iterator(self): - transitions_orig = [(0, 1, 0.5), (0, 2, 0.5), (1, 3, 0.5), (1, 4, 0.5), - (2, 5, 0.5), (2, 6, 0.5), (3, 1, 0.5), (3, 7, 0.5), - (4, 8, 0.5), (4, 9, 0.5), (5, 10, 0.5), (5, 11, 0.5), - (6, 2, 0.5), (6, 12, 0.5), (7, 7, 1), (8, 8, 1), - (9, 9, 1), (10, 10, 1), (11, 11, 1), (12, 12, 1) - ] - model = stormpy.build_sparse_model_from_explicit(get_example_path("dtmc", "die.tra"), - get_example_path("dtmc", "die.lab")) + transitions_orig = [ + (0, 1, 0.5), + (0, 2, 0.5), + (1, 3, 0.5), + (1, 4, 0.5), + (2, 5, 0.5), + (2, 6, 0.5), + (3, 1, 0.5), + (3, 7, 0.5), + (4, 8, 0.5), + (4, 9, 0.5), + (5, 10, 0.5), + (5, 11, 0.5), + (6, 2, 0.5), + (6, 12, 0.5), + (7, 7, 1), + (8, 8, 1), + (9, 9, 1), + (10, 10, 1), + (11, 11, 1), + (12, 12, 1), + ] + model = stormpy.build_sparse_model_from_explicit(get_example_path("dtmc", "die.tra"), get_example_path("dtmc", "die.lab")) i = 0 for state in model.states: for transition in model.transition_matrix.row_iter(state.id, state.id): diff --git a/tests/storage/test_state_generation.py b/tests/storage/test_state_generation.py index d139b9758..71c68d5b6 100644 --- a/tests/storage/test_state_generation.py +++ b/tests/storage/test_state_generation.py @@ -2,6 +2,7 @@ from stormpy.examples.files import prism_dtmc_die import pytest + class _DfsQueue: def __init__(self): self.queue = [] @@ -44,9 +45,7 @@ def _load_program(filename): program = program.substitute_constants() expression_parser = stormpy.ExpressionParser(program.expression_manager) - expression_parser.set_identifier_mapping( - {var.name: var.get_expression() - for var in program.variables}) + expression_parser.set_identifier_mapping({var.name: var.get_expression() for var in program.variables}) return program, expression_parser @@ -56,6 +55,7 @@ def _find_variable(program, name): return var return None + @pytest.mark.skipif(True, reason="State generation is broken") def test_knuth_yao_die(): program, expression_parser = _load_program(prism_dtmc_die) diff --git a/tests/utility/test_shortestpaths.py b/tests/utility/test_shortestpaths.py index 8f9ff1f92..47ee92edb 100644 --- a/tests/utility/test_shortestpaths.py +++ b/tests/utility/test_shortestpaths.py @@ -10,6 +10,7 @@ # this is admittedly slightly overengineered + class ModelWithKnownShortestPaths: """Knuth's die model with reference kSP methods""" @@ -17,7 +18,7 @@ def __init__(self): self.target_label = "one" program_path = get_example_path("dtmc", "die.pm") - raw_formula = "P=? [ F \"" + self.target_label + "\" ]" + raw_formula = 'P=? [ F "' + self.target_label + '" ]' program = stormpy.parse_prism_program(program_path) formulas = stormpy.parse_properties_for_prism_program(raw_formula, program) diff --git a/tests/utility/test_smtsolver.py b/tests/utility/test_smtsolver.py index cd4327c41..c2e8fe00c 100644 --- a/tests/utility/test_smtsolver.py +++ b/tests/utility/test_smtsolver.py @@ -2,7 +2,8 @@ import pytest -class TestSmtSolver(): + +class TestSmtSolver: def test_smtsolver_init(self): manager = stormpy.ExpressionManager() solver = stormpy.utility.Z3SmtSolver(manager) @@ -50,5 +51,3 @@ def test_smtsolver_arithmetic_unsat(self): solver.add(c2) assert solver.check() == stormpy.utility.SmtCheckResult.Sat assert solver.model.get_integer_value(x) == 1 - - From 8e6c421a55e8bfd3a4917d87de1a0c58ef8d7d27 Mon Sep 17 00:00:00 2001 From: Auto Format Date: Tue, 19 Nov 2024 09:38:50 +0000 Subject: [PATCH 2/2] Add code formatting commit to .git-blame-ignore-revs --- .git-blame-ignore-revs | 1 + 1 file changed, 1 insertion(+) diff --git a/.git-blame-ignore-revs b/.git-blame-ignore-revs index e69de29bb..81681f371 100644 --- a/.git-blame-ignore-revs +++ b/.git-blame-ignore-revs @@ -0,0 +1 @@ +534f29c9e329007d67428da3ef7be84141140fe2