JANI next-state generator appears to be working (without rewards)

Former-commit-id: 3ca5c3ccf2

src/generator/JaniNextStateGenerator.cpp

@@ -22,7 +22,7 @@ namespace storm {
         
         template<typename ValueType, typename StateType>
         JaniNextStateGenerator<ValueType, StateType>::JaniNextStateGenerator(storm::jani::Model const& model, NextStateGeneratorOptions const& options, bool flag) : NextStateGenerator<ValueType, StateType>(model.getExpressionManager(), VariableInformation(model), options), model(model) {
-            STORM_LOG_THROW(!model.hasDefaultComposition(), storm::exceptions::WrongFormatException, "The explicit next-state generator currently does not support custom system compositions.");
+            STORM_LOG_THROW(model.hasDefaultComposition(), storm::exceptions::WrongFormatException, "The explicit next-state generator currently does not support custom system compositions.");
             STORM_LOG_THROW(!this->options.isBuildAllRewardModelsSet() && this->options.getRewardModelNames().empty(), storm::exceptions::InvalidSettingsException, "The explicit next-state generator currently does not support building reward models.");
             STORM_LOG_THROW(!this->options.isBuildChoiceLabelsSet(), storm::exceptions::InvalidSettingsException, "JANI next-state generator cannot generate choice labels.");
             
@@ -125,12 +125,21 @@ namespace storm {
                 
                 // Gather iterators to the initial locations of all the automata.
                 std::vector<std::set<uint64_t>::const_iterator> initialLocationsIterators;
+                uint64_t currentLocationVariable = 0;
                 for (auto const& automaton : this->model.getAutomata()) {
                     initialLocationsIterators.push_back(automaton.getInitialLocationIndices().cbegin());
+                    
+                    // Initialize the locations to the first possible combination.
+                    setLocation(initialState, this->variableInformation.locationVariables[currentLocationVariable], *initialLocationsIterators.back());
+                    ++currentLocationVariable;
                 }
                 
                 // Now iterate through all combinations of initial locations.
                 while (true) {
+                    // Register initial state.
+                    StateType id = stateToIdCallback(initialState);
+                    initialStateIndices.push_back(id);
+                    
                     uint64_t index = 0;
                     for (; index < initialLocationsIterators.size(); ++index) {
                         ++initialLocationsIterators[index];
@@ -145,11 +154,9 @@ namespace storm {
                     if (index == initialLocationsIterators.size()) {
                         break;
                     } else {
-                        setLocation(initialState, this->variableInformation.locationVariables[index], *initialLocationsIterators[index]);
-
-                        // Register initial state and return it.
-                        StateType id = stateToIdCallback(initialState);
-                        initialStateIndices.push_back(id);
+                        for (uint64_t j = 0; j <= index; ++j) {
+                            setLocation(initialState, this->variableInformation.locationVariables[j], *initialLocationsIterators[j]);
+                        }
                     }
                 }
                 
@@ -178,7 +185,7 @@ namespace storm {
                 while (assignmentIt->getExpressionVariable() != boolIt->variable) {
                     ++boolIt;
                 }
-                newState.set(boolIt->bitOffset, this->evaluator.asBool(assignmentIt->getExpressionVariable()));
+                newState.set(boolIt->bitOffset, this->evaluator.asBool(assignmentIt->getAssignedExpression()));
             }
             
             // Iterate over all integer assignments and carry them out.
@@ -427,7 +434,6 @@ namespace storm {
                 }
                 
                 std::vector<storm::jani::Edge const*> edgePointers;
-                edgePointers.reserve(edges.size());
                 for (auto const& edge : edges) {
                     if (this->evaluator.asBool(edge.getGuard())) {
                         edgePointers.push_back(&edge);
@@ -436,7 +442,7 @@ namespace storm {
                 
                 // If there was no enabled edge although the automaton has some edge with the required action, we must
                 // not return anything.
-                if (edgePointers.size() == 0) {
+                if (edgePointers.empty()) {
                     return std::vector<std::vector<storm::jani::Edge const*>>();
                 }
                 

src/generator/VariableInformation.cpp

@@ -50,7 +50,7 @@ namespace storm {
             sortVariables();
         }
         
-        VariableInformation::VariableInformation(storm::jani::Model const& model) {
+        VariableInformation::VariableInformation(storm::jani::Model const& model) : totalBitOffset(0) {
             for (auto const& variable : model.getGlobalVariables().getBooleanVariables()) {
                 booleanVariables.emplace_back(variable.getExpressionVariable(), totalBitOffset);
                 ++totalBitOffset;

src/storage/jani/Automaton.cpp

@@ -114,7 +114,7 @@ namespace storm {
             initialLocationIndices.insert(index);
         }
         
-        std::set<uint64_t> Automaton::getInitialLocationIndices() const {
+        std::set<uint64_t> const& Automaton::getInitialLocationIndices() const {
             return initialLocationIndices;
         }
 
@@ -170,14 +170,15 @@ namespace storm {
                     count = step;
                 }
             }
-            
+            it1 = first;
+
             // If there is no such edge, we can return now.
             if (it1 != last && it1->getActionIndex() > actionIndex) {
                 return Edges(last, last);
             }
             
             // Otherwise, perform a binary search for the end of the edges with the given action index.
-            count = std::distance(first,last);
+            count = std::distance(it1,last);
             
             ForwardIt it2;
             while (count > 0) {
@@ -189,6 +190,7 @@ namespace storm {
                     count -= step + 1;
                 } else count = step;
             }
+            it2 = first;
             
             return Edges(it1, it2);
         }
@@ -217,6 +219,7 @@ namespace storm {
                     count = step;
                 }
             }
+            it1 = first;
             
             // If there is no such edge, we can return now.
             if (it1 != last && it1->getActionIndex() > actionIndex) {
@@ -224,11 +227,11 @@ namespace storm {
             }
             
             // Otherwise, perform a binary search for the end of the edges with the given action index.
-            count = std::distance(first,last);
+            count = std::distance(it1,last);
             
             ForwardIt it2;
             while (count > 0) {
-                it2 = it1;
+                it2 = first;
                 step = count / 2;
                 std::advance(it2, step);
                 if (!(actionIndex < it2->getActionIndex())) {
@@ -236,6 +239,7 @@ namespace storm {
                     count -= step + 1;
                 } else count = step;
             }
+            it2 = first;
             
             return ConstEdges(it1, it2);
         }

src/storage/jani/Automaton.h

@@ -164,7 +164,7 @@ namespace storm {
             /*!
              * Retrieves the indices of the initial locations.
              */
-            std::set<uint64_t> getInitialLocationIndices() const;
+            std::set<uint64_t> const& getInitialLocationIndices() const;
 
             /*!
              * Retrieves the edges of the location with the given name.

src/storage/jani/CompositionInformationVisitor.cpp

@@ -6,6 +6,10 @@
 namespace storm {
     namespace jani {
         
+        CompositionInformation::CompositionInformation() : automatonNameToMultiplicity(), nonsilentActions(), renameComposition(false), restrictedParallelComposition(false) {
+            // Intentionally left empty.
+        }
+        
         CompositionInformation::CompositionInformation(std::map<std::string, uint64_t> const& automatonNameToMultiplicity, std::set<std::string> const& nonsilentActions, bool containsRenameComposition, bool containsRestrictedParallelComposition) : automatonNameToMultiplicity(automatonNameToMultiplicity), nonsilentActions(nonsilentActions), renameComposition(containsRenameComposition), restrictedParallelComposition(containsRestrictedParallelComposition) {
             // Intentionally left empty.
         }
@@ -105,9 +109,8 @@ namespace storm {
             if (!containsRestrictedParallelComposition) {
                 std::set<std::string> commonNonsilentActions;
                 std::set_intersection(left.getNonsilentActions().begin(), left.getNonsilentActions().end(), right.getNonsilentActions().begin(), right.getNonsilentActions().end(), std::inserter(commonNonsilentActions, commonNonsilentActions.begin()));
-                if (commonNonsilentActions != composition.getSynchronizationAlphabet()) {
-                    containsRestrictedParallelComposition = true;
-                }
+                bool allCommonActionsIncluded = std::includes(commonNonsilentActions.begin(), commonNonsilentActions.end(), composition.getSynchronizationAlphabet().begin(), composition.getSynchronizationAlphabet().end());
+                containsRestrictedParallelComposition = !allCommonActionsIncluded;
             }
             
             return CompositionInformation(joinedAutomatonToMultiplicity, nonsilentActions, containsRenameComposition, containsRestrictedParallelComposition);

src/storage/jani/CompositionInformationVisitor.h

@@ -15,7 +15,7 @@ namespace storm {
         
         class CompositionInformation {
         public:
-            CompositionInformation() = default;
+            CompositionInformation();
             CompositionInformation(std::map<std::string, uint64_t> const& automatonNameToMultiplicity, std::set<std::string> const& nonsilentActions, bool containsRenaming, bool containsRestrictedParallelComposition);
 
             void increaseAutomatonMultiplicity(std::string const& automatonName, uint64_t count = 1);

src/storage/prism/CompositionToJaniVisitor.cpp

@@ -0,0 +1,66 @@
+#include "src/storage/prism/CompositionToJaniVisitor.h"
+#include "src/storage/prism/Compositions.h"
+
+#include "src/storage/jani/Compositions.h"
+#include "src/storage/jani/Model.h"
+
+namespace storm {
+    namespace prism {
+        
+        std::shared_ptr<storm::jani::Composition> CompositionToJaniVisitor::toJani(Composition const& composition, storm::jani::Model const& model) {
+            return boost::any_cast<std::shared_ptr<storm::jani::Composition>>(composition.accept(*this, model));
+        }
+        
+        boost::any CompositionToJaniVisitor::visit(ModuleComposition const& composition, boost::any const& data) {
+            std::shared_ptr<storm::jani::Composition> result = std::make_shared<storm::jani::AutomatonComposition>(composition.getModuleName());
+            return result;
+        }
+        
+        boost::any CompositionToJaniVisitor::visit(RenamingComposition const& composition, boost::any const& data) {
+            std::map<std::string, boost::optional<std::string>> newRenaming;
+            for (auto const& renamingPair : composition.getActionRenaming()) {
+                newRenaming.emplace(renamingPair.first, renamingPair.second);
+            }
+            auto subcomposition = boost::any_cast<std::shared_ptr<storm::jani::Composition>>(composition.getSubcomposition().accept(*this, data));
+            std::shared_ptr<storm::jani::Composition> result = std::make_shared<storm::jani::RenameComposition>(subcomposition, newRenaming);
+            return result;
+        }
+        
+        boost::any CompositionToJaniVisitor::visit(HidingComposition const& composition, boost::any const& data) {
+            std::map<std::string, boost::optional<std::string>> newRenaming;
+            for (auto const& action : composition.getActionsToHide()) {
+                newRenaming.emplace(action, boost::none);
+            }
+            auto subcomposition = boost::any_cast<std::shared_ptr<storm::jani::Composition>>(composition.getSubcomposition().accept(*this, data));
+            std::shared_ptr<storm::jani::Composition> result = std::make_shared<storm::jani::RenameComposition>(subcomposition, newRenaming);
+            return result;
+        }
+        
+        boost::any CompositionToJaniVisitor::visit(SynchronizingParallelComposition const& composition, boost::any const& data) {
+            auto leftSubcomposition = boost::any_cast<std::shared_ptr<storm::jani::Composition>>(composition.getLeftSubcomposition().accept(*this, data));
+            auto rightSubcomposition = boost::any_cast<std::shared_ptr<storm::jani::Composition>>(composition.getRightSubcomposition().accept(*this, data));
+            
+            storm::jani::Model const& model = boost::any_cast<storm::jani::Model const&>(data);
+            std::set<std::string> allActions;
+            for (auto const& action : model.getActions()) {
+                allActions.insert(action.getName());
+            }
+            std::shared_ptr<storm::jani::Composition> result = std::make_shared<storm::jani::ParallelComposition>(leftSubcomposition, rightSubcomposition, allActions);
+            return result;
+        }
+        
+        boost::any CompositionToJaniVisitor::visit(InterleavingParallelComposition const& composition, boost::any const& data) {
+            auto leftSubcomposition = boost::any_cast<std::shared_ptr<storm::jani::Composition>>(composition.getLeftSubcomposition().accept(*this, data));
+            auto rightSubcomposition = boost::any_cast<std::shared_ptr<storm::jani::Composition>>(composition.getRightSubcomposition().accept(*this, data));
+            std::shared_ptr<storm::jani::Composition> result = std::make_shared<storm::jani::ParallelComposition>(leftSubcomposition, rightSubcomposition, std::set<std::string>());
+            return result;
+        }
+        
+        boost::any CompositionToJaniVisitor::visit(RestrictedParallelComposition const& composition, boost::any const& data) {
+            auto leftSubcomposition = boost::any_cast<std::shared_ptr<storm::jani::Composition>>(composition.getLeftSubcomposition().accept(*this, data));
+            auto rightSubcomposition = boost::any_cast<std::shared_ptr<storm::jani::Composition>>(composition.getRightSubcomposition().accept(*this, data));
+            std::shared_ptr<storm::jani::Composition> result = std::make_shared<storm::jani::ParallelComposition>(leftSubcomposition, rightSubcomposition, composition.getSynchronizingActions());
+            return result;
+        }
+    }
+}

src/storage/prism/CompositionToJaniVisitor.h

@@ -0,0 +1,29 @@
+#pragma once
+
+#include <memory>
+
+#include "src/storage/prism/CompositionVisitor.h"
+
+namespace storm {
+    namespace jani {
+        class Composition;
+        class Model;
+    }
+    
+    namespace prism {
+        class Composition;
+        
+        class CompositionToJaniVisitor : public CompositionVisitor {
+        public:
+            std::shared_ptr<storm::jani::Composition> toJani(Composition const& composition, storm::jani::Model const& model);
+            
+            virtual boost::any visit(ModuleComposition const& composition, boost::any const& data) override;
+            virtual boost::any visit(RenamingComposition const& composition, boost::any const& data) override;
+            virtual boost::any visit(HidingComposition const& composition, boost::any const& data) override;
+            virtual boost::any visit(SynchronizingParallelComposition const& composition, boost::any const& data) override;
+            virtual boost::any visit(InterleavingParallelComposition const& composition, boost::any const& data) override;
+            virtual boost::any visit(RestrictedParallelComposition const& composition, boost::any const& data) override;
+        };
+        
+    }
+}

src/storage/prism/Program.cpp

@@ -20,6 +20,7 @@
 
 #include "src/storage/prism/CompositionVisitor.h"
 #include "src/storage/prism/Compositions.h"
+#include "src/storage/prism/CompositionToJaniVisitor.h"
 
 namespace storm {
     namespace prism {
@@ -1510,8 +1511,6 @@ namespace storm {
         }
         
         storm::jani::Model Program::toJani(bool allVariablesGlobal) const {
-            STORM_LOG_THROW(!this->specifiesSystemComposition(), storm::exceptions::InvalidOperationException, "Cannot translate PRISM program with custom system composition to JANI.");
-            
             // Start by creating an empty JANI model.
             storm::jani::ModelType modelType;
             switch (this->getModelType()) {
@@ -1659,7 +1658,12 @@ namespace storm {
             janiModel.setInitialStatesExpression(globalInitialStatesExpression);
             
             // Set the standard system composition. This is possible, because we reject non-standard compositions anyway.
-            janiModel.setSystemComposition(janiModel.getStandardSystemComposition());
+            if (this->specifiesSystemComposition()) {
+                CompositionToJaniVisitor visitor;
+                janiModel.setSystemComposition(visitor.toJani(this->getSystemCompositionConstruct().getSystemComposition(), janiModel));
+            } else {
+                janiModel.setSystemComposition(janiModel.getStandardSystemComposition());
+            }
             
             return janiModel;
         }

test/functional/permissiveschedulers/SmtPermissiveSchedulerTest.cpp

@@ -11,7 +11,7 @@
 #include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h"
 
 
-#ifdef STORM_HAVE_MSAT
+#if defined(STORM_HAVE_MSAT) || defined(STORM_HAVE_Z3)
 
 TEST(SmtPermissiveSchedulerTest, DieSelection) {
     storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die_c1.nm");
@@ -25,11 +25,7 @@ TEST(SmtPermissiveSchedulerTest, DieSelection) {
     auto formula001b = formulaParser.parseSingleFormulaFromString("P<=0.05 [ F \"one\"]")->asProbabilityOperatorFormula();
     
     // Customize and perform model-building.
-    typename storm::builder::ExplicitModelBuilder<double>::Options options;
-    
-    options = typename storm::builder::ExplicitModelBuilder<double>::Options(formula02b);
-    options.addConstantDefinitionsFromString(program, "");
-    options.buildCommandLabels = true;
+    storm::generator::NextStateGeneratorOptions options(formula02b);
     
     std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = storm::builder::ExplicitModelBuilder<double>(program, options).build()->as<storm::models::sparse::Mdp<double>>();
     
@@ -62,4 +58,4 @@ TEST(SmtPermissiveSchedulerTest, DieSelection) {
     
 }
 
-#endif // STORM_HAVE_MSAT
+#endif // STORM_HAVE_MSAT || STORM_HAVE_Z3