Browse Source

Renamed preprocess_prism_program to preprocess_symbolic_input

refactoring
Matthias Volk 4 years ago
parent
commit
03605b44c4
No known key found for this signature in database GPG Key ID: 83A57678F739FCD3
  1. 4
      src/core/input.cpp
  2. 10
      tests/gspn/test_gspn_io.py
  3. 4
      tests/pars/test_parametric_model.py

4
src/core/input.cpp

@ -24,7 +24,7 @@ void define_input(py::module& m) {
return storm::api::parseJaniModel(path);
}, "Parse Jani model", py::arg("path"));
m.def("preprocess_prism_program", [](storm::storage::SymbolicModelDescription const& input, std::vector<storm::jani::Property> properties, std::string constantDefinitionString){
m.def("preprocess_symbolic_input", [](storm::storage::SymbolicModelDescription const& input, std::vector<storm::jani::Property> properties, std::string constantDefinitionString){
// Substitute constant definitions in symbolic input.
std::map<storm::expressions::Variable, storm::expressions::Expression> constantDefinitions;
storm::storage::SymbolicModelDescription output;
@ -36,7 +36,7 @@ void define_input(py::module& m) {
}
//ensureNoUndefinedPropertyConstants(outputProperties);
return std::pair<storm::storage::SymbolicModelDescription, std::vector<storm::jani::Property>>(output, outputProperties);
}, "Preprocess Prism program", py::arg("prism_program"), py::arg("properties"), py::arg("constant_definition_string"));
}, "Preprocess symoblic input", py::arg("symbolic_model_description"), py::arg("properties"), py::arg("constant_definition_string"));
// JaniType
py::enum_<storm::jani::ModelType>(m, "JaniModelType", "Type of the Jani model")

10
tests/gspn/test_gspn_io.py

@ -50,9 +50,8 @@ class TestGSPNJani:
properties = jani_builder.create_deadlock_properties(jani_program)
# Instantiate constants
description = stormpy.SymbolicModelDescription(jani_program)
constant_definitions = description.parse_constant_definitions("TIME_BOUND=1")
jani_program = description.instantiate_constants(constant_definitions).as_jani_model()
jani_program, properties = stormpy.preprocess_symbolic_input(jani_program, properties, "TIME_BOUND=1")
jani_program = jani_program.as_jani_model()
# Build model
# Leads to incorrect result
@ -64,8 +63,7 @@ class TestGSPNJani:
assert initial_state == 0
result = stormpy.model_checking(model, properties[0])
assert math.isclose(result.at(initial_state), 1.0)
# Not parsable
#result = stormpy.model_checking(model, properties[1])
#assert math.isclose(result.at(initial_state), 0.09123940783)
result = stormpy.model_checking(model, properties[1])
assert math.isclose(result.at(initial_state), 0.09123940783)
result = stormpy.model_checking(model, properties[2])
assert math.isclose(result.at(initial_state), 5.445544554455446)

4
tests/pars/test_parametric_model.py

@ -22,7 +22,7 @@ class TestSparseParametricModel:
def test_build_parametric_dtmc_preprocess(self):
program = stormpy.parse_prism_program(get_example_path("pdtmc", "herman5.pm"))
formulas = stormpy.parse_properties_for_prism_program("R=? [ F \"stable\" ]", program)
trans_program, trans_formulas = stormpy.preprocess_prism_program(program, formulas, "")
trans_program, trans_formulas = stormpy.preprocess_symbolic_input(program, formulas, "")
trans_prism = trans_program.as_prism_program()
model = stormpy.build_parametric_model(trans_prism, trans_formulas)
assert model.nr_states == 33
@ -70,7 +70,7 @@ class TestSymbolicParametricModel:
def test_build_parametric_dtmc_preprocess(self):
program = stormpy.parse_prism_program(get_example_path("pdtmc", "herman5.pm"))
formulas = stormpy.parse_properties_for_prism_program("R=? [ F \"stable\" ]", program)
trans_program, trans_formulas = stormpy.preprocess_prism_program(program, formulas, "")
trans_program, trans_formulas = stormpy.preprocess_symbolic_input(program, formulas, "")
trans_prism = trans_program.as_prism_program()
model = stormpy.build_symbolic_parametric_model(trans_prism, trans_formulas)
assert model.nr_states == 33

Loading…
Cancel
Save