From c812d950a5cbd7f7aadf85f76d11352e4675cb67 Mon Sep 17 00:00:00 2001 From: sjunges Date: Thu, 11 Aug 2016 15:34:43 +0200 Subject: [PATCH] restrict-initial support & error message for invariants Former-commit-id: 2940a8c6750493efe102e9b4d96fec7080489cc4 [formerly f9fc0f967d30011f0aa18e1f5662f8dbaebe373c] Former-commit-id: 63a5c9e844b1ae5232eae085f8ea824d1d48a7a1 --- src/parser/JaniParser.cpp | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/src/parser/JaniParser.cpp b/src/parser/JaniParser.cpp index c4f67d17b..e6854d377 100644 --- a/src/parser/JaniParser.cpp +++ b/src/parser/JaniParser.cpp @@ -564,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 + "' 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")) { @@ -582,6 +582,12 @@ namespace storm { for(json const& initLocStruct : automatonStructure.at("initial-locations")) { automaton.addInitialLocation(getString(initLocStruct, "Initial locations for automaton '" + name + "'.")); } + STORM_LOG_THROW(automatonStructure.count("restrict-initial") < 2, storm::exceptions::InvalidJaniException, "Automaton '" << name << "' has multiple initial value restrictions"); + storm::expressions::Expression initialValueRestriction = expressionManager->boolean(true); + if(automatonStructure.count("restrict-initial") > 0) { + initialValueRestriction = parseExpression(automatonStructure.at("restrict-initial"), "Initial value restriction for automaton " + name); + } + automaton.setInitialStatesExpression(initialValueRestriction); uint64_t varDeclCount = automatonStructure.count("variables"); STORM_LOG_THROW(varDeclCount < 2, storm::exceptions::InvalidJaniException, "Automaton '" << name << "' has more than one list of variables"); std::unordered_map> localVars;