diff --git a/src/models/sparse/Mdp.cpp b/src/models/sparse/Mdp.cpp
index 1c8bd1b50..469dfe54e 100644
--- a/src/models/sparse/Mdp.cpp
+++ b/src/models/sparse/Mdp.cpp
@@ -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;
diff --git a/src/models/sparse/Mdp.h b/src/models/sparse/Mdp.h
index 18879ee76..3b66d0e61 100644
--- a/src/models/sparse/Mdp.h
+++ b/src/models/sparse/Mdp.h
@@ -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.
diff --git a/src/models/sparse/Model.cpp b/src/models/sparse/Model.cpp
index b2ca03c1d..506083cbc 100644
--- a/src/models/sparse/Model.cpp
+++ b/src/models/sparse/Model.cpp
@@ -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;
diff --git a/src/models/sparse/Model.h b/src/models/sparse/Model.h
index 5457370e6..4d1901d1f 100644
--- a/src/models/sparse/Model.h
+++ b/src/models/sparse/Model.h
@@ -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.
*
diff --git a/src/storage/SparseMatrix.cpp b/src/storage/SparseMatrix.cpp
index ce5419099..2cb9f995b 100644
--- a/src/storage/SparseMatrix.cpp
+++ b/src/storage/SparseMatrix.cpp
@@ -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
diff --git a/src/storage/SparseMatrix.h b/src/storage/SparseMatrix.h
index 35ff09658..7d7092377 100644
--- a/src/storage/SparseMatrix.h
+++ b/src/storage/SparseMatrix.h
@@ -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.
*
diff --git a/src/storage/expressions/IfThenElseExpression.cpp b/src/storage/expressions/IfThenElseExpression.cpp
index f3e65a94f..4692675bf 100644
--- a/src/storage/expressions/IfThenElseExpression.cpp
+++ b/src/storage/expressions/IfThenElseExpression.cpp
@@ -70,7 +70,7 @@ namespace storm {
}
std::shared_ptr<BaseExpression const> IfThenElseExpression::simplify() const {
- std::shared_ptr<BaseExpression const> conditionSimplified;
+ std::shared_ptr<BaseExpression const> conditionSimplified = this->condition->simplify();
if (conditionSimplified->isTrue()) {
return this->thenExpression->simplify();
} else if (conditionSimplified->isFalse()) {
diff --git a/src/storage/prism/Program.cpp b/src/storage/prism/Program.cpp
index 0b61fd795..3792bea94 100644
--- a/src/storage/prism/Program.cpp
+++ b/src/storage/prism/Program.cpp
@@ -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()
+ {
this->createMappings();
// Create a new initial construct if the corresponding flag was set.
@@ -36,7 +45,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()) {
@@ -51,9 +61,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);
}
}
@@ -509,7 +518,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;
@@ -602,40 +612,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;
@@ -654,7 +630,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.
@@ -762,6 +738,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 {
@@ -816,5 +889,7 @@ namespace storm {
return stream;
}
+
+
} // namespace prism
} // namepsace storm
diff --git a/src/storage/prism/Program.h b/src/storage/prism/Program.h
index 94bcf7353..6a124e4e0 100644
--- a/src/storage/prism/Program.h
+++ b/src/storage/prism/Program.h
@@ -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
diff --git a/src/utility/cli.h b/src/utility/cli.h
index 3e1b820e4..8a28cb0e4 100644
--- a/src/utility/cli.h
+++ b/src/utility/cli.h
@@ -400,7 +400,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.
@@ -416,68 +419,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.");
+ }
+ }
}
}
}