From 55f4efd40a72286df05209c9f04d09114dac0f28 Mon Sep 17 00:00:00 2001 From: Stefan Pranger Date: Tue, 11 Aug 2020 16:33:38 +0200 Subject: [PATCH] added SMG ModelType --- src/storm-parsers/parser/PrismParser.h | 14 +++++++------ src/storm/generator/NextStateGenerator.h | 21 ++++++++++--------- .../generator/PrismNextStateGenerator.cpp | 5 +++-- .../storage/SymbolicModelDescription.cpp | 3 ++- src/storm/storage/SymbolicModelDescription.h | 18 ++++++++-------- src/storm/storage/prism/Program.cpp | 2 +- src/storm/storage/prism/Program.h | 3 ++- 7 files changed, 36 insertions(+), 30 deletions(-) diff --git a/src/storm-parsers/parser/PrismParser.h b/src/storm-parsers/parser/PrismParser.h index b816b9c1f..f3058e9d0 100644 --- a/src/storm-parsers/parser/PrismParser.h +++ b/src/storm-parsers/parser/PrismParser.h @@ -101,10 +101,11 @@ namespace storm { ("ctmdp", storm::prism::Program::ModelType::CTMDP) ("ma", storm::prism::Program::ModelType::MA) ("pomdp", storm::prism::Program::ModelType::POMDP) - ("pta", storm::prism::Program::ModelType::PTA); + ("pta", storm::prism::Program::ModelType::PTA) + ("smg", storm::prism::Program::ModelType::SMG); } }; - + struct keywordsStruct : qi::symbols { keywordsStruct() { add @@ -131,19 +132,20 @@ namespace storm { ("init", 21) ("endinit", 22) ("invariant", 23) - ("endinvariant", 24); + ("endinvariant", 24) + ("smg", 25); } }; - + // Functor used for annotating entities with line number information. class PositionAnnotation { public: typedef void result_type; - + PositionAnnotation(Iterator first) : first(first) { // Intentionally left empty. } - + template result_type operator()(Entity& entity, First f, Last) const { entity.setLineNumber(get_line(f)); diff --git a/src/storm/generator/NextStateGenerator.h b/src/storm/generator/NextStateGenerator.h index d4633ede4..605618142 100644 --- a/src/storm/generator/NextStateGenerator.h +++ b/src/storm/generator/NextStateGenerator.h @@ -24,44 +24,45 @@ namespace storm { namespace generator { typedef storm::builder::BuilderOptions NextStateGeneratorOptions; - + enum class ModelType { DTMC, CTMC, MDP, MA, - POMDP + POMDP, + SMG }; - + template class NextStateGenerator { public: typedef std::function StateToIdCallback; NextStateGenerator(storm::expressions::ExpressionManager const& expressionManager, VariableInformation const& variableInformation, NextStateGeneratorOptions const& options); - + /*! * Creates a new next state generator. This version of the constructor default-constructs the variable information. * Hence, the subclass is responsible for suitably initializing it in its constructor. */ NextStateGenerator(storm::expressions::ExpressionManager const& expressionManager, NextStateGeneratorOptions const& options); - + virtual ~NextStateGenerator() = default; - + uint64_t getStateSize() const; virtual ModelType getModelType() const = 0; virtual bool isDeterministicModel() const = 0; virtual bool isDiscreteTimeModel() const = 0; virtual bool isPartiallyObservable() const = 0; virtual std::vector getInitialStates(StateToIdCallback const& stateToIdCallback) = 0; - + /// Initializes a builder for state valuations by adding the appropriate variables. virtual storm::storage::sparse::StateValuationsBuilder initializeStateValuationsBuilder() const; - + void load(CompressedState const& state); virtual StateBehavior expand(StateToIdCallback const& stateToIdCallback) = 0; bool satisfies(storm::expressions::Expression const& expression) const; - + /// Adds the valuation for the currently loaded state to the given builder virtual void addStateValuation(storm::storage::sparse::state_type const& currentStateIndex, storm::storage::sparse::StateValuationsBuilder& valuationsBuilder) const; /// Adds the valuation for the currently loaded state @@ -69,7 +70,7 @@ namespace storm { virtual std::size_t getNumberOfRewardModels() const = 0; virtual storm::builder::RewardModelInformation getRewardModelInformation(uint64_t const& index) const = 0; - + std::string stateToString(CompressedState const& state) const; uint32_t observabilityClass(CompressedState const& state) const; diff --git a/src/storm/generator/PrismNextStateGenerator.cpp b/src/storm/generator/PrismNextStateGenerator.cpp index 823b0305c..814ed9340 100644 --- a/src/storm/generator/PrismNextStateGenerator.cpp +++ b/src/storm/generator/PrismNextStateGenerator.cpp @@ -127,16 +127,17 @@ namespace storm { case storm::prism::Program::ModelType::MDP: return ModelType::MDP; case storm::prism::Program::ModelType::MA: return ModelType::MA; case storm::prism::Program::ModelType::POMDP: return ModelType::POMDP; + case storm::prism::Program::ModelType::SMG: return ModelType::SMG; default: STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Invalid model type."); } } - + template bool PrismNextStateGenerator::isDeterministicModel() const { return program.isDeterministicModel(); } - + template bool PrismNextStateGenerator::isDiscreteTimeModel() const { return program.isDiscreteTimeModel(); diff --git a/src/storm/storage/SymbolicModelDescription.cpp b/src/storm/storage/SymbolicModelDescription.cpp index af6dd5631..abf9aa340 100644 --- a/src/storm/storage/SymbolicModelDescription.cpp +++ b/src/storm/storage/SymbolicModelDescription.cpp @@ -65,12 +65,13 @@ namespace storm { case storm::prism::Program::ModelType::MDP: return SymbolicModelDescription::ModelType::MDP; case storm::prism::Program::ModelType::POMDP: return SymbolicModelDescription::ModelType::POMDP; case storm::prism::Program::ModelType::MA: return SymbolicModelDescription::ModelType::MA; + case storm::prism::Program::ModelType::SMG: return SymbolicModelDescription::ModelType::SMG; default: STORM_LOG_THROW(false, storm::exceptions::InvalidTypeException, "Expected other PRISM model type."); } } } - + storm::expressions::ExpressionManager& SymbolicModelDescription::getManager() const { if (this->isPrismProgram()) { return this->asPrismProgram().getManager(); diff --git a/src/storm/storage/SymbolicModelDescription.h b/src/storm/storage/SymbolicModelDescription.h index 0d72bf5e3..495091755 100644 --- a/src/storm/storage/SymbolicModelDescription.h +++ b/src/storm/storage/SymbolicModelDescription.h @@ -7,39 +7,39 @@ namespace storm { namespace storage { - + class SymbolicModelDescription { public: enum class ModelType { - DTMC, CTMC, MDP, MA, POMDP + DTMC, CTMC, MDP, MA, POMDP, SMG }; - + SymbolicModelDescription() = default; SymbolicModelDescription(storm::jani::Model const& model); SymbolicModelDescription(storm::prism::Program const& program); SymbolicModelDescription& operator=(storm::jani::Model const& model); SymbolicModelDescription& operator=(storm::prism::Program const& program); - + bool hasModel() const; bool isJaniModel() const; bool isPrismProgram() const; - + ModelType getModelType() const; storm::expressions::ExpressionManager& getManager() const; void setModel(storm::jani::Model const& model); void setModel(storm::prism::Program const& program); - + storm::jani::Model const& asJaniModel() const; storm::jani::Model& asJaniModel(); storm::prism::Program const& asPrismProgram() const; storm::prism::Program& asPrismProgram(); - + std::vector getParameterNames() const; - + SymbolicModelDescription toJani(bool makeVariablesGlobal = true) const; - + /*! * Ensures that this model is a JANI model by, e.g., converting prism to jani. * If labels or reward models had to be converted during conversion, the renamings are applied to the given properties diff --git a/src/storm/storage/prism/Program.cpp b/src/storm/storage/prism/Program.cpp index 01127d555..ff906190e 100644 --- a/src/storm/storage/prism/Program.cpp +++ b/src/storm/storage/prism/Program.cpp @@ -187,7 +187,7 @@ namespace storm { } bool Program::isDiscreteTimeModel() const { - return modelType == ModelType::DTMC || modelType == ModelType::MDP || modelType == ModelType::POMDP; + return modelType == ModelType::DTMC || modelType == ModelType::MDP || modelType == ModelType::POMDP || modelType == ModelType::SMG; } bool Program::isDeterministicModel() const { diff --git a/src/storm/storage/prism/Program.h b/src/storm/storage/prism/Program.h index 94b11ad46..cc2b5ed07 100644 --- a/src/storm/storage/prism/Program.h +++ b/src/storm/storage/prism/Program.h @@ -15,6 +15,7 @@ #include "storm/storage/prism/SystemCompositionConstruct.h" #include "storm/storage/prism/InitialConstruct.h" #include "storm/storage/prism/Composition.h" +#include "storm/storage/prism/Player.h" #include "storm/storage/BoostTypes.h" #include "storm/utility/solver.h" #include "storm/utility/OsDetection.h" @@ -31,7 +32,7 @@ namespace storm { /*! * An enum for the different model types. */ - enum class ModelType {UNDEFINED, DTMC, CTMC, MDP, CTMDP, MA, POMDP, PTA}; + enum class ModelType {UNDEFINED, DTMC, CTMC, MDP, CTMDP, MA, POMDP, PTA, SMG}; enum class ValidityCheckLevel : unsigned {VALIDINPUT = 0, READYFORPROCESSING = 1};