From 2905c010d20ed4343f53c381124b5676e45009ec Mon Sep 17 00:00:00 2001 From: sjunges Date: Thu, 22 Sep 2016 16:05:47 +0200 Subject: [PATCH] updated parser: sync result optional, invariant is called differently now Former-commit-id: a5b829c3f763e6522e7513132d721e0b9f9571bd [formerly 72050e32b0c9a679ded9630e633ba0668d5ed026] Former-commit-id: dc6851e733ae3a09f34ed62b533240c11b8061c4 --- src/builder/DdJaniModelBuilder.cpp | 4 +- src/parser/JaniParser.cpp | 39 +++++++------------ .../jani/CompositionInformationVisitor.cpp | 4 +- src/storage/jani/Model.cpp | 2 +- src/storage/jani/ParallelComposition.cpp | 24 ++++++------ src/storage/jani/ParallelComposition.h | 7 ++-- src/storm-pgcl.cpp | 1 - 7 files changed, 34 insertions(+), 47 deletions(-) diff --git a/src/builder/DdJaniModelBuilder.cpp b/src/builder/DdJaniModelBuilder.cpp index 2425f3400..889c5439b 100644 --- a/src/builder/DdJaniModelBuilder.cpp +++ b/src/builder/DdJaniModelBuilder.cpp @@ -646,14 +646,14 @@ namespace storm { for (auto const& synchVector : composition.getSynchronizationVectors()) { auto it = actionIndexToLocalNondeterminismVariableOffset.find(actionInformation.getActionIndex(synchVector.getOutput())); STORM_LOG_THROW(it != actionIndexToLocalNondeterminismVariableOffset.end(), storm::exceptions::InvalidArgumentException, "Invalid action " << synchVector.getOutput() << "."); - if (synchVector.getInput(0) != storm::jani::SynchronizationVector::getNoActionInput()) { + if (synchVector.getInput(0) != storm::jani::SynchronizationVector::NO_ACTION_INPUT) { newSynchronizingActionToOffsetMap[actionInformation.getActionIndex(synchVector.getInput(0))] = it->second; } } } else { // Based on the previous results, we need to update the offsets. for (auto const& synchVector : composition.getSynchronizationVectors()) { - if (synchVector.getInput(subcompositionIndex) != storm::jani::SynchronizationVector::getNoActionInput()) { + if (synchVector.getInput(subcompositionIndex) != storm::jani::SynchronizationVector::NO_ACTION_INPUT) { boost::optional previousActionPosition = synchVector.getPositionOfPrecedingParticipatingAction(subcompositionIndex); if (previousActionPosition) { AutomatonDd const& previousAutomatonDd = subautomata[previousActionPosition.get()]; diff --git a/src/parser/JaniParser.cpp b/src/parser/JaniParser.cpp index 343f8e2ce..6a5d2a2bb 100644 --- a/src/parser/JaniParser.cpp +++ b/src/parser/JaniParser.cpp @@ -153,28 +153,7 @@ namespace storm { } if (constantStructure.at("type").is_object()) { -// STORM_LOG_THROW(variableStructure.at("type").count("kind") == 1, storm::exceptions::InvalidJaniException, "For complex type as in variable " << name << "(scope: " << scopeDescription << ") kind must be given"); -// std::string kind = getString(variableStructure.at("type").at("kind"), "kind for complex type as in variable " + name + "(scope: " + scopeDescription + ") "); -// if(kind == "bounded") { -// // First do the bounds, that makes the code a bit more streamlined -// STORM_LOG_THROW(variableStructure.at("type").count("lower-bound") == 1, storm::exceptions::InvalidJaniException, "For bounded type as in variable " << name << "(scope: " << scopeDescription << ") lower-bound must be given"); -// storm::expressions::Expression lowerboundExpr = parseExpression(variableStructure.at("type").at("lower-bound"), "Lower bound for variable "+ name + " (scope: " + scopeDescription + ")"); -// assert(lowerboundExpr.isInitialized()); -// STORM_LOG_THROW(variableStructure.at("type").count("upper-bound") == 1, storm::exceptions::InvalidJaniException, "For bounded type as in variable " << name << "(scope: " << scopeDescription << ") upper-bound must be given"); -// storm::expressions::Expression upperboundExpr = parseExpression(variableStructure.at("type").at("upper-bound"), "Upper bound for variable "+ name + " (scope: " + scopeDescription + ")"); -// assert(upperboundExpr.isInitialized()); -// STORM_LOG_THROW(variableStructure.at("type").count("base") == 1, storm::exceptions::InvalidJaniException, "For bounded type as in variable " << name << "(scope: " << scopeDescription << ") base must be given"); -// std::string basictype = getString(variableStructure.at("type").at("base"), "base for bounded type as in variable " + name + "(scope: " + scopeDescription + ") "); -// if(basictype == "int") { -// STORM_LOG_THROW(lowerboundExpr.hasIntegerType(), storm::exceptions::InvalidJaniException, "Lower bound for bounded integer variable " << name << "(scope: " << scopeDescription << ") must be integer-typed"); -// STORM_LOG_THROW(upperboundExpr.hasIntegerType(), storm::exceptions::InvalidJaniException, "Upper bound for bounded integer variable " << name << "(scope: " << scopeDescription << ") must be integer-typed"); -// return std::make_shared(name, expressionManager->declareIntegerVariable(exprManagerName), lowerboundExpr, upperboundExpr); -// } else { -// STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unsupported base " << basictype << " for bounded variable " << name << "(scope: " << scopeDescription << ") "); -// } -// } else { -// STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unsupported kind " << kind << " for complex type of variable " << name << "(scope: " << scopeDescription << ") "); -// } + } else if(constantStructure.at("type").is_string()) { if(constantStructure.at("type") == "real") { @@ -231,10 +210,11 @@ namespace storm { expressionManager->declareRationalVariable(name); if(initvalcount == 1) { if(variableStructure.at("initial-value").is_null()) { + STORM_LOG_WARN("Deprecated null value in initial value"); initVal = expressionManager->rational(defaultRationalInitialValue); } else { initVal = parseExpression(variableStructure.at("initial-value"), "Initial value for variable " + name + " (scope: " + scopeDescription + ") "); - STORM_LOG_THROW(initVal.get().hasRationalType(), storm::exceptions::InvalidJaniException, "Initial value for integer variable " + name + "(scope " + scopeDescription + ") should be a rational"); + STORM_LOG_THROW(initVal.get().hasRationalType() || initVal.get().hasIntegerType(), storm::exceptions::InvalidJaniException, "Initial value for rational variable " + name + "(scope " + scopeDescription + ") should be a rational"); } return std::make_shared(name, expressionManager->declareRationalVariable(exprManagerName), initVal.get(), transientVar); @@ -243,6 +223,7 @@ namespace storm { } else if(variableStructure.at("type") == "bool") { if(initvalcount == 1) { if(variableStructure.at("initial-value").is_null()) { + STORM_LOG_WARN("Deprecated null value in initial value"); initVal = expressionManager->boolean(defaultBooleanInitialValue); } else { initVal = parseExpression(variableStructure.at("initial-value"), "Initial value for variable " + name + " (scope: " + scopeDescription + ") "); @@ -254,6 +235,7 @@ namespace storm { } else if(variableStructure.at("type") == "int") { if(initvalcount == 1) { if(variableStructure.at("initial-value").is_null()) { + STORM_LOG_WARN("Deprecated null value in initial value"); initVal = expressionManager->integer(defaultIntegerInitialValue); } else { initVal = parseExpression(variableStructure.at("initial-value"), "Initial value for variable " + name + " (scope: " + scopeDescription + ") "); @@ -582,7 +564,7 @@ namespace storm { STORM_LOG_THROW(locEntry.count("name") == 1, storm::exceptions::InvalidJaniException, "Locations for automaton '" << name << "' must have exactly one name"); std::string locName = getString(locEntry.at("name"), "location of automaton " + name); STORM_LOG_THROW(locIds.count(locName) == 0, storm::exceptions::InvalidJaniException, "Location with name '" + locName + "' already exists in automaton '" + name + "'"); - STORM_LOG_THROW(locEntry.count("invariant") == 0, storm::exceptions::InvalidJaniException, "Invariants in locations as in '" + locName + "' in automaton '" + name + "' are not supported"); + STORM_LOG_THROW(locEntry.count("time-progress") == 0, storm::exceptions::InvalidJaniException, "Time progress conditions in locations as in '" + locName + "' in automaton '" + name + "' are not supported"); //STORM_LOG_THROW(locEntry.count("invariant") > 0 && !supportsInvariants(parentModel.getModelType()), storm::exceptions::InvalidJaniException, "Invariants are not supported in the model type " + to_string(parentModel.getModelType())); std::vector transientAssignments; for(auto const& transientValueEntry : locEntry.at("transient-values")) { @@ -734,8 +716,13 @@ namespace storm { inputs.push_back(syncInput); } } - std::string syncResult = syncEntry.at("result"); - syncVectors.emplace_back(inputs, syncResult); + if (syncEntry.count("result") > 0) { + std::string syncResult = syncEntry.at("result"); + syncVectors.emplace_back(inputs, syncResult); + } else { + syncVectors.emplace_back(inputs); + } + } } diff --git a/src/storage/jani/CompositionInformationVisitor.cpp b/src/storage/jani/CompositionInformationVisitor.cpp index 5f6a08839..d2635c882 100644 --- a/src/storage/jani/CompositionInformationVisitor.cpp +++ b/src/storage/jani/CompositionInformationVisitor.cpp @@ -152,7 +152,7 @@ namespace storm { std::set actionsInSynch; for (uint64_t synchVectorIndex = 0; synchVectorIndex < composition.getNumberOfSynchronizationVectors(); ++synchVectorIndex) { auto const& synchVector = composition.getSynchronizationVector(synchVectorIndex); - if (synchVector.getInput(infoIndex) != SynchronizationVector::getNoActionInput()) { + if (synchVector.getInput(infoIndex) != SynchronizationVector::NO_ACTION_INPUT) { for (auto const& nonSilentActionIndex : subinfo.getNonSilentActionIndices()) { std::string const& nonSilentAction = indexToNameMap.at(nonSilentActionIndex); if (synchVector.getInput(infoIndex) == nonSilentAction) { @@ -201,7 +201,7 @@ namespace storm { input.push_back(actionName); ++numberOfParticipatingAutomata; } else { - input.push_back(SynchronizationVector::getNoActionInput()); + input.push_back(SynchronizationVector::NO_ACTION_INPUT); } } diff --git a/src/storage/jani/Model.cpp b/src/storage/jani/Model.cpp index bfad5d8a8..56e07c226 100644 --- a/src/storage/jani/Model.cpp +++ b/src/storage/jani/Model.cpp @@ -246,7 +246,7 @@ namespace storm { ++numberOfParticipatingAutomata; synchVectorInputs.push_back(actionName); } else { - synchVectorInputs.push_back(storm::jani::SynchronizationVector::getNoActionInput()); + synchVectorInputs.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT); } ++i; } diff --git a/src/storage/jani/ParallelComposition.cpp b/src/storage/jani/ParallelComposition.cpp index 374eee402..597518d37 100644 --- a/src/storage/jani/ParallelComposition.cpp +++ b/src/storage/jani/ParallelComposition.cpp @@ -6,16 +6,21 @@ #include "src/utility/macros.h" #include "src/exceptions/WrongFormatException.h" +#include "src/storage/jani/Model.h" namespace storm { namespace jani { - const std::string SynchronizationVector::noAction = "-"; + const std::string SynchronizationVector::NO_ACTION_INPUT = "-"; SynchronizationVector::SynchronizationVector(std::vector const& input, std::string const& output) : input(input), output(output) { // Intentionally left empty. } + SynchronizationVector::SynchronizationVector(std::vector const& input) : input(input), output(storm::jani::Model::SILENT_ACTION_NAME) { + + } + std::size_t SynchronizationVector::size() const { return input.size(); } @@ -27,11 +32,6 @@ namespace storm { std::string const& SynchronizationVector::getInput(uint64_t index) const { return input[index]; } - - std::string const& SynchronizationVector::getNoActionInput() { - return SynchronizationVector::noAction; - } - std::string const& SynchronizationVector::getOutput() const { return output; } @@ -52,13 +52,13 @@ namespace storm { uint64_t i = index - 1; for (; i > 0; --i) { - if (this->getInput(i) != SynchronizationVector::getNoActionInput()) { + if (this->getInput(i) != NO_ACTION_INPUT) { return boost::make_optional(i); } } // Check the 0-index. - if (this->getInput(i) != SynchronizationVector::getNoActionInput()) { + if (this->getInput(i) != NO_ACTION_INPUT) { return boost::make_optional(i); } @@ -67,7 +67,7 @@ namespace storm { uint64_t SynchronizationVector::getPositionOfFirstParticipatingAction() const { for (uint64_t result = 0; result < this->size(); ++result) { - if (this->getInput(result) != getNoActionInput()) { + if (this->getInput(result) != NO_ACTION_INPUT) { return result; } } @@ -75,7 +75,7 @@ namespace storm { } bool SynchronizationVector::isNoActionInput(std::string const& action) { - return action == noAction; + return action == NO_ACTION_INPUT; } std::ostream& operator<<(std::ostream& stream, SynchronizationVector const& synchronizationVector) { @@ -181,7 +181,7 @@ namespace storm { for (auto const& vector : synchronizationVectors) { STORM_LOG_THROW(vector.size() == this->subcompositions.size(), storm::exceptions::WrongFormatException, "Synchronization vectors must match parallel composition size."); std::string const& action = vector.getInput(inputIndex); - if (action != SynchronizationVector::getNoActionInput()) { + if (action != SynchronizationVector::NO_ACTION_INPUT) { STORM_LOG_THROW(actions.find(action) == actions.end(), storm::exceptions::WrongFormatException, "Cannot use the same action multiple times as input in synchronization vectors."); actions.insert(action); } @@ -191,7 +191,7 @@ namespace storm { for (auto const& vector : synchronizationVectors) { bool hasInput = false; for (auto const& input : vector.getInput()) { - if (input != SynchronizationVector::getNoActionInput()) { + if (input != SynchronizationVector::NO_ACTION_INPUT) { hasInput = true; break; } diff --git a/src/storage/jani/ParallelComposition.h b/src/storage/jani/ParallelComposition.h index 4cd62587d..b6ae63fdd 100644 --- a/src/storage/jani/ParallelComposition.h +++ b/src/storage/jani/ParallelComposition.h @@ -15,13 +15,13 @@ namespace storm { class SynchronizationVector { public: SynchronizationVector(std::vector const& input, std::string const& output); + SynchronizationVector(std::vector const& input); std::size_t size() const; std::vector const& getInput() const; std::string const& getInput(uint64_t index) const; std::string const& getOutput() const; - static std::string const& getNoActionInput(); static bool isNoActionInput(std::string const& action); /*! @@ -41,10 +41,11 @@ namespace storm { */ uint64_t getPositionOfFirstParticipatingAction() const; - private: + // A marker that can be used as one of the inputs. The semantics is that no action of the corresponding // automaton takes part in the synchronization. - static const std::string noAction; + static const std::string NO_ACTION_INPUT; + private: /// The input to the synchronization. std::vector input; diff --git a/src/storm-pgcl.cpp b/src/storm-pgcl.cpp index b9d97b391..729e12588 100644 --- a/src/storm-pgcl.cpp +++ b/src/storm-pgcl.cpp @@ -35,7 +35,6 @@ void initializeSettings() { } int handleJani(storm::jani::Model& model) { - if (!storm::settings::getModule().isJaniFileSet()) { // For now, we have to have a jani file storm::jani::JsonExporter::toStream(model, std::cout);