Browse Source

Binding for preprocessing prism models

refactoring
Matthias Volk 5 years ago
parent
commit
e831ae36c5
  1. 46
      lib/stormpy/examples/files/pdtmc/herman5.pm
  2. 14
      src/core/input.cpp
  3. 13
      tests/pars/test_parametric_model.py

46
lib/stormpy/examples/files/pdtmc/herman5.pm

@ -0,0 +1,46 @@
// herman's self stabilising algorithm [Her90]
// gxn/dxp 13/07/02
// the procotol is synchronous with no nondeterminism (a DTMC)
dtmc
// coin
const double p;
// module for process 1
module process1
// Boolean variable for process 1
x1 : [0..1];
i1 : bool init false;
[initial] (!i1) -> 0.5 : (x1'=0) & (i1'=true) + 0.5 : (x1'=1) & (i1'=true);
[step] (i1 & x1=x0) -> p : (x1'=0) + 1-p : (x1'=1);
[step] (i1 & x1!=x0) -> (x1'=x0);
endmodule
// add further processes through renaming
module process2 = process1 [ x1=x2, x0=x1, i1=i2 ] endmodule
module process3 = process1 [ x1=x3, x0=x2, i1=i3 ] endmodule
module process4 = process1 [ x1=x4, x0=x3, i1=i4 ] endmodule
module process5 = process1 [ x1=x0, x0=x4, i1=i5 ] endmodule
formula initialized = i1 & i2 & i3 & i4 & i5;
// cost - 1 in each state (expected number of steps)
rewards "steps"
initialized : 1;
endrewards
// formula, for use in properties: number of tokens
// (i.e. number of processes that have the same value as the process to their left)
formula num_tokens = (x1=x0?1:0)
+(x2=x1?1:0)
+(x3=x2?1:0)
+(x4=x3?1:0)
+(x0=x4?1:0);
// label - stable configurations (1 token)
label "stable" = num_tokens=1 & initialized;

14
src/core/input.cpp

@ -24,6 +24,20 @@ void define_input(py::module& m) {
return storm::api::parseJaniModel(path); return storm::api::parseJaniModel(path);
}, "Parse Jani model", py::arg("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){
// Substitute constant definitions in symbolic input.
std::map<storm::expressions::Variable, storm::expressions::Expression> constantDefinitions;
storm::storage::SymbolicModelDescription output;
std::vector<storm::jani::Property> outputProperties;
constantDefinitions = input.parseConstantDefinitions(constantDefinitionString);
output = input.preprocess(constantDefinitions);
if (!properties.empty()) {
outputProperties = storm::api::substituteConstantsInProperties(properties, constantDefinitions);
}
//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"));
// JaniType // JaniType
py::enum_<storm::jani::ModelType>(m, "JaniModelType", "Type of the Jani model") py::enum_<storm::jani::ModelType>(m, "JaniModelType", "Type of the Jani model")
.value("DTMC", storm::jani::ModelType::DTMC) .value("DTMC", storm::jani::ModelType::DTMC)

13
tests/pars/test_parametric_model.py

@ -54,6 +54,19 @@ class TestSymbolicParametricModel:
assert model.has_parameters assert model.has_parameters
assert type(model) is stormpy.SymbolicSylvanParametricDtmc assert type(model) is stormpy.SymbolicSylvanParametricDtmc
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_prism = trans_program.as_prism_program()
model = stormpy.build_symbolic_parametric_model(trans_prism, trans_formulas)
assert model.nr_states == 33
assert model.nr_transitions == 276
assert model.model_type == stormpy.ModelType.DTMC
assert model.supports_parameters
assert model.has_parameters
assert type(model) is stormpy.SymbolicSylvanParametricDtmc
def test_build_dtmc_supporting_parameters(self): def test_build_dtmc_supporting_parameters(self):
program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm")) program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm"))
formulas = stormpy.parse_properties_for_prism_program("P=? [ F \"one\" ]", program) formulas = stormpy.parse_properties_for_prism_program("P=? [ F \"one\" ]", program)

Loading…
Cancel
Save