added all composition operators of PRISM

Former-commit-id: f9a25fbcb1

src/generator/PrismNextStateGenerator.cpp

@@ -11,7 +11,7 @@ namespace storm {
         
         template<typename ValueType, typename StateType>
         PrismNextStateGenerator<ValueType, StateType>::PrismNextStateGenerator(storm::prism::Program const& program, VariableInformation const& variableInformation, bool buildChoiceLabeling) : program(program), selectedRewardModels(), buildChoiceLabeling(buildChoiceLabeling), variableInformation(variableInformation), evaluator(program.getManager()), state(nullptr), comparator() {
-            // Intentionally left empty.
+            STORM_LOG_THROW(!program.specifiesSystemComposition(), storm::exceptions::WrongFormatException, "The explicit next-state generator currently does not support custom system compositions.");
         }
                 
         template<typename ValueType, typename StateType>

src/parser/PrismParser.cpp

@@ -1,5 +1,7 @@
 #include "src/parser/PrismParser.h"
 
+#include "src/storage/prism/Compositions.h"
+
 #include "src/settings/SettingsManager.h"
 
 #include "src/exceptions/InvalidArgumentException.h"
@@ -133,6 +135,45 @@ namespace storm {
             initialStatesConstruct = (qi::lit("init") > expressionParser > qi::lit("endinit"))[qi::_pass = phoenix::bind(&PrismParser::addInitialStatesConstruct, phoenix::ref(*this), qi::_1, qi::_r1)];
             initialStatesConstruct.name("initial construct");
             
+            systemCompositionConstruct = (qi::lit("system") > parallelComposition > qi::lit("endsystem"))[phoenix::bind(&PrismParser::addSystemCompositionConstruct, phoenix::ref(*this), qi::_1, qi::_r1)];
+            systemCompositionConstruct.name("system composition construct");
+            
+            actionNameList %= identifier[phoenix::insert(qi::_val, qi::_1)] >> *("," >> identifier[phoenix::insert(qi::_val, qi::_1)]);
+            actionNameList.name("action list");
+            
+            parallelComposition = hidingOrRenamingComposition[qi::_val = qi::_1] >> *((interleavingParallelComposition > hidingOrRenamingComposition)[qi::_val = phoenix::bind(&PrismParser::createInterleavingParallelComposition, phoenix::ref(*this), qi::_val, qi::_1)] |
+                                                                                      (synchronizingParallelComposition > hidingOrRenamingComposition)[qi::_val = phoenix::bind(&PrismParser::createSynchronizingParallelComposition, phoenix::ref(*this), qi::_val, qi::_1)] |
+                                                                                      (restrictedParallelComposition > hidingOrRenamingComposition)[qi::_val = phoenix::bind(&PrismParser::createRestrictedParallelComposition, phoenix::ref(*this), qi::_val, qi::_1, qi::_2)]
+                                                                                      );
+            parallelComposition.name("parallel composition");
+
+            synchronizingParallelComposition = qi::lit("||");
+            synchronizingParallelComposition.name("synchronizing parallel composition");
+            
+            interleavingParallelComposition = qi::lit("|||");
+            interleavingParallelComposition.name("interleaving parallel composition");
+
+            restrictedParallelComposition = qi::lit("|[") > actionNameList > qi::lit("]|");
+            restrictedParallelComposition.name("restricted parallel composition");
+            
+            hidingOrRenamingComposition = hidingComposition | renamingComposition | atomicComposition;
+            hidingOrRenamingComposition.name("hiding/renaming composition");
+            
+            hidingComposition = (atomicComposition >> qi::lit("/") > (qi::lit("{") > actionNameList > qi::lit("}")))[qi::_val = phoenix::bind(&PrismParser::createHidingComposition, phoenix::ref(*this), qi::_1, qi::_2)];
+            hidingComposition.name("hiding composition");
+            
+            actionRenamingList = +(identifier >> (qi::lit("<-") >> identifier))[phoenix::insert(qi::_val, phoenix::construct<std::pair<std::string, std::string>>(qi::_2, qi::_1))];
+            actionRenamingList.name("action renaming list");
+            
+            renamingComposition = (atomicComposition >> qi::lit("{") > (actionRenamingList > qi::lit("}")))[qi::_val = phoenix::bind(&PrismParser::createRenamingComposition, phoenix::ref(*this), qi::_1, qi::_2)];
+            renamingComposition.name("renaming composition");
+            
+            atomicComposition = qi::lit("(") > parallelComposition > qi::lit(")") | moduleComposition;
+            atomicComposition.name("atomic composition");
+            
+            moduleComposition = identifier[qi::_val = phoenix::bind(&PrismParser::createModuleComposition, phoenix::ref(*this), qi::_1)];
+            moduleComposition.name("module composition");
+            
             labelDefinition = (qi::lit("label") > -qi::lit("\"") > identifier > -qi::lit("\"") > qi::lit("=") > expressionParser >> qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createLabel, phoenix::ref(*this), qi::_1, qi::_2)];
             labelDefinition.name("label definition");
             
@@ -179,7 +220,7 @@ namespace storm {
                          | labelDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::labels, qi::_a), qi::_1)] 
                          | formulaDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::formulas, qi::_a), qi::_1)]
                      )
-                     > qi::eoi)[qi::_val = phoenix::bind(&PrismParser::createProgram, phoenix::ref(*this), qi::_a)];
+                     > -(systemCompositionConstruct(qi::_a)) > qi::eoi)[qi::_val = phoenix::bind(&PrismParser::createProgram, phoenix::ref(*this), qi::_a)];
             start.name("probabilistic program");
             
             // Enable location tracking for important entities.
@@ -245,6 +286,35 @@ namespace storm {
             return true;
         }
         
+        bool PrismParser::addSystemCompositionConstruct(std::shared_ptr<storm::prism::Composition> const& composition, GlobalProgramInformation& globalProgramInformation) {
+            globalProgramInformation.systemCompositionConstruct = storm::prism::SystemCompositionConstruct(composition, this->getFilename(), get_line(qi::_3));
+            return true;
+        }
+        
+        std::shared_ptr<storm::prism::Composition> PrismParser::createModuleComposition(std::string const& moduleName) const {
+            return std::make_shared<storm::prism::ModuleComposition>(moduleName);
+        }
+        
+        std::shared_ptr<storm::prism::Composition> PrismParser::createRenamingComposition(std::shared_ptr<storm::prism::Composition> const& subcomposition, std::map<std::string, std::string> const& renaming) const {
+            return std::make_shared<storm::prism::RenamingComposition>(subcomposition, renaming);
+        }
+        
+        std::shared_ptr<storm::prism::Composition> PrismParser::createHidingComposition(std::shared_ptr<storm::prism::Composition> const& subcomposition, std::set<std::string> const& actionsToHide) const {
+            return std::make_shared<storm::prism::HidingComposition>(subcomposition, actionsToHide);
+        }
+        
+        std::shared_ptr<storm::prism::Composition> PrismParser::createSynchronizingParallelComposition(std::shared_ptr<storm::prism::Composition> const& left, std::shared_ptr<storm::prism::Composition> const& right) const {
+            return std::make_shared<storm::prism::SynchronizingParallelComposition>(left, right);
+        }
+        
+        std::shared_ptr<storm::prism::Composition> PrismParser::createInterleavingParallelComposition(std::shared_ptr<storm::prism::Composition> const& left, std::shared_ptr<storm::prism::Composition> const& right) const {
+            return std::make_shared<storm::prism::InterleavingParallelComposition>(left, right);
+        }
+        
+        std::shared_ptr<storm::prism::Composition> PrismParser::createRestrictedParallelComposition(std::shared_ptr<storm::prism::Composition> const& left, std::set<std::string> const& synchronizingActions, std::shared_ptr<storm::prism::Composition> const& right) const {
+            return std::make_shared<storm::prism::RestrictedParallelComposition>(left, synchronizingActions, right);
+        }
+        
         storm::prism::Constant PrismParser::createUndefinedBooleanConstant(std::string const& newConstant) const {
             if (!this->secondRun) {
                 try {
@@ -570,7 +640,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, 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);
+            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))), globalProgramInformation.systemCompositionConstruct, this->getFilename(), 1, this->secondRun);
         }
     } // namespace parser
 } // namespace storm

src/parser/PrismParser.h

@@ -24,7 +24,7 @@ namespace storm {
         class GlobalProgramInformation {
         public:
             // Default construct the header information.
-            GlobalProgramInformation() : modelType(), constants(), formulas(), globalBooleanVariables(), globalIntegerVariables(), moduleToIndexMap(), actionIndices(), modules(), rewardModels(), labels(), hasInitialConstruct(false), initialConstruct(), currentCommandIndex(0), currentUpdateIndex(0) {
+            GlobalProgramInformation() : modelType(), constants(), formulas(), globalBooleanVariables(), globalIntegerVariables(), moduleToIndexMap(), actionIndices(), modules(), rewardModels(), labels(), hasInitialConstruct(false), initialConstruct(), systemCompositionConstruct(boost::none), currentCommandIndex(0), currentUpdateIndex(0) {
                 // Map the empty action to index 0.
                 actionIndices.emplace("", 0);
             }
@@ -42,6 +42,7 @@ namespace storm {
             std::vector<storm::prism::Label> labels;
             bool hasInitialConstruct;
             storm::prism::InitialConstruct initialConstruct;
+            boost::optional<storm::prism::SystemCompositionConstruct> systemCompositionConstruct;
             
             // Counters to provide unique indexing for commands and updates.
             uint_fast64_t currentCommandIndex;
@@ -206,6 +207,20 @@ namespace storm {
             // Rules for initial states expression.
             qi::rule<Iterator, qi::unused_type(GlobalProgramInformation&), Skipper> initialStatesConstruct;
             
+            // Rules for the system composition.
+            qi::rule<Iterator, qi::unused_type(GlobalProgramInformation&), Skipper> systemCompositionConstruct;
+            qi::rule<Iterator, std::shared_ptr<storm::prism::Composition>(), Skipper> parallelComposition;
+            qi::rule<Iterator, qi::unused_type(), Skipper> synchronizingParallelComposition;
+            qi::rule<Iterator, qi::unused_type(), Skipper> interleavingParallelComposition;
+            qi::rule<Iterator, std::set<std::string>(), Skipper> restrictedParallelComposition;
+            qi::rule<Iterator, std::shared_ptr<storm::prism::Composition>(), Skipper> hidingOrRenamingComposition;
+            qi::rule<Iterator, std::shared_ptr<storm::prism::Composition>(), Skipper> hidingComposition;
+            qi::rule<Iterator, std::shared_ptr<storm::prism::Composition>(), Skipper> renamingComposition;
+            qi::rule<Iterator, std::shared_ptr<storm::prism::Composition>(), Skipper> atomicComposition;
+            qi::rule<Iterator, std::shared_ptr<storm::prism::Composition>(), Skipper> moduleComposition;
+            qi::rule<Iterator, std::set<std::string>(), Skipper> actionNameList;
+            qi::rule<Iterator, std::map<std::string, std::string>(), Skipper> actionRenamingList;
+
             // Rules for label definitions.
             qi::rule<Iterator, storm::prism::Label(), Skipper> labelDefinition;
             
@@ -227,7 +242,16 @@ namespace storm {
             // Helper methods used in the grammar.
             bool isValidIdentifier(std::string const& identifier);
             bool addInitialStatesConstruct(storm::expressions::Expression initialStatesExpression, GlobalProgramInformation& globalProgramInformation);
+            bool addSystemCompositionConstruct(std::shared_ptr<storm::prism::Composition> const& composition, GlobalProgramInformation& globalProgramInformation);
+            
             
+            std::shared_ptr<storm::prism::Composition> createModuleComposition(std::string const& moduleName) const;
+            std::shared_ptr<storm::prism::Composition> createRenamingComposition(std::shared_ptr<storm::prism::Composition> const& subcomposition, std::map<std::string, std::string> const& renaming) const;
+            std::shared_ptr<storm::prism::Composition> createHidingComposition(std::shared_ptr<storm::prism::Composition> const& subcomposition, std::set<std::string> const& actionsToHide) const;
+            std::shared_ptr<storm::prism::Composition> createSynchronizingParallelComposition(std::shared_ptr<storm::prism::Composition> const& left, std::shared_ptr<storm::prism::Composition> const& right) const;
+            std::shared_ptr<storm::prism::Composition> createInterleavingParallelComposition(std::shared_ptr<storm::prism::Composition> const& left, std::shared_ptr<storm::prism::Composition> const& right) const;
+            std::shared_ptr<storm::prism::Composition> createRestrictedParallelComposition(std::shared_ptr<storm::prism::Composition> const& left, std::set<std::string> const& synchronizingActions, std::shared_ptr<storm::prism::Composition> const& right) const;
+
             storm::prism::Constant createUndefinedBooleanConstant(std::string const& newConstant) const;
             storm::prism::Constant createUndefinedIntegerConstant(std::string const& newConstant) const;
             storm::prism::Constant createUndefinedDoubleConstant(std::string const& newConstant) const;

src/storage/prism/Composition.h

@@ -3,6 +3,8 @@
 
 #include <ostream>
 
+#include "src/storage/prism/CompositionVisitor.h"
+
 namespace storm {
     namespace prism {
         class Composition {
@@ -11,6 +13,8 @@ namespace storm {
             
             friend std::ostream& operator<<(std::ostream& stream, Composition const& composition);
             
+            virtual boost::any accept(CompositionVisitor& visitor) const = 0;
+            
         protected:
             virtual void writeToStream(std::ostream& stream) const = 0;
             

src/storage/prism/CompositionVisitor.h

@@ -8,13 +8,19 @@ namespace storm {
         
         class ModuleComposition;
         class RenamingComposition;
-        class ParallelComposition;
+        class HidingComposition;
+        class SynchronizingParallelComposition;
+        class InterleavingParallelComposition;
+        class RestrictedParallelComposition;
         
         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;
+            virtual boost::any visit(HidingComposition const& composition) = 0;
+            virtual boost::any visit(SynchronizingParallelComposition const& composition) = 0;
+            virtual boost::any visit(InterleavingParallelComposition const& composition) = 0;
+            virtual boost::any visit(RestrictedParallelComposition const& composition) = 0;
         };
     }
 }

src/storage/prism/Compositions.h

@@ -0,0 +1,6 @@
+#include "src/storage/prism/ModuleComposition.h"
+#include "src/storage/prism/RestrictedParallelComposition.h"
+#include "src/storage/prism/RenamingComposition.h"
+#include "src/storage/prism/SynchronizingParallelComposition.h"
+#include "src/storage/prism/InterleavingParallelComposition.h"
+#include "src/storage/prism/HidingComposition.h"

src/storage/prism/HidingComposition.cpp

@@ -0,0 +1,25 @@
+#include "src/storage/prism/HidingComposition.h"
+
+#include <boost/algorithm/string/join.hpp>
+
+namespace storm {
+    namespace prism {
+        
+        HidingComposition::HidingComposition(std::shared_ptr<Composition> const& sub, std::set<std::string> const& actionsToHide) : sub(sub), actionsToHide(actionsToHide) {
+            // Intentionally left empty.
+        }
+
+        boost::any HidingComposition::accept(CompositionVisitor& visitor) const {
+            return visitor.visit(*this);
+        }
+        
+        Composition const& HidingComposition::getSubcomposition() const {
+            return *sub;
+        }
+        
+        void HidingComposition::writeToStream(std::ostream& stream) const {
+            stream << "(" << *sub << ")" << " " << "{" << boost::join(actionsToHide, ", ") << "}";
+        }
+
+    }
+}

src/storage/prism/HidingComposition.h

@@ -0,0 +1,31 @@
+#ifndef STORM_STORAGE_PRISM_HIDINGCOMPOSITION_H_
+#define STORM_STORAGE_PRISM_HIDINGCOMPOSITION_H_
+
+#include <set>
+#include <string>
+
+#include "src/storage/prism/Composition.h"
+
+namespace storm {
+    namespace prism {
+        class HidingComposition : public Composition {
+        public:
+            HidingComposition(std::shared_ptr<Composition> const& sub, std::set<std::string> const& actionsToHide);
+            
+            virtual boost::any accept(CompositionVisitor& visitor) const override;
+            
+            Composition const& getSubcomposition() const;
+            
+        protected:
+            virtual void writeToStream(std::ostream& stream) const override;
+            
+        private:
+            std::shared_ptr<Composition> sub;
+            
+            // The actions to hide.
+            std::set<std::string> actionsToHide;
+        };
+    }
+}
+
+#endif /* STORM_STORAGE_PRISM_HIDINGCOMPOSITION_H_ */

src/storage/prism/InitialConstruct.h

@@ -10,17 +10,15 @@
 
 
 namespace storm {
-        namespace expressions {
-            class Variable;
-        }
+    namespace expressions {
+        class Variable;
+    }
 }
 
-
-
 namespace storm {
     namespace prism {
         class InitialConstruct : public LocatedInformation {
-            public:
+        public:
             /*!
              * Creates an initial construct with the given expression.
              *

src/storage/prism/InterleavingParallelComposition.cpp

@@ -0,0 +1,19 @@
+#include "src/storage/prism/InterleavingParallelComposition.h"
+
+namespace storm {
+    namespace prism {
+        
+        InterleavingParallelComposition::InterleavingParallelComposition(std::shared_ptr<Composition> const& left, std::shared_ptr<Composition> const& right) : ParallelComposition(left, right) {
+            // Intentionally left empty.
+        }
+     
+        boost::any InterleavingParallelComposition::accept(CompositionVisitor& visitor) const {
+            return visitor.visit(*this);
+        }
+        
+        void InterleavingParallelComposition::writeToStream(std::ostream& stream) const {
+            stream << "(" << *left << " ||| " << *right << ")";
+        }
+        
+    }
+}

src/storage/prism/InterleavingParallelComposition.h

@@ -0,0 +1,24 @@
+#ifndef STORM_STORAGE_PRISM_INTERLEAVINGPARALLELCOMPOSITION_H_
+#define STORM_STORAGE_PRISM_INTERLEAVINGPARALLELCOMPOSITION_H_
+
+#include "src/storage/prism/ParallelComposition.h"
+
+namespace storm {
+    namespace prism {
+        class InterleavingParallelComposition : public ParallelComposition {
+        public:
+            InterleavingParallelComposition(std::shared_ptr<Composition> const& left, std::shared_ptr<Composition> const& right);
+            
+            virtual boost::any accept(CompositionVisitor& visitor) const override;
+
+        protected:
+            virtual void writeToStream(std::ostream& stream) const override;
+            
+        private:
+            std::shared_ptr<Composition> left;
+            std::shared_ptr<Composition> right;
+        };
+    }
+}
+
+#endif /* STORM_STORAGE_PRISM_INTERLEAVINGPARALLELCOMPOSITION_H_ */

src/storage/prism/ModuleComposition.cpp

@@ -7,6 +7,14 @@ namespace storm {
             // Intentionally left empty.
         }
         
+        boost::any ModuleComposition::accept(CompositionVisitor& visitor) const {
+            return visitor.visit(*this);
+        }
+        
+        std::string const& ModuleComposition::getModuleName() const {
+            return moduleName;
+        }
+        
         void ModuleComposition::writeToStream(std::ostream& stream) const {
             stream << moduleName;
         }

src/storage/prism/ModuleComposition.h

@@ -7,10 +7,14 @@
 
 namespace storm {
     namespace prism {
-        class ModuleComposition : Composition {
+        class ModuleComposition : public Composition {
         public:
             ModuleComposition(std::string const& moduleName);
             
+            virtual boost::any accept(CompositionVisitor& visitor) const override;
+            
+            std::string const& getModuleName() const;
+            
         protected:
             virtual void writeToStream(std::ostream& stream) const override;
             

src/storage/prism/ParallelComposition.cpp

@@ -5,13 +5,17 @@
 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) {
+        ParallelComposition::ParallelComposition(std::shared_ptr<Composition> const& left, std::shared_ptr<Composition> const& right) : left(left), right(right) {
             // Intentionally left empty.
         }
         
-        void ParallelComposition::writeToStream(std::ostream& stream) const {
-            stream << "(" << *left << " |[" << boost::algorithm::join(synchronizingActions, ", ") << "]| " << *right << ")";
+        Composition const& ParallelComposition::getLeftSubcomposition() const {
+            return *left;
         }
-
+        
+        Composition const& ParallelComposition::getRightSubcomposition() const {
+            return *right;
+        }
+        
     }
 }

src/storage/prism/ParallelComposition.h

@@ -1,6 +1,7 @@
 #ifndef STORM_STORAGE_PRISM_PARALLELCOMPOSITION_H_
 #define STORM_STORAGE_PRISM_PARALLELCOMPOSITION_H_
 
+#include <memory>
 #include <set>
 #include <string>
 
@@ -8,16 +9,15 @@
 
 namespace storm {
     namespace prism {
-        class ParallelComposition : Composition {
+        class ParallelComposition : public Composition {
         public:
-            ParallelComposition(std::shared_ptr<Composition> const& left, std::set<std::string> const& synchronizingActions, std::shared_ptr<Composition> const& right);
+            ParallelComposition(std::shared_ptr<Composition> const& left, std::shared_ptr<Composition> const& right);
             
-        protected:
-            virtual void writeToStream(std::ostream& stream) const override;
+            Composition const& getLeftSubcomposition() const;
+            Composition const& getRightSubcomposition() const;
             
         private:
             std::shared_ptr<Composition> left;
-            std::set<std::string> synchronizingActions;
             std::shared_ptr<Composition> right;
         };
     }

src/storage/prism/Program.cpp

@@ -15,15 +15,56 @@
 #include "src/exceptions/InvalidTypeException.h"
 #include "src/solver/SmtSolver.h"
 
+#include "src/storage/prism/CompositionVisitor.h"
+#include "src/storage/prism/Compositions.h"
+
 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, 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)
+        class CompositionValidityChecker : public CompositionVisitor {
+        public:
+            CompositionValidityChecker(storm::prism::Program const& program) : program(program) {
+                // Intentionally left empty.
+            }
+            
+            bool isValid(Composition const& composition) {
+                return boost::any_cast<bool>(composition.accept(*this));
+            }
+            
+            virtual boost::any visit(ModuleComposition const& composition) override {
+                return program.hasModule(composition.getModuleName());
+            }
+            
+            virtual boost::any visit(RenamingComposition const& composition) override {
+                return composition.getSubcomposition().accept(*this);
+            }
+            
+            virtual boost::any visit(HidingComposition const& composition) override {
+                return composition.getSubcomposition().accept(*this);
+            }
+            
+            virtual boost::any visit(SynchronizingParallelComposition const& composition) override {
+                return boost::any_cast<bool>(composition.getLeftSubcomposition().accept(*this)) && boost::any_cast<bool>(composition.getRightSubcomposition().accept(*this));
+            }
+            
+            virtual boost::any visit(InterleavingParallelComposition const& composition) override {
+                return boost::any_cast<bool>(composition.getLeftSubcomposition().accept(*this)) && boost::any_cast<bool>(composition.getRightSubcomposition().accept(*this));
+            }
+            
+            virtual boost::any visit(RestrictedParallelComposition const& composition) override {
+                return boost::any_cast<bool>(composition.getLeftSubcomposition().accept(*this)) && boost::any_cast<bool>(composition.getRightSubcomposition().accept(*this));
+            }
+            
+        private:
+            storm::prism::Program const& program;
+        };
+        
+        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<SystemCompositionConstruct> const& compositionConstruct, 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(), systemComposition(composition),
+            rewardModels(rewardModels), rewardModelToIndexMap(), systemCompositionConstruct(compositionConstruct),
             labels(labels), labelToIndexMap(), actionToIndexMap(actionToIndexMap), indexToActionMap(), actions(),
             synchronizingActionIndices(), actionIndicesToModuleIndexMap(), variableToModuleIndexMap()
         {
@@ -277,6 +318,10 @@ namespace storm {
             return this->modules[index];
         }
         
+        bool Program::hasModule(std::string const& moduleName) const {
+            return this->moduleToIndexMap.find(moduleName) != this->moduleToIndexMap.end();
+        }
+        
         Module const& Program::getModule(std::string const& moduleName) const {
             auto const& nameIndexPair = this->moduleToIndexMap.find(moduleName);
             STORM_LOG_THROW(nameIndexPair != this->moduleToIndexMap.end(), storm::exceptions::OutOfRangeException, "Unknown module '" << moduleName << "'.");
@@ -296,15 +341,15 @@ namespace storm {
         }
         
         bool Program::specifiesSystemComposition() const {
-            return static_cast<bool>(systemComposition);
+            return static_cast<bool>(systemCompositionConstruct);
         }
         
-        Composition const& Program::getSystemComposition() const {
-            return *systemComposition.get();
+        SystemCompositionConstruct const& Program::getSystemCompositionConstruct() const {
+            return systemCompositionConstruct.get();
         }
         
-        boost::optional<std::shared_ptr<Composition>> Program::getOptionalSystemComposition() const {
-            return systemComposition;
+        boost::optional<SystemCompositionConstruct> Program::getOptionalSystemCompositionConstruct() const {
+            return systemCompositionConstruct;
         }
         
         std::set<std::string> const& Program::getActions() const {
@@ -430,7 +475,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(), this->getLabels(), this->getInitialConstruct(), this->getOptionalSystemComposition());
+            return Program(this->manager, this->getModelType(), this->getConstants(), this->getGlobalBooleanVariables(), this->getGlobalIntegerVariables(), this->getFormulas(), newModules, this->getActionNameToIndexMapping(), this->getRewardModels(), this->getLabels(), this->getInitialConstruct(), this->getOptionalSystemCompositionConstruct());
         }
         
         void Program::createMappings() {
@@ -530,7 +575,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(), this->getLabels(), this->getInitialConstruct(), this->getOptionalSystemComposition());
+            return Program(this->manager, this->getModelType(), newConstants, this->getGlobalBooleanVariables(), this->getGlobalIntegerVariables(), this->getFormulas(), this->getModules(), this->getActionNameToIndexMapping(), this->getRewardModels(), this->getLabels(), this->getInitialConstruct(), this->getOptionalSystemCompositionConstruct());
         }
         
         Program Program::substituteConstants() const {
@@ -590,7 +635,7 @@ namespace storm {
                 newLabels.emplace_back(label.substitute(constantSubstitution));
             }
             
-            return Program(this->manager, this->getModelType(), newConstants, newBooleanVariables, newIntegerVariables, newFormulas, newModules, this->getActionNameToIndexMapping(), newRewardModels, newLabels, newInitialConstruct, this->getOptionalSystemComposition());
+            return Program(this->manager, this->getModelType(), newConstants, newBooleanVariables, newIntegerVariables, newFormulas, newModules, this->getActionNameToIndexMapping(), newRewardModels, newLabels, newInitialConstruct, this->getOptionalSystemCompositionConstruct());
         }
         
         void Program::checkValidity(Program::ValidityCheckLevel lvl) const {
@@ -914,6 +959,13 @@ namespace storm {
             bool isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedIdentifiers.begin(), containedIdentifiers.end());
             STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << this->getInitialConstruct().getFilename() << ", line " << this->getInitialConstruct().getLineNumber() << ": initial expression refers to unknown identifiers.");
             
+            // Check the system composition if given.
+            if (systemCompositionConstruct) {
+                CompositionValidityChecker checker(*this);
+                isValid = checker.isValid(systemCompositionConstruct.get().getSystemComposition());
+                STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in system composition expression.");
+            }
+            
             // Check the labels.
             for (auto const& label : this->getLabels()) {
                 std::set<storm::expressions::Variable> containedVariables = label.getStatePredicateExpression().getVariables();
@@ -1031,7 +1083,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(), getLabels(), getInitialConstruct(), this->getOptionalSystemComposition());
+            return Program(this->manager, modelType, newConstants, getGlobalBooleanVariables(), getGlobalIntegerVariables(), getFormulas(), newModules, getActionNameToIndexMapping(), getRewardModels(), getLabels(), getInitialConstruct(), this->getOptionalSystemCompositionConstruct());
         }
         
         Program Program::flattenModules(std::unique_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory) const {
@@ -1217,7 +1269,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(), this->getLabels(), this->getInitialConstruct(), this->getOptionalSystemComposition(), 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->getOptionalSystemCompositionConstruct(), this->getFilename(), 0, true);
         }
 
         std::unordered_map<uint_fast64_t, std::string> Program::buildCommandIndexToActionNameMap() const {
@@ -1370,9 +1422,7 @@ namespace storm {
             stream << program.getInitialConstruct() << std::endl;
             
             if (program.specifiesSystemComposition()) {
-                stream << "system" << std::endl;
-                stream << "\t" << program.getSystemComposition() << std::endl;
-                stream << "endsystem" << std::endl;
+                stream << program.getSystemCompositionConstruct();
             }
             
             return stream;

src/storage/prism/Program.h

@@ -13,6 +13,7 @@
 #include "src/storage/prism/Label.h"
 #include "src/storage/prism/Module.h"
 #include "src/storage/prism/RewardModel.h"
+#include "src/storage/prism/SystemCompositionConstruct.h"
 #include "src/storage/prism/InitialConstruct.h"
 #include "src/storage/prism/Composition.h"
 #include "src/utility/solver.h"
@@ -45,13 +46,13 @@ namespace storm {
              * @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 compositionConstruct 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, 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);
+            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<SystemCompositionConstruct> const& compositionConstruct, std::string const& filename = "", uint_fast64_t lineNumber = 0, bool finalModel = true);
             
             // Provide default implementations for constructors and assignments.
             Program() = default;
@@ -237,6 +238,13 @@ namespace storm {
              */
             Module const& getModule(uint_fast64_t index) const;
 
+            /*!
+             * Retrieves whether the program has a module with the given name.
+             *
+             * @return True iff a module with the given name exists.
+             */
+            bool hasModule(std::string const& moduleName) const;
+            
             /*!
              * Retrieves the module with the given name.
              *
@@ -275,18 +283,18 @@ namespace storm {
             bool specifiesSystemComposition() const;
             
             /*!
-             * If the program specifies a system composition, this method retrieves it.
+             * If the program specifies a system composition construct, this method retrieves it.
              *
-             * @return The system composition as specified by the program.
+             * @return The system composition construct as specified by the program.
              */
-            Composition const& getSystemComposition() const;
+            SystemCompositionConstruct const& getSystemCompositionConstruct() const;
             
             /*!
-             * Retrieves the system composition (if any) and none otherwise.
+             * Retrieves the system composition construct (if any) and none otherwise.
              *
-             * @return The system composition specified by the program or none.
+             * @return The system composition construct specified by the program or none.
              */
-            boost::optional<std::shared_ptr<Composition>> getOptionalSystemComposition() const;
+            boost::optional<SystemCompositionConstruct> getOptionalSystemCompositionConstruct() const;
             
             /*!
              * Retrieves the set of actions present in the program.
@@ -576,7 +584,7 @@ namespace storm {
             InitialConstruct initialConstruct;
             
             // If set, this specifies the way the modules are composed to obtain the full system.
-            boost::optional<std::shared_ptr<Composition>> systemComposition;
+            boost::optional<SystemCompositionConstruct> systemCompositionConstruct;
             
             // The labels that are defined for this model.
             std::vector<Label> labels;

src/storage/prism/RenamingComposition.cpp

@@ -7,21 +7,26 @@
 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) {
+        RenamingComposition::RenamingComposition(std::shared_ptr<Composition> const& sub, std::map<std::string, std::string> const& actionRenaming) : sub(sub), actionRenaming(actionRenaming) {
             // Intentionally left empty.
         }
         
+        boost::any RenamingComposition::accept(CompositionVisitor& visitor) const {
+            return visitor.visit(*this);
+        }
+        
+        Composition const& RenamingComposition::getSubcomposition() const {
+            return *sub;
+        }
+        
         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;
+                s << renaming.second << " <- " << renaming.first;
                 renamings.push_back(s.str());
             }
-            stream << *left << "{" << boost::join(renamings, ", ") << "}";
+            stream << *sub << "{" << boost::join(renamings, ", ") << "}";
         }
         
     }

src/storage/prism/RenamingComposition.h

@@ -9,18 +9,22 @@
 
 namespace storm {
     namespace prism {
-        class RenamingComposition : Composition {
+        class RenamingComposition : public Composition {
         public:
-            RenamingComposition(std::shared_ptr<Composition> const& left, std::map<std::string, boost::optional<std::string>> const& actionRenaming);
+            RenamingComposition(std::shared_ptr<Composition> const& sub, std::map<std::string, std::string> const& actionRenaming);
+            
+            virtual boost::any accept(CompositionVisitor& visitor) const override;
+            
+            Composition const& getSubcomposition() const;
             
         protected:
             virtual void writeToStream(std::ostream& stream) const override;
             
         private:
-            std::shared_ptr<Composition> left;
+            std::shared_ptr<Composition> sub;
             
             // 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;
+            std::map<std::string, std::string> actionRenaming;
         };
     }
 }

src/storage/prism/RestrictedParallelComposition.cpp

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

src/storage/prism/RestrictedParallelComposition.h

@@ -0,0 +1,28 @@
+#ifndef STORM_STORAGE_PRISM_RESTRICTEDPARALLELCOMPOSITION_H_
+#define STORM_STORAGE_PRISM_RESTRICTEDPARALLELCOMPOSITION_H_
+
+#include <set>
+#include <string>
+
+#include "src/storage/prism/ParallelComposition.h"
+
+namespace storm {
+    namespace prism {
+        class RestrictedParallelComposition : public ParallelComposition {
+        public:
+            RestrictedParallelComposition(std::shared_ptr<Composition> const& left, std::set<std::string> const& synchronizingActions, std::shared_ptr<Composition> const& right);
+            
+            virtual boost::any accept(CompositionVisitor& visitor) const override;
+
+        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_RESTRICTEDPARALLELCOMPOSITION_H_ */

src/storage/prism/SynchronizingParallelComposition.cpp

@@ -0,0 +1,19 @@
+#include "src/storage/prism/SynchronizingParallelComposition.h"
+
+namespace storm {
+    namespace prism {
+        
+        SynchronizingParallelComposition::SynchronizingParallelComposition(std::shared_ptr<Composition> const& left, std::shared_ptr<Composition> const& right) : ParallelComposition(left, right) {
+            // Intentionally left empty.
+        }
+        
+        boost::any SynchronizingParallelComposition::accept(CompositionVisitor& visitor) const {
+            return visitor.visit(*this);
+        }
+        
+        void SynchronizingParallelComposition::writeToStream(std::ostream& stream) const {
+            stream << "(" << *left << " || " << *right << ")";
+        }
+        
+    }
+}

src/storage/prism/SynchronizingParallelComposition.h

@@ -0,0 +1,24 @@
+#ifndef STORM_STORAGE_PRISM_SYNCHRONIZINGPARALLELCOMPOSITION_H_
+#define STORM_STORAGE_PRISM_SYNCHRONIZINGPARALLELCOMPOSITION_H_
+
+#include "src/storage/prism/ParallelComposition.h"
+
+namespace storm {
+    namespace prism {
+        class SynchronizingParallelComposition : public ParallelComposition {
+        public:
+            SynchronizingParallelComposition(std::shared_ptr<Composition> const& left, std::shared_ptr<Composition> const& right);
+            
+            virtual boost::any accept(CompositionVisitor& visitor) const override;
+            
+        protected:
+            virtual void writeToStream(std::ostream& stream) const override;
+            
+        private:
+            std::shared_ptr<Composition> left;
+            std::shared_ptr<Composition> right;
+        };
+    }
+}
+
+#endif /* STORM_STORAGE_PRISM_SYNCHRONIZINGPARALLELCOMPOSITION_H_ */

src/storage/prism/SystemCompositionConstruct.cpp

@@ -0,0 +1,22 @@
+#include "src/storage/prism/SystemCompositionConstruct.h"
+
+namespace storm {
+    namespace prism {
+        
+        SystemCompositionConstruct::SystemCompositionConstruct(std::shared_ptr<Composition> const& composition, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), composition(composition) {
+            // Intentionlly left empty.
+        }
+        
+        Composition const& SystemCompositionConstruct::getSystemComposition() const {
+            return *composition;
+        }
+        
+        std::ostream& operator<<(std::ostream& stream, SystemCompositionConstruct const& systemCompositionConstruct) {
+            stream << "system" << std::endl;
+            stream << "\t" << systemCompositionConstruct.getSystemComposition() << std::endl;
+            stream << "endsystem" << std::endl;
+            return stream;
+        }
+        
+    }
+}

src/storage/prism/SystemCompositionConstruct.h

@@ -0,0 +1,44 @@
+#ifndef STORM_STORAGE_PRISM_SYSTEMCOMPOSITIONCONSTRUCT_H_
+#define STORM_STORAGE_PRISM_SYSTEMCOMPOSITIONCONSTRUCT_H_
+
+#include <string>
+#include <memory>
+
+#include "src/storage/prism/LocatedInformation.h"
+#include "src/utility/OsDetection.h"
+
+#include "src/storage/prism/Composition.h"
+
+namespace storm {
+    namespace prism {
+        class SystemCompositionConstruct : public LocatedInformation {
+        public:
+            /*!
+             * Creates an system composition construct with the given composition.
+             *
+             * @param composition A composition expression defining the system composition.
+             * @param filename The filename in which the command is defined.
+             * @param lineNumber The line number in which the command is defined.
+             */
+            SystemCompositionConstruct(std::shared_ptr<Composition> const& composition, std::string const& filename = "", uint_fast64_t lineNumber = 0);
+            
+            // Create default implementations of constructors/assignment.
+            SystemCompositionConstruct() = default;
+            SystemCompositionConstruct(SystemCompositionConstruct const& other) = default;
+            SystemCompositionConstruct& operator=(SystemCompositionConstruct const& other)= default;
+#ifndef WINDOWS
+            SystemCompositionConstruct(SystemCompositionConstruct&& other) = default;
+            SystemCompositionConstruct& operator=(SystemCompositionConstruct&& other) = default;
+#endif
+            
+            Composition const& getSystemComposition() const;
+            
+            friend std::ostream& operator<<(std::ostream& stream, SystemCompositionConstruct const& systemCompositionConstruct);
+
+        private:
+            std::shared_ptr<Composition> composition;
+        };
+    }
+}
+
+#endif /* STORM_STORAGE_PRISM_SYSTEMCOMPOSITIONCONSTRUCT_H_ */

test/functional/builder/ExplicitPrismModelBuilderTest.cpp

@@ -97,4 +97,10 @@ TEST(ExplicitPrismModelBuilderTest, Mdp) {
     model = storm::builder::ExplicitPrismModelBuilder<double>(program).translate();
     EXPECT_EQ(37ul, model->getNumberOfStates());
     EXPECT_EQ(59ul, model->getNumberOfTransitions());
+}
+
+TEST(ExplicitPrismModelBuilderTest, Fail) {
+    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/system_composition.nm");
+
+    ASSERT_THROW(storm::builder::ExplicitPrismModelBuilder<double>(program).translate(), storm::exceptions::WrongFormatException);
 }

test/functional/builder/system_composition.nm

@@ -0,0 +1,27 @@
+mdp
+
+module one
+	x : [0 .. 2] init 0;
+
+	[a] x = 0 -> (x'=1);
+	[] x = 1 -> true;
+endmodule
+
+module two
+	y : [0 .. 2] init 0;
+
+	[b] y=0 -> (y'=1);
+	[] y=1 -> true;
+endmodule
+
+module three
+	z : [0 .. 2] init 0;
+
+	[c] z=0 -> (z'=1);
+	[] z=1 -> true;
+endmodule
+
+system
+	((one || two) {a <- b} |[a]| (three {a <- c})) / {a, b, c}
+endsystem
+