added composition specification to PRISM program

Former-commit-id: 2c032f5d7e

src/builder/DdPrismModelBuilder.cpp

@@ -799,7 +799,7 @@ namespace storm {
             STORM_LOG_TRACE("Translating (first) module '" << generationInfo.program.getModule(0).getName() << "'.");
             ModuleDecisionDiagram system = createModuleDecisionDiagram(generationInfo, generationInfo.program.getModule(0), synchronizingActionToOffsetMap);
 
-            // No translate module by module and combine it with the system created thus far.
+            // Now translate module by module and combine it with the system created thus far.
             for (uint_fast64_t i = 1; i < generationInfo.program.getNumberOfModules(); ++i) {
                 storm::prism::Module const& currentModule = generationInfo.program.getModule(i);
                 STORM_LOG_TRACE("Translating module '" << currentModule.getName() << "'.");

src/parser/PrismParser.cpp

@@ -570,7 +570,7 @@ namespace storm {
         }
         
         storm::prism::Program PrismParser::createProgram(GlobalProgramInformation const& globalProgramInformation) const {
-            return storm::prism::Program(manager, globalProgramInformation.modelType, globalProgramInformation.constants, globalProgramInformation.globalBooleanVariables, globalProgramInformation.globalIntegerVariables, globalProgramInformation.formulas, globalProgramInformation.modules, globalProgramInformation.actionIndices, globalProgramInformation.rewardModels, this->secondRun && !globalProgramInformation.hasInitialConstruct, globalProgramInformation.initialConstruct, globalProgramInformation.labels, this->getFilename(), 1, this->secondRun);
+            return storm::prism::Program(manager, globalProgramInformation.modelType, globalProgramInformation.constants, globalProgramInformation.globalBooleanVariables, globalProgramInformation.globalIntegerVariables, globalProgramInformation.formulas, globalProgramInformation.modules, globalProgramInformation.actionIndices, globalProgramInformation.rewardModels, globalProgramInformation.labels, secondRun && !globalProgramInformation.hasInitialConstruct ? boost::none : boost::optional<storm::prism::InitialConstruct>(storm::prism::InitialConstruct(manager->boolean(false))), boost::none, this->getFilename(), 1, this->secondRun);
         }
     } // namespace parser
 } // namespace storm

src/solver/GmmxxMinMaxLinearEquationSolver.cpp

@@ -51,7 +51,7 @@ namespace storm {
 
 				// Proceed with the iterations as long as the method did not converge or reach the user-specified maximum number
 				// of iterations.
-				while (!converged && iterations < this->maximalNumberOfIterations && !(this->hasCustomTerminationCondition() && this->getTerminationCondition().terminateNow(*currentX))) {
+				while (!converged && iterations < this->maximalNumberOfIterations) {
 					// Compute x' = A*x + b.
 					gmm::mult(*gmmxxMatrix, *currentX, *multiplyResult);
 					gmm::add(b, *multiplyResult);
@@ -60,7 +60,7 @@ namespace storm {
 					storm::utility::vector::reduceVectorMinOrMax(dir, *multiplyResult, *newX, rowGroupIndices);
 					
 					// Determine whether the method converged.
-					converged = storm::utility::vector::equalModuloPrecision(*currentX, *newX, this->precision, this->relative);
+					converged = storm::utility::vector::equalModuloPrecision(*currentX, *newX, this->precision, this->relative) || (this->hasCustomTerminationCondition() && this->getTerminationCondition().terminateNow(*newX));
 
 					// Update environment variables.
 					std::swap(currentX, newX);

src/storage/prism/Assignment.cpp

@@ -26,12 +26,6 @@ namespace storm {
         bool Assignment::isIdentity() const {
             if(this->expression.isVariable()) {
                 assert(this->expression.getVariables().size() == 1);
-                //if( variable == *(this->expression.getVariables().begin())) {
-                //    std::cout << variable.getName() << " == " << (this->expression.getVariables().begin())->getName() << std::endl;
-                //}
-                //else {
-                //    std::cout << "********" << variable.getName() << " != " << (this->expression.getVariables().begin())->getName() << std::endl;
-                //}
                 return variable == *(this->expression.getVariables().begin());
             }
             return false;

src/storage/prism/Assignment.h

@@ -61,7 +61,7 @@ namespace storm {
             Assignment substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const;
             
             /*!
-             * Checks whether the assignment is an identity  (lhs equals rhs)
+             * Checks whether the assignment is an identity (lhs equals rhs)
              * 
              * @return true iff the assignment is of the form a' = a.
              */

src/storage/prism/Composition.cpp

@@ -0,0 +1,12 @@
+#include "src/storage/prism/Composition.h"
+
+namespace storm {
+    namespace prism {
+        
+        std::ostream& operator<<(std::ostream& stream, Composition const& composition) {
+            composition.writeToStream(stream);
+            return stream;
+        }
+        
+    }
+}

src/storage/prism/Composition.h

@@ -0,0 +1,23 @@
+#ifndef STORM_STORAGE_PRISM_COMPOSITION_H_
+#define STORM_STORAGE_PRISM_COMPOSITION_H_
+
+#include <ostream>
+
+namespace storm {
+    namespace prism {
+        class Composition {
+        public:
+            Composition() = default;
+            
+            friend std::ostream& operator<<(std::ostream& stream, Composition const& composition);
+            
+        protected:
+            virtual void writeToStream(std::ostream& stream) const = 0;
+            
+        private:
+            
+        };
+    }
+}
+
+#endif /* STORM_STORAGE_PRISM_COMPOSITION_H_ */

src/storage/prism/CompositionVisitor.h

@@ -0,0 +1,22 @@
+#ifndef STORM_STORAGE_PRISM_COMPOSITIONVISITOR_H_
+#define STORM_STORAGE_PRISM_COMPOSITIONVISITOR_H_
+
+#include <boost/any.hpp>
+
+namespace storm {
+    namespace prism {
+        
+        class ModuleComposition;
+        class RenamingComposition;
+        class ParallelComposition;
+        
+        class CompositionVisitor {
+        public:
+            virtual boost::any visit(ModuleComposition const& composition) = 0;
+            virtual boost::any visit(RenamingComposition const& composition) = 0;
+            virtual boost::any visit(ParallelComposition const& composition) = 0;
+        };
+    }
+}
+
+#endif /* STORM_STORAGE_PRISM_COMPOSITIONVISITOR_H_ */

src/storage/prism/ModuleComposition.cpp

@@ -0,0 +1,14 @@
+#include "src/storage/prism/ModuleComposition.h"
+
+namespace storm {
+    namespace prism {
+        
+        ModuleComposition::ModuleComposition(std::string const& moduleName) : moduleName(moduleName) {
+            // Intentionally left empty.
+        }
+        
+        void ModuleComposition::writeToStream(std::ostream& stream) const {
+            stream << moduleName;
+        }
+    }
+}

src/storage/prism/ModuleComposition.h

@@ -0,0 +1,24 @@
+#ifndef STORM_STORAGE_PRISM_MODULECOMPOSITION_H_
+#define STORM_STORAGE_PRISM_MODULECOMPOSITION_H_
+
+#include <string>
+
+#include "src/storage/prism/Composition.h"
+
+namespace storm {
+    namespace prism {
+        class ModuleComposition : Composition {
+        public:
+            ModuleComposition(std::string const& moduleName);
+            
+        protected:
+            virtual void writeToStream(std::ostream& stream) const override;
+            
+        private:
+            // The name of the module to compose.
+            std::string moduleName;
+        };
+    }
+}
+
+#endif /* STORM_STORAGE_PRISM_MODULECOMPOSITION_H_ */

src/storage/prism/ParallelComposition.cpp

@@ -0,0 +1,17 @@
+#include "src/storage/prism/ParallelComposition.h"
+
+#include <boost/algorithm/string/join.hpp>
+
+namespace storm {
+    namespace prism {
+        
+        ParallelComposition::ParallelComposition(std::shared_ptr<Composition> const& left, std::set<std::string> const& synchronizingActions, std::shared_ptr<Composition> const& right) : left(left), synchronizingActions(synchronizingActions), right(right) {
+            // Intentionally left empty.
+        }
+        
+        void ParallelComposition::writeToStream(std::ostream& stream) const {
+            stream << "(" << *left << " |[" << boost::algorithm::join(synchronizingActions, ", ") << "]| " << *right << ")";
+        }
+
+    }
+}

src/storage/prism/ParallelComposition.h

@@ -0,0 +1,26 @@
+#ifndef STORM_STORAGE_PRISM_PARALLELCOMPOSITION_H_
+#define STORM_STORAGE_PRISM_PARALLELCOMPOSITION_H_
+
+#include <set>
+#include <string>
+
+#include "src/storage/prism/Composition.h"
+
+namespace storm {
+    namespace prism {
+        class ParallelComposition : Composition {
+        public:
+            ParallelComposition(std::shared_ptr<Composition> const& left, std::set<std::string> const& synchronizingActions, std::shared_ptr<Composition> const& right);
+            
+        protected:
+            virtual void writeToStream(std::ostream& stream) const override;
+            
+        private:
+            std::shared_ptr<Composition> left;
+            std::set<std::string> synchronizingActions;
+            std::shared_ptr<Composition> right;
+        };
+    }
+}
+
+#endif /* STORM_STORAGE_PRISM_PARALLELCOMPOSITION_H_ */

src/storage/prism/Program.cpp

@@ -17,13 +17,13 @@
 
 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 finalModel) 
+        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, std::vector<Label> const& labels, boost::optional<InitialConstruct> const& initialConstruct, boost::optional<std::shared_ptr<Composition>> const& composition, 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), 
+            rewardModels(rewardModels), rewardModelToIndexMap(), systemComposition(composition),
             labels(labels), labelToIndexMap(), actionToIndexMap(actionToIndexMap), indexToActionMap(), actions(),
             synchronizingActionIndices(), actionIndicesToModuleIndexMap(), variableToModuleIndexMap()
         {
@@ -31,8 +31,11 @@ namespace storm {
             // Start by creating the necessary mappings from the given ones.
             this->createMappings();
 
-            // Create a new initial construct if the corresponding flag was set.
-            if (fixInitialConstruct) {
+            // Set the initial construct.
+            if (initialConstruct) {
+                this->initialConstruct = initialConstruct.get();
+            } else {
+                // Create a new initial construct if none was given.
                 storm::expressions::Expression newInitialExpression = manager->boolean(true);
                 
                 for (auto const& booleanVariable : this->getGlobalBooleanVariables()) {
@@ -53,7 +56,6 @@ namespace storm {
             }
 
             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()) {
@@ -293,6 +295,18 @@ namespace storm {
             return this->initialConstruct;
         }
         
+        bool Program::specifiesSystemComposition() const {
+            return static_cast<bool>(systemComposition);
+        }
+        
+        Composition const& Program::getSystemComposition() const {
+            return *systemComposition.get();
+        }
+        
+        boost::optional<std::shared_ptr<Composition>> Program::getOptionalSystemComposition() const {
+            return systemComposition;
+        }
+        
         std::set<std::string> const& Program::getActions() const {
             return this->actions;
         }
@@ -416,7 +430,7 @@ namespace storm {
                 newModules.push_back(module.restrictCommands(indexSet));
             }
             
-            return Program(this->manager, this->getModelType(), this->getConstants(), this->getGlobalBooleanVariables(), this->getGlobalIntegerVariables(), this->getFormulas(), newModules, this->getActionNameToIndexMapping(), this->getRewardModels(), false, this->getInitialConstruct(), this->getLabels());
+            return Program(this->manager, this->getModelType(), this->getConstants(), this->getGlobalBooleanVariables(), this->getGlobalIntegerVariables(), this->getFormulas(), newModules, this->getActionNameToIndexMapping(), this->getRewardModels(), this->getLabels(), this->getInitialConstruct(), this->getOptionalSystemComposition());
         }
         
         void Program::createMappings() {
@@ -516,7 +530,7 @@ namespace storm {
                 STORM_LOG_THROW(definedUndefinedConstants.find(constantExpressionPair.first) != definedUndefinedConstants.end(), storm::exceptions::InvalidArgumentException, "Unable to define non-existant constant.");
             }
             
-            return Program(this->manager, this->getModelType(), newConstants, this->getGlobalBooleanVariables(), this->getGlobalIntegerVariables(), this->getFormulas(), this->getModules(), this->getActionNameToIndexMapping(), this->getRewardModels(), false, this->getInitialConstruct(), this->getLabels());
+            return Program(this->manager, this->getModelType(), newConstants, this->getGlobalBooleanVariables(), this->getGlobalIntegerVariables(), this->getFormulas(), this->getModules(), this->getActionNameToIndexMapping(), this->getRewardModels(), this->getLabels(), this->getInitialConstruct(), this->getOptionalSystemComposition());
         }
         
         Program Program::substituteConstants() const {
@@ -576,7 +590,7 @@ namespace storm {
                 newLabels.emplace_back(label.substitute(constantSubstitution));
             }
             
-            return Program(this->manager, this->getModelType(), newConstants, newBooleanVariables, newIntegerVariables, newFormulas, newModules, this->getActionNameToIndexMapping(), newRewardModels, false, newInitialConstruct, newLabels);
+            return Program(this->manager, this->getModelType(), newConstants, newBooleanVariables, newIntegerVariables, newFormulas, newModules, this->getActionNameToIndexMapping(), newRewardModels, newLabels, newInitialConstruct, this->getOptionalSystemComposition());
         }
         
         void Program::checkValidity(Program::ValidityCheckLevel lvl) const {
@@ -1017,7 +1031,7 @@ namespace storm {
         }
         
         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);
+            return Program(this->manager, modelType, newConstants, getGlobalBooleanVariables(), getGlobalIntegerVariables(), getFormulas(), newModules, getActionNameToIndexMapping(), getRewardModels(), getLabels(), getInitialConstruct(), this->getOptionalSystemComposition());
         }
         
         Program Program::flattenModules(std::unique_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory) const {
@@ -1203,7 +1217,7 @@ namespace storm {
             
             // Finally, we can create the module and the program and return it.
             storm::prism::Module singleModule(newModuleName.str(), allBooleanVariables, allIntegerVariables, newCommands, this->getFilename(), 0);
-            return Program(manager, this->getModelType(), this->getConstants(), std::vector<storm::prism::BooleanVariable>(), std::vector<storm::prism::IntegerVariable>(), this->getFormulas(), {singleModule}, actionToIndexMap, this->getRewardModels(), false, this->getInitialConstruct(), this->getLabels(), this->getFilename(), 0, true);
+            return Program(manager, this->getModelType(), this->getConstants(), std::vector<storm::prism::BooleanVariable>(), std::vector<storm::prism::IntegerVariable>(), this->getFormulas(), {singleModule}, actionToIndexMap, this->getRewardModels(), this->getLabels(), this->getInitialConstruct(), this->getOptionalSystemComposition(), this->getFilename(), 0, true);
         }
 
         std::unordered_map<uint_fast64_t, std::string> Program::buildCommandIndexToActionNameMap() const {
@@ -1353,6 +1367,14 @@ namespace storm {
                 stream << label << std::endl;
             }
             
+            stream << program.getInitialConstruct() << std::endl;
+            
+            if (program.specifiesSystemComposition()) {
+                stream << "system" << std::endl;
+                stream << "\t" << program.getSystemComposition() << std::endl;
+                stream << "endsystem" << std::endl;
+            }
+            
             return stream;
         }
         

src/storage/prism/Program.h

@@ -1,10 +1,12 @@
 #ifndef STORM_STORAGE_PRISM_PROGRAM_H_
 #define STORM_STORAGE_PRISM_PROGRAM_H_
 
+#include <memory>
 #include <map>
 #include <vector>
 #include <set>
 #include <boost/container/flat_set.hpp>
+#include <boost/optional.hpp>
 
 #include "src/storage/prism/Constant.h"
 #include "src/storage/prism/Formula.h"
@@ -12,6 +14,7 @@
 #include "src/storage/prism/Module.h"
 #include "src/storage/prism/RewardModel.h"
 #include "src/storage/prism/InitialConstruct.h"
+#include "src/storage/prism/Composition.h"
 #include "src/utility/solver.h"
 #include "src/utility/OsDetection.h"
 
@@ -38,18 +41,17 @@ namespace storm {
              * @param formulas The formulas defined in the program.
              * @param modules The modules of the program.
              * @param actionToIndexMap A mapping of action names to their indices.
-             * @param fixInitialConstruct A flag that indicates whether the given initial construct is to be ignored and
-             * replaced by a new one created from the initial values of the variables.
-             * @param initialConstruct The initial construct of the program. If the initial construct specifies "false"
-             * as the initial condition, the default values of the variables are used to construct a legal initial
-             * condition.
              * @param rewardModels The reward models of the program.
              * @param labels The labels defined for this program.
+             * @param initialConstruct The initial construct of the program. If none, then an initial construct is built
+             * using the initial values of the variables.
+             * @param composition If not none, specifies how the modules are composed for the full system. If none, the
+             * regular parallel composition is assumed.
              * @param filename The filename in which the program is defined.
              * @param lineNumber The line number in which the program is defined.
              * @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 finalModel = 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, std::vector<Label> const& labels, boost::optional<InitialConstruct> const& initialConstruct, boost::optional<std::shared_ptr<Composition>> const& composition, std::string const& filename = "", uint_fast64_t lineNumber = 0, bool finalModel = true);
             
             // Provide default implementations for constructors and assignments.
             Program() = default;
@@ -100,7 +102,7 @@ namespace storm {
              *
              * @return The undefined constants in the program.
              */
-            std::vector<std::reference_wrapper<storm::prism::Constant const>> getUndefinedConstants() const;
+            std::vector<std::reference_wrapper<Constant const>> getUndefinedConstants() const;
 
             /*!
              * Retrieves the undefined constants in the program as a comma-separated string.
@@ -262,7 +264,29 @@ namespace storm {
              *
              * @return The initial construct of the program.
              */
-            storm::prism::InitialConstruct const& getInitialConstruct() const;
+            InitialConstruct const& getInitialConstruct() const;
+            
+            /*!
+             * Retrieves whether the program specifies a system composition in terms of process algebra operations over
+             * the modules.
+             *
+             * @return True iff the program specifies a system composition.
+             */
+            bool specifiesSystemComposition() const;
+            
+            /*!
+             * If the program specifies a system composition, this method retrieves it.
+             *
+             * @return The system composition as specified by the program.
+             */
+            Composition const& getSystemComposition() const;
+            
+            /*!
+             * Retrieves the system composition (if any) and none otherwise.
+             *
+             * @return The system composition specified by the program or none.
+             */
+            boost::optional<std::shared_ptr<Composition>> getOptionalSystemComposition() const;
             
             /*!
              * Retrieves the set of actions present in the program.
@@ -549,7 +573,10 @@ namespace storm {
             std::map<std::string, uint_fast64_t> rewardModelToIndexMap;
             
             // The initial construct of the program.
-            storm::prism::InitialConstruct initialConstruct;
+            InitialConstruct initialConstruct;
+            
+            // If set, this specifies the way the modules are composed to obtain the full system.
+            boost::optional<std::shared_ptr<Composition>> systemComposition;
             
             // The labels that are defined for this model.
             std::vector<Label> labels;

src/storage/prism/RenamingComposition.cpp

@@ -0,0 +1,28 @@
+#include "src/storage/prism/RenamingComposition.h"
+
+#include <vector>
+#include <sstream>
+#include <boost/algorithm/string/join.hpp>
+
+namespace storm {
+    namespace prism {
+        
+        RenamingComposition::RenamingComposition(std::shared_ptr<Composition> const& left, std::map<std::string, boost::optional<std::string>> const& actionRenaming) : left(left), actionRenaming(actionRenaming) {
+            // Intentionally left empty.
+        }
+        
+        void RenamingComposition::writeToStream(std::ostream& stream) const {
+            std::vector<std::string> renamings;
+            for (auto const& renaming : actionRenaming) {
+                std::stringstream s;
+                if (renaming.second) {
+                    s << renaming.second.get();
+                }
+                s << " <- " << renaming.first;
+                renamings.push_back(s.str());
+            }
+            stream << *left << "{" << boost::join(renamings, ", ") << "}";
+        }
+        
+    }
+}

src/storage/prism/RenamingComposition.h

@@ -0,0 +1,28 @@
+#ifndef STORM_STORAGE_PRISM_RENAMINGCOMPOSITION_H_
+#define STORM_STORAGE_PRISM_RENAMINGCOMPOSITION_H_
+
+#include <string>
+#include <map>
+#include <boost/optional.hpp>
+
+#include "src/storage/prism/Composition.h"
+
+namespace storm {
+    namespace prism {
+        class RenamingComposition : Composition {
+        public:
+            RenamingComposition(std::shared_ptr<Composition> const& left, std::map<std::string, boost::optional<std::string>> const& actionRenaming);
+            
+        protected:
+            virtual void writeToStream(std::ostream& stream) const override;
+            
+        private:
+            std::shared_ptr<Composition> left;
+            
+            // The renaming of action indices to apply. If the target name is none, the action is hidden.
+            std::map<std::string, boost::optional<std::string>> actionRenaming;
+        };
+    }
+}
+
+#endif /* STORM_STORAGE_PRISM_RENAMINGCOMPOSITION_H_ */