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

Former-commit-id: 3a9965dcfd

examples/dtmc/tiny_lra/tiny_lra.pctl

@@ -0,0 +1 @@
+LRA=? [ "a" ]

examples/dtmc/tiny_lra/tiny_lra.pm

@@ -0,0 +1,16 @@
+// tiny LRA example
+
+dtmc
+
+module main
+	
+	s : [0..2] init 0;
+	
+	[] s=0 -> 1:(s'=1);
+	[] s=1 -> 0.5:(s'=1) + 0.5:(s'=2);
+	[] s=2 -> 0.5:(s'=1) + 0.5:(s'=2);
+	
+endmodule
+
+label "a" = s=1;
+

src/utility/cli.h

@@ -583,8 +583,9 @@ namespace storm {
                 }
                 
                 // Then proceed to parsing the property (if given), since the model we are building may depend on the property.
-                boost::optional<std::shared_ptr<storm::logic::Formula>> formula;
+                std::vector<boost::optional<std::shared_ptr<storm::logic::Formula>>> formulas;
                 if (settings.isPropertySet()) {
+					boost::optional<std::shared_ptr<storm::logic::Formula>> formula;
                     if (program) {
                         storm::parser::FormulaParser formulaParser(program.get().getManager().getSharedPointer());
                         formula = formulaParser.parseFromString(settings.getProperty());
@@ -592,8 +593,45 @@ namespace storm {
                         storm::parser::FormulaParser formulaParser;
                         formula = formulaParser.parseFromString(settings.getProperty());
                     }
+					formulas.push_back(formula);
+                }
+				else if (settings.isPropertyFileSet()) {
+					std::cout << "Reading properties from " << settings.getPropertiesFilename() << std::endl;
+
+					std::ifstream inputFileStream(settings.getPropertiesFilename(), std::ios::in);
+
+					std::vector<std::string> properties;
+
+					if (inputFileStream.good()) {
+						try {
+							std::string prop;
+							std::getline(inputFileStream, prop);
+							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;
+						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);
+					}
+					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()) {
@@ -613,5 +651,6 @@ namespace storm {
             }
         }
     }
+}
 
 #endif