Browse Source

Refactoring

Former-commit-id: b3896c45a4
tempestpy_adaptions
Mavo 8 years ago
parent
commit
cfc082417b
  1. 4
      resources/3rdparty/CMakeLists.txt
  2. 2
      src/CMakeLists.txt
  3. 41
      src/generator/DftNextStateGenerator.cpp
  4. 5
      src/generator/DftNextStateGenerator.h
  5. 201
      src/modelchecker/DFTAnalyser.h
  6. 214
      src/modelchecker/dft/DFTModelChecker.cpp
  7. 104
      src/modelchecker/dft/DFTModelChecker.h
  8. 20
      src/storm-dyftee.cpp

4
resources/3rdparty/CMakeLists.txt

@ -18,7 +18,7 @@ ExternalProject_Add(
DOWNLOAD_COMMAND ""
PREFIX ${CMAKE_CURRENT_BINARY_DIR}/glpk-4.57
SOURCE_DIR ${CMAKE_CURRENT_SOURCE_DIR}/glpk-4.57
CONFIGURE_COMMAND ${CMAKE_CURRENT_SOURCE_DIR}/glpk-4.57/configure --prefix=${CMAKE_CURRENT_BINARY_DIR}/glpk-4.57 --libdir=${CMAKE_CURRENT_BINARY_DIR}/glpk-4.57/lib CC=${CMAKE_C_COMPILER}
CONFIGURE_COMMAND ${CMAKE_CURRENT_SOURCE_DIR}/glpk-4.57/configure --prefix=${CMAKE_CURRENT_BINARY_DIR}/glpk-4.57 --libdir=${CMAKE_CURRENT_BINARY_DIR}/glpk-4.57/lib CC=${CMAKE_C_COMPILER} CXX=${CMAKE_CXX_COMPILER}
BUILD_COMMAND make "CFLAGS=-O2 -w"
INSTALL_COMMAND make install
BUILD_IN_SOURCE 0
@ -33,7 +33,7 @@ ExternalProject_Add(
SOURCE_DIR ${CMAKE_CURRENT_SOURCE_DIR}/cudd-3.0.0
PREFIX ${CMAKE_CURRENT_BINARY_DIR}/cudd-3.0.0
UPDATE_COMMAND autoreconf
CONFIGURE_COMMAND ${CMAKE_CURRENT_SOURCE_DIR}/cudd-3.0.0/configure --enable-shared --enable-obj --prefix=${CMAKE_CURRENT_BINARY_DIR}/cudd-3.0.0 --libdir=${CMAKE_CURRENT_BINARY_DIR}/cudd-3.0.0/lib CC=${CMAKE_C_COMPILER} CXX=${CMAKE_CXX_COMPILER}
CONFIGURE_COMMAND ${CMAKE_CURRENT_SOURCE_DIR}/cudd-3.0.0/configure --enable-shared --enable-obj --prefix=${CMAKE_CURRENT_BINARY_DIR}/cudd-3.0.0 --libdir=${CMAKE_CURRENT_BINARY_DIR}/cudd-3.0.0/lib CC=${CMAKE_C_COMPILER} CXX=${CMAKE_CXX_COMPILER}
BUILD_COMMAND make "CFLAGS=-O2 -w"
INSTALL_COMMAND make install
BUILD_IN_SOURCE 0

2
src/CMakeLists.txt

@ -22,6 +22,7 @@ file(GLOB_RECURSE STORM_MODELCHECKER_PRCTL_HELPER_FILES ${PROJECT_SOURCE_DIR}/sr
file(GLOB STORM_MODELCHECKER_CSL_FILES ${PROJECT_SOURCE_DIR}/src/modelchecker/csl/*.h ${PROJECT_SOURCE_DIR}/src/modelchecker/csl/*.cpp)
file(GLOB_RECURSE STORM_MODELCHECKER_CSL_HELPER_FILES ${PROJECT_SOURCE_DIR}/src/modelchecker/csl/helper/*.h ${PROJECT_SOURCE_DIR}/src/modelchecker/csl/helper/*.cpp)
file(GLOB_RECURSE STORM_MODELCHECKER_REACHABILITY_FILES ${PROJECT_SOURCE_DIR}/src/modelchecker/reachability/*.h ${PROJECT_SOURCE_DIR}/src/modelchecker/reachability/*.cpp)
file(GLOB_RECURSE STORM_MODELCHECKER_DFT_FILES ${PROJECT_SOURCE_DIR}/src/modelchecker/dft/*.h ${PROJECT_SOURCE_DIR}/src/modelchecker/dft/*.cpp)
file(GLOB_RECURSE STORM_MODELCHECKER_EXPLORATION_FILES ${PROJECT_SOURCE_DIR}/src/modelchecker/exploration/*.h ${PROJECT_SOURCE_DIR}/src/modelchecker/exploration/*.cpp)
file(GLOB_RECURSE STORM_MODELCHECKER_PROPOSITIONAL_FILES ${PROJECT_SOURCE_DIR}/src/modelchecker/propositional/*.h ${PROJECT_SOURCE_DIR}/src/modelchecker/propositional/*.cpp)
file(GLOB_RECURSE STORM_MODELCHECKER_RESULTS_FILES ${PROJECT_SOURCE_DIR}/src/modelchecker/results/*.h ${PROJECT_SOURCE_DIR}/src/modelchecker/results/*.cpp)
@ -75,6 +76,7 @@ source_group(modelchecker\\prctl FILES ${STORM_MODELCHECKER_PRCTL_FILES})
source_group(modelchecker\\prctl\\helper FILES ${STORM_MODELCHECKER_PRCTL_HELPER_FILES})
source_group(modelchecker\\csl FILES ${STORM_MODELCHECKER_CSL_FILES})
source_group(modelchecker\\csl\\helper FILES ${STORM_MODELCHECKER_CSL_HELPER_FILES})
source_group(modelchecker\\dft FILES ${STORM_MODELCHECKER_DFT_FILES})
source_group(modelchecker\\exploration FILES ${STORM_MODELCHECKER_EXPLORATION_FILES})
source_group(modelchecker\\reachability FILES ${STORM_MODELCHECKER_REACHABILITY_FILES})
source_group(modelchecker\\propositional FILES ${STORM_MODELCHECKER_PROPOSITIONAL_FILES})

41
src/generator/DftNextStateGenerator.cpp

@ -27,12 +27,18 @@ namespace storm {
initialState->setId(id);
return {id};
}
template<typename ValueType, typename StateType>
void DftNextStateGenerator<ValueType, StateType>::load(CompressedState const& state) {
// Load the state from bitvector
size_t id = 0; //TODO Matthias: set correct id
this->state = std::make_shared<storm::storage::DFTState<ValueType>>(state, mDft, mStateGenerationInfo, id);
}
template<typename ValueType, typename StateType>
void DftNextStateGenerator<ValueType, StateType>::load(DFTStatePointer const& state) {
// TODO Matthias load state from bitvector
// Store a pointer to the state itself, because we need to be able to access it when expanding it.
this->state = &state;
this->state = state;
}
template<typename ValueType, typename StateType>
@ -42,23 +48,22 @@ namespace storm {
template<typename ValueType, typename StateType>
StateBehavior<ValueType, StateType> DftNextStateGenerator<ValueType, StateType>::expand(StateToIdCallback const& stateToIdCallback) {
DFTStatePointer currentState = *state;
STORM_LOG_TRACE("Explore state: " << mDft.getStateString(currentState));
STORM_LOG_TRACE("Explore state: " << mDft.getStateString(state));
// Prepare the result, in case we return early.
StateBehavior<ValueType, StateType> result;
// Initialization
bool hasDependencies = currentState->nrFailableDependencies() > 0;
size_t failableCount = hasDependencies ? currentState->nrFailableDependencies() : currentState->nrFailableBEs();
bool hasDependencies = state->nrFailableDependencies() > 0;
size_t failableCount = hasDependencies ? state->nrFailableDependencies() : state->nrFailableBEs();
size_t currentFailable = 0;
Choice<ValueType, StateType> choice(0, !hasDependencies);
// Check for absorbing state
if (mDft.hasFailed(currentState) || mDft.isFailsafe(currentState) || currentState->nrFailableBEs() == 0) {
if (mDft.hasFailed(state) || mDft.isFailsafe(state) || state->nrFailableBEs() == 0) {
// Add self loop
choice.addProbability(currentState->getId(), storm::utility::one<ValueType>());
STORM_LOG_TRACE("Added self loop for " << currentState->getId());
choice.addProbability(state->getId(), storm::utility::one<ValueType>());
STORM_LOG_TRACE("Added self loop for " << state->getId());
// No further exploration required
result.addChoice(std::move(choice));
result.setExpanded();
@ -67,15 +72,15 @@ namespace storm {
// Let BE fail
while (currentFailable < failableCount) {
STORM_LOG_ASSERT(!mDft.hasFailed(currentState), "Dft has failed.");
STORM_LOG_ASSERT(!mDft.hasFailed(state), "Dft has failed.");
// Construct new state as copy from original one
DFTStatePointer newState = std::make_shared<storm::storage::DFTState<ValueType>>(*currentState);
DFTStatePointer newState = std::make_shared<storm::storage::DFTState<ValueType>>(*state);
std::pair<std::shared_ptr<storm::storage::DFTBE<ValueType> const>, bool> nextBEPair = newState->letNextBEFail(currentFailable);
std::shared_ptr<storm::storage::DFTBE<ValueType> const>& nextBE = nextBEPair.first;
STORM_LOG_ASSERT(nextBE, "NextBE is null.");
STORM_LOG_ASSERT(nextBEPair.second == hasDependencies, "Failure due to dependencies does not match.");
STORM_LOG_TRACE("With the failure of: " << nextBE->name() << " [" << nextBE->id() << "] in " << mDft.getStateString(currentState));
STORM_LOG_TRACE("With the failure of: " << nextBE->name() << " [" << nextBE->id() << "] in " << mDft.getStateString(state));
/*if (storm::settings::getModule<storm::settings::modules::DFTSettings>().computeApproximation()) {
if (!storm::utility::isZero(exitRate)) {
@ -163,13 +168,13 @@ namespace storm {
// Set transitions
if (hasDependencies) {
// Failure is due to dependency -> add non-deterministic choice
std::shared_ptr<storm::storage::DFTDependency<ValueType> const> dependency = mDft.getDependency(currentState->getDependencyId(currentFailable));
std::shared_ptr<storm::storage::DFTDependency<ValueType> const> dependency = mDft.getDependency(state->getDependencyId(currentFailable));
choice.addProbability(newStateId, dependency->probability());
STORM_LOG_TRACE("Added transition to " << newStateId << " with probability " << dependency->probability());
if (!storm::utility::isOne(dependency->probability())) {
// Add transition to state where dependency was unsuccessful
DFTStatePointer unsuccessfulState = std::make_shared<storm::storage::DFTState<ValueType>>(*currentState);
DFTStatePointer unsuccessfulState = std::make_shared<storm::storage::DFTState<ValueType>>(*state);
unsuccessfulState->letDependencyBeUnsuccessful(currentFailable);
// Add state
StateType unsuccessfulStateId = stateToIdCallback(unsuccessfulState);
@ -185,7 +190,7 @@ namespace storm {
if (mDft.hasRepresentant(nextBE->id())) {
// Active must be checked for the state we are coming from as this state is responsible for the
// rate and not the new state we are going to
isActive = currentState->isActive(mDft.getRepresentant(nextBE->id())->id());
isActive = state->isActive(mDft.getRepresentant(nextBE->id())->id());
}
ValueType rate = isActive ? nextBE->activeFailureRate() : nextBE->passiveFailureRate();
STORM_LOG_ASSERT(!storm::utility::isZero(rate), "Rate is 0.");
@ -201,7 +206,7 @@ namespace storm {
result.addChoice(std::move(choice));
}
STORM_LOG_TRACE("Finished exploring state: " << mDft.getStateString(currentState));
STORM_LOG_TRACE("Finished exploring state: " << mDft.getStateString(state));
result.setExpanded();
return result;
}
@ -228,4 +233,4 @@ namespace storm {
template class DftNextStateGenerator<double>;
template class DftNextStateGenerator<storm::RationalFunction>;
}
}
}

5
src/generator/DftNextStateGenerator.h

@ -29,6 +29,7 @@ namespace storm {
virtual std::vector<StateType> getInitialStates(StateToIdCallback const& stateToIdCallback) override;
virtual void load(DFTStatePointer const& state) override;
void load(CompressedState const& state);
virtual StateBehavior<ValueType, StateType> expand(StateToIdCallback const& stateToIdCallback) override;
virtual bool satisfies(storm::expressions::Expression const& expression) const override;
@ -50,7 +51,7 @@ namespace storm {
storm::storage::DFTStateGenerationInfo const& mStateGenerationInfo;
// Current state
DFTStatePointer const* state;
DFTStatePointer state;
// Flag indicating if dont care propagation is enabled.
bool enableDC;
@ -71,4 +72,4 @@ namespace storm {
}
}
#endif /* STORM_GENERATOR_DFTNEXTSTATEGENERATOR_H_ */
#endif /* STORM_GENERATOR_DFTNEXTSTATEGENERATOR_H_ */

201
src/modelchecker/DFTAnalyser.h

@ -1,201 +0,0 @@
#pragma once
#include "src/logic/Formula.h"
#include "src/parser/DFTGalileoParser.h"
#include "src/builder/ExplicitDFTModelBuilder.h"
#include "src/builder/ExplicitDFTModelBuilderApprox.h"
#include "src/modelchecker/results/CheckResult.h"
#include "src/utility/storm.h"
#include "src/storage/dft/DFTIsomorphism.h"
#include "src/settings/modules/DFTSettings.h"
#include "src/utility/bitoperations.h"
#include <chrono>
template<typename ValueType>
class DFTAnalyser {
std::chrono::duration<double> buildingTime = std::chrono::duration<double>::zero();
std::chrono::duration<double> explorationTime = std::chrono::duration<double>::zero();
std::chrono::duration<double> bisimulationTime = std::chrono::duration<double>::zero();
std::chrono::duration<double> modelCheckingTime = std::chrono::duration<double>::zero();
std::chrono::duration<double> totalTime = std::chrono::duration<double>::zero();
ValueType checkResult = storm::utility::zero<ValueType>();
public:
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) {
// Building DFT
std::chrono::high_resolution_clock::time_point totalStart = std::chrono::high_resolution_clock::now();
// Optimizing DFT
storm::storage::DFT<ValueType> dft = origDft.optimize();
checkResult = checkHelper(dft, formula, symred, allowModularisation, enableDC);
totalTime = std::chrono::high_resolution_clock::now() - totalStart;
}
private:
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) {
STORM_LOG_TRACE("Check helper called");
bool invResults = false;
std::vector<storm::storage::DFT<ValueType>> dfts = {dft};
std::vector<ValueType> res;
size_t nrK = 0; // K out of M
size_t nrM = 0; // K out of M
if(allowModularisation) {
if(dft.topLevelType() == storm::storage::DFTElementType::AND) {
STORM_LOG_TRACE("top modularisation called AND");
dfts = dft.topModularisation();
STORM_LOG_TRACE("Modularsation into " << dfts.size() << " submodules.");
nrK = dfts.size();
nrM = dfts.size();
}
if(dft.topLevelType() == storm::storage::DFTElementType::OR) {
STORM_LOG_TRACE("top modularisation called OR");
dfts = dft.topModularisation();
STORM_LOG_TRACE("Modularsation into " << dfts.size() << " submodules.");
nrK = 0;
nrM = dfts.size();
invResults = true;
}
if(dft.topLevelType() == storm::storage::DFTElementType::VOT) {
STORM_LOG_TRACE("top modularisation called VOT");
dfts = dft.topModularisation();
STORM_LOG_TRACE("Modularsation into " << dfts.size() << " submodules.");
nrK = std::static_pointer_cast<storm::storage::DFTVot<ValueType> const>(dft.getTopLevelGate())->threshold();
nrM = dfts.size();
if(nrK <= nrM/2) {
nrK -= 1;
invResults = true;
}
}
if(dfts.size() > 1) {
STORM_LOG_TRACE("Recursive CHECK Call");
for(auto const ft : dfts) {
res.push_back(checkHelper(ft, formula, symred, allowModularisation));
}
}
}
if(res.empty()) {
// Model based modularisation.
auto const& models = buildMarkovModels(dfts, formula, symred, enableDC);
for (auto const& model : models) {
// Model checking
STORM_LOG_INFO("Model checking...");
std::chrono::high_resolution_clock::time_point modelCheckingStart = std::chrono::high_resolution_clock::now();
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.");
result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates()));
modelCheckingTime += std::chrono::high_resolution_clock::now() - modelCheckingStart;
res.push_back(result->asExplicitQuantitativeCheckResult<ValueType>().getValueMap().begin()->second);
}
}
if(nrM <= 1) {
// No modularisation done.
STORM_LOG_ASSERT(res.size()==1, "Result size not 1.");
return res[0];
}
STORM_LOG_TRACE("Combining all results... K=" << nrK << "; M=" << nrM << "; invResults=" << (invResults?"On":"Off"));
ValueType result = storm::utility::zero<ValueType>();
int limK = invResults ? -1 : nrM+1;
int chK = invResults ? -1 : 1;
for(int cK = nrK; cK != limK; cK += chK ) {
STORM_LOG_ASSERT(cK >= 0, "ck negative.");
size_t permutation = smallestIntWithNBitsSet(static_cast<size_t>(cK));
do {
STORM_LOG_TRACE("Permutation="<<permutation);
ValueType permResult = storm::utility::one<ValueType>();
for(size_t i = 0; i < res.size(); ++i) {
if(permutation & (1 << i)) {
permResult *= res[i];
} else {
permResult *= storm::utility::one<ValueType>() - res[i];
}
}
STORM_LOG_TRACE("Result for permutation:"<<permResult);
permutation = nextBitPermutation(permutation);
result += permResult;
} while(permutation < (1 << nrM) && permutation != 0);
}
if(invResults) {
return storm::utility::one<ValueType>() - result;
}
return result;
}
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;
for(auto& dft : dfts) {
std::chrono::high_resolution_clock::time_point buildingStart = std::chrono::high_resolution_clock::now();
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);
}
std::chrono::high_resolution_clock::time_point buildingEnd = std::chrono::high_resolution_clock::now();
buildingTime += buildingEnd - buildingStart;
// Building Markov Automaton
STORM_LOG_INFO("Building Model...");
std::shared_ptr<storm::models::sparse::Model<ValueType>> model;
// TODO Matthias: use only one builder if everything works again
if (storm::settings::getModule<storm::settings::modules::DFTSettings>().computeApproximation()) {
storm::builder::ExplicitDFTModelBuilderApprox<ValueType> builder(dft, symmetries, enableDC);
typename storm::builder::ExplicitDFTModelBuilderApprox<ValueType>::LabelOptions labeloptions; // TODO initialize this with the formula
model = builder.buildModel(labeloptions);
} else {
storm::builder::ExplicitDFTModelBuilder<ValueType> builder(dft, symmetries, enableDC);
typename storm::builder::ExplicitDFTModelBuilder<ValueType>::LabelOptions labeloptions; // TODO initialize this with the formula
model = builder.buildModel(labeloptions);
}
//model->printModelInformationToStream(std::cout);
STORM_LOG_INFO("No. states (Explored): " << model->getNumberOfStates());
STORM_LOG_INFO("No. transitions (Explored): " << model->getNumberOfTransitions());
std::chrono::high_resolution_clock::time_point explorationEnd = std::chrono::high_resolution_clock::now();
explorationTime += explorationEnd -buildingEnd;
// Bisimulation
if (model->isOfType(storm::models::ModelType::Ctmc) && storm::settings::getModule<storm::settings::modules::GeneralSettings>().isBisimulationSet()) {
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->printModelInformationToStream(std::cout);
}
STORM_LOG_INFO("No. states (Bisimulation): " << model->getNumberOfStates());
STORM_LOG_INFO("No. transitions (Bisimulation): " << model->getNumberOfTransitions());
bisimulationTime += std::chrono::high_resolution_clock::now() - explorationEnd;
models.push_back(model);
}
return models;
}
public:
void printTimings(std::ostream& os = std::cout) {
os << "Times:" << std::endl;
os << "Building:\t" << buildingTime.count() << std::endl;
os << "Exploration:\t" << explorationTime.count() << std::endl;
os << "Bisimulation:\t" << bisimulationTime.count() << std::endl;
os << "Modelchecking:\t" << modelCheckingTime.count() << std::endl;
os << "Total:\t\t" << totalTime.count() << std::endl;
}
void printResult(std::ostream& os = std::cout) {
os << "Result: [";
os << checkResult << "]" << std::endl;
}
};

214
src/modelchecker/dft/DFTModelChecker.cpp

@ -0,0 +1,214 @@
#include "src/modelchecker/dft/DFTModelChecker.h"
#include "src/builder/ExplicitDFTModelBuilder.h"
#include "src/builder/ExplicitDFTModelBuilderApprox.h"
#include "src/storage/dft/DFTIsomorphism.h"
#include "src/settings/modules/DFTSettings.h"
#include "src/utility/bitoperations.h"
namespace storm {
namespace modelchecker {
template<typename ValueType>
DFTModelChecker<ValueType>::DFTModelChecker() {
// Intentionally left empty.
}
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) {
std::chrono::high_resolution_clock::time_point totalStart = std::chrono::high_resolution_clock::now();
// Optimizing DFT
storm::storage::DFT<ValueType> dft = origDft.optimize();
checkResult = checkHelper(dft, formula, symred, allowModularisation, enableDC);
totalTime = std::chrono::high_resolution_clock::now() - totalStart;
}
template<typename ValueType>
ValueType DFTModelChecker<ValueType>::checkHelper(storm::storage::DFT<ValueType> const& dft, std::shared_ptr<const storm::logic::Formula> const& formula, bool symred, bool allowModularisation, bool enableDC) {
STORM_LOG_TRACE("Check helper called");
bool invResults = false;
std::vector<storm::storage::DFT<ValueType>> dfts = {dft};
std::vector<ValueType> res;
size_t nrK = 0; // K out of M
size_t nrM = 0; // K out of M
// Try modularisation
if(allowModularisation) {
if(dft.topLevelType() == storm::storage::DFTElementType::AND) {
STORM_LOG_TRACE("top modularisation called AND");
dfts = dft.topModularisation();
STORM_LOG_TRACE("Modularsation into " << dfts.size() << " submodules.");
nrK = dfts.size();
nrM = dfts.size();
}
if(dft.topLevelType() == storm::storage::DFTElementType::OR) {
STORM_LOG_TRACE("top modularisation called OR");
dfts = dft.topModularisation();
STORM_LOG_TRACE("Modularsation into " << dfts.size() << " submodules.");
nrK = 0;
nrM = dfts.size();
invResults = true;
}
if(dft.topLevelType() == storm::storage::DFTElementType::VOT) {
STORM_LOG_TRACE("top modularisation called VOT");
dfts = dft.topModularisation();
STORM_LOG_TRACE("Modularsation into " << dfts.size() << " submodules.");
nrK = std::static_pointer_cast<storm::storage::DFTVot<ValueType> const>(dft.getTopLevelGate())->threshold();
nrM = dfts.size();
if(nrK <= nrM/2) {
nrK -= 1;
invResults = true;
}
}
if(dfts.size() > 1) {
STORM_LOG_TRACE("Recursive CHECK Call");
for(auto const ft : dfts) {
res.push_back(checkHelper(ft, formula, symred, allowModularisation, enableDC));
}
}
}
if(res.empty()) {
// Model based modularisation.
auto const& models = buildMarkovModels(dfts, formula, symred, enableDC);
for (auto const& model : models) {
// Model checking
STORM_LOG_INFO("Model checking...");
std::chrono::high_resolution_clock::time_point modelCheckingStart = std::chrono::high_resolution_clock::now();
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.");
result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates()));
modelCheckingTime += std::chrono::high_resolution_clock::now() - modelCheckingStart;
res.push_back(result->asExplicitQuantitativeCheckResult<ValueType>().getValueMap().begin()->second);
}
}
if(nrM <= 1) {
// No modularisation done.
STORM_LOG_ASSERT(res.size()==1, "Result size not 1.");
return res[0];
}
STORM_LOG_TRACE("Combining all results... K=" << nrK << "; M=" << nrM << "; invResults=" << (invResults?"On":"Off"));
ValueType result = storm::utility::zero<ValueType>();
int limK = invResults ? -1 : nrM+1;
int chK = invResults ? -1 : 1;
for(int cK = nrK; cK != limK; cK += chK ) {
STORM_LOG_ASSERT(cK >= 0, "ck negative.");
size_t permutation = smallestIntWithNBitsSet(static_cast<size_t>(cK));
do {
STORM_LOG_TRACE("Permutation="<<permutation);
ValueType permResult = storm::utility::one<ValueType>();
for(size_t i = 0; i < res.size(); ++i) {
if(permutation & (1 << i)) {
permResult *= res[i];
} else {
permResult *= storm::utility::one<ValueType>() - res[i];
}
}
STORM_LOG_TRACE("Result for permutation:"<<permResult);
permutation = nextBitPermutation(permutation);
result += permResult;
} while(permutation < (1 << nrM) && permutation != 0);
}
if(invResults) {
return storm::utility::one<ValueType>() - result;
}
return result;
}
template<typename ValueType>
std::vector<ValueType> DFTModelChecker<ValueType>::checkModel(std::vector<storm::storage::DFT<ValueType>> const& dfts, std::shared_ptr<const storm::logic::Formula> const& formula, bool symred, bool enableDC, double approximationError) {
std::vector<ValueType> results;
auto const& models = buildMarkovModels(dfts, formula, symred, enableDC);
for (auto const& model : models) {
// Model checking
STORM_LOG_INFO("Model checking...");
std::chrono::high_resolution_clock::time_point modelCheckingStart = std::chrono::high_resolution_clock::now();
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.");
result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates()));
modelCheckingTime += std::chrono::high_resolution_clock::now() - modelCheckingStart;
results.push_back(result->asExplicitQuantitativeCheckResult<ValueType>().getValueMap().begin()->second);
}
return results;
}
template<typename ValueType>
std::vector<std::shared_ptr<storm::models::sparse::Model<ValueType>>> DFTModelChecker<ValueType>::buildMarkovModels(std::vector<storm::storage::DFT<ValueType>> const& dfts, std::shared_ptr<const storm::logic::Formula> const& formula, bool symred, bool enableDC, double approximationError) {
std::vector<std::shared_ptr<storm::models::sparse::Model<ValueType>>> models;
for(auto& dft : dfts) {
std::chrono::high_resolution_clock::time_point buildingStart = std::chrono::high_resolution_clock::now();
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);
}
std::chrono::high_resolution_clock::time_point buildingEnd = std::chrono::high_resolution_clock::now();
buildingTime += buildingEnd - buildingStart;
// Building Markov Automaton
STORM_LOG_INFO("Building Model...");
std::shared_ptr<storm::models::sparse::Model<ValueType>> model;
// TODO Matthias: use only one builder if everything works again
if (storm::settings::getModule<storm::settings::modules::DFTSettings>().computeApproximation()) {
storm::builder::ExplicitDFTModelBuilderApprox<ValueType> builder(dft, symmetries, enableDC);
typename storm::builder::ExplicitDFTModelBuilderApprox<ValueType>::LabelOptions labeloptions; // TODO initialize this with the formula
model = builder.buildModel(labeloptions);
} else {
storm::builder::ExplicitDFTModelBuilder<ValueType> builder(dft, symmetries, enableDC);
typename storm::builder::ExplicitDFTModelBuilder<ValueType>::LabelOptions labeloptions; // TODO initialize this with the formula
model = builder.buildModel(labeloptions);
}
//model->printModelInformationToStream(std::cout);
STORM_LOG_INFO("No. states (Explored): " << model->getNumberOfStates());
STORM_LOG_INFO("No. transitions (Explored): " << model->getNumberOfTransitions());
std::chrono::high_resolution_clock::time_point explorationEnd = std::chrono::high_resolution_clock::now();
explorationTime += explorationEnd -buildingEnd;
// Bisimulation
if (model->isOfType(storm::models::ModelType::Ctmc) && storm::settings::getModule<storm::settings::modules::GeneralSettings>().isBisimulationSet()) {
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->printModelInformationToStream(std::cout);
}
STORM_LOG_INFO("No. states (Bisimulation): " << model->getNumberOfStates());
STORM_LOG_INFO("No. transitions (Bisimulation): " << model->getNumberOfTransitions());
bisimulationTime += std::chrono::high_resolution_clock::now() - explorationEnd;
models.push_back(model);
}
return models;
}
template<typename ValueType>
void DFTModelChecker<ValueType>::printTimings(std::ostream& os) {
os << "Times:" << std::endl;
os << "Building:\t" << buildingTime.count() << std::endl;
os << "Exploration:\t" << explorationTime.count() << std::endl;
os << "Bisimulation:\t" << bisimulationTime.count() << std::endl;
os << "Modelchecking:\t" << modelCheckingTime.count() << std::endl;
os << "Total:\t\t" << totalTime.count() << std::endl;
}
template<typename ValueType>
void DFTModelChecker<ValueType>::printResult(std::ostream& os) {
os << "Result: [";
os << checkResult << "]" << std::endl;
}
template class DFTModelChecker<double>;
#ifdef STORM_HAVE_CARL
template class DFTModelChecker<storm::RationalFunction>;
#endif
}
}

104
src/modelchecker/dft/DFTModelChecker.h

@ -0,0 +1,104 @@
#ifndef STORM_MODELCHECKER_DFT_DFTMODELCHECKER_H_
#include "src/logic/Formula.h"
#include "src/modelchecker/results/CheckResult.h"
#include "src/storage/dft/DFT.h"
#include "src/utility/storm.h"
#include <chrono>
namespace storm {
namespace modelchecker {
/**
* Analyser for DFTs.
*/
template<typename ValueType>
class DFTModelChecker {
public:
/**
* Constructor.
*/
DFTModelChecker();
/**
* Main method for checking DFTs.
*
* @param origDft Original DFT
* @param formula Formula 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
*/
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);
/**
* Print timings of all operations to stream.
*
* @param os Output stream to write to.
*/
void printTimings(std::ostream& os = std::cout);
/**
* Print result to stream.
*
* @param os Output stream to write to.
*/
void printResult(std::ostream& os = std::cout);
private:
// Timing values
std::chrono::duration<double> buildingTime = std::chrono::duration<double>::zero();
std::chrono::duration<double> explorationTime = std::chrono::duration<double>::zero();
std::chrono::duration<double> bisimulationTime = std::chrono::duration<double>::zero();
std::chrono::duration<double> modelCheckingTime = std::chrono::duration<double>::zero();
std::chrono::duration<double> totalTime = std::chrono::duration<double>::zero();
// Model checking result
ValueType checkResult = storm::utility::zero<ValueType>();
/**
* Internal helper for model checking a DFT.
*
* @param dft DFT
* @param formula Formula 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
*
* @return Model checking result
*/
ValueType checkHelper(storm::storage::DFT<ValueType> const& dft, std::shared_ptr<const storm::logic::Formula> const& formula, bool symred, bool allowModularisation, bool enableDC);
/**
* Check the Dfts via model checking.
*
* @param dfts Vector of Dfts
* @param formula Formula 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 Vector of results for each model
*/
std::vector<ValueType> checkModel(std::vector<storm::storage::DFT<ValueType>> const& dfts, std::shared_ptr<const storm::logic::Formula> const& formula, bool symred, bool enableDC, double approximationError = 0.0);
/**
* Build markov models from DFTs.
*
* @param dfts Vector of Dfts
* @param formula Formula 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 Vector of markov models corresponding to DFTs.
*/
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, double approximationError = 0.0);
};
}
}
#endif /* STORM_MODELCHECKER_DFT_DFTMODELCHECKER_H_ */

20
src/storm-dyftee.cpp

@ -1,12 +1,12 @@
#include "logic/Formula.h"
#include "utility/initialize.h"
#include "utility/storm.h"
#include "modelchecker/DFTAnalyser.h"
#include "src/logic/Formula.h"
#include "src/utility/initialize.h"
#include "src/utility/storm.h"
#include "src/parser/DFTGalileoParser.h"
#include "src/modelchecker/dft/DFTModelChecker.h"
#include "src/cli/cli.h"
#include "src/exceptions/BaseException.h"
#include "src/utility/macros.h"
#include "src/builder/DftSmtBuilder.h"
#include <boost/lexical_cast.hpp>
#include "src/settings/modules/GeneralSettings.h"
#include "src/settings/modules/DFTSettings.h"
@ -24,6 +24,8 @@
//#include "src/settings/modules/ParametricSettings.h"
#include "src/settings/modules/SparseDtmcEliminationModelCheckerSettings.h"
#include <boost/lexical_cast.hpp>
/*!
* Load DFT from filename, build corresponding Model and check against given property.
*
@ -39,10 +41,10 @@ void analyzeDFT(std::string filename, std::string property, bool symred = false,
std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::parseFormulasForExplicit(property);
STORM_LOG_ASSERT(formulas.size() == 1, "Wrong number of formulas.");
DFTAnalyser<ValueType> analyser;
analyser.check(dft, formulas[0], symred, allowModularisation, enableDC);
analyser.printTimings();
analyser.printResult();
storm::modelchecker::DFTModelChecker<ValueType> modelChecker;
modelChecker.check(dft, formulas[0], symred, allowModularisation, enableDC);
modelChecker.printTimings();
modelChecker.printResult();
}
template<typename ValueType>

Loading…
Cancel
Save