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

Cleaned IR classes a bit and made attributes private. Changed grammar rules accordingly.

tempestpy_adaptions
dehnert 12 years ago
parent
b381321653
commit
f7194a416d
11 changed files with 123 additions and 73 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. 31
      src/ir/Assignment.h
  2. 7
      src/ir/BooleanVariable.h
  3. 34
      src/ir/Command.h
  4. 11
      src/ir/IntegerVariable.h
  5. 18
      src/ir/Module.h
  6. 42
      src/ir/Program.h
  7. 1
      src/ir/RewardModel.h
  8. 27
      src/ir/Update.h
  9. 9
      src/ir/Variable.h
  10. 4
      src/ir/expressions/BaseExpression.h
  11. 12
      src/parser/PrismParser.h

31
src/ir/Assignment.h
View File

@ -8,8 +8,7 @@
#ifndef ASSIGNMENT_H_
#define ASSIGNMENT_H_
#include "expressions/Expressions.h"
#include <boost/fusion/include/adapt_struct.hpp>
#include "expressions/BaseExpression.h"
namespace storm {
@ -18,6 +17,28 @@ namespace ir {
class Assignment {
public:
Assignment() : variableName(""), expression(nullptr) {
}
Assignment(std::string variableName, std::shared_ptr<storm::ir::expressions::BaseExpression> expression)
: variableName(variableName), expression(expression) {
}
std::string getVariableName() {
return variableName;
}
std::shared_ptr<storm::ir::expressions::BaseExpression> getExpression() {
return expression;
}
std::string toString() {
return variableName + "' = " + expression->toString();
}
private:
std::string variableName;
std::shared_ptr<storm::ir::expressions::BaseExpression> expression;
};
@ -26,10 +47,4 @@ public:
}
BOOST_FUSION_ADAPT_STRUCT(
storm::ir::Assignment,
(std::string, variableName)
(std::shared_ptr<storm::ir::expressions::BaseExpression>, expression)
)
#endif /* ASSIGNMENT_H_ */

7
src/ir/BooleanVariable.h
View File

@ -27,7 +27,7 @@ public:
}
virtual std::string toString() {
return variableName + ": bool;";
return getVariableName() + ": bool;";
}
};
@ -35,9 +35,4 @@ public:
}
BOOST_FUSION_ADAPT_STRUCT(
storm::ir::BooleanVariable,
(std::string, variableName)
)
#endif /* BOOLEANVARIABLE_H_ */

34
src/ir/Command.h
View File

@ -16,25 +16,37 @@ namespace ir {
class Command {
public:
std::string commandName;
std::shared_ptr<storm::ir::expressions::BaseExpression> guardExpression;
std::vector<storm::ir::Update> updates;
Command() : commandName(""), guardExpression(nullptr), updates() {
}
Command(std::string commandName, std::shared_ptr<storm::ir::expressions::BaseExpression> guardExpression, std::vector<storm::ir::Update> updates)
: commandName(commandName), guardExpression(guardExpression), updates(updates) {
}
std::string toString() {
return "command!";
std::string result = "[" + commandName + "] " + guardExpression->toString() + " -> ";
for (uint_fast64_t i = 0; i < updates.size(); ++i) {
result += updates[i].toString();
if (i < updates.size() - 1) {
result += " + ";
}
}
result += ";";
return result;
}
private:
std::string commandName;
std::shared_ptr<storm::ir::expressions::BaseExpression> guardExpression;
std::vector<storm::ir::Update> updates;
};
}
}
BOOST_FUSION_ADAPT_STRUCT(
storm::ir::Command,
(std::string, commandName)
(std::shared_ptr<storm::ir::expressions::BaseExpression>, guardExpression)
(std::vector<storm::ir::Update>, updates)
)
#endif /* COMMAND_H_ */

11
src/ir/IntegerVariable.h
View File

@ -29,17 +29,10 @@ public:
}
virtual std::string toString() {
return variableName + ": int[];";
}
void setLowerBound(std::shared_ptr<storm::ir::expressions::BaseExpression>& lowerBound) {
this->lowerBound = lowerBound;
}
void setUpperBound(std::shared_ptr<storm::ir::expressions::BaseExpression>& upperBound) {
this->upperBound = upperBound;
return getVariableName() + ": int[" + lowerBound->toString() + ".." + upperBound->toString() + "];";
}
private:
std::shared_ptr<storm::ir::expressions::BaseExpression> lowerBound;
std::shared_ptr<storm::ir::expressions::BaseExpression> upperBound;
};

18
src/ir/Module.h
View File

@ -16,7 +16,16 @@ namespace ir {
class Module {
public:
Module() {
Module() : moduleName(""), booleanVariables(), integerVariables(), commands() {
}
Module(std::string moduleName, std::vector<storm::ir::BooleanVariable> booleanVariables, std::vector<storm::ir::IntegerVariable> integerVariables, std::vector<storm::ir::Command> commands)
: moduleName(moduleName), booleanVariables(booleanVariables), integerVariables(integerVariables), commands(commands) {
}
Module(std::string moduleName, std::vector<storm::ir::Command> commands) : moduleName(moduleName), booleanVariables(), integerVariables(), commands(commands) {
}
@ -44,6 +53,7 @@ public:
integerVariables.push_back(variable);
}
private:
std::string moduleName;
std::vector<storm::ir::BooleanVariable> booleanVariables;
@ -56,10 +66,4 @@ public:
}
BOOST_FUSION_ADAPT_STRUCT(
storm::ir::Module,
(std::string, moduleName)
(std::vector<storm::ir::Command>, commands)
)
#endif /* MODULE_H_ */

42
src/ir/Program.h
View File

@ -18,15 +18,30 @@ namespace ir {
class Program {
public:
enum ModelType {DTMC, CTMC, MDP, CTMDP} modelType;
std::map<std::string, std::shared_ptr<storm::ir::expressions::BooleanConstantExpression>> booleanUndefinedConstantExpressions;
std::map<std::string, std::shared_ptr<storm::ir::expressions::IntegerConstantExpression>> integerUndefinedConstantExpressions;
std::map<std::string, std::shared_ptr<storm::ir::expressions::DoubleConstantExpression>> doubleUndefinedConstantExpressions;
std::vector<storm::ir::Module> modules;
std::map<std::string, storm::ir::RewardModel> rewards;
enum ModelType {DTMC, CTMC, MDP, CTMDP};
Program() : modelType(DTMC), booleanUndefinedConstantExpressions(), integerUndefinedConstantExpressions(), doubleUndefinedConstantExpressions(), modules(), rewards() {
}
Program(ModelType modelType, std::map<std::string, std::shared_ptr<storm::ir::expressions::BooleanConstantExpression>> booleanUndefinedConstantExpressions, std::map<std::string, std::shared_ptr<storm::ir::expressions::IntegerConstantExpression>> integerUndefinedConstantExpressions, std::map<std::string, std::shared_ptr<storm::ir::expressions::DoubleConstantExpression>> doubleUndefinedConstantExpressions, std::vector<storm::ir::Module> modules, std::map<std::string, storm::ir::RewardModel> rewards)
: modelType(modelType), booleanUndefinedConstantExpressions(booleanUndefinedConstantExpressions), integerUndefinedConstantExpressions(integerUndefinedConstantExpressions), doubleUndefinedConstantExpressions(doubleUndefinedConstantExpressions), modules(modules), rewards(rewards) {
}
Program(ModelType modelType, std::vector<storm::ir::Module> modules) : modelType(modelType), booleanUndefinedConstantExpressions(), integerUndefinedConstantExpressions(), doubleUndefinedConstantExpressions(), modules(modules), rewards() {
}
std::string toString() {
std::string result = "";
switch (modelType) {
case DTMC: result += "dtmc\n"; break;
case CTMC: result += "ctmc\n"; break;
case MDP: result += "mdp\n"; break;
case CTMDP: result += "ctmdp\n"; break;
}
for (auto element : booleanUndefinedConstantExpressions) {
result += "const bool " + element.first + ";\n";
}
@ -55,18 +70,17 @@ public:
doubleUndefinedConstantExpressions[constantName] = constantExpression;
}
void setModules(std::vector<storm::ir::Module> modules) {
this->modules = modules;
}
private:
ModelType modelType;
std::map<std::string, std::shared_ptr<storm::ir::expressions::BooleanConstantExpression>> booleanUndefinedConstantExpressions;
std::map<std::string, std::shared_ptr<storm::ir::expressions::IntegerConstantExpression>> integerUndefinedConstantExpressions;
std::map<std::string, std::shared_ptr<storm::ir::expressions::DoubleConstantExpression>> doubleUndefinedConstantExpressions;
std::vector<storm::ir::Module> modules;
std::map<std::string, storm::ir::RewardModel> rewards;
};
}
}
BOOST_FUSION_ADAPT_STRUCT(
storm::ir::Program,
(std::vector<storm::ir::Module>, modules)
)
#endif /* PROGRAM_H_ */

1
src/ir/RewardModel.h
View File

@ -20,5 +20,4 @@ class RewardModel {
}
#endif /* REWARDMODEL_H_ */

27
src/ir/Update.h
View File

@ -16,6 +16,27 @@ namespace ir {
class Update {
public:
Update() : likelihoodExpression(nullptr), assignments() {
}
Update(std::shared_ptr<storm::ir::expressions::BaseExpression> likelihoodExpression, std::vector<storm::ir::Assignment> assignments)
: likelihoodExpression(likelihoodExpression), assignments(assignments) {
}
std::string toString() {
std::string result = likelihoodExpression->toString() + " : ";
for (uint_fast64_t i = 0; i < assignments.size(); ++i) {
result += assignments[i].toString();
if (i < assignments.size() - 1) {
result += " & ";
}
}
return result;
}
private:
std::shared_ptr<storm::ir::expressions::BaseExpression> likelihoodExpression;
std::vector<storm::ir::Assignment> assignments;
};
@ -24,10 +45,4 @@ public:
}
BOOST_FUSION_ADAPT_STRUCT(
storm::ir::Update,
(std::shared_ptr<storm::ir::expressions::BaseExpression>, likelihoodExpression)
(std::vector<storm::ir::Assignment>, assignments)
)
#endif /* UPDATE_H_ */

9
src/ir/Variable.h
View File

@ -14,8 +14,6 @@ namespace ir {
class Variable {
public:
std::string variableName;
Variable() {
}
@ -32,9 +30,12 @@ public:
return variableName;
}
void setVariableName(std::string variableName) {
this->variableName = variableName;
std::string getVariableName() {
return variableName;
}
private:
std::string variableName;
};
}

4
src/ir/expressions/BaseExpression.h
View File

@ -21,7 +21,9 @@ public:
}
virtual std::string toString() const = 0;
virtual std::string toString() const {
return "expr here!";
}
};
}

12
src/parser/PrismParser.h
View File

@ -98,7 +98,7 @@ private:
expression %= (booleanExpression | integerExpression | doubleExpression);
booleanVariableDefinition = (freeIdentifierName >> qi::lit(":") >> qi::lit("bool") >> qi::lit(";"))[qi::_val = phoenix::construct<storm::ir::BooleanVariable>(qi::_1), qi::_a = phoenix::construct<std::shared_ptr<storm::ir::expressions::VariableExpression>>(phoenix::new_<storm::ir::expressions::VariableExpression>(qi::_1)), phoenix::bind(booleanVariables_.add, qi::_1, qi::_a), phoenix::bind(booleanVariableNames_.add, qi::_1, qi::_1), phoenix::bind(allVariables_.add, qi::_1, qi::_a)];
integerVariableDefinition = (freeIdentifierName >> qi::lit(":") >> qi::lit("[") >> integerConstantExpression >> qi::lit("..") >> integerConstantExpression >> qi::lit("]") >> qi::lit(";"))[qi::_val = phoenix::construct<storm::ir::IntegerVariable>(qi::_1, qi::_2, qi::_3), qi::_a = phoenix::construct<std::shared_ptr<storm::ir::expressions::VariableExpression>>(phoenix::new_<storm::ir::expressions::VariableExpression>(qi::_1)), phoenix::bind(integerVariables_.add, qi::_1, qi::_a), phoenix::bind(integerVariableNames_.add, qi::_1, qi::_1), phoenix::bind(allVariables_.add, qi::_1, qi::_a), phoenix::bind(&storm::ir::IntegerVariable::setVariableName, qi::_val, qi::_1), phoenix::bind(&storm::ir::IntegerVariable::setLowerBound, qi::_val, qi::_2), phoenix::bind(&storm::ir::IntegerVariable::setUpperBound, qi::_val, qi::_3)];
integerVariableDefinition = (freeIdentifierName >> qi::lit(":") >> qi::lit("[") >> integerConstantExpression >> qi::lit("..") >> integerConstantExpression >> qi::lit("]") >> qi::lit(";"))[qi::_val = phoenix::construct<storm::ir::IntegerVariable>(qi::_1, qi::_2, qi::_3), qi::_a = phoenix::construct<std::shared_ptr<storm::ir::expressions::VariableExpression>>(phoenix::new_<storm::ir::expressions::VariableExpression>(qi::_1)), phoenix::bind(integerVariables_.add, qi::_1, qi::_a), phoenix::bind(integerVariableNames_.add, qi::_1, qi::_1), phoenix::bind(allVariables_.add, qi::_1, qi::_a)];
variableDefinition = (booleanVariableDefinition[phoenix::bind(&storm::ir::Module::addBooleanVariable, qi::_r1, qi::_1)] | integerVariableDefinition[phoenix::bind(&storm::ir::Module::addIntegerVariable, qi::_r1, qi::_1)]);
definedBooleanConstantDefinition = (qi::lit("const") >> qi::lit("bool") >> freeIdentifierName >> qi::lit("=") >> booleanLiteralExpression >> qi::lit(";"))[phoenix::bind(booleanConstants_.add, qi::_1, qi::_2), phoenix::bind(allConstants_.add, qi::_1, qi::_2), qi::_val = qi::_2];
@ -116,17 +116,17 @@ private:
integerVariableName %= integerVariableNames_;
booleanVariableName %= booleanVariableNames_;
assignmentDefinition = qi::lit("(") >> integerVariableName >> qi::lit("'") >> integerExpression >> qi::lit(")") | qi::lit("(") >> booleanVariableName >> qi::lit("'") >> booleanExpression >> qi::lit(")");
assignmentDefinition = (qi::lit("(") >> integerVariableName >> qi::lit("'") >> integerExpression >> qi::lit(")"))[qi::_val = phoenix::construct<storm::ir::Assignment>(qi::_1, qi::_2)] | (qi::lit("(") >> booleanVariableName >> qi::lit("'") >> booleanExpression >> qi::lit(")"))[qi::_val = phoenix::construct<storm::ir::Assignment>(qi::_1, qi::_2)];
assignmentDefinitionList %= assignmentDefinition % "&";
updateDefinition %= doubleConstantExpression >> qi::lit(":") >> assignmentDefinitionList;
updateDefinition = (doubleConstantExpression >> qi::lit(":") >> assignmentDefinitionList)[qi::_val = phoenix::construct<storm::ir::Update>(qi::_1, qi::_2)];
updateListDefinition = +updateDefinition;
commandDefinition %= qi::lit("[") >> freeIdentifierName >> qi::lit("]") >> booleanExpression >> qi::lit("->") >> updateListDefinition >> qi::lit(";");
commandDefinition = (qi::lit("[") >> freeIdentifierName >> qi::lit("]") >> booleanExpression >> qi::lit("->") >> updateListDefinition >> qi::lit(";"))[qi::_val = phoenix::construct<storm::ir::Command>(qi::_1, qi::_2, qi::_3)];
moduleDefinition %= qi::lit("module") >> freeIdentifierName >> *variableDefinition(qi::_val) >> *commandDefinition >> qi::lit("endmodule");
moduleDefinition = (qi::lit("module") >> freeIdentifierName >> *variableDefinition(qi::_val) >> *commandDefinition >> qi::lit("endmodule"))[qi::_val = phoenix::construct<storm::ir::Module>(qi::_1, qi::_2)];
moduleDefinitionList = +moduleDefinition;
start = constantDefinitionList >> moduleDefinitionList;
start = (constantDefinitionList >> moduleDefinitionList)[qi::_val = phoenix::construct<storm::ir::Program>(storm::ir::Program::ModelType::DTMC, qi::_1)];
}
// The starting point of the grammar.

Write Preview
Loading…
Cancel
Save