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

adapted cli to use symbolic model description rather than PRISM program 

Former-commit-id: d06884a848 [formerly 9a128e04f1]
Former-commit-id: 25a820d000
main
dehnert 9 years ago
parent
d5ba9e00e8
commit
e274cd33eb
12 changed files with 134 additions and 142 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. 47
      src/builder/DdJaniModelBuilder.cpp
  2. 22
      src/builder/DdJaniModelBuilder.h
  3. 33
      src/builder/DdPrismModelBuilder.cpp
  4. 11
      src/builder/DdPrismModelBuilder.h
  5. 13
      src/cli/cli.cpp
  6. 56
      src/cli/entrypoints.h
  7. 2
      src/storage/SymbolicModelDescription.h
  8. 6
      src/storage/jani/Model.cpp
  9. 7
      src/storage/jani/Model.h
  10. 1
      src/storage/prism/Program.cpp
  11. 15
      src/utility/storm.cpp
  12. 63
      src/utility/storm.h

47
src/builder/DdJaniModelBuilder.cpp
View File

@ -102,22 +102,6 @@ namespace storm {
}
}
template <storm::dd::DdType Type, typename ValueType>
DdJaniModelBuilder<Type, ValueType>::DdJaniModelBuilder(storm::jani::Model const& model, Options const& options) : model(model), options(options) {
if (this->model->hasUndefinedConstants()) {
std::vector<std::reference_wrapper<storm::jani::Constant const>> undefinedConstants = this->model->getUndefinedConstants();
std::vector<std::string> strings;
for (auto const& constant : undefinedConstants) {
std::stringstream stream;
stream << constant.get().getName() << " (" << constant.get().getType() << ")";
strings.push_back(stream.str());
}
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Program still contains these undefined constants: " << boost::join(strings, ", ") << ".");
}
this->model = this->model->substituteConstants();
}
template <storm::dd::DdType Type, typename ValueType>
struct CompositionVariables {
CompositionVariables() : manager(std::make_shared<storm::dd::DdManager<Type>>()),
@ -1732,31 +1716,42 @@ namespace storm {
}
template <storm::dd::DdType Type, typename ValueType>
std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>> DdJaniModelBuilder<Type, ValueType>::build() {
std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>> DdJaniModelBuilder<Type, ValueType>::build(storm::jani::Model const& model, Options const& options) {
if (model.hasUndefinedConstants()) {
std::vector<std::reference_wrapper<storm::jani::Constant const>> undefinedConstants = model.getUndefinedConstants();
std::vector<std::string> strings;
for (auto const& constant : undefinedConstants) {
std::stringstream stream;
stream << constant.get().getName() << " (" << constant.get().getType() << ")";
strings.push_back(stream.str());
}
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Model still contains these undefined constants: " << boost::join(strings, ", ") << ".");
}
// Create all necessary variables.
CompositionVariableCreator<Type, ValueType> variableCreator(*this->model);
CompositionVariableCreator<Type, ValueType> variableCreator(model);
CompositionVariables<Type, ValueType> variables = variableCreator.create();
// Create a builder to compose and build the model.
// SeparateEdgesSystemComposer<Type, ValueType> composer(*this->model, variables);
CombinedEdgesSystemComposer<Type, ValueType> composer(*this->model, variables);
// SeparateEdgesSystemComposer<Type, ValueType> composer(model, variables);
CombinedEdgesSystemComposer<Type, ValueType> composer(model, variables);
ComposerResult<Type, ValueType> system = composer.compose();
// Postprocess the variables in place.
postprocessVariables(this->model->getModelType(), system, variables);
postprocessVariables(model.getModelType(), system, variables);
// Postprocess the system in place and get the states that were terminal (i.e. whose transitions were cut off).
storm::dd::Bdd<Type> terminalStates = postprocessSystem(*this->model, system, variables, options);
storm::dd::Bdd<Type> terminalStates = postprocessSystem(model, system, variables, options);
// Start creating the model components.
ModelComponents<Type, ValueType> modelComponents;
// Build initial states.
modelComponents.initialStates = computeInitialStates(*this->model, variables);
modelComponents.initialStates = computeInitialStates(model, variables);
// Perform reachability analysis to obtain reachable states.
storm::dd::Bdd<Type> transitionMatrixBdd = system.transitions.notZero();
if (this->model->getModelType() == storm::jani::ModelType::MDP) {
if (model.getModelType() == storm::jani::ModelType::MDP) {
transitionMatrixBdd = transitionMatrixBdd.existsAbstract(variables.allNondeterminismVariables);
}
modelComponents.reachableStates = storm::utility::dd::computeReachableStates(modelComponents.initialStates, transitionMatrixBdd, variables.rowMetaVariables, variables.columnMetaVariables);
@ -1770,13 +1765,13 @@ namespace storm {
modelComponents.transitionMatrix = system.transitions * reachableStatesAdd;
// Fix deadlocks if existing.
modelComponents.deadlockStates = fixDeadlocks(this->model->getModelType(), modelComponents.transitionMatrix, transitionMatrixBdd, modelComponents.reachableStates, variables);
modelComponents.deadlockStates = fixDeadlocks(model.getModelType(), modelComponents.transitionMatrix, transitionMatrixBdd, modelComponents.reachableStates, variables);
// Cut the deadlock states by removing all states that we 'converted' to deadlock states by making them terminal.
modelComponents.deadlockStates = modelComponents.deadlockStates && !terminalStates;
// Finally, create the model.
return createModel(this->model->getModelType(), variables, modelComponents);
return createModel(model.getModelType(), variables, modelComponents);
}
template class DdJaniModelBuilder<storm::dd::DdType::CUDD, double>;

22
src/builder/DdJaniModelBuilder.h
View File

@ -77,11 +77,6 @@ namespace storm {
boost::optional<storm::expressions::Expression> negatedTerminalStates;
};
/*!
* Creates a builder for the given model that uses the given options.
*/
DdJaniModelBuilder(storm::jani::Model const& model, Options const& options = Options());
/*!
* Translates the given program into a symbolic model (i.e. one that stores the transition relation as a
* decision diagram).
@ -89,22 +84,7 @@ namespace storm {
* @param model The model to translate.
* @return A pointer to the resulting model.
*/
std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>> build();
/*!
* Retrieves the model that was actually translated (i.e. including constant substitutions etc.). Note
* that this function may only be called after a succesful translation.
*
* @return The translated model.
*/
storm::jani::Model const& getTranslatedModel() const;
private:
/// The model to translate.
boost::optional<storm::jani::Model> model;
/// The options to use for building the model.
Options options;
std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>> build(storm::jani::Model const& model, Options const& options = Options());
};
}

33
src/builder/DdPrismModelBuilder.cpp
View File

@ -1222,17 +1222,10 @@ namespace storm {
return storm::models::symbolic::StandardRewardModel<Type, ValueType>(stateRewards, stateActionRewards, transitionRewards);
}
template <storm::dd::DdType Type, typename ValueType>
storm::prism::Program const& DdPrismModelBuilder<Type, ValueType>::getTranslatedProgram() const {
return preparedProgram.get();
}
template <storm::dd::DdType Type, typename ValueType>
std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>> DdPrismModelBuilder<Type, ValueType>::build(storm::prism::Program const& program, Options const& options) {
preparedProgram = program;
if (preparedProgram->hasUndefinedConstants()) {
std::vector<std::reference_wrapper<storm::prism::Constant const>> undefinedConstants = preparedProgram->getUndefinedConstants();
if (program.hasUndefinedConstants()) {
std::vector<std::reference_wrapper<storm::prism::Constant const>> undefinedConstants = program.getUndefinedConstants();
std::stringstream stream;
bool printComma = false;
for (auto const& constant : undefinedConstants) {
@ -1247,13 +1240,11 @@ namespace storm {
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Program still contains these undefined constants: " + stream.str());
}
preparedProgram = preparedProgram->substituteConstants();
STORM_LOG_DEBUG("Building representation of program:" << std::endl << *preparedProgram << std::endl);
STORM_LOG_DEBUG("Building representation of program:" << std::endl << program << std::endl);
// Start by initializing the structure used for storing all information needed during the model generation.
// In particular, this creates the meta variables used to encode the model.
GenerationInformation generationInfo(*preparedProgram);
GenerationInformation generationInfo(program);
SystemResult system = createSystemDecisionDiagram(generationInfo);
storm::dd::Add<Type, ValueType> transitionMatrix = system.allTransitionsDd;
@ -1264,7 +1255,7 @@ namespace storm {
// If we were asked to treat some states as terminal states, we cut away their transitions now.
storm::dd::Bdd<Type> terminalStatesBdd = generationInfo.manager->getBddZero();
if (options.terminalStates || options.negatedTerminalStates) {
std::map<storm::expressions::Variable, storm::expressions::Expression> constantsSubstitution = preparedProgram->getConstantsSubstitution();
std::map<storm::expressions::Variable, storm::expressions::Expression> constantsSubstitution = program.getConstantsSubstitution();
if (options.terminalStates) {
storm::expressions::Expression terminalExpression;
@ -1273,7 +1264,7 @@ namespace storm {
} else {
std::string const& labelName = boost::get<std::string>(options.terminalStates.get());
if (program.hasLabel(labelName)) {
terminalExpression = preparedProgram->getLabelExpression(labelName);
terminalExpression = program.getLabelExpression(labelName);
} else {
STORM_LOG_THROW(labelName == "init" || labelName == "deadlock", storm::exceptions::InvalidArgumentException, "Terminal states refer to illegal label '" << labelName << "'.");
}
@ -1294,7 +1285,7 @@ namespace storm {
} else {
std::string const& labelName = boost::get<std::string>(options.negatedTerminalStates.get());
if (program.hasLabel(labelName)) {
negatedTerminalExpression = preparedProgram->getLabelExpression(labelName);
negatedTerminalExpression = program.getLabelExpression(labelName);
} else {
STORM_LOG_THROW(labelName == "init" || labelName == "deadlock", storm::exceptions::InvalidArgumentException, "Terminal states refer to illegal label '" << labelName << "'.");
}
@ -1377,18 +1368,18 @@ namespace storm {
// First, we make sure that all selected reward models actually exist.
for (auto const& rewardModelName : options.rewardModelsToBuild) {
STORM_LOG_THROW(rewardModelName.empty() || preparedProgram->hasRewardModel(rewardModelName), storm::exceptions::InvalidArgumentException, "Model does not possess a reward model with the name '" << rewardModelName << "'.");
STORM_LOG_THROW(rewardModelName.empty() || program.hasRewardModel(rewardModelName), storm::exceptions::InvalidArgumentException, "Model does not possess a reward model with the name '" << rewardModelName << "'.");
}
for (auto const& rewardModel : preparedProgram->getRewardModels()) {
for (auto const& rewardModel : program.getRewardModels()) {
if (options.buildAllRewardModels || options.rewardModelsToBuild.find(rewardModel.getName()) != options.rewardModelsToBuild.end()) {
selectedRewardModels.push_back(rewardModel);
}
}
// If no reward model was selected until now and a referenced reward model appears to be unique, we build
// the only existing reward model (given that no explicit name was given for the referenced reward model).
if (selectedRewardModels.empty() && preparedProgram->getNumberOfRewardModels() == 1 && options.rewardModelsToBuild.size() == 1 && *options.rewardModelsToBuild.begin() == "") {
selectedRewardModels.push_back(preparedProgram->getRewardModel(0));
if (selectedRewardModels.empty() && program.getNumberOfRewardModels() == 1 && options.rewardModelsToBuild.size() == 1 && *options.rewardModelsToBuild.begin() == "") {
selectedRewardModels.push_back(program.getRewardModel(0));
}
std::unordered_map<std::string, storm::models::symbolic::StandardRewardModel<Type, ValueType>> rewardModels;
@ -1398,7 +1389,7 @@ namespace storm {
// Build the labels that can be accessed as a shortcut.
std::map<std::string, storm::expressions::Expression> labelToExpressionMapping;
for (auto const& label : preparedProgram->getLabels()) {
for (auto const& label : program.getLabels()) {
labelToExpressionMapping.emplace(label.getName(), label.getStatePredicateExpression());
}

11
src/builder/DdPrismModelBuilder.h
View File

@ -98,14 +98,6 @@ namespace storm {
*/
std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>> build(storm::prism::Program const& program, Options const& options = Options());
/*!
* Retrieves the program that was actually translated (i.e. including constant substitutions etc.). Note
* that this function may only be called after a succesful translation.
*
* @return The translated program.
*/
storm::prism::Program const& getTranslatedProgram() const;
private:
// This structure can store the decision diagrams representing a particular action.
struct UpdateDecisionDiagram {
@ -243,9 +235,6 @@ namespace storm {
static SystemResult createSystemDecisionDiagram(GenerationInformation& generationInfo);
static storm::dd::Bdd<Type> createInitialStatesDecisionDiagram(GenerationInformation& generationInfo);
// This member holds the program that was most recently translated (if any).
boost::optional<storm::prism::Program> preparedProgram;
};
} // namespace adapters

13
src/cli/cli.cpp
View File

@ -231,27 +231,20 @@ namespace storm {
}
}
// There may be constants of the model appearing in the formulas, so we replace all their occurrences
// by their definitions in the translated program.
std::vector<std::shared_ptr<storm::logic::Formula const>> preprocessedFormulas;
for (auto const& formula : formulas) {
preprocessedFormulas.emplace_back(formula->substitute(constantsSubstitution));
}
if (storm::settings::getModule<storm::settings::modules::GeneralSettings>().isParametricSet()) {
#ifdef STORM_HAVE_CARL
buildAndCheckSymbolicModel<storm::RationalFunction>(preprocessedProgram, preprocessedFormulas, true);
buildAndCheckSymbolicModel<storm::RationalFunction>(model, formulas, true);
#else
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "No parameters are supported in this build.");
#endif
} else if (storm::settings::getModule<storm::settings::modules::GeneralSettings>().isExactSet()) {
#ifdef STORM_HAVE_CARL
buildAndCheckSymbolicModel<storm::RationalNumber>(preprocessedProgram, preprocessedFormulas, true);
buildAndCheckSymbolicModel<storm::RationalNumber>(model, formulas, true);
#else
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "No exact numbers are supported in this build.");
#endif
} else {
buildAndCheckSymbolicModel<double>(preprocessedProgram, preprocessedFormulas, true);
buildAndCheckSymbolicModel<double>(model, formulas, true);
}
} else if (storm::settings::getModule<storm::settings::modules::IOSettings>().isExplicitSet()) {
STORM_LOG_THROW(storm::settings::getModule<storm::settings::modules::CoreSettings>().getEngine() == storm::settings::modules::CoreSettings::Engine::Sparse, storm::exceptions::InvalidSettingsException, "Only the sparse engine supports explicit model input.");

56
src/cli/entrypoints.h
View File

@ -3,7 +3,10 @@
#include "src/utility/storm.h"
#include "src/storage/SymbolicModelDescription.h"
#include "src/exceptions/NotImplementedException.h"
#include "src/exceptions/InvalidSettingsException.h"
namespace storm {
namespace cli {
@ -49,12 +52,14 @@ namespace storm {
#endif
template<storm::dd::DdType DdType>
void verifySymbolicModelWithAbstractionRefinementEngine(storm::prism::Program const& program, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool onlyInitialStatesRelevant = false) {
void verifySymbolicModelWithAbstractionRefinementEngine(storm::storage::SymbolicModelDescription const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool onlyInitialStatesRelevant = false) {
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Abstraction Refinement is not yet implemented.");
}
template<typename ValueType>
void verifySymbolicModelWithExplorationEngine(storm::prism::Program const& program, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool onlyInitialStatesRelevant = false) {
void verifySymbolicModelWithExplorationEngine(storm::storage::SymbolicModelDescription const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool onlyInitialStatesRelevant = false) {
STORM_LOG_THROW(model.isPrismProgram(), storm::exceptions::InvalidSettingsException, "Exploration engine is currently only applicable to PRISM models.");
storm::prism::Program const& program = model.asPrismProgram();
STORM_LOG_THROW(program.getModelType() == storm::prism::Program::ModelType::DTMC || program.getModelType() == storm::prism::Program::ModelType::MDP, storm::exceptions::InvalidSettingsException, "Currently exploration-based verification is only available for DTMCs and MDPs.");
for (auto const& formula : formulas) {
@ -98,7 +103,7 @@ namespace storm {
#ifdef STORM_HAVE_CARL
template<>
void verifySymbolicModelWithExplorationEngine<storm::RationalFunction>(storm::prism::Program const& program, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool onlyInitialStatesRelevant) {
void verifySymbolicModelWithExplorationEngine<storm::RationalFunction>(storm::storage::SymbolicModelDescription const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool onlyInitialStatesRelevant) {
STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Exploration-based verification does currently not support parametric models.");
}
#endif
@ -177,81 +182,80 @@ namespace storm {
}
template<storm::dd::DdType LibraryType>
void buildAndCheckSymbolicModelWithSymbolicEngine(bool hybrid, storm::prism::Program const& program, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool onlyInitialStatesRelevant = false) {
void buildAndCheckSymbolicModelWithSymbolicEngine(bool hybrid, storm::storage::SymbolicModelDescription const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool onlyInitialStatesRelevant = false) {
// Start by building the model.
auto model = buildSymbolicModel<double, LibraryType>(program, formulas);
auto markovModel = buildSymbolicModel<double, LibraryType>(model, formulas);
// Print some information about the model.
model->printModelInformationToStream(std::cout);
markovModel->printModelInformationToStream(std::cout);
// Then select the correct engine.
if (hybrid) {
verifySymbolicModelWithHybridEngine(model, formulas, onlyInitialStatesRelevant);
verifySymbolicModelWithHybridEngine(markovModel, formulas, onlyInitialStatesRelevant);
} else {
verifySymbolicModelWithDdEngine(model, formulas, onlyInitialStatesRelevant);
verifySymbolicModelWithDdEngine(markovModel, formulas, onlyInitialStatesRelevant);
}
}
template<typename ValueType>
void buildAndCheckSymbolicModelWithSparseEngine(storm::prism::Program const& program, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool onlyInitialStatesRelevant = false) {
void buildAndCheckSymbolicModelWithSparseEngine(storm::storage::SymbolicModelDescription const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool onlyInitialStatesRelevant = false) {
// Start by building the model.
std::shared_ptr<storm::models::ModelBase> model = buildSparseModel<ValueType>(program, formulas);
std::shared_ptr<storm::models::ModelBase> markovModel = buildSparseModel<ValueType>(model, formulas);
// Print some information about the model.
model->printModelInformationToStream(std::cout);
markovModel->printModelInformationToStream(std::cout);
// Preprocess the model.
BRANCH_ON_SPARSE_MODELTYPE(model, model, ValueType, preprocessModel, formulas);
BRANCH_ON_SPARSE_MODELTYPE(markovModel, markovModel, ValueType, preprocessModel, formulas);
std::shared_ptr<storm::models::sparse::Model<ValueType>> sparseModel = model->template as<storm::models::sparse::Model<ValueType>>();
std::shared_ptr<storm::models::sparse::Model<ValueType>> sparseModel = markovModel->template as<storm::models::sparse::Model<ValueType>>();
// Finally, treat the formulas.
if (storm::settings::getModule<storm::settings::modules::CoreSettings>().isCounterexampleSet()) {
generateCounterexamples<ValueType>(program, sparseModel, formulas);
generateCounterexamples<ValueType>(model, sparseModel, formulas);
} else {
verifySparseModel<ValueType>(sparseModel, formulas, onlyInitialStatesRelevant);
}
}
template<typename ValueType>
void buildAndCheckSymbolicModel(storm::prism::Program const& program, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool onlyInitialStatesRelevant = false) {
void buildAndCheckSymbolicModel(storm::storage::SymbolicModelDescription const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool onlyInitialStatesRelevant = false) {
if (storm::settings::getModule<storm::settings::modules::CoreSettings>().getEngine() == storm::settings::modules::CoreSettings::Engine::AbstractionRefinement) {
auto ddlib = storm::settings::getModule<storm::settings::modules::CoreSettings>().getDdLibraryType();
if (ddlib == storm::dd::DdType::CUDD) {
verifySymbolicModelWithAbstractionRefinementEngine<storm::dd::DdType::CUDD>(program, formulas, onlyInitialStatesRelevant);
verifySymbolicModelWithAbstractionRefinementEngine<storm::dd::DdType::CUDD>(model, formulas, onlyInitialStatesRelevant);
} else {
verifySymbolicModelWithAbstractionRefinementEngine<storm::dd::DdType::Sylvan>(program, formulas, onlyInitialStatesRelevant);
verifySymbolicModelWithAbstractionRefinementEngine<storm::dd::DdType::Sylvan>(model, formulas, onlyInitialStatesRelevant);
}
} else if (storm::settings::getModule<storm::settings::modules::CoreSettings>().getEngine() == storm::settings::modules::CoreSettings::Engine::Exploration) {
verifySymbolicModelWithExplorationEngine<ValueType>(program, formulas, onlyInitialStatesRelevant);
verifySymbolicModelWithExplorationEngine<ValueType>(model, formulas, onlyInitialStatesRelevant);
} else {
auto engine = storm::settings::getModule<storm::settings::modules::CoreSettings>().getEngine();
if (engine == storm::settings::modules::CoreSettings::Engine::Dd || engine == storm::settings::modules::CoreSettings::Engine::Hybrid) {
auto ddlib = storm::settings::getModule<storm::settings::modules::CoreSettings>().getDdLibraryType();
if (ddlib == storm::dd::DdType::CUDD) {
buildAndCheckSymbolicModelWithSymbolicEngine<storm::dd::DdType::CUDD>(engine == storm::settings::modules::CoreSettings::Engine::Hybrid, program, formulas, onlyInitialStatesRelevant);
buildAndCheckSymbolicModelWithSymbolicEngine<storm::dd::DdType::CUDD>(engine == storm::settings::modules::CoreSettings::Engine::Hybrid, model, formulas, onlyInitialStatesRelevant);
} else {
buildAndCheckSymbolicModelWithSymbolicEngine<storm::dd::DdType::Sylvan>(engine == storm::settings::modules::CoreSettings::Engine::Hybrid, program, formulas, onlyInitialStatesRelevant);
buildAndCheckSymbolicModelWithSymbolicEngine<storm::dd::DdType::Sylvan>(engine == storm::settings::modules::CoreSettings::Engine::Hybrid, model, formulas, onlyInitialStatesRelevant);
}
} else {
STORM_LOG_THROW(engine == storm::settings::modules::CoreSettings::Engine::Sparse, storm::exceptions::InvalidSettingsException, "Illegal engine.");
buildAndCheckSymbolicModelWithSparseEngine<ValueType>(program, formulas, onlyInitialStatesRelevant);
buildAndCheckSymbolicModelWithSparseEngine<ValueType>(model, formulas, onlyInitialStatesRelevant);
}
}
}
#ifdef STORM_HAVE_CARL
template<>
void buildAndCheckSymbolicModel<storm::RationalNumber>(storm::prism::Program const& program, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool onlyInitialStatesRelevant) {
void buildAndCheckSymbolicModel<storm::RationalNumber>(storm::storage::SymbolicModelDescription const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool onlyInitialStatesRelevant) {
STORM_LOG_THROW(storm::settings::getModule<storm::settings::modules::CoreSettings>().getEngine() == storm::settings::modules::CoreSettings::Engine::Sparse, storm::exceptions::InvalidSettingsException, "Cannot use this data type with an engine different than the sparse one.");
buildAndCheckSymbolicModelWithSparseEngine<storm::RationalNumber>(program, formulas, onlyInitialStatesRelevant);
buildAndCheckSymbolicModelWithSparseEngine<storm::RationalNumber>(model, formulas, onlyInitialStatesRelevant);
}
template<>
void buildAndCheckSymbolicModel<storm::RationalFunction>(storm::prism::Program const& program, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool onlyInitialStatesRelevant) {
void buildAndCheckSymbolicModel<storm::RationalFunction>(storm::storage::SymbolicModelDescription const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool onlyInitialStatesRelevant) {
STORM_LOG_THROW(storm::settings::getModule<storm::settings::modules::CoreSettings>().getEngine() == storm::settings::modules::CoreSettings::Engine::Sparse, storm::exceptions::InvalidSettingsException, "Cannot use this data type with an engine different than the sparse one.");
buildAndCheckSymbolicModelWithSparseEngine<storm::RationalFunction>(program, formulas, onlyInitialStatesRelevant);
buildAndCheckSymbolicModelWithSparseEngine<storm::RationalFunction>(model, formulas, onlyInitialStatesRelevant);
}
#endif

2
src/storage/SymbolicModelDescription.h
View File

@ -10,7 +10,7 @@ namespace storm {
class SymbolicModelDescription {
public:
SymbolicModelDescription();
SymbolicModelDescription() = default;
SymbolicModelDescription(storm::jani::Model const& model);
SymbolicModelDescription(storm::prism::Program const& program);

6
src/storage/jani/Model.cpp
View File

@ -34,6 +34,10 @@ namespace storm {
silentActionIndex = addAction(storm::jani::Action(SILENT_ACTION_NAME));
}
storm::expressions::ExpressionManager& Model::getManager() const {
return *expressionManager;
}
uint64_t Model::getJaniVersion() const {
return version;
}
@ -104,7 +108,7 @@ namespace storm {
std::vector<Constant>& Model::getConstants() {
return constants;
}
Variable const& Model::addVariable(Variable const& variable) {
if (variable.isBooleanVariable()) {
return addVariable(variable.asBooleanVariable());

7
src/storage/jani/Model.h
View File

@ -30,6 +30,11 @@ namespace storm {
* Creates an empty model with the given type.
*/
Model(std::string const& name, ModelType const& modelType, uint64_t version = 1, boost::optional<std::shared_ptr<storm::expressions::ExpressionManager>> const& expressionManager = boost::none);
/*!
* Retrieves the expression manager responsible for the expressions in the model.
*/
storm::expressions::ExpressionManager& getManager() const;
/*!
* Retrieves the JANI-version of the model.
@ -106,7 +111,7 @@ namespace storm {
* Retrieves the constant with the given name (if any).
*/
Constant const& getConstant(std::string const& name) const;
/*!
* Adds the given variable to this model.
*/

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

@ -332,7 +332,6 @@ namespace storm {
return constantsSubstitution;
}
std::size_t Program::getNumberOfConstants() const {
return this->getConstants().size();
}

15
src/utility/storm.cpp
View File

@ -43,12 +43,23 @@ namespace storm {
return parseFormulas(formulaParser, inputString);
}
std::vector<std::shared_ptr<storm::logic::Formula const>> substituteConstantsInFormulas(std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) {
std::vector<std::shared_ptr<storm::logic::Formula const>> preprocessedFormulas;
for (auto const& formula : formulas) {
preprocessedFormulas.emplace_back(formula->substitute(substitution));
}
return preprocessedFormulas;
}
std::vector<std::shared_ptr<storm::logic::Formula const>> parseFormulasForJaniModel(std::string const& inputString, storm::jani::Model const& model) {
storm::parser::FormulaParser formulaParser(model.getManager().getSharedPointer());
return parseFormulas(formulaParser, inputString);
auto formulas = parseFormulas(formulaParser, inputString);
return substituteConstantsInFormulas(formulas, model.getConstantsSubstitution());
}
std::vector<std::shared_ptr<storm::logic::Formula const>> parseFormulasForPrismProgram(std::string const& inputString, storm::prism::Program const& program) {
storm::parser::FormulaParser formulaParser(program);
return parseFormulas(formulaParser, inputString);
auto formulas = parseFormulas(formulaParser, inputString);
return substituteConstantsInFormulas(formulas, program.getConstantsSubstitution());
}
}

63
src/utility/storm.h
View File

@ -48,11 +48,13 @@
// Headers of builders.
#include "src/builder/ExplicitModelBuilder.h"
#include "src/builder/DdPrismModelBuilder.h"
#include "src/builder/DdJaniModelBuilder.h"
// Headers for model processing.
#include "src/storage/bisimulation/DeterministicModelBisimulationDecomposition.h"
#include "src/storage/bisimulation/NondeterministicModelBisimulationDecomposition.h"
#include "src/storage/ModelFormulasPair.h"
#include "src/storage/SymbolicModelDescription.h"
// Headers for model checking.
#include "src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h"
@ -79,9 +81,9 @@
#include "src/counterexamples/MILPMinimalLabelSetGenerator.h"
#include "src/counterexamples/SMTMinimalCommandSetGenerator.h"
// Headers related to PRISM model building.
// Headers related to model building.
#include "src/generator/PrismNextStateGenerator.h"
#include "src/utility/prism.h"
#include "src/generator/JaniNextStateGenerator.h"
// Headers related to exception handling.
#include "src/exceptions/InvalidStateException.h"
@ -101,10 +103,11 @@ namespace storm {
std::pair<storm::jani::Model, std::vector<storm::jani::Property>> parseJaniModel(std::string const& path);
storm::prism::Program parseProgram(std::string const& path);
std::vector<std::shared_ptr<storm::logic::Formula const>> parseFormulasForExplicit(std::string const& inputString);
std::vector<std::shared_ptr<storm::logic::Formula const>> parseFormulasForProgram(std::string const& inputString, storm::prism::Program const& program);
std::vector<std::shared_ptr<storm::logic::Formula const>> parseFormulasForPrismProgram(std::string const& inputString, storm::prism::Program const& program);
std::vector<std::shared_ptr<storm::logic::Formula const>> parseFormulasForJaniModel(std::string const& inputString, storm::jani::Model const& model);
template<typename ValueType>
std::shared_ptr<storm::models::sparse::Model<ValueType>> buildSparseModel(storm::prism::Program const& program, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool onlyInitialStatesRelevant = false) {
std::shared_ptr<storm::models::sparse::Model<ValueType>> buildSparseModel(storm::storage::SymbolicModelDescription const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool onlyInitialStatesRelevant = false) {
storm::generator::NextStateGeneratorOptions options(formulas);
// Generate command labels if we are going to build a counterexample later.
@ -112,18 +115,34 @@ namespace storm {
options.setBuildChoiceLabels(true);
}
std::shared_ptr<storm::generator::NextStateGenerator<ValueType, uint32_t>> generator = std::make_shared<storm::generator::PrismNextStateGenerator<ValueType, uint32_t>>(program, options);
std::shared_ptr<storm::generator::NextStateGenerator<ValueType, uint32_t>> generator;
if (model.isPrismProgram()) {
generator = std::make_shared<storm::generator::PrismNextStateGenerator<ValueType, uint32_t>>(model.asPrismProgram(), options);
} else if (model.isJaniModel()) {
generator = std::make_shared<storm::generator::JaniNextStateGenerator<ValueType, uint32_t>>(model.asJaniModel(), options);
} else {
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Cannot build sparse model from this symbolic model description.");
}
storm::builder::ExplicitModelBuilder<ValueType> builder(generator);
return builder.build();
}
template<typename ValueType, storm::dd::DdType LibraryType = storm::dd::DdType::CUDD>
std::shared_ptr<storm::models::symbolic::Model<LibraryType, ValueType>> buildSymbolicModel(storm::prism::Program const& program, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) {
typename storm::builder::DdPrismModelBuilder<LibraryType, ValueType>::Options options;
options = typename storm::builder::DdPrismModelBuilder<LibraryType, ValueType>::Options(formulas);
storm::builder::DdPrismModelBuilder<LibraryType, ValueType> builder;
return builder.build(program, options);
std::shared_ptr<storm::models::symbolic::Model<LibraryType, ValueType>> buildSymbolicModel(storm::storage::SymbolicModelDescription const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) {
if (model.isPrismProgram()) {
typename storm::builder::DdPrismModelBuilder<LibraryType, ValueType>::Options options;
options = typename storm::builder::DdPrismModelBuilder<LibraryType, ValueType>::Options(formulas);
storm::builder::DdPrismModelBuilder<LibraryType, ValueType> builder;
return builder.build(model.asPrismProgram(), options);
} else {
STORM_LOG_THROW(model.isJaniModel(), storm::exceptions::InvalidArgumentException, "Cannot build symbolic model for the given symbolic model description.");
typename storm::builder::DdJaniModelBuilder<LibraryType, ValueType>::Options options;
options = typename storm::builder::DdJaniModelBuilder<LibraryType, ValueType>::Options(formulas);
storm::builder::DdJaniModelBuilder<LibraryType, ValueType> builder;
return builder.build(model.asJaniModel(), options);
}
}
template<typename ModelType>
@ -205,11 +224,13 @@ namespace storm {
}
template<typename ValueType>
void generateCounterexample(storm::prism::Program const& program, std::shared_ptr<storm::models::sparse::Model<ValueType>> model, std::shared_ptr<storm::logic::Formula const> const& formula) {
void generateCounterexample(storm::storage::SymbolicModelDescription const& model, std::shared_ptr<storm::models::sparse::Model<ValueType>> markovModel, std::shared_ptr<storm::logic::Formula const> const& formula) {
if (storm::settings::getModule<storm::settings::modules::CounterexampleGeneratorSettings>().isMinimalCommandSetGenerationSet()) {
STORM_LOG_THROW(model->getType() == storm::models::ModelType::Mdp, storm::exceptions::InvalidTypeException, "Minimal command set generation is only available for MDPs.");
std::shared_ptr<storm::models::sparse::Mdp<ValueType>> mdp = model->template as<storm::models::sparse::Mdp<ValueType>>();
STORM_LOG_THROW(model.isPrismProgram(), storm::exceptions::InvalidTypeException, "Minimal command set generation is only available for PRISM models.");
STORM_LOG_THROW(markovModel->getType() == storm::models::ModelType::Mdp, storm::exceptions::InvalidTypeException, "Minimal command set generation is only available for MDPs.");
storm::prism::Program const& program = model.asPrismProgram();
std::shared_ptr<storm::models::sparse::Mdp<ValueType>> mdp = markovModel->template as<storm::models::sparse::Mdp<ValueType>>();
// Determine whether we are required to use the MILP-version or the SAT-version.
bool useMILP = storm::settings::getModule<storm::settings::modules::CounterexampleGeneratorSettings>().isUseMilpBasedMinimalCommandSetGenerationSet();
@ -227,20 +248,20 @@ namespace storm {
#ifdef STORM_HAVE_CARL
template<>
inline void generateCounterexample(storm::prism::Program const& program, std::shared_ptr<storm::models::sparse::Model<storm::RationalNumber>> model, std::shared_ptr<storm::logic::Formula const> const& formula) {
STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unable to generate counterexample for parametric model.");
inline void generateCounterexample(storm::storage::SymbolicModelDescription const& model, std::shared_ptr<storm::models::sparse::Model<storm::RationalNumber>> markovModel, std::shared_ptr<storm::logic::Formula const> const& formula) {
STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unable to generate counterexample for exact arithmetic model.");
}
template<>
inline void generateCounterexample(storm::prism::Program const& program, std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> model, std::shared_ptr<storm::logic::Formula const> const& formula) {
inline void generateCounterexample(storm::storage::SymbolicModelDescription const& model, std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> markovModel, std::shared_ptr<storm::logic::Formula const> const& formula) {
STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unable to generate counterexample for parametric model.");
}
#endif
template<typename ValueType>
void generateCounterexamples(storm::prism::Program const& program, std::shared_ptr<storm::models::sparse::Model<ValueType>> model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) {
void generateCounterexamples(storm::storage::SymbolicModelDescription const& model, std::shared_ptr<storm::models::sparse::Model<ValueType>> markovModel, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) {
for (auto const& formula : formulas) {
generateCounterexample(program, model, formula);
generateCounterexample(model, markovModel, formula);
}
}
@ -408,7 +429,7 @@ namespace storm {
// Program and formula
storm::prism::Program program = parseProgram(programFilePath);
program.checkValidity();
std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = parseFormulasForProgram(formulaString, program);;
std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = parseFormulasForPrismProgram(formulaString, program);
if(formulas.size()!=1) {
STORM_LOG_ERROR("The given formulaString does not specify exactly one formula");
return false;

Write Preview
Loading…
Cancel
Save