Started working on Markovian commands in PRISM programs.

Former-commit-id: 94ed3c747c

src/parser/PrismParser.cpp

@@ -1,4 +1,7 @@
 #include "src/parser/PrismParser.h"
+
+#include "src/settings/SettingsManager.h"
+
 #include "src/exceptions/InvalidArgumentException.h"
 #include "src/exceptions/InvalidTypeException.h"
 #include "src/exceptions/WrongFormatException.h"
@@ -139,7 +142,12 @@ namespace storm {
             updateListDefinition %= +updateDefinition(qi::_r1) % "+";
             updateListDefinition.name("update list");
             
-            commandDefinition = (qi::lit("[") > -(identifier[qi::_a = qi::_1]) > qi::lit("]") > +(qi::char_ - qi::lit(";")) > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createCommand, phoenix::ref(*this), qi::_a, qi::_r1)];
+            // This is a dummy command-definition (it ignores the actual contents of the command) that is overwritten when the parser is moved to the second run.
+            commandDefinition = (((qi::lit("[") > -(identifier[qi::_a = qi::_1]) > qi::lit("]"))
+                                  |
+                                 (qi::lit("<") > -(identifier[qi::_a = qi::_1]) > qi::lit(">")[qi::_b = true]))
+                                 > +(qi::char_ - qi::lit(";"))
+                                 > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createCommand, phoenix::ref(*this), qi::_a, 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)];
@@ -191,7 +199,13 @@ namespace storm {
         void PrismParser::moveToSecondRun() {
             // In the second run, we actually need to parse the commands instead of just skipping them,
             // so we adapt the rule for parsing commands.
-            commandDefinition = (qi::lit("[") > -(identifier[qi::_a = qi::_1]) > qi::lit("]") > expressionParser > qi::lit("->") > updateListDefinition(qi::_r1) > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createCommand, phoenix::ref(*this), qi::_a, qi::_2, qi::_3, qi::_r1)];
+            commandDefinition = (((qi::lit("[") > -(identifier[qi::_a = qi::_1]) > qi::lit("]"))
+                                 |
+                                  (qi::lit("<") > -(identifier[qi::_a = qi::_1]) > qi::lit(">")[qi::_b = true]))
+                                 > expressionParser
+                                 > qi::lit("->")
+                                 > updateListDefinition(qi::_r1)
+                                 > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createCommand, phoenix::ref(*this), qi::_b, qi::_a, qi::_2, qi::_3, qi::_r1)];
             
             this->secondRun = true;
             this->expressionParser.setIdentifierMapping(&this->identifiers_);
@@ -359,7 +373,7 @@ namespace storm {
             return storm::prism::Update(globalProgramInformation.currentUpdateIndex - 1, likelihoodExpression, assignments, this->getFilename());
         }
         
-        storm::prism::Command PrismParser::createCommand(std::string const& actionName, storm::expressions::Expression guardExpression, std::vector<storm::prism::Update> const& updates, GlobalProgramInformation& globalProgramInformation) const {
+        storm::prism::Command PrismParser::createCommand(bool markovian, std::string const& actionName, storm::expressions::Expression guardExpression, std::vector<storm::prism::Update> const& updates, GlobalProgramInformation& globalProgramInformation) const {
             ++globalProgramInformation.currentCommandIndex;
             if (!actionName.empty()) {
                 auto const& nameIndexPair = globalProgramInformation.actionIndices.find(actionName);
@@ -367,7 +381,8 @@ namespace storm {
                     globalProgramInformation.actionIndices[actionName] = globalProgramInformation.actionIndices.size();
                 }
             }
-            return storm::prism::Command(globalProgramInformation.currentCommandIndex - 1, actionName.empty() ? 0 : globalProgramInformation.actionIndices[actionName], actionName, guardExpression, updates, this->getFilename());
+            
+            return storm::prism::Command(globalProgramInformation.currentCommandIndex - 1, markovian, actionName.empty() ? 0 : globalProgramInformation.actionIndices[actionName], actionName, guardExpression, updates, this->getFilename());
         }
         
         storm::prism::Command PrismParser::createCommand(std::string const& actionName, GlobalProgramInformation& globalProgramInformation) const {
@@ -507,7 +522,7 @@ namespace storm {
                         }
                     }
                     
-                    commands.emplace_back(globalProgramInformation.currentCommandIndex, newActionName.empty() ? 0 : globalProgramInformation.actionIndices[newActionName], newActionName, command.getGuardExpression().substitute(expressionRenaming), updates, this->getFilename(), get_line(qi::_1));
+                    commands.emplace_back(globalProgramInformation.currentCommandIndex, command.isMarkovian(), newActionName.empty() ? 0 : globalProgramInformation.actionIndices[newActionName], newActionName, command.getGuardExpression().substitute(expressionRenaming), updates, this->getFilename(), get_line(qi::_1));
                     ++globalProgramInformation.currentCommandIndex;
                 }
                 

src/parser/PrismParser.h

@@ -187,7 +187,7 @@ namespace storm {
             qi::rule<Iterator, storm::prism::IntegerVariable(), qi::locals<storm::expressions::Expression>, Skipper> integerVariableDefinition;
             
             // Rules for command definitions.
-            qi::rule<Iterator, storm::prism::Command(GlobalProgramInformation&), qi::locals<std::string>, Skipper> commandDefinition;
+            qi::rule<Iterator, storm::prism::Command(GlobalProgramInformation&), qi::locals<std::string, bool>, Skipper> commandDefinition;
             qi::rule<Iterator, std::vector<storm::prism::Update>(GlobalProgramInformation&), Skipper> updateListDefinition;
             qi::rule<Iterator, storm::prism::Update(GlobalProgramInformation&), Skipper> updateDefinition;
             qi::rule<Iterator, std::vector<storm::prism::Assignment>(), Skipper> assignmentDefinitionList;
@@ -236,7 +236,7 @@ namespace storm {
             storm::prism::TransitionReward createTransitionReward(std::string const& actionName, storm::expressions::Expression statePredicateExpression, storm::expressions::Expression rewardValueExpression, GlobalProgramInformation& globalProgramInformation) const;
             storm::prism::Assignment createAssignment(std::string const& variableName, storm::expressions::Expression assignedExpression) const;
             storm::prism::Update createUpdate(storm::expressions::Expression likelihoodExpression, std::vector<storm::prism::Assignment> const& assignments, GlobalProgramInformation& globalProgramInformation) const;
-            storm::prism::Command createCommand(std::string const& actionName, storm::expressions::Expression guardExpression, std::vector<storm::prism::Update> const& updates, GlobalProgramInformation& globalProgramInformation) const;
+            storm::prism::Command createCommand(bool markovianCommand, std::string const& actionName, storm::expressions::Expression guardExpression, std::vector<storm::prism::Update> const& updates, GlobalProgramInformation& globalProgramInformation) const;
             storm::prism::Command createCommand(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;

src/settings/modules/GeneralSettings.cpp

@@ -44,6 +44,8 @@ namespace storm {
             const std::string GeneralSettings::engineOptionName = "engine";
             const std::string GeneralSettings::engineOptionShortName = "e";
             const std::string GeneralSettings::cudaOptionName = "cuda";
+            const std::string GeneralSettings::prismCompatibilityOptionName = "prismcompat";
+            const std::string GeneralSettings::prismCompatibilityOptionShortName = "pc";
             
 #ifdef STORM_HAVE_CARL
             const std::string GeneralSettings::parametricOptionName = "parametric";
@@ -52,6 +54,7 @@ namespace storm {
             GeneralSettings::GeneralSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager, moduleName) {
                 this->addOption(storm::settings::OptionBuilder(moduleName, helpOptionName, false, "Shows all available options, arguments and descriptions.").setShortName(helpOptionShortName)
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("hint", "A regular expression to show help for all matching entities or 'all' for the complete help.").setDefaultValueString("all").build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, prismCompatibilityOptionName, false, "Enables PRISM compatibility. This may be necessary to process some PRISM models.").setShortName(prismCompatibilityOptionShortName).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, versionOptionName, false, "Prints the version information.").build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, verboseOptionName, false, "Enables more verbose output.").setShortName(verboseOptionShortName).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, precisionOptionName, false, "The internally used precision.").setShortName(precisionOptionShortName)
@@ -273,6 +276,10 @@ namespace storm {
                 STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown engine '" << engine << "'.");
             }
             
+            bool GeneralSettings::isPrismCompatibilityEnabled() const {
+                return this->getOption(prismCompatibilityOptionName).getHasOptionBeenSet();
+            }
+            
 #ifdef STORM_HAVE_CARL
             bool GeneralSettings::isParametricSet() const {
                 return this->getOption(parametricOptionName).getHasOptionBeenSet();

src/settings/modules/GeneralSettings.h

@@ -311,6 +311,13 @@ namespace storm {
                  */
                 Engine getEngine() const;
                 
+                /*!
+                 * Retrieves whether the PRISM compatibility mode was enabled.
+                 *
+                 * @return True iff the PRISM compatibility mode was enabled.
+                 */
+                bool isPrismCompatibilityEnabled() const;
+                
 #ifdef STORM_HAVE_CARL
                 /*!
                  * Retrieves whether the option enabling parametric model checking is set.
@@ -362,6 +369,8 @@ namespace storm {
                 static const std::string engineOptionName;
                 static const std::string engineOptionShortName;
                 static const std::string cudaOptionName;
+                static const std::string prismCompatibilityOptionName;
+                static const std::string prismCompatibilityOptionShortName;
                 
 #ifdef STORM_HAVE_CARL
                 static const std::string parametricOptionName;

src/storage/prism/Command.cpp

@@ -2,7 +2,7 @@
 
 namespace storm {
     namespace prism {
-        Command::Command(uint_fast64_t globalIndex, uint_fast64_t actionIndex, std::string const& actionName, storm::expressions::Expression const& guardExpression, std::vector<storm::prism::Update> const& updates, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), actionIndex(actionIndex), actionName(actionName), guardExpression(guardExpression), updates(updates), globalIndex(globalIndex), labeled(actionName != "") {
+        Command::Command(uint_fast64_t globalIndex, bool markovian, uint_fast64_t actionIndex, std::string const& actionName, storm::expressions::Expression const& guardExpression, std::vector<storm::prism::Update> const& updates, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), actionIndex(actionIndex), markovian(markovian), actionName(actionName), guardExpression(guardExpression), updates(updates), globalIndex(globalIndex), labeled(actionName != "") {
             // Nothing to do here.
         }
 
@@ -10,6 +10,14 @@ namespace storm {
             return this->actionIndex;
         }
         
+        bool Command::isMarkovian() const {
+            return this->markovian;
+        }
+        
+        void Command::setMarkovian(bool value) {
+            this->markovian = value;
+        }
+        
         std::string const& Command::getActionName() const {
             return this->actionName;
         }
@@ -41,7 +49,7 @@ namespace storm {
                 newUpdates.emplace_back(update.substitute(substitution));
             }
             
-            return Command(this->getGlobalIndex(), this->getActionIndex(), this->getActionName(), this->getGuardExpression().substitute(substitution).simplify(), newUpdates, this->getFilename(), this->getLineNumber());
+            return Command(this->getGlobalIndex(), this->isMarkovian(), this->getActionIndex(), this->getActionName(), this->getGuardExpression().substitute(substitution).simplify(), newUpdates, this->getFilename(), this->getLineNumber());
         }
         
         bool Command::isLabeled() const {
@@ -64,7 +72,12 @@ namespace storm {
         }
         
         std::ostream& operator<<(std::ostream& stream, Command const& command) {
-            stream << "[" << command.getActionName() << "] " << command.getGuardExpression() << " -> ";
+            if (command.isMarkovian()) {
+                stream << "<" << command.getActionName() << "> ";
+            } else {
+                stream << "[" << command.getActionName() << "] ";
+            }
+            stream << command.getGuardExpression() << " -> ";
             for (uint_fast64_t i = 0; i < command.getUpdates().size(); ++i) {
                 stream << command.getUpdate(i);
                 if (i < command.getUpdates().size() - 1) {

src/storage/prism/Command.h

@@ -17,6 +17,8 @@ namespace storm {
              * Creates a command with the given action name, guard and updates.
              *
              * @param globalIndex The global index of the command.
+             * @param markovian A flag indicating whether the command's update probabilities are to be interpreted as
+             * rates in a continuous-time model.
              * @param actionIndex The index of the action of the command.
              * @param actionName The action name of the command.
              * @param guardExpression the expression that defines the guard of the command.
@@ -24,7 +26,7 @@ namespace storm {
              * @param filename The filename in which the command is defined.
              * @param lineNumber The line number in which the command is defined.
              */
-            Command(uint_fast64_t globalIndex, uint_fast64_t actionIndex, std::string const& actionName, storm::expressions::Expression const& guardExpression, std::vector<storm::prism::Update> const& updates, std::string const& filename = "", uint_fast64_t lineNumber = 0);
+            Command(uint_fast64_t globalIndex, bool markovian, uint_fast64_t actionIndex, std::string const& actionName, storm::expressions::Expression const& guardExpression, std::vector<storm::prism::Update> const& updates, std::string const& filename = "", uint_fast64_t lineNumber = 0);
             
             // Create default implementations of constructors/assignment.
             Command() = default;
@@ -49,6 +51,22 @@ namespace storm {
              */
             uint_fast64_t getActionIndex() const;
             
+            /*!
+             * Retrieves whether the command is a Markovian command, i.e. it's update likelihoods are to be interpreted
+             * as rates in a continuous-time model.
+             *
+             * @return True iff the command is Markovian.
+             */
+            bool isMarkovian() const;
+            
+            /*!
+             * Sets whether this command is a Markovian command, i.e. it's update likelihoods are to be interpreted as
+             * rates in a continuous-time model.
+             *
+             * @param value The command is flagged as Markovian iff this flag is set.
+             */
+            void setMarkovian(bool value);
+            
             /*!
              * Retrieves a reference to the guard of the command.
              *
@@ -114,6 +132,10 @@ namespace storm {
             //  The index of the action associated with this command.
             uint_fast64_t actionIndex;
 
+            // A flag indicating whether the likelihoods attached to the updates are to be interpreted as rates rather
+            // than probabilities.
+            bool markovian;
+            
             // The name of the command.
             std::string actionName;
             

src/storage/prism/Module.cpp

@@ -63,6 +63,10 @@ namespace storm {
             return this->commands;
         }
         
+        std::vector<storm::prism::Command>& Module::getCommands() {
+            return this->commands;
+        }
+        
         std::string const& Module::getName() const {
             return this->moduleName;
         }

src/storage/prism/Module.h

@@ -126,6 +126,13 @@ namespace storm {
              * @return The commands of the module.
              */
             std::vector<storm::prism::Command> const& getCommands() const;
+
+            /*!
+             * Retrieves the commands of the module.
+             *
+             * @return The commands of the module.
+             */
+            std::vector<storm::prism::Command>& getCommands();
             
             /*!
              * Retrieves the name of the module.

src/storage/prism/Program.cpp

@@ -3,6 +3,7 @@
 #include <algorithm>
 
 #include "src/storage/expressions/ExpressionManager.h"
+#include "src/settings/SettingsManager.h"
 #include "src/utility/macros.h"
 #include "src/exceptions/InvalidArgumentException.h"
 #include "src/exceptions/OutOfRangeException.h"
@@ -34,8 +35,23 @@ namespace storm {
                 }
                 this->initialConstruct = storm::prism::InitialConstruct(newInitialExpression, this->getInitialConstruct().getFilename(), this->getInitialConstruct().getLineNumber());
             }
-            
+
             if (checkValidity) {
+                // If the model is supposed to be a CTMC, but contains probabilistic commands, we transform them to Markovian
+                // commands and issue a warning.
+                if (modelType == storm::prism::Program::ModelType::CTMC && storm::settings::generalSettings().isPrismCompatibilityEnabled()) {
+                    bool hasProbabilisticCommands = false;
+                    for (auto& module : this->modules) {
+                        for (auto& command : module.getCommands()) {
+                            if (!command.isMarkovian()) {
+                                command.setMarkovian(true);
+                                hasProbabilisticCommands = true;
+                            }
+                        }
+                    }
+                    STORM_LOG_WARN_COND(!hasProbabilisticCommands, "The input model is a CTMC, but uses probabilistic commands like they are used in PRISM. Consider rewriting the commands to use Markovian commands instead.");
+                }
+                
                 this->checkValidity();
             }
         }
@@ -576,6 +592,8 @@ namespace storm {
             std::set_union(variables.begin(), variables.end(), constants.begin(), constants.end(), std::inserter(variablesAndConstants, variablesAndConstants.begin()));
             
             // Check the commands of the modules.
+            bool hasProbabilisticCommand = false;
+            bool hasMarkovianCommand = false;
             for (auto const& module : this->getModules()) {
                 std::set<storm::expressions::Variable> legalVariables = globalVariables;
                 for (auto const& variable : module.getBooleanVariables()) {
@@ -585,13 +603,20 @@ namespace storm {
                     legalVariables.insert(variable.getExpressionVariable());
                 }
                 
-                for (auto const& command : module.getCommands()) {
+                for (auto& command : module.getCommands()) {
                     // Check the guard.
                     std::set<storm::expressions::Variable> containedVariables = command.getGuardExpression().getVariables();
                     bool isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedVariables.begin(), containedVariables.end());
                     STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": guard refers to unknown identifiers.");
                     STORM_LOG_THROW(command.getGuardExpression().hasBooleanType(), storm::exceptions::WrongFormatException, "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": expression for guard must evaluate to type 'bool'.");
                     
+                    // Record which types of commands were seen.
+                    if (command.isMarkovian()) {
+                        hasMarkovianCommand = true;
+                    } else {
+                        hasProbabilisticCommand = true;
+                    }
+                    
                     // Check all updates.
                     for (auto const& update : command.getUpdates()) {
                         containedVariables = update.getLikelihoodExpression().getVariables();
@@ -629,6 +654,12 @@ namespace storm {
                 }
             }
             
+            if (this->getModelType() == Program::ModelType::DTMC || this->getModelType() == Program::ModelType::MDP) {
+                STORM_LOG_THROW(!hasMarkovianCommand, storm::exceptions::WrongFormatException, "Discrete-time model must not have Markovian commands.");
+            } else if (this->getModelType() == Program::ModelType::CTMC) {
+                STORM_LOG_THROW(!hasProbabilisticCommand, storm::exceptions::WrongFormatException, "The input model is a CTMC, but uses probabilistic commands like they are used in PRISM. Please use Markovian commands instead or turn on the PRISM compatibility mode using the appropriate flag.");
+            }
+            
             // Now check the reward models.
             for (auto const& rewardModel : this->getRewardModels()) {
                 for (auto const& stateReward : rewardModel.getStateRewards()) {

test/performance/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp

@@ -8,7 +8,7 @@
 #include "src/settings/SettingMemento.h"
 #include "src/parser/AutoParser.h"
 
-TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, AsynchronousLeader) {
+TEST(DISABLED_TopologicalValueIterationMdpPrctlModelCheckerTest, AsynchronousLeader) {
     std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.tra", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.lab", "", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.trans.rew")->as<storm::models::sparse::Mdp<double>>();
 
 	ASSERT_EQ(mdp->getNumberOfStates(), 2095783ull);
@@ -77,7 +77,7 @@ TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, AsynchronousLeader) {
 	rewardFormula.reset();
 }
 
-TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, Consensus) {
+TEST(DISABLED_TopologicalValueIterationMdpPrctlModelCheckerTest, Consensus) {
     // Increase the maximal number of iterations, because the solver does not converge otherwise.
 	// This is done in the main cpp unit