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

Merge 

Former-commit-id: 664b51e9ec
main
Mavo 9 years ago
parent
2754450f91 102602dea2
commit
8d591a391b
7 changed files with 57 additions and 19 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 29
      src/builder/ExplicitDFTModelBuilder.cpp
  2. 10
      src/builder/ExplicitDFTModelBuilder.h
  3. 10
      src/storage/dft/DFT.cpp
  4. 1
      src/storage/dft/DFT.h
  5. 2
      src/storage/dft/DFTElements.h
  6. 3
      src/storm-dyftee.cpp
  7. 21
      src/utility/storm.h

29
src/builder/ExplicitDFTModelBuilder.cpp
View File

@ -55,7 +55,7 @@ namespace storm {
template <typename ValueType>
std::shared_ptr<storm::models::sparse::Model<ValueType>> ExplicitDFTModelBuilder<ValueType>::buildModel() {
std::shared_ptr<storm::models::sparse::Model<ValueType>> ExplicitDFTModelBuilder<ValueType>::buildModel(LabelOptions const& labelOpts) {
// Initialize
DFTStatePointer state = std::make_shared<storm::storage::DFTState<ValueType>>(mDft, *mStateGenerationInfo, newIndex++);
mStates.findOrAdd(state->status(), state->getId());
@ -88,26 +88,33 @@ namespace storm {
modelComponents.stateLabeling.addLabel("init");
modelComponents.stateLabeling.addLabelToState("init", 0);
// Label all states corresponding to their status (failed, failsafe, failed BE)
modelComponents.stateLabeling.addLabel("failed");
modelComponents.stateLabeling.addLabel("failsafe");
if(labelOpts.buildFailLabel) {
modelComponents.stateLabeling.addLabel("failed");
}
if(labelOpts.buildFailSafeLabel) {
modelComponents.stateLabeling.addLabel("failsafe");
}
// Collect labels for all BE
std::vector<std::shared_ptr<storage::DFTBE<ValueType>>> basicElements = mDft.getBasicElements();
for (std::shared_ptr<storage::DFTBE<ValueType>> elem : basicElements) {
modelComponents.stateLabeling.addLabel(elem->name() + "_fail");
if(labelOpts.beLabels.count(elem->name()) > 0) {
modelComponents.stateLabeling.addLabel(elem->name() + "_fail");
}
}
for (auto const& stateIdPair : mStates) {
storm::storage::BitVector state = stateIdPair.first;
size_t stateId = stateIdPair.second;
if (mDft.hasFailed(state, *mStateGenerationInfo)) {
if (labelOpts.buildFailLabel && mDft.hasFailed(state, *mStateGenerationInfo)) {
modelComponents.stateLabeling.addLabelToState("failed", stateId);
}
if (mDft.isFailsafe(state, *mStateGenerationInfo)) {
if (labelOpts.buildFailSafeLabel && mDft.isFailsafe(state, *mStateGenerationInfo)) {
modelComponents.stateLabeling.addLabelToState("failsafe", stateId);
};
// Set fail status for each BE
for (std::shared_ptr<storage::DFTBE<ValueType>> elem : basicElements) {
if (storm::storage::DFTState<ValueType>::hasFailed(state, mStateGenerationInfo->getStateIndex(elem->id()))) {
if (labelOpts.beLabels.count(elem->name()) > 0 && storm::storage::DFTState<ValueType>::hasFailed(state, mStateGenerationInfo->getStateIndex(elem->id())) ) {
modelComponents.stateLabeling.addLabelToState(elem->name() + "_fail", stateId);
}
}
@ -129,7 +136,13 @@ namespace storm {
}
model = std::make_shared<storm::models::sparse::Ctmc<ValueType>>(std::move(rateMatrix), std::move(modelComponents.stateLabeling));
} else {
model = std::make_shared<storm::models::sparse::MarkovAutomaton<ValueType>>(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), std::move(modelComponents.markovianStates), std::move(modelComponents.exitRates), true);
std::shared_ptr<storm::models::sparse::MarkovAutomaton<ValueType>> ma = std::make_shared<storm::models::sparse::MarkovAutomaton<ValueType>>(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), std::move(modelComponents.markovianStates), std::move(modelComponents.exitRates), true);
if (ma->hasOnlyTrivialNondeterminism()) {
// Markov automaton can be converted into CTMC
model = ma->convertToCTMC();
} else {
model = ma;
}
}
model->printModelInformationToStream(std::cout);

10
src/builder/ExplicitDFTModelBuilder.h
View File

@ -46,15 +46,23 @@ namespace storm {
const size_t INITIAL_BUCKETSIZE = 20000;
storm::storage::DFT<ValueType> const& mDft;
std::shared_ptr<storm::storage::DFTStateGenerationInfo> mStateGenerationInfo;
storm::storage::BitVectorHashMap<size_t> mStates;
size_t newIndex = 0;
public:
struct LabelOptions {
bool buildFailLabel = true;
bool buildFailSafeLabel = false;
std::set<std::string> beLabels = {};
};
ExplicitDFTModelBuilder(storm::storage::DFT<ValueType> const& dft);
std::shared_ptr<storm::models::sparse::Model<ValueType>> buildModel();
std::shared_ptr<storm::models::sparse::Model<ValueType>> buildModel(LabelOptions const& labelOpts);
private:
bool exploreStates(std::queue<DFTStatePointer>& stateQueue, storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder, std::vector<uint_fast64_t>& markovianStates, std::vector<ValueType>& exitRates);

10
src/storage/dft/DFT.cpp
View File

@ -237,11 +237,21 @@ namespace storm {
return ISD;
}
template<typename ValueType>
std::vector<size_t> DFT<ValueType>::immediateFailureCauses(size_t index) const {
if(isGate(index)) {
} else {
return {index};
}
}
template<typename ValueType>
DFTColouring<ValueType> DFT<ValueType>::colourDFT() const {
return DFTColouring<ValueType>(*this);
}
template<typename ValueType>
DFTIndependentSymmetries DFT<ValueType>::findSymmetries(DFTColouring<ValueType> const& colouring) const {
std::vector<size_t> vec;

1
src/storage/dft/DFT.h
View File

@ -274,6 +274,7 @@ namespace storm {
DFTIndependentSymmetries findSymmetries(DFTColouring<ValueType> const& colouring) const;
std::vector<size_t> immediateFailureCauses(size_t index) const;
private:
std::pair<std::vector<size_t>, std::vector<size_t>> getSortedParentAndOutDepIds(size_t index) const;

2
src/storage/dft/DFTElements.h
View File

@ -173,6 +173,8 @@ namespace storm {
}
virtual void extendSpareModule(std::set<size_t>& elementsInModule) const;
// virtual void extendImmediateFailureCausePathEvents(std::set<size_t>& ) const;
virtual size_t nrChildren() const = 0;

3
src/storm-dyftee.cpp
View File

@ -32,7 +32,8 @@ void analyzeDFT(std::string filename, std::string property, bool symred = false)
// Building Markov Automaton
std::cout << "Building Model..." << std::endl;
storm::builder::ExplicitDFTModelBuilder<ValueType> builder(dft);
std::shared_ptr<storm::models::sparse::Model<ValueType>> model = builder.buildModel();
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::cout << "Built Model" << std::endl;
// Model checking

21
src/utility/storm.h
View File

@ -196,6 +196,15 @@ namespace storm {
template<typename ModelType>
std::shared_ptr<storm::models::ModelBase> preprocessModel(std::shared_ptr<storm::models::ModelBase> model, std::vector<std::shared_ptr<const storm::logic::Formula>> const& formulas) {
if(model->getType() == storm::models::ModelType::MarkovAutomaton && model->isSparseModel()) {
std::shared_ptr<storm::models::sparse::MarkovAutomaton<typename ModelType::ValueType>> ma = model->template as<storm::models::sparse::MarkovAutomaton<typename ModelType::ValueType>>();
if (ma->hasOnlyTrivialNondeterminism()) {
// Markov automaton can be converted into CTMC
model = ma->convertToCTMC();
}
}
if (model->isSparseModel() && storm::settings::generalSettings().isBisimulationSet()) {
storm::storage::BisimulationType bisimType = storm::storage::BisimulationType::Strong;
if (storm::settings::bisimulationSettings().isWeakBisimulationSet()) {
@ -205,6 +214,7 @@ namespace storm {
STORM_LOG_THROW(model->isSparseModel(), storm::exceptions::InvalidSettingsException, "Bisimulation minimization is currently only available for sparse models.");
return performBisimulationMinimization<ModelType>(model->template as<storm::models::sparse::Model<typename ModelType::ValueType>>(), formulas, bisimType);
}
return model;
}
@ -302,15 +312,8 @@ namespace storm {
result = modelchecker.check(task);
} else if (model->getType() == storm::models::ModelType::MarkovAutomaton) {
std::shared_ptr<storm::models::sparse::MarkovAutomaton<ValueType>> ma = model->template as<storm::models::sparse::MarkovAutomaton<ValueType>>();
if (ma->hasOnlyTrivialNondeterminism()) {
// Markov automaton can be converted into CTMC
std::shared_ptr<storm::models::sparse::Ctmc<ValueType>> ctmc = ma->convertToCTMC();
storm::modelchecker::SparseCtmcCslModelChecker<storm::models::sparse::Ctmc<ValueType>> modelchecker(*ctmc);
result = modelchecker.check(task);
} else {
storm::modelchecker::SparseMarkovAutomatonCslModelChecker<storm::models::sparse::MarkovAutomaton<ValueType>> modelchecker(*ma);
result = modelchecker.check(task);
}
storm::modelchecker::SparseMarkovAutomatonCslModelChecker<storm::models::sparse::MarkovAutomaton<ValueType>> modelchecker(*ma);
result = modelchecker.check(task);
} else {
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The model type " << model->getType() << " is not supported.");
}

Write Preview
Loading…
Cancel
Save