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

updated dft->gspn->jani workflow

main
Sebastian Junges 9 years ago
parent
b9e46cf8c1
commit
88e17d423a
9 changed files with 151 additions and 100 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. 11
      src/storm-dft-cli/storm-dyftee.cpp
  2. 163
      src/storm-gspn/builder/JaniGSPNBuilder.h
  3. 32
      src/storm-gspn/storm-gspn.h
  4. 11
      src/storm/cli/cli.cpp
  5. 2
      src/storm/settings/modules/GSPNExportSettings.h
  6. 9
      src/storm/storage/jani/OrderedAssignments.cpp
  7. 2
      src/storm/storage/jani/OrderedAssignments.h
  8. 11
      src/storm/utility/storm.cpp
  9. 10
      src/storm/utility/storm.h

11
src/storm-dft-cli/storm-dyftee.cpp
View File

@ -22,6 +22,7 @@
#include "storm-dft/settings/modules/DFTSettings.h"
#include "storm-gspn/storage/gspn/GSPN.h"
#include "storm-gspn/storm-gspn.h"
#include "storm/settings/modules/GSPNSettings.h"
#include "storm/settings/modules/GSPNExportSettings.h"
@ -112,6 +113,7 @@ void initializeSettings() {
// For translation into JANI via GSPN.
storm::settings::addModule<storm::settings::modules::GSPNSettings>();
storm::settings::addModule<storm::settings::modules::GSPNExportSettings>();
storm::settings::addModule<storm::settings::modules::JaniExportSettings>();
}
/*!
@ -140,7 +142,16 @@ int main(const int argc, const char** argv) {
if (dftSettings.isTransformToGspn()) {
storm::gspn::GSPN* gspn = transformDFT<double>(dftSettings.getDftFilename());
storm::handleGSPNExportSettings(*gspn);
storm::jani::Model* model = storm::buildJani(*gspn);
storm::settings::modules::JaniExportSettings const& janiSettings = storm::settings::getModule<storm::settings::modules::JaniExportSettings>();
if (janiSettings.isJaniFileSet()) {
storm::exportJaniModel(*model, {}, janiSettings.getJaniFilename());
}
delete model;
delete gspn;
storm::utility::cleanUp();
return 0;

163
src/storm-gspn/builder/JaniGSPNBuilder.h
View File

@ -9,17 +9,15 @@ namespace storm {
class JaniGSPNBuilder {
public:
JaniGSPNBuilder(storm::gspn::GSPN const& gspn, std::shared_ptr<storm::expressions::ExpressionManager> const& expManager) : gspn(gspn), expressionManager(expManager) {
gspn.writeDotToStream(std::cout);
}
virtual ~JaniGSPNBuilder() {
for (auto const& varEntry : vars) {
delete varEntry.second;
}
}
void setIgnoreWeights(bool ignore = true) {
ignoreWeights = ignore;
//ignoreWeights = ignore;
}
@ -46,8 +44,8 @@ namespace storm {
}
assert(janiVar != nullptr);
assert(vars.count(place.getID()) == 0);
vars[place.getID()] = janiVar;
model->addVariable(*janiVar);
vars[place.getID()] = &model->addVariable(*janiVar);
delete janiVar;
}
}
@ -59,95 +57,76 @@ namespace storm {
void addEdges(storm::jani::Automaton& automaton, uint64_t locId) {
storm::expressions::Expression guard = expressionManager->boolean(true);
for (auto const& trans : gspn.getImmediateTransitions()) {
if (ignoreWeights || trans.noWeightAttached()) {
std::vector<storm::jani::Assignment> assignments;
uint64_t lastPriority = -1;
storm::expressions::Expression lastPriorityGuard = expressionManager->boolean(false);
storm::expressions::Expression priorityGuard = expressionManager->boolean(true);
// TODO here there is something to fix if we add transition partitions.
for (auto const& partition : gspn.getPartitions()) {
storm::expressions::Expression guard = expressionManager->boolean(false);
std::vector<storm::jani::EdgeDestination> weightedDestinations;
assert(lastPriority >= partition.priority);
if (lastPriority > partition.priority) {
priorityGuard = priorityGuard && !lastPriorityGuard;
lastPriority = partition.priority;
} else {
assert(lastPriority == partition.priority);
}
// Compute enabled weight expression.
storm::expressions::Expression totalWeight = expressionManager->rational(0.0);
for (auto const& transId : partition.transitions) {
auto const& trans = gspn.getImmediateTransitions()[transId];
if (trans.noWeightAttached()) {
continue;
}
storm::expressions::Expression destguard = expressionManager->boolean(true);
for (auto const& inPlaceEntry : trans.getInputPlaces()) {
guard = guard && (vars[inPlaceEntry.first]->getExpressionVariable() > inPlaceEntry.second);
assignments.emplace_back( *vars[inPlaceEntry.first], (vars[inPlaceEntry.first])->getExpressionVariable() - inPlaceEntry.second);
destguard = destguard && (vars[inPlaceEntry.first]->getExpressionVariable() >= inPlaceEntry.second);
}
for (auto const& inhibPlaceEntry : trans.getInhibitionPlaces()) {
guard = guard && (vars[inhibPlaceEntry.first]->getExpressionVariable() > inhibPlaceEntry.second);
destguard = destguard && (vars[inhibPlaceEntry.first]->getExpressionVariable() >= inhibPlaceEntry.second);
}
for (auto const& outputPlaceEntry : trans.getOutputPlaces()) {
assignments.emplace_back( *vars[outputPlaceEntry.first], (vars[outputPlaceEntry.first])->getExpressionVariable() + outputPlaceEntry.second );
}
storm::jani::OrderedAssignments oa(assignments);
storm::jani::EdgeDestination dest(locId, expressionManager->integer(1), oa);
storm::jani::Edge e(locId, storm::jani::Model::SILENT_ACTION_INDEX, boost::none, guard, {dest});
automaton.addEdge(e);
totalWeight = totalWeight + storm::expressions::ite(destguard, expressionManager->rational(trans.getWeight()), expressionManager->rational(0.0));
}
totalWeight = totalWeight.simplify();
}
if(!ignoreWeights) {
uint64_t lastPriority;
storm::expressions::Expression lastPriorityGuard = expressionManager->boolean(false);
storm::expressions::Expression priorityGuard = expressionManager->boolean(true);
// TODO here there is something to fix if we add transition partitions.
for (auto const& partition : gspn.getPartitions()) {
storm::expressions::Expression guard = expressionManager->boolean(false);
std::vector<storm::jani::EdgeDestination> weightedDestinations;
assert(lastPriority <= partition.priority);
if (lastPriority < partition.priority) {
priorityGuard = priorityGuard && !lastPriorityGuard;
lastPriority = partition.priority;
} else {
assert(lastPriority == partition.priority);
for (auto const& transId : partition.transitions) {
auto const& trans = gspn.getImmediateTransitions()[transId];
if (trans.noWeightAttached()) {
std::cout << "ERROR -- no weights attached at transition" << std::endl;
continue;
}
// Compute enabled weight expression.
storm::expressions::Expression totalWeight = expressionManager->rational(0.0);
for (auto const& transId : partition.transitions) {
auto const& trans = gspn.getImmediateTransitions()[transId];
if (trans.noWeightAttached()) {
continue;
}
storm::expressions::Expression destguard = expressionManager->boolean(true);
for (auto const& inPlaceEntry : trans.getInputPlaces()) {
destguard = destguard && (vars[inPlaceEntry.first]->getExpressionVariable() > inPlaceEntry.second);
}
for (auto const& inhibPlaceEntry : trans.getInhibitionPlaces()) {
destguard = destguard && (vars[inhibPlaceEntry.first]->getExpressionVariable() > inhibPlaceEntry.second);
storm::expressions::Expression destguard = expressionManager->boolean(true);
std::vector<storm::jani::Assignment> assignments;
for (auto const& inPlaceEntry : trans.getInputPlaces()) {
destguard = destguard && (vars[inPlaceEntry.first]->getExpressionVariable() > inPlaceEntry.second);
if (trans.getOutputPlaces().count(inPlaceEntry.first) == 0) {
assignments.emplace_back( *vars[inPlaceEntry.first], (vars[inPlaceEntry.first])->getExpressionVariable() - inPlaceEntry.second);
}
totalWeight = totalWeight + storm::expressions::ite(destguard, expressionManager->rational(trans.getWeight()), expressionManager->rational(0.0));
}
totalWeight = totalWeight.simplify();
for (auto const& transId : partition.transitions) {
auto const& trans = gspn.getImmediateTransitions()[transId];
if (trans.noWeightAttached()) {
continue;
}
storm::expressions::Expression destguard = expressionManager->boolean(true);
std::vector<storm::jani::Assignment> assignments;
for (auto const& inPlaceEntry : trans.getInputPlaces()) {
destguard = destguard && (vars[inPlaceEntry.first]->getExpressionVariable() > inPlaceEntry.second);
assignments.emplace_back( *vars[inPlaceEntry.first], (vars[inPlaceEntry.first]->getExpressionVariable() - inPlaceEntry.second) );
}
for (auto const& inhibPlaceEntry : trans.getInhibitionPlaces()) {
destguard = destguard && (vars[inhibPlaceEntry.first]->getExpressionVariable() > inhibPlaceEntry.second);
}
for (auto const& outputPlaceEntry : trans.getOutputPlaces()) {
assignments.emplace_back( *vars[outputPlaceEntry.first], (vars[outputPlaceEntry.first]->getExpressionVariable() + outputPlaceEntry.second) );
for (auto const& inhibPlaceEntry : trans.getInhibitionPlaces()) {
destguard = destguard && (vars[inhibPlaceEntry.first]->getExpressionVariable() > inhibPlaceEntry.second);
}
for (auto const& outputPlaceEntry : trans.getOutputPlaces()) {
if (trans.getInputPlaces().count(outputPlaceEntry.first) == 0) {
assignments.emplace_back( *vars[outputPlaceEntry.first], (vars[outputPlaceEntry.first])->getExpressionVariable() + outputPlaceEntry.second );
} else {
assignments.emplace_back( *vars[outputPlaceEntry.first], (vars[outputPlaceEntry.first])->getExpressionVariable() + outputPlaceEntry.second - trans.getInputPlaces().at(outputPlaceEntry.first));
}
destguard = destguard.simplify();
guard = guard || destguard;
storm::jani::OrderedAssignments oa(assignments);
storm::jani::EdgeDestination dest(locId, storm::expressions::ite(destguard, (expressionManager->rational(trans.getWeight()) / totalWeight), expressionManager->rational(0.0)), oa);
weightedDestinations.push_back(dest);
}
storm::jani::Edge e(locId, storm::jani::Model::SILENT_ACTION_INDEX, boost::none, (priorityGuard && guard).simplify(), weightedDestinations);
automaton.addEdge(e);
lastPriorityGuard = lastPriorityGuard || guard;
destguard = destguard.simplify();
guard = guard || destguard;
storm::jani::OrderedAssignments oa(assignments);
storm::jani::EdgeDestination dest(locId, storm::expressions::ite(destguard, (expressionManager->rational(trans.getWeight()) / totalWeight), expressionManager->rational(0.0)), oa);
weightedDestinations.push_back(dest);
}
storm::jani::Edge e(locId, storm::jani::Model::SILENT_ACTION_INDEX, boost::none, (priorityGuard && guard).simplify(), weightedDestinations);
automaton.addEdge(e);
lastPriorityGuard = lastPriorityGuard || guard;
}
for (auto const& trans : gspn.getTimedTransitions()) {
@ -155,27 +134,33 @@ namespace storm {
std::vector<storm::jani::Assignment> assignments;
for (auto const& inPlaceEntry : trans.getInputPlaces()) {
guard = guard && (vars[inPlaceEntry.first]->getExpressionVariable() > inPlaceEntry.second);
assignments.emplace_back( *vars[inPlaceEntry.first], (vars[inPlaceEntry.first]->getExpressionVariable() - inPlaceEntry.second) );
guard = guard && (vars[inPlaceEntry.first]->getExpressionVariable() >= inPlaceEntry.second);
if (trans.getOutputPlaces().count(inPlaceEntry.first) == 0) {
assignments.emplace_back( *vars[inPlaceEntry.first], (vars[inPlaceEntry.first])->getExpressionVariable() - inPlaceEntry.second);
}
}
for (auto const& inhibPlaceEntry : trans.getInhibitionPlaces()) {
guard = guard && (vars[inhibPlaceEntry.first]->getExpressionVariable() > inhibPlaceEntry.second);
guard = guard && (vars[inhibPlaceEntry.first]->getExpressionVariable() >= inhibPlaceEntry.second);
}
for (auto const& outputPlaceEntry : trans.getOutputPlaces()) {
assignments.emplace_back( *vars[outputPlaceEntry.first], (vars[outputPlaceEntry.first]->getExpressionVariable() + outputPlaceEntry.second) );
if (trans.getInputPlaces().count(outputPlaceEntry.first) == 0) {
assignments.emplace_back( *vars[outputPlaceEntry.first], (vars[outputPlaceEntry.first])->getExpressionVariable() + outputPlaceEntry.second );
} else {
assignments.emplace_back( *vars[outputPlaceEntry.first], (vars[outputPlaceEntry.first])->getExpressionVariable() + outputPlaceEntry.second - trans.getInputPlaces().at(outputPlaceEntry.first));
}
}
storm::jani::OrderedAssignments oa(assignments);
storm::jani::EdgeDestination dest(locId, expressionManager->integer(1), oa);
storm::jani::Edge e(locId, storm::jani::Model::SILENT_ACTION_INDEX, expressionManager->rational(trans.getRate()), guard, {dest});
automaton.addEdge(e);
}
}
private:
bool ignoreWeights;
const uint64_t janiVersion = 1;
storm::gspn::GSPN const& gspn;
std::map<uint64_t, storm::jani::Variable*> vars;
std::map<uint64_t, storm::jani::Variable const*> vars;
std::shared_ptr<storm::expressions::ExpressionManager> expressionManager;
};

32
src/storm-gspn/storm-gspn.h
View File

@ -0,0 +1,32 @@
#pragma once
#include "storm/storage/jani/Model.h"
#include "storm-gspn/builder/JaniGSPNBuilder.h"
#include "storm-gspn/storage/gspn/Gspn.h"
#include "storm/settings/modules/GSPNExportSettings.h"
namespace storm {
/**
* Builds JANI model from GSPN.
*/
storm::jani::Model* buildJani(storm::gspn::GSPN const& gspn) {
std::shared_ptr<storm::expressions::ExpressionManager> exprManager(new storm::expressions::ExpressionManager());
storm::builder::JaniGSPNBuilder builder(gspn, exprManager);
return builder.build();
}
void handleGSPNExportSettings(storm::gspn::GSPN const& gspn) {
storm::settings::modules::GSPNExportSettings const& exportSettings = storm::settings::getModule<storm::settings::modules::GSPNExportSettings>();
if (exportSettings.isWriteToDotSet()) {
std::ofstream fs;
fs.open(exportSettings.getWriteToDotFilename());
gspn.writeDotToStream(std::cout);
gspn.writeDotToStream(fs);
fs.close();
}
}
}

11
src/storm/cli/cli.cpp
View File

@ -12,7 +12,7 @@
#include "storm/settings/modules/JaniExportSettings.h"
#include "storm/utility/storm-version.h"
#include "storm/storage/jani/JSONExporter.h"
// Includes for the linked libraries and versions header.
@ -253,14 +253,7 @@ namespace storm {
}
if (model.isJaniModel() && storm::settings::getModule<storm::settings::modules::JaniExportSettings>().isJaniFileSet()) {
STORM_LOG_TRACE("Exporting JANI model.");
if (storm::settings::getModule<storm::settings::modules::JaniExportSettings>().isExportAsStandardJaniSet()) {
storm::jani::Model normalisedModel = storm::jani::Model(model.asJaniModel());
normalisedModel.makeStandardJaniCompliant();
storm::jani::JsonExporter::toFile(normalisedModel, formulasInProperties(properties), storm::settings::getModule<storm::settings::modules::JaniExportSettings>().getJaniFilename());
} else {
storm::jani::JsonExporter::toFile(model.asJaniModel(), formulasInProperties(properties), storm::settings::getModule<storm::settings::modules::JaniExportSettings>().getJaniFilename());
}
exportJaniModel(model.asJaniModel(), properties, storm::settings::getModule<storm::settings::modules::JaniExportSettings>().getJaniFilename());
}
if (ioSettings.isNoBuildModelSet()) {

2
src/storm/settings/modules/GSPNExportSettings.h
View File

@ -15,7 +15,7 @@ namespace storm {
GSPNExportSettings();
/**
* Retrievew whether the pgcl file option was set
* Retrieve whether the pgcl file option was set
*/
bool isWriteToDotSet() const;

9
src/storm/storage/jani/OrderedAssignments.cpp
View File

@ -141,5 +141,14 @@ namespace storm {
return std::lower_bound(assignments.begin(), assignments.end(), assignment, storm::jani::AssignmentPartialOrderByLevelAndVariable());
}
std::ostream& operator<<(std::ostream& stream, OrderedAssignments const& assignments) {
stream << "[";
for(auto const& e : assignments.allAssignments) {
stream << *e << std::endl;
}
stream << "]";
return stream;
}
}
}

2
src/storm/storage/jani/OrderedAssignments.h
View File

@ -109,6 +109,8 @@ namespace storm {
*/
void substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution);
friend std::ostream& operator<<(std::ostream& stream, OrderedAssignments const& assignments);
private:
static std::vector<std::shared_ptr<Assignment>>::const_iterator lowerBound(Assignment const& assignment, std::vector<std::shared_ptr<Assignment>> const& assignments);

11
src/storm/utility/storm.cpp
View File

@ -30,6 +30,17 @@ namespace storm{
modelAndFormulae.first.checkValid();
return modelAndFormulae;
}
void exportJaniModel(storm::jani::Model const& model, std::vector<storm::jani::Property> const& properties, std::string const& filepath) {
STORM_LOG_TRACE("Exporting JANI model.");
if (storm::settings::getModule<storm::settings::modules::JaniExportSettings>().isExportAsStandardJaniSet()) {
storm::jani::Model normalisedModel = model;
normalisedModel.makeStandardJaniCompliant();
storm::jani::JsonExporter::toFile(normalisedModel, formulasInProperties(properties), filepath);
} else {
storm::jani::JsonExporter::toFile(model, formulasInProperties(properties), filepath);
}
}
/**
* Helper

10
src/storm/utility/storm.h
View File

@ -23,6 +23,7 @@
#include "storm/settings/modules/RegionSettings.h"
#include "storm/settings/modules/EliminationSettings.h"
#include "storm/settings/modules/JitBuilderSettings.h"
#include "storm/settings/modules/JaniExportSettings.h"
// Formula headers.
#include "storm/logic/Formulas.h"
@ -55,6 +56,7 @@
#include "storm/storage/bisimulation/NondeterministicModelBisimulationDecomposition.h"
#include "storm/storage/ModelFormulasPair.h"
#include "storm/storage/SymbolicModelDescription.h"
#include "storm/storage/jani/JSONExporter.h"
// Headers for model checking.
#include "storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h"
@ -575,7 +577,13 @@ namespace storm {
}
return result;
}
/**
*
*/
void exportJaniModel(storm::jani::Model const& model, std::vector<storm::jani::Property> const& properties, std::string const& filepath);
template<typename ValueType>
void exportMatrixToFile(std::shared_ptr<storm::models::sparse::Model<ValueType>> model, std::string const& filepath) {
STORM_LOG_THROW(model->getType() != storm::models::ModelType::Ctmc, storm::exceptions::NotImplementedException, "This functionality is not yet implemented." );

Write Preview
Loading…
Cancel
Save