From 8afa3529f4ae68116105cbd3e7e36e6e5d6b6a45 Mon Sep 17 00:00:00 2001 From: hannah Date: Wed, 7 Oct 2020 13:33:49 +0200 Subject: [PATCH] api rst files --- doc/source/api/core.ipynb | 1375 ------------------------------- doc/source/api/core.rst | 7 + doc/source/api/dft.ipynb | 99 --- doc/source/api/dft.rst | 7 + doc/source/api/exceptions.ipynb | 25 - doc/source/api/exceptions.rst | 7 + doc/source/api/gspn.ipynb | 384 --------- doc/source/api/gspn.rst | 7 + doc/source/api/info.ipynb | 34 - doc/source/api/info.rst | 7 + doc/source/api/logic.ipynb | 101 --- doc/source/api/logic.rst | 7 + doc/source/api/pars.ipynb | 110 --- doc/source/api/pars.rst | 7 + doc/source/api/storage.ipynb | 759 ----------------- doc/source/api/storage.rst | 7 + doc/source/api/utility.ipynb | 53 -- doc/source/api/utility.rst | 7 + 18 files changed, 63 insertions(+), 2940 deletions(-) delete mode 100644 doc/source/api/core.ipynb create mode 100644 doc/source/api/core.rst delete mode 100644 doc/source/api/dft.ipynb create mode 100644 doc/source/api/dft.rst delete mode 100644 doc/source/api/exceptions.ipynb create mode 100644 doc/source/api/exceptions.rst delete mode 100644 doc/source/api/gspn.ipynb create mode 100644 doc/source/api/gspn.rst delete mode 100644 doc/source/api/info.ipynb create mode 100644 doc/source/api/info.rst delete mode 100644 doc/source/api/logic.ipynb create mode 100644 doc/source/api/logic.rst delete mode 100644 doc/source/api/pars.ipynb create mode 100644 doc/source/api/pars.rst delete mode 100644 doc/source/api/storage.ipynb create mode 100644 doc/source/api/storage.rst delete mode 100644 doc/source/api/utility.ipynb create mode 100644 doc/source/api/utility.rst diff --git a/doc/source/api/core.ipynb b/doc/source/api/core.ipynb deleted file mode 100644 index 391aacf..0000000 --- a/doc/source/api/core.ipynb +++ /dev/null @@ -1,1375 +0,0 @@ -{ - "cells": [ - { - "cell_type": "markdown", - "metadata": {}, - "source": [ - "# Stormpy.core\n", - "\n", - "class AtomicExpressionFormulaFormula with an atomic expression\n", - "\n", - "class AtomicLabelFormulaFormula with an atomic label\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 BinaryPathFormulaPath formula with two operands\n", - "\n", - "property left_subformulaproperty right_subformulaclass BinaryStateFormulaState formula with two operands\n", - "\n", - "class BisimulationTypeTypes of bisimulation\n", - "\n", - "STRONG = BisimulationType.STRONGWEAK = BisimulationType.WEAKclass 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 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 BuilderOptionsOptions for building process\n", - "\n", - "property preserved_label_namesLabels preserved\n", - "\n", - "set_add_out_of_bounds_stateself: stormpy.core.BuilderOptionsnew_value: bool = Truestormpy.core.BuilderOptionsBuild with out of bounds state\n", - "\n", - "set_add_overlapping_guards_labelself: stormpy.core.BuilderOptionsnew_value: bool = Truestormpy.core.BuilderOptionsBuild with overlapping guards state labeled\n", - "\n", - "set_build_all_labelsself: stormpy.core.BuilderOptionsnew_value: bool = Truestormpy.core.BuilderOptionsBuild with all state labels\n", - "\n", - "set_build_all_reward_modelsself: stormpy.core.BuilderOptionsnew_value: bool = Truestormpy.core.BuilderOptionsBuild with all reward models\n", - "\n", - "set_build_choice_labelsself: stormpy.core.BuilderOptionsnew_value: bool = Truestormpy.core.BuilderOptionsBuild with choice labels\n", - "\n", - "set_build_state_valuationsself: stormpy.core.BuilderOptionsnew_value: bool = Truestormpy.core.BuilderOptionsBuild state valuations\n", - "\n", - "set_build_with_choice_originsself: stormpy.core.BuilderOptionsnew_value: bool = Truestormpy.core.BuilderOptionsBuild choice origins\n", - "\n", - "class CheckTaskTask for model checking\n", - "\n", - "set_produce_schedulersself: stormpy.core.CheckTaskproduce_schedulers: bool = TrueNoneSet whether schedulers should be produced (if possible)\n", - "\n", - "class 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 ComparisonTypeGEQ = ComparisonType.GEQGREATER = ComparisonType.GREATERLEQ = ComparisonType.LEQLESS = ComparisonType.LESSclass ConditionalFormulaFormula with the right hand side being a condition.\n", - "\n", - "class ConstraintCollectorCollector for constraints on parametric Markov chains\n", - "\n", - "property graph_preserving_constraintsGet the constraints ensuring the graph is preserved\n", - "\n", - "property wellformed_constraintsGet the constraints ensuring a wellformed model\n", - "\n", - "class CumulativeRewardFormulaSummed rewards over a the paths\n", - "\n", - "class 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 DirectEncodingOptionsproperty allow_placeholdersclass DirectEncodingParserOptionsOptions for the .drn parser\n", - "\n", - "property build_choice_labelsBuild with choice labels\n", - "\n", - "class DistributionDoubleFinite Support Distribution\n", - "\n", - "class EliminationLabelBehaviorBehavior of labels while eliminating non-Markovian chains\n", - "\n", - "DELETE_LABELS = EliminationLabelBehavior.DELETE_LABELSKEEP_LABELS = EliminationLabelBehavior.KEEP_LABELSMERGE_LABELS = EliminationLabelBehavior.MERGE_LABELSclass Environmentproperty solver_environmentsolver part of environment\n", - "\n", - "class EquationSolverTypeSolver type for equation systems\n", - "\n", - "eigen = EquationSolverType.eigenelimination = EquationSolverType.eliminationgmmxx = EquationSolverType.gmmxxnative = EquationSolverType.nativetopological = EquationSolverType.topologicalclass EventuallyFormulaFormula for eventually\n", - "\n", - "class ExplicitExactQuantitativeCheckResultExplicit exact quantitative model checking result\n", - "\n", - "atself: stormpy.core.ExplicitExactQuantitativeCheckResultstate: int__gmp_expr<__mpq_struct [1], __mpq_struct [1]>Get result for given state\n", - "\n", - "get_valuesself: stormpy.core.ExplicitExactQuantitativeCheckResultList[__gmp_expr<__mpq_struct [1], __mpq_struct [1]>]Get model checking result values for all states\n", - "\n", - "class ExplicitModelBuilder_DoubleModel builder for sparse models\n", - "\n", - "buildself: stormpy.core.ExplicitModelBuilder_Doublestorm::models::sparse::Model >Build the model\n", - "\n", - "export_lookupself: stormpy.core.ExplicitModelBuilder_Doublestorm::builder::ExplicitStateLookupExport a lookup model\n", - "\n", - "class ExplicitModelBuilder_RFModel builder for sparse models\n", - "\n", - "buildself: stormpy.core.ExplicitModelBuilder_RFstorm::models::sparse::Model, carl::StdMultivariatePolynomialPolicies > >, true>, storm::models::sparse::StandardRewardModel, carl::StdMultivariatePolynomialPolicies > >, true> > >Build the model\n", - "\n", - "export_lookupself: stormpy.core.ExplicitModelBuilder_RFstorm::builder::ExplicitStateLookupExport a lookup model\n", - "\n", - "class ExplicitParametricQuantitativeCheckResultExplicit parametric quantitative model checking result\n", - "\n", - "atself: stormpy.core.ExplicitParametricQuantitativeCheckResultstate: intcarl::RationalFunction, carl::StdMultivariatePolynomialPolicies > >, true>Get result for given state\n", - "\n", - "get_valuesself: stormpy.core.ExplicitParametricQuantitativeCheckResultList[carl::RationalFunction, carl::StdMultivariatePolynomialPolicies > >, true>]Get model checking result values for all states\n", - "\n", - "class ExplicitQualitativeCheckResultExplicit qualitative model checking result\n", - "\n", - "atself: stormpy.core.ExplicitQualitativeCheckResultstate: intboolGet result for given state\n", - "\n", - "get_truth_valuesself: stormpy.core.ExplicitQualitativeCheckResultstorm::storage::BitVectorGet BitVector representing the truth values\n", - "\n", - "class ExplicitQuantitativeCheckResultExplicit quantitative model checking result\n", - "\n", - "atself: stormpy.core.ExplicitQuantitativeCheckResultstate: intfloatGet result for given state\n", - "\n", - "get_valuesself: stormpy.core.ExplicitQuantitativeCheckResultList[float]Get model checking result values for all states\n", - "\n", - "property schedulerget scheduler\n", - "\n", - "class ExplicitStateLookupLookup model for states\n", - "\n", - "lookupself: stormpy.core.ExplicitStateLookup, state_description: Dict[storm::expressions::Variable, storm::expressions::Expression]intclass 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 FactorizedPolynomialRepresent a polynomial with its factorization\n", - "\n", - "cacheself: pycarl.cln.cln.FactorizedPolynomialpycarl.cln.cln._FactorizationCacheproperty coefficientconstant_partself: pycarl.cln.cln.FactorizedPolynomialpycarl.cln.cln.Rationalderiveself: pycarl.cln.cln.FactorizedPolynomialvariable: pycarl.core.Variablepycarl.cln.cln.FactorizedPolynomialCompute the derivative\n", - "\n", - "evaluateself: pycarl.cln.cln.FactorizedPolynomialarg0: Dict[pycarl.core.Variable, pycarl.cln.cln.Rational]pycarl.cln.cln.Rationalfactorizationself: pycarl.cln.cln.FactorizedPolynomialpycarl.cln.cln.FactorizationGet factorization\n", - "\n", - "gather_variablesself: pycarl.cln.cln.FactorizedPolynomialSet[pycarl.core.Variable]is_constantself: pycarl.cln.cln.FactorizedPolynomialboolis_oneself: pycarl.cln.cln.FactorizedPolynomialboolpolynomialself: pycarl.cln.cln.FactorizedPolynomialpycarl.cln.cln.PolynomialGet underlying polynomial\n", - "\n", - "to_smt2self: pycarl.cln.cln.FactorizedPolynomialstrclass FactorizedRationalFunctionRepresent a rational function, that is the fraction of two factorized polynomials\n", - "\n", - "constant_partself: pycarl.cln.cln.FactorizedRationalFunctionpycarl.cln.cln.Rationalproperty denominatorderiveself: pycarl.cln.cln.FactorizedRationalFunctionvariable: pycarl.core.Variablepycarl.cln.cln.FactorizedRationalFunctionCompute the derivative\n", - "\n", - "evaluateself: pycarl.cln.cln.FactorizedRationalFunctionarg0: Dict[pycarl.core.Variable, pycarl.cln.cln.Rational]pycarl.cln.cln.Rationalgather_variablesself: pycarl.cln.cln.FactorizedRationalFunctionSet[pycarl.core.Variable]is_constantself: pycarl.cln.cln.FactorizedRationalFunctionboolproperty numeratorrational_functionself: pycarl.cln.cln.FactorizedRationalFunctionpycarl.cln.cln.RationalFunctionto_smt2self: pycarl.cln.cln.FactorizedRationalFunctionstrclass FlatSetContainer to pass to program\n", - "\n", - "insertself: stormpy.core.FlatSetarg0: intNoneinsert_setself: stormpy.core.FlatSetarg0: stormpy.core.FlatSetNoneis_subset_ofself: stormpy.core.FlatSetarg0: stormpy.core.FlatSetboolclass 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 HybridExactQuantitativeCheckResultSymbolic exact hybrid quantitative model checking result\n", - "\n", - "get_valuesself: stormpy.core.HybridExactQuantitativeCheckResultList[__gmp_expr<__mpq_struct [1], __mpq_struct [1]>]Get model checking result values for all states\n", - "\n", - "class HybridParametricQuantitativeCheckResultSymbolic parametric hybrid quantitative model checking result\n", - "\n", - "get_valuesself: stormpy.core.HybridParametricQuantitativeCheckResultList[carl::RationalFunction, carl::StdMultivariatePolynomialPolicies > >, true>]Get model checking result values for all states\n", - "\n", - "class HybridQuantitativeCheckResultHybrid quantitative model checking result\n", - "\n", - "get_valuesself: stormpy.core.HybridQuantitativeCheckResultList[float]Get model checking result values for all states\n", - "\n", - "class InstantaneousRewardFormulaInstantaneous reward\n", - "\n", - "class 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.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 JaniModelTypeType of the Jani model\n", - "\n", - "CTMC = JaniModelType.CTMCCTMDP = JaniModelType.CTMDPDTMC = JaniModelType.DTMCHA = JaniModelType.HALTS = JaniModelType.LTSMA = JaniModelType.MAMDP = JaniModelType.MDPPHA = JaniModelType.PHAPTA = JaniModelType.PTASHA = JaniModelType.SHASTA = JaniModelType.STATA = JaniModelType.TAUNDEFINED = JaniModelType.UNDEFINEDclass 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 LongRunAvarageOperatorLong run average operator\n", - "\n", - "class LongRunAverageRewardFormulaLong run average reward\n", - "\n", - "class MinMaxMethodMethod for min-max equation systems\n", - "\n", - "interval_iteration = MinMaxMethod.interval_iterationlinear_programming = MinMaxMethod.linear_programmingoptimistic_value_iteration = MinMaxMethod.optimistic_value_iterationpolicy_iteration = MinMaxMethod.policy_iterationrational_search = MinMaxMethod.rational_searchsound_value_iteration = MinMaxMethod.sound_value_iterationtopological = MinMaxMethod.topologicaltopological_cuda = MinMaxMethod.topological_cudavalue_iteration = MinMaxMethod.value_iterationclass MinMaxSolverEnvironmentEnvironment for Min-Max-Solvers\n", - "\n", - "property methodproperty precisionclass ModelFormulasPairPair of model and formulas\n", - "\n", - "property formulasThe formulas\n", - "\n", - "property modelThe model\n", - "\n", - "class ModelTypeType of the model\n", - "\n", - "CTMC = ModelType.CTMCDTMC = ModelType.DTMCMA = ModelType.MAMDP = ModelType.MDPPOMDP = ModelType.POMDPclass NativeLinearEquationSolverMethodMethod for linear equation systems with the native solver\n", - "\n", - "SOR = NativeLinearEquationSolverMethod.SORgauss_seidel = NativeLinearEquationSolverMethod.gauss_seidelinterval_iteration = NativeLinearEquationSolverMethod.interval_iterationjacobi = NativeLinearEquationSolverMethod.jacobioptimistic_value_iteration = NativeLinearEquationSolverMethod.optimistic_value_iterationpower_iteration = NativeLinearEquationSolverMethod.power_iterationrational_search = NativeLinearEquationSolverMethod.rational_searchsound_value_iteration = NativeLinearEquationSolverMethod.sound_value_iterationwalker_chae = NativeLinearEquationSolverMethod.walker_chaeclass NativeSolverEnvironmentEnvironment for Native solvers\n", - "\n", - "property maximum_iterationsproperty methodclass 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 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 OptimizationDirectionMaximize = OptimizationDirection.MaximizeMinimize = OptimizationDirection.Minimizeclass ParametricCheckTaskTask for parametric model checking\n", - "\n", - "set_produce_schedulersself: stormpy.core.ParametricCheckTaskproduce_schedulers: bool = TrueNoneSet whether schedulers should be produced (if possible)\n", - "\n", - "class ParametricSparseMatrixParametric sparse matrix\n", - "\n", - "get_rowself: stormpy.storage.storage.ParametricSparseMatrixrow: intstorm::storage::SparseMatrix, carl::StdMultivariatePolynomialPolicies > >, 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::StdMultivariatePolynomialPolicies > >, 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::RationalFunctioncarl::StdMultivariatePolynomialPolicies > >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", - "
\n", - "
Parameters
\n", - "
\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](#stormpy.RationalFunction)) – The value that is to be set at the specified row and column \n", - "\n", - "\n", - "
\n", - "\n", - "
\n", - "\n", - "buildself: stormpy.storage.storage.ParametricSparseMatrixBuilderoverridden_row_count: int=0overridden_column_count: int=0overridden-row_group_count: int=0storm::storage::SparseMatrix, carl::StdMultivariatePolynomialPolicies > >, 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", - "
\n", - "
Parameters
\n", - "
\n", - "- const& replacements (std::vector) – 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", - "
\n", - "\n", - "
\n", - "\n", - "class ParametricSparseMatrixEntryEntry of parametric sparse matrix\n", - "\n", - "property columnColumn\n", - "\n", - "set_valueself: stormpy.storage.storage.ParametricSparseMatrixEntryvalue: carl::RationalFunctioncarl::StdMultivariatePolynomialPolicies > >true>NoneSet value\n", - "\n", - "valueself: stormpy.storage.storage.ParametricSparseMatrixEntrycarl::RationalFunction, carl::StdMultivariatePolynomialPolicies > >, true>Value\n", - "\n", - "class ParametricSparseMatrixRowsSet of rows in a parametric sparse matrix\n", - "\n", - "class PathFormulaFormula about the probability of a set of paths in an automaton\n", - "\n", - "class PolynomialRepresent a multivariate polynomial\n", - "\n", - "constant_partself: pycarl.cln.cln.Polynomialpycarl.cln.cln.Rationaldegreeself: pycarl.cln.cln.Polynomialarg0: pycarl.core.Variableintderiveself: pycarl.cln.cln.Polynomialvariable: pycarl.core.Variablepycarl.cln.cln.PolynomialCompute the derivative\n", - "\n", - "evaluateself: pycarl.cln.cln.Polynomialarg0: Dict[pycarl.core.Variable, pycarl.cln.cln.Rational]pycarl.cln.cln.Rationalgather_variablesself: pycarl.cln.cln.PolynomialSet[pycarl.core.Variable]is_constantself: pycarl.cln.cln.Polynomialboolproperty nr_termssubstituteself: pycarl.cln.cln.Polynomialarg0: Dict[pycarl.core.Variable, pycarl.cln.cln.Polynomial]pycarl.cln.cln.Polynomialto_smt2self: pycarl.cln.cln.Polynomialstrproperty total_degreeclass 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.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 ProbabilityOperatorProbability operator\n", - "\n", - "class Propertyproperty nameObtain the name of the property\n", - "\n", - "property raw_formulaObtain the formula directly\n", - "\n", - "class RationalClass wrapping gmp-rational numbers\n", - "\n", - "property denominatorproperty nominatorproperty numeratorclass RationalFunctionRepresent a rational function, that is the fraction of two multivariate polynomials\n", - "\n", - "constant_partself: pycarl.cln.cln.RationalFunctionpycarl.cln.cln.Rationalproperty denominatorderiveself: pycarl.cln.cln.RationalFunctionvariable: pycarl.core.Variablepycarl.cln.cln.RationalFunctionCompute the derivative\n", - "\n", - "evaluateself: pycarl.cln.cln.RationalFunctionarg0: Dict[pycarl.core.Variable, pycarl.cln.cln.Rational]pycarl.cln.cln.Rationalgather_variablesself: pycarl.cln.cln.RationalFunctionSet[pycarl.core.Variable]is_constantself: pycarl.cln.cln.RationalFunctionboolproperty nominatorproperty numeratorto_smt2self: pycarl.cln.cln.RationalFunctionstrRationalRFalias of `pycarl.cln.cln.Rational`\n", - "\n", - "class RewardOperatorReward operator\n", - "\n", - "has_reward_nameself: stormpy.logic.logic.RewardOperatorboolproperty reward_nameclass SMTCounterExampleGeneratorHighlevel Counterexample Generator with SMT as backend\n", - "\n", - "buildenv: stormpy.core.Environmentstats: stormpy.core.SMTCounterExampleGeneratorStatssymbolic_model: storm::storage::SymbolicModelDescriptionmodel: storm::models::sparse::Model >cex_input: storm::counterexamples::SMTMinimalLabelSetGenerator::CexInputdontcare: stormpy.core.FlatSetoptions: stormpy.core.SMTCounterExampleGeneratorOptionsList[stormpy.core.FlatSet]Compute counterexample\n", - "\n", - "precomputeenv: stormpy.core.Environmentsymbolic_model: storm::storage::SymbolicModelDescriptionmodel: storm::models::sparse::Model >formula: storm::logic::Formulastorm::counterexamples::SMTMinimalLabelSetGenerator::CexInputPrecompute input for counterexample generation\n", - "\n", - "class SMTCounterExampleGeneratorOptionsOptions for highlevel counterexample generation\n", - "\n", - "property add_backward_implication_cutsproperty check_threshold_feasibleproperty continue_after_first_counterexampleproperty encode_reachabilityproperty maximum_counterexamplesproperty maximum_iterations_after_counterexampleproperty silentproperty use_dynamic_constraintsclass SMTCounterExampleGeneratorStatsStats for highlevel counterexample generation\n", - "\n", - "property analysis_timeproperty cut_timeproperty iterationsproperty model_checking_timeproperty setup_timeproperty solver_timeclass SMTCounterExampleInputPrecomputed input for counterexample generation\n", - "\n", - "add_reward_and_thresholdself: stormpy.core.SMTCounterExampleInputreward_name: strthreshold: floatNoneadd another reward structure and threshold\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::DistributionGet 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::SchedulerChoiceproperty 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 SolverEnvironmentEnvironment for solvers\n", - "\n", - "property minmax_solver_environmentproperty native_solver_environmentset_force_soundself: stormpy.core.SolverEnvironmentnew_value: bool = TrueNoneforce soundness\n", - "\n", - "set_linear_equation_solver_typeself: stormpy.core.SolverEnvironmentnew_value: stormpy.core.EquationSolverTypeset_from_default: bool = FalseNoneset solver type to use\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::Schedulerdrop_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::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::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", - "
\n", - "
Parameters
\n", - "
\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", - "
\n", - "\n", - "
\n", - "\n", - "buildself: stormpy.storage.storage.SparseMatrixBuilderoverridden_row_count: int=0overridden_column_count: int=0overridden-row_group_count: int=0storm::storage::SparseMatrixFinalize 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", - "
\n", - "
Parameters
\n", - "
\n", - "- const& replacements (std::vector) – 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", - "
\n", - "\n", - "
\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::Schedulerdrop_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::Schedulercarl::StdMultivariatePolynomialPolicies > >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::Schedulercarl::StdMultivariatePolynomialPolicies > >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::StdMultivariatePolynomialPolicies > >, true>get_state_rewardself: stormpy.storage.storage.SparseParametricRewardModelarg0: intcarl::RationalFunction, carl::StdMultivariatePolynomialPolicies > >, true>property has_state_action_rewardsproperty has_state_rewardsproperty has_transition_rewardsreduce_to_state_based_rewardsself: stormpy.storage.storage.SparseParametricRewardModeltransition_matrix: storm::storage::SparseMatrixcarl::StdMultivariatePolynomialPolicies > >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::SparseMatrixstormpy.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::SparseMatrixonly_state_rewards: boolNoneReduce to state-based rewards\n", - "\n", - "property state_action_rewardsproperty state_rewardsproperty transition_rewardsclass StateFormulaFormula about a state of an automaton\n", - "\n", - "class 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", - "exception StormErrormessageBase class for exceptions in Storm.\n", - "\n", - "class SubsystemBuilderOptionsOptions for constructing the subsystem\n", - "\n", - "property build_action_mappingproperty build_kept_actionsproperty build_state_mappingproperty check_transitions_outsideclass SubsystemBuilderReturnTypeDoubleResult of the construction of a subsystem\n", - "\n", - "property kept_actionsActions of the subsystem available in the original system\n", - "\n", - "property modelthe submodel\n", - "\n", - "property new_to_old_action_mappingfor each action in result, the action index in the original model\n", - "\n", - "property new_to_old_state_mappingfor each state in result, the state index in the original model\n", - "\n", - "class SymbolicExactQuantitativeCheckResultSymbolic exact quantitative model checking result\n", - "\n", - "cloneself: stormpy.core.SymbolicExactQuantitativeCheckResultstormpy.core.SymbolicExactQuantitativeCheckResultclass SymbolicModelDescriptionSymbolic description of model\n", - "\n", - "as_jani_modelself: stormpy.core.SymbolicModelDescriptionstorm::jani::ModelReturn Jani model\n", - "\n", - "as_prism_programself: stormpy.core.SymbolicModelDescriptionstorm::prism::ProgramReturn Prism program\n", - "\n", - "instantiate_constantsself: stormpy.core.SymbolicModelDescription, constant_definitions: Dict[storm::expressions::Variable, storm::expressions::Expression]stormpy.core.SymbolicModelDescriptionInstantiate constants in symbolic model description\n", - "\n", - "property is_jani_modelFlag if program is in Jani format\n", - "\n", - "property is_prism_programFlag if program is in Prism format\n", - "\n", - "parse_constant_definitionsself: stormpy.core.SymbolicModelDescriptionString containing constants and their values: strDict[storm::expressions::Variable, storm::expressions::Expression]Parse given constant definitions\n", - "\n", - "class SymbolicParametricQuantitativeCheckResultSymbolic parametric quantitative model checking result\n", - "\n", - "cloneself: stormpy.core.SymbolicParametricQuantitativeCheckResultstormpy.core.SymbolicParametricQuantitativeCheckResultclass SymbolicQualitativeCheckResultSymbolic qualitative model checking result\n", - "\n", - "get_truth_valuesself: stormpy.core.SymbolicQualitativeCheckResultstorm::dd::Bdd<(storm::dd::DdType)1>Get Dd representing the truth values\n", - "\n", - "class SymbolicQuantitativeCheckResultSymbolic quantitative model checking result\n", - "\n", - "cloneself: stormpy.core.SymbolicQuantitativeCheckResultstormpy.core.SymbolicQuantitativeCheckResultclass 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 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\n", - "\n", - "class Variableproperty idproperty is_no_variableproperty nameproperty rankproperty typebuild_modelsymbolic_descriptionproperties=NoneBuild a model in sparse representation from a symbolic description.\n", - "\n", - "\n", - "
\n", - "
Parameters
\n", - "
\n", - "- symbolic_description – Symbolic model description to translate into a model. \n", - "- properties (List[[Property](#stormpy.Property)]) – List of properties that should be preserved during the translation. If None, then all properties are preserved. \n", - "\n", - "\n", - "
\n", - "
Returns
\n", - "
\n", - "Model in sparse representation.\n", - "\n", - "
\n", - "\n", - "
\n", - "\n", - "build_model_from_drnfileoptions=Build a model in sparse representation from the explicit DRN representation.\n", - "\n", - "\n", - "
\n", - "
Parameters
\n", - "
\n", - "- file (String) – DRN file containing the model. \n", - "- DirectEncodingParserOptions – Options for the parser. \n", - "\n", - "\n", - "
\n", - "
Returns
\n", - "
\n", - "Model in sparse representation.\n", - "\n", - "
\n", - "\n", - "
\n", - "\n", - "build_parametric_modelsymbolic_descriptionproperties=NoneBuild a parametric model in sparse representation from a symbolic description.\n", - "\n", - "\n", - "
\n", - "
Parameters
\n", - "
\n", - "- symbolic_description – Symbolic model description to translate into a model. \n", - "- properties (List[[Property](#stormpy.Property)]) – List of properties that should be preserved during the translation. If None, then all properties are preserved. \n", - "\n", - "\n", - "
\n", - "
Returns
\n", - "
\n", - "Parametric model in sparse representation.\n", - "\n", - "
\n", - "\n", - "
\n", - "\n", - "build_parametric_model_from_drnfileoptions=Build a parametric model in sparse representation from the explicit DRN representation.\n", - "\n", - "\n", - "
\n", - "
Parameters
\n", - "
\n", - "- file (String) – DRN file containing the model. \n", - "- DirectEncodingParserOptions – Options for the parser. \n", - "\n", - "\n", - "
\n", - "
Returns
\n", - "
\n", - "Parametric model in sparse representation.\n", - "\n", - "
\n", - "\n", - "
\n", - "\n", - "build_parametric_sparse_matrixarrayrow_group_indices=[]Build a sparse matrix from numpy array.\n", - "\n", - "\n", - "
\n", - "
Parameters
\n", - "
\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", - "
\n", - "
Returns
\n", - "
\n", - "Parametric sparse matrix.\n", - "\n", - "
\n", - "\n", - "
\n", - "\n", - "build_sparse_matrixarrayrow_group_indices=[]Build a sparse matrix from numpy array.\n", - "\n", - "\n", - "
\n", - "
Parameters
\n", - "
\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", - "
\n", - "
Returns
\n", - "
\n", - "Sparse matrix.\n", - "\n", - "
\n", - "\n", - "
\n", - "\n", - "build_sparse_modelsymbolic_descriptionproperties=NoneBuild a model in sparse representation from a symbolic description.\n", - "\n", - "\n", - "
\n", - "
Parameters
\n", - "
\n", - "- symbolic_description – Symbolic model description to translate into a model. \n", - "- properties (List[[Property](#stormpy.Property)]) – List of properties that should be preserved during the translation. If None, then all properties are preserved. \n", - "\n", - "\n", - "
\n", - "
Returns
\n", - "
\n", - "Model in sparse representation.\n", - "\n", - "
\n", - "\n", - "
\n", - "\n", - "build_sparse_model_from_explicittransition_file: strlabeling_file: strstate_reward_file: Optional[str] = ''transition_reward_file: Optional[str] = ''choice_labeling_file: Optional[str] = ''storm::models::sparse::Model >Build the model model from explicit input\n", - "\n", - "build_sparse_model_with_optionsmodel_description: storm::storage::SymbolicModelDescriptionoptions: storm::builder::BuilderOptionsuse_jit: bool=Falsedoctor: bool=Falsestorm::models::ModelBaseBuild the model in sparse representation\n", - "\n", - "build_sparse_parametric_modelsymbolic_descriptionproperties=NoneBuild a parametric model in sparse representation from a symbolic description.\n", - "\n", - "\n", - "
\n", - "
Parameters
\n", - "
\n", - "- symbolic_description – Symbolic model description to translate into a model. \n", - "- properties (List[[Property](#stormpy.Property)]) – List of properties that should be preserved during the translation. If None, then all properties are preserved. \n", - "\n", - "\n", - "
\n", - "
Returns
\n", - "
\n", - "Parametric model in sparse representation.\n", - "\n", - "
\n", - "\n", - "
\n", - "\n", - "build_sparse_parametric_model_with_optionsmodel_description: storm::storage::SymbolicModelDescriptionoptions: storm::builder::BuilderOptionsuse_jit: bool=Falsedoctor: bool=Falsestorm::models::ModelBaseBuild the model in sparse representation\n", - "\n", - "build_symbolic_modelsymbolic_descriptionproperties=NoneBuild a model in symbolic representation from a symbolic description.\n", - "\n", - "\n", - "
\n", - "
Parameters
\n", - "
\n", - "- symbolic_description – Symbolic model description to translate into a model. \n", - "- properties (List[[Property](#stormpy.Property)]) – List of properties that should be preserved during the translation. If None, then all properties are preserved. \n", - "\n", - "\n", - "
\n", - "
Returns
\n", - "
\n", - "Model in symbolic representation.\n", - "\n", - "
\n", - "\n", - "
\n", - "\n", - "build_symbolic_parametric_modelsymbolic_descriptionproperties=NoneBuild a parametric model in symbolic representation from a symbolic description.\n", - "\n", - "\n", - "
\n", - "
Parameters
\n", - "
\n", - "- symbolic_description – Symbolic model description to translate into a model. \n", - "- properties (List[[Property](#stormpy.Property)]) – List of properties that should be preserved during the translation. If None, then all properties are preserved. \n", - "\n", - "\n", - "
\n", - "
Returns
\n", - "
\n", - "Parametric model in symbolic representation.\n", - "\n", - "
\n", - "\n", - "
\n", - "\n", - "check_model_ddmodelpropertyonly_initial_states=Falseenvironment=Perform model checking using dd engine.\n", - ":param model: Model.\n", - ":param property: Property to check for.\n", - ":param only_initial_states: If True, only results for initial states are computed, otherwise for all states.\n", - ":return: Model checking result.\n", - ":rtype: CheckResult\n", - "\n", - "check_model_hybridmodelpropertyonly_initial_states=Falseenvironment=Perform model checking using hybrid engine.\n", - ":param model: Model.\n", - ":param property: Property to check for.\n", - ":param only_initial_states: If True, only results for initial states are computed, otherwise for all states.\n", - ":return: Model checking result.\n", - ":rtype: CheckResult\n", - "\n", - "check_model_sparsemodelpropertyonly_initial_states=Falseextract_scheduler=Falseenvironment=Perform model checking on model for property.\n", - ":param model: Model.\n", - ":param property: Property to check for.\n", - ":param only_initial_states: If True, only results for initial states are computed, otherwise for all states.\n", - ":param extract_scheduler: If True, try to extract a scheduler\n", - ":return: Model checking result.\n", - ":rtype: CheckResult\n", - "\n", - "collect_informationarg0: stormpy.storage.storage.JaniModelstormpy.storage.storage.JaniInformationObjectcompute_all_until_probabilitiesarg0: stormpy.core.Environmentarg1: stormpy.core.CheckTaskarg2: storm::models::sparse::Ctmc >arg3: storm::storage::BitVectorarg4: storm::storage::BitVectorList[float]Compute forward until probabilities\n", - "\n", - "compute_prob01_statesmodelphi_statespsi_statesCompute prob01 states for properties of the form phi_states until psi_states\n", - "\n", - "\n", - "
\n", - "
Parameters
\n", - "
\n", - "- model (SparseDTMC) – \n", - "- phi_states ([BitVector](#stormpy.BitVector)) – \n", - "- psi_states ([BitVector](#stormpy.BitVector)) – Target states \n", - "\n", - "\n", - "
\n", - "\n", - "
\n", - "\n", - "compute_prob01max_statesmodelphi_statespsi_statescompute_prob01min_statesmodelphi_statespsi_statescompute_transient_probabilitiesarg0: stormpy.core.Environmentarg1: storm::models::sparse::Ctmc >arg2: storm::storage::BitVectorarg3: storm::storage::BitVectorarg4: floatList[float]Compute transient probabilities\n", - "\n", - "construct_submodelmodelstatesactionskeep_unreachable_states=Trueoptions=\n", - "
\n", - "
Parameters
\n", - "
\n", - "- model – The model \n", - "- states – Which states should be preserved \n", - "- actions – Which actions should be preserved \n", - "- keep_unreachable_states – If False, run a reachability analysis. \n", - "\n", - "\n", - "
\n", - "
Returns
\n", - "
\n", - "A model with fewer states/actions\n", - "\n", - "
\n", - "\n", - "
\n", - "\n", - "create_filter_initial_states_sparsemodel: storm::models::sparse::Model >stormpy.core._QualitativeCheckResultCreate a filter for the initial states on a sparse model\n", - "\n", - "create_filter_initial_states_symbolicmodel: storm::models::symbolic::Model<(storm::dd::DdType)1double>stormpy.core._QualitativeCheckResultCreate a filter for the initial states on a symbolic model\n", - "\n", - "create_filter_symbolicmodel: storm::models::symbolic::Model<(storm::dd::DdType)1double>states: storm::expressions::Expressionstormpy.core._QualitativeCheckResultCreates a filter for the given states and a symbolic model\n", - "\n", - "eliminate_non_markovian_chainsmapropertieslabel_behaviorEliminate chains of non-Markovian states if possible.\n", - ":param ma: Markov automaton.\n", - ":param properties: List of properties to transform as well.\n", - ":param label_behavior: Behavior of labels while elimination.\n", - ":return: Tuple (converted MA, converted properties).\n", - "\n", - "eliminate_reward_accumulationsmodel: stormpy.storage.storage.JaniModelproperties: List[stormpy.core.Property]List[stormpy.core.Property]Eliminate reward accumulations\n", - "\n", - "export_parametric_to_drnmodel: storm::models::sparse::Modelcarl::StdMultivariatePolynomialPolicies > >true>storm::models::sparse::StandardRewardModelcarl::StdMultivariatePolynomialPolicies > >true> > >file: stroptions: stormpy.core.DirectEncodingOptions=NoneExport parametric model in DRN format\n", - "\n", - "export_to_drnmodel: storm::models::sparse::Model >file: stroptions: stormpy.core.DirectEncodingOptions=NoneExport model in DRN format\n", - "\n", - "make_sparse_model_buildermodel_description: storm::storage::SymbolicModelDescriptionoptions: storm::builder::BuilderOptionsstorm::builder::ExplicitModelBuilder, unsigned int>Construct a builder instance\n", - "\n", - "make_sparse_model_builder_parametricmodel_description: storm::storage::SymbolicModelDescriptionoptions: storm::builder::BuilderOptionsstorm::builder::ExplicitModelBuilder, unsigned int>Construct a builder instance\n", - "\n", - "model_checkingmodelpropertyonly_initial_states=Falseextract_scheduler=Falseenvironment=Perform model checking on model for property.\n", - ":param model: Model.\n", - ":param property: Property to check for.\n", - ":param only_initial_states: If True, only results for initial states are computed, otherwise for all states.\n", - ":param extract_scheduler: If True, try to extract a scheduler\n", - ":return: Model checking result.\n", - ":rtype: CheckResult\n", - "\n", - "parse_jani_modelpath: strTuple[storm::jani::Model, List[stormpy.core.Property]]Parse Jani model\n", - "\n", - "parse_prism_programpath: strprism_compat: bool = Falsesimplify: bool = Truestorm::prism::ProgramParse Prism program\n", - "\n", - "parse_propertiespropertiescontext=Nonefilters=None\n", - "
\n", - "
Parameters
\n", - "
\n", - "- properties – A string with the pctl properties \n", - "- context – A symbolic model that gives meaning to variables and constants. \n", - "- filters – filters, if applicable. \n", - "\n", - "\n", - "
\n", - "
Returns
\n", - "
\n", - "A list of properties\n", - "\n", - "
\n", - "\n", - "
\n", - "\n", - "parse_properties_for_jani_modelformula_string: strjani_model: storm::jani::Modelproperty_filter: Optional[Set[str]]=NoneList[stormpy.core.Property]parse_properties_for_prism_programformula_string: strprism_program: storm::prism::Programproperty_filter: Optional[Set[str]]=NoneList[stormpy.core.Property]Parses properties given in the prism format, allows references to variables in the prism program.\n", - "\n", - "\n", - "
\n", - "
Parameters
\n", - "
\n", - "- formula_str (str) – A string of formulas \n", - "- prism_program ([PrismProgram](#stormpy.PrismProgram)) – A prism program \n", - "- property_filter (str) – A filter \n", - "\n", - "\n", - "
\n", - "
Returns
\n", - "
\n", - "A list of properties\n", - "\n", - "
\n", - "\n", - "
\n", - "\n", - "parse_properties_without_contextformula_string: strproperty_filter: Optional[Set[str]] = NoneList[stormpy.core.Property]Parse properties given in the prism format.\n", - "\n", - "\n", - "
\n", - "
Parameters
\n", - "
\n", - "- formula_str (str) – A string of formulas \n", - "- property_filter (str) – A filter \n", - "\n", - "\n", - "
\n", - "
Returns
\n", - "
\n", - "A list of properties\n", - "\n", - "
\n", - "\n", - "
\n", - "\n", - "perform_bisimulationmodelpropertiesbisimulation_typePerform bisimulation on model.\n", - ":param model: Model.\n", - ":param properties: Properties to preserve during bisimulation.\n", - ":param bisimulation_type: Type of bisimulation (weak or strong).\n", - ":return: Model after bisimulation.\n", - "\n", - "perform_sparse_bisimulationmodelpropertiesbisimulation_typePerform bisimulation on model in sparse representation.\n", - ":param model: Model.\n", - ":param properties: Properties to preserve during bisimulation.\n", - ":param bisimulation_type: Type of bisimulation (weak or strong).\n", - ":return: Model after bisimulation.\n", - "\n", - "perform_symbolic_bisimulationmodelpropertiesPerform bisimulation on model in symbolic representation.\n", - ":param model: Model.\n", - ":param properties: Properties to preserve during bisimulation.\n", - ":return: Model after bisimulation.\n", - "\n", - "preprocess_symbolic_inputsymbolic_model_description: storm::storage::SymbolicModelDescription, properties: List[stormpy.core.Property], constant_definition_string: strTuple[storm::storage::SymbolicModelDescription, List[stormpy.core.Property]]Preprocess symoblic input\n", - "\n", - "prob01max_statesmodeleventually_formulaprob01min_statesmodeleventually_formulaset_settingsarguments: List[str]NoneSet settings\n", - "\n", - "topological_sortmodelforward=Trueinitial=[]\n", - "
\n", - "
Parameters
\n", - "
\n", - "- model – \n", - "- forward – \n", - "\n", - "\n", - "
\n", - "
Returns
\n", - "
\n", - "\n", - "\n", - "
\n", - "\n", - "
\n", - "\n", - "transform_to_discrete_time_modelmodelpropertiesTransform continuous-time model to discrete time model.\n", - ":param model: Continuous-time model.\n", - ":param properties: List of properties to transform as well.\n", - ":return: Tuple (Discrete-time model, converted properties).\n", - "\n", - "transform_to_sparse_modelmodelTransform model in symbolic representation into model in sparse representation.\n", - ":param model: Symbolic model.\n", - ":return: Sparse model." - ] - } - ], - "metadata": { - "date": 1598178166.5084927, - "filename": "core.rst", - "kernelspec": { - "display_name": "Python", - "language": "python3", - "name": "python3" - }, - "title": "Stormpy.core" - }, - "nbformat": 4, - "nbformat_minor": 4 -} \ No newline at end of file diff --git a/doc/source/api/core.rst b/doc/source/api/core.rst new file mode 100644 index 0000000..b9a41a1 --- /dev/null +++ b/doc/source/api/core.rst @@ -0,0 +1,7 @@ +Stormpy.core +************************** + +.. automodule:: stormpy + :members: + :undoc-members: + :imported-members: diff --git a/doc/source/api/dft.ipynb b/doc/source/api/dft.ipynb deleted file mode 100644 index b44e9b3..0000000 --- a/doc/source/api/dft.ipynb +++ /dev/null @@ -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 -} \ No newline at end of file diff --git a/doc/source/api/dft.rst b/doc/source/api/dft.rst new file mode 100644 index 0000000..331f60c --- /dev/null +++ b/doc/source/api/dft.rst @@ -0,0 +1,7 @@ +Stormpy.dft +************************** + +.. automodule:: stormpy.dft + :members: + :undoc-members: + :imported-members: diff --git a/doc/source/api/exceptions.ipynb b/doc/source/api/exceptions.ipynb deleted file mode 100644 index 37975e0..0000000 --- a/doc/source/api/exceptions.ipynb +++ /dev/null @@ -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 -} \ No newline at end of file diff --git a/doc/source/api/exceptions.rst b/doc/source/api/exceptions.rst new file mode 100644 index 0000000..8a3e2b2 --- /dev/null +++ b/doc/source/api/exceptions.rst @@ -0,0 +1,7 @@ +Stormpy.exceptions +************************** + +.. automodule:: stormpy.exceptions + :members: + :undoc-members: + :imported-members: diff --git a/doc/source/api/gspn.ipynb b/doc/source/api/gspn.ipynb deleted file mode 100644 index 65cb570..0000000 --- a/doc/source/api/gspn.ipynb +++ /dev/null @@ -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::ImmediateTransitionReturns the immediate transition with the corresponding name\n", - "\n", - "get_immediate_transitionsself: stormpy.gspn.gspn.GSPNList[storm::gspn::ImmediateTransition]> Returns the immediate transitions of this GSPN.\n", - "\n", - "\n", - "\n", - "
\n", - "
Return type
\n", - "
\n", - "list[stormpy.ImmediateTransition]\n", - "\n", - "
\n", - "\n", - "
\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", - "
\n", - "
param uint64_t id
\n", - "
\n", - " The ID of the place. \n", - "
\n", - "
rtype
\n", - "
\n", - " stormpy.Place \n", - "
\n", - " \n", - "
\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", - "
\n", - "
Return type
\n", - "
\n", - "list[stormpy.Place]\n", - "\n", - "
\n", - "\n", - "
\n", - "\n", - "get_timed_transitionself: stormpy.gspn.gspn.GSPNname: strstorm::gspn::TimedTransitionReturns the timed transition with the corresponding name\n", - "\n", - "get_timed_transitionsself: stormpy.gspn.gspn.GSPNList[storm::gspn::TimedTransition]> Returns a vector of the timed transitions of this GSPN.\n", - "\n", - "\n", - "\n", - "
\n", - "
Return type
\n", - "
\n", - "list[stormpy.TimedTransition]\n", - "\n", - "
\n", - "\n", - "
\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", - "
\n", - "
param from
\n", - "
\n", - " The ID or name of the place from which the arc is originating. \n", - "
\n", - "
type from
\n", - "
\n", - " uint_64_t or str \n", - "
\n", - "
param to
\n", - "
\n", - " The ID or name of the transition to which the arc goes to. \n", - "
\n", - "
type to
\n", - "
\n", - " uint_64_t or str \n", - "
\n", - "
param uint64_t multiplicity
\n", - "
\n", - " The multiplicity of the arc, default = 1. \n", - "
\n", - " \n", - "
\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", - "
\n", - "
param from
\n", - "
\n", - " The ID or name of the place from which the arc is originating. \n", - "
\n", - "
type from
\n", - "
\n", - " uint_64_t or str \n", - "
\n", - "
param uint_64_t to
\n", - "
\n", - " The ID or name of the transition to which the arc goes to. \n", - "
\n", - "
type from
\n", - "
\n", - " uint_64_t or str \n", - "
\n", - "
param uint64_t multiplicity
\n", - "
\n", - " The multiplicity of the arc, default = 1. \n", - "
\n", - " \n", - "
\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", - "
\n", - "
Parameters
\n", - "
\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", - "
\n", - "\n", - "
\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", - "
\n", - "
param from
\n", - "
\n", - " The ID or name of the transition from which the arc is originating. \n", - "
\n", - "
type from
\n", - "
\n", - " uint_64_t or str \n", - "
\n", - "
param to
\n", - "
\n", - " The ID or name of the place to which the arc goes to. \n", - "
\n", - "
type to
\n", - "
\n", - " uint_64_t or str \n", - "
\n", - "
param uint64_t multiplicity
\n", - "
\n", - " The multiplicity of the arc, default = 1. \n", - "
\n", - " \n", - "
\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", - "
\n", - "
Parameters
\n", - "
\n", - "- id (uint64_t) – The ID of the place. \n", - "- layout_info (stormpy.LayoutInfo) – The layout information. \n", - "\n", - "\n", - "
\n", - "\n", - "
\n", - "\n", - "set_transition_layout_infoself: stormpy.gspn.gspn.GSPNBuildertransition_id: intlayout_info: storm::gspn::LayoutInfoNone> Set transition layout information.\n", - "\n", - "\n", - "\n", - "
\n", - "
Parameters
\n", - "
\n", - "- id (uint64_t) – The ID of the transition. \n", - "- layout_info (stormpy.LayoutInfo) – The layout information. \n", - "\n", - "\n", - "
\n", - "\n", - "
\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 -} \ No newline at end of file diff --git a/doc/source/api/gspn.rst b/doc/source/api/gspn.rst new file mode 100644 index 0000000..d752360 --- /dev/null +++ b/doc/source/api/gspn.rst @@ -0,0 +1,7 @@ +Stormpy.gspn +************************** + +.. automodule:: stormpy.gspn + :members: + :undoc-members: + :imported-members: diff --git a/doc/source/api/info.ipynb b/doc/source/api/info.ipynb deleted file mode 100644 index 2f83a2b..0000000 --- a/doc/source/api/info.ipynb +++ /dev/null @@ -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 -} \ No newline at end of file diff --git a/doc/source/api/info.rst b/doc/source/api/info.rst new file mode 100644 index 0000000..8421b2b --- /dev/null +++ b/doc/source/api/info.rst @@ -0,0 +1,7 @@ +Stormpy.info +************************** + +.. automodule:: stormpy.info + :members: + :undoc-members: + :imported-members: diff --git a/doc/source/api/logic.ipynb b/doc/source/api/logic.ipynb deleted file mode 100644 index 3e09b4f..0000000 --- a/doc/source/api/logic.ipynb +++ /dev/null @@ -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 -} \ No newline at end of file diff --git a/doc/source/api/logic.rst b/doc/source/api/logic.rst new file mode 100644 index 0000000..84d34a9 --- /dev/null +++ b/doc/source/api/logic.rst @@ -0,0 +1,7 @@ +Stormpy.logic +************************** + +.. automodule:: stormpy.logic + :members: + :undoc-members: + :imported-members: diff --git a/doc/source/api/pars.ipynb b/doc/source/api/pars.ipynb deleted file mode 100644 index 449d116..0000000 --- a/doc/source/api/pars.ipynb +++ /dev/null @@ -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 -} \ No newline at end of file diff --git a/doc/source/api/pars.rst b/doc/source/api/pars.rst new file mode 100644 index 0000000..2c66395 --- /dev/null +++ b/doc/source/api/pars.rst @@ -0,0 +1,7 @@ +Stormpy.pars +************************** + +.. automodule:: stormpy.pars + :members: + :undoc-members: + :imported-members: diff --git a/doc/source/api/storage.ipynb b/doc/source/api/storage.ipynb deleted file mode 100644 index 85fc184..0000000 --- a/doc/source/api/storage.ipynb +++ /dev/null @@ -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.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::StdMultivariatePolynomialPolicies > >, 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::StdMultivariatePolynomialPolicies > >, 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::RationalFunctioncarl::StdMultivariatePolynomialPolicies > >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", - "
\n", - "
Parameters
\n", - "
\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", - "
\n", - "\n", - "
\n", - "\n", - "buildself: stormpy.storage.storage.ParametricSparseMatrixBuilderoverridden_row_count: int=0overridden_column_count: int=0overridden-row_group_count: int=0storm::storage::SparseMatrix, carl::StdMultivariatePolynomialPolicies > >, 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", - "
\n", - "
Parameters
\n", - "
\n", - "- const& replacements (std::vector) – 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", - "
\n", - "\n", - "
\n", - "\n", - "class ParametricSparseMatrixEntryEntry of parametric sparse matrix\n", - "\n", - "property columnColumn\n", - "\n", - "set_valueself: stormpy.storage.storage.ParametricSparseMatrixEntryvalue: carl::RationalFunctioncarl::StdMultivariatePolynomialPolicies > >true>NoneSet value\n", - "\n", - "valueself: stormpy.storage.storage.ParametricSparseMatrixEntrycarl::RationalFunction, carl::StdMultivariatePolynomialPolicies > >, 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.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::DistributionGet 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::SchedulerChoiceproperty 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::Schedulerdrop_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::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::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", - "
\n", - "
Parameters
\n", - "
\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", - "
\n", - "\n", - "
\n", - "\n", - "buildself: stormpy.storage.storage.SparseMatrixBuilderoverridden_row_count: int=0overridden_column_count: int=0overridden-row_group_count: int=0storm::storage::SparseMatrixFinalize 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", - "
\n", - "
Parameters
\n", - "
\n", - "- const& replacements (std::vector) – 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", - "
\n", - "\n", - "
\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::Schedulerdrop_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::Schedulercarl::StdMultivariatePolynomialPolicies > >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::Schedulercarl::StdMultivariatePolynomialPolicies > >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::StdMultivariatePolynomialPolicies > >, true>get_state_rewardself: stormpy.storage.storage.SparseParametricRewardModelarg0: intcarl::RationalFunction, carl::StdMultivariatePolynomialPolicies > >, true>property has_state_action_rewardsproperty has_state_rewardsproperty has_transition_rewardsreduce_to_state_based_rewardsself: stormpy.storage.storage.SparseParametricRewardModeltransition_matrix: storm::storage::SparseMatrixcarl::StdMultivariatePolynomialPolicies > >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::SparseMatrixstormpy.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::SparseMatrixonly_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", - "
\n", - "
Parameters
\n", - "
\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", - "
\n", - "
Returns
\n", - "
\n", - "Parametric sparse matrix.\n", - "\n", - "
\n", - "\n", - "
\n", - "\n", - "build_sparse_matrixarrayrow_group_indices=[]Build a sparse matrix from numpy array.\n", - "\n", - "\n", - "
\n", - "
Parameters
\n", - "
\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", - "
\n", - "
Returns
\n", - "
\n", - "Sparse matrix.\n", - "\n", - "
\n", - "\n", - "
\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 -} \ No newline at end of file diff --git a/doc/source/api/storage.rst b/doc/source/api/storage.rst new file mode 100644 index 0000000..5281904 --- /dev/null +++ b/doc/source/api/storage.rst @@ -0,0 +1,7 @@ +Stormpy.storage +************************** + +.. automodule:: stormpy.storage + :members: + :undoc-members: + :imported-members: diff --git a/doc/source/api/utility.ipynb b/doc/source/api/utility.ipynb deleted file mode 100644 index 60b0946..0000000 --- a/doc/source/api/utility.ipynb +++ /dev/null @@ -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 -} \ No newline at end of file diff --git a/doc/source/api/utility.rst b/doc/source/api/utility.rst new file mode 100644 index 0000000..6bfe305 --- /dev/null +++ b/doc/source/api/utility.rst @@ -0,0 +1,7 @@ +Stormpy.utility +************************** + +.. automodule:: stormpy.utility + :members: + :undoc-members: + :imported-members: