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

Merge remote-tracking branch 'refs/remotes/origin/master' into modelchecker-helper-refactor

tempestpy_adaptions
Tim Quatmann 4 years ago
parent
b7883a8ef1 72813a9774
commit
7e6b0c27c3
11 changed files with 94 additions and 99 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. 41
      src/storm-dft-cli/storm-dft.cpp
  2. 35
      src/storm-dft/api/storm-dft.h
  3. 7
      src/storm-dft/builder/ExplicitDFTModelBuilder.cpp
  4. 7
      src/storm-dft/builder/ExplicitDFTModelBuilder.h
  5. 17
      src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
  6. 2
      src/storm-dft/parser/DFTGalileoParser.cpp
  7. 5
      src/storm-dft/storage/dft/DFT.cpp
  8. 34
      src/storm-dft/storage/dft/DFTIsomorphism.h
  9. 18
      src/storm-dft/utility/FDEPConflictFinder.cpp
  10. 3
      src/storm-gspn/parser/GreatSpnEditorProjectParser.cpp
  11. 24
      src/test/storm-dft/api/DftModelBuildingTest.cpp

41
src/storm-dft-cli/storm-dft.cpp
View File

@ -90,46 +90,25 @@ void processOptions() {
dft = storm::api::applyTransformations(*dft, faultTreeSettings.isUniqueFailedBE(), true);
STORM_LOG_DEBUG(dft->getElementsString());
dft->setDynamicBehaviorInfo();
storm::api::PreprocessingResult preResults;
// Compute minimal number of BE failures leading to system failure and
// maximal number of BE failures not leading to system failure yet.
// TODO: always needed?
preResults.lowerBEBound = storm::dft::utility::FailureBoundFinder::getLeastFailureBound(*dft, useSMT, solverTimeout);
preResults.upperBEBound = storm::dft::utility::FailureBoundFinder::getAlwaysFailedBound(*dft, useSMT, solverTimeout);
STORM_LOG_DEBUG("BE failure bounds" << std::endl << "========================================" << std::endl <<
"Lower bound: " << std::to_string(preResults.lowerBEBound) << std::endl <<
"Upper bound: " << std::to_string(preResults.upperBEBound));
auto bounds = storm::api::computeBEFailureBounds(*dft, useSMT, solverTimeout);
STORM_LOG_DEBUG("BE failure bounds: lower bound: " << bounds.first << ", upper bound: " << bounds.second << ".");
// TODO: move into API call?
preResults.fdepConflicts = storm::dft::utility::FDEPConflictFinder<ValueType>::getDependencyConflicts(*dft, useSMT, solverTimeout);
if (preResults.fdepConflicts.empty()) {
STORM_LOG_DEBUG("No FDEP conflicts found");
// Check which FDEPs actually introduce conflicts which need non-deterministic resolution
bool hasConflicts = storm::api::computeDependencyConflicts(*dft, useSMT, solverTimeout);
if (hasConflicts) {
STORM_LOG_DEBUG("FDEP conflicts found.");
} else {
STORM_LOG_DEBUG("========================================" << std::endl << "FDEP CONFLICTS" << std::endl << "========================================");
}
for (auto pair: preResults.fdepConflicts) {
STORM_LOG_DEBUG("Conflict between " << dft->getElement(pair.first)->name() << " and " << dft->getElement(pair.second)->name());
}
// Set the conflict map of the dft
std::set<size_t> conflict_set;
for (auto conflict : preResults.fdepConflicts) {
conflict_set.insert(size_t(conflict.first));
conflict_set.insert(size_t(conflict.second));
}
for (size_t depId : dft->getDependencies()) {
if (!conflict_set.count(depId)) {
dft->setDependencyNotInConflict(depId);
}
STORM_LOG_DEBUG("No FDEP conflicts found.");
}
#ifdef STORM_HAVE_Z3
if (useSMT) {
// Solve with SMT
STORM_LOG_DEBUG("Running DFT analysis with use of SMT");
STORM_LOG_DEBUG("Running DFT analysis with use of SMT.");
// Set dynamic behavior vector
storm::api::analyzeDFTSMT(*dft, true);
}

35
src/storm-dft/api/storm-dft.h
View File

@ -18,12 +18,6 @@
namespace storm {
namespace api {
struct PreprocessingResult {
uint64_t lowerBEBound;
uint64_t upperBEBound;
std::vector<std::pair<uint64_t, uint64_t>> fdepConflicts;
};
/*!
* Load DFT from Galileo file.
@ -93,29 +87,36 @@ namespace storm {
return transformedDFT;
}
template <typename ValueType>
bool computeDependencyConflicts(storm::storage::DFT<ValueType> const& dft, bool useSMT, double solverTimeout) {
std::vector<std::pair<uint64_t, uint64_t>> fdepConflicts = storm::dft::utility::FDEPConflictFinder<ValueType>::getDependencyConflicts(*dft, useSMT, solverTimeout);
template<typename ValueType>
std::pair<uint64_t, uint64_t> computeBEFailureBounds(storm::storage::DFT<ValueType> const& dft, bool useSMT, double solverTimeout) {
uint64_t lowerBEBound = storm::dft::utility::FailureBoundFinder::getLeastFailureBound(dft, useSMT, solverTimeout);
uint64_t upperBEBound = storm::dft::utility::FailureBoundFinder::getAlwaysFailedBound(dft, useSMT, solverTimeout);
return std::make_pair(lowerBEBound, upperBEBound);
}
if (fdepConflicts.empty()) {
return false;
}
for (auto pair: fdepConflicts) {
template<typename ValueType>
bool computeDependencyConflicts(storm::storage::DFT<ValueType>& dft, bool useSMT, double solverTimeout) {
// Initialize which DFT elements have dynamic behavior
dft.setDynamicBehaviorInfo();
std::vector<std::pair<uint64_t, uint64_t>> fdepConflicts = storm::dft::utility::FDEPConflictFinder<ValueType>::getDependencyConflicts(dft, useSMT, solverTimeout);
for (auto const& pair: fdepConflicts) {
STORM_LOG_DEBUG("Conflict between " << dft.getElement(pair.first)->name() << " and " << dft.getElement(pair.second)->name());
}
// Set the conflict map of the dft
std::set<size_t> conflict_set;
for (auto conflict : fdepConflicts) {
for (auto const& conflict : fdepConflicts) {
conflict_set.insert(size_t(conflict.first));
conflict_set.insert(size_t(conflict.second));
}
for (size_t depId : dft->getDependencies()) {
for (size_t depId : dft.getDependencies()) {
if (!conflict_set.count(depId)) {
dft->setDependencyNotInConflict(depId);
dft.setDependencyNotInConflict(depId);
}
}
return true;
return !fdepConflicts.empty();
}
/*!

7
src/storm-dft/builder/ExplicitDFTModelBuilder.cpp
View File

@ -34,19 +34,18 @@ namespace storm {
}
template<typename ValueType, typename StateType>
ExplicitDFTModelBuilder<ValueType, StateType>::ExplicitDFTModelBuilder(storm::storage::DFT<ValueType> const& dft, storm::storage::DFTIndependentSymmetries const& symmetries, std::set<size_t> const& relevantEvents, bool allowDCForRelevantEvents) :
ExplicitDFTModelBuilder<ValueType, StateType>::ExplicitDFTModelBuilder(storm::storage::DFT<ValueType> const& dft, storm::storage::DFTIndependentSymmetries const& symmetries) :
dft(dft),
stateGenerationInfo(std::make_shared<storm::storage::DFTStateGenerationInfo>(dft.buildStateGenerationInfo(symmetries))),
relevantEvents(relevantEvents),
generator(dft, *stateGenerationInfo),
matrixBuilder(!generator.isDeterministicModel()),
stateStorage(dft.stateBitVectorSize()),
explorationQueue(1, 0, 0.9, false)
{
// Set relevant events
this->dft.setRelevantEvents(this->relevantEvents, allowDCForRelevantEvents);
STORM_LOG_DEBUG("Relevant events: " << this->dft.getRelevantEventsString());
if (this->relevantEvents.empty()) {
if (dft.getRelevantEvents().size() <= 1) {
STORM_LOG_ASSERT(dft.getRelevantEvents()[0] == dft.getTopLevelIndex(), "TLE is not relevant");
// Only interested in top level event -> introduce unique failed state
this->uniqueFailedState = true;
STORM_LOG_DEBUG("Using unique failed state with id 0.");

7
src/storm-dft/builder/ExplicitDFTModelBuilder.h
View File

@ -155,10 +155,8 @@ namespace storm {
*
* @param dft DFT.
* @param symmetries Symmetries in the dft.
* @param relevantEvents List with ids of relevant events which should be observed.
* @param allowDCForRelevantEvents If true, Don't Care propagation is allowed even for relevant events.
*/
ExplicitDFTModelBuilder(storm::storage::DFT<ValueType> const& dft, storm::storage::DFTIndependentSymmetries const& symmetries, std::set<size_t> const& relevantEvents, bool allowDCForRelevantEvents);
ExplicitDFTModelBuilder(storm::storage::DFT<ValueType> const& dft, storm::storage::DFTIndependentSymmetries const& symmetries);
/*!
* Build model from DFT.
@ -291,9 +289,6 @@ namespace storm {
// TODO: use const reference
std::shared_ptr<storm::storage::DFTStateGenerationInfo> stateGenerationInfo;
// List with ids of relevant events which should be observed.
std::set<size_t> const& relevantEvents;
// Heuristic used for approximation
storm::builder::ApproximationHeuristic usedHeuristic;

17
src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
View File

@ -207,6 +207,7 @@ namespace storm {
STORM_LOG_DEBUG("Building Model via parallel composition...");
explorationTimer.start();
ft.setRelevantEvents(relevantEvents, allowDCForRelevantEvents);
// Find symmetries
std::map<size_t, std::vector<std::vector<size_t>>> emptySymmetry;
storm::storage::DFTIndependentSymmetries symmetries(emptySymmetry);
@ -219,7 +220,7 @@ namespace storm {
// Build a single CTMC
STORM_LOG_DEBUG("Building Model from DFT with top level element " << ft.getElement(ft.getTopLevelIndex())->toString() << " ...");
storm::builder::ExplicitDFTModelBuilder<ValueType> builder(ft, symmetries, relevantEvents, allowDCForRelevantEvents);
storm::builder::ExplicitDFTModelBuilder<ValueType> builder(ft, symmetries);
builder.buildModel(0, 0.0);
std::shared_ptr<storm::models::sparse::Model<ValueType>> model = builder.getModel();
explorationTimer.stop();
@ -267,6 +268,9 @@ namespace storm {
} else {
// No composition was possible
explorationTimer.start();
dft.setRelevantEvents(relevantEvents, allowDCForRelevantEvents);
// Find symmetries
std::map<size_t, std::vector<std::vector<size_t>>> emptySymmetry;
storm::storage::DFTIndependentSymmetries symmetries(emptySymmetry);
@ -279,8 +283,7 @@ namespace storm {
// Build a single CTMC
STORM_LOG_DEBUG("Building Model...");
storm::builder::ExplicitDFTModelBuilder<ValueType> builder(dft, symmetries, relevantEvents,
allowDCForRelevantEvents);
storm::builder::ExplicitDFTModelBuilder<ValueType> builder(dft, symmetries);
builder.buildModel(0, 0.0);
std::shared_ptr<storm::models::sparse::Model<ValueType>> model = builder.getModel();
if (printInfo) {
@ -306,6 +309,8 @@ namespace storm {
auto ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>();
auto dftIOSettings = storm::settings::getModule<storm::settings::modules::DftIOSettings>();
dft.setRelevantEvents(relevantEvents, allowDCForRelevantEvents);
// Find symmetries
std::map<size_t, std::vector<std::vector<size_t>>> emptySymmetry;
storm::storage::DFTIndependentSymmetries symmetries(emptySymmetry);
@ -324,8 +329,7 @@ namespace storm {
storm::utility::zero<ValueType>());
std::shared_ptr<storm::models::sparse::Model<ValueType>> model;
std::vector<ValueType> newResult;
storm::builder::ExplicitDFTModelBuilder<ValueType> builder(dft, symmetries, relevantEvents,
allowDCForRelevantEvents);
storm::builder::ExplicitDFTModelBuilder<ValueType> builder(dft, symmetries);
// TODO: compute approximation for all properties simultaneously?
std::shared_ptr<const storm::logic::Formula> property = properties[0];
@ -422,8 +426,7 @@ namespace storm {
// Build a single Markov Automaton
auto ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>();
STORM_LOG_DEBUG("Building Model...");
storm::builder::ExplicitDFTModelBuilder<ValueType> builder(dft, symmetries, relevantEvents,
allowDCForRelevantEvents);
storm::builder::ExplicitDFTModelBuilder<ValueType> builder(dft, symmetries);
builder.buildModel(0, 0.0);
std::shared_ptr<storm::models::sparse::Model<ValueType>> model = builder.getModel();
if (eliminateChains && model->isOfType(storm::models::ModelType::MarkovAutomaton)) {

2
src/storm-dft/parser/DFTGalileoParser.cpp
View File

@ -148,7 +148,7 @@ namespace storm {
ValueType probability = valueParser.parseValue(type.substr(5));
success = builder.addDepElement(name, childNames, probability);
} else if (type.find("=") != std::string::npos) {
success = parseBasicElement(name, line, lineNo, builder, valueParser);
success = parseBasicElement(tokens[0], line, lineNo, builder, valueParser);
} else if (type.find("insp") != std::string::npos) {
// Inspection as defined by DFTCalc
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Inspections (defined in line " << lineNo << ") are not supported.");

5
src/storm-dft/storage/dft/DFT.cpp
View File

@ -799,6 +799,11 @@ namespace storm {
bool sharedSpareMode = false;
std::map<size_t, size_t> bijection;
if (getElement(index1)->isRelevant() || getElement(index2)->isRelevant()) {
// Relevant events need to be uniquely identified and cannot be symmetric.
return {};
}
if (isBasicElement(index1)) {
if (!isBasicElement(index2)) {
return {};

34
src/storm-dft/storage/dft/DFTIsomorphism.h
View File

@ -57,16 +57,16 @@ namespace storage {
BEColourClass() = default;
BEColourClass(storm::storage::BEType t, ValueType a, ValueType p, size_t h) : type(t), hash(h), aRate(a), pRate(p) {
STORM_LOG_ASSERT(t == storm::storage::BEType::EXPONENTIAL, "Expected type EXPONENTIAL but got type " << t);
BEColourClass(storm::storage::BEType type, ValueType active, ValueType passive, size_t parents) : type(type), nrParents(parents), aRate(active), pRate(passive) {
STORM_LOG_ASSERT(type == storm::storage::BEType::EXPONENTIAL, "Expected type EXPONENTIAL but got type " << type);
}
BEColourClass(storm::storage::BEType t, bool fail, size_t h) : type(t), hash(h), failed(fail) {
STORM_LOG_ASSERT(t == storm::storage::BEType::CONSTANT, "Expected type CONSTANT but got type " << t);
BEColourClass(storm::storage::BEType type, bool fail, size_t parents) : type(type), nrParents(parents), failed(fail) {
STORM_LOG_ASSERT(type == storm::storage::BEType::CONSTANT, "Expected type CONSTANT but got type " << type);
}
storm::storage::BEType type;
size_t hash;
size_t nrParents;
ValueType aRate;
ValueType pRate;
bool failed;
@ -80,9 +80,9 @@ namespace storage {
}
switch (lhs.type) {
case storm::storage::BEType::EXPONENTIAL:
return lhs.hash == rhs.hash && lhs.aRate == rhs.aRate && lhs.pRate == rhs.pRate;
return lhs.nrParents == rhs.nrParents && lhs.aRate == rhs.aRate && lhs.pRate == rhs.pRate;
case storm::storage::BEType::CONSTANT:
return lhs.hash == rhs.hash && lhs.failed == rhs.failed;
return lhs.nrParents == rhs.nrParents && lhs.failed == rhs.failed;
default:
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "BE of type '" << lhs.type << "' is not known.");
break;
@ -491,7 +491,12 @@ namespace storage {
// We can skip BEs, as they are identified by they're homomorphic if they are in the same class
for(auto const& indexpair : bijection) {
// Check type first. Colouring takes care of a lot, but not necesarily everything (e.g. voting thresholds)
equalType(*dft.getElement(indexpair.first), *dft.getElement(indexpair.second));
if (!equalType(*dft.getElement(indexpair.first), *dft.getElement(indexpair.second))) {
return false;
}
if (dft.getElement(indexpair.first)->isRelevant() || dft.getElement(indexpair.second)->isRelevant()) {
return false;
}
if(dft.isGate(indexpair.first)) {
STORM_LOG_ASSERT(dft.isGate(indexpair.second), "Element is no gate.");
auto const& lGate = dft.getGate(indexpair.first);
@ -699,22 +704,25 @@ namespace std {
template<typename ValueType>
struct hash<storm::storage::BEColourClass<ValueType>> {
size_t operator()(storm::storage::BEColourClass<ValueType> const& bcc) const {
constexpr uint_fast64_t fivebitmask = (1 << 6) - 1;
constexpr uint_fast64_t eightbitmask = (1 << 9) - 1;
constexpr uint_fast64_t fivebitmask = (1ul << 6) - 1ul;
constexpr uint_fast64_t eightbitmask = (1ul << 9) - 1ul;
constexpr uint_fast64_t fortybitmask = (1ul << 41) - 1ul;
std::hash<ValueType> hasher;
uint_fast64_t groupHash = static_cast<uint_fast64_t>(1) << 63;
groupHash |= (static_cast<uint_fast64_t>(bcc.type) & fivebitmask) << (62 - 5);
switch (bcc.type) {
case storm::storage::BEType::CONSTANT:
return (bcc.failed << 8);
groupHash |= (static_cast<uint_fast64_t>(bcc.failed) & fortybitmask) << 8;
break;
case storm::storage::BEType::EXPONENTIAL:
return (hasher(bcc.aRate) ^ hasher(bcc.pRate) << 8);
groupHash |= ((hasher(bcc.aRate) ^ hasher(bcc.pRate)) & fortybitmask) << 8;
break;
default:
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "BE of type '" << bcc.type << "' is not known.");
break;
}
groupHash |= static_cast<uint_fast64_t>(bcc.hash) & eightbitmask;
groupHash |= static_cast<uint_fast64_t>(bcc.nrParents) & eightbitmask;
return groupHash;
}
};

18
src/storm-dft/utility/FDEPConflictFinder.cpp
View File

@ -25,29 +25,29 @@ namespace storm {
if (dft.getDynamicBehavior()[dep1Index] && dft.getDynamicBehavior()[dep2Index]) {
if (useSMT) { // if an SMT solver is to be used
if (dft.getDependency(dep1Index)->triggerEvent() == dft.getDependency(dep2Index)->triggerEvent()) {
STORM_LOG_DEBUG("Conflict between " << dft.getElement(dep1Index)->name() << " and " << dft.getElement(dep2Index)->name() << ": Same trigger");
STORM_LOG_TRACE("Conflict between " << dft.getElement(dep1Index)->name() << " and " << dft.getElement(dep2Index)->name() << ": Same trigger");
res.emplace_back(std::pair<uint64_t, uint64_t>(dep1Index, dep2Index));
} else {
switch (smtChecker->checkDependencyConflict(dep1Index, dep2Index, timeout)) {
case storm::solver::SmtSolver::CheckResult::Sat:
STORM_LOG_DEBUG("Conflict between " << dft.getElement(dep1Index)->name() << " and " << dft.getElement(dep2Index)->name());
STORM_LOG_TRACE("Conflict between " << dft.getElement(dep1Index)->name() << " and " << dft.getElement(dep2Index)->name());
res.emplace_back(std::pair<uint64_t, uint64_t>(dep1Index, dep2Index));
break;
case storm::solver::SmtSolver::CheckResult::Unknown:
STORM_LOG_DEBUG("Unknown: Conflict between " << dft.getElement(dep1Index)->name() << " and " << dft.getElement(dep2Index)->name());
STORM_LOG_TRACE("Unknown: Conflict between " << dft.getElement(dep1Index)->name() << " and " << dft.getElement(dep2Index)->name());
res.emplace_back(std::pair<uint64_t, uint64_t>(dep1Index, dep2Index));
break;
default:
STORM_LOG_DEBUG("No conflict between " << dft.getElement(dep1Index)->name() << " and " << dft.getElement(dep2Index)->name());
STORM_LOG_TRACE("No conflict between " << dft.getElement(dep1Index)->name() << " and " << dft.getElement(dep2Index)->name());
break;
}
}
} else {
STORM_LOG_DEBUG("Conflict between " << dft.getElement(dep1Index)->name() << " and " << dft.getElement(dep2Index)->name());
STORM_LOG_TRACE("Conflict between " << dft.getElement(dep1Index)->name() << " and " << dft.getElement(dep2Index)->name());
res.emplace_back(std::pair<uint64_t, uint64_t>(dep1Index, dep2Index));
}
} else {
STORM_LOG_DEBUG("Static behavior: No conflict between " << dft.getElement(dep1Index)->name() << " and " << dft.getElement(dep2Index)->name());
STORM_LOG_TRACE("Static behavior: No conflict between " << dft.getElement(dep1Index)->name() << " and " << dft.getElement(dep2Index)->name());
break;
}
}
@ -70,10 +70,10 @@ namespace storm {
for (size_t j = i + 1; j < dft.getDependencies().size(); ++j) {
dep2Index = dft.getDependencies().at(j);
if (dft.getDynamicBehavior()[dep1Index] && dft.getDynamicBehavior()[dep2Index]) {
STORM_LOG_DEBUG("Conflict between " << dft.getElement(dep1Index)->name() << " and " << dft.getElement(dep2Index)->name());
STORM_LOG_TRACE("Conflict between " << dft.getElement(dep1Index)->name() << " and " << dft.getElement(dep2Index)->name());
res.emplace_back(std::pair<uint64_t, uint64_t>(dep1Index, dep2Index));
} else {
STORM_LOG_DEBUG("Static behavior: No conflict between " << dft.getElement(dep1Index)->name() << " and " << dft.getElement(dep2Index)->name());
STORM_LOG_TRACE("Static behavior: No conflict between " << dft.getElement(dep1Index)->name() << " and " << dft.getElement(dep2Index)->name());
break;
}
}
@ -88,4 +88,4 @@ namespace storm {
class FDEPConflictFinder<storm::RationalFunction>;
}
}
}
}

3
src/storm-gspn/parser/GreatSpnEditorProjectParser.cpp
View File

@ -88,7 +88,8 @@ namespace storm {
if (name.compare("name") == 0) {
builder.setGspnName(storm::adapters::XMLtoString(attr->getNodeValue()));
} else if (name.compare("show-color-cmd") == 0 ||
name.compare("show-fluid-cmd") == 0) {
name.compare("show-fluid-cmd") == 0 ||
name.compare("zoom") == 0) {
// ignore node
} else {
// Found node or attribute which is at the moment not handled by this parser.

24
src/test/storm-dft/api/DftModelBuildingTest.cpp
View File

@ -19,17 +19,18 @@ namespace {
// Set relevant events (none)
std::set<size_t> relevantEvents;
dft->setRelevantEvents(relevantEvents, false);
// Build model
storm::builder::ExplicitDFTModelBuilder<double> builder(*dft, symmetries, relevantEvents, false);
storm::builder::ExplicitDFTModelBuilder<double> builder(*dft, symmetries);
builder.buildModel(0, 0.0);
std::shared_ptr<storm::models::sparse::Model<double>> model = builder.getModel();
EXPECT_EQ(8ul, model->getNumberOfStates());
EXPECT_EQ(13ul, model->getNumberOfTransitions());
// Set relevant events (all)
relevantEvents = dft->getAllIds();
dft->setRelevantEvents(dft->getAllIds(), false);
// Build model
storm::builder::ExplicitDFTModelBuilder<double> builder2(*dft, symmetries, relevantEvents, false);
storm::builder::ExplicitDFTModelBuilder<double> builder2(*dft, symmetries);
builder2.buildModel(0, 0.0);
model = builder2.getModel();
EXPECT_EQ(512ul, model->getNumberOfStates());
@ -38,8 +39,9 @@ namespace {
// Set relevant events (H)
relevantEvents.clear();
relevantEvents.insert(dft->getIndex("H"));
dft->setRelevantEvents(relevantEvents, false);
// Build model
storm::builder::ExplicitDFTModelBuilder<double> builder3(*dft, symmetries, relevantEvents, false);
storm::builder::ExplicitDFTModelBuilder<double> builder3(*dft, symmetries);
builder3.buildModel(0, 0.0);
model = builder3.getModel();
EXPECT_EQ(12ul, model->getNumberOfStates());
@ -50,8 +52,9 @@ namespace {
relevantEvents.clear();
relevantEvents.insert(dft->getIndex("H"));
relevantEvents.insert(dft->getIndex("I"));
dft->setRelevantEvents(relevantEvents, false);
// Build model
storm::builder::ExplicitDFTModelBuilder<double> builder4(*dft, symmetries, relevantEvents, false);
storm::builder::ExplicitDFTModelBuilder<double> builder4(*dft, symmetries);
builder4.buildModel(0, 0.0);
model = builder4.getModel();
EXPECT_EQ(16ul, model->getNumberOfStates());
@ -59,17 +62,18 @@ namespace {
// Set relevant events (none)
relevantEvents.clear();
dft->setRelevantEvents(relevantEvents, true);
// Build model
storm::builder::ExplicitDFTModelBuilder<double> builder5(*dft, symmetries, relevantEvents, true);
storm::builder::ExplicitDFTModelBuilder<double> builder5(*dft, symmetries);
builder5.buildModel(0, 0.0);
model = builder5.getModel();
EXPECT_EQ(8ul, model->getNumberOfStates());
EXPECT_EQ(13ul, model->getNumberOfTransitions());
// Set relevant events (all)
relevantEvents = dft->getAllIds();
dft->setRelevantEvents(dft->getAllIds(), true);
// Build model
storm::builder::ExplicitDFTModelBuilder<double> builder6(*dft, symmetries, relevantEvents, true);
storm::builder::ExplicitDFTModelBuilder<double> builder6(*dft, symmetries);
builder6.buildModel(0, 0.0);
model = builder6.getModel();
EXPECT_EQ(8ul, model->getNumberOfStates());
@ -80,13 +84,13 @@ namespace {
relevantEvents.clear();
relevantEvents.insert(dft->getIndex("H"));
relevantEvents.insert(dft->getIndex("I"));
dft->setRelevantEvents(relevantEvents, true);
// Build model
storm::builder::ExplicitDFTModelBuilder<double> builder7(*dft, symmetries, relevantEvents, true);
storm::builder::ExplicitDFTModelBuilder<double> builder7(*dft, symmetries);
builder7.buildModel(0, 0.0);
model = builder7.getModel();
EXPECT_EQ(8ul, model->getNumberOfStates());
EXPECT_EQ(13ul, model->getNumberOfTransitions());
}
}
Write Preview
Loading…
Cancel
Save