BIsmulation simplification bisimulation + fix lattice

src/storm-pars-cli/storm-pars.cpp

@@ -568,6 +568,28 @@ namespace storm {
 
             STORM_LOG_THROW(model || input.properties.empty(), storm::exceptions::InvalidSettingsException, "No input model.");
 
+
+
+            if (model) {
+                auto preprocessingResult = storm::pars::preprocessModel<DdType, ValueType>(model, input);
+                if (preprocessingResult.changed) {
+                    model = preprocessingResult.model;
+
+                    if (preprocessingResult.formulas) {
+                        std::vector<storm::jani::Property> newProperties;
+                        for (size_t i = 0; i < preprocessingResult.formulas.get().size(); ++i) {
+                            auto formula = preprocessingResult.formulas.get().at(i);
+                            STORM_LOG_ASSERT(i < input.properties.size(), "Index " << i << " greater than number of properties.");
+                            storm::jani::Property property = input.properties.at(i);
+                            newProperties.push_back(storm::jani::Property(property.getName(), formula, property.getUndefinedConstants(), property.getComment()));
+                        }
+                        input.properties = newProperties;
+                    }
+
+                    model->printModelInformationToStream(std::cout);
+                }
+            }
+
             if (parSettings.isMonotonicityAnalysisSet()) {
                 std::cout << "Hello, Jip1" << std::endl;
                 // Simplify the model
@@ -612,7 +634,7 @@ namespace storm {
                 std::cout << "Bye, Jip1" << std::endl;
             }
 
-            if (model) {
+            if (parSettings.isMonotonicityAnalysisSet() && model) {
                 auto preprocessingResult = storm::pars::preprocessModel<DdType, ValueType>(model, input);
                 if (preprocessingResult.changed) {
                     model = preprocessingResult.model;
@@ -632,6 +654,7 @@ namespace storm {
                 }
             }
 
+
             if (parSettings.isSccEliminationSet()) {
                 storm::utility::Stopwatch eliminationWatch(true);
                 // TODO: check for correct Model type