sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

updated parser: sync result optional, invariant is called differently now 

Former-commit-id: a5b829c3f7 [formerly 72050e32b0]
Former-commit-id: dc6851e733
main
sjunges 9 years ago
parent
cacbc64871
commit
2905c010d2
7 changed files with 34 additions and 47 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 4
      src/builder/DdJaniModelBuilder.cpp
  2. 35
      src/parser/JaniParser.cpp
  3. 4
      src/storage/jani/CompositionInformationVisitor.cpp
  4. 2
      src/storage/jani/Model.cpp
  5. 24
      src/storage/jani/ParallelComposition.cpp
  6. 7
      src/storage/jani/ParallelComposition.h
  7. 1
      src/storm-pgcl.cpp

4
src/builder/DdJaniModelBuilder.cpp
View File

@ -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<uint64_t> previousActionPosition = synchVector.getPositionOfPrecedingParticipatingAction(subcompositionIndex);
if (previousActionPosition) {
AutomatonDd const& previousAutomatonDd = subautomata[previousActionPosition.get()];

35
src/parser/JaniParser.cpp
View File

@ -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<storm::jani::BoundedIntegerVariable>(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<storm::jani::RealVariable>(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<storm::jani::Assignment> transientAssignments;
for(auto const& transientValueEntry : locEntry.at("transient-values")) {
@ -734,8 +716,13 @@ namespace storm {
inputs.push_back(syncInput);
}
}
if (syncEntry.count("result") > 0) {
std::string syncResult = syncEntry.at("result");
syncVectors.emplace_back(inputs, syncResult);
} else {
syncVectors.emplace_back(inputs);
}
}
}

4
src/storage/jani/CompositionInformationVisitor.cpp
View File

@ -152,7 +152,7 @@ namespace storm {
std::set<uint64_t> 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);
}
}

2
src/storage/jani/Model.cpp
View File

@ -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;
}

24
src/storage/jani/ParallelComposition.cpp
View File

@ -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<std::string> const& input, std::string const& output) : input(input), output(output) {
// Intentionally left empty.
}
SynchronizationVector::SynchronizationVector(std::vector<std::string> 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;
}

7
src/storage/jani/ParallelComposition.h
View File

@ -15,13 +15,13 @@ namespace storm {
class SynchronizationVector {
public:
SynchronizationVector(std::vector<std::string> const& input, std::string const& output);
SynchronizationVector(std::vector<std::string> const& input);
std::size_t size() const;
std::vector<std::string> 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<std::string> input;

1
src/storm-pgcl.cpp
View File

@ -35,7 +35,6 @@ void initializeSettings() {
}
int handleJani(storm::jani::Model& model) {
if (!storm::settings::getModule<storm::settings::modules::JaniExportSettings>().isJaniFileSet()) {
// For now, we have to have a jani file
storm::jani::JsonExporter::toStream(model, std::cout);

Write Preview
Loading…
Cancel
Save