sp
/
tempestpy
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

api rst files

refactoring
hannah 4 years ago
committed by Matthias Volk
parent
afb1987830
commit
8afa3529f4
No known key found for this signature in database GPG Key ID: 83A57678F739FCD3
18 changed files with 63 additions and 2940 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 1375
      doc/source/api/core.ipynb
  2. 7
      doc/source/api/core.rst
  3. 99
      doc/source/api/dft.ipynb
  4. 7
      doc/source/api/dft.rst
  5. 25
      doc/source/api/exceptions.ipynb
  6. 7
      doc/source/api/exceptions.rst
  7. 384
      doc/source/api/gspn.ipynb
  8. 7
      doc/source/api/gspn.rst
  9. 34
      doc/source/api/info.ipynb
  10. 7
      doc/source/api/info.rst
  11. 101
      doc/source/api/logic.ipynb
  12. 7
      doc/source/api/logic.rst
  13. 110
      doc/source/api/pars.ipynb
  14. 7
      doc/source/api/pars.rst
  15. 759
      doc/source/api/storage.ipynb
  16. 7
      doc/source/api/storage.rst
  17. 53
      doc/source/api/utility.ipynb
  18. 7
      doc/source/api/utility.rst

1375
doc/source/api/core.ipynb
File diff suppressed because it is too large
View File

7
doc/source/api/core.rst
View File

@ -0,0 +1,7 @@
Stormpy.core
**************************
.. automodule:: stormpy
:members:
:undoc-members:
:imported-members:

99
doc/source/api/dft.ipynb
View File

@ -1,99 +0,0 @@
{
"cells": [
{
"cell_type": "markdown",
"metadata": {},
"source": [
"# Stormpy.dft\n",
"\n",
"class DFTDynamic Fault Tree\n",
"\n",
"can_have_nondeterminismself: stormpy.dft.dft.DFTboolWhether the model can contain non-deterministic choices\n",
"\n",
"get_elementself: stormpy.dft.dft.DFTindex: intstormpy.dft.dft.DFTElementGet DFT element at index\n",
"\n",
"get_element_by_nameself: stormpy.dft.dft.DFTname: strstormpy.dft.dft.DFTElementGet DFT element by name\n",
"\n",
"modularisationself: stormpy.dft.dft.DFTList[stormpy.dft.dft.DFT]Split DFT into independent modules\n",
"\n",
"nr_beself: stormpy.dft.dft.DFTintNumber of basic elements\n",
"\n",
"nr_dynamicself: stormpy.dft.dft.DFTintNumber of dynamic elements\n",
"\n",
"nr_elementsself: stormpy.dft.dft.DFTintTotal number of elements\n",
"\n",
"symmetriesself: stormpy.dft.dft.DFTstorm::storage::DFTIndependentSymmetriesCompute symmetries in DFT\n",
"\n",
"property top_level_elementGet top level element\n",
"\n",
"class DFTElementDFT element\n",
"\n",
"property idId\n",
"\n",
"property nameName\n",
"\n",
"class DFTSymmetriesSymmetries in DFT\n",
"\n",
"property groupsSymmetry groups\n",
"\n",
"class ParametricDFTParametric DFT\n",
"\n",
"can_have_nondeterminismself: stormpy.dft.dft.ParametricDFTboolWhether the model can contain non-deterministic choices\n",
"\n",
"get_elementself: stormpy.dft.dft.ParametricDFTindex: intstormpy.dft.dft.ParametricDFTElementGet DFT element at index\n",
"\n",
"get_element_by_nameself: stormpy.dft.dft.ParametricDFTname: strstormpy.dft.dft.ParametricDFTElementGet DFT element by name\n",
"\n",
"modularisationself: stormpy.dft.dft.ParametricDFTList[stormpy.dft.dft.ParametricDFT]Split DFT into independent modules\n",
"\n",
"nr_beself: stormpy.dft.dft.ParametricDFTintNumber of basic elements\n",
"\n",
"nr_dynamicself: stormpy.dft.dft.ParametricDFTintNumber of dynamic elements\n",
"\n",
"nr_elementsself: stormpy.dft.dft.ParametricDFTintTotal number of elements\n",
"\n",
"symmetriesself: stormpy.dft.dft.ParametricDFTstorm::storage::DFTIndependentSymmetriesCompute symmetries in DFT\n",
"\n",
"property top_level_elementGet top level element\n",
"\n",
"class ParametricDFTElementParametric DFT element\n",
"\n",
"property idId\n",
"\n",
"property nameName\n",
"\n",
"analyze_dftdft: stormpy.dft.dft.DFTproperties: List[stormpy.logic.logic.Formula]symred: bool = Trueallow_modularisation: bool = Falserelevant_events: Set[int] = set()dc_for_relevant: bool = FalseList[float]Analyze the DFT\n",
"\n",
"compute_dependency_conflictsdft: stormpy.dft.dft.DFTuse_smt: bool = Falsesolver_timeout: float = 0boolSet conflicts between FDEPs. Is used in analysis.\n",
"\n",
"compute_relevant_eventsdft: stormpy.dft.dft.DFTproperties: List[stormpy.logic.logic.Formula]additional_relevant_names: List[str] = []Set[int]Compute relevant event ids from properties and additional relevant names\n",
"\n",
"export_dft_json_filedft: stormpy.dft.dft.DFTpath: strNoneExport DFT to JSON file\n",
"\n",
"export_dft_json_stringdft: stormpy.dft.dft.DFTstrExport DFT to JSON string\n",
"\n",
"is_well_formeddft: stormpy.dft.dft.DFTcheck_valid_for_analysis: bool = TrueTuple[bool, str]Check whether DFT is well-formed.\n",
"\n",
"load_dft_galileo_filepath: strstormpy.dft.dft.DFTLoad DFT from Galileo file\n",
"\n",
"load_dft_json_filepath: strstormpy.dft.dft.DFTLoad DFT from JSON file\n",
"\n",
"load_dft_json_stringjson_string: strstormpy.dft.dft.DFTLoad DFT from JSON string\n",
"\n",
"transform_dftdft: stormpy.dft.dft.DFTunique_constant_be: boolbinary_fdeps: boolstormpy.dft.dft.DFTApply transformations on DFT"
]
}
],
"metadata": {
"date": 1598178166.5329514,
"filename": "dft.rst",
"kernelspec": {
"display_name": "Python",
"language": "python3",
"name": "python3"
},
"title": "Stormpy.dft"
},
"nbformat": 4,
"nbformat_minor": 4
}

7
doc/source/api/dft.rst
View File

@ -0,0 +1,7 @@
Stormpy.dft
**************************
.. automodule:: stormpy.dft
:members:
:undoc-members:
:imported-members:

25
doc/source/api/exceptions.ipynb
View File

@ -1,25 +0,0 @@
{
"cells": [
{
"cell_type": "markdown",
"metadata": {},
"source": [
"# Stormpy.exceptions\n",
"\n",
"exception StormErrormessageBase class for exceptions in Storm."
]
}
],
"metadata": {
"date": 1598178166.53555,
"filename": "exceptions.rst",
"kernelspec": {
"display_name": "Python",
"language": "python3",
"name": "python3"
},
"title": "Stormpy.exceptions"
},
"nbformat": 4,
"nbformat_minor": 4
}

7
doc/source/api/exceptions.rst
View File

@ -0,0 +1,7 @@
Stormpy.exceptions
**************************
.. automodule:: stormpy.exceptions
:members:
:undoc-members:
:imported-members:

384
doc/source/api/gspn.ipynb
View File

@ -1,384 +0,0 @@
{
"cells": [
{
"cell_type": "markdown",
"metadata": {},
"source": [
"# Stormpy.gspn\n",
"\n",
"class GSPNGeneralized Stochastic Petri Net\n",
"\n",
"export_gspn_pnml_fileself: stormpy.gspn.gspn.GSPNfilepath: strNoneExport GSPN to PNML file\n",
"\n",
"export_gspn_pnpro_fileself: stormpy.gspn.gspn.GSPNfilepath: strNoneExport GSPN to PNPRO file\n",
"\n",
"get_immediate_transitionself: stormpy.gspn.gspn.GSPNname: strstorm::gspn::ImmediateTransition<double>Returns the immediate transition with the corresponding name\n",
"\n",
"get_immediate_transitionsself: stormpy.gspn.gspn.GSPNList[storm::gspn::ImmediateTransition<double>]> Returns the immediate transitions of this GSPN.\n",
"\n",
"\n",
"\n",
"<dl style='margin: 20px 0;'>\n",
"<dt>Return type</dt>\n",
"<dd>\n",
"list[stormpy.ImmediateTransition]\n",
"\n",
"</dd>\n",
"\n",
"</dl>\n",
"\n",
"get_initial_markingself: stormpy.gspn.gspn.GSPNarg0: Dict[int, int]arg1: intstorm::gspn::MarkingComputes the initial marking of this GSPN\n",
"\n",
"get_nameself: stormpy.gspn.gspn.GSPNstrGet name of GSPN\n",
"\n",
"get_number_of_immediate_transitionsself: stormpy.gspn.gspn.GSPNintGet the number of immediate transitions in this GSPN\n",
"\n",
"get_number_of_placesself: stormpy.gspn.gspn.GSPNintGet the number of places in this GSPN\n",
"\n",
"get_number_of_timed_transitionsself: stormpy.gspn.gspn.GSPNintGet the number of timed transitions in this GSPN\n",
"\n",
"get_partitionsself: stormpy.gspn.gspn.GSPNList[storm::gspn::TransitionPartition]Get the partitions of this GSPN\n",
"\n",
"get_place*args**kwargsOverloaded function.\n",
"\n",
"1. get_place(self: stormpy.gspn.gspn.GSPN, id: int) -> storm::gspn::Place \n",
" \n",
" \n",
" Returns the place with the corresponding id. \n",
" \n",
" \n",
" <dl style='margin: 20px 0;'>\n",
" <dt>param uint64_t id</dt>\n",
" <dd>\n",
" The ID of the place. \n",
" </dd>\n",
" <dt>rtype</dt>\n",
" <dd>\n",
" stormpy.Place \n",
" </dd>\n",
" \n",
" </dl>\n",
" \n",
" \n",
"1. get_place(self: stormpy.gspn.gspn.GSPN, name: str) -> storm::gspn::Place \n",
"\n",
"\n",
"get_placesself: stormpy.gspn.gspn.GSPNList[storm::gspn::Place]> Returns a vector of the places of this GSPN.\n",
"\n",
"\n",
"\n",
"<dl style='margin: 20px 0;'>\n",
"<dt>Return type</dt>\n",
"<dd>\n",
"list[stormpy.Place]\n",
"\n",
"</dd>\n",
"\n",
"</dl>\n",
"\n",
"get_timed_transitionself: stormpy.gspn.gspn.GSPNname: strstorm::gspn::TimedTransition<double>Returns the timed transition with the corresponding name\n",
"\n",
"get_timed_transitionsself: stormpy.gspn.gspn.GSPNList[storm::gspn::TimedTransition<double>]> Returns a vector of the timed transitions of this GSPN.\n",
"\n",
"\n",
"\n",
"<dl style='margin: 20px 0;'>\n",
"<dt>Return type</dt>\n",
"<dd>\n",
"list[stormpy.TimedTransition]\n",
"\n",
"</dd>\n",
"\n",
"</dl>\n",
"\n",
"get_transitionself: stormpy.gspn.gspn.GSPNname: strstorm::gspn::TransitionReturns the transition with the corresponding name\n",
"\n",
"immediate_transition_id_to_transition_idarg0: intintis_validself: stormpy.gspn.gspn.GSPNboolPerform some checks\n",
"\n",
"set_nameself: stormpy.gspn.gspn.GSPNarg0: strNoneSet name of GSPN\n",
"\n",
"timed_transition_id_to_transition_idarg0: intinttransition_id_to_immediate_transition_idarg0: intinttransition_id_to_timed_transition_idarg0: intintclass GSPNBuilderGeneralized Stochastic Petri Net Builder\n",
"\n",
"add_immediate_transitionself: stormpy.gspn.gspn.GSPNBuilderpriority: int = 0weight: float = 0name: str = ''intAdd an immediate transition to the GSPN\n",
"\n",
"add_inhibition_arc*args**kwargsOverloaded function.\n",
"\n",
"1. add_inhibition_arc(self: stormpy.gspn.gspn.GSPNBuilder, from: int, to: int, multiplicity: int=1) -> None \n",
" \n",
" \n",
" Add an new inhibition arc from a place to a transition. \n",
" \n",
" \n",
" <dl style='margin: 20px 0;'>\n",
" <dt>param from</dt>\n",
" <dd>\n",
" The ID or name of the place from which the arc is originating. \n",
" </dd>\n",
" <dt>type from</dt>\n",
" <dd>\n",
" uint_64_t or str \n",
" </dd>\n",
" <dt>param to</dt>\n",
" <dd>\n",
" The ID or name of the transition to which the arc goes to. \n",
" </dd>\n",
" <dt>type to</dt>\n",
" <dd>\n",
" uint_64_t or str \n",
" </dd>\n",
" <dt>param uint64_t multiplicity</dt>\n",
" <dd>\n",
" The multiplicity of the arc, default = 1. \n",
" </dd>\n",
" \n",
" </dl>\n",
" \n",
" \n",
"1. add_inhibition_arc(self: stormpy.gspn.gspn.GSPNBuilder, from: str, to: str, multiplicity: int=1) -> None \n",
"\n",
"\n",
"add_input_arc*args**kwargsOverloaded function.\n",
"\n",
"1. add_input_arc(self: stormpy.gspn.gspn.GSPNBuilder, from: int, to: int, multiplicity: int=1) -> None \n",
" \n",
" \n",
" Add a new input arc from a place to a transition \n",
" \n",
" \n",
" <dl style='margin: 20px 0;'>\n",
" <dt>param from</dt>\n",
" <dd>\n",
" The ID or name of the place from which the arc is originating. \n",
" </dd>\n",
" <dt>type from</dt>\n",
" <dd>\n",
" uint_64_t or str \n",
" </dd>\n",
" <dt>param uint_64_t to</dt>\n",
" <dd>\n",
" The ID or name of the transition to which the arc goes to. \n",
" </dd>\n",
" <dt>type from</dt>\n",
" <dd>\n",
" uint_64_t or str \n",
" </dd>\n",
" <dt>param uint64_t multiplicity</dt>\n",
" <dd>\n",
" The multiplicity of the arc, default = 1. \n",
" </dd>\n",
" \n",
" </dl>\n",
" \n",
" \n",
"1. add_input_arc(self: stormpy.gspn.gspn.GSPNBuilder, from: str, to: str, multiplicity: int=1) -> None \n",
"\n",
"\n",
"add_normal_arcself: stormpy.gspn.gspn.GSPNBuilderfrom: strto: strmultiplicity: int=1None> Add an arc from a named element to a named element.\n",
"Can be both input or output arc, but not an inhibition arc.\n",
"Convenience function for textual format parsers.\n",
"\n",
"\n",
"\n",
"<dl style='margin: 20px 0;'>\n",
"<dt>Parameters</dt>\n",
"<dd>\n",
"- from (str) – Source element in the GSPN from where this arc starts. \n",
"- to (str) – Target element in the GSPN where this arc ends. \n",
"- multiplicity (uint64_t) – Multiplicity of the arc, default = 1. \n",
"\n",
"\n",
"</dd>\n",
"\n",
"</dl>\n",
"\n",
"add_output_arc*args**kwargsOverloaded function.\n",
"\n",
"1. add_output_arc(self: stormpy.gspn.gspn.GSPNBuilder, from: int, to: int, multiplicity: int=1) -> None \n",
" \n",
" \n",
" Add an new output arc from a transition to a place. \n",
" \n",
" \n",
" <dl style='margin: 20px 0;'>\n",
" <dt>param from</dt>\n",
" <dd>\n",
" The ID or name of the transition from which the arc is originating. \n",
" </dd>\n",
" <dt>type from</dt>\n",
" <dd>\n",
" uint_64_t or str \n",
" </dd>\n",
" <dt>param to</dt>\n",
" <dd>\n",
" The ID or name of the place to which the arc goes to. \n",
" </dd>\n",
" <dt>type to</dt>\n",
" <dd>\n",
" uint_64_t or str \n",
" </dd>\n",
" <dt>param uint64_t multiplicity</dt>\n",
" <dd>\n",
" The multiplicity of the arc, default = 1. \n",
" </dd>\n",
" \n",
" </dl>\n",
" \n",
" \n",
"1. add_output_arc(self: stormpy.gspn.gspn.GSPNBuilder, from: str, to: str, multiplicity: int) -> None \n",
"\n",
"\n",
"add_placeself: stormpy.gspn.gspn.GSPNBuildercapacity: Optional[int] = 1initial_tokens: int = 0name: str = ''intAdd a place to the GSPN\n",
"\n",
"add_timed_transition*args**kwargsOverloaded function.\n",
"\n",
"1. add_timed_transition(self: stormpy.gspn.gspn.GSPNBuilder, priority: int, rate: float, name: str=’’) -> int \n",
"\n",
"\n",
"Add a timed transition to the GSPN\n",
"\n",
"1. add_timed_transition(self: stormpy.gspn.gspn.GSPNBuilder, priority: int, rate: float, num_servers: Optional[int], name: str=’’) -> int \n",
"\n",
"\n",
"build_gspnself: stormpy.gspn.gspn.GSPNBuilderexpression_manager: stormpy.storage.storage.ExpressionManager = Noneconstants_substitution: Dict[stormpy.storage.storage.Variable, stormpy.storage.storage.Expression] = {}storm::gspn::GSPNConstruct GSPN\n",
"\n",
"set_nameself: stormpy.gspn.gspn.GSPNBuildername: strNoneSet name of GSPN\n",
"\n",
"set_place_layout_infoself: stormpy.gspn.gspn.GSPNBuilderplace_id: intlayout_info: storm::gspn::LayoutInfoNone> Set place layout information.\n",
"\n",
"\n",
"\n",
"<dl style='margin: 20px 0;'>\n",
"<dt>Parameters</dt>\n",
"<dd>\n",
"- id (uint64_t) – The ID of the place. \n",
"- layout_info (stormpy.LayoutInfo) – The layout information. \n",
"\n",
"\n",
"</dd>\n",
"\n",
"</dl>\n",
"\n",
"set_transition_layout_infoself: stormpy.gspn.gspn.GSPNBuildertransition_id: intlayout_info: storm::gspn::LayoutInfoNone> Set transition layout information.\n",
"\n",
"\n",
"\n",
"<dl style='margin: 20px 0;'>\n",
"<dt>Parameters</dt>\n",
"<dd>\n",
"- id (uint64_t) – The ID of the transition. \n",
"- layout_info (stormpy.LayoutInfo) – The layout information. \n",
"\n",
"\n",
"</dd>\n",
"\n",
"</dl>\n",
"\n",
"class GSPNParserparseself: stormpy.gspn.gspn.GSPNParserfilename: strconstant_definitions: str = ''stormpy.gspn.gspn.GSPNclass GSPNToJaniBuilderbuildself: stormpy.gspn.gspn.GSPNToJaniBuilderautomaton_name: str = 'gspn_automaton'stormpy.storage.storage.JaniModelBuild Jani model from GSPN\n",
"\n",
"create_deadlock_propertiesself: stormpy.gspn.gspn.GSPNToJaniBuilderjani_model: stormpy.storage.storage.JaniModelList[stormpy.core.Property]Create standard properties for deadlocks\n",
"\n",
"class ImmediateTransitionImmediateTransition in a GSPN\n",
"\n",
"get_weightself: stormpy.gspn.gspn.ImmediateTransitionfloatGet weight of this transition\n",
"\n",
"no_weight_attachedself: stormpy.gspn.gspn.ImmediateTransitionboolTrue iff no weight is attached\n",
"\n",
"set_weightself: stormpy.gspn.gspn.ImmediateTransitionweight: floatNoneSet weight of this transition\n",
"\n",
"class LayoutInfoproperty rotationproperty xproperty yclass PlacePlace in a GSPN\n",
"\n",
"get_capacityself: stormpy.gspn.gspn.PlaceintGet the capacity of tokens of this place\n",
"\n",
"get_idself: stormpy.gspn.gspn.PlaceintGet the id of this place\n",
"\n",
"get_nameself: stormpy.gspn.gspn.PlacestrGet name of this place\n",
"\n",
"get_number_of_initial_tokensself: stormpy.gspn.gspn.PlaceintGet the number of initial tokens of this place\n",
"\n",
"has_restricted_capacityself: stormpy.gspn.gspn.PlaceboolIs capacity of this place restricted\n",
"\n",
"set_capacityself: stormpy.gspn.gspn.Placecap: Optional[int]NoneSet the capacity of tokens of this place\n",
"\n",
"set_nameself: stormpy.gspn.gspn.Placename: strNoneSet name of this place\n",
"\n",
"set_number_of_initial_tokensself: stormpy.gspn.gspn.Placetokens: intNoneSet the number of initial tokens of this place\n",
"\n",
"class TimedTransitionTimedTransition in a GSPN\n",
"\n",
"get_number_of_serversself: stormpy.gspn.gspn.TimedTransitionintGet number of servers\n",
"\n",
"get_rateself: stormpy.gspn.gspn.TimedTransitionfloatGet rate of this transition\n",
"\n",
"has_infinite_server_semanticsself: stormpy.gspn.gspn.TimedTransitionboolGet semantics of this transition\n",
"\n",
"has_k_server_semanticsself: stormpy.gspn.gspn.TimedTransitionboolGet semantics of this transition\n",
"\n",
"has_single_server_semanticsself: stormpy.gspn.gspn.TimedTransitionboolGet semantics of this transition\n",
"\n",
"set_infinite_server_semanticsself: stormpy.gspn.gspn.TimedTransitionNoneSet semantics of this transition\n",
"\n",
"set_k_server_semanticsself: stormpy.gspn.gspn.TimedTransitionk: intNoneSet semantics of this transition\n",
"\n",
"set_rateself: stormpy.gspn.gspn.TimedTransitionrate: floatNoneSet rate of this transition\n",
"\n",
"set_single_server_semanticsself: stormpy.gspn.gspn.TimedTransitionNoneSet semantics of this transition\n",
"\n",
"class TransitionTransition in a GSPN\n",
"\n",
"exists_inhibition_arcself: stormpy.gspn.gspn.Transitionplace: stormpy.gspn.gspn.PlaceboolCheck whether the given place is connected to this transition via an inhibition arc.\n",
"\n",
"exists_input_arcself: stormpy.gspn.gspn.Transitionplace: stormpy.gspn.gspn.PlaceboolCheck whether the given place is connected to this transition via an input arc.\n",
"\n",
"exists_output_arcself: stormpy.gspn.gspn.Transitionplace: stormpy.gspn.gspn.PlaceboolCheck whether the given place is connected to this transition via an output arc.\n",
"\n",
"fireself: stormpy.gspn.gspn.Transitionmarking: storm::gspn::Markingstorm::gspn::MarkingFire the transition if possible.\n",
"\n",
"get_idself: stormpy.gspn.gspn.TransitionintGet id of this transition\n",
"\n",
"get_inhibition_arc_multiplicityself: stormpy.gspn.gspn.Transitionplace: stormpy.gspn.gspn.PlaceintReturns the corresponding multiplicity.\n",
"\n",
"get_inhibition_placesself: stormpy.gspn.gspn.TransitionDict[int, int]get_input_arc_multiplicityself: stormpy.gspn.gspn.Transitionplace: stormpy.gspn.gspn.PlaceintReturns the corresponding multiplicity.\n",
"\n",
"get_input_placesself: stormpy.gspn.gspn.TransitionDict[int, int]get_nameself: stormpy.gspn.gspn.TransitionstrGet name of this transition\n",
"\n",
"get_output_arc_multiplicityself: stormpy.gspn.gspn.Transitionplace: stormpy.gspn.gspn.PlaceintReturns the corresponding multiplicity.\n",
"\n",
"get_output_placesself: stormpy.gspn.gspn.TransitionDict[int, int]get_priorityself: stormpy.gspn.gspn.TransitionintGet priority of this transition\n",
"\n",
"is_enabledself: stormpy.gspn.gspn.Transitionmarking: storm::gspn::MarkingboolCheck if the given marking enables the transition.\n",
"\n",
"remove_inhibition_arcself: stormpy.gspn.gspn.Transitionplace: stormpy.gspn.gspn.PlaceboolRemove an inhibition arc connected to a given place.\n",
"\n",
"remove_input_arcself: stormpy.gspn.gspn.Transitionplace: stormpy.gspn.gspn.PlaceboolRemove an input arc connected to a given place.\n",
"\n",
"remove_output_arcself: stormpy.gspn.gspn.Transitionplace: stormpy.gspn.gspn.PlaceboolRemove an output arc connected to a given place.\n",
"\n",
"set_inhibition_arc_multiplicityself: stormpy.gspn.gspn.Transitionplace: stormpy.gspn.gspn.Placemultiplicity: intNoneSet the multiplicity of the inhibition arc originating from the place.\n",
"\n",
"set_input_arc_multiplicityself: stormpy.gspn.gspn.Transitionplace: stormpy.gspn.gspn.Placemultiplicity: intNoneSet the multiplicity of the input arc originating from the place.\n",
"\n",
"set_nameself: stormpy.gspn.gspn.Transitionname: strNoneSet name of this transition\n",
"\n",
"set_output_arc_multiplicityself: stormpy.gspn.gspn.Transitionplace: stormpy.gspn.gspn.Placemultiplicity: intNoneSet the multiplicity of the output arc going to the place.\n",
"\n",
"set_priorityself: stormpy.gspn.gspn.Transitionpriority: intNoneSet priority of this transition\n",
"\n",
"class TransitionPartitionnr_transitionsself: stormpy.gspn.gspn.TransitionPartitionintGet number of transitions\n",
"\n",
"property priorityproperty transitions"
]
}
],
"metadata": {
"date": 1598178166.7294815,
"filename": "gspn.rst",
"kernelspec": {
"display_name": "Python",
"language": "python3",
"name": "python3"
},
"title": "Stormpy.gspn"
},
"nbformat": 4,
"nbformat_minor": 4
}

7
doc/source/api/gspn.rst
View File

@ -0,0 +1,7 @@
Stormpy.gspn
**************************
.. automodule:: stormpy.gspn
:members:
:undoc-members:
:imported-members:

34
doc/source/api/info.ipynb
View File

@ -1,34 +0,0 @@
{
"cells": [
{
"cell_type": "markdown",
"metadata": {},
"source": [
"# Stormpy.info\n",
"\n",
"class VersionVersion information for Storm\n",
"\n",
"build_info = \"Compiled on Linux 5.4.0-31-generic using gcc 9.3.0 with flags ' -std=c++14 -O3 -DNDEBUG -fprefetch-loop-arrays -flto -flto-partition=none -march=native -fomit-frame-pointer'\"development = Truelong = 'Version 1.6.1 (dev) (+ 121 commits) build from revision 8d9e2a92f03b713aee2a4b6b65737cc5c8c54856 (clean)'major = 1minor = 6patch = 1short = '1.6.1 (dev)'storm_exact_use_clnCheck if exact arithmetic in Storm uses CLN.\n",
":return: True if exact arithmetic uses CLN.\n",
"\n",
"storm_ratfunc_use_clnCheck if rational functions in Storm use CLN.\n",
":return: True iff rational functions use CLN.\n",
"\n",
"storm_versionGet storm version.\n",
":return: Storm version"
]
}
],
"metadata": {
"date": 1598178166.7365491,
"filename": "info.rst",
"kernelspec": {
"display_name": "Python",
"language": "python3",
"name": "python3"
},
"title": "Stormpy.info"
},
"nbformat": 4,
"nbformat_minor": 4
}

7
doc/source/api/info.rst
View File

@ -0,0 +1,7 @@
Stormpy.info
**************************
.. automodule:: stormpy.info
:members:
:undoc-members:
:imported-members:

101
doc/source/api/logic.ipynb
View File

@ -1,101 +0,0 @@
{
"cells": [
{
"cell_type": "markdown",
"metadata": {},
"source": [
"# Stormpy.logic\n",
"\n",
"class AtomicExpressionFormulaFormula with an atomic expression\n",
"\n",
"class AtomicLabelFormulaFormula with an atomic label\n",
"\n",
"class BinaryPathFormulaPath formula with two operands\n",
"\n",
"property left_subformulaproperty right_subformulaclass BinaryStateFormulaState formula with two operands\n",
"\n",
"class BooleanBinaryStateFormulaBoolean binary state formula\n",
"\n",
"class BooleanLiteralFormulaFormula with a boolean literal\n",
"\n",
"class BoundedUntilFormulaUntil Formula with either a step or a time bound.\n",
"\n",
"class ComparisonTypeGEQ = ComparisonType.GEQGREATER = ComparisonType.GREATERLEQ = ComparisonType.LEQLESS = ComparisonType.LESSclass ConditionalFormulaFormula with the right hand side being a condition.\n",
"\n",
"class CumulativeRewardFormulaSummed rewards over a the paths\n",
"\n",
"class EventuallyFormulaFormula for eventually\n",
"\n",
"class FormulaGeneric Storm Formula\n",
"\n",
"cloneself: stormpy.logic.logic.Formulastormpy.logic.logic.Formulaproperty is_probability_operatoris it a probability operator\n",
"\n",
"property is_reward_operatoris it a reward operator\n",
"\n",
"substituteself: stormpy.logic.logic.Formulaconstants_map: Dict[stormpy.storage.storage.Variable, stormpy.storage.storage.Expression]stormpy.logic.logic.FormulaSubstitute variables\n",
"\n",
"substitute_labels_by_labelsself: stormpy.logic.logic.Formulareplacements: Dict[str, str]stormpy.logic.logic.Formulasubstitute label occurences\n",
"\n",
"class GloballyFormulaFormula for globally\n",
"\n",
"class InstantaneousRewardFormulaInstantaneous reward\n",
"\n",
"class LongRunAvarageOperatorLong run average operator\n",
"\n",
"class LongRunAverageRewardFormulaLong run average reward\n",
"\n",
"class OperatorFormulaOperator formula\n",
"\n",
"property comparison_typeComparison type of bound\n",
"\n",
"property has_boundFlag if formula is bounded\n",
"\n",
"property has_optimality_typeFlag if an optimality type is present\n",
"\n",
"property optimality_typeFlag for the optimality type\n",
"\n",
"remove_boundself: stormpy.logic.logic.OperatorFormulaNoneremove_optimality_typeself: stormpy.logic.logic.OperatorFormulaNoneremove the optimality type\n",
"\n",
"set_boundself: stormpy.logic.logic.OperatorFormulacomparison_type: stormpy.logic.logic.ComparisonTypebound: stormpy.storage.storage.ExpressionNoneSet bound\n",
"\n",
"set_optimality_typeself: stormpy.logic.logic.OperatorFormulanew_optimality_type: stormpy.core.OptimizationDirectionNoneset the optimality type (use remove optimiality type for clearing)\n",
"\n",
"property thresholdThreshold of bound (currently only applicable to rational expressions)\n",
"\n",
"property threshold_exprclass PathFormulaFormula about the probability of a set of paths in an automaton\n",
"\n",
"class ProbabilityOperatorProbability operator\n",
"\n",
"class RewardOperatorReward operator\n",
"\n",
"has_reward_nameself: stormpy.logic.logic.RewardOperatorboolproperty reward_nameclass StateFormulaFormula about a state of an automaton\n",
"\n",
"class TimeOperatorThe time operator\n",
"\n",
"class UnaryBooleanStateFormulaUnary boolean state formula\n",
"\n",
"class UnaryPathFormulaPath formula with one operand\n",
"\n",
"property is_bounded_until_formulaproperty is_eventually_formulaproperty is_until_formulaproperty subformulathe subformula\n",
"\n",
"class UnaryStateFormulaState formula with one operand\n",
"\n",
"property subformulathe subformula\n",
"\n",
"class UntilFormulaPath Formula for unbounded until"
]
}
],
"metadata": {
"date": 1598178166.754715,
"filename": "logic.rst",
"kernelspec": {
"display_name": "Python",
"language": "python3",
"name": "python3"
},
"title": "Stormpy.logic"
},
"nbformat": 4,
"nbformat_minor": 4
}

7
doc/source/api/logic.rst
View File

@ -0,0 +1,7 @@
Stormpy.logic
**************************
.. automodule:: stormpy.logic
:members:
:undoc-members:
:imported-members:

110
doc/source/api/pars.ipynb
View File

@ -1,110 +0,0 @@
{
"cells": [
{
"cell_type": "markdown",
"metadata": {},
"source": [
"# Stormpy.pars\n",
"\n",
"class DtmcParameterLiftingModelCheckerRegion model checker for DTMCs\n",
"\n",
"get_bound_all_statesself: stormpy.pars.pars.DtmcParameterLiftingModelCheckerenvironment: stormpy.core.Environmentregion: stormpy.pars.pars.ParameterRegionmaximise: bool = Truestormpy.core.ExplicitQuantitativeCheckResultGet bound\n",
"\n",
"class MdpParameterLiftingModelCheckerRegion model checker for MPDs\n",
"\n",
"get_bound_all_statesself: stormpy.pars.pars.MdpParameterLiftingModelCheckerenvironment: stormpy.core.Environmentregion: stormpy.pars.pars.ParameterRegionmaximise: bool = Truestormpy.core.ExplicitQuantitativeCheckResultGet bound\n",
"\n",
"class ModelInstantiatormodelClass for instantiating models.\n",
"\n",
"instantiatevaluationInstantiate model with given valuation.\n",
":param valuation: Valuation from parameter to value.\n",
":return: Instantiated model.\n",
"\n",
"class ModelTypeType of the model\n",
"\n",
"CTMC = ModelType.CTMCDTMC = ModelType.DTMCMA = ModelType.MAMDP = ModelType.MDPPOMDP = ModelType.POMDPclass PCtmcInstantiatorInstantiate PCTMCs to CTMCs\n",
"\n",
"instantiateself: stormpy.pars.pars.PCtmcInstantiatorarg0: Dict[pycarl.core.Variable, pycarl.cln.cln.Rational]stormpy.storage.storage.SparseCtmcInstantiate model with given parameter values\n",
"\n",
"class PDtmcExactInstantiationCheckerInstantiate pDTMCs to exact DTMCs and immediately check\n",
"\n",
"checkself: stormpy.pars.pars.PDtmcExactInstantiationCheckerenv: stormpy.core.Environmentinstantiation: Dict[pycarl.core.Variable, pycarl.cln.cln.Rational]stormpy.core._CheckResultset_graph_preservingself: stormpy.pars.pars._PDtmcExactInstantiationCheckerBasevalue: boolNoneclass PDtmcInstantiationCheckerInstantiate pDTMCs to DTMCs and immediately check\n",
"\n",
"checkself: stormpy.pars.pars.PDtmcInstantiationCheckerenv: stormpy.core.Environmentinstantiation: Dict[pycarl.core.Variable, pycarl.cln.cln.Rational]stormpy.core._CheckResultset_graph_preservingself: stormpy.pars.pars._PDtmcInstantiationCheckerBasevalue: boolNoneclass PDtmcInstantiatorInstantiate PDTMCs to DTMCs\n",
"\n",
"instantiateself: stormpy.pars.pars.PDtmcInstantiatorarg0: Dict[pycarl.core.Variable, pycarl.cln.cln.Rational]stormpy.storage.storage.SparseDtmcInstantiate model with given parameter values\n",
"\n",
"class PMaInstantiatorInstantiate PMAs to MAs\n",
"\n",
"instantiateself: stormpy.pars.pars.PMaInstantiatorarg0: Dict[pycarl.core.Variable, pycarl.cln.cln.Rational]stormpy.storage.storage.SparseMAInstantiate model with given parameter values\n",
"\n",
"class PMdpExactInstantiationCheckerInstantiate PMDP to exact MDPs and immediately check\n",
"\n",
"checkself: stormpy.pars.pars.PMdpExactInstantiationCheckerenv: stormpy.core.Environmentinstantiation: Dict[pycarl.core.Variable, pycarl.cln.cln.Rational]stormpy.core._CheckResultset_graph_preservingself: stormpy.pars.pars._PMdpExactInstantiationCheckerBasevalue: boolNoneclass PMdpInstantiationCheckerInstantiate PMDP to MDPs and immediately check\n",
"\n",
"checkself: stormpy.pars.pars.PMdpInstantiationCheckerenv: stormpy.core.Environmentinstantiation: Dict[pycarl.core.Variable, pycarl.cln.cln.Rational]stormpy.core._CheckResultset_graph_preservingself: stormpy.pars.pars._PMdpInstantiationCheckerBasevalue: boolNoneclass PMdpInstantiatorInstantiate PMDPs to MDPs\n",
"\n",
"instantiateself: stormpy.pars.pars.PMdpInstantiatorarg0: Dict[pycarl.core.Variable, pycarl.cln.cln.Rational]stormpy.storage.storage.SparseMdpInstantiate model with given parameter values\n",
"\n",
"class ParameterRegionParameter region\n",
"\n",
"property areaGet area\n",
"\n",
"create_from_stringregion_string: strvariables: Set[pycarl.core.Variable]stormpy.pars.pars.ParameterRegionCreate region from string\n",
"\n",
"class PartialPCtmcInstantiatorInstantiate PCTMCs to CTMCs\n",
"\n",
"instantiateself: stormpy.pars.pars.PartialPCtmcInstantiatorarg0: Dict[pycarl.core.Variable, pycarl.cln.cln.Rational]stormpy.storage.storage.SparseParametricCtmcInstantiate model with given parameter values\n",
"\n",
"class PartialPDtmcInstantiatorInstantiate PDTMCs to DTMCs\n",
"\n",
"instantiateself: stormpy.pars.pars.PartialPDtmcInstantiatorarg0: Dict[pycarl.core.Variable, pycarl.cln.cln.Rational]stormpy.storage.storage.SparseParametricDtmcInstantiate model with given parameter values\n",
"\n",
"class PartialPMaInstantiatorInstantiate PMAs to MAs\n",
"\n",
"instantiateself: stormpy.pars.pars.PartialPMaInstantiatorarg0: Dict[pycarl.core.Variable, pycarl.cln.cln.Rational]stormpy.storage.storage.SparseParametricMAInstantiate model with given parameter values\n",
"\n",
"class PartialPMdpInstantiatorInstantiate PMDPs to MDPs\n",
"\n",
"instantiateself: stormpy.pars.pars.PartialPMdpInstantiatorarg0: Dict[pycarl.core.Variable, pycarl.cln.cln.Rational]stormpy.storage.storage.SparseParametricMdpInstantiate model with given parameter values\n",
"\n",
"class RegionModelCheckerRegion model checker via paramater lifting\n",
"\n",
"check_regionself: stormpy.pars.pars.RegionModelCheckerenvironment: stormpy.core.Environmentregion: stormpy.pars.pars.ParameterRegionhypothesis: stormpy.pars.pars.RegionResultHypothesis = RegionResultHypothesis.UNKNOWNinitialResult: stormpy.pars.pars.RegionResult = RegionResult.UNKNOWNsampleVertices: bool = Falsestormpy.pars.pars.RegionResultCheck region\n",
"\n",
"get_boundself: stormpy.pars.pars.RegionModelCheckerenvironment: stormpy.core.Environmentregion: stormpy.pars.pars.ParameterRegionmaximise: bool = Truepycarl.cln.cln.FactorizedRationalFunctionGet bound\n",
"\n",
"get_split_suggestionself: stormpy.pars.pars.RegionModelCheckerDict[pycarl.core.Variable, float]Get estimate\n",
"\n",
"specifyself: stormpy.pars.pars.RegionModelCheckerenvironment: stormpy.core.Environmentmodel: stormpy.storage.storage._SparseParametricModelformula: stormpy.logic.logic.Formulagenerate_splitting_estimate: bool = Falseallow_model_simplification: bool = TrueNonespecify arguments\n",
"\n",
"class RegionResultTypes of region check results\n",
"\n",
"ALLSAT = RegionResult.ALLSATALLVIOLATED = RegionResult.ALLVIOLATEDCENTERSAT = RegionResult.CENTERSATCENTERVIOLATED = RegionResult.CENTERVIOLATEDEXISTSBOTH = RegionResult.EXISTSBOTHEXISTSSAT = RegionResult.EXISTSSATEXISTSVIOLATED = RegionResult.EXISTSVIOLATEDUNKNOWN = RegionResult.UNKNOWNclass RegionResultHypothesisHypothesis for the result of a parameter region\n",
"\n",
"ALLSAT = RegionResultHypothesis.ALLSATALLVIOLATED = RegionResultHypothesis.ALLVIOLATEDUNKNOWN = RegionResultHypothesis.UNKNOWNexception StormErrormessageBase class for exceptions in Storm.\n",
"\n",
"create_region_checkerenvironment: stormpy.core.Environmentmodel: stormpy.storage.storage._SparseParametricModelformula: stormpy.logic.logic.Formulagenerate_splitting_estimate: bool = Falseallow_model_simplification: bool = Truestormpy.pars.pars.RegionModelCheckerCreate region checker\n",
"\n",
"gather_derivativesmodel: stormpy.storage.storage._SparseParametricModelvar: pycarl.core.VariableSet[pycarl.cln.cln.FactorizedPolynomial]Gather all derivatives of transition probabilities\n",
"\n",
"simplify_modelmodelformulaSimplify parametric model preserving the given formula by eliminating states with constant outgoing probabilities.\n",
":param model: Model.\n",
":param formula: Formula.\n",
":return: Tuple of simplified model and simplified formula."
]
}
],
"metadata": {
"date": 1598178166.7897925,
"filename": "pars.rst",
"kernelspec": {
"display_name": "Python",
"language": "python3",
"name": "python3"
},
"title": "Stormpy.pars"
},
"nbformat": 4,
"nbformat_minor": 4
}

7
doc/source/api/pars.rst
View File

@ -0,0 +1,7 @@
Stormpy.pars
**************************
.. automodule:: stormpy.pars
:members:
:undoc-members:
:imported-members:

759
doc/source/api/storage.ipynb
View File

@ -1,759 +0,0 @@
{
"cells": [
{
"cell_type": "markdown",
"metadata": {},
"source": [
"# Stormpy.storage\n",
"\n",
"class Bdd_SylvanBdd\n",
"\n",
"to_expressionself: stormpy.storage.storage.Bdd_Sylvanexpression_manager: storm::expressions::ExpressionManagerTuple[List[storm::expressions::Expression], Dict[int, storm::expressions::Variable]]class BitVectorgetself: stormpy.storage.storage.BitVectorindex: intboolload_from_stringdescription: strstormpy.storage.storage.BitVectornumber_of_set_bitsself: stormpy.storage.storage.BitVectorintsetself: stormpy.storage.storage.BitVectorindex: intvalue: bool = TrueNoneSet\n",
"\n",
"sizeself: stormpy.storage.storage.BitVectorintstore_as_stringself: stormpy.storage.storage.BitVectorstrclass ChoiceLabelingLabeling for choices\n",
"\n",
"add_label_to_choiceself: stormpy.storage.storage.ChoiceLabelinglabel: strstate: intNoneAdds a label to a given choice\n",
"\n",
"get_choicesself: stormpy.storage.storage.ChoiceLabelinglabel: strstormpy.storage.storage.BitVectorGet all choices which have the given label\n",
"\n",
"get_labels_of_choiceself: stormpy.storage.storage.ChoiceLabelingchoice: intSet[str]Get labels of the given choice\n",
"\n",
"set_choicesself: stormpy.storage.storage.ChoiceLabelinglabel: strchoices: stormpy.storage.storage.BitVectorNoneAdd a label to a the given choices\n",
"\n",
"class ChoiceOriginsThis class represents the origin of choices of a model in terms of the input model spec.\n",
"\n",
"as_jani_choice_originsself: stormpy.storage.storage.ChoiceOriginsstorm::storage::sparse::JaniChoiceOriginsas_prism_choice_originsself: stormpy.storage.storage.ChoiceOriginsstorm::storage::sparse::PrismChoiceOriginsget_choice_infoself: stormpy.storage.storage.ChoiceOriginsidentifier: intstrhuman readable string\n",
"\n",
"get_identifier_infoself: stormpy.storage.storage.ChoiceOriginsidentifier: intstrhuman readable string\n",
"\n",
"get_number_of_identifiersself: stormpy.storage.storage.ChoiceOriginsintthe number of considered identifier\n",
"\n",
"is_jani_choice_originsself: stormpy.storage.storage.ChoiceOriginsboolis_prism_choice_originsself: stormpy.storage.storage.ChoiceOriginsboolclass DdManager_Sylvanget_meta_variableself: stormpy.storage.storage.DdManager_Sylvanexpression_variable: storm::expressions::Variablestormpy.storage.storage.DdMetaVariable_Sylvanclass DdMetaVariableTypeBitvector = DdMetaVariableType.BitvectorBool = DdMetaVariableType.BoolInt = DdMetaVariableType.Intclass DdMetaVariable_Sylvancompute_indicesself: stormpy.storage.storage.DdMetaVariable_Sylvansorted: bool = TrueList[int]property lowest_valueproperty nameproperty typeclass Dd_SylvanDd\n",
"\n",
"property dd_managerget the manager\n",
"\n",
"property meta_variablesthe contained meta variables\n",
"\n",
"property node_countget node count\n",
"\n",
"class DistributionDoubleFinite Support Distribution\n",
"\n",
"class ExpressionHolds an expression\n",
"\n",
"Andarg0: stormpy.storage.storage.Expressionarg1: stormpy.storage.storage.Expressionstormpy.storage.storage.ExpressionConjunctionarg0: List[stormpy.storage.storage.Expression]stormpy.storage.storage.ExpressionDisjunctionarg0: List[stormpy.storage.storage.Expression]stormpy.storage.storage.ExpressionDividearg0: stormpy.storage.storage.Expressionarg1: stormpy.storage.storage.Expressionstormpy.storage.storage.ExpressionEqarg0: stormpy.storage.storage.Expressionarg1: stormpy.storage.storage.Expressionstormpy.storage.storage.ExpressionGeqarg0: stormpy.storage.storage.Expressionarg1: stormpy.storage.storage.Expressionstormpy.storage.storage.ExpressionGreaterarg0: stormpy.storage.storage.Expressionarg1: stormpy.storage.storage.Expressionstormpy.storage.storage.ExpressionIffarg0: stormpy.storage.storage.Expressionarg1: stormpy.storage.storage.Expressionstormpy.storage.storage.ExpressionImpliesarg0: stormpy.storage.storage.Expressionarg1: stormpy.storage.storage.Expressionstormpy.storage.storage.ExpressionLeqarg0: stormpy.storage.storage.Expressionarg1: stormpy.storage.storage.Expressionstormpy.storage.storage.ExpressionLessarg0: stormpy.storage.storage.Expressionarg1: stormpy.storage.storage.Expressionstormpy.storage.storage.ExpressionMinusarg0: stormpy.storage.storage.Expressionarg1: stormpy.storage.storage.Expressionstormpy.storage.storage.ExpressionModuloarg0: stormpy.storage.storage.Expressionarg1: stormpy.storage.storage.Expressionstormpy.storage.storage.ExpressionMultiplyarg0: stormpy.storage.storage.Expressionarg1: stormpy.storage.storage.Expressionstormpy.storage.storage.ExpressionNeqarg0: stormpy.storage.storage.Expressionarg1: stormpy.storage.storage.Expressionstormpy.storage.storage.ExpressionOrarg0: stormpy.storage.storage.Expressionarg1: stormpy.storage.storage.Expressionstormpy.storage.storage.ExpressionPlusarg0: stormpy.storage.storage.Expressionarg1: stormpy.storage.storage.Expressionstormpy.storage.storage.Expressionproperty arityThe arity of the expression\n",
"\n",
"contains_variableself: stormpy.storage.storage.Expressionvariables: Set[stormpy.storage.storage.Variable]boolCheck if the expression contains any of the given variables.\n",
"\n",
"contains_variablesself: stormpy.storage.storage.ExpressionboolCheck if the expression contains variables.\n",
"\n",
"evaluate_as_boolself: stormpy.storage.storage.ExpressionboolGet the boolean value this expression evaluates to\n",
"\n",
"evaluate_as_doubleself: stormpy.storage.storage.ExpressionfloatGet the double value this expression evaluates to\n",
"\n",
"evaluate_as_intself: stormpy.storage.storage.ExpressionintGet the integer value this expression evaluates to\n",
"\n",
"evaluate_as_rationalself: stormpy.storage.storage.Expression__gmp_expr<__mpq_struct [1], __mpq_struct [1]>Get the rational number this expression evaluates to\n",
"\n",
"get_operandself: stormpy.storage.storage.ExpressionoperandIndex: intstormpy.storage.storage.ExpressionGet the operand at the given index\n",
"\n",
"get_variablesself: stormpy.storage.storage.ExpressionSet[stormpy.storage.storage.Variable]Get the variables\n",
"\n",
"has_boolean_typeself: stormpy.storage.storage.ExpressionboolCheck if the expression is a boolean\n",
"\n",
"has_integer_typeself: stormpy.storage.storage.ExpressionboolCheck if the expression is an integer\n",
"\n",
"has_rational_typeself: stormpy.storage.storage.ExpressionboolCheck if the expression is a rational\n",
"\n",
"identifierself: stormpy.storage.storage.ExpressionstrRetrieves the identifier associated with this expression if this expression is a variable\n",
"\n",
"property is_function_applicationTrue iff the expression is a function application (of any sort\n",
"\n",
"is_literalself: stormpy.storage.storage.ExpressionboolCheck if the expression is a literal\n",
"\n",
"is_variableself: stormpy.storage.storage.ExpressionboolCheck if the expression is a variable\n",
"\n",
"property managerGet the manager\n",
"\n",
"property operatorThe operator of the expression (if it is a function application)\n",
"\n",
"simplifyself: stormpy.storage.storage.Expressionstormpy.storage.storage.ExpressionSimplify expression\n",
"\n",
"substituteself: stormpy.storage.storage.Expressionsubstitution_map: Dict[stormpy.storage.storage.Variable, stormpy.storage.storage.Expression]stormpy.storage.storage.Expressionproperty typeGet the Type\n",
"\n",
"class ExpressionManagerManages variables for expressions\n",
"\n",
"create_booleanself: stormpy.storage.storage.ExpressionManagerboolean: boolstorm::expressions::ExpressionCreate expression from boolean\n",
"\n",
"create_boolean_variableself: stormpy.storage.storage.ExpressionManagername: strauxiliary: bool = Falsestorm::expressions::Variablecreate Boolean variable\n",
"\n",
"create_integerself: stormpy.storage.storage.ExpressionManagerinteger: intstorm::expressions::ExpressionCreate expression from integer number\n",
"\n",
"create_integer_variableself: stormpy.storage.storage.ExpressionManagername: strauxiliary: bool = Falsestorm::expressions::Variablecreate Integer variable\n",
"\n",
"create_rationalself: stormpy.storage.storage.ExpressionManager, rational: __gmp_expr<__mpq_struct [1], __mpq_struct [1]>storm::expressions::ExpressionCreate expression from rational number\n",
"\n",
"create_rational_variableself: stormpy.storage.storage.ExpressionManagername: strauxiliary: bool = Falsestorm::expressions::Variablecreate Rational variable\n",
"\n",
"get_variableself: stormpy.storage.storage.ExpressionManagername: strstorm::expressions::Variableget variably by name\n",
"\n",
"class ExpressionParserParser for storm-expressions\n",
"\n",
"parseself: stormpy.storage.storage.ExpressionParserstring: strignore_error: bool = Falsestormpy.storage.storage.Expressionparse\n",
"\n",
"set_identifier_mappingself: stormpy.storage.storage.ExpressionParserarg0: Dict[str, stormpy.storage.storage.Expression]Nonesets identifiers\n",
"\n",
"class ExpressionTypeThe type of an expression\n",
"\n",
"property is_booleanproperty is_integerproperty is_rationalclass ItemLabelingLabeling\n",
"\n",
"add_labelself: stormpy.storage.storage.ItemLabelinglabel: strNoneAdd label\n",
"\n",
"contains_labelself: stormpy.storage.storage.ItemLabelinglabel: strboolCheck if the given label is contained in the labeling\n",
"\n",
"get_labelsself: stormpy.storage.storage.ItemLabelingSet[str]Get all labels\n",
"\n",
"class JaniAssignmentJani Assignment\n",
"\n",
"property expressionclass JaniAutomatonA Jani Automation\n",
"\n",
"add_edgeself: stormpy.storage.storage.JaniAutomatonedge: storm::jani::EdgeNoneadd_initial_locationself: stormpy.storage.storage.JaniAutomatonindex: intNoneadd_locationself: stormpy.storage.storage.JaniAutomatonlocation: storm::jani::Locationintadds a new location, returns the index\n",
"\n",
"property edgesget edges\n",
"\n",
"property initial_location_indicesproperty initial_states_restrictioninitial state restriction\n",
"\n",
"property location_variableproperty locationsproperty nameproperty variablesclass JaniBoundedIntegerVariableA Bounded Integer\n",
"\n",
"class JaniChoiceOriginsThis class represents for each choice the origin in the jani spec.\n",
"\n",
"get_edge_index_setself: stormpy.storage.storage.JaniChoiceOriginschoice_index: intstormpy.core.FlatSetreturns the set of edges that induced the choice\n",
"\n",
"property modelretrieves the associated JANI model\n",
"\n",
"class JaniConstantA Constant in JANI\n",
"\n",
"property definedis constant defined by some expression\n",
"\n",
"property expression_variableexpression variable for this constant\n",
"\n",
"property namename of constant\n",
"\n",
"property typetype of constant\n",
"\n",
"class JaniEdgeA Jani Edge\n",
"\n",
"property action_indexaction index\n",
"\n",
"property colorcolor for the edge\n",
"\n",
"property destinationsedge destinations\n",
"\n",
"property guardedge guard\n",
"\n",
"has_silent_actionself: stormpy.storage.storage.JaniEdgeboolIs the edge labelled with the silent action\n",
"\n",
"property nr_destinationsnr edge destinations\n",
"\n",
"property rateedge rate\n",
"\n",
"property source_location_indexindex for source location\n",
"\n",
"substituteself: stormpy.storage.storage.JaniEdge, mapping: Dict[storm::expressions::Variable, storm::expressions::Expression]Noneproperty template_edgetemplate edge\n",
"\n",
"class JaniEdgeDestinationDestination in Jani\n",
"\n",
"property assignmentsproperty probabilityproperty target_location_indexclass JaniInformationObjectAn object holding information about a JANI model\n",
"\n",
"property avg_var_domain_sizeproperty model_typeproperty nr_automataproperty nr_edgesproperty nr_variablesproperty state_domain_sizeclass JaniLocationA Location in JANI\n",
"\n",
"property assignmentslocation assignments\n",
"\n",
"property namename of the location\n",
"\n",
"class JaniLocationExpanderA transformer for Jani expanding variables into locations\n",
"\n",
"get_resultself: stormpy.storage.storage.JaniLocationExpanderstormpy.storage.storage.JaniModeltransformself: stormpy.storage.storage.JaniLocationExpanderautomaton_name: strvariable_name: strNoneclass JaniModelA Jani Model\n",
"\n",
"add_automatonself: stormpy.storage.storage.JaniModelautomaton: storm::jani::Automatonintadd an automaton (with a unique name)\n",
"\n",
"property automataget automata\n",
"\n",
"check_validself: stormpy.storage.storage.JaniModelNoneSome basic checks to ensure validity\n",
"\n",
"property constantsget constants\n",
"\n",
"decode_automaton_and_edge_indexarg0: intTuple[int, int]get edge and automaton from edge/automaton index\n",
"\n",
"define_constantsself: stormpy.storage.storage.JaniModel, map: Dict[storm::expressions::Variable, storm::expressions::Expression]stormpy.storage.storage.JaniModeldefine constants with a mapping from the corresponding expression variables to expressions\n",
"\n",
"encode_automaton_and_edge_indexarg0: intarg1: intintget edge/automaton-index\n",
"\n",
"property expression_managerget expression manager\n",
"\n",
"finalizeself: stormpy.storage.storage.JaniModelNonefinalizes the model. After this action, be careful changing the data structure.\n",
"\n",
"flatten_compositionself: stormpy.storage.storage.JaniModelsmt_solver_factory: stormpy.utility.utility.SmtSolverFactory=<stormpy.utility.utility.SmtSolverFactory object at 0x7fd42a716670>stormpy.storage.storage.JaniModelget_automatonself: stormpy.storage.storage.JaniModelname: strstorm::jani::Automatonget_automaton_indexself: stormpy.storage.storage.JaniModelname: strintget index for automaton name\n",
"\n",
"get_constantself: stormpy.storage.storage.JaniModelname: strstorm::jani::Constantget constant by name\n",
"\n",
"property global_variableshas_standard_compositionself: stormpy.storage.storage.JaniModelboolis the composition the standard composition\n",
"\n",
"property has_undefined_constantsFlag if program has undefined constants\n",
"\n",
"property initial_states_restrictioninitial states restriction\n",
"\n",
"make_standard_compliantself: stormpy.storage.storage.JaniModelNonemake standard JANI compliant\n",
"\n",
"property model_typeModel type\n",
"\n",
"property namemodel name\n",
"\n",
"remove_constantself: stormpy.storage.storage.JaniModelconstant_name: strNoneremove a constant. Make sure the constant does not appear in the model.\n",
"\n",
"replace_automatonself: stormpy.storage.storage.JaniModelindex: intnew_automaton: storm::jani::AutomatonNonereplace automaton at index\n",
"\n",
"restrict_edgesself: stormpy.storage.storage.JaniModeledge_set: stormpy.core.FlatSetstormpy.storage.storage.JaniModelrestrict model to edges given by set\n",
"\n",
"set_model_typeself: stormpy.storage.storage.JaniModelarg0: stormpy.core.JaniModelTypeNoneSets (only) the model type\n",
"\n",
"set_standard_system_compositionself: stormpy.storage.storage.JaniModelNonesets the composition to the standard composition\n",
"\n",
"substitute_constantsself: stormpy.storage.storage.JaniModelstormpy.storage.storage.JaniModelsubstitute constants\n",
"\n",
"substitute_functionsself: stormpy.storage.storage.JaniModelNonesubstitute functions\n",
"\n",
"to_dotself: stormpy.storage.storage.JaniModelstrproperty undefined_constants_are_graph_preservingFlag if the undefined constants do not change the graph structure\n",
"\n",
"class JaniOrderedAssignmentsSet of assignments\n",
"\n",
"addself: stormpy.storage.storage.JaniOrderedAssignmentsnew_assignment: storm::jani::Assignmentadd_to_existing: bool=Falseboolcloneself: stormpy.storage.storage.JaniOrderedAssignmentsstormpy.storage.storage.JaniOrderedAssignmentsclone assignments (performs a deep copy)\n",
"\n",
"substituteself: stormpy.storage.storage.JaniOrderedAssignments, substitution_map: Dict[storm::expressions::Variable, storm::expressions::Expression]Nonesubstitute in rhs according to given substitution map\n",
"\n",
"class JaniScopeChangerA transformer for Jani changing variables from local to global and vice versa\n",
"\n",
"make_variables_localself: stormpy.storage.storage.JaniScopeChangermodel: stormpy.storage.storage.JaniModelproperties: List[stormpy.core.Property] = []stormpy.storage.storage.JaniModelclass JaniTemplateEdgeTemplate edge, internal data structure for edges\n",
"\n",
"add_destinationself: stormpy.storage.storage.JaniTemplateEdgearg0: storm::jani::TemplateEdgeDestinationNoneproperty assignmentsproperty destinationsproperty guardclass JaniTemplateEdgeDestinationTemplate edge destination, internal data structure for edge destinations\n",
"\n",
"property assignmentsclass JaniVariableA Variable in JANI\n",
"\n",
"property expression_variableexpression variable for this variable\n",
"\n",
"property namename of constant\n",
"\n",
"class JaniVariableSetJani Set of Variables\n",
"\n",
"add_bounded_integer_variableself: stormpy.storage.storage.JaniVariableSetvariable: storm::jani::BoundedIntegerVariablestorm::jani::BoundedIntegerVariableadd_variableself: stormpy.storage.storage.JaniVariableSetarg0: storm::jani::VariableNoneemptyself: stormpy.storage.storage.JaniVariableSetboolis there a variable in the set?\n",
"\n",
"get_variable_by_expr_variableself: stormpy.storage.storage.JaniVariableSetarg0: storm::expressions::Variablestorm::jani::Variableget_variable_by_nameself: stormpy.storage.storage.JaniVariableSetarg0: strstorm::jani::Variableclass ModelTypeType of the model\n",
"\n",
"CTMC = ModelType.CTMCDTMC = ModelType.DTMCMA = ModelType.MAMDP = ModelType.MDPPOMDP = ModelType.POMDPclass OperatorTypeType of an operator (of any sort)\n",
"\n",
"And = OperatorType.AndCeil = OperatorType.CeilDivide = OperatorType.DivideEqual = OperatorType.EqualFloor = OperatorType.FloorGreater = OperatorType.GreaterGreaterOrEqual = OperatorType.GreaterOrEqualIff = OperatorType.IffImplies = OperatorType.ImpliesIte = OperatorType.IteLess = OperatorType.LessLessOrEqual = OperatorType.LessOrEqualMax = OperatorType.MaxMin = OperatorType.MinMinus = OperatorType.MinusModulo = OperatorType.ModuloNot = OperatorType.NotNotEqual = OperatorType.NotEqualOr = OperatorType.OrPlus = OperatorType.PlusPower = OperatorType.PowerTimes = OperatorType.TimesXor = OperatorType.Xorclass ParametricSparseMatrixParametric sparse matrix\n",
"\n",
"get_rowself: stormpy.storage.storage.ParametricSparseMatrixrow: intstorm::storage::SparseMatrix<carl::RationalFunction<carl::FactorizedPolynomial<carl::MultivariatePolynomial<cln::cl_RA, carl::MonomialComparator<&carl::Monomial::compareGradedLexical, true>, carl::StdMultivariatePolynomialPolicies<carl::NoReasons, carl::NoAllocator> > >, true> >::rowsGet row\n",
"\n",
"get_row_group_endself: stormpy.storage.storage.ParametricSparseMatrixarg0: intintget_row_group_startself: stormpy.storage.storage.ParametricSparseMatrixarg0: intintget_rowsself: stormpy.storage.storage.ParametricSparseMatrixrow_start: introw_end: intstorm::storage::SparseMatrix<carl::RationalFunction<carl::FactorizedPolynomial<carl::MultivariatePolynomial<cln::cl_RA, carl::MonomialComparator<&carl::Monomial::compareGradedLexical, true>, carl::StdMultivariatePolynomialPolicies<carl::NoReasons, carl::NoAllocator> > >, true> >::rowsGet rows from start to end\n",
"\n",
"property has_trivial_row_groupingTrivial row grouping\n",
"\n",
"property nr_columnsNumber of columns\n",
"\n",
"property nr_entriesNumber of non-zero entries\n",
"\n",
"property nr_rowsNumber of rows\n",
"\n",
"print_rowself: stormpy.storage.storage.ParametricSparseMatrixrow: intstrPrint row\n",
"\n",
"row_iterself: stormpy.storage.storage.ParametricSparseMatrixrow_start: introw_end: intiteratorGet iterator from start to end\n",
"\n",
"submatrixself: stormpy.storage.storage.ParametricSparseMatrixrow_constraint: stormpy.storage.storage.BitVectorcolumn_constraint: stormpy.storage.storage.BitVectorinsert_diagonal_entries: bool = Falsestormpy.storage.storage.ParametricSparseMatrixGet submatrix\n",
"\n",
"class ParametricSparseMatrixBuilderBuilder of parametric sparse matrix\n",
"\n",
"add_next_valueself: stormpy.storage.storage.ParametricSparseMatrixBuilderrow: intcolumn: intvalue: carl::RationalFunction<carl::FactorizedPolynomial<carl::MultivariatePolynomial<cln::cl_RAcarl::MonomialComparator<&carl::Monomial::compareGradedLexicaltrue>carl::StdMultivariatePolynomialPolicies<carl::NoReasonscarl::NoAllocator> > >true>NoneSets the matrix entry at the given row and column to the given value. After all entries have been added,\n",
"calling function build() is mandatory.\n",
"\n",
"Note: this is a linear setter. That is, it must be called consecutively for each entry, row by row and\n",
"column by column. As multiple entries per column are admitted, consecutive calls to this method are\n",
"admitted to mention the same row-column-pair. If rows are skipped entirely, the corresponding rows are\n",
"treated as empty. If these constraints are not met, an exception is thrown.\n",
"\n",
"\n",
"<dl style='margin: 20px 0;'>\n",
"<dt>Parameters</dt>\n",
"<dd>\n",
"- row (double) – The row in which the matrix entry is to be set \n",
"- column (double) – The column in which the matrix entry is to be set \n",
"- value ([RationalFunction](core#stormpy.RationalFunction)) – The value that is to be set at the specified row and column \n",
"\n",
"\n",
"</dd>\n",
"\n",
"</dl>\n",
"\n",
"buildself: stormpy.storage.storage.ParametricSparseMatrixBuilderoverridden_row_count: int=0overridden_column_count: int=0overridden-row_group_count: int=0storm::storage::SparseMatrix<carl::RationalFunction<carl::FactorizedPolynomial<carl::MultivariatePolynomial<cln::cl_RA, carl::MonomialComparator<&carl::Monomial::compareGradedLexical, true>, carl::StdMultivariatePolynomialPolicies<carl::NoReasons, carl::NoAllocator> > >, true> >Finalize the sparse matrix\n",
"\n",
"get_current_row_group_countself: stormpy.storage.storage.ParametricSparseMatrixBuilderintGet the current row group count\n",
"\n",
"get_last_columnself: stormpy.storage.storage.ParametricSparseMatrixBuilderintthe most recently used column\n",
"\n",
"get_last_rowself: stormpy.storage.storage.ParametricSparseMatrixBuilderintGet the most recently used row\n",
"\n",
"new_row_groupself: stormpy.storage.storage.ParametricSparseMatrixBuilderstarting_row: intNoneStart a new row group in the matrix\n",
"\n",
"replace_columnsself: stormpy.storage.storage.ParametricSparseMatrixBuilderreplacements: List[int]offset: intNoneReplaces all columns with id >= offset according to replacements.\n",
"Every state with id offset+i is replaced by the id in replacements[i]. Afterwards the columns are sorted.\n",
"\n",
"\n",
"<dl style='margin: 20px 0;'>\n",
"<dt>Parameters</dt>\n",
"<dd>\n",
"- const& replacements (std::vector<double>) – replacements Mapping indicating the replacements from offset+i -> value of i \n",
"- offset (int) – Offset to add to each id in vector index. \n",
"\n",
"\n",
"</dd>\n",
"\n",
"</dl>\n",
"\n",
"class ParametricSparseMatrixEntryEntry of parametric sparse matrix\n",
"\n",
"property columnColumn\n",
"\n",
"set_valueself: stormpy.storage.storage.ParametricSparseMatrixEntryvalue: carl::RationalFunction<carl::FactorizedPolynomial<carl::MultivariatePolynomial<cln::cl_RAcarl::MonomialComparator<&carl::Monomial::compareGradedLexicaltrue>carl::StdMultivariatePolynomialPolicies<carl::NoReasonscarl::NoAllocator> > >true>NoneSet value\n",
"\n",
"valueself: stormpy.storage.storage.ParametricSparseMatrixEntrycarl::RationalFunction<carl::FactorizedPolynomial<carl::MultivariatePolynomial<cln::cl_RA, carl::MonomialComparator<&carl::Monomial::compareGradedLexical, true>, carl::StdMultivariatePolynomialPolicies<carl::NoReasons, carl::NoAllocator> > >, true>Value\n",
"\n",
"class ParametricSparseMatrixRowsSet of rows in a parametric sparse matrix\n",
"\n",
"class PrismAssignmentAn assignment in prism\n",
"\n",
"property expressionExpression for the update\n",
"\n",
"property variableVariable that is updated\n",
"\n",
"class PrismBooleanVariableA program boolean variable in a Prism program\n",
"\n",
"class PrismChoiceOriginsThis class represents for each choice the set of prism commands that induced the choice.\n",
"\n",
"get_command_setself: stormpy.storage.storage.PrismChoiceOriginschoice_index: intstormpy.core.FlatSetReturns the set of prism commands that induced the choice\n",
"\n",
"property programretrieves the associated Prism program\n",
"\n",
"class PrismCommandA command in a Prism program\n",
"\n",
"property global_indexGet global index\n",
"\n",
"property guard_expressionGet guard expression\n",
"\n",
"property updatesUpdates in the command\n",
"\n",
"class PrismConstantA constant in a Prism program\n",
"\n",
"property definedIs the constant defined?\n",
"\n",
"property definitionDefining expression\n",
"\n",
"property expression_variableExpression variable\n",
"\n",
"property nameConstant name\n",
"\n",
"property typeThe type of the constant\n",
"\n",
"class PrismIntegerVariableA program integer variable in a Prism program\n",
"\n",
"property lower_bound_expressionThe the lower bound expression of this integer variable\n",
"\n",
"property upper_bound_expressionThe the upper bound expression of this integer variable\n",
"\n",
"class PrismLabelA label in prism\n",
"\n",
"property expressionproperty nameclass PrismModelTypeType of the prism model\n",
"\n",
"CTMC = PrismModelType.CTMCCTMDP = PrismModelType.CTMDPDTMC = PrismModelType.DTMCMA = PrismModelType.MAMDP = PrismModelType.MDPUNDEFINED = PrismModelType.UNDEFINEDclass PrismModuleA module in a Prism program\n",
"\n",
"property boolean_variablesAll boolean Variables of this module\n",
"\n",
"property commandsCommands in the module\n",
"\n",
"get_boolean_variableself: stormpy.storage.storage.PrismModulevariable_name: strstorm::prism::BooleanVariableget_integer_variableself: stormpy.storage.storage.PrismModulevariable_name: strstorm::prism::IntegerVariableproperty integer_variablesAll integer Variables of this module\n",
"\n",
"property nameName of the module\n",
"\n",
"class PrismProgramA Prism Program\n",
"\n",
"property constantsGet Program Constants\n",
"\n",
"define_constantsself: stormpy.storage.storage.PrismProgram, arg0: Dict[storm::expressions::Variable, storm::expressions::Expression]stormpy.storage.storage.PrismProgramDefine constants\n",
"\n",
"property expression_managerGet the expression manager for expressions in this program\n",
"\n",
"flattenself: stormpy.storage.storage.PrismProgramsmt_factory: stormpy.utility.utility.SmtSolverFactory=<stormpy.utility.utility.SmtSolverFactory object at 0x7fd42a7e1730>stormpy.storage.storage.PrismProgramPut program into a single module\n",
"\n",
"get_constantself: stormpy.storage.storage.PrismProgramname: strstorm::prism::Constantget_label_expressionself: stormpy.storage.storage.PrismProgramlabel: strstorm::expressions::ExpressionGet the expression of the given label.\n",
"\n",
"get_moduleself: stormpy.storage.storage.PrismProgrammodule_name: strstorm::prism::Moduleproperty hasUndefinedConstantsDoes the program have undefined constants?\n",
"\n",
"property has_undefined_constantsFlag if program has undefined constants\n",
"\n",
"property isDeterministicModelDoes the program describe a deterministic model?\n",
"\n",
"property labelsGet all labels in the program\n",
"\n",
"property model_typeModel type\n",
"\n",
"property modulesModules in the program\n",
"\n",
"property nr_modulesNumber of modules\n",
"\n",
"restrict_commandsself: stormpy.storage.storage.PrismProgramarg0: stormpy.core.FlatSetstormpy.storage.storage.PrismProgramRestrict commands\n",
"\n",
"property reward_modelsThe defined reward models\n",
"\n",
"simplifyself: stormpy.storage.storage.PrismProgramstormpy.storage.storage.PrismProgramSimplify\n",
"\n",
"substitute_constantsself: stormpy.storage.storage.PrismProgramstormpy.storage.storage.PrismProgramSubstitute constants within program\n",
"\n",
"substitute_formulasself: stormpy.storage.storage.PrismProgramstormpy.storage.storage.PrismProgramSubstitute formulas within program\n",
"\n",
"to_janiself: stormpy.storage.storage.PrismProgramproperties: List[stormpy.core.Property]all_variables_global: bool = Truesuffix: str = ''Tuple[storm::jani::Model, List[stormpy.core.Property]]Transform to Jani program\n",
"\n",
"property undefined_constants_are_graph_preservingFlag if the undefined constants do not change the graph structure\n",
"\n",
"used_constantsself: stormpy.storage.storage.PrismProgramList[storm::prism::Constant]Compute Used Constants\n",
"\n",
"property variablesGet all Expression Variables used by the program\n",
"\n",
"class PrismRewardModelReward declaration in prism\n",
"\n",
"property nameget name of the reward model\n",
"\n",
"class PrismUpdateAn update in a Prism command\n",
"\n",
"property assignmentsAssignments in the update\n",
"\n",
"property probability_expressionThe probability expression for this update\n",
"\n",
"class PrismVariableA program variable in a Prism program\n",
"\n",
"property expression_variableThe expression variable corresponding to the variable\n",
"\n",
"property initial_value_expressionThe expression represented the initial value of the variable\n",
"\n",
"property nameVariable name\n",
"\n",
"class SchedulerChoiceDoubleA choice of a finite memory scheduler\n",
"\n",
"property definedIs the choice defined by the scheduler?\n",
"\n",
"property deterministicIs the choice deterministic (given by a Dirac distribution)?\n",
"\n",
"get_choiceself: stormpy.storage.storage.SchedulerChoiceDoublestorm::storage::Distribution<double, unsigned long>Get the distribution over the actions\n",
"\n",
"get_deterministic_choiceself: stormpy.storage.storage.SchedulerChoiceDoubleintGet the deterministic choice\n",
"\n",
"class SchedulerDoubleA Finite Memory Scheduler\n",
"\n",
"compute_action_supportself: stormpy.storage.storage.SchedulerDoublenondeterministic_choice_indices: List[int]stormpy.storage.storage.BitVectorproperty deterministicIs the scheduler deterministic?\n",
"\n",
"get_choiceself: stormpy.storage.storage.SchedulerDoublestate_index: intmemory_index: int = 0storm::storage::SchedulerChoice<double>property memory_sizeHow much memory does the scheduler take?\n",
"\n",
"property memorylessIs the scheduler memoryless?\n",
"\n",
"property partialIs the scheduler partial?\n",
"\n",
"class SparseCtmcCTMC in sparse representation\n",
"\n",
"property exit_ratesclass SparseDtmcDTMC in sparse representation\n",
"\n",
"class SparseMAMA in sparse representation\n",
"\n",
"apply_schedulerself: stormpy.storage.storage.SparseMAscheduler: storm::storage::Scheduler<double>drop_unreachable_states: bool=Truestormpy.storage.storage._SparseModelapply scheduler\n",
"\n",
"convert_to_ctmcself: stormpy.storage.storage.SparseMAstormpy.storage.storage.SparseCtmcConvert the MA into a CTMC.\n",
"\n",
"property convertible_to_ctmcCheck whether the MA can be converted into a CTMC.\n",
"\n",
"property exit_ratesproperty markovian_statesproperty nondeterministic_choice_indicesclass SparseMatrixSparse matrix\n",
"\n",
"get_rowself: stormpy.storage.storage.SparseMatrixrow: intstorm::storage::SparseMatrix<double>::rowsGet row\n",
"\n",
"get_row_group_endself: stormpy.storage.storage.SparseMatrixarg0: intintget_row_group_startself: stormpy.storage.storage.SparseMatrixarg0: intintget_rowsself: stormpy.storage.storage.SparseMatrixrow_start: introw_end: intstorm::storage::SparseMatrix<double>::rowsGet rows from start to end\n",
"\n",
"property has_trivial_row_groupingTrivial row grouping\n",
"\n",
"property nr_columnsNumber of columns\n",
"\n",
"property nr_entriesNumber of non-zero entries\n",
"\n",
"property nr_rowsNumber of rows\n",
"\n",
"print_rowself: stormpy.storage.storage.SparseMatrixrow: intstrPrint rows from start to end\n",
"\n",
"row_iterself: stormpy.storage.storage.SparseMatrixrow_start: introw_end: intiteratorGet iterator from start to end\n",
"\n",
"submatrixself: stormpy.storage.storage.SparseMatrixrow_constraint: stormpy.storage.storage.BitVectorcolumn_constraint: stormpy.storage.storage.BitVectorinsert_diagonal_entries: bool = Falsestormpy.storage.storage.SparseMatrixGet submatrix\n",
"\n",
"class SparseMatrixBuilderBuilder of sparse matrix\n",
"\n",
"add_next_valueself: stormpy.storage.storage.SparseMatrixBuilderrow: intcolumn: intvalue: floatNoneSets the matrix entry at the given row and column to the given value. After all entries have been added,\n",
"calling function build() is mandatory.\n",
"\n",
"Note: this is a linear setter. That is, it must be called consecutively for each entry, row by row and\n",
"column by column. As multiple entries per column are admitted, consecutive calls to this method are\n",
"admitted to mention the same row-column-pair. If rows are skipped entirely, the corresponding rows are\n",
"treated as empty. If these constraints are not met, an exception is thrown.\n",
"\n",
"\n",
"<dl style='margin: 20px 0;'>\n",
"<dt>Parameters</dt>\n",
"<dd>\n",
"- row (double) – The row in which the matrix entry is to be set \n",
"- column (double) – The column in which the matrix entry is to be set \n",
"- value (double) – The value that is to be set at the specified row and column \n",
"\n",
"\n",
"</dd>\n",
"\n",
"</dl>\n",
"\n",
"buildself: stormpy.storage.storage.SparseMatrixBuilderoverridden_row_count: int=0overridden_column_count: int=0overridden-row_group_count: int=0storm::storage::SparseMatrix<double>Finalize the sparse matrix\n",
"\n",
"get_current_row_group_countself: stormpy.storage.storage.SparseMatrixBuilderintGet the current row group count\n",
"\n",
"get_last_columnself: stormpy.storage.storage.SparseMatrixBuilderintthe most recently used column\n",
"\n",
"get_last_rowself: stormpy.storage.storage.SparseMatrixBuilderintGet the most recently used row\n",
"\n",
"new_row_groupself: stormpy.storage.storage.SparseMatrixBuilderstarting_row: intNoneStart a new row group in the matrix\n",
"\n",
"replace_columnsself: stormpy.storage.storage.SparseMatrixBuilderreplacements: List[int]offset: intNoneReplaces all columns with id >= offset according to replacements.\n",
"Every state with id offset+i is replaced by the id in replacements[i]. Afterwards the columns are sorted.\n",
"\n",
"\n",
"<dl style='margin: 20px 0;'>\n",
"<dt>Parameters</dt>\n",
"<dd>\n",
"- const& replacements (std::vector<double>) – replacements Mapping indicating the replacements from offset+i -> value of i \n",
"- offset (int) – Offset to add to each id in vector index. \n",
"\n",
"\n",
"</dd>\n",
"\n",
"</dl>\n",
"\n",
"class SparseMatrixEntryEntry of sparse matrix\n",
"\n",
"property columnColumn\n",
"\n",
"set_valueself: stormpy.storage.storage.SparseMatrixEntryvalue: floatNoneSet value\n",
"\n",
"valueself: stormpy.storage.storage.SparseMatrixEntryfloatValue\n",
"\n",
"class SparseMatrixRowsSet of rows in a sparse matrix\n",
"\n",
"class SparseMdpMDP in sparse representation\n",
"\n",
"apply_schedulerself: stormpy.storage.storage.SparseMdpscheduler: storm::storage::Scheduler<double>drop_unreachable_states: bool=Truestormpy.storage.storage._SparseModelapply scheduler\n",
"\n",
"get_choice_indexself: stormpy.storage.storage.SparseMdpstate: intaction_offset: intintgets the choice index for the offset action from the given state.\n",
"\n",
"get_nr_available_actionsself: stormpy.storage.storage.SparseMdpstate: intintproperty nondeterministic_choice_indicesclass SparseModelActionAction for state in sparse model\n",
"\n",
"property idId\n",
"\n",
"property transitionsGet transitions\n",
"\n",
"class SparseModelActionsActions for state in sparse model\n",
"\n",
"class SparseModelComponentsComponents required for building a sparse model\n",
"\n",
"property choice_labelingA list that stores a labeling for each choice\n",
"\n",
"property choice_originsStores for each choice from which parts of the input model description it originates\n",
"\n",
"property exit_ratesThe exit rate for each state. Must be given for CTMCs and MAs, if rate_transitions is false. Otherwise, it is optional.\n",
"\n",
"property markovian_statesA list that stores which states are Markovian (only for Markov Automata)\n",
"\n",
"property observability_classesThe POMDP observations\n",
"\n",
"property player1_matrixMatrix of player 1 choices (needed for stochastic two player games\n",
"\n",
"property rate_transitionsTrue iff the transition values (for Markovian choices) are interpreted as rates\n",
"\n",
"property reward_modelsReward models associated with the model\n",
"\n",
"property state_labelingThe state labeling\n",
"\n",
"property state_valuationsA list that stores for each state to which variable valuation it belongs\n",
"\n",
"property transition_matrixThe transition matrix\n",
"\n",
"class SparseModelStateState in sparse model\n",
"\n",
"property actionsGet actions\n",
"\n",
"property idId\n",
"\n",
"property labelsLabels\n",
"\n",
"class SparseModelStatesStates in sparse model\n",
"\n",
"class SparseParametricCtmcpCTMC in sparse representation\n",
"\n",
"class SparseParametricDtmcpDTMC in sparse representation\n",
"\n",
"class SparseParametricMApMA in sparse representation\n",
"\n",
"apply_schedulerself: stormpy.storage.storage.SparseParametricMAscheduler: storm::storage::Scheduler<carl::RationalFunction<carl::FactorizedPolynomial<carl::MultivariatePolynomial<cln::cl_RAcarl::MonomialComparator<&carl::Monomial::compareGradedLexicaltrue>carl::StdMultivariatePolynomialPolicies<carl::NoReasonscarl::NoAllocator> > >true> >drop_unreachable_states: bool=Truestormpy.storage.storage._SparseParametricModelapply scheduler\n",
"\n",
"property nondeterministic_choice_indicesclass SparseParametricMdppMDP in sparse representation\n",
"\n",
"apply_schedulerself: stormpy.storage.storage.SparseParametricMdpscheduler: storm::storage::Scheduler<carl::RationalFunction<carl::FactorizedPolynomial<carl::MultivariatePolynomial<cln::cl_RAcarl::MonomialComparator<&carl::Monomial::compareGradedLexicaltrue>carl::StdMultivariatePolynomialPolicies<carl::NoReasonscarl::NoAllocator> > >true> >drop_unreachable_states: bool=Truestormpy.storage.storage._SparseParametricModelapply scheduler\n",
"\n",
"property nondeterministic_choice_indicesclass SparseParametricModelActionAction for state in sparse parametric model\n",
"\n",
"property idId\n",
"\n",
"property transitionsGet transitions\n",
"\n",
"class SparseParametricModelActionsActions for state in sparse parametric model\n",
"\n",
"class SparseParametricModelStateState in sparse parametric model\n",
"\n",
"property actionsGet actions\n",
"\n",
"property idId\n",
"\n",
"property labelsLabels\n",
"\n",
"class SparseParametricModelStatesStates in sparse parametric model\n",
"\n",
"class SparseParametricPomdpPOMDP in sparse representation\n",
"\n",
"get_observationself: stormpy.storage.storage.SparseParametricPomdpstate: intintproperty nr_observationsproperty observationsclass SparseParametricRewardModelReward structure for parametric sparse models\n",
"\n",
"get_state_action_rewardself: stormpy.storage.storage.SparseParametricRewardModelarg0: intcarl::RationalFunction<carl::FactorizedPolynomial<carl::MultivariatePolynomial<cln::cl_RA, carl::MonomialComparator<&carl::Monomial::compareGradedLexical, true>, carl::StdMultivariatePolynomialPolicies<carl::NoReasons, carl::NoAllocator> > >, true>get_state_rewardself: stormpy.storage.storage.SparseParametricRewardModelarg0: intcarl::RationalFunction<carl::FactorizedPolynomial<carl::MultivariatePolynomial<cln::cl_RA, carl::MonomialComparator<&carl::Monomial::compareGradedLexical, true>, carl::StdMultivariatePolynomialPolicies<carl::NoReasons, carl::NoAllocator> > >, true>property has_state_action_rewardsproperty has_state_rewardsproperty has_transition_rewardsreduce_to_state_based_rewardsself: stormpy.storage.storage.SparseParametricRewardModeltransition_matrix: storm::storage::SparseMatrix<carl::RationalFunction<carl::FactorizedPolynomial<carl::MultivariatePolynomial<cln::cl_RAcarl::MonomialComparator<&carl::Monomial::compareGradedLexicaltrue>carl::StdMultivariatePolynomialPolicies<carl::NoReasonscarl::NoAllocator> > >true> >only_state_rewards: boolNoneReduce to state-based rewards\n",
"\n",
"property state_action_rewardsproperty state_rewardsproperty transition_rewardsclass SparsePomdpPOMDP in sparse representation\n",
"\n",
"get_observationself: stormpy.storage.storage.SparsePomdpstate: intintproperty nr_observationsproperty observationsclass SparseRewardModelReward structure for sparse models\n",
"\n",
"get_state_action_rewardself: stormpy.storage.storage.SparseRewardModelarg0: intfloatget_state_rewardself: stormpy.storage.storage.SparseRewardModelarg0: intfloatget_zero_reward_statesself: stormpy.storage.storage.SparseRewardModeltransition_matrix: storm::storage::SparseMatrix<double>stormpy.storage.storage.BitVectorget states where all rewards are zero\n",
"\n",
"property has_state_action_rewardsproperty has_state_rewardsproperty has_transition_rewardsreduce_to_state_based_rewardsself: stormpy.storage.storage.SparseRewardModeltransition_matrix: storm::storage::SparseMatrix<double>only_state_rewards: boolNoneReduce to state-based rewards\n",
"\n",
"property state_action_rewardsproperty state_rewardsproperty transition_rewardsclass StateLabelingLabeling for states\n",
"\n",
"add_label_to_stateself: stormpy.storage.storage.StateLabelinglabel: strstate: intNoneAdd label to state\n",
"\n",
"get_labels_of_stateself: stormpy.storage.storage.StateLabelingstate: intSet[str]Get labels of given state\n",
"\n",
"get_statesself: stormpy.storage.storage.StateLabelinglabel: strstormpy.storage.storage.BitVectorGet all states which have the given label\n",
"\n",
"has_state_labelself: stormpy.storage.storage.StateLabelinglabel: strstate: intboolCheck if the given state has the given label\n",
"\n",
"set_statesself: stormpy.storage.storage.StateLabelinglabel: strstates: stormpy.storage.storage.BitVectorNoneAdd a label to the given states\n",
"\n",
"class StateValuationValuations for explicit states\n",
"\n",
"get_boolean_valueself: stormpy.storage.storage.StateValuationstate: intvariable: storm::expressions::Variableboolget_integer_valueself: stormpy.storage.storage.StateValuationstate: intvariable: storm::expressions::Variableintget_jsonself: stormpy.storage.storage.StateValuationstate: intselected_variables: Optional[Set[storm::expressions::Variable]]=Nonestrget_nr_of_statesself: stormpy.storage.storage.StateValuationintget_rational_valueself: stormpy.storage.storage.StateValuationstate: intvariable: storm::expressions::Variable__gmp_expr<__mpq_struct [1], __mpq_struct [1]>get_stringself: stormpy.storage.storage.StateValuationstate: intpretty: bool=Trueselected_variables: Optional[Set[storm::expressions::Variable]]=Nonestrclass StateValuationsBuilderadd_stateself: stormpy.storage.storage.StateValuationsBuilder, state: int, boolean_values: List[bool]=[], integer_values: List[int]=[], rational_values: List[__gmp_expr<__mpq_struct [1], __mpq_struct [1]>]=[]NoneAdds a new state, no more variables should be added afterwards\n",
"\n",
"add_variableself: stormpy.storage.storage.StateValuationsBuildervariable: storm::expressions::VariableNoneAdds a new variable\n",
"\n",
"buildself: stormpy.storage.storage.StateValuationsBuilderarg0: intstormpy.storage.storage.StateValuationCreates the finalized state valuations object\n",
"\n",
"class SymbolicSylvanCtmcCTMC in symbolic representation\n",
"\n",
"class SymbolicSylvanDtmcDTMC in symbolic representation\n",
"\n",
"class SymbolicSylvanMAMA in symbolic representation\n",
"\n",
"class SymbolicSylvanMdpMDP in symbolic representation\n",
"\n",
"class SymbolicSylvanParametricCtmcpCTMC in symbolic representation\n",
"\n",
"class SymbolicSylvanParametricDtmcpDTMC in symbolic representation\n",
"\n",
"class SymbolicSylvanParametricMApMA in symbolic representation\n",
"\n",
"class SymbolicSylvanParametricMdppMDP in symbolic representation\n",
"\n",
"class SymbolicSylvanParametricRewardModelReward structure for parametric symbolic models\n",
"\n",
"property has_state_action_rewardsproperty has_state_rewardsproperty has_transition_rewardsclass SymbolicSylvanRewardModelReward structure for symbolic models\n",
"\n",
"property has_state_action_rewardsproperty has_state_rewardsproperty has_transition_rewardsclass VariableRepresents a variable\n",
"\n",
"get_expressionself: stormpy.storage.storage.Variablestorm::expressions::ExpressionGet expression from variable\n",
"\n",
"has_bitvector_typeself: stormpy.storage.storage.VariableboolCheck if the variable is of bitvector type\n",
"\n",
"has_boolean_typeself: stormpy.storage.storage.VariableboolCheck if the variable is of boolean type\n",
"\n",
"has_integer_typeself: stormpy.storage.storage.VariableboolCheck if the variable is of integer type\n",
"\n",
"has_numerical_typeself: stormpy.storage.storage.VariableboolCheck if the variable is of numerical type\n",
"\n",
"has_rational_typeself: stormpy.storage.storage.VariableboolCheck if the variable is of rational type\n",
"\n",
"property nameVariable name\n",
"\n",
"build_parametric_sparse_matrixarrayrow_group_indices=[]Build a sparse matrix from numpy array.\n",
"\n",
"\n",
"<dl style='margin: 20px 0;'>\n",
"<dt>Parameters</dt>\n",
"<dd>\n",
"- array (numpy) – The array. \n",
"- row_group_indices (List[double]) – List containing the starting row of each row group in ascending order. \n",
"\n",
"\n",
"</dd>\n",
"<dt>Returns</dt>\n",
"<dd>\n",
"Parametric sparse matrix.\n",
"\n",
"</dd>\n",
"\n",
"</dl>\n",
"\n",
"build_sparse_matrixarrayrow_group_indices=[]Build a sparse matrix from numpy array.\n",
"\n",
"\n",
"<dl style='margin: 20px 0;'>\n",
"<dt>Parameters</dt>\n",
"<dd>\n",
"- array (numpy) – The array. \n",
"- row_group_indices (List[double]) – List containing the starting row of each row group in ascending order. \n",
"\n",
"\n",
"</dd>\n",
"<dt>Returns</dt>\n",
"<dd>\n",
"Sparse matrix.\n",
"\n",
"</dd>\n",
"\n",
"</dl>\n",
"\n",
"collect_informationarg0: stormpy.storage.storage.JaniModelstormpy.storage.storage.JaniInformationObjecteliminate_reward_accumulationsmodel: stormpy.storage.storage.JaniModelproperties: List[stormpy.core.Property]List[stormpy.core.Property]Eliminate reward accumulations"
]
}
],
"metadata": {
"date": 1598178167.095977,
"filename": "storage.rst",
"kernelspec": {
"display_name": "Python",
"language": "python3",
"name": "python3"
},
"title": "Stormpy.storage"
},
"nbformat": 4,
"nbformat_minor": 4
}

7
doc/source/api/storage.rst
View File

@ -0,0 +1,7 @@
Stormpy.storage
**************************
.. automodule:: stormpy.storage
:members:
:undoc-members:
:imported-members:

53
doc/source/api/utility.ipynb
View File

@ -1,53 +0,0 @@
{
"cells": [
{
"cell_type": "markdown",
"metadata": {},
"source": [
"# Stormpy.utility\n",
"\n",
"class MatrixFormatI_Minus_P = MatrixFormat.I_Minus_PStraight = MatrixFormat.Straightclass ModelReferenceLightweight Wrapper around results\n",
"\n",
"get_boolean_valueself: stormpy.utility.utility.ModelReferencevariable: storm::expressions::Variableboolget a value for a boolean variable\n",
"\n",
"get_integer_valueself: stormpy.utility.utility.ModelReferencevariable: storm::expressions::Variableintget a value for an integer variable\n",
"\n",
"get_rational_valueself: stormpy.utility.utility.ModelReferencevariable: storm::expressions::Variablefloatget a value (as double) for an rational variable\n",
"\n",
"class Pathproperty distanceproperty predecessorKproperty predecessorNodeclass ShortestPathsGeneratorget_distanceself: stormpy.utility.utility.ShortestPathsGeneratork: intfloatget_path_as_listself: stormpy.utility.utility.ShortestPathsGeneratork: intList[int]get_statesself: stormpy.utility.utility.ShortestPathsGeneratork: intstorm::storage::BitVectorclass SmtCheckResultResult type\n",
"\n",
"Sat = SmtCheckResult.SatUnknown = SmtCheckResult.UnknownUnsat = SmtCheckResult.Unsatclass SmtSolverGeneric Storm SmtSolver Wrapper\n",
"\n",
"addself: stormpy.utility.utility.SmtSolverarg0: storm::expressions::ExpressionNoneaddconstraint\n",
"\n",
"checkself: stormpy.utility.utility.SmtSolverstormpy.utility.utility.SmtCheckResultcheck\n",
"\n",
"property modelget the model\n",
"\n",
"popself: stormpy.utility.utility.SmtSolverlevels: intNonepop\n",
"\n",
"pushself: stormpy.utility.utility.SmtSolverNonepush\n",
"\n",
"resetself: stormpy.utility.utility.SmtSolverNonereset\n",
"\n",
"class SmtSolverFactoryFactory for creating SMT Solvers\n",
"\n",
"class Z3SmtSolverz3 API for storm smtsolver wrapper\n",
"\n",
"class millisecondscountself: stormpy.utility.utility.millisecondsint"
]
}
],
"metadata": {
"date": 1598178167.1070933,
"filename": "utility.rst",
"kernelspec": {
"display_name": "Python",
"language": "python3",
"name": "python3"
},
"title": "Stormpy.utility"
},
"nbformat": 4,
"nbformat_minor": 4
}

7
doc/source/api/utility.rst
View File

@ -0,0 +1,7 @@
Stormpy.utility
**************************
.. automodule:: stormpy.utility
:members:
:undoc-members:
:imported-members:
Write Preview
Loading…
Cancel
Save