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

Merge branch 'future' into menu_games 

Former-commit-id: b6b21923f2
main
dehnert 10 years ago
parent
7c3333497a ebbd03c15b
commit
c73cfd7826
6 changed files with 63 additions and 41 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. 2
      CMakeLists.txt
  2. 85
      src/cli/entrypoints.h
  3. 5
      src/parser/SpiritParserDefinitions.h
  4. 7
      src/settings/modules/GeneralSettings.cpp
  5. 2
      src/settings/modules/GeneralSettings.h
  6. 3
      src/utility/storm.h

2
CMakeLists.txt
View File

@ -85,7 +85,7 @@ if(CMAKE_COMPILER_IS_GNUCC)
set(CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -funroll-loops")
set(CMAKE_C_FLAGS_RELEASE "${CMAKE_C_FLAGS_RELEASE} -funroll-loops")
add_definitions(-DBOOST_RESULT_OF_USE_DECLTYPE)
set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -std=c++14 -Wall -pedantic -Wno-deprecated-declarations -Wno-unused-local-typedefs")
set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -std=c++14 -Wall -pedantic -Wno-deprecated-declarations -Wno-unused-local-typedefs -Wno-unknown-pragmas")
set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -Wall -pedantic -Wno-deprecated-declarations")
# Turn on popcnt instruction if desired (yes by default)

85
src/cli/entrypoints.h
View File

@ -3,6 +3,8 @@
#include "src/utility/storm.h"
#include "src/exceptions/NotImplementedException.h"
namespace storm {
namespace cli {
@ -47,6 +49,11 @@ namespace storm {
}
#endif
template<storm::dd::DdType DdType>
void verifySymbolicModelWithAbstractionRefinementEngine(storm::prism::Program const& program, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) {
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Abstraction Refinement is not yet implemented.");
}
template<storm::dd::DdType DdType>
void verifySymbolicModelWithHybridEngine(std::shared_ptr<storm::models::symbolic::Model<DdType>> model, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) {
for (auto const& formula : formulas) {
@ -108,50 +115,56 @@ namespace storm {
template<typename ValueType, storm::dd::DdType LibraryType>
void buildAndCheckSymbolicModel(storm::prism::Program const& program, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) {
storm::storage::ModelProgramPair modelProgramPair = buildSymbolicModel<ValueType, LibraryType>(program, formulas);
STORM_LOG_THROW(modelProgramPair.model != nullptr, storm::exceptions::InvalidStateException, "Model could not be constructed for an unknown reason.");
// Preprocess the model if needed.
BRANCH_ON_MODELTYPE(modelProgramPair.model, modelProgramPair.model, ValueType, LibraryType, preprocessModel, formulas);
// Print some information about the model.
modelProgramPair.model->printModelInformationToStream(std::cout);
storm::settings::modules::GeneralSettings const& settings = storm::settings::generalSettings();
// Verify the model, if a formula was given.
if (!formulas.empty()) {
// There may be constants of the model appearing in the formulas, so we replace all their occurrences
// by their definitions in the translated program.
if (settings.getEngine() == storm::settings::modules::GeneralSettings::Engine::AbstractionRefinement) {
verifySymbolicModelWithAbstractionRefinementEngine(program, formulas);
} else {
storm::storage::ModelProgramPair modelProgramPair = buildSymbolicModel<ValueType, LibraryType>(program, formulas);
STORM_LOG_THROW(modelProgramPair.model != nullptr, storm::exceptions::InvalidStateException, "Model could not be constructed for an unknown reason.");
// Start by building a mapping from constants of the (translated) model to their defining expressions.
std::map<storm::expressions::Variable, storm::expressions::Expression> constantSubstitution;
for (auto const& constant : modelProgramPair.program.getConstants()) {
if (constant.isDefined()) {
constantSubstitution.emplace(constant.getExpressionVariable(), constant.getExpression());
}
}
// Preprocess the model if needed.
BRANCH_ON_MODELTYPE(modelProgramPair.model, modelProgramPair.model, ValueType, LibraryType, preprocessModel, formulas);
std::vector<std::shared_ptr<storm::logic::Formula>> preparedFormulas;
for (auto const& formula : formulas) {
preparedFormulas.emplace_back(formula->substitute(constantSubstitution));
}
// Print some information about the model.
modelProgramPair.model->printModelInformationToStream(std::cout);
if (modelProgramPair.model->isSparseModel()) {
if(storm::settings::generalSettings().isCounterexampleSet()) {
// If we were requested to generate a counterexample, we now do so for each formula.
for(auto const& formula : preparedFormulas) {
generateCounterexample<ValueType>(program, modelProgramPair.model->as<storm::models::sparse::Model<ValueType>>(), formula);
// Verify the model, if a formula was given.
if (!formulas.empty()) {
// There may be constants of the model appearing in the formulas, so we replace all their occurrences
// by their definitions in the translated program.
// Start by building a mapping from constants of the (translated) model to their defining expressions.
std::map<storm::expressions::Variable, storm::expressions::Expression> constantSubstitution;
for (auto const& constant : modelProgramPair.program.getConstants()) {
if (constant.isDefined()) {
constantSubstitution.emplace(constant.getExpressionVariable(), constant.getExpression());
}
} else {
verifySparseModel<ValueType>(modelProgramPair.model->as<storm::models::sparse::Model<ValueType>>(), preparedFormulas);
}
} else if (modelProgramPair.model->isSymbolicModel()) {
if (storm::settings::generalSettings().getEngine() == storm::settings::modules::GeneralSettings::Engine::Hybrid) {
verifySymbolicModelWithHybridEngine(modelProgramPair.model->as<storm::models::symbolic::Model<LibraryType>>(), preparedFormulas);
std::vector<std::shared_ptr<storm::logic::Formula>> preparedFormulas;
for (auto const& formula : formulas) {
preparedFormulas.emplace_back(formula->substitute(constantSubstitution));
}
if (modelProgramPair.model->isSparseModel()) {
if(settings.isCounterexampleSet()) {
// If we were requested to generate a counterexample, we now do so for each formula.
for(auto const& formula : preparedFormulas) {
generateCounterexample<ValueType>(program, modelProgramPair.model->as<storm::models::sparse::Model<ValueType>>(), formula);
}
} else {
verifySparseModel<ValueType>(modelProgramPair.model->as<storm::models::sparse::Model<ValueType>>(), preparedFormulas);
}
} else if (modelProgramPair.model->isSymbolicModel()) {
if (settings.getEngine() == storm::settings::modules::GeneralSettings::Engine::Hybrid) {
verifySymbolicModelWithHybridEngine(modelProgramPair.model->as<storm::models::symbolic::Model<LibraryType>>(), preparedFormulas);
} else {
verifySymbolicModelWithSymbolicEngine(modelProgramPair.model->as<storm::models::symbolic::Model<LibraryType>>(), preparedFormulas);
}
} else {
verifySymbolicModelWithSymbolicEngine(modelProgramPair.model->as<storm::models::symbolic::Model<LibraryType>>(), preparedFormulas);
STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Invalid input model type.");
}
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Invalid input model type.");
}
}
}

5
src/parser/SpiritParserDefinitions.h
View File

@ -1,6 +1,9 @@
#ifndef STORM_PARSER_SPIRITPARSERDEFINITIONS_H_
#define STORM_PARSER_SPIRITPARSERDEFINITIONS_H_
#pragma clang diagnostic push
#pragma clang diagnostic ignored "-Wno-#pragma-messages"
// Include boost spirit.
#define BOOST_SPIRIT_USE_PHOENIX_V3
#include <boost/typeof/typeof.hpp>
@ -9,6 +12,8 @@
#include <boost/spirit/include/support_line_pos_iterator.hpp>
#include <boost/spirit/home/classic/iterator/position_iterator.hpp>
#pragma clang diagnostic pop
namespace qi = boost::spirit::qi;
namespace phoenix = boost::phoenix;

7
src/settings/modules/GeneralSettings.cpp
View File

@ -98,9 +98,9 @@ namespace storm {
this->addOption(storm::settings::OptionBuilder(moduleName, noCutsOptionName, false, "Do not perform cuts when buildings the state space.").build());
this->addOption(storm::settings::OptionBuilder(moduleName, dontFixDeadlockOptionName, false, "If the model contains deadlock states, this flag disables automatically fixing them.").setShortName(dontFixDeadlockOptionShortName).build());
std::vector<std::string> engines = {"sparse", "hybrid", "dd"};
std::vector<std::string> engines = {"sparse", "hybrid", "dd", "abs"};
this->addOption(storm::settings::OptionBuilder(moduleName, engineOptionName, false, "Sets which engine is used for model building and model checking.").setShortName(engineOptionShortName)
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the engine to use. Available are {sparse, hybrid, dd}.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(engines)).setDefaultValueString("sparse").build()).build());
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the engine to use. Available are {sparse, hybrid, dd, ar}.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(engines)).setDefaultValueString("sparse").build()).build());
std::vector<std::string> linearEquationSolver = {"gmm++", "native"};
this->addOption(storm::settings::OptionBuilder(moduleName, eqSolverOptionName, false, "Sets which solver is preferred for solving systems of linear equations.")
@ -352,10 +352,11 @@ namespace storm {
engine = GeneralSettings::Engine::Hybrid;
} else if (engineStr == "dd") {
engine = GeneralSettings::Engine::Dd;
} else if (engineStr == "abs") {
engine = GeneralSettings::Engine::AbstractionRefinement;
} else {
STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown engine '" << engineStr << "'.");
}
}
bool GeneralSettings::check() const {

2
src/settings/modules/GeneralSettings.h
View File

@ -27,7 +27,7 @@ namespace storm {
// An enumeration of all engines.
enum class Engine {
Sparse, Hybrid, Dd
Sparse, Hybrid, Dd, AbstractionRefinement
};
/*!

3
src/utility/storm.h
View File

@ -232,6 +232,9 @@ namespace storm {
STORM_LOG_THROW(ddModel != nullptr, storm::exceptions::InvalidArgumentException, "Dd engine requires a dd input model");
return verifySymbolicModelWithDdEngine(ddModel, formula);
}
case storm::settings::modules::GeneralSettings::Engine::AbstractionRefinement: {
STORM_LOG_ASSERT(false, "This position should not be reached, as at this point no model has been built.");
}
}
}

Write Preview
Loading…
Cancel
Save