diff --git a/src/generator/PrismNextStateGenerator.cpp b/src/generator/PrismNextStateGenerator.cpp index 9ccec9605..d82db2e6b 100644 --- a/src/generator/PrismNextStateGenerator.cpp +++ b/src/generator/PrismNextStateGenerator.cpp @@ -11,7 +11,7 @@ namespace storm { template PrismNextStateGenerator::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 diff --git a/src/parser/PrismParser.cpp b/src/parser/PrismParser.cpp index 9944d8abd..1a55f0339 100644 --- a/src/parser/PrismParser.cpp +++ b/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>(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 const& composition, GlobalProgramInformation& globalProgramInformation) { + globalProgramInformation.systemCompositionConstruct = storm::prism::SystemCompositionConstruct(composition, this->getFilename(), get_line(qi::_3)); + return true; + } + + std::shared_ptr PrismParser::createModuleComposition(std::string const& moduleName) const { + return std::make_shared(moduleName); + } + + std::shared_ptr PrismParser::createRenamingComposition(std::shared_ptr const& subcomposition, std::map const& renaming) const { + return std::make_shared(subcomposition, renaming); + } + + std::shared_ptr PrismParser::createHidingComposition(std::shared_ptr const& subcomposition, std::set const& actionsToHide) const { + return std::make_shared(subcomposition, actionsToHide); + } + + std::shared_ptr PrismParser::createSynchronizingParallelComposition(std::shared_ptr const& left, std::shared_ptr const& right) const { + return std::make_shared(left, right); + } + + std::shared_ptr PrismParser::createInterleavingParallelComposition(std::shared_ptr const& left, std::shared_ptr const& right) const { + return std::make_shared(left, right); + } + + std::shared_ptr PrismParser::createRestrictedParallelComposition(std::shared_ptr const& left, std::set const& synchronizingActions, std::shared_ptr const& right) const { + return std::make_shared(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(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(manager->boolean(false))), globalProgramInformation.systemCompositionConstruct, this->getFilename(), 1, this->secondRun); } } // namespace parser } // namespace storm diff --git a/src/parser/PrismParser.h b/src/parser/PrismParser.h index 44da8fc5a..84a5b601e 100644 --- a/src/parser/PrismParser.h +++ b/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 labels; bool hasInitialConstruct; storm::prism::InitialConstruct initialConstruct; + boost::optional 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 initialStatesConstruct; + // Rules for the system composition. + qi::rule systemCompositionConstruct; + qi::rule(), Skipper> parallelComposition; + qi::rule synchronizingParallelComposition; + qi::rule interleavingParallelComposition; + qi::rule(), Skipper> restrictedParallelComposition; + qi::rule(), Skipper> hidingOrRenamingComposition; + qi::rule(), Skipper> hidingComposition; + qi::rule(), Skipper> renamingComposition; + qi::rule(), Skipper> atomicComposition; + qi::rule(), Skipper> moduleComposition; + qi::rule(), Skipper> actionNameList; + qi::rule(), Skipper> actionRenamingList; + // Rules for label definitions. qi::rule 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 const& composition, GlobalProgramInformation& globalProgramInformation); + + std::shared_ptr createModuleComposition(std::string const& moduleName) const; + std::shared_ptr createRenamingComposition(std::shared_ptr const& subcomposition, std::map const& renaming) const; + std::shared_ptr createHidingComposition(std::shared_ptr const& subcomposition, std::set const& actionsToHide) const; + std::shared_ptr createSynchronizingParallelComposition(std::shared_ptr const& left, std::shared_ptr const& right) const; + std::shared_ptr createInterleavingParallelComposition(std::shared_ptr const& left, std::shared_ptr const& right) const; + std::shared_ptr createRestrictedParallelComposition(std::shared_ptr const& left, std::set const& synchronizingActions, std::shared_ptr 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; diff --git a/src/storage/prism/Composition.h b/src/storage/prism/Composition.h index 6fd3a6a63..97352162d 100644 --- a/src/storage/prism/Composition.h +++ b/src/storage/prism/Composition.h @@ -3,6 +3,8 @@ #include +#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; diff --git a/src/storage/prism/CompositionVisitor.h b/src/storage/prism/CompositionVisitor.h index 5d782d026..2cb705654 100644 --- a/src/storage/prism/CompositionVisitor.h +++ b/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; }; } } diff --git a/src/storage/prism/Compositions.h b/src/storage/prism/Compositions.h new file mode 100644 index 000000000..968142479 --- /dev/null +++ b/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" \ No newline at end of file diff --git a/src/storage/prism/HidingComposition.cpp b/src/storage/prism/HidingComposition.cpp new file mode 100644 index 000000000..baaa2572f --- /dev/null +++ b/src/storage/prism/HidingComposition.cpp @@ -0,0 +1,25 @@ +#include "src/storage/prism/HidingComposition.h" + +#include + +namespace storm { + namespace prism { + + HidingComposition::HidingComposition(std::shared_ptr const& sub, std::set 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, ", ") << "}"; + } + + } +} \ No newline at end of file diff --git a/src/storage/prism/HidingComposition.h b/src/storage/prism/HidingComposition.h new file mode 100644 index 000000000..048847fa5 --- /dev/null +++ b/src/storage/prism/HidingComposition.h @@ -0,0 +1,31 @@ +#ifndef STORM_STORAGE_PRISM_HIDINGCOMPOSITION_H_ +#define STORM_STORAGE_PRISM_HIDINGCOMPOSITION_H_ + +#include +#include + +#include "src/storage/prism/Composition.h" + +namespace storm { + namespace prism { + class HidingComposition : public Composition { + public: + HidingComposition(std::shared_ptr const& sub, std::set 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 sub; + + // The actions to hide. + std::set actionsToHide; + }; + } +} + +#endif /* STORM_STORAGE_PRISM_HIDINGCOMPOSITION_H_ */ diff --git a/src/storage/prism/InitialConstruct.h b/src/storage/prism/InitialConstruct.h index 5200fe805..8bd911386 100644 --- a/src/storage/prism/InitialConstruct.h +++ b/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. * diff --git a/src/storage/prism/InterleavingParallelComposition.cpp b/src/storage/prism/InterleavingParallelComposition.cpp new file mode 100644 index 000000000..311b7eede --- /dev/null +++ b/src/storage/prism/InterleavingParallelComposition.cpp @@ -0,0 +1,19 @@ +#include "src/storage/prism/InterleavingParallelComposition.h" + +namespace storm { + namespace prism { + + InterleavingParallelComposition::InterleavingParallelComposition(std::shared_ptr const& left, std::shared_ptr 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 << ")"; + } + + } +} \ No newline at end of file diff --git a/src/storage/prism/InterleavingParallelComposition.h b/src/storage/prism/InterleavingParallelComposition.h new file mode 100644 index 000000000..883323bbf --- /dev/null +++ b/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 const& left, std::shared_ptr const& right); + + virtual boost::any accept(CompositionVisitor& visitor) const override; + + protected: + virtual void writeToStream(std::ostream& stream) const override; + + private: + std::shared_ptr left; + std::shared_ptr right; + }; + } +} + +#endif /* STORM_STORAGE_PRISM_INTERLEAVINGPARALLELCOMPOSITION_H_ */ diff --git a/src/storage/prism/ModuleComposition.cpp b/src/storage/prism/ModuleComposition.cpp index 9b72e80f3..3dd32d37d 100644 --- a/src/storage/prism/ModuleComposition.cpp +++ b/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; } diff --git a/src/storage/prism/ModuleComposition.h b/src/storage/prism/ModuleComposition.h index 9056f5617..6208fa27a 100644 --- a/src/storage/prism/ModuleComposition.h +++ b/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; diff --git a/src/storage/prism/ParallelComposition.cpp b/src/storage/prism/ParallelComposition.cpp index 633f2c42e..b74b12d53 100644 --- a/src/storage/prism/ParallelComposition.cpp +++ b/src/storage/prism/ParallelComposition.cpp @@ -5,13 +5,17 @@ namespace storm { namespace prism { - ParallelComposition::ParallelComposition(std::shared_ptr const& left, std::set const& synchronizingActions, std::shared_ptr const& right) : left(left), synchronizingActions(synchronizingActions), right(right) { + ParallelComposition::ParallelComposition(std::shared_ptr const& left, std::shared_ptr 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; + } + } } \ No newline at end of file diff --git a/src/storage/prism/ParallelComposition.h b/src/storage/prism/ParallelComposition.h index cc7b49fb9..5426ef97e 100644 --- a/src/storage/prism/ParallelComposition.h +++ b/src/storage/prism/ParallelComposition.h @@ -1,6 +1,7 @@ #ifndef STORM_STORAGE_PRISM_PARALLELCOMPOSITION_H_ #define STORM_STORAGE_PRISM_PARALLELCOMPOSITION_H_ +#include #include #include @@ -8,16 +9,15 @@ namespace storm { namespace prism { - class ParallelComposition : Composition { + class ParallelComposition : public Composition { public: - ParallelComposition(std::shared_ptr const& left, std::set const& synchronizingActions, std::shared_ptr const& right); + ParallelComposition(std::shared_ptr const& left, std::shared_ptr const& right); - protected: - virtual void writeToStream(std::ostream& stream) const override; + Composition const& getLeftSubcomposition() const; + Composition const& getRightSubcomposition() const; private: std::shared_ptr left; - std::set synchronizingActions; std::shared_ptr right; }; } diff --git a/src/storage/prism/Program.cpp b/src/storage/prism/Program.cpp index b78b6e97a..e1b6d3a5c 100644 --- a/src/storage/prism/Program.cpp +++ b/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 manager, ModelType modelType, std::vector const& constants, std::vector const& globalBooleanVariables, std::vector const& globalIntegerVariables, std::vector const& formulas, std::vector const& modules, std::map const& actionToIndexMap, std::vector const& rewardModels, std::vector