parsing prism PTAs

src/storm-parsers/parser/PrismParser.cpp

@@ -86,8 +86,6 @@ namespace storm {
             modelTypeDefinition %= modelType_;
             modelTypeDefinition.name("model type");
             
-
-            
             undefinedBooleanConstantDefinition = ((qi::lit("const") >> qi::lit("bool")) > identifier > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createUndefinedBooleanConstant, phoenix::ref(*this), qi::_1)];
             undefinedBooleanConstantDefinition.name("undefined boolean constant declaration");
             
@@ -121,7 +119,10 @@ namespace storm {
             integerVariableDefinition = ((identifier >> qi::lit(":") >> qi::lit("[")) > expression_ > qi::lit("..") > expression_ > qi::lit("]") > -(qi::lit("init") > expression_[qi::_a = qi::_1]) > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createIntegerVariable, phoenix::ref(*this), qi::_1, qi::_2, qi::_3, qi::_a)];
             integerVariableDefinition.name("integer variable definition");
             
-            variableDefinition = (booleanVariableDefinition[phoenix::push_back(qi::_r1, qi::_1)] | integerVariableDefinition[phoenix::push_back(qi::_r2, qi::_1)]);
+            clockVariableDefinition = ((identifier >> qi::lit(":") >> qi::lit("clock")) > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createClockVariable, phoenix::ref(*this), qi::_1)];
+            clockVariableDefinition.name("clock variable definition");
+            
+            variableDefinition = (booleanVariableDefinition[phoenix::push_back(qi::_r1, qi::_1)] | integerVariableDefinition[phoenix::push_back(qi::_r2, qi::_1)] | clockVariableDefinition[phoenix::push_back(qi::_r3, qi::_1)]);
             variableDefinition.name("variable declaration");
             
             globalVariableDefinition = (qi::lit("global") > (booleanVariableDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::globalBooleanVariables, qi::_r1), qi::_1)] | integerVariableDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::globalIntegerVariables, qi::_r1), qi::_1)]));
@@ -150,6 +151,9 @@ namespace storm {
             observablesConstruct = (qi::lit("observables") > (identifier % qi::lit(",") )> qi::lit("endobservables"))[phoenix::bind(&PrismParser::createObservablesList, phoenix::ref(*this), qi::_1)];
             observablesConstruct.name("observables construct");
             
+            invariantConstruct = (qi::lit("invariant") > expression_ > qi::lit("endinvariant"))[qi::_val = qi::_1];
+            invariantConstruct.name("invariant 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");
             
@@ -212,7 +216,7 @@ namespace storm {
                                  > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createDummyCommand, phoenix::ref(*this), qi::_1, qi::_r1)];
             commandDefinition.name("command definition");
 
-            moduleDefinition = ((qi::lit("module") >> identifier >> *(variableDefinition(qi::_a, qi::_b))) > *commandDefinition(qi::_r1) > qi::lit("endmodule"))[qi::_val = phoenix::bind(&PrismParser::createModule, phoenix::ref(*this), qi::_1, qi::_a, qi::_b, qi::_2, qi::_r1)];
+            moduleDefinition = ((qi::lit("module") >> identifier >> *(variableDefinition(qi::_a, qi::_b, qi::_c))) > -invariantConstruct > (*commandDefinition(qi::_r1)) > qi::lit("endmodule"))[qi::_val = phoenix::bind(&PrismParser::createModule, phoenix::ref(*this), qi::_1, qi::_a, qi::_b, qi::_c, qi::_2, qi::_3, qi::_r1)];
             moduleDefinition.name("module definition");
             
             moduleRenaming = ((qi::lit("module") >> identifier >> qi::lit("=")) > identifier > qi::lit("[")
@@ -249,6 +253,7 @@ namespace storm {
             qi::on_success(definedDoubleConstantDefinition, setLocationInfoFunction);
             qi::on_success(booleanVariableDefinition, setLocationInfoFunction);
             qi::on_success(integerVariableDefinition, setLocationInfoFunction);
+            qi::on_success(clockVariableDefinition, setLocationInfoFunction);
             qi::on_success(moduleDefinition, setLocationInfoFunction);
             qi::on_success(moduleRenaming, setLocationInfoFunction);
             qi::on_success(formulaDefinition, setLocationInfoFunction);
@@ -586,14 +591,35 @@ namespace storm {
             return storm::prism::IntegerVariable(manager->getVariable(variableName), lowerBoundExpression, upperBoundExpression, initialValueExpression, observable, this->getFilename());
         }
         
+        storm::prism::ClockVariable PrismParser::createClockVariable(std::string const& variableName) const {
+            if (!this->secondRun) {
+                try {
+                    storm::expressions::Variable newVariable = manager->declareRationalVariable(variableName);
+                    this->identifiers_.add(variableName, newVariable.getExpression());
+                } catch (storm::exceptions::InvalidArgumentException const& e) {
+                    if (manager->hasVariable(variableName)) {
+                        STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << variableName << "'.");
+                    } else {
+                        STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": illegal identifier '" << variableName << "'.");
+                    }
+                }
+            }
+            bool observable = this->observables.count(variableName) > 0;
+            if(observable) {
+                this->observables.erase(variableName);
+            }
+
+            return storm::prism::ClockVariable(manager->getVariable(variableName), observable, this->getFilename());
+        }
+
         void PrismParser::createObservablesList(std::vector<std::string> const& observables) {
             this->observables.insert(observables.begin(), observables.end());
             // We need this list to be filled in both runs.
         }
         
-        storm::prism::Module PrismParser::createModule(std::string const& moduleName, std::vector<storm::prism::BooleanVariable> const& booleanVariables, std::vector<storm::prism::IntegerVariable> const& integerVariables, std::vector<storm::prism::Command> const& commands, GlobalProgramInformation& globalProgramInformation) const {
+        storm::prism::Module PrismParser::createModule(std::string const& moduleName, std::vector<storm::prism::BooleanVariable> const& booleanVariables, std::vector<storm::prism::IntegerVariable> const& integerVariables, std::vector<storm::prism::ClockVariable> const& clockVariables, boost::optional<storm::expressions::Expression> const& invariant, std::vector<storm::prism::Command> const& commands, GlobalProgramInformation& globalProgramInformation) const {
             globalProgramInformation.moduleToIndexMap[moduleName] = globalProgramInformation.modules.size();
-            return storm::prism::Module(moduleName, booleanVariables, integerVariables, commands, this->getFilename());
+            return storm::prism::Module(moduleName, booleanVariables, integerVariables, clockVariables, invariant.is_initialized()? invariant.get() : storm::expressions::Expression(), commands, this->getFilename());
         }
         
         storm::prism::Module PrismParser::createRenamedModule(std::string const& newModuleName, std::string const& oldModuleName, std::map<std::string, std::string> const& renaming, GlobalProgramInformation& globalProgramInformation) const {
@@ -622,6 +648,15 @@ namespace storm {
                         this->observables.erase(renamingPair->second);
                     }
                 }
+                for (auto const& variable : moduleToRename.getClockVariables()) {
+                    auto const& renamingPair = renaming.find(variable.getName());
+                    STORM_LOG_THROW(renamingPair != renaming.end(), storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Clock variable '" << variable.getName() << " was not renamed.");
+                    storm::expressions::Variable renamedVariable = manager->declareRationalVariable(renamingPair->second);
+                    this->identifiers_.add(renamingPair->second, renamedVariable.getExpression());
+                    if(this->observables.count(renamingPair->second) > 0) {
+                        this->observables.erase(renamingPair->second);
+                    }
+                }
                 
                 for (auto const& command : moduleToRename.getCommands()) {
                     std::string newActionName = command.getActionName();
@@ -678,6 +713,24 @@ namespace storm {
                     integerVariables.push_back(storm::prism::IntegerVariable(manager->getVariable(renamingPair->second), variable.getLowerBoundExpression().substitute(expressionRenaming), variable.getUpperBoundExpression().substitute(expressionRenaming), variable.hasInitialValue() ? variable.getInitialValueExpression().substitute(expressionRenaming) : variable.getInitialValueExpression(), observable, this->getFilename(), get_line(qi::_1)));
                 }
 
+                // Rename the clock variables.
+                std::vector<storm::prism::ClockVariable> clockVariables;
+                for (auto const& variable : moduleToRename.getClockVariables()) {
+                    auto const& renamingPair = renaming.find(variable.getName());
+                    STORM_LOG_THROW(renamingPair != renaming.end(), storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Clock variable '" << variable.getName() << " was not renamed.");
+                    bool observable = this->observables.count(renamingPair->second) > 0;
+                    if (observable) {
+                        this->observables.erase(renamingPair->second);
+                    }
+                    clockVariables.push_back(storm::prism::ClockVariable(manager->getVariable(renamingPair->second), observable, this->getFilename(), get_line(qi::_1)));
+                }
+                
+                // Rename invariant (if present)
+                storm::expressions::Expression invariant;
+                if (moduleToRename.hasInvariant()) {
+                    invariant = moduleToRename.getInvariant().substitute(expressionRenaming);
+                }
+                
                 // Rename commands.
                 std::vector<storm::prism::Command> commands;
                 for (auto const& command : moduleToRename.getCommands()) {
@@ -716,7 +769,7 @@ namespace storm {
                     ++globalProgramInformation.currentCommandIndex;
                 }
                 
-                return storm::prism::Module(newModuleName, booleanVariables, integerVariables, commands, oldModuleName, renaming);
+                return storm::prism::Module(newModuleName, booleanVariables, integerVariables, clockVariables, invariant, commands, oldModuleName, renaming);
             }
         }
         

src/storm-parsers/parser/PrismParser.h

@@ -98,7 +98,8 @@ namespace storm {
                     ("mdp", storm::prism::Program::ModelType::MDP)
                     ("ctmdp", storm::prism::Program::ModelType::CTMDP)
                     ("ma", storm::prism::Program::ModelType::MA)
-                    ("pomdp", storm::prism::Program::ModelType::POMDP);
+                    ("pomdp", storm::prism::Program::ModelType::POMDP)
+                    ("pta", storm::prism::Program::ModelType::PTA);
                 }
             };
             
@@ -111,21 +112,24 @@ namespace storm {
                     ("ctmdp", 4)
                     ("ma", 5)
                     ("pomdp", 6)
-                    ("const", 7)
-                    ("int", 8)
-                    ("bool", 9)
-                    ("module", 10)
-                    ("endmodule", 11)
-                    ("rewards", 12)
-                    ("endrewards", 13)
-                    ("true", 14)
-                    ("false", 15)
-                    ("min", 16)
-                    ("max", 17)
-                    ("floor", 18)
-                    ("ceil", 19)
-                    ("init", 20)
-                    ("endinit", 21);
+                    ("pta", 7)
+                    ("const", 8)
+                    ("int", 9)
+                    ("bool", 10)
+                    ("module", 11)
+                    ("endmodule", 12)
+                    ("rewards", 13)
+                    ("endrewards", 14)
+                    ("true", 15)
+                    ("false", 16)
+                    ("min", 17)
+                    ("max", 18)
+                    ("floor", 19)
+                    ("ceil", 20)
+                    ("init", 21)
+                    ("endinit", 22)
+                    ("invariant", 23)
+                    ("endinvariant", 24);
                 }
             };
             
@@ -213,13 +217,14 @@ namespace storm {
             
             // Rules for modules definition.
             qi::rule<Iterator, std::vector<storm::prism::Module>(GlobalProgramInformation&), Skipper> moduleDefinitionList;
-            qi::rule<Iterator, storm::prism::Module(GlobalProgramInformation&), qi::locals<std::vector<storm::prism::BooleanVariable>, std::vector<storm::prism::IntegerVariable>>, Skipper> moduleDefinition;
+            qi::rule<Iterator, storm::prism::Module(GlobalProgramInformation&), qi::locals<std::vector<storm::prism::BooleanVariable>, std::vector<storm::prism::IntegerVariable>, std::vector<storm::prism::ClockVariable>>, Skipper> moduleDefinition;
             qi::rule<Iterator, storm::prism::Module(GlobalProgramInformation&), qi::locals<std::map<std::string, std::string>>, Skipper> moduleRenaming;
             
             // Rules for variable definitions.
-            qi::rule<Iterator, qi::unused_type(std::vector<storm::prism::BooleanVariable>&, std::vector<storm::prism::IntegerVariable>&), Skipper> variableDefinition;
+            qi::rule<Iterator, qi::unused_type(std::vector<storm::prism::BooleanVariable>&, std::vector<storm::prism::IntegerVariable>&, std::vector<storm::prism::ClockVariable>&), Skipper> variableDefinition;
             qi::rule<Iterator, storm::prism::BooleanVariable(), qi::locals<storm::expressions::Expression>, Skipper> booleanVariableDefinition;
             qi::rule<Iterator, storm::prism::IntegerVariable(), qi::locals<storm::expressions::Expression>, Skipper> integerVariableDefinition;
+            qi::rule<Iterator, storm::prism::ClockVariable(), qi::locals<storm::expressions::Expression>, Skipper> clockVariableDefinition;
             
             // Rules for command definitions.
             qi::rule<Iterator, storm::prism::Command(GlobalProgramInformation&), qi::locals<bool>, Skipper> commandDefinition;
@@ -239,6 +244,9 @@ namespace storm {
 
             qi::rule<Iterator, qi::unused_type(), Skipper> observablesConstruct;
             
+            // Rules for invariant constructs
+            qi::rule<Iterator, storm::expressions::Expression(), Skipper> invariantConstruct;
+
             // 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;
@@ -303,7 +311,8 @@ namespace storm {
             storm::prism::Command createDummyCommand(boost::optional<std::string> const& actionName, GlobalProgramInformation& globalProgramInformation) const;
             storm::prism::BooleanVariable createBooleanVariable(std::string const& variableName, storm::expressions::Expression initialValueExpression) const;
             storm::prism::IntegerVariable createIntegerVariable(std::string const& variableName, storm::expressions::Expression lowerBoundExpression, storm::expressions::Expression upperBoundExpression, storm::expressions::Expression initialValueExpression) const;
-            storm::prism::Module createModule(std::string const& moduleName, std::vector<storm::prism::BooleanVariable> const& booleanVariables, std::vector<storm::prism::IntegerVariable> const& integerVariables, std::vector<storm::prism::Command> const& commands, GlobalProgramInformation& globalProgramInformation) const;
+            storm::prism::ClockVariable createClockVariable(std::string const& variableName) const;
+            storm::prism::Module createModule(std::string const& moduleName, std::vector<storm::prism::BooleanVariable> const& booleanVariables, std::vector<storm::prism::IntegerVariable> const& integerVariables, std::vector<storm::prism::ClockVariable> const& clockVariables, boost::optional<storm::expressions::Expression> const& invariant, std::vector<storm::prism::Command> const& commands, GlobalProgramInformation& globalProgramInformation) const;
             storm::prism::Module createRenamedModule(std::string const& newModuleName, std::string const& oldModuleName, std::map<std::string, std::string> const& renaming, GlobalProgramInformation& globalProgramInformation) const;
             storm::prism::Program createProgram(GlobalProgramInformation const& globalProgramInformation) const;
             void createObservablesList(std::vector<std::string> const& observables);

src/storm/storage/prism/ClockVariable.cpp

@@ -0,0 +1,24 @@
+#include "storm/storage/prism/ClockVariable.h"
+
+#include "storm/storage/expressions/ExpressionManager.h"
+#include "storm/utility/constants.h"
+
+namespace storm {
+    namespace prism {
+        ClockVariable::ClockVariable(storm::expressions::Variable const& variable, bool observable, std::string const& filename, uint_fast64_t lineNumber) : Variable(variable, variable.getManager().rational(storm::utility::zero<storm::RationalNumber>()), observable, filename, lineNumber) {
+            // Nothing to do here.
+        }
+        
+        void ClockVariable::createMissingInitialValue() {
+            if (!this->hasInitialValue()) {
+                this->setInitialValueExpression(this->getExpressionVariable().getManager().rational(storm::utility::zero<storm::RationalNumber>()));
+            }
+        }
+        
+        std::ostream& operator<<(std::ostream& stream, ClockVariable const& variable) {
+            stream << variable.getName() << ": clock" << ";";
+            return stream;
+        }
+        
+    } // namespace prism
+} // namespace storm

src/storm/storage/prism/ClockVariable.h

@@ -0,0 +1,37 @@
+#pragma once
+
+#include <map>
+
+#include "storm/storage/prism/Variable.h"
+
+namespace storm {
+    namespace prism {
+        class ClockVariable : public Variable {
+        public:
+            // Create default implementations of constructors/assignment.
+            ClockVariable() = default;
+            ClockVariable(ClockVariable const& other) = default;
+            ClockVariable& operator=(ClockVariable const& other)= default;
+            ClockVariable(ClockVariable&& other) = default;
+            ClockVariable& operator=(ClockVariable&& other) = default;
+
+            /*!
+             * Creates a clock variable
+             *
+             * @param variable The expression variable associated with this variable.
+             * @param filename The filename in which the variable is defined.
+             * @param lineNumber The line number in which the variable is defined.
+             */
+            ClockVariable(storm::expressions::Variable const& variable, bool observable, std::string const& filename = "", uint_fast64_t lineNumber = 0);
+            
+            /*!
+             * Sets a missing initial value (note that for clock variables, this is always zero)
+             */
+            virtual void createMissingInitialValue() override;
+            
+            friend std::ostream& operator<<(std::ostream& stream, ClockVariable const& variable);
+        };
+        
+    } // namespace prism
+} // namespace storm
+

src/storm/storage/prism/Module.cpp

@@ -6,11 +6,11 @@
 
 namespace storm {
     namespace prism {
-        Module::Module(std::string const& moduleName, std::vector<storm::prism::BooleanVariable> const& booleanVariables, std::vector<storm::prism::IntegerVariable> const& integerVariables, std::vector<storm::prism::Command> const& commands, std::string const& filename, uint_fast64_t lineNumber) : Module(moduleName, booleanVariables, integerVariables, commands, "", std::map<std::string, std::string>(), filename, lineNumber) {
+        Module::Module(std::string const& moduleName, std::vector<storm::prism::BooleanVariable> const& booleanVariables, std::vector<storm::prism::IntegerVariable> const& integerVariables, std::vector<storm::prism::ClockVariable> const& clockVariables, storm::expressions::Expression const& invariant, std::vector<storm::prism::Command> const& commands, std::string const& filename, uint_fast64_t lineNumber) : Module(moduleName, booleanVariables, integerVariables, clockVariables, invariant, commands, "", std::map<std::string, std::string>(), filename, lineNumber) {
             // Intentionally left empty.
         }
         
-        Module::Module(std::string const& moduleName, std::vector<storm::prism::BooleanVariable> const& booleanVariables, std::vector<storm::prism::IntegerVariable> const& integerVariables, std::vector<storm::prism::Command> const& commands, std::string const& renamedFromModule, std::map<std::string, std::string> const& renaming, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), moduleName(moduleName), booleanVariables(booleanVariables), booleanVariableToIndexMap(), integerVariables(integerVariables), integerVariableToIndexMap(), commands(commands), synchronizingActionIndices(), actionIndicesToCommandIndexMap(), renamedFromModule(renamedFromModule), renaming(renaming) {
+        Module::Module(std::string const& moduleName, std::vector<storm::prism::BooleanVariable> const& booleanVariables, std::vector<storm::prism::IntegerVariable> const& integerVariables, std::vector<storm::prism::ClockVariable> const& clockVariables, storm::expressions::Expression const& invariant, std::vector<storm::prism::Command> const& commands, std::string const& renamedFromModule, std::map<std::string, std::string> const& renaming, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), moduleName(moduleName), booleanVariables(booleanVariables), booleanVariableToIndexMap(), integerVariables(integerVariables), integerVariableToIndexMap(), clockVariables(clockVariables), clockVariableToIndexMap(), invariant(invariant), commands(commands), synchronizingActionIndices(), actionIndicesToCommandIndexMap(), renamedFromModule(renamedFromModule), renaming(renaming) {
             // Initialize the internal mappings for fast information retrieval.
             this->createMappings();
         }
@@ -43,6 +43,20 @@ namespace storm {
             return this->integerVariables;
         }
         
+        std::size_t Module::getNumberOfClockVariables() const {
+            return this->clockVariables.size();
+        }
+        
+        storm::prism::ClockVariable const& Module::getClockVariable(std::string const& variableName) const {
+            auto const& nameIndexPair = this->clockVariableToIndexMap.find(variableName);
+            STORM_LOG_THROW(nameIndexPair != this->clockVariableToIndexMap.end(), storm::exceptions::InvalidArgumentException, "Unknown clock variable '" << variableName << "'.");
+            return this->getClockVariables()[nameIndexPair->second];
+        }
+        
+        std::vector<storm::prism::ClockVariable> const& Module::getClockVariables() const {
+            return this->clockVariables;
+        }
+
         std::set<storm::expressions::Variable> Module::getAllExpressionVariables() const {
             std::set<storm::expressions::Variable> result;
             for (auto const& var : this->getBooleanVariables()) {
@@ -51,6 +65,9 @@ namespace storm {
             for (auto const& var : this->getIntegerVariables()) {
                 result.insert(var.getExpressionVariable());
             }
+            for (auto const& var : this->getClockVariables()) {
+                result.insert(var.getExpressionVariable());
+            }
             return result;
         }
         
@@ -134,6 +151,9 @@ namespace storm {
             for (uint_fast64_t i = 0; i < this->integerVariables.size(); ++i) {
                 this->integerVariableToIndexMap[this->getIntegerVariables()[i].getName()] = i;
             }
+            for (uint_fast64_t i = 0; i < this->clockVariables.size(); ++i) {
+                this->booleanVariableToIndexMap[this->getClockVariables()[i].getName()] = i;
+            }
             
             // Add the mapping for all commands.
             for (uint_fast64_t i = 0; i < this->commands.size(); i++) {
@@ -169,7 +189,7 @@ namespace storm {
                 }
             }
             
-            return Module(this->getName(), this->getBooleanVariables(), this->getIntegerVariables(), newCommands);
+            return Module(this->getName(), this->getBooleanVariables(), this->getIntegerVariables(), this->getClockVariables(), this->getInvariant(), newCommands);
         }
         
         Module Module::restrictActionIndices(boost::container::flat_set<uint_fast64_t> const& actionIndices) const {
@@ -181,7 +201,7 @@ namespace storm {
                 }
             }
             
-            return Module(this->getName(), this->getBooleanVariables(), this->getIntegerVariables(), newCommands);
+            return Module(this->getName(), this->getBooleanVariables(), this->getIntegerVariables(), this->getClockVariables(), this->getInvariant(), newCommands);
         }
         
         Module Module::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
@@ -203,7 +223,7 @@ namespace storm {
                 newCommands.emplace_back(command.substitute(substitution));
             }
             
-            return Module(this->getName(), newBooleanVariables, newIntegerVariables, newCommands, this->getFilename(), this->getLineNumber());
+            return Module(this->getName(), newBooleanVariables, newIntegerVariables, this->getClockVariables(), this->getInvariant(), newCommands, this->getFilename(), this->getLineNumber());
         }
         
         bool Module::containsVariablesOnlyInUpdateProbabilities(std::set<storm::expressions::Variable> const& undefinedConstantVariables) const {
@@ -240,6 +260,17 @@ namespace storm {
             for (auto& variable : integerVariables) {
                 variable.createMissingInitialValue();
             }
+            for (auto& variable : clockVariables) {
+                variable.createMissingInitialValue();
+            }
+        }
+        
+        bool Module::hasInvariant() const {
+            return this->invariant.isInitialized();
+        }
+
+        storm::expressions::Expression const& Module::getInvariant() const {
+            return this->invariant;
         }
 
         std::ostream& operator<<(std::ostream& stream, Module const& module) {
@@ -250,6 +281,9 @@ namespace storm {
             for (auto const& integerVariable : module.getIntegerVariables()) {
                 stream << "\t" << integerVariable << std::endl;
             }
+            for (auto const& clockVariable : module.getClockVariables()) {
+                stream << "\t" << clockVariable << std::endl;
+            }
             for (auto const& command : module.getCommands()) {
                 stream << "\t" << command << std::endl;
             }

src/storm/storage/prism/Module.h

@@ -10,6 +10,7 @@
 
 #include "storm/storage/prism/BooleanVariable.h"
 #include "storm/storage/prism/IntegerVariable.h"
+#include "storm/storage/prism/ClockVariable.h"
 #include "storm/storage/prism/Command.h"
 #include "storm/utility/OsDetection.h"
 
@@ -23,11 +24,13 @@ namespace storm {
              * @param moduleName The name of the module.
              * @param booleanVariables The boolean variables defined by the module.
              * @param integerVariables The integer variables defined by the module.
+             * @param clockVariables The clock variables defined by the module (only for PTA models).
+             * @param invariant An invariant that is used to restrict the values of the clock variables (only for PTA models).
              * @param commands The commands of the module.
              * @param filename The filename in which the module is defined.
              * @param lineNumber The line number in which the module is defined.
              */
-            Module(std::string const& moduleName, std::vector<storm::prism::BooleanVariable> const& booleanVariables, std::vector<storm::prism::IntegerVariable> const& integerVariables, std::vector<storm::prism::Command> const& commands, std::string const& filename = "", uint_fast64_t lineNumber = 0);
+            Module(std::string const& moduleName, std::vector<storm::prism::BooleanVariable> const& booleanVariables, std::vector<storm::prism::IntegerVariable> const& integerVariables, std::vector<storm::prism::ClockVariable> const& clockVariables, storm::expressions::Expression const& invariant, std::vector<storm::prism::Command> const& commands, std::string const& filename = "", uint_fast64_t lineNumber = 0);
 
             /*!
              * Creates a module with the given name, variables and commands that is marked as being renamed from the
@@ -36,13 +39,15 @@ namespace storm {
              * @param moduleName The name of the module.
              * @param booleanVariables The boolean variables defined by the module.
              * @param integerVariables The integer variables defined by the module.
+             * @param clockVariables The clock variables defined by the module (only for PTA models).
+             * @param invariant An invariant that is used to restrict the values of the clock variables (only for PTA models).
              * @param commands The commands of the module.
              * @param renamedFromModule The name of the module from which this module was renamed.
              * @param renaming The renaming of identifiers used to create this module.
              * @param filename The filename in which the module is defined.
              * @param lineNumber The line number in which the module is defined.
              */
-            Module(std::string const& moduleName, std::vector<storm::prism::BooleanVariable> const& booleanVariables, std::vector<storm::prism::IntegerVariable> const& integerVariables, std::vector<storm::prism::Command> const& commands, std::string const& renamedFromModule, std::map<std::string, std::string> const& renaming, std::string const& filename = "", uint_fast64_t lineNumber = 0);
+            Module(std::string const& moduleName, std::vector<storm::prism::BooleanVariable> const& booleanVariables, std::vector<storm::prism::IntegerVariable> const& integerVariables, std::vector<storm::prism::ClockVariable> const& clockVariables, storm::expressions::Expression const& invariant, std::vector<storm::prism::Command> const& commands, std::string const& renamedFromModule, std::map<std::string, std::string> const& renaming, std::string const& filename = "", uint_fast64_t lineNumber = 0);
 
             // Create default implementations of constructors/assignment.
             Module() = default;
@@ -95,6 +100,28 @@ namespace storm {
              */
             std::vector<storm::prism::IntegerVariable> const& getIntegerVariables() const;
             
+            /*!
+             * Retrieves the number of clock variables in the module.
+             *
+             * @return the number of clock variables in the module.
+             */
+            std::size_t getNumberOfClockVariables() const;
+            
+            /*!
+             * Retrieves a reference to the clock variable with the given name.
+             *
+             * @param variableName The name of the clock variable to retrieve.
+             * @return A reference to the clock variable with the given name.
+             */
+            storm::prism::ClockVariable const& getClockVariable(std::string const& variableName) const;
+            
+            /*!
+             * Retrieves the clock variables of the module.
+             *
+             * @return The clock variables of the module.
+             */
+            std::vector<storm::prism::ClockVariable> const& getClockVariables() const;
+            
             /*!
              * Retrieves all expression variables used by this module.
              *
@@ -236,6 +263,16 @@ namespace storm {
              */
             void createMissingInitialValues();
             
+            /*!
+             * Returns true, if an invariant was specified (only relevant for PTA models)
+             */
+            bool hasInvariant() const;
+            
+            /*!
+             * Returns the specified invariant (only relevant for PTA models)
+             */
+             storm::expressions::Expression const& getInvariant() const;
+            
             friend std::ostream& operator<<(std::ostream& stream, Module const& module);
 
         private:
@@ -259,6 +296,15 @@ namespace storm {
             // A mapping from integer variables to the corresponding indices in the vector.
             std::map<std::string, uint_fast64_t> integerVariableToIndexMap;
             
+            // A list of clock variables.
+            std::vector<storm::prism::ClockVariable> clockVariables;
+
+            // A mapping from clock variables to the corresponding indices in the vector.
+            std::map<std::string, uint_fast64_t> clockVariableToIndexMap;
+            
+            // An invariant (only for PTA models)
+            storm::expressions::Expression invariant;
+
             // The commands associated with the module.
             std::vector<storm::prism::Command> commands;
             

src/storm/storage/prism/Program.cpp

@@ -810,9 +810,12 @@ namespace storm {
                 for (auto const& booleanVariable : module.getBooleanVariables()) {
                     this->variableToModuleIndexMap[booleanVariable.getName()] = moduleIndex;
                 }
-                for (auto const& integerVariable : module.getBooleanVariables()) {
+                for (auto const& integerVariable : module.getIntegerVariables()) {
                     this->variableToModuleIndexMap[integerVariable.getName()] = moduleIndex;
                 }
+                for (auto const& clockVariable : module.getClockVariables()) {
+                    this->variableToModuleIndexMap[clockVariable.getName()] = moduleIndex;
+                }
             }
             
         }
@@ -1104,6 +1107,12 @@ namespace storm {
                     variables.insert(variable.getExpressionVariable());
                     all.insert(variable.getExpressionVariable());
                 }
+                
+                for (auto const& variable : module.getClockVariables()) {
+                    // Record the new identifier for future checks.
+                    variables.insert(variable.getExpressionVariable());
+                    all.insert(variable.getExpressionVariable());
+                }
             }
             
             // Create the set of valid identifiers for future checks.
@@ -1121,7 +1130,7 @@ namespace storm {
                 }
             }
             
-            // Check the commands of the modules.
+            // Check the commands and invariants of the modules.
             bool hasProbabilisticCommand = false;
             bool hasMarkovianCommand = false;
             bool hasLabeledMarkovianCommand = false;
@@ -1133,6 +1142,24 @@ namespace storm {
                 for (auto const& variable : module.getIntegerVariables()) {
                     legalVariables.insert(variable.getExpressionVariable());
                 }
+                for (auto const& variable : module.getClockVariables()) {
+                    legalVariables.insert(variable.getExpressionVariable());
+                }
+                
+                if (module.hasInvariant()) {
+                    std::set<storm::expressions::Variable> containedVariables = module.getInvariant().getVariables();
+                    std::set<storm::expressions::Variable> illegalVariables;
+                    std::set_difference(containedVariables.begin(), containedVariables.end(), variablesAndConstants.begin(), variablesAndConstants.end(), std::inserter(illegalVariables, illegalVariables.begin()));
+                    bool isValid = illegalVariables.empty();
+                    if (!isValid) {
+                        std::vector<std::string> illegalVariableNames;
+                        for (auto const& var : illegalVariables) {
+                            illegalVariableNames.push_back(var.getName());
+                        }
+                        STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << module.getFilename() << ", line " << module.getLineNumber() << ": invariant " << module.getInvariant()  << " refers to unknown identifiers: " << boost::algorithm::join(illegalVariableNames, ",") << ".");
+                    }
+                    STORM_LOG_THROW(module.getInvariant().hasBooleanType(), storm::exceptions::WrongFormatException, "Error in " << module.getFilename() << ", line " << module.getLineNumber() << ": invariant " << module.getInvariant() << " must evaluate to type 'bool'.");
+                }
                 
                 for (auto& command : module.getCommands()) {
                     // Check the guard.
@@ -1189,7 +1216,7 @@ namespace storm {
                                 }
                             }
                             STORM_LOG_THROW(alreadyAssignedVariables.find(assignedVariable) == alreadyAssignedVariables.end(), storm::exceptions::WrongFormatException, "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": duplicate assignment to variable '" << assignment.getVariableName() << "'.");
-                            STORM_LOG_THROW(assignedVariable.getType() == assignment.getExpression().getType(), storm::exceptions::WrongFormatException, "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": illegally assigning a value of type '" << assignment.getExpression().getType() << "' to variable '" << assignment.getVariableName() << "' of type '" << assignedVariable.getType() << "'.");
+                            STORM_LOG_THROW(assignedVariable.getType() == assignment.getExpression().getType() || (assignedVariable.getType().isRationalType() && assignment.getExpression().getType().isNumericalType()), storm::exceptions::WrongFormatException, "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": illegally assigning a value of type '" << assignment.getExpression().getType() << "' to variable '" << assignment.getVariableName() << "' of type '" << assignedVariable.getType() << "'.");
                             
                             containedVariables = assignment.getExpression().getVariables();
                             illegalVariables.clear();
@@ -1409,7 +1436,8 @@ namespace storm {
                     }
                 }
                 
-                newModules.emplace_back(module.getName(), newBooleanVars, newIntegerVars, newCommands);
+                // we currently do not simplify clock variables or invariants
+                newModules.emplace_back(module.getName(), newBooleanVars, newIntegerVars, module.getClockVariables(), module.getInvariant(), newCommands);
                 
                 // Determine the set of action indices that have been deleted entirely.
                 std::set_difference(module.getSynchronizingActionIndices().begin(), module.getSynchronizingActionIndices().end(), newModules.back().getSynchronizingActionIndices().begin(), newModules.back().getSynchronizingActionIndices().end(), std::inserter(actionIndicesToDelete, actionIndicesToDelete.begin()));
@@ -1464,6 +1492,7 @@ namespace storm {
             std::stringstream newModuleName;
             std::vector<storm::prism::BooleanVariable> allBooleanVariables;
             std::vector<storm::prism::IntegerVariable> allIntegerVariables;
+            std::vector<storm::prism::ClockVariable> allClockVariables;
             std::vector<storm::prism::Command> newCommands;
             uint_fast64_t nextCommandIndex = 0;
             uint_fast64_t nextUpdateIndex = 0;
@@ -1489,6 +1518,7 @@ namespace storm {
             // this is just for simplicity and is not needed.
             allBooleanVariables.insert(allBooleanVariables.end(), this->getGlobalBooleanVariables().begin(), this->getGlobalBooleanVariables().end());
             allIntegerVariables.insert(allIntegerVariables.end(), this->getGlobalIntegerVariables().begin(), this->getGlobalIntegerVariables().end());
+            storm::expressions::Expression newInvariant;
             
             // Now go through the modules, gather the variables, construct the name of the new module and assert the
             // bounds of the discovered variables.
@@ -1496,12 +1526,17 @@ namespace storm {
                 newModuleName << module.getName() << "_";
                 allBooleanVariables.insert(allBooleanVariables.end(), module.getBooleanVariables().begin(), module.getBooleanVariables().end());
                 allIntegerVariables.insert(allIntegerVariables.end(), module.getIntegerVariables().begin(), module.getIntegerVariables().end());
+                allClockVariables.insert(allClockVariables.end(), module.getClockVariables().begin(), module.getClockVariables().end());
                 
                 for (auto const& variable : module.getIntegerVariables()) {
                     solver->add(variable.getExpression() >= variable.getLowerBoundExpression());
                     solver->add(variable.getExpression() <= variable.getUpperBoundExpression());
                 }
                 
+                if (module.hasInvariant()) {
+                    newInvariant = newInvariant.isInitialized() ? (newInvariant && module.getInvariant()) : module.getInvariant();
+                }
+                
                 // The commands without a synchronizing action name, can simply be copied (plus adjusting the global
                 // indices of the command and its updates).
                 for (auto const& command : module.getCommands()) {
@@ -1643,7 +1678,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);
+            storm::prism::Module singleModule(newModuleName.str(), allBooleanVariables, allIntegerVariables, allClockVariables, newInvariant, 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->getOptionalInitialConstruct(), this->getOptionalSystemCompositionConstruct(), prismCompatibility, this->getFilename(), 0, true);
         }
@@ -1852,6 +1887,7 @@ namespace storm {
                 case Program::ModelType::CTMDP: out << "ctmdp"; break;
                 case Program::ModelType::MA: out << "ma"; break;
                 case Program::ModelType::POMDP: out << "pomdp"; break;
+                case Program::ModelType::PTA: out << "pta"; break;
             }
             return out;
         }

src/storm/storage/prism/Program.h

@@ -31,7 +31,7 @@ namespace storm {
             /*!
              * An enum for the different model types.
              */
-            enum class ModelType {UNDEFINED, DTMC, CTMC, MDP, CTMDP, MA, POMDP};
+            enum class ModelType {UNDEFINED, DTMC, CTMC, MDP, CTMDP, MA, POMDP, PTA};
             
             enum class ValidityCheckLevel  : unsigned {VALIDINPUT = 0, READYFORPROCESSING = 1};