Merge branch 'master' of https://srv-i2.informatik.rwth-aachen.de/scm/git/stormpy

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 <div> 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,

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/ <https://github.com/moves-rwth/stormpy/blob/master/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 <https://github.com/moves-rwth/stormpy/blob/master/examples/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 <https://github.com/moves-rwth/stormpy/blob/master/examples/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 <https://github.com/moves-rwth/stormpy/blob/master/examples/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 <https://github.com/moves-rwth/stormpy/blob/master/examples/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 <https://github.com/moves-rwth/stormpy/blob/master/examples/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.
 
 
 

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 <https://moves-rwth.github.io/storm/>`_. 
-
-
 Stormpy Documentation
 ===================================
 
+
+Stormpy is a set of python bindings for the probabilistic model checker `storm <https://moves-rwth.github.io/storm/>`_.
+
+
 .. toctree::
    :maxdepth: 2
    :caption: Contents:

examples/05-getting-started.py → 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()
+    example_getting_started_06()