Browse Source

further preparation of partial bisimulation model checker

tempestpy_adaptions
dehnert 7 years ago
parent
commit
b415c12c25
  1. 16
      src/storm-cli-utilities/model-handling.h
  2. 8
      src/storm/api/verification.h
  3. 35
      src/storm/modelchecker/abstraction/PartialBisimulationMdpModelChecker.cpp
  4. 15
      src/storm/modelchecker/abstraction/PartialBisimulationMdpModelChecker.h
  5. 4
      src/storm/settings/modules/AbstractionSettings.cpp
  6. 1
      src/storm/utility/resources.h

16
src/storm-cli-utilities/model-handling.h

@ -30,6 +30,7 @@
#include "storm/settings/modules/DebugSettings.h"
#include "storm/settings/modules/IOSettings.h"
#include "storm/settings/modules/CoreSettings.h"
#include "storm/settings/modules/AbstractionSettings.h"
#include "storm/settings/modules/ResourceSettings.h"
#include "storm/settings/modules/JaniExportSettings.h"
@ -209,7 +210,7 @@ namespace storm {
std::shared_ptr<storm::models::ModelBase> result;
if (input.model) {
if (engine == storm::settings::modules::CoreSettings::Engine::Dd || engine == storm::settings::modules::CoreSettings::Engine::Hybrid) {
if (engine == storm::settings::modules::CoreSettings::Engine::Dd || engine == storm::settings::modules::CoreSettings::Engine::Hybrid || engine == storm::settings::modules::CoreSettings::Engine::AbstractionRefinement) {
result = buildModelDd<DdType, ValueType>(input);
} else if (engine == storm::settings::modules::CoreSettings::Engine::Sparse) {
result = buildModelSparse<ValueType>(input, ioSettings);
@ -554,7 +555,7 @@ namespace storm {
auto task = storm::api::createTask<ValueType>(formula, filterForInitialStates);
auto symbolicModel = model->as<storm::models::symbolic::Model<DdType, ValueType>>();
std::unique_ptr<storm::modelchecker::CheckResult> result = storm::api::verifyWithDdEngine<DdType, ValueType>(model->as<storm::models::symbolic::Model<DdType, ValueType>>(), storm::api::createTask<ValueType>(formula, true));
std::unique_ptr<storm::modelchecker::CheckResult> result = storm::api::verifyWithDdEngine<DdType, ValueType>(symbolicModel, storm::api::createTask<ValueType>(formula, true));
std::unique_ptr<storm::modelchecker::CheckResult> filter;
if (filterForInitialStates) {
@ -569,6 +570,15 @@ namespace storm {
});
}
template <storm::dd::DdType DdType, typename ValueType>
void verifyWithAbstractionRefinementEngine(std::shared_ptr<storm::models::ModelBase> const& model, SymbolicInput const& input) {
verifyProperties<ValueType>(input.properties, [&model] (std::shared_ptr<storm::logic::Formula const> const& formula, std::shared_ptr<storm::logic::Formula const> const& states) {
STORM_LOG_THROW(states->isInitialFormula(), storm::exceptions::NotSupportedException, "Abstraction-refinement can only filter initial states.");
auto symbolicModel = model->as<storm::models::symbolic::Model<DdType, ValueType>>();
return storm::api::verifyWithAbstractionRefinementEngine<DdType, ValueType>(symbolicModel, storm::api::createTask<ValueType>(formula, true));
});
}
template <storm::dd::DdType DdType, typename ValueType>
typename std::enable_if<DdType != storm::dd::DdType::CUDD || std::is_same<ValueType, double>::value, void>::type verifySymbolicModel(std::shared_ptr<storm::models::ModelBase> const& model, SymbolicInput const& input, storm::settings::modules::CoreSettings const& coreSettings) {
storm::settings::modules::CoreSettings::Engine engine = coreSettings.getEngine();;
@ -629,7 +639,7 @@ namespace storm {
// For several engines, no model building step is performed, but the verification is started right away.
storm::settings::modules::CoreSettings::Engine engine = coreSettings.getEngine();
if (engine == storm::settings::modules::CoreSettings::Engine::AbstractionRefinement && abstractionSettings.getMethod() == storm::settings::modules::AbstractionSettings::Method::Games) {
if (engine == storm::settings::modules::CoreSettings::Engine::AbstractionRefinement && abstractionSettings.getAbstractionRefinementMethod() == storm::settings::modules::AbstractionSettings::Method::Games) {
verifyWithAbstractionRefinementEngine<DdType, ValueType>(input);
} else if (engine == storm::settings::modules::CoreSettings::Engine::Exploration) {
verifyWithExplorationEngine<ValueType>(input);

8
src/storm/api/verification.h

@ -48,13 +48,13 @@ namespace storm {
if (modelchecker.canHandle(task)) {
result = modelchecker.check(task);
}
} else {
} else if (model.getModelType() == storm::storage::SymbolicModelDescription::ModelType::MDP) {
storm::modelchecker::GameBasedMdpModelChecker<DdType, storm::models::symbolic::Mdp<DdType, ValueType>> modelchecker(model);
if (modelchecker.canHandle(task)) {
result = modelchecker.check(task);
}
} else {
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException);
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The model type is currently not supported.");
}
return result;
}
@ -68,12 +68,12 @@ namespace storm {
typename std::enable_if<std::is_same<ValueType, double>::value, std::unique_ptr<storm::modelchecker::CheckResult>>::type verifyWithAbstractionRefinementEngine(std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> const& model, storm::modelchecker::CheckTask<storm::logic::Formula, ValueType> const& task) {
std::unique_ptr<storm::modelchecker::CheckResult> result;
if (model->getType() == storm::models::ModelType::Dtmc) {
storm::modelchecker::PartialBisimulationMdpModelChecker<storm::models::symbolic::Dtmc<DdType, ValueType>> modelchecker(model->as<storm::models::symbolic::Dtmc<DdType, double>>());
storm::modelchecker::PartialBisimulationMdpModelChecker<storm::models::symbolic::Dtmc<DdType, ValueType>> modelchecker(*model->template as<storm::models::symbolic::Dtmc<DdType, double>>());
if (modelchecker.canHandle(task)) {
result = modelchecker.check(task);
}
} else if (model->getType() == storm::models::ModelType::Mdp) {
storm::modelchecker::PartialBisimulationMdpModelChecker<storm::models::symbolic::Mdp<DdType, ValueType>> modelchecker(model->as<storm::models::symbolic::Mdp<DdType, double>>());
storm::modelchecker::PartialBisimulationMdpModelChecker<storm::models::symbolic::Mdp<DdType, ValueType>> modelchecker(*model->template as<storm::models::symbolic::Mdp<DdType, double>>());
if (modelchecker.canHandle(task)) {
result = modelchecker.check(task);
}

35
src/storm/modelchecker/abstraction/PartialBisimulationMdpModelChecker.cpp

@ -3,17 +3,38 @@
#include "storm/models/symbolic/Dtmc.h"
#include "storm/models/symbolic/Mdp.h"
#include "storm/modelchecker/results/CheckResult.h"
#include "storm/logic/FragmentSpecification.h"
namespace storm {
namespace modelchecker {
template<storm::dd::DdType Type, typename ModelType>
PartialBisimulationMdpModelChecker<Type, ModelType>::PartialBisimulationMdpModelChecker(ModelType const& model) : model(model) {
template<typename ModelType>
PartialBisimulationMdpModelChecker<ModelType>::PartialBisimulationMdpModelChecker(ModelType const& model) : SymbolicPropositionalModelChecker<ModelType>(model) {
// Intentionally left empty.
}
template<typename ModelType>
bool PartialBisimulationMdpModelChecker<ModelType>::canHandle(CheckTask<storm::logic::Formula> const& checkTask) const {
storm::logic::Formula const& formula = checkTask.getFormula();
storm::logic::FragmentSpecification fragment = storm::logic::reachability();
return formula.isInFragment(fragment) && checkTask.isOnlyInitialStatesRelevantSet();
}
template<typename ModelType>
std::unique_ptr<CheckResult> PartialBisimulationMdpModelChecker<ModelType>::computeUntilProbabilities(CheckTask<storm::logic::UntilFormula> const& checkTask) {
return nullptr;
}
template<typename ModelType>
std::unique_ptr<CheckResult> PartialBisimulationMdpModelChecker<ModelType>::computeReachabilityProbabilities(CheckTask<storm::logic::EventuallyFormula> const& checkTask) {
return nullptr;
}
template class PartialBisimulationMdpModelChecker<storm::dd::DdType::CUDD, storm::models::symbolic::Dtmc<storm::dd::DdType::CUDD, double>>;
template class PartialBisimulationMdpModelChecker<storm::dd::DdType::CUDD, storm::models::symbolic::Mdp<storm::dd::DdType::CUDD, double>>;
template class PartialBisimulationMdpModelChecker<storm::dd::DdType::Sylvan, storm::models::symbolic::Dtmc<storm::dd::DdType::Sylvan, double>>;
template class PartialBisimulationMdpModelChecker<storm::dd::DdType::Sylvan, storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan, double>>;
template class PartialBisimulationMdpModelChecker<storm::models::symbolic::Dtmc<storm::dd::DdType::CUDD, double>>;
template class PartialBisimulationMdpModelChecker<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD, double>>;
template class PartialBisimulationMdpModelChecker<storm::models::symbolic::Dtmc<storm::dd::DdType::Sylvan, double>>;
template class PartialBisimulationMdpModelChecker<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan, double>>;
}
}

15
src/storm/modelchecker/abstraction/PartialBisimulationMdpModelChecker.h

@ -1,14 +1,14 @@
#pragma once
#include "storm/modelchecker/AbstractModelChecker.h"
#include "storm/modelchecker/propositional/SymbolicPropositionalModelChecker.h"
#include "storm/storage/dd/DdType.h"
namespace storm {
namespace modelchecker {
template<storm::dd::DdType Type, typename ModelType>
class PartialBisimulationMdpModelChecker : public AbstractModelChecker<ModelType> {
template<typename ModelType>
class PartialBisimulationMdpModelChecker : public SymbolicPropositionalModelChecker<ModelType> {
public:
typedef typename ModelType::ValueType ValueType;
@ -18,12 +18,9 @@ namespace storm {
explicit PartialBisimulationMdpModelChecker(ModelType const& model);
// /// Overridden methods from super class.
// virtual bool canHandle(CheckTask<storm::logic::Formula> const& checkTask) const override;
// virtual std::unique_ptr<CheckResult> computeUntilProbabilities(CheckTask<storm::logic::UntilFormula> const& checkTask) override;
// virtual std::unique_ptr<CheckResult> computeReachabilityProbabilities(CheckTask<storm::logic::EventuallyFormula> const& checkTask) override;
private:
ModelType const& model;
virtual bool canHandle(CheckTask<storm::logic::Formula> const& checkTask) const override;
virtual std::unique_ptr<CheckResult> computeUntilProbabilities(CheckTask<storm::logic::UntilFormula> const& checkTask) override;
virtual std::unique_ptr<CheckResult> computeReachabilityProbabilities(CheckTask<storm::logic::EventuallyFormula> const& checkTask) override;
};
}
}

4
src/storm/settings/modules/AbstractionSettings.cpp

@ -67,10 +67,10 @@ namespace storm {
}
AbstractionSettings::Method AbstractionSettings::getAbstractionRefinementMethod() const {
std::string methodAsString = this->getOption(methodOptionName).getArgumentByName("method").getValueAsString();
std::string methodAsString = this->getOption(methodOptionName).getArgumentByName("name").getValueAsString();
if (methodAsString == "games") {
return Method::Games;
} else if (methodAsString == "bisimulation" || methodAsString == "bism") {
} else if (methodAsString == "bisimulation" || methodAsString == "bisim") {
return Method::Bisimulation;
}
STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown abstraction-refinement method '" << methodAsString << "'.");

1
src/storm/utility/resources.h

@ -56,6 +56,7 @@ namespace storm {
rl.rlim_cur = megabytes * 1024 * 1024;
setrlimit(RLIMIT_AS, &rl);
#else
(void)megabytes;
STORM_LOG_WARN("Setting a memory limit is not supported for your operating system.");
#endif
}

Loading…
Cancel
Save