sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Merge branch 'monolithic-dft-update' of https://sselab.de/lab9/private/git/storm into monolithic-dft-update 

Former-commit-id: 8ac6c51c92
tempestpy_adaptions
sjunges 9 years ago
parent
e390e1c39d e5fd604498
commit
eeb289bdb8
4 changed files with 17 additions and 13 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 4
      src/builder/ExplicitDFTModelBuilder.cpp
  2. 3
      src/builder/ExplicitDFTModelBuilder.h
  3. 12
      src/modelchecker/DFTAnalyser.h
  4. 11
      src/storm-dyftee.cpp

4
src/builder/ExplicitDFTModelBuilder.cpp
View File

@ -15,7 +15,7 @@ namespace storm {
} }
template <typename ValueType> template <typename ValueType>
ExplicitDFTModelBuilder<ValueType>::ExplicitDFTModelBuilder(storm::storage::DFT<ValueType> const& dft, storm::storage::DFTIndependentSymmetries const& symmetries) : mDft(dft), mStates(((mDft.stateVectorSize() / 64) + 1) * 64, INITIAL_BUCKETSIZE) {
ExplicitDFTModelBuilder<ValueType>::ExplicitDFTModelBuilder(storm::storage::DFT<ValueType> const& dft, storm::storage::DFTIndependentSymmetries const& symmetries, bool enableDC) : mDft(dft), mStates(((mDft.stateVectorSize() / 64) + 1) * 64, INITIAL_BUCKETSIZE), enableDC(enableDC) {
// stateVectorSize is bound for size of bitvector // stateVectorSize is bound for size of bitvector
mStateGenerationInfo = std::make_shared<storm::storage::DFTStateGenerationInfo>(mDft.buildStateGenerationInfo(symmetries)); mStateGenerationInfo = std::make_shared<storm::storage::DFTStateGenerationInfo>(mDft.buildStateGenerationInfo(symmetries));
@ -218,7 +218,7 @@ namespace storm {
next->checkFailsafe(*newState, queues); next->checkFailsafe(*newState, queues);
} }
while (!queues.dontCarePropagationDone()) {
while (enableDC && !queues.dontCarePropagationDone()) {
DFTElementPointer next = queues.nextDontCarePropagation(); DFTElementPointer next = queues.nextDontCarePropagation();
next->checkDontCareAnymore(*newState, queues); next->checkDontCareAnymore(*newState, queues);
} }

3
src/builder/ExplicitDFTModelBuilder.h
View File

@ -55,6 +55,7 @@ namespace storm {
std::vector<std::pair<uint_fast64_t, storm::storage::BitVector>> mPseudoStatesMapping; // vector of (id to concrete state, bitvector) std::vector<std::pair<uint_fast64_t, storm::storage::BitVector>> mPseudoStatesMapping; // vector of (id to concrete state, bitvector)
size_t newIndex = 0; size_t newIndex = 0;
bool mergeFailedStates = true; bool mergeFailedStates = true;
bool enableDC = true;
size_t failedIndex = 0; size_t failedIndex = 0;
size_t initialStateIndex = 0; size_t initialStateIndex = 0;
@ -65,7 +66,7 @@ namespace storm {
std::set<std::string> beLabels = {}; std::set<std::string> beLabels = {};
}; };
ExplicitDFTModelBuilder(storm::storage::DFT<ValueType> const& dft, storm::storage::DFTIndependentSymmetries const& symmetries);
ExplicitDFTModelBuilder(storm::storage::DFT<ValueType> const& dft, storm::storage::DFTIndependentSymmetries const& symmetries, bool enableDC);
std::shared_ptr<storm::models::sparse::Model<ValueType>> buildModel(LabelOptions const& labelOpts); std::shared_ptr<storm::models::sparse::Model<ValueType>> buildModel(LabelOptions const& labelOpts);

12
src/modelchecker/DFTAnalyser.h
View File

@ -21,7 +21,7 @@ class DFTAnalyser {
std::chrono::duration<double> totalTime = std::chrono::duration<double>::zero(); std::chrono::duration<double> totalTime = std::chrono::duration<double>::zero();
ValueType checkResult = storm::utility::zero<ValueType>(); ValueType checkResult = storm::utility::zero<ValueType>();
public: public:
void check(storm::storage::DFT<ValueType> dft , std::shared_ptr<const storm::logic::Formula> const& formula, bool symred = true, bool allowModularisation = true) {
void check(storm::storage::DFT<ValueType> dft , std::shared_ptr<const storm::logic::Formula> const& formula, bool symred = true, bool allowModularisation = true, bool enableDC = true) {
// Building DFT // Building DFT
std::chrono::high_resolution_clock::time_point totalStart = std::chrono::high_resolution_clock::now(); std::chrono::high_resolution_clock::time_point totalStart = std::chrono::high_resolution_clock::now();
@ -30,7 +30,7 @@ public:
// Optimizing DFT // Optimizing DFT
dft = dft.optimize(); dft = dft.optimize();
std::vector<storm::storage::DFT<ValueType>> dfts; std::vector<storm::storage::DFT<ValueType>> dfts;
checkResult = checkHelper(dft, formula, symred, allowModularisation);
checkResult = checkHelper(dft, formula, symred, allowModularisation, enableDC);
totalTime = std::chrono::high_resolution_clock::now() - totalStart; totalTime = std::chrono::high_resolution_clock::now() - totalStart;
@ -38,7 +38,7 @@ public:
} }
private: private:
ValueType checkHelper(storm::storage::DFT<ValueType> const& dft , std::shared_ptr<const storm::logic::Formula> const& formula, bool symred = true, bool allowModularisation = true) {
ValueType checkHelper(storm::storage::DFT<ValueType> const& dft , std::shared_ptr<const storm::logic::Formula> const& formula, bool symred = true, bool allowModularisation = true, bool enableDC = true) {
std::cout << "check helper called" << std::endl; std::cout << "check helper called" << std::endl;
bool invResults = false; bool invResults = false;
std::vector<storm::storage::DFT<ValueType>> dfts = {dft}; std::vector<storm::storage::DFT<ValueType>> dfts = {dft};
@ -82,7 +82,7 @@ private:
} }
if(res.empty()) { if(res.empty()) {
// Model based modularisation. // Model based modularisation.
auto const& models = buildMarkovModels(dfts, formula, symred);
auto const& models = buildMarkovModels(dfts, formula, symred, enableDC);
for (auto const& model : models) { for (auto const& model : models) {
@ -132,7 +132,7 @@ private:
} }
std::vector<std::shared_ptr<storm::models::sparse::Model<ValueType>>> buildMarkovModels(std::vector<storm::storage::DFT<ValueType>> const& dfts, std::shared_ptr<const storm::logic::Formula> const& formula, bool symred) {
std::vector<std::shared_ptr<storm::models::sparse::Model<ValueType>>> buildMarkovModels(std::vector<storm::storage::DFT<ValueType>> const& dfts, std::shared_ptr<const storm::logic::Formula> const& formula, bool symred, bool enableDC) {
std::vector<std::shared_ptr<storm::models::sparse::Model<ValueType>>> models; std::vector<std::shared_ptr<storm::models::sparse::Model<ValueType>>> models;
for(auto& dft : dfts) { for(auto& dft : dfts) {
std::chrono::high_resolution_clock::time_point buildingStart = std::chrono::high_resolution_clock::now(); std::chrono::high_resolution_clock::time_point buildingStart = std::chrono::high_resolution_clock::now();
@ -150,7 +150,7 @@ private:
// Building Markov Automaton // Building Markov Automaton
std::cout << "Building Model..." << std::endl; std::cout << "Building Model..." << std::endl;
storm::builder::ExplicitDFTModelBuilder<ValueType> builder(dft, symmetries);
storm::builder::ExplicitDFTModelBuilder<ValueType> builder(dft, symmetries, enableDC);
typename storm::builder::ExplicitDFTModelBuilder<ValueType>::LabelOptions labeloptions; // TODO initialize this with the formula typename storm::builder::ExplicitDFTModelBuilder<ValueType>::LabelOptions labeloptions; // TODO initialize this with the formula
std::shared_ptr<storm::models::sparse::Model<ValueType>> model = builder.buildModel(labeloptions); std::shared_ptr<storm::models::sparse::Model<ValueType>> model = builder.buildModel(labeloptions);
//model->printModelInformationToStream(std::cout); //model->printModelInformationToStream(std::cout);

11
src/storm-dyftee.cpp
View File

@ -11,7 +11,7 @@
* @param property PCTC formula capturing the property to check. * @param property PCTC formula capturing the property to check.
*/ */
template <typename ValueType> template <typename ValueType>
void analyzeDFT(std::string filename, std::string property, bool symred = false, bool allowModularisation = false) {
void analyzeDFT(std::string filename, std::string property, bool symred = false, bool allowModularisation = false, bool enableDC = true) {
storm::settings::SettingsManager& manager = storm::settings::mutableManager(); storm::settings::SettingsManager& manager = storm::settings::mutableManager();
manager.setFromString(""); manager.setFromString("");
@ -22,7 +22,7 @@ void analyzeDFT(std::string filename, std::string property, bool symred = false,
assert(formulas.size() == 1); assert(formulas.size() == 1);
DFTAnalyser<ValueType> analyser; DFTAnalyser<ValueType> analyser;
analyser.check(dft, formulas[0], symred, allowModularisation);
analyser.check(dft, formulas[0], symred, allowModularisation, enableDC);
analyser.printTimings(); analyser.printTimings();
analyser.printResult(); analyser.printResult();
} }
@ -47,6 +47,7 @@ int main(int argc, char** argv) {
bool minimal = true; bool minimal = true;
bool allowModular = true; bool allowModular = true;
bool enableModularisation = false; bool enableModularisation = false;
bool disableDC = false;
std::string filename = argv[1]; std::string filename = argv[1];
std::string operatorType = ""; std::string operatorType = "";
std::string targetFormula = ""; std::string targetFormula = "";
@ -92,6 +93,8 @@ int main(int argc, char** argv) {
symred = true; symred = true;
} else if (option == "--modularisation") { } else if (option == "--modularisation") {
enableModularisation = true; enableModularisation = true;
} else if (option == "--disabledc") {
disableDC = true;
} else if (option == "--min") { } else if (option == "--min") {
minimal = true; minimal = true;
} else if (option == "--max") { } else if (option == "--max") {
@ -114,8 +117,8 @@ int main(int argc, char** argv) {
std::cout << "Running " << (parametric ? "parametric " : "") << "DFT analysis on file " << filename << " with property " << pctlFormula << std::endl; std::cout << "Running " << (parametric ? "parametric " : "") << "DFT analysis on file " << filename << " with property " << pctlFormula << std::endl;
if (parametric) { if (parametric) {
analyzeDFT<storm::RationalFunction>(filename, pctlFormula, symred, allowModular && enableModularisation );
analyzeDFT<storm::RationalFunction>(filename, pctlFormula, symred, allowModular && enableModularisation, !disableDC );
} else { } else {
analyzeDFT<double>(filename, pctlFormula, symred, allowModular && enableModularisation);
analyzeDFT<double>(filename, pctlFormula, symred, allowModular && enableModularisation, !disableDC);
} }
} }
Write Preview
Loading…
Cancel
Save