diff --git a/doc/source/reward_models.rst b/doc/source/reward_models.rst index 11956d1..8f12b20 100644 --- a/doc/source/reward_models.rst +++ b/doc/source/reward_models.rst @@ -22,6 +22,7 @@ We consider the die again, but with another property which talks about the expec >>> assert len(model.reward_models) == 1 The model now has a reward model, as the property talks about rewards. +When :doc:`building_models` from explicit sources, the reward model is always included if it is defined in the source. We can do model checking analogous to probabilities:: @@ -61,4 +62,3 @@ In this example, we only have state-action rewards. These rewards are a vector, 0.0 - diff --git a/examples/building_models/01-building-models.py b/examples/building_models/01-building-models.py index 68ee92d..2ecccbf 100644 --- a/examples/building_models/01-building-models.py +++ b/examples/building_models/01-building-models.py @@ -5,7 +5,7 @@ import stormpy.examples import stormpy.examples.files -def example_building_models(): +def example_building_models_01(): path = stormpy.examples.files.drn_ctmc_dft model = stormpy.build_model_from_drn(path) print(model.model_type) @@ -24,6 +24,5 @@ def example_building_models(): print("Number of states: {}".format(model.nr_states)) - if __name__ == '__main__': - example_building_models() \ No newline at end of file + example_building_models_01() \ No newline at end of file diff --git a/examples/building_models/02-building-models.py b/examples/building_models/02-building-models.py new file mode 100644 index 0000000..67cedec --- /dev/null +++ b/examples/building_models/02-building-models.py @@ -0,0 +1,56 @@ +import stormpy +import stormpy.core + +import stormpy.examples +import stormpy.examples.files + +import stormpy.info +import pycarl + +def example_building_models_02(): + + + import stormpy.pars + if stormpy.info.storm_ratfunc_use_cln(): + import pycarl.cln as pc + else: + import pycarl.gmp as pc + + def make_factorized_rf(var, cache): + num = pc.FactorizedPolynomial(pc.Polynomial(var), cache) + denom = pc.FactorizedPolynomial(pc.Rational(1)) + return pc.FactorizedRationalFunction(num, denom) + + # And the parametric + path = stormpy.examples.files.drn_pdtmc_die + model = stormpy.build_parametric_model_from_drn(path) + + + + + parameters = model.collect_probability_parameters() + bar_parameters = dict() + for p in parameters: + # Ensure that variables with that name are not recognized by pycarl. + assert pycarl.variable_with_name(p.name + "_bar").is_no_variable + bar_parameters[p] = pycarl.Variable(p.name + "_bar") + + substitutions = dict([[pc.Polynomial(1) - p, bar_parameters[p]] for p in parameters]) + print(substitutions) + + matrix = model.transition_matrix + for e in matrix: + val = e.value() + if val.is_constant(): + continue + val_pol = val.numerator.polynomial() + cache = val.numerator.cache() + for sub, repl in substitutions.items(): + if val_pol - sub == 0: + print("Found substitution") + e.set_value(make_factorized_rf(repl, cache)) + break # Assume only one substitution per entry + print(matrix) + +if __name__ == '__main__': + example_building_models_02() \ No newline at end of file diff --git a/examples/reward_models/01-reward-models.py b/examples/reward_models/01-reward-models.py index 47c586c..1ce13dc 100644 --- a/examples/reward_models/01-reward-models.py +++ b/examples/reward_models/01-reward-models.py @@ -24,7 +24,9 @@ def example_reward_models_01(): print(reward) assert not model.reward_models[reward_model_name].has_transition_rewards - + model = stormpy.build_parametric_model_from_drn(stormpy.examples.files.drn_pdtmc_die) + assert len(model.reward_models) == 1 + assert reward_model_name == "coin_flips" if __name__ == '__main__': example_reward_models_01() \ No newline at end of file diff --git a/lib/stormpy/__init__.py b/lib/stormpy/__init__.py index 93a83ad..8ffd318 100644 --- a/lib/stormpy/__init__.py +++ b/lib/stormpy/__init__.py @@ -137,11 +137,13 @@ def perform_bisimulation(model, properties, bisimulation_type): return core._perform_bisimulation(model, formulae, bisimulation_type) -def model_checking(model, property): +def model_checking(model, property, only_initial_states=False): """ Perform model checking on model for property. :param model: Model. :param property: Property to check for. + :param only_initial_states: If True, only results for initial states are computed. + If False, results for all states are computed. :return: Model checking result. :rtype: CheckResult """ @@ -151,10 +153,10 @@ def model_checking(model, property): formula = property if model.supports_parameters: - task = core.ParametricCheckTask(formula, False) + task = core.ParametricCheckTask(formula, only_initial_states) return core._parametric_model_checking_sparse_engine(model, task) else: - task = core.CheckTask(formula, False) + task = core.CheckTask(formula, only_initial_states) return core._model_checking_sparse_engine(model, task) diff --git a/lib/stormpy/examples/files/pdtmc/die.drn b/lib/stormpy/examples/files/pdtmc/die.drn index f1d0e3e..2f035a8 100644 --- a/lib/stormpy/examples/files/pdtmc/die.drn +++ b/lib/stormpy/examples/files/pdtmc/die.drn @@ -4,35 +4,35 @@ @parameters p q @reward_models - +coin_flips @nr_states 13 @model -state 0 init +state 0 init [1] action 0 1 : p 2 : (-1)*p+1 -state 1 +state 1 [1] action 0 3 : q 4 : (-1)*q+1 -state 2 +state 2 [1] action 0 5 : q 6 : (-1)*q+1 -state 3 +state 3 [1] action 0 1 : p 7 : (-1)*p+1 -state 4 +state 4 [1] action 0 8 : p 9 : (-1)*p+1 -state 5 +state 5 [1] action 0 2 : p 10 : (-1)*p+1 -state 6 +state 6 [1] action 0 11 : p 12 : (-1)*p+1 diff --git a/src/core/core.cpp b/src/core/core.cpp index 63a6107..d32af44 100644 --- a/src/core/core.cpp +++ b/src/core/core.cpp @@ -2,6 +2,7 @@ #include "storm/utility/initialize.h" #include "storm/utility/DirectEncodingExporter.h" #include "storm/storage/ModelFormulasPair.h" +#include "storm/solver/OptimizationDirection.h" void define_core(py::module& m) { // Init @@ -81,6 +82,13 @@ void define_build(py::module& m) { .def("set_build_with_choice_origins", &storm::builder::BuilderOptions::setBuildChoiceOrigins, "Build choice origins", py::arg("new_value")); } +void define_optimality_type(py::module& m) { + py::enum_(m, "OptimizationDirection") + .value("Minimize", storm::solver::OptimizationDirection::Minimize) + .value("Maximize", storm::solver::OptimizationDirection::Maximize) + ; +} + // Thin wrapper for exporting model template void exportDRN(std::shared_ptr> model, std::string const& file) { diff --git a/src/core/core.h b/src/core/core.h index b56aa28..51bc696 100644 --- a/src/core/core.h +++ b/src/core/core.h @@ -7,5 +7,6 @@ void define_core(py::module& m); void define_parse(py::module& m); void define_build(py::module& m); void define_export(py::module& m); +void define_optimality_type(py::module& m); #endif /* PYTHON_CORE_CORE_H_ */ diff --git a/src/logic/formulae.cpp b/src/logic/formulae.cpp index 072136f..d6d2dd8 100644 --- a/src/logic/formulae.cpp +++ b/src/logic/formulae.cpp @@ -22,6 +22,8 @@ void define_formulae(py::module& m) { py::class_>(m, "EventuallyFormula", "Formula for eventually", unaryPathFormula); py::class_>(m, "GloballyFormula", "Formula for globally", unaryPathFormula); py::class_> binaryPathFormula(m, "BinaryPathFormula", "Path formula with two operands", pathFormula); + binaryPathFormula.def_property_readonly("left_subformula", &storm::logic::BinaryPathFormula::getLeftSubformula); + binaryPathFormula.def_property_readonly("right_subformula", &storm::logic::BinaryPathFormula::getRightSubformula); py::class_>(m, "BoundedUntilFormula", "Until Formula with either a step or a time bound.", binaryPathFormula); py::class_>(m, "ConditionalFormula", "Formula with the right hand side being a condition.", formula); py::class_>(m, "UntilFormula", "Path Formula for unbounded until", binaryPathFormula); @@ -56,10 +58,8 @@ void define_formulae(py::module& m) { .def("set_bound", [](storm::logic::OperatorFormula& f, storm::logic::ComparisonType comparisonType, storm::expressions::Expression const& bound) { f.setBound(storm::logic::Bound(comparisonType, bound)); }, "Set bound", py::arg("comparison_type"), py::arg("bound")) - // the above method should be sufficient for now; reinstate the following if needed - //.def_property("_threshold_expression", &storm::logic::OperatorFormula::getThreshold, &storm::logic::OperatorFormula::setThreshold, "Threshold expression") - //.def_property_readonly("_threshold_as_rational", &storm::logic::OperatorFormula::getThresholdAs, "Rational threshold of bound, if applicable") - //.def_property_readonly("_threshold_expression_has_rational_type", [](storm::logic::OperatorFormula const& f) { return f.getThreshold().hasRationalType(); } , "Check expression type [without needing a Python expression object]") + .def_property_readonly("has_optimality_type", &storm::logic::OperatorFormula::hasOptimalityType, "Flag if an optimality type is present") + .def_property_readonly("optimality_type", &storm::logic::OperatorFormula::getOptimalityType, "Flag for the optimality type") ; py::class_>(m, "TimeOperator", "The time operator", operatorFormula); py::class_>(m, "LongRunAvarageOperator", "Long run average operator", operatorFormula); diff --git a/src/mod_core.cpp b/src/mod_core.cpp index f7f1140..9d58ab1 100644 --- a/src/mod_core.cpp +++ b/src/mod_core.cpp @@ -21,6 +21,7 @@ PYBIND11_MODULE(core, m) { define_property(m); define_parse(m); define_build(m); + define_optimality_type(m); define_export(m); define_result(m); define_modelchecking(m); diff --git a/src/pars/pla.cpp b/src/pars/pla.cpp index 92ab461..2afb288 100644 --- a/src/pars/pla.cpp +++ b/src/pars/pla.cpp @@ -3,23 +3,36 @@ #include "storm/api/storm.h" -typedef storm::modelchecker::SparseDtmcParameterLiftingModelChecker, double> SparseDtmcRegionChecker; +typedef storm::modelchecker::SparseDtmcParameterLiftingModelChecker, double> DtmcParameterLiftingModelChecker; +typedef storm::modelchecker::SparseMdpParameterLiftingModelChecker, double> MdpParameterLiftingModelChecker; + typedef storm::modelchecker::RegionModelChecker RegionModelChecker; typedef storm::storage::ParameterRegion Region; // Thin wrappers -std::shared_ptr createRegionChecker(storm::Environment const& env, std::shared_ptr> const& model, std::shared_ptr const& formula) { - return storm::api::initializeParameterLiftingRegionModelChecker(env, model, storm::api::createTask(formula, true)); +std::shared_ptr createRegionChecker(storm::Environment const& env, std::shared_ptr> const& model, std::shared_ptr const& formula, bool generateSplittingEstimate, bool allowModelSimplifications) { + return storm::api::initializeParameterLiftingRegionModelChecker(env, model, storm::api::createTask(formula, true), generateSplittingEstimate, allowModelSimplifications); +} + +void specify(std::shared_ptr& checker, storm::Environment const& env, std::shared_ptr> const& model, std::shared_ptr const& formula, bool generateSplittingEstimate, bool allowModelSimplifications) { + return checker->specify(env, model, storm::api::createTask(formula, true), generateSplittingEstimate, allowModelSimplifications); } storm::modelchecker::RegionResult checkRegion(std::shared_ptr& checker, storm::Environment const& env, Region const& region, storm::modelchecker::RegionResultHypothesis const& hypothesis, storm::modelchecker::RegionResult const& initialResult, bool sampleVertices) { return checker->analyzeRegion(env, region, hypothesis, initialResult, sampleVertices); } -storm::RationalFunction getBound(std::shared_ptr& checker, storm::Environment const& env, Region const& region, bool maximise) { +storm::RationalFunction getBoundAtInit(std::shared_ptr& checker, storm::Environment const& env, Region const& region, bool maximise) { return checker->getBoundAtInitState(env, region, maximise ? storm::solver::OptimizationDirection::Maximize : storm::solver::OptimizationDirection::Minimize); } +storm::modelchecker::ExplicitQuantitativeCheckResult getBound_dtmc(std::shared_ptr& checker, storm::Environment const& env, Region const& region, bool maximise) { + return checker->getBound(env, region, maximise ? storm::solver::OptimizationDirection::Maximize : storm::solver::OptimizationDirection::Minimize)->asExplicitQuantitativeCheckResult(); +} + +storm::modelchecker::ExplicitQuantitativeCheckResult getBound_mdp(std::shared_ptr& checker, storm::Environment const& env, Region const& region, bool maximise) { + return checker->getBound(env, region, maximise ? storm::solver::OptimizationDirection::Maximize : storm::solver::OptimizationDirection::Minimize)->asExplicitQuantitativeCheckResult(); +} std::set gatherDerivatives(storm::models::sparse::Model const& model, carl::Variable const& var) { std::set derivatives; @@ -66,20 +79,22 @@ void define_pla(py::module& m) { ; // RegionModelChecker - //py::class_>(m, "SparseDtmcRegionChecker", "Region model checker for sparse DTMCs") - py::class_>(m, "RegionModelChecker", "Region model checker via paramater lifting") -/* .def("__init__", [](std::unique_ptr& instance, std::shared_ptr> model, storm::modelchecker::CheckTask const& task) -> void { - // Better use storm::api::initializeParameterLiftingRegionModelChecker(model, task); - //SparseDtmcRegionChecker tmp; - //tmp.specify(model, task); - auto tmp = storm::api::initializeParameterLiftingRegionModelChecker(model, task); - new (&instance) std::unique_ptr(tmp); - }, py::arg("model"), py::arg("task")*/ - .def("check_region", &checkRegion, "Check region", py::arg("environment"), py::arg("region"), py::arg("hypothesis") = storm::modelchecker::RegionResultHypothesis::Unknown, py::arg("initialResult") = storm::modelchecker::RegionResult::Unknown, py::arg("sampleVertices") = false) - .def("get_bound", &getBound, "Get bound", py::arg("environment"), py::arg("region"), py::arg("maximise")= true); + + py::class_> regionModelChecker(m, "RegionModelChecker", "Region model checker via paramater lifting"); + regionModelChecker.def("check_region", &checkRegion, "Check region", py::arg("environment"), py::arg("region"), py::arg("hypothesis") = storm::modelchecker::RegionResultHypothesis::Unknown, py::arg("initialResult") = storm::modelchecker::RegionResult::Unknown, py::arg("sampleVertices") = false) + .def("get_bound", &getBoundAtInit, "Get bound", py::arg("environment"), py::arg("region"), py::arg("maximise")= true) + .def("specify", &specify, "specify arguments",py::arg("environment"), py::arg("model"), py::arg("formula"), py::arg("generate_splitting_estimate") = false, py::arg("allow_model_simplification") = true); ; - m.def("create_region_checker", &createRegionChecker, "Create region checker", py::arg("environment"), py::arg("model"), py::arg("formula")); + + py::class_>(m, "DtmcParameterLiftingModelChecker", "Region model checker for DTMCs", regionModelChecker) + .def(py::init<>()) + .def("get_bound_all_states", &getBound_dtmc, "Get bound", py::arg("environment"), py::arg("region"), py::arg("maximise")= true); + py::class_>(m, "MdpParameterLiftingModelChecker", "Region model checker for MPDs", regionModelChecker) + .def(py::init<>()) + .def("get_bound_all_states", &getBound_mdp, "Get bound", py::arg("environment"), py::arg("region"), py::arg("maximise")= true); + + m.def("create_region_checker", &createRegionChecker, "Create region checker", py::arg("environment"), py::arg("model"), py::arg("formula"), py::arg("generate_splitting_estimate") = false, py::arg("allow_model_simplification") = true); //m.def("is_parameter_lifting_sound", &storm::utility::parameterlifting::validateParameterLiftingSound, "Check if parameter lifting is sound", py::arg("model"), py::arg("formula")); m.def("gather_derivatives", &gatherDerivatives, "Gather all derivatives of transition probabilities", py::arg("model"), py::arg("var")); } diff --git a/src/storage/expressions.cpp b/src/storage/expressions.cpp index 87613f4..8f9dc34 100644 --- a/src/storage/expressions.cpp +++ b/src/storage/expressions.cpp @@ -46,6 +46,7 @@ void define_expressions(py::module& m) { .def("parse", &storm::parser::ExpressionParser::parseFromString, "parse") ; + py::class_(m, "ExpressionType", "The type of an expression") .def_property_readonly("is_boolean", &storm::expressions::Type::isBooleanType) .def_property_readonly("is_integer", &storm::expressions::Type::isIntegerType) diff --git a/src/storage/matrix.cpp b/src/storage/matrix.cpp index 0e09ffc..19b74d2 100644 --- a/src/storage/matrix.cpp +++ b/src/storage/matrix.cpp @@ -38,6 +38,9 @@ void define_sparse_matrix(py::module& m) { .def_property_readonly("nr_columns", &SparseMatrix::getColumnCount, "Number of columns") .def_property_readonly("nr_entries", &SparseMatrix::getEntryCount, "Number of non-zero entries") .def_property_readonly("_row_group_indices", &SparseMatrix::getRowGroupIndices, "Starting rows of row groups") + + .def("get_row_group_start", [](SparseMatrix& matrix, entry_index row) {return matrix.getRowGroupIndices()[row];}) + .def("get_row_group_end", [](SparseMatrix& matrix, entry_index row) {return matrix.getRowGroupIndices()[row+1];}) .def_property_readonly("has_trivial_row_grouping", &SparseMatrix::hasTrivialRowGrouping, "Trivial row grouping") .def("get_row", [](SparseMatrix& matrix, entry_index row) { return matrix.getRows(row, row+1); @@ -87,6 +90,8 @@ void define_sparse_matrix(py::module& m) { .def_property_readonly("nr_columns", &SparseMatrix::getColumnCount, "Number of columns") .def_property_readonly("nr_entries", &SparseMatrix::getEntryCount, "Number of non-zero entries") .def_property_readonly("_row_group_indices", &SparseMatrix::getRowGroupIndices, "Starting rows of row groups") + .def("get_row_group_start", [](SparseMatrix& matrix, entry_index row) {return matrix.getRowGroupIndices()[row];}) + .def("get_row_group_end", [](SparseMatrix& matrix, entry_index row) {return matrix.getRowGroupIndices()[row+1];}) .def_property_readonly("has_trivial_row_grouping", &SparseMatrix::hasTrivialRowGrouping, "Trivial row grouping") .def("get_row", [](SparseMatrix& matrix, entry_index row) { return matrix.getRows(row, row+1); diff --git a/src/storage/model.cpp b/src/storage/model.cpp index 167e003..ec3d43f 100644 --- a/src/storage/model.cpp +++ b/src/storage/model.cpp @@ -156,7 +156,9 @@ void define_model(py::module& m) { .def_property_readonly("has_transition_rewards", &RewardModel::hasTransitionRewards) .def_property_readonly("transition_rewards", [](RewardModel& rewardModel) {return rewardModel.getTransitionRewardMatrix();}) .def_property_readonly("state_rewards", [](RewardModel& rewardModel) {return rewardModel.getStateRewardVector();}) - .def_property_readonly("state_action_rewards", [](RewardModel& rewardModel) {return rewardModel.getStateActionRewardVector();}) + .def("get_state_reward", [](RewardModel& rewardModel, uint64_t state) {return rewardModel.getStateReward(state);}) + .def("get_state_action_reward", [](RewardModel& rewardModel, uint64_t action_index) {return rewardModel.getStateActionReward(action_index);}) + .def_property_readonly("state_action_rewards", [](RewardModel& rewardModel) {return rewardModel.getStateActionRewardVector();}) .def("reduce_to_state_based_rewards", [](RewardModel& rewardModel, SparseMatrix const& transitions, bool onlyStateRewards){return rewardModel.reduceToStateBasedRewards(transitions, onlyStateRewards);}, py::arg("transition_matrix"), py::arg("only_state_rewards"), "Reduce to state-based rewards") ; @@ -201,6 +203,9 @@ void define_model(py::module& m) { .def_property_readonly("has_transition_rewards", &RewardModel::hasTransitionRewards) .def_property_readonly("transition_rewards", [](RewardModel& rewardModel) {return rewardModel.getTransitionRewardMatrix();}) .def_property_readonly("state_rewards", [](RewardModel& rewardModel) {return rewardModel.getStateRewardVector();}) + .def("get_state_reward", [](RewardModel& rewardModel, uint64_t state) {return rewardModel.getStateReward(state);}) + .def("get_state_action_reward", [](RewardModel& rewardModel, uint64_t action_index) {return rewardModel.getStateActionReward(action_index);}) + .def_property_readonly("state_action_rewards", [](RewardModel& rewardModel) {return rewardModel.getStateActionRewardVector();}) .def("reduce_to_state_based_rewards", [](RewardModel& rewardModel, SparseMatrix const& transitions, bool onlyStateRewards){return rewardModel.reduceToStateBasedRewards(transitions, onlyStateRewards);}, py::arg("transition_matrix"), py::arg("only_state_rewards"), "Reduce to state-based rewards") ; diff --git a/src/storage/prism.cpp b/src/storage/prism.cpp index 508e2c6..c011fcc 100644 --- a/src/storage/prism.cpp +++ b/src/storage/prism.cpp @@ -3,6 +3,7 @@ #include "src/helpers.h" #include + using namespace storm::prism; void define_prism(py::module& m) { @@ -39,6 +40,7 @@ void define_prism(py::module& m) { .def_property_readonly("expression", &Assignment::getExpression, "Expression for the update"); + // PrismType py::enum_(m, "PrismModelType", "Type of the prism model") .value("DTMC", storm::prism::Program::ModelType::DTMC) @@ -57,4 +59,5 @@ void define_prism(py::module& m) { .def_property_readonly("variable", &Constant::getExpressionVariable, "Expression variable") ; + } \ No newline at end of file diff --git a/src/storage/state.cpp b/src/storage/state.cpp index fadd676..b13c887 100644 --- a/src/storage/state.cpp +++ b/src/storage/state.cpp @@ -17,12 +17,14 @@ void define_state(py::module& m) { .def_property_readonly("id", &SparseModelState::getIndex, "Id") .def_property_readonly("labels", &SparseModelState::getLabels, "Labels") .def_property_readonly("actions", &SparseModelState::getActions, "Get actions") + .def("__int__",&SparseModelState::getIndex) ; py::class_>(m, "SparseParametricModelState", "State in sparse parametric model") .def("__str__", &SparseModelState::toString) .def_property_readonly("id", &SparseModelState::getIndex, "Id") .def_property_readonly("labels", &SparseModelState::getLabels, "Labels") .def_property_readonly("actions", &SparseModelState::getActions, "Get actions") + .def("__int__",&SparseModelState::getIndex) ; // SparseModelActions diff --git a/tests/core/test_modelchecking.py b/tests/core/test_modelchecking.py index b0c1c1b..70b6ae5 100644 --- a/tests/core/test_modelchecking.py +++ b/tests/core/test_modelchecking.py @@ -69,6 +69,17 @@ class TestModelChecking: reference = [0.16666666666666663, 0.3333333333333333, 0, 0.6666666666666666, 0, 0, 0, 1, 0, 0, 0, 0, 0] assert all(map(math.isclose, result.get_values(), reference)) + def test_model_checking_only_initial(self): + program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm")) + formulas = stormpy.parse_properties_for_prism_program("Pmax=? [F{\"coin_flips\"}<=3 \"one\"]", program) + model = stormpy.build_model(program, formulas) + assert len(model.initial_states) == 1 + initial_state = model.initial_states[0] + assert initial_state == 0 + result = stormpy.model_checking(model, formulas[0], only_initial_states=True) + assert not result.result_for_all_states + assert math.isclose(result.at(initial_state), 0.125) + def test_model_checking_prob01(self): program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm")) formulaPhi = stormpy.parse_properties("true")[0] diff --git a/tests/pars/test_pla.py b/tests/pars/test_pla.py index 6336527..87a55d8 100644 --- a/tests/pars/test_pla.py +++ b/tests/pars/test_pla.py @@ -1,5 +1,6 @@ import stormpy import stormpy.logic +import math from helpers.helper import get_example_path from configurations import pars @@ -30,3 +31,69 @@ class TestPLA: region = stormpy.pars.ParameterRegion("0.1<=pL<=0.73,0.2<=pK<=0.715", parameters) result = checker.check_region(env, region) assert result == stormpy.pars.RegionResult.ALLVIOLATED + + def test_pla_bounds(self): + program = stormpy.parse_prism_program(get_example_path("pdtmc", "brp16_2.pm")) + prop = "P=? [F s=5 ]" + formulas = stormpy.parse_properties_for_prism_program(prop, program) + model = stormpy.build_parametric_model(program, formulas) + assert model.has_parameters + env = stormpy.Environment() + checker = stormpy.pars.create_region_checker(env, model, formulas[0].raw_formula) + parameters = model.collect_probability_parameters() + assert len(parameters) == 2 + region = stormpy.pars.ParameterRegion("0.7<=pL<=0.9,0.75<=pK<=0.95", parameters) + result = checker.get_bound(env, region, True) + assert math.isclose(float(result.constant_part()), 0.8369631383670559) + #result_vec = checker.get_bound_all_states(env, region, True) + #result = result_vec.at(model.initial_states[0]) + #assert math.isclose(float(result.constant_part()), 0.8369631383670559) + + def test_pla_manual(self): + program = stormpy.parse_prism_program(get_example_path("pdtmc", "brp16_2.pm")) + prop = "P=? [F s=5 ]" + formulas = stormpy.parse_properties_for_prism_program(prop, program) + model = stormpy.build_parametric_model(program, formulas) + assert model.has_parameters + env = stormpy.Environment() + checker = stormpy.pars.DtmcParameterLiftingModelChecker() + checker.specify(env, model, formulas[0].raw_formula) + parameters = model.collect_probability_parameters() + assert len(parameters) == 2 + region = stormpy.pars.ParameterRegion("0.7<=pL<=0.9,0.75<=pK<=0.95", parameters) + result = checker.get_bound(env, region, True) + assert math.isclose(float(result.constant_part()), 0.8369631383670559) + + def test_pla_manual_no_simplification(self): + program = stormpy.parse_prism_program(get_example_path("pdtmc", "brp16_2.pm")) + prop = "P=? [F s=5 ]" + formulas = stormpy.parse_properties_for_prism_program(prop, program) + model = stormpy.build_parametric_model(program, formulas) + assert model.has_parameters + env = stormpy.Environment() + checker = stormpy.pars.DtmcParameterLiftingModelChecker() + checker.specify(env, model, formulas[0].raw_formula, allow_model_simplification=False) + parameters = model.collect_probability_parameters() + assert len(parameters) == 2 + region = stormpy.pars.ParameterRegion("0.7<=pL<=0.9,0.75<=pK<=0.95", parameters) + result = checker.get_bound(env, region, True) + assert math.isclose(float(result.constant_part()), 0.836963056082918) + + def test_pla_state_bounds(self): + program = stormpy.parse_prism_program(get_example_path("pdtmc", "brp16_2.pm")) + prop = "P=? [F s=5 ]" + formulas = stormpy.parse_properties_for_prism_program(prop, program) + model = stormpy.build_parametric_model(program, formulas) + assert model.has_parameters + env = stormpy.Environment() + checker = stormpy.pars.DtmcParameterLiftingModelChecker() + checker.specify(env, model, formulas[0].raw_formula, allow_model_simplification=False) + parameters = model.collect_probability_parameters() + assert len(parameters) == 2 + region = stormpy.pars.ParameterRegion("0.7<=pL<=0.9,0.75<=pK<=0.95", parameters) + result_vec = checker.get_bound_all_states(env, region, True) + assert len(result_vec.get_values()) == model.nr_states + assert math.isclose(result_vec.at(model.initial_states[0]), 0.836963056082918) + + + diff --git a/travis/build.sh b/travis/build.sh index 9ac4fba..745305b 100755 --- a/travis/build.sh +++ b/travis/build.sh @@ -16,6 +16,7 @@ linux) docker exec stormpy mkdir opt/stormpy docker cp . stormpy:/opt/stormpy # Install virtualenv + docker exec stormpy apt-get update docker exec stormpy apt-get install -qq -y python python3 virtualenv set +e