From 7d84b0a4c58dd731ef5d0ed5a903f05447814a47 Mon Sep 17 00:00:00 2001
From: David_Korzeniewski <david.korzeniewski@rwth-aachen.de>
Date: Fri, 29 May 2015 16:41:25 +0200
Subject: [PATCH] Added ability to check properties from property file to cli
 utility. Added minimal example for lra on dtmc

Former-commit-id: eec774f05a71b27e61a93eb2dd3971ad56f64b96
---
 examples/dtmc/tiny_lra/tiny_lra.pctl |  1 +
 examples/dtmc/tiny_lra/tiny_lra.pm   | 16 +++++++
 src/utility/cli.h                    | 63 ++++++++++++++++++++++------
 3 files changed, 68 insertions(+), 12 deletions(-)
 create mode 100644 examples/dtmc/tiny_lra/tiny_lra.pctl
 create mode 100644 examples/dtmc/tiny_lra/tiny_lra.pm

diff --git a/examples/dtmc/tiny_lra/tiny_lra.pctl b/examples/dtmc/tiny_lra/tiny_lra.pctl
new file mode 100644
index 000000000..27700ade2
--- /dev/null
+++ b/examples/dtmc/tiny_lra/tiny_lra.pctl
@@ -0,0 +1 @@
+LRA=? [ "a" ]
\ No newline at end of file
diff --git a/examples/dtmc/tiny_lra/tiny_lra.pm b/examples/dtmc/tiny_lra/tiny_lra.pm
new file mode 100644
index 000000000..0d49f8d3c
--- /dev/null
+++ b/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;
+
diff --git a/src/utility/cli.h b/src/utility/cli.h
index 7fd03536d..efc3f62f7 100644
--- a/src/utility/cli.h
+++ b/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,23 +593,61 @@ 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;
+				}
                 
-                if (settings.isSymbolicSet()) {
+				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.");
+					}
+				}
             }
         }
     }