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

players now get stored in PRISM programs

tempestpy_adaptions
Stefan Pranger 4 years ago
parent
48276e47a9
commit
11f7464372
4 changed files with 31 additions and 11 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 4
      src/storm-parsers/parser/PrismParser.cpp
  2. 4
      src/storm-parsers/parser/PrismParser.h
  3. 22
      src/storm/storage/prism/Program.cpp
  4. 12
      src/storm/storage/prism/Program.h

4
src/storm-parsers/parser/PrismParser.cpp
View File

@ -302,7 +302,7 @@ namespace storm {
> modelTypeDefinition[phoenix::bind(&PrismParser::setModelType, phoenix::ref(*this), phoenix::ref(globalProgramInformation), qi::_1)]
> -observablesConstruct
> *( definedConstantDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::constants, phoenix::ref(globalProgramInformation)), qi::_1)]
| playerDefinition
| playerDefinition(phoenix::ref(globalProgramInformation))[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::players, phoenix::ref(globalProgramInformation)), qi::_1)]
| undefinedConstantDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::constants, phoenix::ref(globalProgramInformation)), qi::_1)]
| formulaDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::formulas, phoenix::ref(globalProgramInformation)), qi::_1)]
| globalVariableDefinition(phoenix::ref(globalProgramInformation))
@ -1001,7 +1001,7 @@ namespace storm {
}
}
return storm::prism::Program(manager, finalModelType, globalProgramInformation.constants, globalProgramInformation.globalBooleanVariables, globalProgramInformation.globalIntegerVariables, orderedFormulas, globalProgramInformation.modules, globalProgramInformation.actionIndices, globalProgramInformation.rewardModels, globalProgramInformation.labels, globalProgramInformation.observationLabels, secondRun && !globalProgramInformation.hasInitialConstruct ? boost::none : boost::make_optional(globalProgramInformation.initialConstruct), globalProgramInformation.systemCompositionConstruct, prismCompatibility, this->getFilename(), 1, this->secondRun);
return storm::prism::Program(manager, finalModelType, globalProgramInformation.constants, globalProgramInformation.globalBooleanVariables, globalProgramInformation.globalIntegerVariables, orderedFormulas, globalProgramInformation.players, globalProgramInformation.modules, globalProgramInformation.actionIndices, globalProgramInformation.rewardModels, globalProgramInformation.labels, globalProgramInformation.observationLabels, secondRun && !globalProgramInformation.hasInitialConstruct ? boost::none : boost::make_optional(globalProgramInformation.initialConstruct), globalProgramInformation.systemCompositionConstruct, prismCompatibility, this->getFilename(), 1, this->secondRun);
}
void PrismParser::removeInitialConstruct(GlobalProgramInformation& globalProgramInformation) const {

4
src/storm-parsers/parser/PrismParser.h
View File

@ -38,6 +38,7 @@ namespace storm {
globalBooleanVariables.clear();
globalIntegerVariables.clear();
moduleToIndexMap.clear();
players.clear();
modules.clear();
rewardModels.clear();
labels.clear();
@ -63,6 +64,7 @@ namespace storm {
std::vector<storm::prism::Label> labels;
std::vector<storm::prism::ObservationLabel> observationLabels;
std::vector<storm::prism::Player> players;
bool hasInitialConstruct;
storm::prism::InitialConstruct initialConstruct;
boost::optional<storm::prism::SystemCompositionConstruct> systemCompositionConstruct;
@ -268,7 +270,7 @@ namespace storm {
qi::rule<Iterator, std::string(), Skipper> freshPlayerName;
qi::rule<Iterator, std::string(), qi::locals<std::string>, Skipper> commandName;
qi::rule<Iterator, std::string(), qi::locals<std::string>, Skipper> moduleName;
qi::rule<Iterator, qi::unused_type(), qi::locals<std::string, std::vector<std::string>, std::vector<std::string>>, Skipper> playerDefinition;
qi::rule<Iterator, storm::prism::Player(GlobalProgramInformation&), qi::locals<std::string, std::vector<std::string>, std::vector<std::string>>, Skipper> playerDefinition;
// Rules for initial states expression.
qi::rule<Iterator, qi::unused_type(GlobalProgramInformation&), Skipper> initialStatesConstruct;

22
src/storm/storage/prism/Program.cpp
View File

@ -137,12 +137,12 @@ namespace storm {
std::set<std::string> appearingModules;
};
Program::Program(std::shared_ptr<storm::expressions::ExpressionManager> manager, ModelType modelType, std::vector<Constant> const& constants, std::vector<BooleanVariable> const& globalBooleanVariables, std::vector<IntegerVariable> const& globalIntegerVariables, std::vector<Formula> const& formulas, std::vector<Module> const& modules, std::map<std::string, uint_fast64_t> const& actionToIndexMap, std::vector<RewardModel> const& rewardModels, std::vector<Label> const& labels, std::vector<ObservationLabel> const& observationLabels, boost::optional<InitialConstruct> const& initialConstruct, boost::optional<SystemCompositionConstruct> const& compositionConstruct, bool prismCompatibility, std::string const& filename, uint_fast64_t lineNumber, bool finalModel)
Program::Program(std::shared_ptr<storm::expressions::ExpressionManager> manager, ModelType modelType, std::vector<Constant> const& constants, std::vector<BooleanVariable> const& globalBooleanVariables, std::vector<IntegerVariable> const& globalIntegerVariables, std::vector<Formula> const& formulas, std::vector<Player> const& players, std::vector<Module> const& modules, std::map<std::string, uint_fast64_t> const& actionToIndexMap, std::vector<RewardModel> const& rewardModels, std::vector<Label> const& labels, std::vector<ObservationLabel> const& observationLabels, boost::optional<InitialConstruct> const& initialConstruct, boost::optional<SystemCompositionConstruct> const& compositionConstruct, bool prismCompatibility, std::string const& filename, uint_fast64_t lineNumber, bool finalModel)
: LocatedInformation(filename, lineNumber), manager(manager),
modelType(modelType), constants(constants), constantToIndexMap(),
globalBooleanVariables(globalBooleanVariables), globalBooleanVariableToIndexMap(),
globalIntegerVariables(globalIntegerVariables), globalIntegerVariableToIndexMap(),
formulas(formulas), formulaToIndexMap(), modules(modules), moduleToIndexMap(),
formulas(formulas), formulaToIndexMap(), players(players), modules(modules), moduleToIndexMap(),
rewardModels(rewardModels), rewardModelToIndexMap(), systemCompositionConstruct(compositionConstruct),
labels(labels), labelToIndexMap(), observationLabels(observationLabels), actionToIndexMap(actionToIndexMap), indexToActionMap(), actions(),
synchronizingActionIndices(), actionIndicesToModuleIndexMap(), variableToModuleIndexMap(), prismCompatibility(prismCompatibility)
@ -479,6 +479,10 @@ namespace storm {
return this->formulas;
}
std::vector<Player> const& Program::getPlayers() const {
return this->players;
}
std::size_t Program::getNumberOfFormulas() const {
return this->getFormulas().size();
}
@ -778,7 +782,7 @@ namespace storm {
newModules.push_back(module.restrictCommands(indexSet));
}
return Program(this->manager, this->getModelType(), this->getConstants(), this->getGlobalBooleanVariables(), this->getGlobalIntegerVariables(), this->getFormulas(), newModules, this->getActionNameToIndexMapping(), this->getRewardModels(), this->getLabels(), this->getObservationLabels(), this->getOptionalInitialConstruct(), this->getOptionalSystemCompositionConstruct(), prismCompatibility);
return Program(this->manager, this->getModelType(), this->getConstants(), this->getGlobalBooleanVariables(), this->getGlobalIntegerVariables(), this->getFormulas(), this->getPlayers(), newModules, this->getActionNameToIndexMapping(), this->getRewardModels(), this->getLabels(), this->getObservationLabels(), this->getOptionalInitialConstruct(), this->getOptionalSystemCompositionConstruct(), prismCompatibility);
}
void Program::createMappings() {
@ -875,7 +879,7 @@ namespace storm {
}
}
return Program(this->manager, this->getModelType(), newConstants, this->getGlobalBooleanVariables(), this->getGlobalIntegerVariables(), this->getFormulas(), this->getModules(), this->getActionNameToIndexMapping(), this->getRewardModels(), this->getLabels(), this->getObservationLabels(), this->getOptionalInitialConstruct(), this->getOptionalSystemCompositionConstruct(), prismCompatibility);
return Program(this->manager, this->getModelType(), newConstants, this->getGlobalBooleanVariables(), this->getGlobalIntegerVariables(), this->getFormulas(), this->getPlayers(), this->getModules(), this->getActionNameToIndexMapping(), this->getRewardModels(), this->getLabels(), this->getObservationLabels(), this->getOptionalInitialConstruct(), this->getOptionalSystemCompositionConstruct(), prismCompatibility);
}
Program Program::substituteConstants() const {
@ -954,7 +958,7 @@ namespace storm {
newObservationLabels.emplace_back(label.substitute(substitution));
}
return Program(this->manager, this->getModelType(), newConstants, newBooleanVariables, newIntegerVariables, newFormulas, newModules, this->getActionNameToIndexMapping(), newRewardModels, newLabels, newObservationLabels, newInitialConstruct, this->getOptionalSystemCompositionConstruct(), prismCompatibility);
return Program(this->manager, this->getModelType(), newConstants, newBooleanVariables, newIntegerVariables, newFormulas, this->getPlayers(), newModules, this->getActionNameToIndexMapping(), newRewardModels, newLabels, newObservationLabels, newInitialConstruct, this->getOptionalSystemCompositionConstruct(), prismCompatibility);
}
void Program::checkValidity(Program::ValidityCheckLevel lvl) const {
@ -1512,7 +1516,7 @@ namespace storm {
newLabels.emplace_back(label.getName(), label.getStatePredicateExpression().simplify());
}
return Program(this->manager, modelType, newConstants, getGlobalBooleanVariables(), getGlobalIntegerVariables(), getFormulas(), newModules, actionIndicesToDelete.empty() ? getActionNameToIndexMapping() : newActionToIndexMap, actionIndicesToDelete.empty() ? this->getRewardModels() : newRewardModels, newLabels, getObservationLabels(), getOptionalInitialConstruct(), this->getOptionalSystemCompositionConstruct(), prismCompatibility);
return Program(this->manager, modelType, newConstants, getGlobalBooleanVariables(), getGlobalIntegerVariables(), getFormulas(), this->getPlayers(), newModules, actionIndicesToDelete.empty() ? getActionNameToIndexMapping() : newActionToIndexMap, actionIndicesToDelete.empty() ? this->getRewardModels() : newRewardModels, newLabels, getObservationLabels(), getOptionalInitialConstruct(), this->getOptionalSystemCompositionConstruct(), prismCompatibility);
}
Program Program::flattenModules(std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory) const {
@ -1720,7 +1724,7 @@ namespace storm {
// Finally, we can create the module and the program and return it.
storm::prism::Module singleModule(newModuleName.str(), allBooleanVariables, allIntegerVariables, allClockVariables, newInvariant, newCommands, this->getFilename(), 0);
return Program(manager, this->getModelType(), this->getConstants(), std::vector<storm::prism::BooleanVariable>(), std::vector<storm::prism::IntegerVariable>(), this->getFormulas(), {singleModule}, actionToIndexMap, this->getRewardModels(), this->getLabels(), this->getObservationLabels(), this->getOptionalInitialConstruct(), this->getOptionalSystemCompositionConstruct(), prismCompatibility, this->getFilename(), 0, true);
return Program(manager, this->getModelType(), this->getConstants(), std::vector<storm::prism::BooleanVariable>(), std::vector<storm::prism::IntegerVariable>(), this->getFormulas(), this->getPlayers(), {singleModule}, actionToIndexMap, this->getRewardModels(), this->getLabels(), this->getObservationLabels(), this->getOptionalInitialConstruct(), this->getOptionalSystemCompositionConstruct(), prismCompatibility, this->getFilename(), 0, true);
}
std::vector<Constant> Program::usedConstants() const {
@ -1947,6 +1951,10 @@ namespace storm {
}
stream << std::endl;
for (auto const& player : program.getPlayers()) {
stream << player << std::endl;
}
for (auto const& variable : program.getGlobalBooleanVariables()) {
stream << "global " << variable << std::endl;
}

12
src/storm/storage/prism/Program.h
View File

@ -58,7 +58,7 @@ namespace storm {
* @param lineNumber The line number in which the program is defined.
* @param finalModel If set to true, the program is checked for input-validity, as well as some post-processing.
*/
Program(std::shared_ptr<storm::expressions::ExpressionManager> manager, ModelType modelType, std::vector<Constant> const& constants, std::vector<BooleanVariable> const& globalBooleanVariables, std::vector<IntegerVariable> const& globalIntegerVariables, std::vector<Formula> const& formulas, std::vector<Module> const& modules, std::map<std::string, uint_fast64_t> const& actionToIndexMap, std::vector<RewardModel> const& rewardModels, std::vector<Label> const& labels, std::vector<ObservationLabel> const& observationLabels, boost::optional<InitialConstruct> const& initialConstruct, boost::optional<SystemCompositionConstruct> const& compositionConstruct, bool prismCompatibility, std::string const& filename = "", uint_fast64_t lineNumber = 0, bool finalModel = true);
Program(std::shared_ptr<storm::expressions::ExpressionManager> manager, ModelType modelType, std::vector<Constant> const& constants, std::vector<BooleanVariable> const& globalBooleanVariables, std::vector<IntegerVariable> const& globalIntegerVariables, std::vector<Formula> const& formulas, std::vector<Player> const& players, std::vector<Module> const& modules, std::map<std::string, uint_fast64_t> const& actionToIndexMap, std::vector<RewardModel> const& rewardModels, std::vector<Label> const& labels, std::vector<ObservationLabel> const& observationLabels, boost::optional<InitialConstruct> const& initialConstruct, boost::optional<SystemCompositionConstruct> const& compositionConstruct, bool prismCompatibility, std::string const& filename = "", uint_fast64_t lineNumber = 0, bool finalModel = true);
// Provide default implementations for constructors and assignments.
Program() = default;
@ -275,6 +275,13 @@ namespace storm {
*/
std::vector<Formula> const& getFormulas() const;
/*!
* Retrieves the players of the program.
*
* @return The players of the program.
*/
std::vector<Player> const& getPlayers() const;
/*!
* Retrieves the number of formulas in the program.
*
@ -739,6 +746,9 @@ namespace storm {
// The modules associated with the program.
std::vector<Module> modules;
// The players associated with the program.
std::vector<Player> players;
// A mapping of module names to their indices.
std::map<std::string, uint_fast64_t> moduleToIndexMap;
Write Preview
Loading…
Cancel
Save