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/parser/JaniParser.cpp b/src/parser/JaniParser.cpp index 6953c70ea..ebcb07d4a 100644 --- a/src/parser/JaniParser.cpp +++ b/src/parser/JaniParser.cpp @@ -26,7 +26,7 @@ namespace storm { const bool JaniParser::defaultBooleanInitialValue = false; const double JaniParser::defaultRationalInitialValue = 0.0; const int64_t JaniParser::defaultIntegerInitialValue = 0; - const std::string VARIABLE_AUTOMATON_DELIMITER = "."; + const std::string VARIABLE_AUTOMATON_DELIMITER = "_"; const std::set JaniParser::unsupportedOpstrings({"sin", "cos", "tan", "cot", "sec", "csc", "asin", "acos", "atan", "acot", "asec", "acsc", "sinh", "cosh", "tanh", "coth", "sech", "csch", "asinh", "acosh", "atanh", "asinh", "acosh"}); 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;