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

DFT wellformedness check can be performed stricter as precondition for analysis

main
Matthias Volk 6 years ago
parent
1767c40f2d
commit
fab86e8823
10 changed files with 62 additions and 45 deletions
Split View
  1. 8
      src/storm-dft-cli/storm-dft.cpp
  2. 9
      src/storm-dft/api/storm-dft.h
  3. 39
      src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
  4. 17
      src/storm-dft/storage/dft/DFT.cpp
  5. 4
      src/storm-dft/storage/dft/DFT.h
  6. 4
      src/test/storm-dft/api/DftApproximationTest.cpp
  7. 2
      src/test/storm-dft/api/DftModelBuildingTest.cpp
  8. 4
      src/test/storm-dft/api/DftModelCheckerTest.cpp
  9. 4
      src/test/storm-dft/api/DftParserTest.cpp
  10. 16
      src/test/storm-dft/api/DftSmtTest.cpp

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

@ -5,7 +5,7 @@
#include "storm-dft/settings/modules/DftGspnSettings.h"
#include "storm-dft/settings/modules/DftIOSettings.h"
#include "storm-dft/settings/modules/FaultTreeSettings.h"
#include <storm/exceptions/UnmetRequirementException.h>
#include "storm/exceptions/UnmetRequirementException.h"
#include "storm/settings/modules/GeneralSettings.h"
#include "storm/settings/modules/DebugSettings.h"
#include "storm/settings/modules/IOSettings.h"
@ -66,10 +66,8 @@ void processOptions() {
dft = dftTransformator.transformBinaryFDEPs(*dft);
}
// Check well-formedness of DFT
std::stringstream stream;
if (!dft->checkWellFormedness(stream)) {
STORM_LOG_THROW(false, storm::exceptions::UnmetRequirementException, "DFT is not well-formed: " << stream.str());
}
auto wellFormedResult = storm::api::isWellFormed(*dft, false);
STORM_LOG_THROW(wellFormedResult.first, storm::exceptions::UnmetRequirementException, "DFT is not well-formed: " << wellFormedResult.second);
if (dftGspnSettings.isTransformToGspn()) {
// Transform to GSPN

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

@ -1,6 +1,7 @@
#pragma once
#include <type_traits>
#include <utility>
#include "storm-dft/parser/DFTGalileoParser.h"
#include "storm-dft/parser/DFTJsonParser.h"
@ -59,12 +60,14 @@ namespace storm {
* Check whether the DFT is well-formed.
*
* @param dft DFT.
* @return True iff the DFT is well-formed.
* @param validForAnalysis If true, additional (more restrictive) checks are performed to check whether the DFT is valid for analysis.
* @return Pair where the first entry is true iff the DFT is well-formed. The second entry contains the error messages for illformed parts.
*/
template<typename ValueType>
bool isWellFormed(storm::storage::DFT<ValueType> const& dft) {
std::pair<bool, std::string> isWellFormed(storm::storage::DFT<ValueType> const& dft, bool validForAnalysis = true) {
std::stringstream stream;
return dft.checkWellFormedness(stream);
bool wellFormed = dft.checkWellFormedness(validForAnalysis, stream);
return std::pair<bool, std::string>(wellFormed, stream.str());
}
/*!

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

@ -3,12 +3,14 @@
#include "storm/settings/modules/IOSettings.h"
#include "storm/settings/modules/GeneralSettings.h"
#include "storm/builder/ParallelCompositionBuilder.h"
#include "storm/exceptions/UnmetRequirementException.h"
#include "storm/utility/bitoperations.h"
#include "storm/utility/DirectEncodingExporter.h"
#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h"
#include "storm/models/ModelType.h"
#include "storm-dft/api/storm-dft.h"
#include "storm-dft/builder/ExplicitDFTModelBuilder.h"
#include "storm-dft/storage/dft/DFTIsomorphism.h"
#include "storm-dft/settings/modules/FaultTreeSettings.h"
@ -18,16 +20,19 @@ namespace storm {
namespace modelchecker {
template<typename ValueType>
typename DFTModelChecker<ValueType>::dft_results
DFTModelChecker<ValueType>::check(storm::storage::DFT<ValueType> const &origDft,
std::vector<std::shared_ptr<const storm::logic::Formula>> const &properties,
bool symred, bool allowModularisation, std::set<size_t> const &relevantEvents,
bool allowDCForRelevantEvents, double approximationError,
storm::builder::ApproximationHeuristic approximationHeuristic,
bool eliminateChains, bool ignoreLabeling) {
typename DFTModelChecker<ValueType>::dft_results DFTModelChecker<ValueType>::check(storm::storage::DFT<ValueType> const& origDft,
std::vector<std::shared_ptr<const storm::logic::Formula>> const& properties, bool symred,
bool allowModularisation, std::set<size_t> const& relevantEvents,
bool allowDCForRelevantEvents, double approximationError,
storm::builder::ApproximationHeuristic approximationHeuristic, bool eliminateChains,
bool ignoreLabeling) {
totalTimer.start();
dft_results results;
// Check well-formedness of DFT
auto wellFormedResult = storm::api::isWellFormed(origDft, true);
STORM_LOG_THROW(wellFormedResult.first, storm::exceptions::UnmetRequirementException, "DFT is not well-formed for analysis: " << wellFormedResult.second);
// Optimizing DFT
storm::storage::DFT<ValueType> dft = origDft.optimize();
@ -37,18 +42,14 @@ namespace storm {
// TODO: distinguish for all properties, not only for first one
if (properties[0]->isTimeOperatorFormula() && allowModularisation) {
// Use parallel composition as modularisation approach for expected time
std::shared_ptr<storm::models::sparse::Model<ValueType>> model = buildModelViaComposition(dft,
properties,
symred, true,
relevantEvents);
std::shared_ptr<storm::models::sparse::Model<ValueType>> model = buildModelViaComposition(dft, properties, symred, true, relevantEvents);
// Model checking
std::vector<ValueType> resultsValue = checkModel(model, properties);
for (ValueType result : resultsValue) {
results.push_back(result);
}
} else {
results = checkHelper(dft, properties, symred, allowModularisation, relevantEvents,
allowDCForRelevantEvents, approximationError, approximationHeuristic,
results = checkHelper(dft, properties, symred, allowModularisation, relevantEvents, allowDCForRelevantEvents, approximationError, approximationHeuristic,
eliminateChains, ignoreLabeling);
}
totalTimer.stop();
@ -56,13 +57,11 @@ namespace storm {
}
template<typename ValueType>
typename DFTModelChecker<ValueType>::dft_results
DFTModelChecker<ValueType>::checkHelper(storm::storage::DFT<ValueType> const &dft,
property_vector const &properties, bool symred,
bool allowModularisation, std::set<size_t> const &relevantEvents,
bool allowDCForRelevantEvents, double approximationError,
storm::builder::ApproximationHeuristic approximationHeuristic,
bool eliminateChains, bool ignoreLabeling) {
typename DFTModelChecker<ValueType>::dft_results DFTModelChecker<ValueType>::checkHelper(storm::storage::DFT<ValueType> const& dft, property_vector const& properties,
bool symred, bool allowModularisation, std::set<size_t> const& relevantEvents,
bool allowDCForRelevantEvents, double approximationError,
storm::builder::ApproximationHeuristic approximationHeuristic,
bool eliminateChains, bool ignoreLabeling) {
STORM_LOG_TRACE("Check helper called");
std::vector<storm::storage::DFT<ValueType>> dfts;
bool invResults = false;

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

@ -760,7 +760,7 @@ namespace storm {
}
template<typename ValueType>
bool DFT<ValueType>::checkWellFormedness(std::ostream& stream) const {
bool DFT<ValueType>::checkWellFormedness(bool validForAnalysis, std::ostream& stream) const {
bool wellformed = true;
// Check independence of spare modules
// TODO: comparing one element of each spare module sufficient?
@ -776,6 +776,21 @@ namespace storm {
}
}
}
if (validForAnalysis) {
// Check that each dependency is binary
for (size_t idDependency : this->getDependencies()) {
std::shared_ptr<DFTDependency<ValueType> const> dependency = this->getDependency(idDependency);
if (dependency->dependentEvents().size() != 1) {
if (!wellformed) {
stream << std::endl;
}
stream << "Dependency '" << dependency->name() << "' is not binary.";
wellformed = false;
}
}
}
// TODO check VOT gates
// TODO check only one constant failed event
return wellformed;

4
src/storm-dft/storage/dft/DFT.h
View File

@ -243,10 +243,12 @@ namespace storm {
/*!
* Check if the DFT is well-formed.
*
* @param validForAnalysis If true, additional (more restrictive) checks are performed to check whether the DFT is valid for analysis.
* @param stream Output stream where warnings about non-well-formed parts are written.
* @return True iff the DFT is well-formed.
*/
bool checkWellFormedness(std::ostream& stream) const;
bool checkWellFormedness(bool validForAnalysis, std::ostream& stream) const;
uint64_t maxRank() const;

4
src/test/storm-dft/api/DftApproximationTest.cpp
View File

@ -54,7 +54,7 @@ namespace {
std::pair<double, double> analyzeMTTF(std::string const& file, double errorBound) {
std::shared_ptr<storm::storage::DFT<double>> dft = storm::api::loadDFTGalileoFile<double>(file);
EXPECT_TRUE(storm::api::isWellFormed(*dft));
EXPECT_TRUE(storm::api::isWellFormed(*dft).first);
std::string property = "T=? [F \"failed\"]";
std::vector<std::shared_ptr<storm::logic::Formula const>> properties = storm::api::extractFormulasFromProperties(storm::api::parseProperties(property));
typename storm::modelchecker::DFTModelChecker<double>::dft_results results = storm::api::analyzeDFT<double>(*dft, properties, config.useSR, false, {}, true, errorBound,
@ -64,7 +64,7 @@ namespace {
std::pair<double, double> analyzeTimebound(std::string const& file, double timeBound, double errorBound) {
std::shared_ptr<storm::storage::DFT<double>> dft = storm::api::loadDFTGalileoFile<double>(file);
EXPECT_TRUE(storm::api::isWellFormed(*dft));
EXPECT_TRUE(storm::api::isWellFormed(*dft).first);
std::stringstream propertyStream;
propertyStream << "P=? [F<=" << timeBound << " \"failed\"]";
std::vector <std::shared_ptr<storm::logic::Formula const>> properties = storm::api::extractFormulasFromProperties(storm::api::parseProperties(propertyStream.str()));

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

@ -11,7 +11,7 @@ namespace {
// Initialize
std::string file = STORM_TEST_RESOURCES_DIR "/dft/dont_care.dft";
std::shared_ptr<storm::storage::DFT<double>> dft = storm::api::loadDFTGalileoFile<double>(file);
EXPECT_TRUE(storm::api::isWellFormed(*dft));
EXPECT_TRUE(storm::api::isWellFormed(*dft).first);
std::string property = "Tmin=? [F \"failed\"]";
std::vector<std::shared_ptr<storm::logic::Formula const>> properties = storm::api::extractFormulasFromProperties(storm::api::parseProperties(property));
std::map<size_t, std::vector<std::vector<size_t>>> emptySymmetry;

4
src/test/storm-dft/api/DftModelCheckerTest.cpp
View File

@ -77,7 +77,7 @@ namespace {
storm::transformations::dft::DftTransformator<double> dftTransformator = storm::transformations::dft::DftTransformator<double>();
std::shared_ptr<storm::storage::DFT<double>> dft = dftTransformator.transformBinaryFDEPs(
*(storm::api::loadDFTGalileoFile<double>(file)));
EXPECT_TRUE(storm::api::isWellFormed(*dft));
EXPECT_TRUE(storm::api::isWellFormed(*dft).first);
std::string property = "Tmin=? [F \"failed\"]";
std::vector<std::shared_ptr<storm::logic::Formula const>> properties = storm::api::extractFormulasFromProperties(storm::api::parseProperties(property));
std::set<size_t> relevantEvents;
@ -92,7 +92,7 @@ namespace {
double analyzeReliability(std::string const &file, double bound) {
storm::transformations::dft::DftTransformator<double> dftTransformator = storm::transformations::dft::DftTransformator<double>();
std::shared_ptr<storm::storage::DFT<double>> dft = dftTransformator.transformBinaryFDEPs(*(storm::api::loadDFTGalileoFile<double>(file)));
EXPECT_TRUE(storm::api::isWellFormed(*dft));
EXPECT_TRUE(storm::api::isWellFormed(*dft).first);
std::string property = "Pmin=? [F<=" + std::to_string(bound) + " \"failed\"]";
std::vector<std::shared_ptr<storm::logic::Formula const>> properties = storm::api::extractFormulasFromProperties(
storm::api::parseProperties(property));

4
src/test/storm-dft/api/DftParserTest.cpp
View File

@ -10,7 +10,7 @@ namespace {
std::shared_ptr<storm::storage::DFT<double>> dft = storm::api::loadDFTGalileoFile<double>(file);
EXPECT_EQ(3ul, dft->nrElements());
EXPECT_EQ(2ul, dft->nrBasicElements());
EXPECT_TRUE(storm::api::isWellFormed(*dft));
EXPECT_TRUE(storm::api::isWellFormed(*dft).first);
}
TEST(DftParserTest, LoadFromJsonFile) {
@ -18,7 +18,7 @@ namespace {
std::shared_ptr<storm::storage::DFT<double>> dft = storm::api::loadDFTJsonFile<double>(file);
EXPECT_EQ(3ul, dft->nrElements());
EXPECT_EQ(2ul, dft->nrBasicElements());
EXPECT_TRUE(storm::api::isWellFormed(*dft));
EXPECT_TRUE(storm::api::isWellFormed(*dft).first);
}
TEST(DftParserTest, CatchCycles) {

16
src/test/storm-dft/api/DftSmtTest.cpp
View File

@ -7,7 +7,7 @@ namespace {
TEST(DftSmtTest, AndTest) {
std::shared_ptr<storm::storage::DFT<double>> dft =
storm::api::loadDFTGalileoFile<double>(STORM_TEST_RESOURCES_DIR "/dft/and.dft");
EXPECT_TRUE(storm::api::isWellFormed(*dft));
EXPECT_TRUE(storm::api::isWellFormed(*dft).first);
storm::modelchecker::DFTASFChecker smtChecker(*dft);
smtChecker.convert();
smtChecker.toSolver();
@ -17,7 +17,7 @@ namespace {
TEST(DftSmtTest, PandTest) {
std::shared_ptr<storm::storage::DFT<double>> dft =
storm::api::loadDFTGalileoFile<double>(STORM_TEST_RESOURCES_DIR "/dft/pand.dft");
EXPECT_TRUE(storm::api::isWellFormed(*dft));
EXPECT_TRUE(storm::api::isWellFormed(*dft).first);
storm::modelchecker::DFTASFChecker smtChecker(*dft);
smtChecker.convert();
smtChecker.toSolver();
@ -27,7 +27,7 @@ namespace {
TEST(DftSmtTest, SpareTest) {
std::shared_ptr<storm::storage::DFT<double>> dft =
storm::api::loadDFTGalileoFile<double>(STORM_TEST_RESOURCES_DIR "/dft/spare_two_modules.dft");
EXPECT_TRUE(storm::api::isWellFormed(*dft));
EXPECT_TRUE(storm::api::isWellFormed(*dft).first);
storm::modelchecker::DFTASFChecker smtChecker(*dft);
smtChecker.convert();
smtChecker.toSolver();
@ -38,7 +38,7 @@ namespace {
TEST(DftSmtTest, BoundTest) {
std::shared_ptr<storm::storage::DFT<double>> dft =
storm::api::loadDFTGalileoFile<double>(STORM_TEST_RESOURCES_DIR "/dft/spare5.dft");
EXPECT_TRUE(storm::api::isWellFormed(*dft));
EXPECT_TRUE(storm::api::isWellFormed(*dft).first);
storm::modelchecker::DFTASFChecker smtChecker(*dft);
smtChecker.convert();
smtChecker.toSolver();
@ -49,7 +49,7 @@ namespace {
TEST(DftSmtTest, FDEPBoundTest) {
std::shared_ptr<storm::storage::DFT<double>> dft =
storm::api::loadDFTGalileoFile<double>(STORM_TEST_RESOURCES_DIR "/dft/fdep_bound.dft");
EXPECT_TRUE(storm::api::isWellFormed(*dft));
EXPECT_TRUE(storm::api::isWellFormed(*dft, false).first);
storm::modelchecker::DFTASFChecker smtChecker(*dft);
smtChecker.convert();
smtChecker.toSolver();
@ -60,7 +60,7 @@ namespace {
TEST(DftSmtTest, FDEPConflictTest) {
std::shared_ptr<storm::storage::DFT<double>> dft =
storm::api::loadDFTGalileoFile<double>(STORM_TEST_RESOURCES_DIR "/dft/spare_conflict_test.dft");
EXPECT_TRUE(storm::api::isWellFormed(*dft));
EXPECT_TRUE(storm::api::isWellFormed(*dft).first);
std::vector<bool> true_vector(10, true);
dft->setDynamicBehaviorInfo();
@ -72,7 +72,7 @@ namespace {
TEST(DftSmtTest, FDEPConflictSPARETest) {
std::shared_ptr<storm::storage::DFT<double>> dft =
storm::api::loadDFTGalileoFile<double>(STORM_TEST_RESOURCES_DIR "/dft/spare_conflict_test.dft");
EXPECT_TRUE(storm::api::isWellFormed(*dft));
EXPECT_TRUE(storm::api::isWellFormed(*dft).first);
std::vector<bool> true_vector(10, true);
dft->setDynamicBehaviorInfo();
@ -84,7 +84,7 @@ namespace {
TEST(DftSmtTest, FDEPConflictSEQTest) {
std::shared_ptr<storm::storage::DFT<double>> dft =
storm::api::loadDFTGalileoFile<double>(STORM_TEST_RESOURCES_DIR "/dft/seq_conflict_test.dft");
EXPECT_TRUE(storm::api::isWellFormed(*dft));
EXPECT_TRUE(storm::api::isWellFormed(*dft).first);
std::vector<bool> expected_dynamic_vector(dft->nrElements(), true);
expected_dynamic_vector.at(dft->getTopLevelIndex()) = false;

Write Preview
|||||||
100:0
Loading…
Cancel
Save