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

Merge branch 'master' of https://sselab.de/lab9/private/git/storm 

Former-commit-id: f48c32691a
tempestpy_adaptions
dehnert 10 years ago
parent
04f789619c 44e609ce86
commit
5365d50811
9 changed files with 244 additions and 101 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. 12
      src/models/sparse/Mdp.cpp
  2. 8
      src/models/sparse/Mdp.h
  3. 5
      src/models/sparse/Model.cpp
  4. 12
      src/models/sparse/Model.h
  5. 8
      src/storage/SparseMatrix.cpp
  6. 8
      src/storage/SparseMatrix.h
  7. 155
      src/storage/prism/Program.cpp
  8. 24
      src/storage/prism/Program.h
  9. 113
      src/utility/cli.h

12
src/models/sparse/Mdp.cpp
View File

@ -72,9 +72,21 @@ namespace storm {
this->hasStateRewards() ? boost::optional<std::vector<ValueType>>(this->getStateRewardVector()) : boost::optional<std::vector<ValueType>>(),
this->hasTransitionRewards() ? boost::optional<storm::storage::SparseMatrix<ValueType>>(this->getTransitionRewardMatrix()) : boost::optional<storm::storage::SparseMatrix<ValueType>>(),
boost::optional<std::vector<LabelSet>>(newChoiceLabeling));
return restrictedMdp;
}
template <typename ValueType>
Mdp<ValueType> Mdp<ValueType>::restrictActions(storm::storage::BitVector const& enabledActions) const {
storm::storage::SparseMatrix<ValueType> restrictedTransitions = this->getTransitionMatrix().restrictRows(enabledActions);
if(this->hasTransitionRewards()) {
return Mdp<ValueType>(restrictedTransitions, this->getStateLabeling(), this->getOptionalStateRewardVector(), boost::optional<storm::storage::SparseMatrix<ValueType>>(this->getTransitionRewardMatrix().restrictRows(enabledActions)), this->getOptionalChoiceLabeling());
} else {
return Mdp<ValueType>( restrictedTransitions, this->getStateLabeling(), this->getOptionalStateRewardVector(), boost::optional<storm::storage::SparseMatrix<ValueType>>(), this->getOptionalChoiceLabeling());
}
}
template <typename ValueType>
bool Mdp<ValueType>::checkValidityOfProbabilityMatrix() const {
storm::utility::ConstantsComparator<ValueType> comparator;

8
src/models/sparse/Mdp.h
View File

@ -63,6 +63,14 @@ namespace storm {
*/
Mdp<ValueType> restrictChoiceLabels(LabelSet const& enabledChoiceLabels) const;
/*!
* Constructs an MDP by copying the current MDP and restricting the choices of each state to the ones given by the bitvector.
*
* @param enabledActions A BitVector of lenght numberOfChoices(), which is one iff the action should be kept.
* @return A subMDP.
*/
Mdp<ValueType> restrictActions(storm::storage::BitVector const& enabledActions) const;
private:
/*!
* Checks the probability matrix for validity.

5
src/models/sparse/Model.cpp
View File

@ -113,6 +113,11 @@ namespace storm {
return choiceLabeling.get();
}
template <typename ValueType>
boost::optional<std::vector<LabelSet>> const& Model<ValueType>::getOptionalChoiceLabeling() const {
return choiceLabeling;
}
template <typename ValueType>
storm::models::sparse::StateLabeling const& Model<ValueType>::getStateLabeling() const {
return stateLabeling;

12
src/models/sparse/Model.h
View File

@ -173,13 +173,20 @@ namespace storm {
boost::optional<std::vector<ValueType>> const& getOptionalStateRewardVector() const;
/*!
* Retrieves the labels for the choices of the model. Note that calling this method is only valud if the
* model has a choice labling.
* Retrieves the labels for the choices of the model. Note that calling this method is only valid if the
* model has a choice labeling.
*
* @return The labels for the choices of the model.
*/
std::vector<LabelSet> const& getChoiceLabeling() const;
/*!
* Retrieves an optional value that contains the choice labeling if there is one.
*
* @return The labels for the choices, if they're saved.
*/
boost::optional<std::vector<LabelSet>> const& getOptionalChoiceLabeling() const;
/*!
* Returns the state labeling associated with this model.
*
@ -194,6 +201,7 @@ namespace storm {
*/
storm::models::sparse::StateLabeling& getStateLabeling();
/*!
* Retrieves whether this model has state rewards.
*

8
src/storage/SparseMatrix.cpp
View File

@ -614,6 +614,14 @@ namespace storm {
return matrixBuilder.build();
}
template<typename ValueType>
SparseMatrix<ValueType> SparseMatrix<ValueType>::restrictRows(storm::storage::BitVector const& rowsToKeep) const {
// For now, we use the expensive call to submatrix.
SparseMatrix<ValueType> res(getSubmatrix(false, rowsToKeep, storm::storage::BitVector(getColumnCount(), true), false));
assert(getRowGroupCount() == res.getRowGroupCount());
return res;
}
template<typename ValueType>
SparseMatrix<ValueType> SparseMatrix<ValueType>::selectRowsFromRowGroups(std::vector<index_type> const& rowGroupToRowIndexMapping, bool insertDiagonalEntries) const {
// First, we need to count how many non-zero entries the resulting matrix will have and reserve space for

8
src/storage/SparseMatrix.h
View File

@ -610,6 +610,14 @@ namespace storm {
*/
SparseMatrix getSubmatrix(bool useGroups, storm::storage::BitVector const& rowConstraint, storm::storage::BitVector const& columnConstraint, bool insertDiagonalEntries = false) const;
/*!
* Restrict rows in grouped rows matrix. Ensures that the number of groups stays the same.
*
* @param rowsToKeep A bit vector indicating which rows to keep.
*
*/
SparseMatrix restrictRows(storm::storage::BitVector const& rowsToKeep) const;
/*!
* Selects exactly one row from each row group of this matrix and returns the resulting matrix.
*

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

@ -12,7 +12,16 @@
namespace storm {
namespace prism {
Program::Program(std::shared_ptr<storm::expressions::ExpressionManager> manager, ModelType modelType, std::vector<Constant> const& constants, std::vector<BooleanVariable> const& globalBooleanVariables, std::vector<IntegerVariable> const& globalIntegerVariables, std::vector<Formula> const& formulas, std::vector<Module> const& modules, std::map<std::string, uint_fast64_t> const& actionToIndexMap, std::vector<RewardModel> const& rewardModels, bool fixInitialConstruct, storm::prism::InitialConstruct const& initialConstruct, std::vector<Label> const& labels, std::string const& filename, uint_fast64_t lineNumber, bool checkValidity) : LocatedInformation(filename, lineNumber), manager(manager), modelType(modelType), constants(constants), constantToIndexMap(), globalBooleanVariables(globalBooleanVariables), globalBooleanVariableToIndexMap(), globalIntegerVariables(globalIntegerVariables), globalIntegerVariableToIndexMap(), formulas(formulas), formulaToIndexMap(), modules(modules), moduleToIndexMap(), rewardModels(rewardModels), rewardModelToIndexMap(), initialConstruct(initialConstruct), labels(labels), actionToIndexMap(actionToIndexMap), indexToActionMap(), actions(), actionIndices(), actionIndicesToModuleIndexMap(), variableToModuleIndexMap() {
Program::Program(std::shared_ptr<storm::expressions::ExpressionManager> manager, ModelType modelType, std::vector<Constant> const& constants, std::vector<BooleanVariable> const& globalBooleanVariables, std::vector<IntegerVariable> const& globalIntegerVariables, std::vector<Formula> const& formulas, std::vector<Module> const& modules, std::map<std::string, uint_fast64_t> const& actionToIndexMap, std::vector<RewardModel> const& rewardModels, bool fixInitialConstruct, storm::prism::InitialConstruct const& initialConstruct, std::vector<Label> const& labels, std::string const& filename, uint_fast64_t lineNumber, bool finalModel)
: LocatedInformation(filename, lineNumber), manager(manager),
modelType(modelType), constants(constants), constantToIndexMap(),
globalBooleanVariables(globalBooleanVariables), globalBooleanVariableToIndexMap(),
globalIntegerVariables(globalIntegerVariables), globalIntegerVariableToIndexMap(),
formulas(formulas), formulaToIndexMap(), modules(modules), moduleToIndexMap(),
rewardModels(rewardModels), rewardModelToIndexMap(), initialConstruct(initialConstruct),
labels(labels), actionToIndexMap(actionToIndexMap), indexToActionMap(), actions(),
actionIndices(), actionIndicesToModuleIndexMap(), variableToModuleIndexMap()
{
// Start by creating the necessary mappings from the given ones.
this->createMappings();
@ -38,7 +47,8 @@ namespace storm {
this->initialConstruct = storm::prism::InitialConstruct(newInitialExpression, this->getInitialConstruct().getFilename(), this->getInitialConstruct().getLineNumber());
}
if (checkValidity) {
if (finalModel) {
// If the model is supposed to be a CTMC, but contains probabilistic commands, we transform them to Markovian
// commands and issue a warning.
if (modelType == storm::prism::Program::ModelType::CTMC && storm::settings::generalSettings().isPrismCompatibilityEnabled()) {
@ -53,9 +63,8 @@ namespace storm {
}
STORM_LOG_WARN_COND(!hasProbabilisticCommands, "The input model is a CTMC, but uses probabilistic commands like they are used in PRISM. Consider rewriting the commands to use Markovian commands instead.");
}
// Then check the validity.
this->checkValidity();
this->checkValidity(Program::ValidityCheckLevel::VALIDINPUT);
}
}
@ -511,7 +520,8 @@ namespace storm {
return Program(this->manager, this->getModelType(), newConstants, newBooleanVariables, newIntegerVariables, newFormulas, newModules, this->getActionNameToIndexMapping(), newRewardModels, false, newInitialConstruct, newLabels);
}
void Program::checkValidity() const {
void Program::checkValidity(Program::ValidityCheckLevel lvl) const {
// Start by checking the constant declarations.
std::set<storm::expressions::Variable> all;
std::set<storm::expressions::Variable> allGlobals;
@ -604,40 +614,6 @@ namespace storm {
std::set<storm::expressions::Variable> variablesAndConstants;
std::set_union(variables.begin(), variables.end(), constants.begin(), constants.end(), std::inserter(variablesAndConstants, variablesAndConstants.begin()));
// We check for each global variable and each labeled command, whether there is at most one instance writing to that variable.
std::set<std::pair<std::string, std::string>> globalBVarsWrittenToByCommand;
std::set<std::pair<std::string, std::string>> globalIVarsWrittenToByCommand;
for(auto const& module : this->getModules()) {
std::set<std::pair<std::string, std::string>> globalBVarsWrittenToByCommandInThisModule;
std::set<std::pair<std::string, std::string>> globalIVarsWrittenToByCommandInThisModule;
for (auto const& command : module.getCommands()) {
if(!command.isLabeled()) continue;
for (auto const& update : command.getUpdates()) {
for (auto const& assignment : update.getAssignments()) {
if(this->globalBooleanVariableExists(assignment.getVariable().getName())) {
globalBVarsWrittenToByCommandInThisModule.insert({assignment.getVariable().getName(), command.getActionName()});
}
else if(this->globalIntegerVariableExists(assignment.getVariable().getName())) {
globalIVarsWrittenToByCommandInThisModule.insert({assignment.getVariable().getName(), command.getActionName()});
}
}
}
}
for(auto const& entry : globalIVarsWrittenToByCommandInThisModule) {
if(globalIVarsWrittenToByCommand.find(entry) != globalIVarsWrittenToByCommand.end()) {
STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Error in " << module.getFilename() << ", line " << module.getLineNumber() << ": assignment of (possibly) synchronizing command with label '" << entry.second << "' writes to global variable '" << entry.first << "'.");
}
}
for(auto const& entry : globalBVarsWrittenToByCommandInThisModule) {
if(globalBVarsWrittenToByCommand.find(entry) != globalBVarsWrittenToByCommand.end()) {
STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Error in " << module.getFilename() << ", line " << module.getLineNumber() << ": assignment of (possibly) synchronizing command with label '" << entry.second << "' writes to global variable '" << entry.first << "'.");
}
}
globalBVarsWrittenToByCommand.insert(globalBVarsWrittenToByCommandInThisModule.begin(), globalBVarsWrittenToByCommandInThisModule.end());
globalIVarsWrittenToByCommand.insert(globalIVarsWrittenToByCommandInThisModule.begin(), globalIVarsWrittenToByCommandInThisModule.end());
}
// Check the commands of the modules.
bool hasProbabilisticCommand = false;
@ -656,7 +632,7 @@ namespace storm {
// Check the guard.
std::set<storm::expressions::Variable> containedVariables = command.getGuardExpression().getVariables();
bool isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedVariables.begin(), containedVariables.end());
STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": guard refers to unknown identifiers.");
STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": guard " << command.getGuardExpression() << " refers to unknown identifiers.");
STORM_LOG_THROW(command.getGuardExpression().hasBooleanType(), storm::exceptions::WrongFormatException, "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": expression for guard must evaluate to type 'bool'.");
// Record which types of commands were seen.
@ -764,6 +740,103 @@ namespace storm {
bool isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedVariables.begin(), containedVariables.end());
STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << formula.getFilename() << ", line " << formula.getLineNumber() << ": formula expression refers to unknown identifiers.");
}
if(lvl >= Program::ValidityCheckLevel::READYFORPROCESSING) {
// We check for each global variable and each labeled command, whether there is at most one instance writing to that variable.
std::set<std::pair<std::string, std::string>> globalBVarsWrittenToByCommand;
std::set<std::pair<std::string, std::string>> globalIVarsWrittenToByCommand;
for(auto const& module : this->getModules()) {
std::set<std::pair<std::string, std::string>> globalBVarsWrittenToByCommandInThisModule;
std::set<std::pair<std::string, std::string>> globalIVarsWrittenToByCommandInThisModule;
for (auto const& command : module.getCommands()) {
if(!command.isLabeled()) continue;
for (auto const& update : command.getUpdates()) {
for (auto const& assignment : update.getAssignments()) {
if(this->globalBooleanVariableExists(assignment.getVariable().getName())) {
globalBVarsWrittenToByCommandInThisModule.insert({assignment.getVariable().getName(), command.getActionName()});
}
else if(this->globalIntegerVariableExists(assignment.getVariable().getName())) {
globalIVarsWrittenToByCommandInThisModule.insert({assignment.getVariable().getName(), command.getActionName()});
}
}
}
}
for(auto const& entry : globalIVarsWrittenToByCommandInThisModule) {
if(globalIVarsWrittenToByCommand.find(entry) != globalIVarsWrittenToByCommand.end()) {
STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Error in " << module.getFilename() << ", line " << module.getLineNumber() << ": assignment of (possibly) synchronizing command with label '" << entry.second << "' writes to global variable '" << entry.first << "'.");
}
}
for(auto const& entry : globalBVarsWrittenToByCommandInThisModule) {
if(globalBVarsWrittenToByCommand.find(entry) != globalBVarsWrittenToByCommand.end()) {
STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Error in " << module.getFilename() << ", line " << module.getLineNumber() << ": assignment of (possibly) synchronizing command with label '" << entry.second << "' writes to global variable '" << entry.first << "'.");
}
}
}
}
}
Program Program::simplify() {
std::vector<Module> newModules;
std::vector<Constant> newConstants = this->getConstants();
for (auto const& module : this->getModules()) {
std::map<storm::expressions::Variable, storm::expressions::Expression> booleanVars;
std::map<storm::expressions::Variable, storm::expressions::Expression> integerVars;
for (auto const& variable : module.getBooleanVariables()) {
booleanVars.emplace(variable.getExpressionVariable(), variable.getInitialValueExpression());
}
for (auto const& variable : module.getIntegerVariables()) {
integerVars.emplace(variable.getExpressionVariable(), variable.getInitialValueExpression());
}
for (auto const& command : module.getCommands()) {
// Check all updates.
for (auto const& update : command.getUpdates()) {
// Check all assignments.
for (auto const& assignment : update.getAssignments()) {
auto bit = booleanVars.find(assignment.getVariable());
if(bit != booleanVars.end()) {
booleanVars.erase(bit);
} else {
auto iit = integerVars.find(assignment.getVariable());
if(iit != integerVars.end()) {
integerVars.erase(iit);
}
}
}
}
}
std::vector<storm::prism::BooleanVariable> newBVars;
for(auto const& variable : module.getBooleanVariables()) {
if(booleanVars.count(variable.getExpressionVariable()) == 0) {
newBVars.push_back(variable);
}
}
std::vector<storm::prism::IntegerVariable> newIVars;
for(auto const& variable : module.getIntegerVariables()) {
if(integerVars.count(variable.getExpressionVariable()) == 0) {
newIVars.push_back(variable);
}
}
newModules.emplace_back(module.getName(), newBVars, newIVars, module.getCommands());
for(auto const& entry : booleanVars) {
newConstants.emplace_back(entry.first, entry.second);
}
for(auto const& entry : integerVars) {
newConstants.emplace_back(entry.first, entry.second);
}
}
return replaceModulesAndConstantsInProgram(newModules, newConstants).substituteConstants();
}
Program Program::replaceModulesAndConstantsInProgram(std::vector<Module> const& newModules, std::vector<Constant> const& newConstants) {
return Program(this->manager, modelType, newConstants, getGlobalBooleanVariables(), getGlobalIntegerVariables(), getFormulas(), newModules, getActionNameToIndexMapping(), getRewardModels(), false, getInitialConstruct(), getLabels(), "", 0, false);
}
storm::expressions::ExpressionManager const& Program::getManager() const {
@ -818,5 +891,7 @@ namespace storm {
return stream;
}
} // namespace prism
} // namepsace storm

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

@ -24,6 +24,8 @@ namespace storm {
*/
enum class ModelType {UNDEFINED, DTMC, CTMC, MDP, CTMDP, MA};
enum class ValidityCheckLevel : unsigned {VALIDINPUT = 0, READYFORPROCESSING = 1};
/*!
* Creates a program with the given model type, undefined constants, global variables, modules, reward
* models, labels and initial states.
@ -45,9 +47,9 @@ namespace storm {
* @param labels The labels defined for this program.
* @param filename The filename in which the program is defined.
* @param lineNumber The line number in which the program is defined.
* @param checkValidity If set to true, the program is checked for validity.
* @param finalModel If set to true, the program is checked for input-validity, as well as some post-processing.
*/
Program(std::shared_ptr<storm::expressions::ExpressionManager> manager, ModelType modelType, std::vector<Constant> const& constants, std::vector<BooleanVariable> const& globalBooleanVariables, std::vector<IntegerVariable> const& globalIntegerVariables, std::vector<Formula> const& formulas, std::vector<Module> const& modules, std::map<std::string, uint_fast64_t> const& actionToIndexMap, std::vector<RewardModel> const& rewardModels, bool fixInitialConstruct, storm::prism::InitialConstruct const& initialConstruct, std::vector<Label> const& labels, std::string const& filename = "", uint_fast64_t lineNumber = 0, bool checkValidity = true);
Program(std::shared_ptr<storm::expressions::ExpressionManager> manager, ModelType modelType, std::vector<Constant> const& constants, std::vector<BooleanVariable> const& globalBooleanVariables, std::vector<IntegerVariable> const& globalIntegerVariables, std::vector<Formula> const& formulas, std::vector<Module> const& modules, std::map<std::string, uint_fast64_t> const& actionToIndexMap, std::vector<RewardModel> const& rewardModels, bool fixInitialConstruct, storm::prism::InitialConstruct const& initialConstruct, std::vector<Label> const& labels, std::string const& filename = "", uint_fast64_t lineNumber = 0, bool finalModel = true);
// Provide default implementations for constructors and assignments.
Program() = default;
@ -399,11 +401,17 @@ namespace storm {
*/
Program substituteConstants() const;
/**
* Entry point for static analysis for simplify. As we use the same expression manager, we recommend to not use the original program any further.
* @return A simplified, equivalent program.
*/
Program simplify();
/*!
* Checks the validity of the program. If the program is not valid, an exception is thrown with a message
* that indicates the source of the problem.
*/
void checkValidity() const;
void checkValidity(Program::ValidityCheckLevel lvl = Program::ValidityCheckLevel::READYFORPROCESSING) const;
friend std::ostream& operator<<(std::ostream& stream, Program const& program);
@ -431,7 +439,7 @@ namespace storm {
// The type of the model.
ModelType modelType;
// The undefined constants of the program.
// The constants of the program.
std::vector<Constant> constants;
// A mapping from constant names to their corresponding indices.
@ -490,6 +498,14 @@ namespace storm {
// A mapping from variable names to the modules in which they were declared.
std::map<std::string, uint_fast64_t> variableToModuleIndexMap;
/**
* Takes the current program and replaces all modules. As we reuse the expression manager, we recommend to not use the original program any further.
* @param newModules the modules which replace the old modules.
* @param newConstants the constants which replace the old constants.
* @return A program with the new modules and constants.
*/
Program replaceModulesAndConstantsInProgram(std::vector<Module> const& newModules, std::vector<Constant> const& newConstants);
};
} // namespace prism

113
src/utility/cli.h
View File

@ -398,7 +398,10 @@ namespace storm {
boost::optional<storm::prism::Program> program;
if (settings.isSymbolicSet()) {
std::string const& programFile = settings.getSymbolicModelFilename();
program = storm::parser::PrismParser::parse(programFile);
program = storm::parser::PrismParser::parse(programFile).simplify();
program->checkValidity();
std::cout << program.get() << std::endl;
}
// Then proceed to parsing the property (if given), since the model we are building may depend on the property.
@ -414,68 +417,68 @@ namespace storm {
}
formulas.push_back(formula);
}
else if (settings.isPropertyFileSet()) {
std::cout << "Reading properties from " << settings.getPropertiesFilename() << std::endl;
else if (settings.isPropertyFileSet()) {
std::cout << "Reading properties from " << settings.getPropertiesFilename() << std::endl;
std::ifstream inputFileStream(settings.getPropertiesFilename(), std::ios::in);
std::ifstream inputFileStream(settings.getPropertiesFilename(), std::ios::in);
std::vector<std::string> properties;
std::vector<std::string> properties;
if (inputFileStream.good()) {
try {
while (inputFileStream.good()) {
std::string prop;
std::getline(inputFileStream, prop);
if (!prop.empty()) {
properties.push_back(prop);
}
}
}
catch (std::exception& e) {
inputFileStream.close();
throw e;
}
inputFileStream.close();
} else {
STORM_LOG_ERROR("Unable to read property file.");
}
if (inputFileStream.good()) {
try {
while (inputFileStream.good()) {
std::string prop;
std::getline(inputFileStream, prop);
if (!prop.empty()) {
properties.push_back(prop);
}
}
}
catch (std::exception& e) {
inputFileStream.close();
throw e;
}
inputFileStream.close();
} else {
STORM_LOG_ERROR("Unable to read property file.");
}
for (std::string prop : properties) {
boost::optional<std::shared_ptr<storm::logic::Formula>> formula;
try {
if (program) {
storm::parser::FormulaParser formulaParser(program.get().getManager().getSharedPointer());
formula = formulaParser.parseFromString(prop);
} else {
storm::parser::FormulaParser formulaParser;
formula = formulaParser.parseFromString(prop);
}
formulas.push_back(formula);
}
catch (storm::exceptions::WrongFormatException &e) {
STORM_LOG_WARN("Unable to parse line as formula: " << prop);
}
}
std::cout << "Parsed " << formulas.size() << " properties from file " << settings.getPropertiesFilename() << std::endl;
}
for (boost::optional<std::shared_ptr<storm::logic::Formula>> formula : formulas) {
if (settings.isSymbolicSet()) {
for (std::string prop : properties) {
boost::optional<std::shared_ptr<storm::logic::Formula>> formula;
try {
if (program) {
storm::parser::FormulaParser formulaParser(program.get().getManager().getSharedPointer());
formula = formulaParser.parseFromString(prop);
} else {
storm::parser::FormulaParser formulaParser;
formula = formulaParser.parseFromString(prop);
}
formulas.push_back(formula);
}
catch (storm::exceptions::WrongFormatException &e) {
STORM_LOG_WARN("Unable to parse line as formula: " << prop);
}
}
std::cout << "Parsed " << formulas.size() << " properties from file " << settings.getPropertiesFilename() << std::endl;
}
for (boost::optional<std::shared_ptr<storm::logic::Formula>> formula : formulas) {
if (settings.isSymbolicSet()) {
#ifdef STORM_HAVE_CARL
if (settings.isParametricSet()) {
buildAndCheckSymbolicModel<storm::RationalFunction>(program.get(), formula);
} else {
if (settings.isParametricSet()) {
buildAndCheckSymbolicModel<storm::RationalFunction>(program.get(), formula);
} else {
#endif
buildAndCheckSymbolicModel<double>(program.get(), formula);
buildAndCheckSymbolicModel<double>(program.get(), formula);
#ifdef STORM_HAVE_CARL
}
}
#endif
} else if (settings.isExplicitSet()) {
buildAndCheckExplicitModel<double>(formula);
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No input model.");
}
}
} else if (settings.isExplicitSet()) {
buildAndCheckExplicitModel<double>(formula);
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No input model.");
}
}
}
}
}

Write Preview
Loading…
Cancel
Save