From cfb6dfbf2f9b7bcf7ead1bc5c1ef220b8ae7f7be Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Fri, 18 May 2018 11:53:00 +0200 Subject: [PATCH] Better naming for sparse model building --- lib/stormpy/__init__.py | 10 +++++----- src/core/core.cpp | 16 ++++++++-------- src/core/core.h | 7 ++----- tests/storage/test_model.py | 14 ++------------ 4 files changed, 17 insertions(+), 30 deletions(-) diff --git a/lib/stormpy/__init__.py b/lib/stormpy/__init__.py index 883cc2c..0720ee3 100644 --- a/lib/stormpy/__init__.py +++ b/lib/stormpy/__init__.py @@ -22,6 +22,7 @@ except ImportError: core._set_up("") + def _convert_sparse_model(model, parametric=False): """ Convert (parametric) model in sparse representation into model corresponding to exact model type. @@ -68,9 +69,9 @@ def build_model(symbolic_description, properties=None): if properties: formulae = [prop.raw_formula for prop in properties] - intermediate = core._build_sparse_model_from_prism_program(symbolic_description, formulae) + intermediate = core._build_sparse_model_from_symbolic_description(symbolic_description, formulae) else: - intermediate = core._build_sparse_model_from_prism_program(symbolic_description) + intermediate = core._build_sparse_model_from_symbolic_description(symbolic_description) return _convert_sparse_model(intermediate, parametric=False) @@ -87,9 +88,9 @@ def build_parametric_model(symbolic_description, properties=None): if properties: formulae = [prop.raw_formula for prop in properties] - intermediate = core._build_sparse_parametric_model_from_prism_program(symbolic_description, formulae) + intermediate = core._build_sparse_parametric_model_from_symbolic_description(symbolic_description, formulae) else: - intermediate = core._build_sparse_parametric_model_from_prism_program(symbolic_description) + intermediate = core._build_sparse_parametric_model_from_symbolic_description(symbolic_description) return _convert_sparse_model(intermediate, parametric=True) @@ -115,7 +116,6 @@ def build_parametric_model_from_drn(file): return _convert_sparse_model(intermediate, parametric=True) - def perform_bisimulation(model, properties, bisimulation_type): """ Perform bisimulation on model. diff --git a/src/core/core.cpp b/src/core/core.cpp index b4b5de6..e0e4af4 100644 --- a/src/core/core.cpp +++ b/src/core/core.cpp @@ -46,9 +46,9 @@ void define_parse(py::module& m) { ; } -// Thin wrapper for model building using one formula as argument +// Thin wrapper for model building using sparse representation template -std::shared_ptr buildSparseModel(storm::storage::SymbolicModelDescription const& modelDescription, std::vector> const& formulas, bool jit = false, bool doctor = false) { +std::shared_ptr> buildSparseModel(storm::storage::SymbolicModelDescription const& modelDescription, std::vector> const& formulas, bool jit = false, bool doctor = false) { if (formulas.empty()) { // Build all labels and rewards storm::builder::BuilderOptions options(true, true); @@ -61,8 +61,8 @@ std::shared_ptr buildSparseModel(storm::storage::Symbo void define_build(py::module& m) { // Build model - m.def("_build_sparse_model_from_prism_program", &buildSparseModel, "Build the model", py::arg("model_description"), py::arg("formulas") = std::vector>(), py::arg("use_jit") = false, py::arg("doctor") = false); - m.def("_build_sparse_parametric_model_from_prism_program", &buildSparseModel, "Build the parametric model", py::arg("model_description"), py::arg("formulas") = std::vector>(), py::arg("use_jit") = false, py::arg("doctor") = false); + m.def("_build_sparse_model_from_symbolic_description", &buildSparseModel, "Build the model in sparse representation", py::arg("model_description"), py::arg("formulas") = std::vector>(), py::arg("use_jit") = false, py::arg("doctor") = false); + m.def("_build_sparse_parametric_model_from_symbolic_description", &buildSparseModel, "Build the parametric model in sparse representation", py::arg("model_description"), py::arg("formulas") = std::vector>(), py::arg("use_jit") = false, py::arg("doctor") = false); m.def("_build_sparse_model_from_drn", &storm::api::buildExplicitDRNModel, "Build the model from DRN", py::arg("file")); m.def("_build_sparse_parametric_model_from_drn", &storm::api::buildExplicitDRNModel, "Build the parametric model from DRN", py::arg("file")); m.def("build_sparse_model_from_explicit", &storm::api::buildExplicitModel, "Build the model model from explicit input", py::arg("transition_file"), py::arg("labeling_file"), py::arg("state_reward_file") = "", py::arg("transition_reward_file") = "", py::arg("choice_labeling_file") = ""); @@ -71,15 +71,15 @@ void define_build(py::module& m) { void define_optimality_type(py::module& m) { py::enum_(m, "OptimizationDirection") - .value("Minimize", storm::solver::OptimizationDirection::Minimize) - .value("Maximize", storm::solver::OptimizationDirection::Maximize) - ; + .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) { - std::ofstream stream; + std::ofstream stream; storm::utility::openFile(file, stream); storm::exporter::explicitExportSparseModel(stream, model, {}); storm::utility::closeFile(stream); diff --git a/src/core/core.h b/src/core/core.h index 51bc696..cf5a0f9 100644 --- a/src/core/core.h +++ b/src/core/core.h @@ -1,5 +1,4 @@ -#ifndef PYTHON_CORE_CORE_H_ -#define PYTHON_CORE_CORE_H_ +#pragma once #include "common.h" @@ -7,6 +6,4 @@ 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_ */ +void define_optimality_type(py::module& m); \ No newline at end of file diff --git a/tests/storage/test_model.py b/tests/storage/test_model.py index d3c4b90..12b8326 100644 --- a/tests/storage/test_model.py +++ b/tests/storage/test_model.py @@ -4,7 +4,7 @@ from helpers.helper import get_example_path import pytest -class TestModel: +class TestSparseModel: def test_build_dtmc_from_prism_program(self): program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm")) model = stormpy.build_model(program) @@ -26,7 +26,7 @@ class TestModel: assert not model.supports_parameters assert type(model) is stormpy.SparseDtmc - def test_build_dtmc_from_prism_program_formulas(self): + def test_build_dtmc_from_prism_program_reward_formulas(self): program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm")) prop = "R=? [F \"done\"]" properties = stormpy.parse_properties_for_prism_program(prop, program, None) @@ -65,16 +65,6 @@ class TestModel: assert not model.supports_parameters assert type(model) is stormpy.SparseDtmc - def test_build_dtmc(self): - program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm")) - formulas = stormpy.parse_properties_for_prism_program("P=? [ F \"one\" ]", program) - model = stormpy.build_model(program, formulas) - assert model.nr_states == 13 - assert model.nr_transitions == 20 - assert model.model_type == stormpy.ModelType.DTMC - assert not model.supports_parameters - assert type(model) is stormpy.SparseDtmc - def test_build_dtmc_with_undefined_constants(self): jani_model, properties = stormpy.parse_jani_model(get_example_path("dtmc", "brp.jani")) assert jani_model.has_undefined_constants