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

Support for checking multiple dft properties at once

tempestpy_adaptions
Matthias Volk 8 years ago
parent
d1b86c8f35
commit
cd1bd6b538
3 changed files with 258 additions and 224 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. 86
      src/storm-dft-cli/storm-dyftee.cpp
  2. 358
      src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
  3. 38
      src/storm-dft/modelchecker/dft/DFTModelChecker.h

86
src/storm-dft-cli/storm-dyftee.cpp
View File

@ -34,35 +34,44 @@
#include <memory>
/*!
* Load DFT from filename, build corresponding Model and check against given property.
* Analyse the given DFT according to the given properties.
* We first load the DFT from the given file, then build the corresponding model and last check against the given properties.
*
* @param property PCTC formula capturing the property to check.
* @param properties PCTL formulas capturing the properties to check.
* @param symred Flag whether symmetry reduction should be used.
* @param allowModularisation Flag whether modularisation should be applied if possible.
* @param enableDC Flag whether Don't Care propagation should be used.
* @param approximationError Allowed approximation error.
*/
template <typename ValueType>
void analyzeDFT(std::string property, bool symred, bool allowModularisation, bool enableDC, double approximationError) {
void analyzeDFT(std::vector<std::string> const& properties, bool symred, bool allowModularisation, bool enableDC, double approximationError) {
storm::settings::modules::DFTSettings const& dftSettings = storm::settings::getModule<storm::settings::modules::DFTSettings>();
std::shared_ptr<storm::storage::DFT<ValueType>> dft;
// Build DFT from given file.
if (dftSettings.isDftJsonFileSet()) {
storm::parser::DFTJsonParser<ValueType> parser;
std::cout << "Running DFT analysis on file " << dftSettings.getDftJsonFilename() << " with property " << property << std::endl;
std::cout << "Loading DFT from file " << dftSettings.getDftJsonFilename() << std::endl;
dft = std::make_shared<storm::storage::DFT<ValueType>>(parser.parseJson(dftSettings.getDftJsonFilename()));
} else {
storm::parser::DFTGalileoParser<ValueType> parser;
std::cout << "Running DFT analysis on file " << dftSettings.getDftFilename() << " with property " << property << std::endl;
std::cout << "Loading DFT from file " << dftSettings.getDftFilename() << std::endl;
dft = std::make_shared<storm::storage::DFT<ValueType>>(parser.parseDFT(dftSettings.getDftFilename()));
}
std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForExplicit(property));
STORM_LOG_ASSERT(formulas.size() == 1, "Wrong number of formulas.");
// Build properties
std::string propString = properties[0];
for (size_t i = 1; i < properties.size(); ++i) {
propString += ";" + properties[i];
}
std::vector<std::shared_ptr<storm::logic::Formula const>> props = storm::extractFormulasFromProperties(storm::parsePropertiesForExplicit(propString));
STORM_LOG_ASSERT(props.size() > 0, "No properties found.");
// Check model
storm::modelchecker::DFTModelChecker<ValueType> modelChecker;
modelChecker.check(*dft, formulas[0], symred, allowModularisation, enableDC, approximationError);
modelChecker.check(*dft, props, symred, allowModularisation, enableDC, approximationError);
modelChecker.printTimings();
modelChecker.printResult();
modelChecker.printResults();
}
/*!
@ -210,43 +219,42 @@ int main(const int argc, const char** argv) {
#endif
// Set min or max
bool minimal = true;
std::string optimizationDirection = "min";
if (dftSettings.isComputeMaximalValue()) {
STORM_LOG_THROW(!dftSettings.isComputeMinimalValue(), storm::exceptions::InvalidSettingsException, "Cannot compute minimal and maximal values at the same time.");
minimal = false;
optimizationDirection = "max";
}
// Construct pctlFormula
std::string pctlFormula = "";
std::string operatorType = "";
std::string targetFormula = "";
// Construct properties to check for
std::vector<std::string> properties;
if (generalSettings.isPropertySet()) {
STORM_LOG_THROW(!dftSettings.usePropExpectedTime() && !dftSettings.usePropProbability() && !dftSettings.usePropTimebound(), storm::exceptions::InvalidSettingsException, "More than one property given.");
pctlFormula = generalSettings.getProperty();
} else if (dftSettings.usePropExpectedTime()) {
STORM_LOG_THROW(!dftSettings.usePropProbability() && !dftSettings.usePropTimebound(), storm::exceptions::InvalidSettingsException, "More than one property given.");
operatorType = "T";
targetFormula = "F \"failed\"";
} else if (dftSettings.usePropProbability()) {
STORM_LOG_THROW(!dftSettings.usePropTimebound(), storm::exceptions::InvalidSettingsException, "More than one property given.");
operatorType = "P";;
targetFormula = "F \"failed\"";
} else {
STORM_LOG_THROW(dftSettings.usePropTimebound(), storm::exceptions::InvalidSettingsException, "No property given.");
properties.push_back(generalSettings.getProperty());
}
if (dftSettings.usePropExpectedTime()) {
properties.push_back("T" + optimizationDirection + "=? [F \"failed\"]");
}
if (dftSettings.usePropProbability()) {
properties.push_back("P" + optimizationDirection + "=? [F \"failed\"]");
}
if (dftSettings.usePropTimebound()) {
std::stringstream stream;
stream << "F<=" << dftSettings.getPropTimebound() << " \"failed\"";
operatorType = "P";
targetFormula = stream.str();
stream << "P" << optimizationDirection << "=? [F<=" << dftSettings.getPropTimebound() << " \"failed\"]";
properties.push_back(stream.str());
}
if (!targetFormula.empty()) {
STORM_LOG_ASSERT(pctlFormula.empty(), "Pctl formula not empty.");
pctlFormula = operatorType + (minimal ? "min" : "max") + "=?[" + targetFormula + "]";
if (dftSettings.usePropTimepoints()) {
for (double timepoint : dftSettings.getPropTimepoints()) {
std::stringstream stream;
stream << "P" << optimizationDirection << "=? [F<=" << timepoint << " \"failed\"]";
properties.push_back(stream.str());
}
}
if (properties.empty()) {
STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No property given.");
}
STORM_LOG_ASSERT(!pctlFormula.empty(), "Pctl formula empty.");
// Set possible approximation error
double approximationError = 0.0;
if (dftSettings.isApproximationErrorSet()) {
approximationError = dftSettings.getApproximationError();
@ -255,12 +263,12 @@ int main(const int argc, const char** argv) {
// From this point on we are ready to carry out the actual computations.
if (parametric) {
#ifdef STORM_HAVE_CARL
analyzeDFT<storm::RationalFunction>(pctlFormula, dftSettings.useSymmetryReduction(), dftSettings.useModularisation(), !dftSettings.isDisableDC(), approximationError);
analyzeDFT<storm::RationalFunction>(properties, dftSettings.useSymmetryReduction(), dftSettings.useModularisation(), !dftSettings.isDisableDC(), approximationError);
#else
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Parameters are not supported in this build.");
#endif
} else {
analyzeDFT<double>(pctlFormula, dftSettings.useSymmetryReduction(), dftSettings.useModularisation(), !dftSettings.isDisableDC(), approximationError);
analyzeDFT<double>(properties, dftSettings.useSymmetryReduction(), dftSettings.useModularisation(), !dftSettings.isDisableDC(), approximationError);
}
// All operations have now been performed, so we clean up everything and terminate.

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

@ -13,12 +13,7 @@ namespace storm {
namespace modelchecker {
template<typename ValueType>
DFTModelChecker<ValueType>::DFTModelChecker() {
checkResult = storm::utility::zero<ValueType>();
}
template<typename ValueType>
void DFTModelChecker<ValueType>::check(storm::storage::DFT<ValueType> const& origDft, std::shared_ptr<const storm::logic::Formula> const& formula, bool symred, bool allowModularisation, bool enableDC, double approximationError) {
void DFTModelChecker<ValueType>::check(storm::storage::DFT<ValueType> const& origDft, std::vector<std::shared_ptr<const storm::logic::Formula>> const& properties, bool symred, bool allowModularisation, bool enableDC, double approximationError) {
// Initialize
this->approximationError = approximationError;
totalTimer.start();
@ -29,31 +24,31 @@ namespace storm {
// TODO Matthias: check that all paths reach the target state for approximation
// Checking DFT
if (formula->isProbabilityOperatorFormula() || !allowModularisation) {
checkResult = checkHelper(dft, formula, symred, allowModularisation, enableDC, approximationError);
} else {
std::shared_ptr<storm::models::sparse::Model<ValueType>> model = buildModelComposition(dft, formula, symred, allowModularisation, enableDC);
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, enableDC, approximationError);
// Model checking
std::unique_ptr<storm::modelchecker::CheckResult> result = checkModel(model, formula);
result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates()));
checkResult = result->asExplicitQuantitativeCheckResult<ValueType>().getValueMap().begin()->second;
std::vector<ValueType> resultsValue = checkModel(model, properties);
for (ValueType result : resultsValue) {
checkResults.push_back(result);
}
} else {
checkResults = checkHelper(dft, properties, symred, allowModularisation, enableDC, approximationError);
}
totalTimer.stop();
}
template<typename ValueType>
typename DFTModelChecker<ValueType>::dft_result DFTModelChecker<ValueType>::checkHelper(storm::storage::DFT<ValueType> const& dft, std::shared_ptr<const storm::logic::Formula> const& formula, bool symred, bool allowModularisation, bool enableDC, double approximationError) {
typename DFTModelChecker<ValueType>::dft_results DFTModelChecker<ValueType>::checkHelper(storm::storage::DFT<ValueType> const& dft, property_vector const& properties, bool symred, bool allowModularisation, bool enableDC, double approximationError) {
STORM_LOG_TRACE("Check helper called");
bool modularisationPossible = allowModularisation;
std::vector<storm::storage::DFT<ValueType>> dfts;
bool invResults = false;
size_t nrK = 0; // K out of M
size_t nrM = 0; // K out of M
// Try modularisation
if(modularisationPossible) {
bool invResults = false;
std::vector<storm::storage::DFT<ValueType>> dfts;
size_t nrK = 0; // K out of M
size_t nrM = 0; // K out of M
if(allowModularisation) {
switch (dft.topLevelType()) {
case storm::storage::DFTElementType::AND:
STORM_LOG_TRACE("top modularisation called AND");
@ -61,7 +56,6 @@ namespace storm {
STORM_LOG_TRACE("Modularsation into " << dfts.size() << " submodules.");
nrK = dfts.size();
nrM = dfts.size();
modularisationPossible = dfts.size() > 1;
break;
case storm::storage::DFTElementType::OR:
STORM_LOG_TRACE("top modularisation called OR");
@ -70,7 +64,6 @@ namespace storm {
nrK = 0;
nrM = dfts.size();
invResults = true;
modularisationPossible = dfts.size() > 1;
break;
case storm::storage::DFTElementType::VOT:
STORM_LOG_TRACE("top modularisation called VOT");
@ -82,22 +75,29 @@ namespace storm {
nrK -= 1;
invResults = true;
}
modularisationPossible = dfts.size() > 1;
break;
default:
// No static gate -> no modularisation applicable
modularisationPossible = false;
break;
}
}
if(modularisationPossible) {
STORM_LOG_TRACE("Recursive CHECK Call");
if (formula->isProbabilityOperatorFormula()) {
// Perform modularisation
if(dfts.size() > 1) {
STORM_LOG_TRACE("Recursive CHECK Call");
// TODO Matthias: compute simultaneously
dft_results results;
for (auto property : properties) {
if (!property->isProbabilityOperatorFormula()) {
STORM_LOG_WARN("Could not check property: " << *property);
} else {
// Recursively call model checking
std::vector<ValueType> res;
for(auto const ft : dfts) {
dft_result ftResult = checkHelper(ft, formula, symred, true, enableDC, 0.0);
res.push_back(boost::get<ValueType>(ftResult));
// TODO Matthias: allow approximation in modularisation
dft_results ftResults = checkHelper(ft, {property}, symred, true, enableDC, 0.0);
STORM_LOG_ASSERT(ftResults.size() == 1, "Wrong number of results");
res.push_back(boost::get<ValueType>(ftResults[0]));
}
// Combine modularisation results
@ -128,148 +128,138 @@ namespace storm {
if(invResults) {
result = storm::utility::one<ValueType>() - result;
}
return result;
results.push_back(result);
}
}
return results;
} else {
// No modularisation was possible
return checkDFT(dft, properties, symred, enableDC, approximationError);
}
// If we are here, no modularisation was possible
STORM_LOG_ASSERT(!modularisationPossible, "Modularisation should not be possible.");
return checkDFT(dft, formula, symred, enableDC, approximationError);
}
template<typename ValueType>
std::shared_ptr<storm::models::sparse::Ctmc<ValueType>> DFTModelChecker<ValueType>::buildModelComposition(storm::storage::DFT<ValueType> const& dft, std::shared_ptr<const storm::logic::Formula> const& formula, bool symred, bool allowModularisation, bool enableDC) {
std::shared_ptr<storm::models::sparse::Ctmc<ValueType>> DFTModelChecker<ValueType>::buildModelViaComposition(storm::storage::DFT<ValueType> const& dft, property_vector const& properties, bool symred, bool allowModularisation, bool enableDC, double approximationError) {
// TODO Matthias: use approximation?
STORM_LOG_TRACE("Build model via composition");
// Use parallel composition for CTMCs for expected time
STORM_LOG_ASSERT(formula->isTimeOperatorFormula(), "Formula is not a time operator formula");
bool modularisationPossible = allowModularisation;
std::vector<storm::storage::DFT<ValueType>> dfts;
bool isAnd = true;
// Try modularisation
if(modularisationPossible) {
std::vector<storm::storage::DFT<ValueType>> dfts;
bool isAnd = true;
if(allowModularisation) {
switch (dft.topLevelType()) {
case storm::storage::DFTElementType::AND:
STORM_LOG_TRACE("top modularisation called AND");
dfts = dft.topModularisation();
STORM_LOG_TRACE("Modularisation into " << dfts.size() << " submodules.");
modularisationPossible = dfts.size() > 1;
isAnd = true;
break;
case storm::storage::DFTElementType::OR:
STORM_LOG_TRACE("top modularisation called OR");
dfts = dft.topModularisation();
STORM_LOG_TRACE("Modularsation into " << dfts.size() << " submodules.");
modularisationPossible = dfts.size() > 1;
isAnd = false;
break;
case storm::storage::DFTElementType::VOT:
/*STORM_LOG_TRACE("top modularisation called VOT");
dfts = dft.topModularisation();
STORM_LOG_TRACE("Modularsation into " << dfts.size() << " submodules.");
std::static_pointer_cast<storm::storage::DFTVot<ValueType> const>(dft.getTopLevelGate())->threshold();
*/
// TODO enable modularisation for voting gate
modularisationPossible = false;
break;
default:
// No static gate -> no modularisation applicable
modularisationPossible = false;
break;
}
}
if(modularisationPossible) {
STORM_LOG_TRACE("Recursive CHECK Call");
bool firstTime = true;
std::shared_ptr<storm::models::sparse::Ctmc<ValueType>> composedModel;
for (auto const ft : dfts) {
STORM_LOG_INFO("Building Model via parallel composition...");
explorationTimer.start();
// Perform modularisation via parallel composition
if(dfts.size() > 1) {
STORM_LOG_TRACE("Recursive CHECK Call");
bool firstTime = true;
std::shared_ptr<storm::models::sparse::Ctmc<ValueType>> composedModel;
for (auto const ft : dfts) {
STORM_LOG_INFO("Building Model via parallel composition...");
explorationTimer.start();
// Find symmetries
std::map<size_t, std::vector<std::vector<size_t>>> emptySymmetry;
storm::storage::DFTIndependentSymmetries symmetries(emptySymmetry);
if(symred) {
auto colouring = ft.colourDFT();
symmetries = ft.findSymmetries(colouring);
STORM_LOG_INFO("Found " << symmetries.groups.size() << " symmetries.");
STORM_LOG_TRACE("Symmetries: " << std::endl << symmetries);
}
// Find symmetries
std::map<size_t, std::vector<std::vector<size_t>>> emptySymmetry;
storm::storage::DFTIndependentSymmetries symmetries(emptySymmetry);
if(symred) {
auto colouring = ft.colourDFT();
symmetries = ft.findSymmetries(colouring);
STORM_LOG_INFO("Found " << symmetries.groups.size() << " symmetries.");
STORM_LOG_TRACE("Symmetries: " << std::endl << symmetries);
}
// Build a single CTMC
STORM_LOG_INFO("Building Model...");
storm::builder::ExplicitDFTModelBuilderApprox<ValueType> builder(ft, symmetries, enableDC);
typename storm::builder::ExplicitDFTModelBuilderApprox<ValueType>::LabelOptions labeloptions; // TODO initialize this with the formula
builder.buildModel(labeloptions, 0, 0.0);
std::shared_ptr<storm::models::sparse::Model<ValueType>> model = builder.getModel();
//model->printModelInformationToStream(std::cout);
STORM_LOG_INFO("No. states (Explored): " << model->getNumberOfStates());
STORM_LOG_INFO("No. transitions (Explored): " << model->getNumberOfTransitions());
explorationTimer.stop();
// Build a single CTMC
STORM_LOG_INFO("Building Model...");
storm::builder::ExplicitDFTModelBuilderApprox<ValueType> builder(ft, symmetries, enableDC);
typename storm::builder::ExplicitDFTModelBuilderApprox<ValueType>::LabelOptions labeloptions; // TODO initialize this with the formula
builder.buildModel(labeloptions, 0, 0.0);
std::shared_ptr<storm::models::sparse::Model<ValueType>> model = builder.getModel();
//model->printModelInformationToStream(std::cout);
STORM_LOG_INFO("No. states (Explored): " << model->getNumberOfStates());
STORM_LOG_INFO("No. transitions (Explored): " << model->getNumberOfTransitions());
explorationTimer.stop();
STORM_LOG_THROW(model->isOfType(storm::models::ModelType::Ctmc), storm::exceptions::NotSupportedException, "Parallel composition only applicable for CTMCs");
std::shared_ptr<storm::models::sparse::Ctmc<ValueType>> ctmc = model->template as<storm::models::sparse::Ctmc<ValueType>>();
ctmc = storm::performDeterministicSparseBisimulationMinimization<storm::models::sparse::Ctmc<ValueType>>(ctmc, {formula}, storm::storage::BisimulationType::Weak)->template as<storm::models::sparse::Ctmc<ValueType>>();
if (firstTime) {
composedModel = ctmc;
firstTime = false;
} else {
composedModel = storm::builder::ParallelCompositionBuilder<ValueType>::compose(composedModel, ctmc, isAnd);
}
STORM_LOG_THROW(model->isOfType(storm::models::ModelType::Ctmc), storm::exceptions::NotSupportedException, "Parallel composition only applicable for CTMCs");
std::shared_ptr<storm::models::sparse::Ctmc<ValueType>> ctmc = model->template as<storm::models::sparse::Ctmc<ValueType>>();
// Apply bisimulation
bisimulationTimer.start();
composedModel = storm::performDeterministicSparseBisimulationMinimization<storm::models::sparse::Ctmc<ValueType>>(composedModel, {formula}, storm::storage::BisimulationType::Weak)->template as<storm::models::sparse::Ctmc<ValueType>>();
bisimulationTimer.stop();
STORM_LOG_INFO("No. states (Composed): " << composedModel->getNumberOfStates());
STORM_LOG_INFO("No. transitions (Composed): " << composedModel->getNumberOfTransitions());
if (composedModel->getNumberOfStates() <= 15) {
STORM_LOG_TRACE("Transition matrix: " << std::endl << composedModel->getTransitionMatrix());
} else {
STORM_LOG_TRACE("Transition matrix: too big to print");
}
// Apply bisimulation to new CTMC
bisimulationTimer.start();
ctmc = storm::performDeterministicSparseBisimulationMinimization<storm::models::sparse::Ctmc<ValueType>>(ctmc, properties, storm::storage::BisimulationType::Weak)->template as<storm::models::sparse::Ctmc<ValueType>>();
bisimulationTimer.stop();
if (firstTime) {
composedModel = ctmc;
firstTime = false;
} else {
composedModel = storm::builder::ParallelCompositionBuilder<ValueType>::compose(composedModel, ctmc, isAnd);
}
return composedModel;
}
}
// If we are here, no composition was possible
STORM_LOG_ASSERT(!modularisationPossible, "Modularisation should not be possible.");
explorationTimer.start();
// Find symmetries
std::map<size_t, std::vector<std::vector<size_t>>> emptySymmetry;
storm::storage::DFTIndependentSymmetries symmetries(emptySymmetry);
if(symred) {
auto colouring = dft.colourDFT();
symmetries = dft.findSymmetries(colouring);
STORM_LOG_INFO("Found " << symmetries.groups.size() << " symmetries.");
STORM_LOG_TRACE("Symmetries: " << std::endl << symmetries);
}
// Build a single CTMC
STORM_LOG_INFO("Building Model...");
// Apply bisimulation to parallel composition
bisimulationTimer.start();
composedModel = storm::performDeterministicSparseBisimulationMinimization<storm::models::sparse::Ctmc<ValueType>>(composedModel, properties, storm::storage::BisimulationType::Weak)->template as<storm::models::sparse::Ctmc<ValueType>>();
bisimulationTimer.stop();
STORM_LOG_INFO("No. states (Composed): " << composedModel->getNumberOfStates());
STORM_LOG_INFO("No. transitions (Composed): " << composedModel->getNumberOfTransitions());
if (composedModel->getNumberOfStates() <= 15) {
STORM_LOG_TRACE("Transition matrix: " << std::endl << composedModel->getTransitionMatrix());
} else {
STORM_LOG_TRACE("Transition matrix: too big to print");
}
}
return composedModel;
} else {
// No composition was possible
explorationTimer.start();
// Find symmetries
std::map<size_t, std::vector<std::vector<size_t>>> emptySymmetry;
storm::storage::DFTIndependentSymmetries symmetries(emptySymmetry);
if(symred) {
auto colouring = dft.colourDFT();
symmetries = dft.findSymmetries(colouring);
STORM_LOG_INFO("Found " << symmetries.groups.size() << " symmetries.");
STORM_LOG_TRACE("Symmetries: " << std::endl << symmetries);
}
// Build a single CTMC
STORM_LOG_INFO("Building Model...");
storm::builder::ExplicitDFTModelBuilderApprox<ValueType> builder(dft, symmetries, enableDC);
typename storm::builder::ExplicitDFTModelBuilderApprox<ValueType>::LabelOptions labeloptions; // TODO initialize this with the formula
builder.buildModel(labeloptions, 0, 0.0);
std::shared_ptr<storm::models::sparse::Model<ValueType>> model = builder.getModel();
//model->printModelInformationToStream(std::cout);
STORM_LOG_INFO("No. states (Explored): " << model->getNumberOfStates());
STORM_LOG_INFO("No. transitions (Explored): " << model->getNumberOfTransitions());
explorationTimer.stop();
STORM_LOG_THROW(model->isOfType(storm::models::ModelType::Ctmc), storm::exceptions::NotSupportedException, "Parallel composition only applicable for CTMCs");
return model->template as<storm::models::sparse::Ctmc<ValueType>>();
storm::builder::ExplicitDFTModelBuilderApprox<ValueType> builder(dft, symmetries, enableDC);
typename storm::builder::ExplicitDFTModelBuilderApprox<ValueType>::LabelOptions labeloptions; // TODO initialize this with the formula
builder.buildModel(labeloptions, 0, 0.0);
std::shared_ptr<storm::models::sparse::Model<ValueType>> model = builder.getModel();
//model->printModelInformationToStream(std::cout);
STORM_LOG_INFO("No. states (Explored): " << model->getNumberOfStates());
STORM_LOG_INFO("No. transitions (Explored): " << model->getNumberOfTransitions());
explorationTimer.stop();
STORM_LOG_THROW(model->isOfType(storm::models::ModelType::Ctmc), storm::exceptions::NotSupportedException, "Parallel composition only applicable for CTMCs");
return model->template as<storm::models::sparse::Ctmc<ValueType>>();
}
}
template<typename ValueType>
typename DFTModelChecker<ValueType>::dft_result DFTModelChecker<ValueType>::checkDFT(storm::storage::DFT<ValueType> const& dft, std::shared_ptr<const storm::logic::Formula> const& formula, bool symred, bool enableDC, double approximationError) {
typename DFTModelChecker<ValueType>::dft_results DFTModelChecker<ValueType>::checkDFT(storm::storage::DFT<ValueType> const& dft, property_vector const& properties, bool symred, bool enableDC, double approximationError) {
explorationTimer.start();
// Find symmetries
@ -288,11 +278,18 @@ namespace storm {
// Build approximate Markov Automata for lower and upper bound
approximation_result approxResult = std::make_pair(storm::utility::zero<ValueType>(), storm::utility::zero<ValueType>());
std::shared_ptr<storm::models::sparse::Model<ValueType>> model;
std::vector<ValueType> newResult;
storm::builder::ExplicitDFTModelBuilderApprox<ValueType> builder(dft, symmetries, enableDC);
typename storm::builder::ExplicitDFTModelBuilderApprox<ValueType>::LabelOptions labeloptions; // TODO initialize this with the formula
bool probabilityFormula = formula->isProbabilityOperatorFormula();
STORM_LOG_ASSERT((formula->isTimeOperatorFormula() && !probabilityFormula) || (!formula->isTimeOperatorFormula() && probabilityFormula), "Probability formula not initialized correctly");
// TODO Matthias: compute approximation for all properties simultaneously?
std::shared_ptr<const storm::logic::Formula> property = properties[0];
if (properties.size() > 1) {
STORM_LOG_WARN("Computing approximation only for first property: " << *property);
}
bool probabilityFormula = property->isProbabilityOperatorFormula();
STORM_LOG_ASSERT((property->isTimeOperatorFormula() && !probabilityFormula) || (!property->isTimeOperatorFormula() && probabilityFormula), "Probability formula not initialized correctly");
size_t iteration = 0;
do {
// Iteratively build finer models
@ -315,12 +312,11 @@ namespace storm {
STORM_LOG_INFO("No. transitions: " << model->getNumberOfTransitions());
buildingTimer.stop();
// Check lower bound
std::unique_ptr<storm::modelchecker::CheckResult> result = checkModel(model, formula);
result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates()));
ValueType newResult = result->asExplicitQuantitativeCheckResult<ValueType>().getValueMap().begin()->second;
STORM_LOG_ASSERT(iteration == 0 || !comparator.isLess(newResult, approxResult.first), "New under-approximation " << newResult << " is smaller than old result " << approxResult.first);
approxResult.first = newResult;
// Check lower bounds
newResult = checkModel(model, {property});
STORM_LOG_ASSERT(newResult.size() == 1, "Wrong size for result vector.");
STORM_LOG_ASSERT(iteration == 0 || !comparator.isLess(newResult[0], approxResult.first), "New under-approximation " << newResult[0] << " is smaller than old result " << approxResult.first);
approxResult.first = newResult[0];
// Build model for upper bound
STORM_LOG_INFO("Getting model for upper bound...");
@ -328,11 +324,10 @@ namespace storm {
model = builder.getModelApproximation(probabilityFormula ? true : false);
buildingTimer.stop();
// Check upper bound
result = checkModel(model, formula);
result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates()));
newResult = result->asExplicitQuantitativeCheckResult<ValueType>().getValueMap().begin()->second;
STORM_LOG_ASSERT(iteration == 0 || !comparator.isLess(approxResult.second, newResult), "New over-approximation " << newResult << " is greater than old result " << approxResult.second);
approxResult.second = newResult;
newResult = checkModel(model, {properties});
STORM_LOG_ASSERT(newResult.size() == 1, "Wrong size for result vector.");
STORM_LOG_ASSERT(iteration == 0 || !comparator.isLess(approxResult.second, newResult[0]), "New over-approximation " << newResult[0] << " is greater than old result " << approxResult.second);
approxResult.second = newResult[0];
++iteration;
STORM_LOG_INFO("Result after iteration " << iteration << ": (" << std::setprecision(10) << approxResult.first << ", " << approxResult.second << ")");
@ -343,7 +338,9 @@ namespace storm {
} while (!isApproximationSufficient(approxResult.first, approxResult.second, approximationError, probabilityFormula));
STORM_LOG_INFO("Finished approximation after " << iteration << " iteration" << (iteration > 1 ? "s." : "."));
return approxResult;
dft_results results;
results.push_back(approxResult);
return results;
} else {
// Build a single Markov Automaton
STORM_LOG_INFO("Building Model...");
@ -365,32 +362,50 @@ namespace storm {
explorationTimer.stop();
// Model checking
std::unique_ptr<storm::modelchecker::CheckResult> result = checkModel(model, formula);
result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates()));
return result->asExplicitQuantitativeCheckResult<ValueType>().getValueMap().begin()->second;
std::vector<ValueType> resultsValue = checkModel(model, properties);
dft_results results;
for (ValueType result : resultsValue) {
results.push_back(result);
}
return results;
}
}
template<typename ValueType>
std::unique_ptr<storm::modelchecker::CheckResult> DFTModelChecker<ValueType>::checkModel(std::shared_ptr<storm::models::sparse::Model<ValueType>>& model, std::shared_ptr<const storm::logic::Formula> const& formula) {
std::vector<ValueType> DFTModelChecker<ValueType>::checkModel(std::shared_ptr<storm::models::sparse::Model<ValueType>>& model, property_vector const& properties) {
// Bisimulation
bisimulationTimer.start();
if (model->isOfType(storm::models::ModelType::Ctmc) && storm::settings::getModule<storm::settings::modules::GeneralSettings>().isBisimulationSet()) {
bisimulationTimer.start();
STORM_LOG_INFO("Bisimulation...");
model = storm::performDeterministicSparseBisimulationMinimization<storm::models::sparse::Ctmc<ValueType>>(model->template as<storm::models::sparse::Ctmc<ValueType>>(), {formula}, storm::storage::BisimulationType::Weak)->template as<storm::models::sparse::Ctmc<ValueType>>();
model = storm::performDeterministicSparseBisimulationMinimization<storm::models::sparse::Ctmc<ValueType>>(model->template as<storm::models::sparse::Ctmc<ValueType>>(), properties, storm::storage::BisimulationType::Weak)->template as<storm::models::sparse::Ctmc<ValueType>>();
STORM_LOG_INFO("No. states (Bisimulation): " << model->getNumberOfStates());
STORM_LOG_INFO("No. transitions (Bisimulation): " << model->getNumberOfTransitions());
bisimulationTimer.stop();
}
bisimulationTimer.stop();
modelCheckingTimer.start();
// Check the model
STORM_LOG_INFO("Model checking...");
std::unique_ptr<storm::modelchecker::CheckResult> result(storm::verifySparseModel(model, formula));
STORM_LOG_INFO("Model checking done.");
STORM_LOG_ASSERT(result, "Result does not exist.");
modelCheckingTimer.start();
std::vector<ValueType> results;
// Check each property
storm::utility::Stopwatch singleModelCheckingTimer;
for (auto property : properties) {
singleModelCheckingTimer.reset();
singleModelCheckingTimer.start();
STORM_PRINT_AND_LOG("Model checking property " << *property << " ..." << std::endl);
std::unique_ptr<storm::modelchecker::CheckResult> result(storm::verifySparseModel(model, property, true));
STORM_LOG_ASSERT(result, "Result does not exist.");
result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates()));
ValueType resultValue = result->asExplicitQuantitativeCheckResult<ValueType>().getValueMap().begin()->second;
STORM_PRINT_AND_LOG("Result (initial states): " << resultValue << std::endl);
results.push_back(resultValue);
singleModelCheckingTimer.stop();
STORM_PRINT_AND_LOG("Time for model checking: " << singleModelCheckingTimer << "." << std::endl);
}
modelCheckingTimer.stop();
return result;
STORM_LOG_INFO("Model checking done.");
return results;
}
template<typename ValueType>
@ -411,21 +426,30 @@ namespace storm {
template<typename ValueType>
void DFTModelChecker<ValueType>::printTimings(std::ostream& os) {
os << "Times:" << std::endl;
os << "Exploration:\t" << explorationTimer.getTimeInMilliseconds() / 1000.0 << "s" << std::endl;
os << "Building:\t" << buildingTimer.getTimeInMilliseconds() / 1000.0 << "s" << std::endl;
os << "Bisimulation:\t" << bisimulationTimer.getTimeInMilliseconds() / 1000.0 << "s" << std::endl;
os << "Modelchecking:\t" << modelCheckingTimer.getTimeInMilliseconds() / 1000.0 << "s" << std::endl;
os << "Total:\t\t" << totalTimer.getTimeInMilliseconds() / 1000.0 << "s" << std::endl;
os << "Exploration:\t" << explorationTimer << "s" << std::endl;
os << "Building:\t" << buildingTimer << "s" << std::endl;
os << "Bisimulation:\t" << bisimulationTimer<< "s" << std::endl;
os << "Modelchecking:\t" << modelCheckingTimer << "s" << std::endl;
os << "Total:\t\t" << totalTimer << "s" << std::endl;
}
template<typename ValueType>
void DFTModelChecker<ValueType>::printResult(std::ostream& os) {
void DFTModelChecker<ValueType>::printResults(std::ostream& os) {
bool first = true;
os << "Result: [";
if (this->approximationError > 0.0) {
approximation_result result = boost::get<approximation_result>(checkResult);
os << "(" << result.first << ", " << result.second << ")";
} else {
os << boost::get<ValueType>(checkResult);
for (auto result : checkResults) {
if (!first) {
os << ", ";
}
if (this->approximationError > 0.0) {
approximation_result resultApprox = boost::get<approximation_result>(result);
os << "(" << resultApprox.first << ", " << resultApprox.second << ")";
} else {
os << boost::get<ValueType>(result);
}
if (first) {
first = false;
}
}
os << "]" << std::endl;
}

38
src/storm-dft/modelchecker/dft/DFTModelChecker.h
View File

@ -18,26 +18,28 @@ namespace storm {
class DFTModelChecker {
typedef std::pair<ValueType, ValueType> approximation_result;
typedef boost::variant<ValueType, approximation_result> dft_result;
typedef std::vector<boost::variant<ValueType, approximation_result>> dft_results;
typedef std::vector<std::shared_ptr<const storm::logic::Formula>> property_vector;
public:
/*!
* Constructor.
*/
DFTModelChecker();
DFTModelChecker() {
}
/*!
* Main method for checking DFTs.
*
* @param origDft Original DFT
* @param formula Formula to check for
* @param properties Properties to check for
* @param symred Flag indicating if symmetry reduction should be used
* @param allowModularisation Flag indication if modularisation is allowed
* @param enableDC Flag indicating if dont care propagation should be used
* @param approximationError Error allowed for approximation. Value 0 indicates no approximation
*/
void check(storm::storage::DFT<ValueType> const& origDft, std::shared_ptr<const storm::logic::Formula> const& formula, bool symred = true, bool allowModularisation = true, bool enableDC = true, double approximationError = 0.0);
void check(storm::storage::DFT<ValueType> const& origDft, property_vector const& properties, bool symred = true, bool allowModularisation = true, bool enableDC = true, double approximationError = 0.0);
/*!
* Print timings of all operations to stream.
@ -51,7 +53,7 @@ namespace storm {
*
* @param os Output stream to write to.
*/
void printResult(std::ostream& os = std::cout);
void printResults(std::ostream& os = std::cout);
private:
@ -62,8 +64,8 @@ namespace storm {
storm::utility::Stopwatch modelCheckingTimer;
storm::utility::Stopwatch totalTimer;
// Model checking result
dft_result checkResult;
// Model checking results
dft_results checkResults;
// Allowed error bound for approximation
double approximationError;
@ -72,21 +74,21 @@ namespace storm {
* Internal helper for model checking a DFT.
*
* @param dft DFT
* @param formula Formula to check for
* @param properties Properties to check for
* @param symred Flag indicating if symmetry reduction should be used
* @param allowModularisation Flag indication if modularisation is allowed
* @param enableDC Flag indicating if dont care propagation should be used
* @param approximationError Error allowed for approximation. Value 0 indicates no approximation
*
* @return Model checking result (or in case of approximation two results for lower and upper bound)
* @return Model checking results (or in case of approximation two results for lower and upper bound)
*/
dft_result checkHelper(storm::storage::DFT<ValueType> const& dft, std::shared_ptr<const storm::logic::Formula> const& formula, bool symred, bool allowModularisation, bool enableDC, double approximationError);
dft_results checkHelper(storm::storage::DFT<ValueType> const& dft, property_vector const& properties, bool symred, bool allowModularisation, bool enableDC, double approximationError);
/*!
* Internal helper for building a CTMC from a DFT via parallel composition.
*
* @param dft DFT
* @param formula Formula to check for
* @param properties Properties to check for
* @param symred Flag indicating if symmetry reduction should be used
* @param allowModularisation Flag indication if modularisation is allowed
* @param enableDC Flag indicating if dont care propagation should be used
@ -94,30 +96,30 @@ namespace storm {
*
* @return CTMC representing the DFT
*/
std::shared_ptr<storm::models::sparse::Ctmc<ValueType>> buildModelComposition(storm::storage::DFT<ValueType> const& dft, std::shared_ptr<const storm::logic::Formula> const& formula, bool symred, bool allowModularisation, bool enableDC);
std::shared_ptr<storm::models::sparse::Ctmc<ValueType>> buildModelViaComposition(storm::storage::DFT<ValueType> const& dft, property_vector const& properties, bool symred, bool allowModularisation, bool enableDC, double approximationError);
/*!
* Check model generated from DFT.
*
* @param dft The DFT
* @param formula Formula to check for
* @param properties Properties to check for
* @param symred Flag indicating if symmetry reduction should be used
* @param enableDC Flag indicating if dont care propagation should be used
* @param approximationError Error allowed for approximation. Value 0 indicates no approximation
*
* @return Model checking result
*/
dft_result checkDFT(storm::storage::DFT<ValueType> const& dft, std::shared_ptr<const storm::logic::Formula> const& formula, bool symred, bool enableDC, double approximationError = 0.0);
dft_results checkDFT(storm::storage::DFT<ValueType> const& dft, property_vector const& properties, bool symred, bool enableDC, double approximationError = 0.0);
/*!
* Check the given markov model for the given property.
* Check the given markov model for the given properties.
*
* @param model Model to check
* @param formula Formula to check for
* @param model Model to check
* @param properties Properties to check for
*
* @return Model checking result
*/
std::unique_ptr<storm::modelchecker::CheckResult> checkModel(std::shared_ptr<storm::models::sparse::Model<ValueType>>& model, std::shared_ptr<const storm::logic::Formula> const& formula);
std::vector<ValueType> checkModel(std::shared_ptr<storm::models::sparse::Model<ValueType>>& model, property_vector const& properties);
/*!
* Checks if the computed approximation is sufficient, i.e.

Write Preview
Loading…
Cancel
Save