From f0132cf2a5fc4f48e94ee5e0d784206ff902e6e7 Mon Sep 17 00:00:00 2001 From: sjunges Date: Mon, 3 Oct 2016 13:43:43 +0200 Subject: [PATCH 01/13] Bounds & co for pgcl. Former-commit-id: 24797ada48f17c633dd4eef48bef17a9a836af39 [formerly 8ec467baf176952dd94b07d8c5775b8c70d28b90] Former-commit-id: 75260b0b733c0beac781f34ddc73b3302b2152f7 --- src/builder/JaniProgramGraphBuilder.cpp | 48 +++++++++++++++++++- src/builder/JaniProgramGraphBuilder.h | 59 +++++++++---------------- src/settings/modules/PGCLSettings.cpp | 2 +- src/storage/IntegerInterval.cpp | 28 ++++++++++++ src/storage/IntegerInterval.h | 1 + src/storage/ppg/ProgramGraph.h | 28 ++++++++++-- src/storm-pgcl.cpp | 5 +++ 7 files changed, 127 insertions(+), 44 deletions(-) diff --git a/src/builder/JaniProgramGraphBuilder.cpp b/src/builder/JaniProgramGraphBuilder.cpp index d6ecb3c23..00965da52 100644 --- a/src/builder/JaniProgramGraphBuilder.cpp +++ b/src/builder/JaniProgramGraphBuilder.cpp @@ -1,16 +1,62 @@ #include "JaniProgramGraphBuilder.h" + #include "src/storage/jani/EdgeDestination.h" namespace storm { namespace builder { unsigned JaniProgramGraphBuilder::janiVersion = 1; + void JaniProgramGraphBuilder::addProcedureVariables(storm::jani::Model& model, storm::jani::Automaton& automaton) { + for (auto const& v : programGraph.getVariables()) { + if (isConstant(v.first)) { + storm::jani::Constant constant(v.second.getName(), v.second, programGraph.getInitialValue(v.first)); + model.addConstant(constant); + } else if (v.second.hasBooleanType()) { + storm::jani::BooleanVariable* janiVar = new storm::jani::BooleanVariable(v.second.getName(), v.second, programGraph.getInitialValue(v.first), false); + automaton.addVariable(*janiVar); + variables.emplace(v.first, janiVar); + } else if (isRestrictedVariable(v.first) && !isRewardVariable(v.first)) { + storm::storage::IntegerInterval const& bounds = variableBounds(v.first); + if (bounds.hasLeftBound()) { + if (bounds.hasRightBound()) { + storm::jani::BoundedIntegerVariable* janiVar = new storm::jani::BoundedIntegerVariable (v.second.getName(), v.second, programGraph.getInitialValue(v.first), false, expManager->integer(bounds.getLeftBound().get()), expManager->integer(bounds.getRightBound().get())); + variables.emplace(v.first, janiVar); + automaton.addVariable(*janiVar); + } else { + // Not yet supported. + assert(false); + } + } else { + // Not yet supported. + assert(false); + } + } else { + storm::jani::UnboundedIntegerVariable* janiVar = new storm::jani::UnboundedIntegerVariable(v.second.getName(), v.second, programGraph.getInitialValue(v.first), isRewardVariable(v.first)); + if(isRewardVariable(v.first)) { + model.addVariable(*janiVar); + } else { + automaton.addVariable(*janiVar); + } + variables.emplace(v.first, janiVar); + + } + } + } + + + storm::jani::OrderedAssignments JaniProgramGraphBuilder::buildOrderedAssignments(storm::jani::Automaton& automaton, storm::ppg::DeterministicProgramAction const& act) { std::vector vec; uint64_t level = 0; for(auto const& group : act) { for(auto const& assignment : group) { - vec.emplace_back(*(variables.at(assignment.first)), assignment.second, level); + if(isRewardVariable(assignment.first)) { + std::unordered_map eval; + eval.emplace((variables.at(assignment.first))->getExpressionVariable(), expManager->integer(0)); + vec.emplace_back(*(variables.at(assignment.first)), assignment.second.substitute(eval).simplify(), level); + } else { + vec.emplace_back(*(variables.at(assignment.first)), assignment.second, level); + } } ++level; } diff --git a/src/builder/JaniProgramGraphBuilder.h b/src/builder/JaniProgramGraphBuilder.h index 4f6c5fc9f..4d03af2c7 100644 --- a/src/builder/JaniProgramGraphBuilder.h +++ b/src/builder/JaniProgramGraphBuilder.h @@ -1,4 +1,5 @@ #include +#include #include "src/storage/ppg/ProgramGraph.h" #include "src/storage/jani/Model.h" @@ -45,6 +46,10 @@ namespace storm { void restrictAllVariables(int64_t from, int64_t to) { + restrictAllVariables(storm::storage::IntegerInterval(from, to)); + } + + void restrictAllVariables(storm::storage::IntegerInterval const& restr) { for (auto const& v : programGraph.getVariables()) { if(isConstant(v.first)) { continue; @@ -53,7 +58,7 @@ namespace storm { continue; // Currently we ignore user bounds if we have bounded integers; } if(v.second.hasIntegerType() ) { - userVariableRestrictions.emplace(v.first, storm::storage::IntegerInterval(from, to)); + userVariableRestrictions.emplace(v.first, restr); } } } @@ -63,7 +68,7 @@ namespace storm { storm::jani::Model* model = new storm::jani::Model(name, storm::jani::ModelType::MDP, janiVersion, expManager); storm::jani::Automaton mainAutomaton("main"); addProcedureVariables(*model, mainAutomaton); - janiLocId = addProcedureLocations(mainAutomaton); + janiLocId = addProcedureLocations(*model, mainAutomaton); addVariableOoBLocations(mainAutomaton); addEdges(mainAutomaton); model->addAutomaton(mainAutomaton); @@ -117,47 +122,23 @@ namespace storm { return std::find(constants.begin(), constants.end(), i) != constants.end(); } - void addProcedureVariables(storm::jani::Model& model, storm::jani::Automaton& automaton) { - for (auto const& v : programGraph.getVariables()) { - if (isConstant(v.first)) { - storm::jani::Constant constant(v.second.getName(), v.second, programGraph.getInitialValue(v.first)); - model.addConstant(constant); - } else if (v.second.hasBooleanType()) { - storm::jani::BooleanVariable* janiVar = new storm::jani::BooleanVariable(v.second.getName(), v.second, programGraph.getInitialValue(v.first), false); - automaton.addVariable(*janiVar); - variables.emplace(v.first, janiVar); - } else if (isRestrictedVariable(v.first) && !isRewardVariable(v.first)) { - storm::storage::IntegerInterval const& bounds = variableBounds(v.first); - if (bounds.hasLeftBound()) { - if (bounds.hasRightBound()) { - storm::jani::BoundedIntegerVariable* janiVar = new storm::jani::BoundedIntegerVariable (v.second.getName(), v.second, programGraph.getInitialValue(v.first), false, expManager->integer(bounds.getLeftBound().get()), expManager->integer(bounds.getRightBound().get())); - variables.emplace(v.first, janiVar); - automaton.addVariable(*janiVar); - } else { - // Not yet supported. - assert(false); - } - } else { - // Not yet supported. - assert(false); - } - } else { - storm::jani::UnboundedIntegerVariable* janiVar = new storm::jani::UnboundedIntegerVariable(v.second.getName(), v.second, programGraph.getInitialValue(v.first), isRewardVariable(v.first)); - if(isRewardVariable(v.first)) { - model.addVariable(*janiVar); - } else { - automaton.addVariable(*janiVar); - } - variables.emplace(v.first, janiVar); - - } - } - } + void addProcedureVariables(storm::jani::Model& model, storm::jani::Automaton& automaton); - std::map addProcedureLocations(storm::jani::Automaton& automaton) { + std::map addProcedureLocations(storm::jani::Model& model, storm::jani::Automaton& automaton) { std::map result; + std::map labelVars; + std::set labels = programGraph.getLabels(); + for(auto const& label : labels) { + storm::jani::BooleanVariable janiVar(label, expManager->declareBooleanVariable(label), expManager->boolean(false), true); + labelVars.emplace(label, &model.addVariable(janiVar)); + } + for (auto it = programGraph.locationBegin(); it != programGraph.locationEnd(); ++it) { storm::jani::Location janiLoc(janiLocationName(it->second.id())); + for(auto const& label : programGraph.getLabels(it->second.id())) { + assert(labelVars.count(label) > 0); + janiLoc.addTransientAssignment(storm::jani::Assignment(*(labelVars.at(label)), expManager->boolean(true))); + } result[it->second.id()] = automaton.addLocation(janiLoc); if (it->second.isInitial()) { automaton.addInitialLocation(result[it->second.id()]); diff --git a/src/settings/modules/PGCLSettings.cpp b/src/settings/modules/PGCLSettings.cpp index 051b23375..e73b9514e 100644 --- a/src/settings/modules/PGCLSettings.cpp +++ b/src/settings/modules/PGCLSettings.cpp @@ -28,7 +28,7 @@ namespace storm { this->addOption(storm::settings::OptionBuilder(moduleName, pgclFileOptionName, false, "Parses the pgcl program.").setShortName(pgclFileOptionShortName).addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "path to file").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, pgclToJaniOptionName, false, "Transform to JANI.").setShortName(pgclToJaniOptionShortName).build()); this->addOption(storm::settings::OptionBuilder(moduleName, programGraphToDotOptionName, false, "Destination for the program graph dot output.").setShortName(programGraphToDotShortOptionName).addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "path to file").build()).build()); - this->addOption(storm::settings::OptionBuilder(moduleName, programVariableRestrictionsOptionName, false, "Restrictions of program variables").setShortName(programVariableRestrictionShortOptionName).addArgument(storm::settings::ArgumentBuilder::createStringArgument("descriptio", "description of the variable restrictions").build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, programVariableRestrictionsOptionName, false, "Restrictions of program variables").setShortName(programVariableRestrictionShortOptionName).addArgument(storm::settings::ArgumentBuilder::createStringArgument("description", "description of the variable restrictions").build()).build()); } bool PGCLSettings::isPgclFileSet() const { diff --git a/src/storage/IntegerInterval.cpp b/src/storage/IntegerInterval.cpp index 7722d359b..4210cbe4b 100644 --- a/src/storage/IntegerInterval.cpp +++ b/src/storage/IntegerInterval.cpp @@ -1,2 +1,30 @@ #include "IntegerInterval.h" +#include +#include + +#include "src/utility/macros.h" +#include "src/exceptions/InvalidArgumentException.h" + +bool starts_with(const std::string& s1, const std::string& s2) { + return s2.size() <= s1.size() && s1.compare(0, s2.size(), s2) == 0; +} + +namespace storm { + namespace storage { + IntegerInterval parseIntegerInterval(std::string const& stringRepr) { + + + if(starts_with(stringRepr, "[") && stringRepr.at(stringRepr.size()-1) == ']') { + auto split = stringRepr.find(","); + std::string first = stringRepr.substr(1,split-1); + + std::string second = stringRepr.substr(split+1, stringRepr.size() - split - 2); + return IntegerInterval(stoi(first), stoi(second)); + + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Cannot parse " << stringRepr << " as integer interval"); + } + } + } +} \ No newline at end of file diff --git a/src/storage/IntegerInterval.h b/src/storage/IntegerInterval.h index f662f1a6d..24b5ed892 100644 --- a/src/storage/IntegerInterval.h +++ b/src/storage/IntegerInterval.h @@ -95,5 +95,6 @@ namespace storm { }; std::ostream& operator<<(std::ostream& os, IntegerInterval const& i); + IntegerInterval parseIntegerInterval(std::string const& stringRepr); } } \ No newline at end of file diff --git a/src/storage/ppg/ProgramGraph.h b/src/storage/ppg/ProgramGraph.h index dc0c58ab6..864a54c1a 100644 --- a/src/storage/ppg/ProgramGraph.h +++ b/src/storage/ppg/ProgramGraph.h @@ -49,10 +49,19 @@ namespace storm { return &(probabilisticActions.emplace(newId, ProbabilisticProgramAction(this, newId, var, from, to)).first->second); } - ProgramLocation* addLocation(bool isInitial = false, bool successfulTermination = false, bool aborted = false, std::vector const& labels = {}) { + ProgramLocation* addLocation(bool isInitial = false, bool successfulTermination = false, bool observeViolated = false, bool aborted = false, std::vector const& labels = {}) { ProgramLocationIdentifier newId = freeLocationIndex(); assert(!hasLocation(newId)); locationLabels[newId] = labels; + if (successfulTermination) { + locationLabels[newId].push_back(succesfulTerminationLabel); + } + if (observeViolated) { + locationLabels[newId].push_back(observeViolatedLabel); + } + if (aborted) { + locationLabels[newId].push_back(abortLabel); + } return &(locations.emplace(newId, ProgramLocation(this, newId, isInitial)).first->second); } @@ -98,7 +107,19 @@ namespace storm { return res; } + std::set getLabels() const { + std::set result; + for(auto const& locEntry : locationLabels) { + for(auto const& label : locEntry.second) { + result.insert(label); + } + } + return result; + } + std::vector getLabels(ProgramLocationIdentifier loc) const { + return locationLabels.at(loc); + } bool hasLabel(ProgramLocationIdentifier loc, std::string const& label) const { return std::find(locationLabels.at(loc).begin(), locationLabels.at(loc).end(), label) != locationLabels.at(loc).end(); @@ -288,8 +309,9 @@ namespace storm { ProgramEdgeIdentifier newEdgeId = 0; ProgramActionIdentifier newActionId = 1; ProgramActionIdentifier noActionId = 0; - std::string succesfulTerminationLabel = "__ret0__"; - std::string abortLabel = "__ret1__"; + std::string succesfulTerminationLabel = "_ret0_"; + std::string abortLabel = "_ret1_"; + std::string observeViolatedLabel = "_viol_"; }; diff --git a/src/storm-pgcl.cpp b/src/storm-pgcl.cpp index 66e227d75..99ac1c960 100644 --- a/src/storm-pgcl.cpp +++ b/src/storm-pgcl.cpp @@ -77,6 +77,11 @@ int main(const int argc, const char** argv) { } if (storm::settings::getModule().isToJaniSet()) { storm::builder::JaniProgramGraphBuilder builder(*progGraph); + if (storm::settings::getModule().isProgramVariableRestrictionSet()) { + // TODO More fine grained control + storm::storage::IntegerInterval restr = storm::storage::parseIntegerInterval(storm::settings::getModule().getProgramVariableRestrictions()); + builder.restrictAllVariables(restr); + } builder.restrictAllVariables(0, 120); storm::jani::Model* model = builder.build(); delete progGraph; From 59a92a8941b50129c9092468eedff80515fa3b80 Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 11 Oct 2016 16:05:47 +0200 Subject: [PATCH 02/13] support for labels in JANI models in sparse and dd engine Former-commit-id: 34ad80be353fce2b47104e3a3d507450332b33de [formerly 67c09e4ff729c8f76b5f78912ac8062eabbed7f7] Former-commit-id: 1bf8ab71a17cb4f967eec4ca496ffdcad8453ff6 --- src/builder/DdJaniModelBuilder.cpp | 75 +++++++++++++++---- src/builder/DdJaniModelBuilder.h | 20 +++++- src/generator/CompressedState.cpp | 14 ++++ src/generator/JaniNextStateGenerator.cpp | 87 +++++++++++++++++++---- src/generator/JaniNextStateGenerator.h | 2 +- src/generator/NextStateGenerator.cpp | 12 ++-- src/generator/NextStateGenerator.h | 2 +- src/generator/PrismNextStateGenerator.cpp | 35 ++++----- src/generator/VariableInformation.cpp | 5 +- src/generator/VariableInformation.h | 7 +- src/storage/BitVector.h | 2 +- src/storage/jani/Model.cpp | 33 +++++++++ src/storage/jani/Model.h | 6 ++ src/storage/jani/VariableSet.cpp | 20 ++++++ src/storage/jani/VariableSet.h | 10 +++ 15 files changed, 269 insertions(+), 61 deletions(-) diff --git a/src/builder/DdJaniModelBuilder.cpp b/src/builder/DdJaniModelBuilder.cpp index 325cfb3a5..8b54e0eba 100644 --- a/src/builder/DdJaniModelBuilder.cpp +++ b/src/builder/DdJaniModelBuilder.cpp @@ -15,6 +15,8 @@ #include "src/storage/dd/Bdd.h" #include "src/adapters/AddExpressionAdapter.h" +#include "src/storage/expressions/ExpressionManager.h" + #include "src/models/symbolic/Dtmc.h" #include "src/models/symbolic/Ctmc.h" #include "src/models/symbolic/Mdp.h" @@ -28,6 +30,7 @@ #include "src/utility/dd.h" #include "src/utility/math.h" #include "src/exceptions/WrongFormatException.h" +#include "src/exceptions/InvalidSettingsException.h" #include "src/exceptions/InvalidArgumentException.h" #include "src/exceptions/InvalidStateException.h" #include "src/exceptions/NotSupportedException.h" @@ -36,7 +39,7 @@ namespace storm { namespace builder { template - DdJaniModelBuilder::Options::Options() : buildAllRewardModels(true), rewardModelsToBuild(), constantDefinitions(), terminalStates(), negatedTerminalStates() { + DdJaniModelBuilder::Options::Options(bool buildAllLabels, bool buildAllRewardModels) : buildAllLabels(buildAllLabels), buildAllRewardModels(buildAllRewardModels), rewardModelsToBuild(), constantDefinitions(), terminalStates(), negatedTerminalStates() { // Intentionally left empty. } @@ -47,7 +50,7 @@ namespace storm { } template - DdJaniModelBuilder::Options::Options(std::vector> const& formulas) : buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), terminalStates(), negatedTerminalStates() { + DdJaniModelBuilder::Options::Options(std::vector> const& formulas) : buildAllLabels(false), buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), terminalStates(), negatedTerminalStates() { if (formulas.empty()) { this->buildAllRewardModels = true; } else { @@ -75,6 +78,12 @@ namespace storm { std::set referencedRewardModels = formula.getReferencedRewardModels(); rewardModelsToBuild.insert(referencedRewardModels.begin(), referencedRewardModels.end()); } + + // Extract all the labels used in the formula. + std::vector> atomicLabelFormulas = formula.getAtomicLabelFormulas(); + for (auto const& formula : atomicLabelFormulas) { + addLabel(formula->getLabel()); + } } template @@ -112,7 +121,18 @@ namespace storm { bool DdJaniModelBuilder::Options::isBuildAllRewardModelsSet() const { return buildAllRewardModels; } + + template + bool DdJaniModelBuilder::Options::isBuildAllLabelsSet() const { + return buildAllLabels; + } + template + void DdJaniModelBuilder::Options::addLabel(std::string const& labelName) { + STORM_LOG_THROW(!buildAllLabels, storm::exceptions::InvalidSettingsException, "Cannot add label, because all labels are built anyway."); + labelNames.insert(labelName); + } + template struct CompositionVariables { CompositionVariables() : manager(std::make_shared>()), @@ -138,8 +158,9 @@ namespace storm { // All pairs of row/column meta variables. std::vector> rowColumnMetaVariablePairs; - // A mapping from automata to the meta variable encoding their location. - std::map> automatonToLocationVariableMap; + // A mapping from automata to the meta variables encoding their location. + std::map automatonToLocationVariableMap; + std::map> automatonToLocationDdVariableMap; // A mapping from action indices to the meta variables used to encode these actions. std::map actionVariablesMap; @@ -245,9 +266,14 @@ namespace storm { for (auto const& automaton : this->model.getAutomata()) { // Start by creating a meta variable for the location of the automaton. + storm::expressions::Variable locationExpressionVariable = model.getManager().declareFreshIntegerVariable(false, "loc"); + result.automatonToLocationVariableMap[automaton.getName()] = locationExpressionVariable; std::pair variablePair = result.manager->addMetaVariable("l_" + automaton.getName(), 0, automaton.getNumberOfLocations() - 1); - result.automatonToLocationVariableMap[automaton.getName()] = variablePair; + result.automatonToLocationDdVariableMap[automaton.getName()] = variablePair; result.rowColumnMetaVariablePairs.push_back(variablePair); + + result.variableToRowMetaVariableMap->emplace(locationExpressionVariable, variablePair.first); + result.variableToColumnMetaVariableMap->emplace(locationExpressionVariable, variablePair.second); // Add the location variable to the row/column variables. result.rowMetaVariables.insert(variablePair.first); @@ -277,7 +303,7 @@ namespace storm { storm::dd::Bdd range = result.manager->getBddOne(); // Add the identity and ranges of the location variables to the ones of the automaton. - std::pair const& locationVariables = result.automatonToLocationVariableMap[automaton.getName()]; + std::pair const& locationVariables = result.automatonToLocationDdVariableMap[automaton.getName()]; storm::dd::Add variableIdentity = result.manager->template getIdentity(locationVariables.first).equals(result.manager->template getIdentity(locationVariables.second)).template toAdd() * result.manager->getRange(locationVariables.first).template toAdd() * result.manager->getRange(locationVariables.second).template toAdd(); identity &= variableIdentity.toBdd(); range &= result.manager->getRange(locationVariables.first); @@ -458,7 +484,7 @@ namespace storm { } } - transitions *= variables.manager->getEncoding(variables.automatonToLocationVariableMap.at(automaton.getName()).second, destination.getLocationIndex()).template toAdd(); + transitions *= variables.manager->getEncoding(variables.automatonToLocationDdVariableMap.at(automaton.getName()).second, destination.getLocationIndex()).template toAdd(); return EdgeDestinationDd(transitions, assignedGlobalVariables); } @@ -1081,7 +1107,7 @@ namespace storm { } // Add the source location and the guard. - transitions *= this->variables.manager->getEncoding(this->variables.automatonToLocationVariableMap.at(automaton.getName()).first, edge.getSourceLocationIndex()).template toAdd() * guard; + transitions *= this->variables.manager->getEncoding(this->variables.automatonToLocationDdVariableMap.at(automaton.getName()).first, edge.getSourceLocationIndex()).template toAdd() * guard; // If we multiply the ranges of global variables, make sure everything stays within its bounds. if (!globalVariablesInSomeDestination.empty()) { @@ -1475,7 +1501,7 @@ namespace storm { for (uint64_t locationIndex = 0; locationIndex < automaton.getNumberOfLocations(); ++locationIndex) { auto const& location = automaton.getLocation(locationIndex); performTransientAssignments(location.getAssignments().getTransientAssignments(), [this,&automatonName,locationIndex,&result] (storm::jani::Assignment const& assignment) { - storm::dd::Add assignedValues = this->variables.manager->getEncoding(this->variables.automatonToLocationVariableMap.at(automatonName).first, locationIndex).template toAdd() * this->variables.rowExpressionAdapter->translateExpression(assignment.getAssignedExpression()); + storm::dd::Add assignedValues = this->variables.manager->getEncoding(this->variables.automatonToLocationDdVariableMap.at(automatonName).first, locationIndex).template toAdd() * this->variables.rowExpressionAdapter->translateExpression(assignment.getAssignedExpression()); auto it = result.transientLocationAssignments.find(assignment.getExpressionVariable()); if (it != result.transientLocationAssignments.end()) { it->second += assignedValues; @@ -1557,17 +1583,18 @@ namespace storm { storm::dd::Bdd deadlockStates; storm::dd::Add transitionMatrix; std::unordered_map> rewardModels; + std::map labelToExpressionMap; }; template std::shared_ptr> createModel(storm::jani::ModelType const& modelType, CompositionVariables const& variables, ModelComponents const& modelComponents) { if (modelType == storm::jani::ModelType::DTMC) { - return std::shared_ptr>(new storm::models::symbolic::Dtmc(variables.manager, modelComponents.reachableStates, modelComponents.initialStates, modelComponents.deadlockStates, modelComponents.transitionMatrix, variables.rowMetaVariables, variables.rowExpressionAdapter, variables.columnMetaVariables, variables.columnExpressionAdapter, variables.rowColumnMetaVariablePairs, std::map(), modelComponents.rewardModels)); + return std::shared_ptr>(new storm::models::symbolic::Dtmc(variables.manager, modelComponents.reachableStates, modelComponents.initialStates, modelComponents.deadlockStates, modelComponents.transitionMatrix, variables.rowMetaVariables, variables.rowExpressionAdapter, variables.columnMetaVariables, variables.columnExpressionAdapter, variables.rowColumnMetaVariablePairs, modelComponents.labelToExpressionMap, modelComponents.rewardModels)); } else if (modelType == storm::jani::ModelType::CTMC) { - return std::shared_ptr>(new storm::models::symbolic::Ctmc(variables.manager, modelComponents.reachableStates, modelComponents.initialStates, modelComponents.deadlockStates, modelComponents.transitionMatrix, variables.rowMetaVariables, variables.rowExpressionAdapter, variables.columnMetaVariables, variables.columnExpressionAdapter, variables.rowColumnMetaVariablePairs, std::map(), modelComponents.rewardModels)); + return std::shared_ptr>(new storm::models::symbolic::Ctmc(variables.manager, modelComponents.reachableStates, modelComponents.initialStates, modelComponents.deadlockStates, modelComponents.transitionMatrix, variables.rowMetaVariables, variables.rowExpressionAdapter, variables.columnMetaVariables, variables.columnExpressionAdapter, variables.rowColumnMetaVariablePairs, modelComponents.labelToExpressionMap, modelComponents.rewardModels)); } else if (modelType == storm::jani::ModelType::MDP) { - return std::shared_ptr>(new storm::models::symbolic::Mdp(variables.manager, modelComponents.reachableStates, modelComponents.initialStates, modelComponents.deadlockStates, modelComponents.transitionMatrix, variables.rowMetaVariables, variables.rowExpressionAdapter, variables.columnMetaVariables, variables.columnExpressionAdapter, variables.rowColumnMetaVariablePairs, variables.allNondeterminismVariables, std::map(), modelComponents.rewardModels)); + return std::shared_ptr>(new storm::models::symbolic::Mdp(variables.manager, modelComponents.reachableStates, modelComponents.initialStates, modelComponents.deadlockStates, modelComponents.transitionMatrix, variables.rowMetaVariables, variables.rowExpressionAdapter, variables.columnMetaVariables, variables.columnExpressionAdapter, variables.rowColumnMetaVariablePairs, variables.allNondeterminismVariables, modelComponents.labelToExpressionMap, modelComponents.rewardModels)); } else { STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Invalid model type."); } @@ -1635,7 +1662,7 @@ namespace storm { for (auto const& automaton : model.getAutomata()) { storm::dd::Bdd initialLocationIndices = variables.manager->getBddZero(); for (auto const& locationIndex : automaton.getInitialLocationIndices()) { - initialLocationIndices |= variables.manager->getEncoding(variables.automatonToLocationVariableMap.at(automaton.getName()).first, locationIndex); + initialLocationIndices |= variables.manager->getEncoding(variables.automatonToLocationDdVariableMap.at(automaton.getName()).first, locationIndex); } initialStates &= initialLocationIndices; } @@ -1698,7 +1725,7 @@ namespace storm { std::vector result; if (options.isBuildAllRewardModelsSet()) { for (auto const& variable : model.getGlobalVariables()) { - if (variable.isTransient()) { + if (variable.isTransient() && (variable.isRealVariable() || variable.isUnboundedIntegerVariable())) { result.push_back(variable.getExpressionVariable()); } } @@ -1709,7 +1736,7 @@ namespace storm { result.push_back(globalVariables.getVariable(rewardModelName).getExpressionVariable()); } else { STORM_LOG_THROW(rewardModelName.empty(), storm::exceptions::InvalidArgumentException, "Cannot build unknown reward model '" << rewardModelName << "'."); - STORM_LOG_THROW(globalVariables.getNumberOfTransientVariables() == 1, storm::exceptions::InvalidArgumentException, "Reference to standard reward model is ambiguous."); + STORM_LOG_THROW(globalVariables.getNumberOfRealTransientVariables() + globalVariables.getNumberOfUnboundedIntegerTransientVariables() == 1, storm::exceptions::InvalidArgumentException, "Reference to standard reward model is ambiguous."); } } @@ -1748,6 +1775,21 @@ namespace storm { return result; } + template + std::map buildLabelExpressions(storm::jani::Model const& model, CompositionVariables const& variables, typename DdJaniModelBuilder::Options const& options) { + std::map result; + + for (auto const& variable : model.getGlobalVariables().getTransientVariables()) { + if (variable->isBooleanVariable()) { + if (options.buildAllLabels || options.labelNames.find(variable->getName()) != options.labelNames.end()) { + result[variable->getName()] = model.getLabelExpression(variable->asBooleanVariable(), variables.automatonToLocationVariableMap); + } + } + } + + return result; + } + template std::shared_ptr> DdJaniModelBuilder::build(storm::jani::Model const& model, Options const& options) { if (model.hasUndefinedConstants()) { @@ -1814,6 +1856,9 @@ namespace storm { // Build the reward models. modelComponents.rewardModels = buildRewardModels(system, rewardVariables); + // Build the label to expressions mapping. + modelComponents.labelToExpressionMap = buildLabelExpressions(model, variables, options); + // Finally, create the model. return createModel(model.getModelType(), variables, modelComponents); } diff --git a/src/builder/DdJaniModelBuilder.h b/src/builder/DdJaniModelBuilder.h index dd99f5fcb..85c62b0bd 100644 --- a/src/builder/DdJaniModelBuilder.h +++ b/src/builder/DdJaniModelBuilder.h @@ -25,7 +25,7 @@ namespace storm { /*! * Creates an object representing the default building options. */ - Options(); + Options(bool buildAllLabels = false, bool buildAllRewardModels = false); /*! Creates an object representing the suggested building options assuming that the given formula is the * only one to check. Additional formulas may be preserved by calling preserveFormula. @@ -63,7 +63,23 @@ namespace storm { * Retrieves the names of the reward models to build. */ std::set const& getRewardModelNames() const; + + /*! + * Adds the given label to the ones that are supposed to be built. + */ + void addLabel(std::string const& labelName); + + /*! + * Retrieves whether the flag to build all labels is set. + */ + bool isBuildAllLabelsSet() const; + + /// A flag that indicates whether all labels are to be built. In this case, the label names are to be ignored. + bool buildAllLabels; + /// A set of labels to build. + std::set labelNames; + /*! * Retrieves whether the flag to build all reward models is set. */ @@ -98,4 +114,4 @@ namespace storm { }; } -} \ No newline at end of file +} diff --git a/src/generator/CompressedState.cpp b/src/generator/CompressedState.cpp index d7707d740..820b2000e 100644 --- a/src/generator/CompressedState.cpp +++ b/src/generator/CompressedState.cpp @@ -10,6 +10,13 @@ namespace storm { template void unpackStateIntoEvaluator(CompressedState const& state, VariableInformation const& variableInformation, storm::expressions::ExpressionEvaluator& evaluator) { + for (auto const& locationVariable : variableInformation.locationVariables) { + if (locationVariable.bitWidth != 0) { + evaluator.setIntegerValue(locationVariable.variable, state.getAsInt(locationVariable.bitOffset, locationVariable.bitWidth)); + } else { + evaluator.setIntegerValue(locationVariable.variable, 0); + } + } for (auto const& booleanVariable : variableInformation.booleanVariables) { evaluator.setBooleanValue(booleanVariable.variable, state.get(booleanVariable.bitOffset)); } @@ -20,6 +27,13 @@ namespace storm { storm::expressions::SimpleValuation unpackStateIntoValuation(CompressedState const& state, VariableInformation const& variableInformation, storm::expressions::ExpressionManager const& manager) { storm::expressions::SimpleValuation result(manager.getSharedPointer()); + for (auto const& locationVariable : variableInformation.locationVariables) { + if (locationVariable.bitWidth != 0) { + result.setIntegerValue(locationVariable.variable, state.getAsInt(locationVariable.bitOffset, locationVariable.bitWidth)); + } else { + result.setIntegerValue(locationVariable.variable, 0); + } + } for (auto const& booleanVariable : variableInformation.booleanVariables) { result.setBooleanValue(booleanVariable.variable, state.get(booleanVariable.bitOffset)); } diff --git a/src/generator/JaniNextStateGenerator.cpp b/src/generator/JaniNextStateGenerator.cpp index b84ffca3c..bc166cba3 100644 --- a/src/generator/JaniNextStateGenerator.cpp +++ b/src/generator/JaniNextStateGenerator.cpp @@ -32,6 +32,9 @@ namespace storm { this->checkValid(); this->variableInformation = VariableInformation(model); + // Create a proper evalator. + this->evaluator = std::make_unique>(model.getManager()); + if (this->options.isBuildAllRewardModelsSet()) { for (auto const& variable : model.getGlobalVariables()) { if (variable.isTransient()) { @@ -46,14 +49,22 @@ namespace storm { rewardVariables.push_back(globalVariables.getVariable(rewardModelName).getExpressionVariable()); } else { STORM_LOG_THROW(rewardModelName.empty(), storm::exceptions::InvalidArgumentException, "Cannot build unknown reward model '" << rewardModelName << "'."); - STORM_LOG_THROW(globalVariables.getNumberOfTransientVariables() == 1, storm::exceptions::InvalidArgumentException, "Reference to standard reward model is ambiguous."); + STORM_LOG_THROW(globalVariables.getNumberOfRealTransientVariables() + globalVariables.getNumberOfUnboundedIntegerTransientVariables() == 1, storm::exceptions::InvalidArgumentException, "Reference to standard reward model is ambiguous."); } } // If no reward model was yet added, but there was one that was given in the options, we try to build the // standard reward model. if (rewardVariables.empty() && !this->options.getRewardModelNames().empty()) { - rewardVariables.push_back(globalVariables.getTransientVariables().front()->getExpressionVariable()); + bool foundTransientVariable = false; + for (auto const& transientVariable : globalVariables.getTransientVariables()) { + if (transientVariable->isUnboundedIntegerVariable() || transientVariable->isRealVariable()) { + rewardVariables.push_back(transientVariable->getExpressionVariable()); + foundTransientVariable = true; + break; + } + } + STORM_LOG_ASSERT(foundTransientVariable, "Expected to find a fitting transient variable."); } } @@ -62,11 +73,28 @@ namespace storm { // If there are terminal states we need to handle, we now need to translate all labels to expressions. if (this->options.hasTerminalStates()) { + std::map locationVariables; + auto locationVariableIt = this->variableInformation.locationVariables.begin(); + for (auto const& automaton : this->model.getAutomata()) { + locationVariables[automaton.getName()] = locationVariableIt->variable; + ++locationVariableIt; + } + for (auto const& expressionOrLabelAndBool : this->options.getTerminalStates()) { if (expressionOrLabelAndBool.first.isExpression()) { this->terminalStates.push_back(std::make_pair(expressionOrLabelAndBool.first.getExpression(), expressionOrLabelAndBool.second)); } else { - STORM_LOG_THROW(expressionOrLabelAndBool.first.getLabel() == "init" || expressionOrLabelAndBool.first.getLabel() == "deadlock", storm::exceptions::InvalidSettingsException, "Terminal states refer to illegal label '" << expressionOrLabelAndBool.first.getLabel() << "'."); + // If it's a label, i.e. refers to a transient boolean variable we need to derive the expression + // for the label so we can cut off the exploration there. + if (expressionOrLabelAndBool.first.getLabel() != "init" && expressionOrLabelAndBool.first.getLabel() != "deadlock") { + STORM_LOG_THROW(model.getGlobalVariables().hasVariable(expressionOrLabelAndBool.first.getLabel()) , storm::exceptions::InvalidSettingsException, "Terminal states refer to illegal label '" << expressionOrLabelAndBool.first.getLabel() << "'."); + + storm::jani::Variable const& variable = model.getGlobalVariables().getVariable(expressionOrLabelAndBool.first.getLabel()); + STORM_LOG_THROW(variable.isBooleanVariable(), storm::exceptions::InvalidSettingsException, "Terminal states refer to non-boolean variable '" << expressionOrLabelAndBool.first.getLabel() << "'."); + STORM_LOG_THROW(variable.isTransient(), storm::exceptions::InvalidSettingsException, "Terminal states refer to non-transient variable '" << expressionOrLabelAndBool.first.getLabel() << "'."); + + this->terminalStates.push_back(std::make_pair(this->model.getLabelExpression(variable.asBooleanVariable(), locationVariables), expressionOrLabelAndBool.second)); + } } } } @@ -116,7 +144,11 @@ namespace storm { auto resultIt = result.begin(); for (auto it = this->variableInformation.locationVariables.begin(), ite = this->variableInformation.locationVariables.end(); it != ite; ++it, ++resultIt) { - *resultIt = getLocation(state, *it); + if (it->bitWidth == 0) { + *resultIt = 0; + } else { + *resultIt = state.getAsInt(it->bitOffset, it->bitWidth); + } } return result; @@ -221,7 +253,7 @@ namespace storm { while (assignmentIt->getExpressionVariable() != boolIt->variable) { ++boolIt; } - newState.set(boolIt->bitOffset, this->evaluator.asBool(assignmentIt->getAssignedExpression())); + newState.set(boolIt->bitOffset, this->evaluator->asBool(assignmentIt->getAssignedExpression())); } // Iterate over all integer assignments and carry them out. @@ -230,7 +262,7 @@ namespace storm { while (assignmentIt->getExpressionVariable() != integerIt->variable) { ++integerIt; } - int_fast64_t assignedValue = this->evaluator.asInt(assignmentIt->getAssignedExpression()); + int_fast64_t assignedValue = this->evaluator->asInt(assignmentIt->getAssignedExpression()); STORM_LOG_THROW(assignedValue <= integerIt->upperBound, storm::exceptions::WrongFormatException, "The update " << assignmentIt->getExpressionVariable().getName() << " := " << assignmentIt->getAssignedExpression() << " leads to an out-of-bounds value (" << assignedValue << ") for the variable '" << assignmentIt->getExpressionVariable().getName() << "'."); newState.setFromInt(integerIt->bitOffset, integerIt->bitWidth, assignedValue - integerIt->lowerBound); STORM_LOG_ASSERT(static_cast(newState.getAsInt(integerIt->bitOffset, integerIt->bitWidth)) + integerIt->lowerBound == assignedValue, "Writing to the bit vector bucket failed (read " << newState.getAsInt(integerIt->bitOffset, integerIt->bitWidth) << " but wrote " << assignedValue << ")."); @@ -266,7 +298,7 @@ namespace storm { // If a terminal expression was set and we must not expand this state, return now. if (!this->terminalStates.empty()) { for (auto const& expressionBool : this->terminalStates) { - if (this->evaluator.asBool(expressionBool.first) == expressionBool.second) { + if (this->evaluator->asBool(expressionBool.first) == expressionBool.second) { return result; } } @@ -356,14 +388,14 @@ namespace storm { } // Skip the command, if it is not enabled. - if (!this->evaluator.asBool(edge.getGuard())) { + if (!this->evaluator->asBool(edge.getGuard())) { continue; } // Determine the exit rate if it's a Markovian edge. boost::optional exitRate = boost::none; if (edge.hasRate()) { - exitRate = this->evaluator.asRational(edge.getRate()); + exitRate = this->evaluator->asRational(edge.getRate()); } result.push_back(Choice(edge.getActionIndex(), static_cast(exitRate))); @@ -377,7 +409,7 @@ namespace storm { StateType stateIndex = stateToIdCallback(applyUpdate(state, destination, this->variableInformation.locationVariables[automatonIndex])); // Update the choice by adding the probability/target state to it. - ValueType probability = this->evaluator.asRational(destination.getProbability()); + ValueType probability = this->evaluator->asRational(destination.getProbability()); probability = exitRate ? exitRate.get() * probability : probability; choice.addProbability(stateIndex, probability); probabilitySum += probability; @@ -437,9 +469,9 @@ namespace storm { // and otherwise insert it. auto targetStateIt = newTargetStates->find(newTargetState); if (targetStateIt != newTargetStates->end()) { - targetStateIt->second += stateProbabilityPair.second * this->evaluator.asRational(destination.getProbability()); + targetStateIt->second += stateProbabilityPair.second * this->evaluator->asRational(destination.getProbability()); } else { - newTargetStates->emplace(newTargetState, stateProbabilityPair.second * this->evaluator.asRational(destination.getProbability())); + newTargetStates->emplace(newTargetState, stateProbabilityPair.second * this->evaluator->asRational(destination.getProbability())); } } @@ -525,7 +557,7 @@ namespace storm { std::vector edgePointers; for (auto const& edge : edges) { - if (this->evaluator.asBool(edge.getGuard())) { + if (this->evaluator->asBool(edge.getGuard())) { edgePointers.push_back(&edge); } } @@ -574,7 +606,32 @@ namespace storm { template storm::models::sparse::StateLabeling JaniNextStateGenerator::label(storm::storage::BitVectorHashMap const& states, std::vector const& initialStateIndices, std::vector const& deadlockStateIndices) { - return NextStateGenerator::label(states, initialStateIndices, deadlockStateIndices, {}); + + // Prepare a mapping from automata names to the location variables. + std::map locationVariables; + auto locationVariableIt = this->variableInformation.locationVariables.begin(); + for (auto const& automaton : model.getAutomata()) { + locationVariables[automaton.getName()] = locationVariableIt->variable; + ++locationVariableIt; + } + + // As in JANI we can use transient boolean variable assignments in locations to identify states, we need to + // create a list of boolean transient variables and the expressions that define them. + std::unordered_map transientVariableToExpressionMap; + for (auto const& variable : model.getGlobalVariables().getTransientVariables()) { + if (variable->isBooleanVariable()) { + if (this->options.isBuildAllLabelsSet() || this->options.getLabelNames().find(variable->getName()) != this->options.getLabelNames().end()) { + transientVariableToExpressionMap[variable->getExpressionVariable()] = model.getLabelExpression(variable->asBooleanVariable(), locationVariables); + } + } + } + + std::vector> transientVariableExpressions; + for (auto const& element : transientVariableToExpressionMap) { + transientVariableExpressions.push_back(std::make_pair(element.first.getName(), element.second)); + } + + return NextStateGenerator::label(states, initialStateIndices, deadlockStateIndices, transientVariableExpressions); } template @@ -595,7 +652,7 @@ namespace storm { if (rewardVariableIt == rewardVariableIte) { break; } else if (*rewardVariableIt == assignment.getExpressionVariable()) { - callback(ValueType(this->evaluator.asRational(assignment.getAssignedExpression()))); + callback(ValueType(this->evaluator->asRational(assignment.getAssignedExpression()))); ++rewardVariableIt; } } diff --git a/src/generator/JaniNextStateGenerator.h b/src/generator/JaniNextStateGenerator.h index 7855bc5cf..7d5907c21 100644 --- a/src/generator/JaniNextStateGenerator.h +++ b/src/generator/JaniNextStateGenerator.h @@ -105,7 +105,7 @@ namespace storm { * Checks the underlying model for validity for this next-state generator. */ void checkValid() const; - + /// The model used for the generation of next states. storm::jani::Model model; diff --git a/src/generator/NextStateGenerator.cpp b/src/generator/NextStateGenerator.cpp index 08fe61ba1..cf15f0a3f 100644 --- a/src/generator/NextStateGenerator.cpp +++ b/src/generator/NextStateGenerator.cpp @@ -224,12 +224,12 @@ namespace storm { } template - NextStateGenerator::NextStateGenerator(storm::expressions::ExpressionManager const& expressionManager, VariableInformation const& variableInformation, NextStateGeneratorOptions const& options) : options(options), expressionManager(expressionManager.getSharedPointer()), variableInformation(variableInformation), evaluator(expressionManager), state(nullptr) { + NextStateGenerator::NextStateGenerator(storm::expressions::ExpressionManager const& expressionManager, VariableInformation const& variableInformation, NextStateGeneratorOptions const& options) : options(options), expressionManager(expressionManager.getSharedPointer()), variableInformation(variableInformation), evaluator(nullptr), state(nullptr) { // Intentionally left empty. } template - NextStateGenerator::NextStateGenerator(storm::expressions::ExpressionManager const& expressionManager, NextStateGeneratorOptions const& options) : options(options), expressionManager(expressionManager.getSharedPointer()), variableInformation(), evaluator(expressionManager), state(nullptr) { + NextStateGenerator::NextStateGenerator(storm::expressions::ExpressionManager const& expressionManager, NextStateGeneratorOptions const& options) : options(options), expressionManager(expressionManager.getSharedPointer()), variableInformation(), evaluator(nullptr), state(nullptr) { // Intentionally left empty. } @@ -246,7 +246,7 @@ namespace storm { template void NextStateGenerator::load(CompressedState const& state) { // Since almost all subsequent operations are based on the evaluator, we load the state into it now. - unpackStateIntoEvaluator(state, variableInformation, evaluator); + unpackStateIntoEvaluator(state, variableInformation, *evaluator); // Also, we need to store a pointer to the state itself, because we need to be able to access it when expanding it. this->state = &state; @@ -257,7 +257,7 @@ namespace storm { if (expression.isTrue()) { return true; } - return evaluator.asBool(expression); + return evaluator->asBool(expression); } template @@ -282,11 +282,11 @@ namespace storm { result.addLabel(label.first); } for (auto const& stateIndexPair : states) { - unpackStateIntoEvaluator(stateIndexPair.first, variableInformation, this->evaluator); + unpackStateIntoEvaluator(stateIndexPair.first, variableInformation, *this->evaluator); for (auto const& label : labelsAndExpressions) { // Add label to state, if the corresponding expression is true. - if (evaluator.asBool(label.second)) { + if (evaluator->asBool(label.second)) { result.addLabelToState(label.first, stateIndexPair.second); } } diff --git a/src/generator/NextStateGenerator.h b/src/generator/NextStateGenerator.h index b2989b256..b9b7bfe23 100644 --- a/src/generator/NextStateGenerator.h +++ b/src/generator/NextStateGenerator.h @@ -211,7 +211,7 @@ namespace storm { VariableInformation variableInformation; /// An evaluator used to evaluate expressions. - storm::expressions::ExpressionEvaluator evaluator; + std::unique_ptr> evaluator; /// The currently loaded state. CompressedState const* state; diff --git a/src/generator/PrismNextStateGenerator.cpp b/src/generator/PrismNextStateGenerator.cpp index 6eceb0c26..e344ab13a 100644 --- a/src/generator/PrismNextStateGenerator.cpp +++ b/src/generator/PrismNextStateGenerator.cpp @@ -30,6 +30,9 @@ namespace storm { this->checkValid(); this->variableInformation = VariableInformation(program); + // Create a proper evalator. + this->evaluator = std::make_unique>(program.getManager()); + if (this->options.isBuildAllRewardModelsSet()) { for (auto const& rewardModel : this->program.getRewardModels()) { rewardModels.push_back(rewardModel); @@ -186,8 +189,8 @@ namespace storm { ValueType stateRewardValue = storm::utility::zero(); if (rewardModel.get().hasStateRewards()) { for (auto const& stateReward : rewardModel.get().getStateRewards()) { - if (this->evaluator.asBool(stateReward.getStatePredicateExpression())) { - stateRewardValue += ValueType(this->evaluator.asRational(stateReward.getRewardValueExpression())); + if (this->evaluator->asBool(stateReward.getStatePredicateExpression())) { + stateRewardValue += ValueType(this->evaluator->asRational(stateReward.getRewardValueExpression())); } } } @@ -197,7 +200,7 @@ namespace storm { // If a terminal expression was set and we must not expand this state, return now. if (!this->terminalStates.empty()) { for (auto const& expressionBool : this->terminalStates) { - if (this->evaluator.asBool(expressionBool.first) == expressionBool.second) { + if (this->evaluator->asBool(expressionBool.first) == expressionBool.second) { return result; } } @@ -252,8 +255,8 @@ namespace storm { if (rewardModel.get().hasStateActionRewards()) { for (auto const& stateActionReward : rewardModel.get().getStateActionRewards()) { for (auto const& choice : allChoices) { - if (stateActionReward.getActionIndex() == choice.getActionIndex() && this->evaluator.asBool(stateActionReward.getStatePredicateExpression())) { - stateActionRewardValue += ValueType(this->evaluator.asRational(stateActionReward.getRewardValueExpression())) * choice.getTotalMass() / totalExitRate; + if (stateActionReward.getActionIndex() == choice.getActionIndex() && this->evaluator->asBool(stateActionReward.getStatePredicateExpression())) { + stateActionRewardValue += ValueType(this->evaluator->asRational(stateActionReward.getRewardValueExpression())) * choice.getTotalMass() / totalExitRate; } } @@ -295,7 +298,7 @@ namespace storm { while (assignmentIt->getVariable() != boolIt->variable) { ++boolIt; } - newState.set(boolIt->bitOffset, this->evaluator.asBool(assignmentIt->getExpression())); + newState.set(boolIt->bitOffset, this->evaluator->asBool(assignmentIt->getExpression())); } // Iterate over all integer assignments and carry them out. @@ -304,7 +307,7 @@ namespace storm { while (assignmentIt->getVariable() != integerIt->variable) { ++integerIt; } - int_fast64_t assignedValue = this->evaluator.asInt(assignmentIt->getExpression()); + int_fast64_t assignedValue = this->evaluator->asInt(assignmentIt->getExpression()); STORM_LOG_THROW(assignedValue <= integerIt->upperBound, storm::exceptions::WrongFormatException, "The update " << update << " leads to an out-of-bounds value (" << assignedValue << ") for the variable '" << assignmentIt->getVariableName() << "'."); STORM_LOG_THROW(assignedValue >= integerIt->lowerBound, storm::exceptions::WrongFormatException, "The update " << update << " leads to an out-of-bounds value (" << assignedValue << ") for the variable '" << assignmentIt->getVariableName() << "'."); newState.setFromInt(integerIt->bitOffset, integerIt->bitWidth, assignedValue - integerIt->lowerBound); @@ -343,7 +346,7 @@ namespace storm { // Look up commands by their indices and add them if the guard evaluates to true in the given state. for (uint_fast64_t commandIndex : commandIndices) { storm::prism::Command const& command = module.getCommand(commandIndex); - if (this->evaluator.asBool(command.getGuardExpression())) { + if (this->evaluator->asBool(command.getGuardExpression())) { commands.push_back(command); } } @@ -376,7 +379,7 @@ namespace storm { if (command.isLabeled()) continue; // Skip the command, if it is not enabled. - if (!this->evaluator.asBool(command.getGuardExpression())) { + if (!this->evaluator->asBool(command.getGuardExpression())) { continue; } @@ -398,7 +401,7 @@ namespace storm { StateType stateIndex = stateToIdCallback(applyUpdate(state, update)); // Update the choice by adding the probability/target state to it. - ValueType probability = this->evaluator.asRational(update.getLikelihoodExpression()); + ValueType probability = this->evaluator->asRational(update.getLikelihoodExpression()); choice.addProbability(stateIndex, probability); probabilitySum += probability; } @@ -408,8 +411,8 @@ namespace storm { ValueType stateActionRewardValue = storm::utility::zero(); if (rewardModel.get().hasStateActionRewards()) { for (auto const& stateActionReward : rewardModel.get().getStateActionRewards()) { - if (stateActionReward.getActionIndex() == choice.getActionIndex() && this->evaluator.asBool(stateActionReward.getStatePredicateExpression())) { - stateActionRewardValue += ValueType(this->evaluator.asRational(stateActionReward.getRewardValueExpression())); + if (stateActionReward.getActionIndex() == choice.getActionIndex() && this->evaluator->asBool(stateActionReward.getStatePredicateExpression())) { + stateActionRewardValue += ValueType(this->evaluator->asRational(stateActionReward.getRewardValueExpression())); } } } @@ -462,9 +465,9 @@ namespace storm { // and otherwise insert it. auto targetStateIt = newTargetStates->find(newTargetState); if (targetStateIt != newTargetStates->end()) { - targetStateIt->second += stateProbabilityPair.second * this->evaluator.asRational(update.getLikelihoodExpression()); + targetStateIt->second += stateProbabilityPair.second * this->evaluator->asRational(update.getLikelihoodExpression()); } else { - newTargetStates->emplace(newTargetState, stateProbabilityPair.second * this->evaluator.asRational(update.getLikelihoodExpression())); + newTargetStates->emplace(newTargetState, stateProbabilityPair.second * this->evaluator->asRational(update.getLikelihoodExpression())); } } } @@ -509,8 +512,8 @@ namespace storm { ValueType stateActionRewardValue = storm::utility::zero(); if (rewardModel.get().hasStateActionRewards()) { for (auto const& stateActionReward : rewardModel.get().getStateActionRewards()) { - if (stateActionReward.getActionIndex() == choice.getActionIndex() && this->evaluator.asBool(stateActionReward.getStatePredicateExpression())) { - stateActionRewardValue += ValueType(this->evaluator.asRational(stateActionReward.getRewardValueExpression())); + if (stateActionReward.getActionIndex() == choice.getActionIndex() && this->evaluator->asBool(stateActionReward.getStatePredicateExpression())) { + stateActionRewardValue += ValueType(this->evaluator->asRational(stateActionReward.getRewardValueExpression())); } } } diff --git a/src/generator/VariableInformation.cpp b/src/generator/VariableInformation.cpp index 125e6089d..c1a00e4e6 100644 --- a/src/generator/VariableInformation.cpp +++ b/src/generator/VariableInformation.cpp @@ -2,6 +2,7 @@ #include "src/storage/prism/Program.h" #include "src/storage/jani/Model.h" +#include "src/storage/expressions/ExpressionManager.h" #include "src/utility/macros.h" #include "src/exceptions/InvalidArgumentException.h" @@ -19,7 +20,7 @@ namespace storm { // Intentionally left empty. } - LocationVariableInformation::LocationVariableInformation(uint64_t highestValue, uint_fast64_t bitOffset, uint_fast64_t bitWidth) : highestValue(highestValue), bitOffset(bitOffset), bitWidth(bitWidth) { + LocationVariableInformation::LocationVariableInformation(storm::expressions::Variable const& variable, uint64_t highestValue, uint_fast64_t bitOffset, uint_fast64_t bitWidth) : variable(variable), highestValue(highestValue), bitOffset(bitOffset), bitWidth(bitWidth) { // Intentionally left empty. } @@ -74,7 +75,7 @@ namespace storm { } for (auto const& automaton : model.getAutomata()) { uint_fast64_t bitwidth = static_cast(std::ceil(std::log2(automaton.getNumberOfLocations()))); - locationVariables.emplace_back(automaton.getNumberOfLocations() - 1, totalBitOffset, bitwidth); + locationVariables.emplace_back(model.getManager().declareFreshIntegerVariable(false, "loc"), automaton.getNumberOfLocations() - 1, totalBitOffset, bitwidth); totalBitOffset += bitwidth; for (auto const& variable : automaton.getVariables().getBooleanVariables()) { diff --git a/src/generator/VariableInformation.h b/src/generator/VariableInformation.h index 1aa8ee95c..0bbef3a6e 100644 --- a/src/generator/VariableInformation.h +++ b/src/generator/VariableInformation.h @@ -56,7 +56,10 @@ namespace storm { // A structure storing information about the location variables of the model. struct LocationVariableInformation { - LocationVariableInformation(uint64_t highestValue, uint_fast64_t bitOffset, uint_fast64_t bitWidth); + LocationVariableInformation(storm::expressions::Variable const& variable, uint64_t highestValue, uint_fast64_t bitOffset, uint_fast64_t bitWidth); + + // The expression variable for this location. + storm::expressions::Variable variable; // The highest possible location value. uint64_t highestValue; @@ -98,4 +101,4 @@ namespace storm { } } -#endif /* STORM_GENERATOR_VARIABLEINFORMATION_H_ */ \ No newline at end of file +#endif /* STORM_GENERATOR_VARIABLEINFORMATION_H_ */ diff --git a/src/storage/BitVector.h b/src/storage/BitVector.h index c8b81709f..ecdd03536 100644 --- a/src/storage/BitVector.h +++ b/src/storage/BitVector.h @@ -472,7 +472,7 @@ namespace storm { * value is equal to a call to size(), then there is no bit set after the specified position. * * @param startingIndex The index at which to start the search for the next bit that is set. The - * bit at this index itself is already considered. + * bit at this index itself is included in the search range. * @return The index of the next bit that is set after the given index. */ uint_fast64_t getNextSetIndex(uint_fast64_t startingIndex) const; diff --git a/src/storage/jani/Model.cpp b/src/storage/jani/Model.cpp index 343d88d78..ee2317df8 100644 --- a/src/storage/jani/Model.cpp +++ b/src/storage/jani/Model.cpp @@ -7,6 +7,7 @@ #include "src/utility/macros.h" #include "src/exceptions/WrongFormatException.h" +#include "src/exceptions/InvalidArgumentException.h" #include "src/exceptions/InvalidOperationException.h" #include "src/exceptions/InvalidTypeException.h" @@ -456,7 +457,39 @@ namespace storm { STORM_LOG_ASSERT(getModelType() != storm::jani::ModelType::UNDEFINED, "Model type not set"); STORM_LOG_ASSERT(!automata.empty(), "No automata set"); STORM_LOG_ASSERT(composition != nullptr, "Composition is not set"); + } + + storm::expressions::Expression Model::getLabelExpression(BooleanVariable const& transientVariable, std::map const& automatonToLocationVariableMap) const { + STORM_LOG_THROW(transientVariable.isTransient(), storm::exceptions::InvalidArgumentException, "Expected transient variable."); + + storm::expressions::Expression result; + bool negate = transientVariable.getInitExpression().isTrue(); + + for (auto const& automaton : this->getAutomata()) { + storm::expressions::Variable const& locationVariable = automatonToLocationVariableMap.at(automaton.getName()); + for (auto const& location : automaton.getLocations()) { + for (auto const& assignment : location.getAssignments().getTransientAssignments()) { + if (assignment.getExpressionVariable() == transientVariable.getExpressionVariable()) { + auto newExpression = (locationVariable == this->getManager().integer(automaton.getLocationIndex(location.getName()))) && (negate ? !assignment.getAssignedExpression() : assignment.getAssignedExpression()); + if (result.isInitialized()) { + result = result || newExpression; + } else { + result = newExpression; + } + } + } + } + } + if (result.isInitialized()) { + if (negate) { + result = !result; + } + } else { + result = this->getManager().boolean(negate); + } + + return result; } bool Model::hasStandardComposition() const { diff --git a/src/storage/jani/Model.h b/src/storage/jani/Model.h index 9a941a48f..35a74ead0 100644 --- a/src/storage/jani/Model.h +++ b/src/storage/jani/Model.h @@ -326,6 +326,12 @@ namespace storm { */ void checkValid() const; + /*! + * Creates the expression that characterizes all states in which the provided transient boolean variable is + * true. The provided location variables are used to encode the location of the automata. + */ + storm::expressions::Expression getLabelExpression(BooleanVariable const& transientVariable, std::map const& automatonToLocationVariableMap) const; + /*! * Checks that undefined constants (parameters) of the model preserve the graph of the underlying model. * That is, undefined constants may only appear in the probability expressions of edge destinations as well diff --git a/src/storage/jani/VariableSet.cpp b/src/storage/jani/VariableSet.cpp index a5468f63a..582fee73b 100644 --- a/src/storage/jani/VariableSet.cpp +++ b/src/storage/jani/VariableSet.cpp @@ -176,6 +176,26 @@ namespace storm { return result; } + uint_fast64_t VariableSet::getNumberOfRealTransientVariables() const { + uint_fast64_t result = 0; + for (auto const& variable : variables) { + if (variable->isTransient() && variable->isRealVariable()) { + ++result; + } + } + return result; + } + + uint_fast64_t VariableSet::getNumberOfUnboundedIntegerTransientVariables() const { + uint_fast64_t result = 0; + for (auto const& variable : variables) { + if (variable->isTransient() && variable->isUnboundedIntegerVariable()) { + ++result; + } + } + return result; + } + std::vector> VariableSet::getTransientVariables() const { std::vector> result; for (auto const& variable : variables) { diff --git a/src/storage/jani/VariableSet.h b/src/storage/jani/VariableSet.h index 1c947669e..031d56652 100644 --- a/src/storage/jani/VariableSet.h +++ b/src/storage/jani/VariableSet.h @@ -173,6 +173,16 @@ namespace storm { */ uint_fast64_t getNumberOfTransientVariables() const; + /*! + * Retrieves the number of real transient variables in this variable set. + */ + uint_fast64_t getNumberOfRealTransientVariables() const; + + /*! + * Retrieves the number of unbounded integer transient variables in this variable set. + */ + uint_fast64_t getNumberOfUnboundedIntegerTransientVariables() const; + /*! * Retrieves a vector of transient variables in this variable set. */ From a265bc49ce317ca510b35a802686bc5658dfac09 Mon Sep 17 00:00:00 2001 From: sjunges Date: Tue, 11 Oct 2016 18:02:14 +0200 Subject: [PATCH 03/13] check if transient values are actually given before looping over them Former-commit-id: 60e15907adaf37c418afe2ba7f9b728810efd545 [formerly 15cbc28a4f8b8e252058e2c2e83f119ddaf95caf] Former-commit-id: a3ed467329ecf2a5fa8bc6ea6d0d425adaf32a32 --- src/parser/JaniParser.cpp | 19 +++++++++++-------- 1 file changed, 11 insertions(+), 8 deletions(-) diff --git a/src/parser/JaniParser.cpp b/src/parser/JaniParser.cpp index ebcb07d4a..a7def4b2a 100644 --- a/src/parser/JaniParser.cpp +++ b/src/parser/JaniParser.cpp @@ -586,13 +586,15 @@ namespace storm { 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("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")) { - STORM_LOG_THROW(transientValueEntry.count("ref") == 1, storm::exceptions::InvalidJaniException, "Transient values in location " << locName << " need exactly one ref that is assigned to"); - STORM_LOG_THROW(transientValueEntry.count("value") == 1, storm::exceptions::InvalidJaniException, "Transient values in location " << locName << " need exactly one assigned value"); - storm::jani::Variable const& lhs = getLValue(transientValueEntry.at("ref"), parentModel.getGlobalVariables(), automaton.getVariables(), "LHS of assignment in location " + locName + " (automaton '" + name + "')"); - STORM_LOG_THROW(lhs.isTransient(), storm::exceptions::InvalidJaniException, "Assigned non-transient variable " + lhs.getName() + " in location " + locName + " (automaton: '" + name + "')"); - storm::expressions::Expression rhs = parseExpression(transientValueEntry.at("value"), "Assignment of variable " + lhs.getName() + " in location " + locName + " (automaton: '" + name + "')"); - transientAssignments.emplace_back(lhs, rhs); + if(locEntry.count("transient-values") > 0) { + for(auto const& transientValueEntry : locEntry.at("transient-values")) { + STORM_LOG_THROW(transientValueEntry.count("ref") == 1, storm::exceptions::InvalidJaniException, "Transient values in location " << locName << " need exactly one ref that is assigned to"); + STORM_LOG_THROW(transientValueEntry.count("value") == 1, storm::exceptions::InvalidJaniException, "Transient values in location " << locName << " need exactly one assigned value"); + storm::jani::Variable const& lhs = getLValue(transientValueEntry.at("ref"), parentModel.getGlobalVariables(), automaton.getVariables(), "LHS of assignment in location " + locName + " (automaton '" + name + "')"); + STORM_LOG_THROW(lhs.isTransient(), storm::exceptions::InvalidJaniException, "Assigned non-transient variable " + lhs.getName() + " in location " + locName + " (automaton: '" + name + "')"); + storm::expressions::Expression rhs = parseExpression(transientValueEntry.at("value"), "Assignment of variable " + lhs.getName() + " in location " + locName + " (automaton: '" + name + "')"); + transientAssignments.emplace_back(lhs, rhs); + } } uint64_t id = automaton.addLocation(storm::jani::Location(locName, transientAssignments)); locIds.emplace(locName, id); @@ -639,7 +641,8 @@ namespace storm { STORM_LOG_THROW(edgeEntry.count("rate") < 2, storm::exceptions::InvalidJaniException, "Edge from '" << sourceLoc << "' in automaton '" << name << "' has multiple rates"); storm::expressions::Expression rateExpr; if(edgeEntry.count("rate") > 0) { - rateExpr = parseExpression(edgeEntry.at("rate"), "rate expression in edge from '" + sourceLoc + "' in automaton '" + name + "'"); + STORM_LOG_THROW(edgeEntry.at("rate").count("exp") == 1, storm::exceptions::InvalidJaniException, "Rate in edge from '" << sourceLoc << "' in automaton '" << name << "' must have a defing expression."); + rateExpr = parseExpression(edgeEntry.at("rate").at("exp"), "rate expression in edge from '" + sourceLoc + "' in automaton '" + name + "'"); STORM_LOG_THROW(rateExpr.hasNumericalType(), storm::exceptions::InvalidJaniException, "Rate '" << rateExpr << "' has not a numerical type"); } // guard From 12a5258a45839113b6f15cc8de9e2bba33442283 Mon Sep 17 00:00:00 2001 From: sjunges Date: Tue, 11 Oct 2016 22:32:49 +0200 Subject: [PATCH 04/13] second time is a charm Former-commit-id: 9af436c8430d7f7665f885a8270dbf1c6974f279 [formerly 0594ee49f8b828485722b544ed48f386d2ed42f8] Former-commit-id: db0f6c4dc3e0753b169441dd5e1b487cfdc6d773 --- src/parser/JaniParser.cpp | 58 +++++++++++++++++++++------------------ 1 file changed, 32 insertions(+), 26 deletions(-) diff --git a/src/parser/JaniParser.cpp b/src/parser/JaniParser.cpp index a7def4b2a..a49ab5548 100644 --- a/src/parser/JaniParser.cpp +++ b/src/parser/JaniParser.cpp @@ -697,24 +697,42 @@ namespace storm { return automaton; } + + std::vector parseSyncVectors(json const& syncVectorStructure) { + std::vector syncVectors; + // TODO add error checks + for (auto const& syncEntry : syncVectorStructure) { + std::vector inputs; + for (auto const& syncInput : syncEntry.at("synchronise")) { + if(syncInput.is_null()) { + // TODO handle null; + } else { + inputs.push_back(syncInput); + } + } + std::string syncResult = syncEntry.at("result"); + syncVectors.emplace_back(inputs, syncResult); + } + return syncVectors; + } std::shared_ptr JaniParser::parseComposition(json const &compositionStructure) { + if(compositionStructure.count("automaton")) { + return std::shared_ptr(new storm::jani::AutomatonComposition(compositionStructure.at("automaton").get())); + } - STORM_LOG_THROW(compositionStructure.count("elements") == 1, storm::exceptions::InvalidJaniException, "Elements of a composition must be given"); + STORM_LOG_THROW(compositionStructure.count("elements") == 1, storm::exceptions::InvalidJaniException, "Elements of a composition must be given, got " << compositionStructure.dump()); - if (compositionStructure.at("elements").size() == 1) { - if (compositionStructure.count("syncs") == 0) { - // We might have an automaton. - STORM_LOG_THROW(compositionStructure.at("elements").back().count("automaton") == 1, storm::exceptions::InvalidJaniException, "Automaton must be given in composition"); - if (compositionStructure.at("elements").back().at("automaton").is_string()) { - std::string name = compositionStructure.at("elements").back().at("automaton"); - // TODO check whether name exist? - return std::shared_ptr(new storm::jani::AutomatonComposition(name)); - } - STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Nesting parallel composition is not supported"); - } else { - // Might be rename or input-enable. + if (compositionStructure.at("elements").size() == 1 && compositionStructure.count("syncs") == 0) { + // We might have an automaton. + STORM_LOG_THROW(compositionStructure.at("elements").back().count("automaton") == 1, storm::exceptions::InvalidJaniException, "Automaton must be given in composition"); + if (compositionStructure.at("elements").back().at("automaton").is_string()) { + std::string name = compositionStructure.at("elements").back().at("automaton"); + // TODO check whether name exist? + return std::shared_ptr(new storm::jani::AutomatonComposition(name)); } + STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Trivial nesting parallel composition is not yet supported"); + } std::vector> compositions; @@ -728,19 +746,7 @@ namespace storm { STORM_LOG_THROW(compositionStructure.count("syncs") < 2, storm::exceptions::InvalidJaniException, "Sync vectors can be given at most once"); std::vector syncVectors; if (compositionStructure.count("syncs") > 0) { - // TODO add error checks - for (auto const& syncEntry : compositionStructure.at("syncs")) { - std::vector inputs; - for (auto const& syncInput : syncEntry.at("synchronise")) { - if(syncInput.is_null()) { - // TODO handle null; - } else { - inputs.push_back(syncInput); - } - } - std::string syncResult = syncEntry.at("result"); - syncVectors.emplace_back(inputs, syncResult); - } + syncVectors = parseSyncVectors(compositionStructure.at("syncs")); } return std::shared_ptr(new storm::jani::ParallelComposition(compositions, syncVectors)); From 011e3fbaa65c06f67a9ca1258bfc444848bd62a4 Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 12 Oct 2016 13:54:29 +0200 Subject: [PATCH 05/13] fixed bug that introduced transient variables in the state space Former-commit-id: b335cf0c0dae3be17160ec6ca44a29c72996b6f9 [formerly 84339f7943cc25252bd8ccd6addc84401e643d2c] Former-commit-id: 6f64020873265b23e9af9cc6c816045ec13d2ce8 --- src/generator/JaniNextStateGenerator.cpp | 4 ++- src/generator/VariableInformation.cpp | 36 +++++++++++++++--------- 2 files changed, 25 insertions(+), 15 deletions(-) diff --git a/src/generator/JaniNextStateGenerator.cpp b/src/generator/JaniNextStateGenerator.cpp index bc166cba3..10053d777 100644 --- a/src/generator/JaniNextStateGenerator.cpp +++ b/src/generator/JaniNextStateGenerator.cpp @@ -178,17 +178,19 @@ namespace storm { std::shared_ptr model = solver->getModel(); for (auto const& booleanVariable : this->variableInformation.booleanVariables) { bool variableValue = model->getBooleanValue(booleanVariable.variable); + std::cout << booleanVariable.variable.getName() << " has val " << variableValue << std::endl; storm::expressions::Expression localBlockingExpression = variableValue ? !booleanVariable.variable : booleanVariable.variable; blockingExpression = blockingExpression.isInitialized() ? blockingExpression || localBlockingExpression : localBlockingExpression; initialState.set(booleanVariable.bitOffset, variableValue); } for (auto const& integerVariable : this->variableInformation.integerVariables) { int_fast64_t variableValue = model->getIntegerValue(integerVariable.variable); + std::cout << integerVariable.variable.getName() << " has val " << variableValue << std::endl; storm::expressions::Expression localBlockingExpression = integerVariable.variable != model->getManager().integer(variableValue); blockingExpression = blockingExpression.isInitialized() ? blockingExpression || localBlockingExpression : localBlockingExpression; initialState.setFromInt(integerVariable.bitOffset, integerVariable.bitWidth, static_cast(variableValue - integerVariable.lowerBound)); } - + // Gather iterators to the initial locations of all the automata. std::vector::const_iterator> initialLocationsIterators; uint64_t currentLocationVariable = 0; diff --git a/src/generator/VariableInformation.cpp b/src/generator/VariableInformation.cpp index c1a00e4e6..3545f1e49 100644 --- a/src/generator/VariableInformation.cpp +++ b/src/generator/VariableInformation.cpp @@ -63,15 +63,19 @@ namespace storm { } for (auto const& variable : model.getGlobalVariables().getBooleanVariables()) { - booleanVariables.emplace_back(variable.getExpressionVariable(), totalBitOffset, true); - ++totalBitOffset; + if (!variable.isTransient()) { + booleanVariables.emplace_back(variable.getExpressionVariable(), totalBitOffset, true); + ++totalBitOffset; + } } for (auto const& variable : model.getGlobalVariables().getBoundedIntegerVariables()) { - int_fast64_t lowerBound = variable.getLowerBound().evaluateAsInt(); - int_fast64_t upperBound = variable.getUpperBound().evaluateAsInt(); - uint_fast64_t bitwidth = static_cast(std::ceil(std::log2(upperBound - lowerBound + 1))); - integerVariables.emplace_back(variable.getExpressionVariable(), lowerBound, upperBound, totalBitOffset, bitwidth, true); - totalBitOffset += bitwidth; + if (!variable.isTransient()) { + int_fast64_t lowerBound = variable.getLowerBound().evaluateAsInt(); + int_fast64_t upperBound = variable.getUpperBound().evaluateAsInt(); + uint_fast64_t bitwidth = static_cast(std::ceil(std::log2(upperBound - lowerBound + 1))); + integerVariables.emplace_back(variable.getExpressionVariable(), lowerBound, upperBound, totalBitOffset, bitwidth, true); + totalBitOffset += bitwidth; + } } for (auto const& automaton : model.getAutomata()) { uint_fast64_t bitwidth = static_cast(std::ceil(std::log2(automaton.getNumberOfLocations()))); @@ -79,15 +83,19 @@ namespace storm { totalBitOffset += bitwidth; for (auto const& variable : automaton.getVariables().getBooleanVariables()) { - booleanVariables.emplace_back(variable.getExpressionVariable(), totalBitOffset); - ++totalBitOffset; + if (!variable.isTransient()) { + booleanVariables.emplace_back(variable.getExpressionVariable(), totalBitOffset); + ++totalBitOffset; + } } for (auto const& variable : automaton.getVariables().getBoundedIntegerVariables()) { - int_fast64_t lowerBound = variable.getLowerBound().evaluateAsInt(); - int_fast64_t upperBound = variable.getUpperBound().evaluateAsInt(); - uint_fast64_t bitwidth = static_cast(std::ceil(std::log2(upperBound - lowerBound + 1))); - integerVariables.emplace_back(variable.getExpressionVariable(), lowerBound, upperBound, totalBitOffset, bitwidth); - totalBitOffset += bitwidth; + if (!variable.isTransient()) { + int_fast64_t lowerBound = variable.getLowerBound().evaluateAsInt(); + int_fast64_t upperBound = variable.getUpperBound().evaluateAsInt(); + uint_fast64_t bitwidth = static_cast(std::ceil(std::log2(upperBound - lowerBound + 1))); + integerVariables.emplace_back(variable.getExpressionVariable(), lowerBound, upperBound, totalBitOffset, bitwidth); + totalBitOffset += bitwidth; + } } } From 91e6bb299923773a89fcb9ea649465f7a9283c7c Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 12 Oct 2016 15:14:47 +0200 Subject: [PATCH 06/13] fixed bug in DD-based JANI model generation related to transient edge assignments Former-commit-id: b2cf168189706f22201bf54c00cd0f822acbbd14 [formerly 0c50ca2d16cc56b2c1a12db38b6736d79e6780c7] Former-commit-id: 05686fd6f1b6198355e31940b5b764998047810a --- src/builder/DdJaniModelBuilder.cpp | 8 +++++--- src/generator/JaniNextStateGenerator.cpp | 2 -- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/src/builder/DdJaniModelBuilder.cpp b/src/builder/DdJaniModelBuilder.cpp index 8b54e0eba..1b759cfc5 100644 --- a/src/builder/DdJaniModelBuilder.cpp +++ b/src/builder/DdJaniModelBuilder.cpp @@ -895,7 +895,6 @@ namespace storm { if (action.isInputEnabled()) { // If the action is input-enabled, we add self-loops to all states. transitions *= actionGuard.ite(action.transitions, encodeIndex(0, action.getLowestLocalNondeterminismVariable(), action.getHighestLocalNondeterminismVariable() - action.getLowestLocalNondeterminismVariable(), this->variables) * actionIdentityPair.second); - actionGuard.ite(action.transitions, encodeIndex(0, action.getLowestLocalNondeterminismVariable(), action.getHighestLocalNondeterminismVariable() - action.getLowestLocalNondeterminismVariable(), this->variables) * actionIdentityPair.second).exportToDot("this.dot"); } else { transitions *= action.transitions; } @@ -1107,7 +1106,8 @@ namespace storm { } // Add the source location and the guard. - transitions *= this->variables.manager->getEncoding(this->variables.automatonToLocationDdVariableMap.at(automaton.getName()).first, edge.getSourceLocationIndex()).template toAdd() * guard; + storm::dd::Add sourceLocationAndGuard = this->variables.manager->getEncoding(this->variables.automatonToLocationDdVariableMap.at(automaton.getName()).first, edge.getSourceLocationIndex()).template toAdd() * guard; + transitions *= sourceLocationAndGuard; // If we multiply the ranges of global variables, make sure everything stays within its bounds. if (!globalVariablesInSomeDestination.empty()) { @@ -1124,7 +1124,9 @@ namespace storm { // Finally treat the transient assignments. std::map> transientEdgeAssignments; if (!this->transientVariables.empty()) { - performTransientAssignments(edge.getAssignments().getTransientAssignments(), [this, &transientEdgeAssignments, &guard] (storm::jani::Assignment const& assignment) { transientEdgeAssignments[assignment.getExpressionVariable()] = guard * this->variables.rowExpressionAdapter->translateExpression(assignment.getAssignedExpression()); } ); + performTransientAssignments(edge.getAssignments().getTransientAssignments(), [this, &transientEdgeAssignments, &guard, &sourceLocationAndGuard] (storm::jani::Assignment const& assignment) { + transientEdgeAssignments[assignment.getExpressionVariable()] = sourceLocationAndGuard * this->variables.rowExpressionAdapter->translateExpression(assignment.getAssignedExpression()); + } ); } return EdgeDd(isMarkovian, guard, guard * transitions, transientEdgeAssignments, globalVariablesInSomeDestination); diff --git a/src/generator/JaniNextStateGenerator.cpp b/src/generator/JaniNextStateGenerator.cpp index 10053d777..b2c786b77 100644 --- a/src/generator/JaniNextStateGenerator.cpp +++ b/src/generator/JaniNextStateGenerator.cpp @@ -178,14 +178,12 @@ namespace storm { std::shared_ptr model = solver->getModel(); for (auto const& booleanVariable : this->variableInformation.booleanVariables) { bool variableValue = model->getBooleanValue(booleanVariable.variable); - std::cout << booleanVariable.variable.getName() << " has val " << variableValue << std::endl; storm::expressions::Expression localBlockingExpression = variableValue ? !booleanVariable.variable : booleanVariable.variable; blockingExpression = blockingExpression.isInitialized() ? blockingExpression || localBlockingExpression : localBlockingExpression; initialState.set(booleanVariable.bitOffset, variableValue); } for (auto const& integerVariable : this->variableInformation.integerVariables) { int_fast64_t variableValue = model->getIntegerValue(integerVariable.variable); - std::cout << integerVariable.variable.getName() << " has val " << variableValue << std::endl; storm::expressions::Expression localBlockingExpression = integerVariable.variable != model->getManager().integer(variableValue); blockingExpression = blockingExpression.isInitialized() ? blockingExpression || localBlockingExpression : localBlockingExpression; initialState.setFromInt(integerVariable.bitOffset, integerVariable.bitWidth, static_cast(variableValue - integerVariable.lowerBound)); From ba0d81ca52172d4bd68fbf10c7a60a3714dc29d2 Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 12 Oct 2016 21:13:09 +0200 Subject: [PATCH 07/13] bugfix for PRISM program: only check initial values of variables if they have one Former-commit-id: c5c548bd62f28b1d2cdc70bb75f7c84d12233c62 [formerly c27c72bd59e9f07a05cb8e9c5f56b65906ff7a2f] Former-commit-id: 97acb66693b15d0464a7dbc15c70a13c73f60f10 --- src/storage/prism/Module.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/storage/prism/Module.cpp b/src/storage/prism/Module.cpp index 095ac3e11..0a4347396 100644 --- a/src/storage/prism/Module.cpp +++ b/src/storage/prism/Module.cpp @@ -196,12 +196,12 @@ namespace storm { bool Module::containsVariablesOnlyInUpdateProbabilities(std::set const& undefinedConstantVariables) const { for (auto const& booleanVariable : this->getBooleanVariables()) { - if (booleanVariable.getInitialValueExpression().containsVariable(undefinedConstantVariables)) { + if (booleanVariable.hasInitialValue() && booleanVariable.getInitialValueExpression().containsVariable(undefinedConstantVariables)) { return false; } } for (auto const& integerVariable : this->getIntegerVariables()) { - if (integerVariable.getInitialValueExpression().containsVariable(undefinedConstantVariables)) { + if (integerVariable.hasInitialValue() && integerVariable.getInitialValueExpression().containsVariable(undefinedConstantVariables)) { return false; } if (integerVariable.getLowerBoundExpression().containsVariable(undefinedConstantVariables)) { From aee1956950574f7eec41df0c4fde4ce6fa11b9ee Mon Sep 17 00:00:00 2001 From: sjunges Date: Thu, 13 Oct 2016 15:03:57 +0200 Subject: [PATCH 08/13] progress towards JANI formula support, fix for gcc Former-commit-id: 66d87dbe8c40c58166f90e538fd647ac33955a12 [formerly ac7ce466a1c796d6356af6ba0bcdb03672a721c7] Former-commit-id: ec11ee9831b08c93c45f758ac62d4803b2b0545c --- src/storage/jani/JSONExporter.cpp | 197 ++++++++++++++++++++++++++++++ src/storage/jani/JSONExporter.h | 27 ++++ src/storage/jani/Property.cpp | 15 +-- src/storage/jani/Property.h | 32 +++-- src/storage/ppg/defines.h | 2 + 5 files changed, 257 insertions(+), 16 deletions(-) diff --git a/src/storage/jani/JSONExporter.cpp b/src/storage/jani/JSONExporter.cpp index 3493affe4..be30b82b8 100644 --- a/src/storage/jani/JSONExporter.cpp +++ b/src/storage/jani/JSONExporter.cpp @@ -6,6 +6,7 @@ #include "src/utility/macros.h" #include "src/exceptions/FileIoException.h" +#include "src/exceptions/NotSupportedException.h" #include "src/exceptions/InvalidJaniException.h" @@ -20,6 +21,8 @@ #include "src/storage/expressions/BinaryRelationExpression.h" #include "src/storage/expressions/VariableExpression.h" +#include "src/logic/Formulas.h" + #include "src/storage/jani/AutomatonComposition.h" #include "src/storage/jani/ParallelComposition.h" @@ -85,6 +88,200 @@ namespace storm { bool allowRecursion; }; + std::string comparisonTypeToJani(storm::logic::ComparisonType ct) { + switch(ct) { + case storm::logic::ComparisonType::Less: + return "<"; + case storm::logic::ComparisonType::LessEqual: + return "≤"; + case storm::logic::ComparisonType::Greater: + return ">"; + case storm::logic::ComparisonType::GreaterEqual: + return "≥"; + } + } + + modernjson::json numberToJson(storm::RationalNumber rn) { + modernjson::json numDecl; + if(carl::isOne(carl::getDenom(rn))) { + numDecl = modernjson::json(carl::toString(carl::getNum(rn))); + } else { + numDecl["op"] = "/"; + numDecl["left"] = carl::toString(carl::getNum(rn)); + numDecl["right"] = carl::toString(carl::getDenom(rn)); + } + return numDecl; + } + + + modernjson::json constructPropertyInterval(uint64_t lower, uint64_t upper) { + modernjson::json iDecl; + iDecl["lower"] = lower; + iDecl["upper"] = upper; + return iDecl; + } + + modernjson::json constructPropertyInterval(double lower, double upper) { + modernjson::json iDecl; + iDecl["lower"] = lower; + iDecl["upper"] = upper; + return iDecl; + } + + boost::any FormulaToJaniJson::visit(storm::logic::AtomicExpressionFormula const& f, boost::any const& data) const { + return ExpressionToJson::translate(f.getExpression()); + } + + boost::any FormulaToJaniJson::visit(storm::logic::AtomicLabelFormula const& f, boost::any const& data) const { + modernjson::json opDecl(f.isTrueFormula() ? "true" : "false"); + return opDecl; + } + boost::any FormulaToJaniJson::visit(storm::logic::BinaryBooleanStateFormula const& f, boost::any const& data) const{ + modernjson::json opDecl; + storm::logic::BinaryBooleanStateFormula::OperatorType op = f.getOperator(); + opDecl["op"] = op == storm::logic::BinaryBooleanStateFormula::OperatorType::And ? "∧" : "∨"; + opDecl["left"] = boost::any_cast(f.getLeftSubformula().accept(*this, boost::none)); + opDecl["right"] = boost::any_cast(f.getRightSubformula().accept(*this, boost::none)); + return opDecl; + } + boost::any FormulaToJaniJson::visit(storm::logic::BooleanLiteralFormula const& f, boost::any const& data) const { + modernjson::json opDecl(f.isTrueFormula() ? "true" : "false"); + return opDecl; + } + boost::any FormulaToJaniJson::visit(storm::logic::BoundedUntilFormula const& f, boost::any const& data) const { + modernjson::json opDecl; + opDecl["op"] = "U"; + opDecl["left"] = boost::any_cast(f.getLeftSubformula().accept(*this, boost::none)); + opDecl["right"] = boost::any_cast(f.getRightSubformula().accept(*this, boost::none)); + if(f.hasDiscreteTimeBound()) { + opDecl["step-bounds"] = constructPropertyInterval(0, f.getDiscreteTimeBound()); + } else { + opDecl["time-bounds"] = constructPropertyInterval(f.getIntervalBounds().first, f.getIntervalBounds().second); + } + return opDecl; + } + + boost::any FormulaToJaniJson::visit(storm::logic::ConditionalFormula const& f, boost::any const& data) const { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Jani currently does not support conditional formulae"); + } + + boost::any FormulaToJaniJson::visit(storm::logic::CumulativeRewardFormula const& f, boost::any const& data) const { + + } + + boost::any FormulaToJaniJson::visit(storm::logic::EventuallyFormula const& f, boost::any const& data) const { + modernjson::json opDecl; + opDecl["op"] = "U"; + opDecl["left"] = boost::any_cast(f.getTrueFormula()->accept(*this, boost::none)); + opDecl["right"] = boost::any_cast(f.getSubformula().accept(*this, boost::none)); + return opDecl; + } + + boost::any FormulaToJaniJson::visit(storm::logic::TimeOperatorFormula const& f, boost::any const& data) const { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Jani currently does not support conditional formulae"); + + } + + boost::any FormulaToJaniJson::visit(storm::logic::GloballyFormula const& f, boost::any const& data) const { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Jani currently does not support conditional formulae"); + } + + boost::any FormulaToJaniJson::visit(storm::logic::InstantaneousRewardFormula const& f, boost::any const& data) const { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Jani currently does not support conditional formulae"); + } + + boost::any FormulaToJaniJson::visit(storm::logic::LongRunAverageOperatorFormula const& f, boost::any const& data) const { + modernjson::json opDecl; + if(f.hasBound()) { + auto bound = f.getBound(); + opDecl["op"] = comparisonTypeToJani(bound.comparisonType); + if(f.hasOptimalityType()) { + opDecl["left"]["op"] = f.getOptimalityType() == storm::solver::OptimizationDirection::Minimize ? "Smin" : "Smax"; + opDecl["left"]["exp"] = boost::any_cast(f.getSubformula().accept(*this, boost::none)); + } else { + opDecl["left"]["op"] = (bound.comparisonType == storm::logic::ComparisonType::Less || bound.comparisonType == storm::logic::ComparisonType::LessEqual) ? "Smax" : "Smin"; + opDecl["left"]["exp"] = boost::any_cast(f.getSubformula().accept(*this, boost::none)); + } + opDecl["right"] = numberToJson(bound.threshold); + } else { + if(f.hasOptimalityType()) { + opDecl["op"] = f.getOptimalityType() == storm::solver::OptimizationDirection::Minimize ? "Smin" : "Smax"; + opDecl["exp"] = boost::any_cast(f.getSubformula().accept(*this, boost::none)); + + } else { + // TODO add checks + opDecl["op"] = "Pmin"; + opDecl["exp"] = boost::any_cast(f.getSubformula().accept(*this, boost::none)); + } + } + return opDecl; + + } + + boost::any FormulaToJaniJson::visit(storm::logic::LongRunAverageRewardFormula const& f, boost::any const& data) const { + + } + + boost::any FormulaToJaniJson::visit(storm::logic::NextFormula const& f, boost::any const& data) const { + modernjson::json opDecl; + opDecl["op"] = "U"; + opDecl["left"] = boost::any_cast(f.getTrueFormula()->accept(*this, boost::none)); + opDecl["right"] = boost::any_cast(f.getSubformula().accept(*this, boost::none)); + opDecl["step-bounds"] = constructPropertyInterval((uint64_t)1, (uint64_t)1); + return opDecl; + } + + + + + boost::any FormulaToJaniJson::visit(storm::logic::ProbabilityOperatorFormula const& f, boost::any const& data) const { + modernjson::json opDecl; + + if(f.hasBound()) { + auto bound = f.getBound(); + opDecl["op"] = comparisonTypeToJani(bound.comparisonType); + if(f.hasOptimalityType()) { + opDecl["left"]["op"] = f.getOptimalityType() == storm::solver::OptimizationDirection::Minimize ? "Pmin" : "Pmax"; + opDecl["left"]["exp"] = boost::any_cast(f.getSubformula().accept(*this, boost::none)); + } else { + opDecl["left"]["op"] = (bound.comparisonType == storm::logic::ComparisonType::Less || bound.comparisonType == storm::logic::ComparisonType::LessEqual) ? "Pmax" : "Pmin"; + opDecl["left"]["exp"] = boost::any_cast(f.getSubformula().accept(*this, boost::none)); + } + opDecl["right"] = numberToJson(bound.threshold); + } else { + if(f.hasOptimalityType()) { + opDecl["op"] = f.getOptimalityType() == storm::solver::OptimizationDirection::Minimize ? "Pmin" : "Pmax"; + opDecl["exp"] = boost::any_cast(f.getSubformula().accept(*this, boost::none)); + + } else { + // TODO add checks + opDecl["op"] = "Pmin"; + opDecl["exp"] = boost::any_cast(f.getSubformula().accept(*this, boost::none)); + } + } + return opDecl; + } + + boost::any FormulaToJaniJson::visit(storm::logic::RewardOperatorFormula const& f, boost::any const& data) const { + + } + + boost::any FormulaToJaniJson::visit(storm::logic::UnaryBooleanStateFormula const& f, boost::any const& data) const { + modernjson::json opDecl; + storm::logic::UnaryBooleanStateFormula::OperatorType op = f.getOperator(); + assert(op == storm::logic::UnaryBooleanStateFormula::OperatorType::Not); + opDecl["op"] = "¬"; + opDecl["exp"] = boost::any_cast(f.getSubformula().accept(*this, boost::none)); + return opDecl; + } + + boost::any FormulaToJaniJson::visit(storm::logic::UntilFormula const& f, boost::any const& data) const { + modernjson::json opDecl; + opDecl["op"] = "U"; + opDecl["left"] = boost::any_cast(f.getLeftSubformula().accept(*this, boost::none)); + opDecl["right"] = boost::any_cast(f.getRightSubformula().accept(*this, boost::none)); + return opDecl; + } std::string operatorTypeToJaniString(storm::expressions::OperatorType optype) { diff --git a/src/storage/jani/JSONExporter.h b/src/storage/jani/JSONExporter.h index 604a27a47..ff54de5e8 100644 --- a/src/storage/jani/JSONExporter.h +++ b/src/storage/jani/JSONExporter.h @@ -2,6 +2,7 @@ #include "src/storage/expressions/ExpressionVisitor.h" +#include "src/logic/FormulaVisitor.h" #include "Model.h" // JSON parser #include "json.hpp" @@ -28,6 +29,31 @@ namespace storm { }; + class FormulaToJaniJson : public storm::logic::FormulaVisitor { + public: + static modernjson::json translate(storm::logic::Formula const& formula); + virtual boost::any visit(storm::logic::AtomicExpressionFormula const& f, boost::any const& data) const; + virtual boost::any visit(storm::logic::AtomicLabelFormula const& f, boost::any const& data) const; + virtual boost::any visit(storm::logic::BinaryBooleanStateFormula const& f, boost::any const& data) const; + virtual boost::any visit(storm::logic::BooleanLiteralFormula const& f, boost::any const& data) const; + virtual boost::any visit(storm::logic::BoundedUntilFormula const& f, boost::any const& data) const; + virtual boost::any visit(storm::logic::ConditionalFormula const& f, boost::any const& data) const; + virtual boost::any visit(storm::logic::CumulativeRewardFormula const& f, boost::any const& data) const; + virtual boost::any visit(storm::logic::EventuallyFormula const& f, boost::any const& data) const; + virtual boost::any visit(storm::logic::TimeOperatorFormula const& f, boost::any const& data) const; + virtual boost::any visit(storm::logic::GloballyFormula const& f, boost::any const& data) const; + virtual boost::any visit(storm::logic::InstantaneousRewardFormula const& f, boost::any const& data) const; + virtual boost::any visit(storm::logic::LongRunAverageOperatorFormula const& f, boost::any const& data) const; + virtual boost::any visit(storm::logic::LongRunAverageRewardFormula const& f, boost::any const& data) const; + virtual boost::any visit(storm::logic::NextFormula const& f, boost::any const& data) const; + virtual boost::any visit(storm::logic::ProbabilityOperatorFormula const& f, boost::any const& data) const; + virtual boost::any visit(storm::logic::RewardOperatorFormula const& f, boost::any const& data) const; + virtual boost::any visit(storm::logic::UnaryBooleanStateFormula const& f, boost::any const& data) const; + virtual boost::any visit(storm::logic::UntilFormula const& f, boost::any const& data) const; + + + }; + class JsonExporter { JsonExporter() = default; @@ -37,6 +63,7 @@ namespace storm { private: void convertModel(storm::jani::Model const& model); + void convertProperty(storm::logic::Formula const& formula); void appendVariableDeclaration(storm::jani::Variable const& variable); modernjson::json finalize() { diff --git a/src/storage/jani/Property.cpp b/src/storage/jani/Property.cpp index 9b097757d..195aec571 100644 --- a/src/storage/jani/Property.cpp +++ b/src/storage/jani/Property.cpp @@ -1,11 +1,11 @@ #include "Property.h" namespace storm { namespace jani { - Property::Property(std::string const& name, std::shared_ptr const& formula, std::string const& comment) - : name(name), formula(formula), comment(comment) - { - - } +// Property::Property(std::string const& name, std::string const& comment) +// : name(name), formula(formula), comment(comment) +// { +// +// } std::string const& Property::getName() const { return this->name; @@ -14,10 +14,7 @@ namespace storm { std::string const& Property::getComment() const { return this->comment; } - - std::shared_ptr const& Property::getFormula() const { - return this->formula; - } + } } \ No newline at end of file diff --git a/src/storage/jani/Property.h b/src/storage/jani/Property.h index 30bddac60..c0f08bc56 100644 --- a/src/storage/jani/Property.h +++ b/src/storage/jani/Property.h @@ -4,6 +4,27 @@ namespace storm { namespace jani { + + enum class FilterType { MIN, MAX, SUM, AVG, COUNT, FORALL, EXISTS, ARGMIN, ARGMAX, VALUES }; + + + class PropertyExpression { + + }; + + class FilterExpression : public PropertyExpression { + std::shared_ptr states; + std::shared_ptr values; + FilterType ft; + }; + + class PathExpression : public PropertyExpression { + std::shared_ptr leftStateExpression; + std::shared_ptr rightStateExpression; + }; + + + class Property { /** * Constructs the property @@ -22,16 +43,13 @@ namespace storm { * @return the comment */ std::string const& getComment() const; - /** - * Get the formula - * @return the formula - */ - std::shared_ptr const& getFormula() const; - + + + private: std::string name; - std::shared_ptr formula; std::string comment; + PropertyExpression propertyExpression; }; } } diff --git a/src/storage/ppg/defines.h b/src/storage/ppg/defines.h index 548160ba9..d993e633e 100644 --- a/src/storage/ppg/defines.h +++ b/src/storage/ppg/defines.h @@ -1,6 +1,8 @@ #pragma once #include #include +#include + namespace storm { namespace ppg { class ProgramGraph; From 6a80319c183a9825cb89960ca2bf8603e029de3f Mon Sep 17 00:00:00 2001 From: sjunges Date: Thu, 13 Oct 2016 15:32:32 +0200 Subject: [PATCH 09/13] another Hwloc script Former-commit-id: cc5efdeb857264fd4c3351dd09063b763e36b623 [formerly 295c0c994ed500e72c1471c288fc22c4ca660ac4] Former-commit-id: fcaf78b967628407d13274a689861d02200259e9 --- resources/cmake/find_modules/FindHwloc.cmake | 206 ++++--------------- 1 file changed, 41 insertions(+), 165 deletions(-) diff --git a/resources/cmake/find_modules/FindHwloc.cmake b/resources/cmake/find_modules/FindHwloc.cmake index d1b5b488e..1db759375 100644 --- a/resources/cmake/find_modules/FindHwloc.cmake +++ b/resources/cmake/find_modules/FindHwloc.cmake @@ -1,179 +1,55 @@ -# FindHwloc -# ---------- +# Try to find hwloc libraries and headers. # -# Try to find Portable Hardware Locality (hwloc) libraries. -# http://www.open-mpi.org/software/hwloc +# Usage of this module: # -# You may declare HWLOC_ROOT environment variable to tell where -# your hwloc library is installed. +# find_package(hwloc) # -# Once done this will define:: +# Variables defined by this module: # -# Hwloc_FOUND - True if hwloc was found -# Hwloc_INCLUDE_DIRS - include directories for hwloc -# Hwloc_LIBRARIES - link against these libraries to use hwloc -# Hwloc_VERSION - version -# Hwloc_CFLAGS - include directories as compiler flags -# Hwloc_LDLFAGS - link paths and libs as compiler flags -# - -#============================================================================= -# Copyright 2014 Mikael Lepistö -# -# Distributed under the OSI-approved BSD License (the "License"); -# -# This software is distributed WITHOUT ANY WARRANTY; without even the -# implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. -# See the License for more information. -#============================================================================= - -if(WIN32) - find_path(Hwloc_INCLUDE_DIR - NAMES - hwloc.h - PATHS - ENV "PROGRAMFILES(X86)" - ENV HWLOC_ROOT - PATH_SUFFIXES - include - ) - - find_library(Hwloc_LIBRARY - NAMES - libhwloc.lib - PATHS - ENV "PROGRAMFILES(X86)" - ENV HWLOC_ROOT - PATH_SUFFIXES - lib - ) - - # - # Check if the found library can be used to linking - # - SET (_TEST_SOURCE "${CMAKE_BINARY_DIR}${CMAKE_FILES_DIRECTORY}/linktest.c") - FILE (WRITE "${_TEST_SOURCE}" - " - #include - int main() - { - hwloc_topology_t topology; - int nbcores; - hwloc_topology_init(&topology); - hwloc_topology_load(topology); - nbcores = hwloc_get_nbobjs_by_type(topology, HWLOC_OBJ_CORE); - hwloc_topology_destroy(topology); - return 0; - } - " - ) - - TRY_COMPILE(_LINK_SUCCESS ${CMAKE_BINARY_DIR} "${_TEST_SOURCE}" - CMAKE_FLAGS - "-DINCLUDE_DIRECTORIES:STRING=${Hwloc_INCLUDE_DIR}" - CMAKE_FLAGS - "-DLINK_LIBRARIES:STRING=${Hwloc_LIBRARY}" - ) - - IF(NOT _LINK_SUCCESS) - if(CMAKE_SIZEOF_VOID_P EQUAL 8) - message(STATUS "You are building 64bit target.") - ELSE() - message(STATUS "You are building 32bit code. If you like to build x64 use e.g. -G 'Visual Studio 12 Win64' generator." ) - ENDIF() - message(FATAL_ERROR "Library found, but linking test program failed.") - ENDIF() - - # - # Resolve version if some compiled binary found... - # - find_program(HWLOC_INFO_EXECUTABLE - NAMES - hwloc-info - PATHS - ENV HWLOC_ROOT - PATH_SUFFIXES - bin - ) - - if(HWLOC_INFO_EXECUTABLE) - execute_process( - COMMAND ${HWLOC_INFO_EXECUTABLE} "--version" - OUTPUT_VARIABLE HWLOC_VERSION_LINE - OUTPUT_STRIP_TRAILING_WHITESPACE - ) - string(REGEX MATCH "([0-9]+.[0-9]+)$" - Hwloc_VERSION "${HWLOC_VERSION_LINE}") - unset(HWLOC_VERSION_LINE) - endif() - - # - # All good - # - - set(Hwloc_LIBRARIES ${Hwloc_LIBRARY}) - set(Hwloc_INCLUDE_DIRS ${Hwloc_INCLUDE_DIR}) - - include(FindPackageHandleStandardArgs) - find_package_handle_standard_args( - Hwloc - FOUND_VAR Hwloc_FOUND - REQUIRED_VARS Hwloc_LIBRARY Hwloc_INCLUDE_DIR - VERSION_VAR Hwloc_VERSION) - - mark_as_advanced( - Hwloc_INCLUDE_DIR - Hwloc_LIBRARY) - - foreach(arg ${Hwloc_INCLUDE_DIRS}) - set(Hwloc_CFLAGS "${Hwloc_CFLAGS} /I${arg}") - endforeach() +# HWLOC_FOUND System has hwloc libraries and headers +# HWLOC_LIBRARIES The hwloc library +# HWLOC_INCLUDE_DIRS The location of HWLOC headers - set(Hwloc_LDFLAGS "${Hwloc_LIBRARY}") +find_path( + HWLOC_PREFIX + NAMES include/hwloc.h +) -else() +if (NOT HWLOC_PREFIX AND NOT $ENV{HWLOC_BASE} STREQUAL "") + set(HWLOC_PREFIX $ENV{HWLOC_BASE}) +endif() - # Find with pkgconfig - find_package(PkgConfig) +message(STATUS "Searching for hwloc library in path " ${HWLOC_PREFIX}) - if(HWLOC_ROOT) - set(ENV{PKG_CONFIG_PATH} "${HWLOC_ROOT}/lib/pkgconfig") - else() - foreach(PREFIX ${CMAKE_PREFIX_PATH}) - set(PKG_CONFIG_PATH "${PKG_CONFIG_PATH}:${PREFIX}/lib/pkgconfig") - endforeach() - set(ENV{PKG_CONFIG_PATH} "${PKG_CONFIG_PATH}:$ENV{PKG_CONFIG_PATH}") - endif() +find_library( + HWLOC_LIBRARIES + NAMES hwloc + HINTS ${HWLOC_PREFIX}/lib +) - if(hwloc_FIND_REQUIRED) - set(_hwloc_OPTS "REQUIRED") - elseif(hwloc_FIND_QUIETLY) - set(_hwloc_OPTS "QUIET") - else() - set(_hwloc_output 1) - endif() +find_path( + HWLOC_INCLUDE_DIRS + NAMES hwloc.h + HINTS ${HWLOC_PREFIX}/include +) - if(hwloc_FIND_VERSION) - if(hwloc_FIND_VERSION_EXACT) - pkg_check_modules(Hwloc ${_hwloc_OPTS} hwloc=${hwloc_FIND_VERSION}) - else() - pkg_check_modules(Hwloc ${_hwloc_OPTS} hwloc>=${hwloc_FIND_VERSION}) - endif() - else() - pkg_check_modules(Hwloc ${_hwloc_OPTS} hwloc) - endif() +include(FindPackageHandleStandardArgs) - if(Hwloc_FOUND) - include(FindPackageHandleStandardArgs) - find_package_handle_standard_args(Hwloc DEFAULT_MSG Hwloc_LIBRARIES) +find_package_handle_standard_args( + HWLOC DEFAULT_MSG + HWLOC_LIBRARIES + HWLOC_INCLUDE_DIRS +) - if(NOT ${Hwloc_VERSION} VERSION_LESS 1.7.0) - set(Hwloc_GL_FOUND 1) - endif() +mark_as_advanced( + HWLOC_LIBRARIES + HWLOC_INCLUDE_DIRS +) - if(_hwloc_output) - message(STATUS - "Found hwloc ${Hwloc_VERSION} in ${Hwloc_INCLUDE_DIRS}:${Hwloc_LIBRARIES}") - endif() +if (HWLOC_FOUND) + if (NOT $ENV{HWLOC_LIB} STREQUAL "") +# set(HWLOC_LIBRARIES "$ENV{HWLOC_LIB}") endif() -endif() + message(STATUS "hwloc includes: " ${HWLOC_INCLUDE_DIRS}) + message(STATUS "hwloc libraries: " ${HWLOC_LIBRARIES}) +endif() \ No newline at end of file From ccfcbc0c69fc1349d2940e956d62039f698897e9 Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 13 Oct 2016 15:37:26 +0200 Subject: [PATCH 10/13] fixed hwloc issue even harder Former-commit-id: 5768663ab4880968d5562114aedea295ea2ec8a9 [formerly 47af70ccf358cd6c066f89ddb3229b1528963c8e] Former-commit-id: ef788dbb6af6a7f6855d5798d964ef13cdec1752 --- resources/3rdparty/CMakeLists.txt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/resources/3rdparty/CMakeLists.txt b/resources/3rdparty/CMakeLists.txt index 244e24057..dcc98e937 100644 --- a/resources/3rdparty/CMakeLists.txt +++ b/resources/3rdparty/CMakeLists.txt @@ -330,7 +330,7 @@ add_dependencies(resources sylvan) if(${OPERATING_SYSTEM} MATCHES "Linux") find_package(Hwloc QUIET REQUIRED) - if(Hwloc_FOUND) + if(HWLOC_FOUND) message(STATUS "StoRM - Linking with hwloc ${Hwloc_VERSION}") list(APPEND STORM_LINK_LIBRARIES ${Hwloc_LIBRARIES}) else() From 744216d5d2c2ae77a681dca3b5df23e0196888fd Mon Sep 17 00:00:00 2001 From: sjunges Date: Thu, 13 Oct 2016 18:39:28 +0200 Subject: [PATCH 11/13] export formulae Former-commit-id: 4932938e383e1c8d2b09dd46591f070a43651380 [formerly 95b3269c755ac84aede16254a514be7d26a2aa24] Former-commit-id: 974a891cb6adfef1b39f9d94f1abdd63950dd7de --- src/cli/cli.cpp | 24 ++--- src/parser/JaniParser.cpp | 7 ++ src/storage/jani/JSONExporter.cpp | 158 ++++++++++++++++++++++++++++-- src/storage/jani/JSONExporter.h | 15 +-- src/storage/jani/Property.cpp | 10 +- src/storage/jani/Property.h | 29 +++--- 6 files changed, 200 insertions(+), 43 deletions(-) diff --git a/src/cli/cli.cpp b/src/cli/cli.cpp index 2c5104123..db9829084 100644 --- a/src/cli/cli.cpp +++ b/src/cli/cli.cpp @@ -222,13 +222,23 @@ namespace storm { model = storm::parseJaniModel(ioSettings.getJaniInputFilename()).first; } + // Then proceed to parsing the properties (if given), since the model we are building may depend on the property. + std::vector> formulas; + if (storm::settings::getModule().isPropertySet()) { + if (model.isJaniModel()) { + formulas = storm::parseFormulasForJaniModel(storm::settings::getModule().getProperty(), model.asJaniModel()); + } else { + formulas = storm::parseFormulasForPrismProgram(storm::settings::getModule().getProperty(), model.asPrismProgram()); + } + } + if(model.isJaniModel() && storm::settings::getModule().isJaniFileSet()) { if (storm::settings::getModule().isExportAsStandardJaniSet()) { storm::jani::Model normalisedModel = storm::jani::Model(model.asJaniModel()); normalisedModel.makeStandardJaniCompliant(); - storm::jani::JsonExporter::toFile(normalisedModel, storm::settings::getModule().getJaniFilename()); + storm::jani::JsonExporter::toFile(normalisedModel, formulas, storm::settings::getModule().getJaniFilename()); } else { - storm::jani::JsonExporter::toFile(model.asJaniModel(), storm::settings::getModule().getJaniFilename()); + storm::jani::JsonExporter::toFile(model.asJaniModel(), formulas, storm::settings::getModule().getJaniFilename()); } } @@ -236,15 +246,7 @@ namespace storm { std::string constantDefinitionString = ioSettings.getConstantDefinitionString(); model = model.preprocess(constantDefinitionString); - // Then proceed to parsing the properties (if given), since the model we are building may depend on the property. - std::vector> formulas; - if (storm::settings::getModule().isPropertySet()) { - if (model.isJaniModel()) { - formulas = storm::parseFormulasForJaniModel(storm::settings::getModule().getProperty(), model.asJaniModel()); - } else { - formulas = storm::parseFormulasForPrismProgram(storm::settings::getModule().getProperty(), model.asPrismProgram()); - } - } + if (storm::settings::getModule().isParametricSet()) { #ifdef STORM_HAVE_CARL diff --git a/src/parser/JaniParser.cpp b/src/parser/JaniParser.cpp index a49ab5548..97fc467e5 100644 --- a/src/parser/JaniParser.cpp +++ b/src/parser/JaniParser.cpp @@ -110,6 +110,13 @@ namespace storm { for (auto const& automataEntry : parsedStructure.at("automata")) { model.addAutomaton(parseAutomaton(automataEntry, model)); } + STORM_LOG_THROW(parsedStructure.count("restrict-initial") < 2, storm::exceptions::InvalidJaniException, "Model has multiple initial value restrictions"); + storm::expressions::Expression initialValueRestriction = expressionManager->boolean(true); + if(parsedStructure.count("restrict-initial") > 0) { + STORM_LOG_THROW(parsedStructure.at("restrict-initial").count("exp") == 1, storm::exceptions::InvalidJaniException, "Model needs an expression inside the initial restricion"); + initialValueRestriction = parseExpression(parsedStructure.at("restrict-initial").at("exp"), "Initial value restriction for automaton " + name); + } + model.setInitialStatesRestriction(initialValueRestriction); STORM_LOG_THROW(parsedStructure.count("system") == 1, storm::exceptions::InvalidJaniException, "Exactly one system description must be given"); std::shared_ptr composition = parseComposition(parsedStructure.at("system")); model.setSystemComposition(composition); diff --git a/src/storage/jani/JSONExporter.cpp b/src/storage/jani/JSONExporter.cpp index be30b82b8..e6c1e9d60 100644 --- a/src/storage/jani/JSONExporter.cpp +++ b/src/storage/jani/JSONExporter.cpp @@ -9,6 +9,7 @@ #include "src/exceptions/NotSupportedException.h" #include "src/exceptions/InvalidJaniException.h" +#include "src/exceptions/NotImplementedException.h" #include "src/storage/expressions/RationalLiteralExpression.h" #include "src/storage/expressions/IntegerLiteralExpression.h" @@ -25,6 +26,7 @@ #include "src/storage/jani/AutomatonComposition.h" #include "src/storage/jani/ParallelComposition.h" +#include "src/storage/jani/Property.h" namespace storm { namespace jani { @@ -128,6 +130,11 @@ namespace storm { return iDecl; } + modernjson::json FormulaToJaniJson::translate(storm::logic::Formula const& formula, bool continuousTime) { + FormulaToJaniJson translator(continuousTime); + return boost::any_cast(formula.accept(translator)); + } + boost::any FormulaToJaniJson::visit(storm::logic::AtomicExpressionFormula const& f, boost::any const& data) const { return ExpressionToJson::translate(f.getExpression()); } @@ -178,16 +185,44 @@ namespace storm { } boost::any FormulaToJaniJson::visit(storm::logic::TimeOperatorFormula const& f, boost::any const& data) const { - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Jani currently does not support conditional formulae"); - + modernjson::json opDecl; + std::vector tvec; + tvec.push_back("time"); + if(f.hasBound()) { + auto bound = f.getBound(); + opDecl["op"] = comparisonTypeToJani(bound.comparisonType); + if(f.hasOptimalityType()) { + opDecl["left"]["op"] = f.getOptimalityType() == storm::solver::OptimizationDirection::Minimize ? "Emin" : "Emax"; + opDecl["left"]["reach"] = boost::any_cast(f.getSubformula().accept(*this, boost::none)); + } else { + opDecl["left"]["op"] = (bound.comparisonType == storm::logic::ComparisonType::Less || bound.comparisonType == storm::logic::ComparisonType::LessEqual) ? "Emax" : "Emin"; + opDecl["left"]["reach"] = boost::any_cast(f.getSubformula().accept(*this, boost::none)); + } + opDecl["left"]["exp"] = modernjson::json(1); + opDecl["left"]["accumulate"] = modernjson::json(tvec); + opDecl["right"] = numberToJson(bound.threshold); + } else { + if(f.hasOptimalityType()) { + opDecl["op"] = f.getOptimalityType() == storm::solver::OptimizationDirection::Minimize ? "Emin" : "Emax"; + opDecl["reach"] = boost::any_cast(f.getSubformula().accept(*this, boost::none)); + + } else { + // TODO add checks + opDecl["op"] = "Pmin"; + opDecl["reach"] = boost::any_cast(f.getSubformula().accept(*this, boost::none)); + } + opDecl["exp"] = modernjson::json(1); + opDecl["accumulate"] = modernjson::json(tvec); + } + return opDecl; } boost::any FormulaToJaniJson::visit(storm::logic::GloballyFormula const& f, boost::any const& data) const { - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Jani currently does not support conditional formulae"); + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Jani currently does not support conversion of a globally formulae"); } boost::any FormulaToJaniJson::visit(storm::logic::InstantaneousRewardFormula const& f, boost::any const& data) const { - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Jani currently does not support conditional formulae"); + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Jani currently does not support conversion of an instanteneous reward formula"); } boost::any FormulaToJaniJson::visit(storm::logic::LongRunAverageOperatorFormula const& f, boost::any const& data) const { @@ -219,7 +254,30 @@ namespace storm { } boost::any FormulaToJaniJson::visit(storm::logic::LongRunAverageRewardFormula const& f, boost::any const& data) const { - +// modernjson::json opDecl; +// if(f.()) { +// auto bound = f.getBound(); +// opDecl["op"] = comparisonTypeToJani(bound.comparisonType); +// if(f.hasOptimalityType()) { +// opDecl["left"]["op"] = f.getOptimalityType() == storm::solver::OptimizationDirection::Minimize ? "Smin" : "Smax"; +// opDecl["left"]["exp"] = boost::any_cast(f.getSubformula().accept(*this, boost::none)); +// } else { +// opDecl["left"]["op"] = (bound.comparisonType == storm::logic::ComparisonType::Less || bound.comparisonType == storm::logic::ComparisonType::LessEqual) ? "Smax" : "Smin"; +// opDecl["left"]["exp"] = boost::any_cast(f.getSubformula().accept(*this, boost::none)); +// } +// opDecl["right"] = numberToJson(bound.threshold); +// } else { +// if(f.hasOptimalityType()) { +// opDecl["op"] = f.getOptimalityType() == storm::solver::OptimizationDirection::Minimize ? "Smin" : "Smax"; +// opDecl["exp"] = boost::any_cast(f.getSubformula().accept(*this, boost::none)); +// +// } else { +// // TODO add checks +// opDecl["op"] = "Pmin"; +// opDecl["exp"] = boost::any_cast(f.getSubformula().accept(*this, boost::none)); +// } +// } +// return opDecl; } boost::any FormulaToJaniJson::visit(storm::logic::NextFormula const& f, boost::any const& data) const { @@ -263,7 +321,40 @@ namespace storm { } boost::any FormulaToJaniJson::visit(storm::logic::RewardOperatorFormula const& f, boost::any const& data) const { - + modernjson::json opDecl; + std::vector accvec; + if(continuous) { + accvec.push_back("time"); + } else { + accvec.push_back("steps"); + } + if(f.hasBound()) { + auto bound = f.getBound(); + opDecl["op"] = comparisonTypeToJani(bound.comparisonType); + if(f.hasOptimalityType()) { + opDecl["left"]["op"] = f.getOptimalityType() == storm::solver::OptimizationDirection::Minimize ? "Emin" : "Emax"; + opDecl["left"]["reach"] = boost::any_cast(f.getSubformula().accept(*this, boost::none)); + } else { + opDecl["left"]["op"] = (bound.comparisonType == storm::logic::ComparisonType::Less || bound.comparisonType == storm::logic::ComparisonType::LessEqual) ? "Emax" : "Emin"; + opDecl["left"]["reach"] = boost::any_cast(f.getSubformula().accept(*this, boost::none)); + } + opDecl["left"]["exp"] = f.hasRewardModelName() ? f.getRewardModelName() : "DEFAULT"; + opDecl["left"]["accumulate"] = modernjson::json(accvec); + opDecl["right"] = numberToJson(bound.threshold); + } else { + if(f.hasOptimalityType()) { + opDecl["op"] = f.getOptimalityType() == storm::solver::OptimizationDirection::Minimize ? "Emin" : "Emax"; + opDecl["reach"] = boost::any_cast(f.getSubformula().accept(*this, boost::none)); + + } else { + // TODO add checks + opDecl["op"] = "Pmin"; + opDecl["reach"] = boost::any_cast(f.getSubformula().accept(*this, boost::none)); + } + opDecl["exp"] = f.hasRewardModelName() ? f.getRewardModelName() : "DEFAULT"; + opDecl["accumulate"] = modernjson::json(accvec); + } + return opDecl; } boost::any FormulaToJaniJson::visit(storm::logic::UnaryBooleanStateFormula const& f, boost::any const& data) const { @@ -402,22 +493,23 @@ namespace storm { - void JsonExporter::toFile(storm::jani::Model const& janiModel, std::string const& filepath, bool checkValid) { + void JsonExporter::toFile(storm::jani::Model const& janiModel, std::vector> const& formulas, std::string const& filepath, bool checkValid) { std::ofstream ofs; ofs.open (filepath, std::ofstream::out ); if(ofs.is_open()) { - toStream(janiModel, ofs, checkValid); + toStream(janiModel, formulas, ofs, checkValid); } else { STORM_LOG_THROW(false, storm::exceptions::FileIoException, "Cannot open " << filepath); } } - void JsonExporter::toStream(storm::jani::Model const& janiModel, std::ostream& os, bool checkValid) { + void JsonExporter::toStream(storm::jani::Model const& janiModel, std::vector> const& formulas, std::ostream& os, bool checkValid) { if(checkValid) { janiModel.checkValid(); } JsonExporter exporter; exporter.convertModel(janiModel); + exporter.convertProperties(formulas, !janiModel.isDiscreteTimeModel()); os << exporter.finalize().dump(4) << std::endl; } @@ -597,6 +689,54 @@ namespace storm { } + std::string janiFilterTypeString(storm::jani::FilterType const& ft) { + switch(ft) { + case storm::jani::FilterType::MIN: + return "min"; + case storm::jani::FilterType::MAX: + return "max"; + case storm::jani::FilterType::SUM: + return "sum"; + case storm::jani::FilterType::AVG: + return "avg"; + case storm::jani::FilterType::COUNT: + return "count"; + case storm::jani::FilterType::EXISTS: + return "∃"; + case storm::jani::FilterType::FORALL: + return "∀"; + case storm::jani::FilterType::ARGMIN: + return "argmin"; + case storm::jani::FilterType::ARGMAX: + return "argmax"; + case storm::jani::FilterType::VALUES: + return "values"; + + } + } + + modernjson::json convertFilterExpression(storm::jani::FilterExpression const& fe, bool continuousModel) { + modernjson::json propDecl; + propDecl["states"] = "initial"; + propDecl["fun"] = janiFilterTypeString(fe.getFilterType()); + propDecl["values"] = FormulaToJaniJson::translate(*fe.getFormula(), continuousModel); + return propDecl; + } + + + void JsonExporter::convertProperties( std::vector> const& formulas, bool continuousModel) { + std::vector properties; + uint64_t index = 0; + for(auto const& f : formulas) { + modernjson::json propDecl; + propDecl["name"] = "prop" + std::to_string(index); + propDecl["expression"] = convertFilterExpression(storm::jani::FilterExpression(f), continuousModel); + ++index; + properties.push_back(propDecl); + } + jsonStruct["properties"] = properties; + } + } } diff --git a/src/storage/jani/JSONExporter.h b/src/storage/jani/JSONExporter.h index ff54de5e8..55895364d 100644 --- a/src/storage/jani/JSONExporter.h +++ b/src/storage/jani/JSONExporter.h @@ -30,8 +30,9 @@ namespace storm { }; class FormulaToJaniJson : public storm::logic::FormulaVisitor { - public: - static modernjson::json translate(storm::logic::Formula const& formula); + + public: + static modernjson::json translate(storm::logic::Formula const& formula, bool continuousTime); virtual boost::any visit(storm::logic::AtomicExpressionFormula const& f, boost::any const& data) const; virtual boost::any visit(storm::logic::AtomicLabelFormula const& f, boost::any const& data) const; virtual boost::any visit(storm::logic::BinaryBooleanStateFormula const& f, boost::any const& data) const; @@ -51,19 +52,21 @@ namespace storm { virtual boost::any visit(storm::logic::UnaryBooleanStateFormula const& f, boost::any const& data) const; virtual boost::any visit(storm::logic::UntilFormula const& f, boost::any const& data) const; - + private: + FormulaToJaniJson(bool continuousModel) : continuous(continuousModel) { } + bool continuous; }; class JsonExporter { JsonExporter() = default; public: - static void toFile(storm::jani::Model const& janiModel, std::string const& filepath, bool checkValid = true); - static void toStream(storm::jani::Model const& janiModel, std::ostream& ostream, bool checkValid = false); + static void toFile(storm::jani::Model const& janiModel, std::vector> const& formulas, std::string const& filepath, bool checkValid = true); + static void toStream(storm::jani::Model const& janiModel, std::vector> const& formulas, std::ostream& ostream, bool checkValid = false); private: void convertModel(storm::jani::Model const& model); - void convertProperty(storm::logic::Formula const& formula); + void convertProperties(std::vector> const& formulas, bool timeContinuousModel); void appendVariableDeclaration(storm::jani::Variable const& variable); modernjson::json finalize() { diff --git a/src/storage/jani/Property.cpp b/src/storage/jani/Property.cpp index 195aec571..28981f313 100644 --- a/src/storage/jani/Property.cpp +++ b/src/storage/jani/Property.cpp @@ -1,11 +1,11 @@ #include "Property.h" namespace storm { namespace jani { -// Property::Property(std::string const& name, std::string const& comment) -// : name(name), formula(formula), comment(comment) -// { -// -// } + Property::Property(std::string const& name, std::shared_ptr const& formula, std::string const& comment) + : name(name), filterExpression(FilterExpression(formula)), comment(comment) + { + + } std::string const& Property::getName() const { return this->name; diff --git a/src/storage/jani/Property.h b/src/storage/jani/Property.h index c0f08bc56..bde51865e 100644 --- a/src/storage/jani/Property.h +++ b/src/storage/jani/Property.h @@ -8,20 +8,25 @@ namespace storm { enum class FilterType { MIN, MAX, SUM, AVG, COUNT, FORALL, EXISTS, ARGMIN, ARGMAX, VALUES }; - class PropertyExpression { - - }; - class FilterExpression : public PropertyExpression { - std::shared_ptr states; - std::shared_ptr values; - FilterType ft; + class FilterExpression { + public: + explicit FilterExpression(std::shared_ptr formula) : values(formula) {} + + std::shared_ptr const& getFormula() const { + return values; + } + + FilterType getFilterType() const { + return ft; + } + private: + // For now, we assume that the states are always the initial states. + + std::shared_ptr values; + FilterType ft = FilterType::VALUES; }; - class PathExpression : public PropertyExpression { - std::shared_ptr leftStateExpression; - std::shared_ptr rightStateExpression; - }; @@ -49,7 +54,7 @@ namespace storm { private: std::string name; std::string comment; - PropertyExpression propertyExpression; + FilterExpression filterExpression; }; } } From 282be9612e139e42af481338cb5fcafe56f58e07 Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 14 Oct 2016 09:44:15 +0200 Subject: [PATCH 12/13] fixed typo in header inclusion Former-commit-id: 7039fe5a3555aca5ec2c8a240221d0d3a0050bfa [formerly 4050360481d33fd40c9f8be22e0b79dbf8d38c74] Former-commit-id: 266f1e06598d5828ae36611f3119ace055bb4cb2 --- src/storage/jani/Property.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/storage/jani/Property.h b/src/storage/jani/Property.h index bde51865e..dc6aab23b 100644 --- a/src/storage/jani/Property.h +++ b/src/storage/jani/Property.h @@ -1,6 +1,6 @@ #pragma once -#include "src/logic/formulas.h" +#include "src/logic/Formulas.h" namespace storm { namespace jani { From 6f663bde0ebd95fadebab7ea0b4f47672d750060 Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 14 Oct 2016 10:35:17 +0200 Subject: [PATCH 13/13] fixing hwloc entry in CMakeLists.txt Former-commit-id: 1359cb4b148859cf9d28a4ac25490fa99de291b8 [formerly 9a108db302551e3fbe9e5689bea7bdad465cebf0] Former-commit-id: ab87e2002eb66a4e915796119ef4d6db222a7874 --- resources/3rdparty/CMakeLists.txt | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/resources/3rdparty/CMakeLists.txt b/resources/3rdparty/CMakeLists.txt index dcc98e937..ffd5fc54c 100644 --- a/resources/3rdparty/CMakeLists.txt +++ b/resources/3rdparty/CMakeLists.txt @@ -331,8 +331,8 @@ add_dependencies(resources sylvan) if(${OPERATING_SYSTEM} MATCHES "Linux") find_package(Hwloc QUIET REQUIRED) if(HWLOC_FOUND) - message(STATUS "StoRM - Linking with hwloc ${Hwloc_VERSION}") - list(APPEND STORM_LINK_LIBRARIES ${Hwloc_LIBRARIES}) + message(STATUS "StoRM - Linking with hwloc ${HWLOC_VERSION}") + list(APPEND STORM_LINK_LIBRARIES ${HWLOC_LIBRARIES}) else() message(FATAL_ERROR "HWLOC is required but was not found.") endif()