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

Merge branch 'future' into TimParamSysAndSMT 

Former-commit-id: 6c6d097826
tempestpy_adaptions
sjunges 9 years ago
parent
8297c51d73 e4725aa4a1
commit
fcdaab2642
6 changed files with 73 additions and 45 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. 39
      src/cli/entrypoints.h
  2. 16
      src/storage/ModelFormulasPair.h
  3. 12
      src/storage/ModelProgramPair.h
  4. 15
      src/storage/prism/Program.cpp
  5. 9
      src/storage/prism/Program.h
  6. 27
      src/utility/storm.h

39
src/cli/entrypoints.h
View File

@ -131,47 +131,32 @@ 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.");
storm::storage::ModelFormulasPair modelFormulasPair = buildSymbolicModel<ValueType, LibraryType>(program, formulas);
STORM_LOG_THROW(modelFormulasPair.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);
BRANCH_ON_MODELTYPE(modelFormulasPair.model, modelFormulasPair.model, ValueType, LibraryType, preprocessModel, formulas);
// Print some information about the model.
modelProgramPair.model->printModelInformationToStream(std::cout);
modelFormulasPair.model->printModelInformationToStream(std::cout);
// 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());
}
}
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 (modelFormulasPair.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);
for(auto const& formula : modelFormulasPair.formulas) {
generateCounterexample<ValueType>(program, modelFormulasPair.model->as<storm::models::sparse::Model<ValueType>>(), formula);
}
} else {
verifySparseModel<ValueType>(modelProgramPair.model->as<storm::models::sparse::Model<ValueType>>(), preparedFormulas);
verifySparseModel<ValueType>(modelFormulasPair.model->as<storm::models::sparse::Model<ValueType>>(), modelFormulasPair.formulas);
}
} else if (modelProgramPair.model->isSymbolicModel()) {
} else if (modelFormulasPair.model->isSymbolicModel()) {
if (storm::settings::generalSettings().getEngine() == storm::settings::modules::GeneralSettings::Engine::Hybrid) {
verifySymbolicModelWithHybridEngine(modelProgramPair.model->as<storm::models::symbolic::Model<LibraryType>>(), preparedFormulas);
verifySymbolicModelWithHybridEngine(modelFormulasPair.model->as<storm::models::symbolic::Model<LibraryType>>(), modelFormulasPair.formulas);
} else {
verifySymbolicModelWithSymbolicEngine(modelProgramPair.model->as<storm::models::symbolic::Model<LibraryType>>(), preparedFormulas);
verifySymbolicModelWithSymbolicEngine(modelFormulasPair.model->as<storm::models::symbolic::Model<LibraryType>>(), modelFormulasPair.formulas);
}
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Invalid input model type.");

16
src/storage/ModelFormulasPair.h
View File

@ -0,0 +1,16 @@
#pragma once
#include "../models/ModelBase.h"
namespace storm {
namespace logic {
class Formula;
}
namespace storage {
struct ModelFormulasPair {
std::shared_ptr<storm::models::ModelBase> model;
std::vector<std::shared_ptr<storm::logic::Formula>> formulas;
};
}
}

12
src/storage/ModelProgramPair.h
View File

@ -1,12 +0,0 @@
#include "../models/ModelBase.h"
#include "prism/Program.h"
namespace storm {
namespace storage {
struct ModelProgramPair {
std::shared_ptr<storm::models::ModelBase> model;
storm::prism::Program program;
};
}
}

15
src/storage/prism/Program.cpp
View File

@ -171,6 +171,21 @@ namespace storm {
}
return result;
}
std::string Program::getUndefinedConstantsAsString() const {
std::stringstream stream;
bool printComma = false;
for (auto const& constant : getUndefinedConstants()) {
if (printComma) {
stream << ", ";
} else {
printComma = true;
}
stream << constant.get().getName() << " (" << constant.get().getType() << ")";
}
stream << ".";
return stream.str();
}
bool Program::hasConstant(std::string const& constantName) const {
return this->constantToIndexMap.find(constantName) != this->constantToIndexMap.end();

9
src/storage/prism/Program.h
View File

@ -89,7 +89,14 @@ namespace storm {
* @return The undefined constants in the program.
*/
std::vector<std::reference_wrapper<storm::prism::Constant const>> getUndefinedConstants() const;
/*!
* Retrieves the undefined constants in the program as a comma-separated string.
*
* @return A string with the undefined constants in the program, separated by a comma
*/
std::string getUndefinedConstantsAsString() const;
/*!
* Retrieves whether the given constant exists in the program.
*

27
src/utility/storm.h
View File

@ -8,6 +8,7 @@
#include <cstdio>
#include <sstream>
#include <memory>
#include <src/storage/ModelFormulasPair.h>
#include "initialize.h"
@ -46,7 +47,7 @@
// Headers for model processing.
#include "src/storage/bisimulation/DeterministicModelBisimulationDecomposition.h"
#include "src/storage/bisimulation/NondeterministicModelBisimulationDecomposition.h"
#include "src/storage/ModelProgramPair.h"
#include "src/storage/ModelFormulasPair.h"
// Headers for model checking.
#include "src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h"
@ -85,10 +86,13 @@ namespace storm {
storm::prism::Program parseProgram(std::string const& path);
std::vector<std::shared_ptr<storm::logic::Formula>> parseFormulasForExplicit(std::string const& inputString);
std::vector<std::shared_ptr<storm::logic::Formula>> parseFormulasForProgram(std::string const& inputString, storm::prism::Program const& program);
template<typename ValueType, storm::dd::DdType LibraryType = storm::dd::DdType::CUDD>
storm::storage::ModelProgramPair buildSymbolicModel(storm::prism::Program const& program, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) {
storm::storage::ModelProgramPair result;
storm::storage::ModelFormulasPair buildSymbolicModel(storm::prism::Program const& program, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) {
storm::storage::ModelFormulasPair result;
storm::prism::Program translatedProgram;
storm::settings::modules::GeneralSettings settings = storm::settings::generalSettings();
@ -108,7 +112,7 @@ namespace storm {
storm::builder::ExplicitPrismModelBuilder<ValueType> builder;
result.model = builder.translateProgram(program, options);
result.program = builder.getTranslatedProgram();
translatedProgram = builder.getTranslatedProgram();
} else if (settings.getEngine() == storm::settings::modules::GeneralSettings::Engine::Dd || settings.getEngine() == storm::settings::modules::GeneralSettings::Engine::Hybrid) {
typename storm::builder::DdPrismModelBuilder<LibraryType>::Options options;
options = typename storm::builder::DdPrismModelBuilder<LibraryType>::Options(formulas);
@ -116,9 +120,22 @@ namespace storm {
storm::builder::DdPrismModelBuilder<LibraryType> builder;
result.model = builder.translateProgram(program, options);
result.program = builder.getTranslatedProgram();
translatedProgram = builder.getTranslatedProgram();
}
// 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 : translatedProgram.getConstants()) {
if (constant.isDefined()) {
constantSubstitution.emplace(constant.getExpressionVariable(), constant.getExpression());
}
}
for (auto const& formula : formulas) {
result.formulas.emplace_back(formula->substitute(constantSubstitution));
}
return result;
}

Write Preview
Loading…
Cancel
Save