Browse Source

Better naming for sparse model building

refactoring
Matthias Volk 7 years ago
parent
commit
cfb6dfbf2f
  1. 10
      lib/stormpy/__init__.py
  2. 16
      src/core/core.cpp
  3. 7
      src/core/core.h
  4. 14
      tests/storage/test_model.py

10
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.

16
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<typename ValueType>
std::shared_ptr<storm::models::ModelBase> buildSparseModel(storm::storage::SymbolicModelDescription const& modelDescription, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool jit = false, bool doctor = false) {
std::shared_ptr<storm::models::sparse::Model<ValueType>> buildSparseModel(storm::storage::SymbolicModelDescription const& modelDescription, std::vector<std::shared_ptr<storm::logic::Formula const>> 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<storm::models::ModelBase> buildSparseModel(storm::storage::Symbo
void define_build(py::module& m) {
// Build model
m.def("_build_sparse_model_from_prism_program", &buildSparseModel<double>, "Build the model", py::arg("model_description"), py::arg("formulas") = std::vector<std::shared_ptr<storm::logic::Formula const>>(), py::arg("use_jit") = false, py::arg("doctor") = false);
m.def("_build_sparse_parametric_model_from_prism_program", &buildSparseModel<storm::RationalFunction>, "Build the parametric model", py::arg("model_description"), py::arg("formulas") = std::vector<std::shared_ptr<storm::logic::Formula const>>(), py::arg("use_jit") = false, py::arg("doctor") = false);
m.def("_build_sparse_model_from_symbolic_description", &buildSparseModel<double>, "Build the model in sparse representation", py::arg("model_description"), py::arg("formulas") = std::vector<std::shared_ptr<storm::logic::Formula const>>(), py::arg("use_jit") = false, py::arg("doctor") = false);
m.def("_build_sparse_parametric_model_from_symbolic_description", &buildSparseModel<storm::RationalFunction>, "Build the parametric model in sparse representation", py::arg("model_description"), py::arg("formulas") = std::vector<std::shared_ptr<storm::logic::Formula const>>(), py::arg("use_jit") = false, py::arg("doctor") = false);
m.def("_build_sparse_model_from_drn", &storm::api::buildExplicitDRNModel<double>, "Build the model from DRN", py::arg("file"));
m.def("_build_sparse_parametric_model_from_drn", &storm::api::buildExplicitDRNModel<storm::RationalFunction>, "Build the parametric model from DRN", py::arg("file"));
m.def("build_sparse_model_from_explicit", &storm::api::buildExplicitModel<double>, "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_<storm::solver::OptimizationDirection>(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<typename ValueType>
void exportDRN(std::shared_ptr<storm::models::sparse::Model<ValueType>> 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);

7
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);

14
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

Loading…
Cancel
Save