Browse Source

Merge branch 'jani_support' of https://sselab.de/lab9/private/git/storm into jani_support

Former-commit-id: b7300b76ad [formerly 79ad42583f]
Former-commit-id: 67f478266b
tempestpy_adaptions
sjunges 8 years ago
parent
commit
8a34ed3280
  1. 2
      examples/pdtmc/die.pm
  2. 19
      src/storage/jani/JSONExporter.cpp

2
examples/pdtmc/die.pm

@ -16,7 +16,7 @@ module die
[] s=2 -> q : (s'=5) + 1-q : (s'=6);
[] s=3 -> p : (s'=1) + 1-p : (s'=7) & (d'=1);
[] s=4 -> p : (s'=7) & (d'=3) + 1-p : (s'=7) & (d'=2);
[] s=5 -> p : (s'=2) + 1-p : (s'=7) & (d'=6);
[] s=5 -> p : (s'=2) + 1-p : (s'=7) & (d'=4);
[] s=6 -> p : (s'=7) & (d'=6) + 1-p : (s'=7) & (d'=5);
[] s=7 -> 1: (s'=7);

19
src/storage/jani/JSONExporter.cpp

@ -60,11 +60,7 @@ namespace storm {
for (auto const& subcomp : composition.getSubcompositions()) {
modernjson::json elemDecl;
if (subcomp->isAutomaton()) {
modernjson::json autDecl;
autDecl["automaton"] = std::static_pointer_cast<AutomatonComposition>(subcomp)->getAutomatonName();
std::vector<modernjson::json> elements;
elements.push_back(autDecl);
elemDecl["elements"] = elements;
elemDecl["automaton"] = std::static_pointer_cast<AutomatonComposition>(subcomp)->getAutomatonName();
} else {
STORM_LOG_THROW(allowRecursion, storm::exceptions::InvalidJaniException, "Nesting composition " << *subcomp << " is not supported by JANI.");
elemDecl = boost::any_cast<modernjson::json>(subcomp->accept(*this, boost::none));
@ -75,7 +71,14 @@ namespace storm {
std::vector<modernjson::json> synElems;
for (auto const& syncs : composition.getSynchronizationVectors()) {
modernjson::json syncDecl;
syncDecl["synchronise"] = syncs.getInput();
syncDecl["synchronise"] = std::vector<std::string>();
for (auto const& syncIn : syncs.getInput()) {
if (syncIn == SynchronizationVector::NO_ACTION_INPUT) {
syncDecl["synchronise"].push_back(nullptr);
} else {
syncDecl["synchronise"].push_back(syncIn);
}
}
syncDecl["result"] = syncs.getOutput();
synElems.push_back(syncDecl);
}
@ -691,10 +694,14 @@ namespace storm {
jsonStruct["restrict-initial"]["exp"] = buildExpression(janiModel.getInitialStatesRestriction());
jsonStruct["automata"] = buildAutomataArray(janiModel.getAutomata(), janiModel.getActionIndexToNameMap());
jsonStruct["system"] = CompositionJsonExporter::translate(janiModel.getSystemComposition());
std::vector<std::string> standardFeatureVector = {"derived-operators"};
jsonStruct["features"] = standardFeatureVector;
}
std::string janiFilterTypeString(storm::modelchecker::FilterType const& ft) {
switch(ft) {
case storm::modelchecker::FilterType::MIN:

Loading…
Cancel
Save