diff --git a/doc/source/conf.py b/doc/source/conf.py index 903456d..09d07f1 100644 --- a/doc/source/conf.py +++ b/doc/source/conf.py @@ -23,6 +23,8 @@ import stormpy import stormpy.logic +import sphinx_bootstrap_theme + # -- General configuration ------------------------------------------------ @@ -54,7 +56,7 @@ master_doc = 'index' # General information about the project. project = 'stormpy' -copyright = '2016 Moves RWTH Aachen' +copyright = '2016--2017 Moves RWTH Aachen' author = 'Sebastian Junges, Matthias Volk' # The version info for the project you're documenting, acts as replacement for @@ -93,13 +95,78 @@ add_module_names = False # The theme to use for HTML and HTML Help pages. See the documentation for # a list of builtin themes. # -html_theme = 'bizstyle' +html_theme = 'bootstrap' + +html_theme_path = sphinx_bootstrap_theme.get_html_theme_path() # Theme options are theme-specific and customize the look and feel of a theme # further. For a list of options available for each theme, see the # documentation. # -# html_theme_options = {} + +html_theme_options = { + # Navigation bar title. (Default: ``project`` value) + 'navbar_title': "Stormpy", + + # Tab name for entire site. (Default: "Site") + '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 + # (name, "/aa/bb", 1) # a link to an arbitrary relative url + # (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", "http://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, + + # Render the current pages TOC in the navbar. (Default: true) + 'navbar_pagenav': True, + + # Tab name for the current pages TOC. (Default: "Page") + 'navbar_pagenav_name': "Page", + + # Global TOC depth for "site" navbar tab. (Default: 1) + # Switching to -1 shows all levels. + 'globaltoc_depth': 2, + + # Include hidden TOCs in Site navbar? + # + # Note: If this is "false", you cannot have mixed ``:hidden:`` and + # non-hidden ``toctree`` directives in the same page, or else the build + # will break. + # + # Values: "true" (default) or "false" + 'globaltoc_includehidden': "true", + + # HTML navbar class (Default: "navbar") to attach to
element. + # For black navbar, do "navbar navbar-inverse" + 'navbar_class': "navbar navbar-inverse", + + # Fix navigation bar to top of page? + # Values: "true" (default) or "false" + 'navbar_fixed_top': "true", + + # Location of link to source. + # Options are "nav" (default), "footer" or anything else to exclude. + '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", + + # Choose Bootstrap version. + # Values: "3" (default) or "2" (in quotes) + 'bootstrap_version': "3", +} # 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, diff --git a/doc/source/getting_started.rst b/doc/source/getting_started.rst index 8d2424e..dc3acc3 100644 --- a/doc/source/getting_started.rst +++ b/doc/source/getting_started.rst @@ -13,7 +13,7 @@ While we assume some very basic programming concepts, we refrain from using more We start with a selection of high-level constructs in stormpy, and go into more details afterwards. -.. seealso:: The code examples are also given in the examples/ folder. These boxes throughout the text will tell you which example contains the code discussed. +.. seealso:: The code examples are also given in the `examples/ `_ folder. These boxes throughout the text will tell you which example contains the code discussed. In order to do this, we import stormpy:: @@ -23,7 +23,7 @@ In order to do this, we import stormpy:: Building models ------------------------------------------------ -.. seealso:: ``01-getting-started.py`` +.. seealso:: `01-getting-started.py `_ There are several ways to create a Markov chain. One of the easiest is to parse a description of such a Markov chain and to let storm build the chain. @@ -59,7 +59,7 @@ We will investigate ways to examine the model in more detail in :ref:`getting-st Building properties -------------------------- -.. seealso:: ``02-getting-started.py`` +.. seealso:: `02-getting-started.py `_ Storm takes properties in the prism-property format. To express that one is interested in the reachability of any state where the prism program variable s is 2, one would formulate:: @@ -96,7 +96,7 @@ then storm is only skipping exploration of successors of the particular state y Checking properties ------------------------------------ -.. seealso:: ``03-getting-started.py`` +.. seealso:: `03-getting-started.py `_ The last lesson taught us to construct properties and models with matching state labels. Now default checking routines are just a simple command away:: @@ -125,7 +125,7 @@ A good way to get the result for the initial states is as follows:: Instantiating parametric models ------------------------------------ -.. seealso:: ``04-getting-started.py`` +.. seealso:: `04-getting-started.py `_ Input formats such as prism allow to specify programs with open constants. We refer to these open constants as parameters. If the constants only influence the probabilities or rates, but not the topology of the underlying model, we can build these models as parametric models:: @@ -161,7 +161,10 @@ Checking parametric models Investigating the model ------------------------------------- -.. seealso:: ``06-getting-started.py`` +.. seealso:: `06-getting-started.py `_ + +One powerful part of the storm model checker is to quickly create the Markov chain from higher-order descriptions. +In this example, we will exploit this, and then explore the underlying matrix. diff --git a/doc/source/index.rst b/doc/source/index.rst index 9b081c5..edfa65c 100644 --- a/doc/source/index.rst +++ b/doc/source/index.rst @@ -3,12 +3,13 @@ You can adapt this file completely to your liking, but it should at least contain the root `toctree` directive. -Stormpy is a set of python bindings for the probabilistic model checker `storm `_. - - Stormpy Documentation =================================== + +Stormpy is a set of python bindings for the probabilistic model checker `storm `_. + + .. toctree:: :maxdepth: 2 :caption: Contents: diff --git a/examples/05-getting-started.py b/examples/06-getting-started.py similarity index 68% rename from examples/05-getting-started.py rename to examples/06-getting-started.py index 7b4c8ba..66481bb 100644 --- a/examples/05-getting-started.py +++ b/examples/06-getting-started.py @@ -1,19 +1,13 @@ import stormpy import stormpy.core -import stormpy.pars - -import pycarl -import pycarl.cln -import pycarl.core import stormpy.examples import stormpy.examples.files -def example_getting_started_05(): +def example_getting_started_06(): path = stormpy.examples.files.prism_dtmc_die prism_program = stormpy.parse_prism_program(path) - formula_str = "P=? [F s=7 & d=2]" properties = stormpy.parse_properties_for_prism_program(formula_str, prism_program) model = stormpy.build_model(prism_program, properties) @@ -21,9 +15,8 @@ def example_getting_started_05(): for state in model.states: for action in state.actions: for transition in action.transitions: - print("from {} with prob {} go to {}".format(state, transition.value(), transition.column)) - + print("From state {}, with probability {}, go to state {}".format(state, transition.value(), transition.column)) if __name__ == '__main__': - example_getting_started_05() \ No newline at end of file + example_getting_started_06() \ No newline at end of file