You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
27 lines
1.6 KiB
27 lines
1.6 KiB
#include "analysis.h"
|
|
|
|
#include "storm-dft/parser/DFTJsonParser.h"
|
|
#include "storm-dft/builder/ExplicitDFTModelBuilder.h"
|
|
#include "storm-dft/storage/dft/DFTIsomorphism.h"
|
|
|
|
|
|
// Thin wrapper for DFT analysis
|
|
template<typename ValueType>
|
|
//std::vector<ValueType> analyzeDFT(storm::storage::DFT<ValueType> const& dft, std::vector<std::shared_ptr<storm::logic::Formula const>> const& properties, bool symred, bool allowModularisation, std::set<size_t> const& relevantEvents = {}, double approximationError = 0.0, storm::builder::ApproximationHeuristic approximationHeuristic = storm::builder::ApproximationHeuristic::DEPTH) {
|
|
std::vector<ValueType> analyzeDFT(storm::storage::DFT<ValueType> const& dft, std::vector<std::shared_ptr<storm::logic::Formula const>> const& properties, bool symred, bool allowModularisation, std::set<size_t> const& relevantEvents, bool allowDCForRelevant) {
|
|
typename storm::modelchecker::DFTModelChecker<ValueType>::dft_results dftResults = storm::api::analyzeDFT(dft, properties, symred, allowModularisation, relevantEvents, allowDCForRelevant, 0.0, storm::builder::ApproximationHeuristic::DEPTH, false);
|
|
|
|
std::vector<ValueType> results;
|
|
for (auto result : dftResults) {
|
|
results.push_back(boost::get<ValueType>(result));
|
|
}
|
|
return results;
|
|
}
|
|
|
|
|
|
// Define python bindings
|
|
void define_analysis(py::module& m) {
|
|
|
|
m.def("analyze_dft", &analyzeDFT<double>, "Analyze the DFT", py::arg("dft"), py::arg("properties"), py::arg("symred")=true, py::arg("allow_modularisation")=false, py::arg("relevant_events")=std::set<size_t>(), py::arg("dc_for_relevant")=true);
|
|
|
|
}
|