diff --git a/src/adapters/ExplicitModelAdapter.cpp b/src/adapters/ExplicitModelAdapter.cpp
index 7b496b66d..3a8bc878e 100644
--- a/src/adapters/ExplicitModelAdapter.cpp
+++ b/src/adapters/ExplicitModelAdapter.cpp
@@ -28,6 +28,8 @@ ExplicitModelAdapter::ExplicitModelAdapter(storm::ir::Program program) : program
booleanVariables(), integerVariables(), booleanVariableToIndexMap(), integerVariableToIndexMap(),
allStates(), stateToIndexMap(), numberOfTransitions(0), numberOfChoices(0), transitionRewards(nullptr), transitionMap() {
this->initializeVariables();
+ storm::settings::Settings* s = storm::settings::instance();
+ this->precision = s->get<double>("precision");
}
ExplicitModelAdapter::~ExplicitModelAdapter() {
@@ -57,6 +59,11 @@ ExplicitModelAdapter::~ExplicitModelAdapter() {
case storm::ir::Program::DTMC:
{
std::shared_ptr<storm::storage::SparseMatrix<double>> matrix = this->buildDeterministicMatrix();
+ std::cerr << "Row 2: ";
+ for (const double* val = matrix->beginConstIterator(2); val != matrix->endConstIterator(2); val++) {
+ std::cerr << *val << ", ";
+ }
+ std::cerr << std::endl;
return std::shared_ptr<storm::models::AbstractModel>(new storm::models::Dtmc<double>(matrix, stateLabeling, stateRewards, this->transitionRewards));
break;
}
@@ -306,6 +313,7 @@ ExplicitModelAdapter::~ExplicitModelAdapter() {
// Add a new map and get pointer.
res.emplace_back();
std::map<uint_fast64_t, double>* states = &res.back().second;
+ double probSum = 0;
// Iterate over all updates.
for (uint_fast64_t k = 0; k < command.getNumberOfUpdates(); ++k) {
@@ -313,6 +321,7 @@ ExplicitModelAdapter::~ExplicitModelAdapter() {
storm::ir::Update const& update = command.getUpdate(k);
uint_fast64_t newStateId = this->getOrAddStateId(this->applyUpdate(state, update));
+ probSum += update.getLikelihoodExpression()->getValueAsDouble(state);
// Check, if we already know this state, add up probabilities for every state.
auto stateIt = states->find(newStateId);
if (stateIt == states->end()) {
@@ -322,6 +331,10 @@ ExplicitModelAdapter::~ExplicitModelAdapter() {
(*states)[newStateId] += update.getLikelihoodExpression()->getValueAsDouble(state);
}
}
+ if (std::abs(1 - probSum) > this->precision) {
+ LOG4CPLUS_ERROR(logger, "Sum of update probabilities should be one for command:\n\t" << command.toString());
+ throw storm::exceptions::WrongFileFormatException() << "Sum of update probabilities should be one for command:\n\t" << command.toString();
+ }
}
}
}
@@ -349,6 +362,7 @@ ExplicitModelAdapter::~ExplicitModelAdapter() {
// Iterate over all commands within this module.
for (storm::ir::Command command : module) {
// Iterate over all updates of this command.
+ double probSum = 0;
for (uint_fast64_t k = 0; k < command.getNumberOfUpdates(); ++k) {
storm::ir::Update const update = command.getUpdate(k);
@@ -356,6 +370,7 @@ ExplicitModelAdapter::~ExplicitModelAdapter() {
for (auto it : resultStates) {
// Apply the new update and get resulting state.
StateType* newState = this->applyUpdate(it.first, update);
+ probSum += update.getLikelihoodExpression()->getValueAsDouble(it.first);
// Insert the new state into newStates array.
// Take care of calculation of likelihood, combine identical states.
auto s = newStates.find(newState);
@@ -366,6 +381,10 @@ ExplicitModelAdapter::~ExplicitModelAdapter() {
}
}
}
+ if (std::abs(1 - probSum) > this->precision) {
+ LOG4CPLUS_ERROR(logger, "Sum of update probabilities should be one for command:\n\t" << command.toString());
+ throw storm::exceptions::WrongFileFormatException() << "Sum of update probabilities should be one for command:\n\t" << command.toString();
+ }
}
for (auto it: resultStates) {
delete it.first;
@@ -437,6 +456,12 @@ ExplicitModelAdapter::~ExplicitModelAdapter() {
}
}
}
+ if (state < 5) {
+ std::cerr << "From " << state << std::endl;
+ for (auto it: map) {
+ std::cerr << "\t" << it.first << ": " << it.second << std::endl;
+ }
+ }
// Scale probabilities by number of choices.
double factor = 1.0 / transitionMap[state].size();
for (auto it : map) {
diff --git a/src/adapters/ExplicitModelAdapter.h b/src/adapters/ExplicitModelAdapter.h
index f97f76c5e..272d79c10 100644
--- a/src/adapters/ExplicitModelAdapter.h
+++ b/src/adapters/ExplicitModelAdapter.h
@@ -60,6 +60,8 @@ public:
private:
+ double precision;
+
// First some generic routines to operate on states.
/*!
diff --git a/src/parser/PrismParser.cpp b/src/parser/PrismParser.cpp
index 1df11819e..4a9678827 100644
--- a/src/parser/PrismParser.cpp
+++ b/src/parser/PrismParser.cpp
@@ -56,10 +56,12 @@ namespace parser {
mapping[name] = value;
}
void PrismParser::PrismGrammar::addIntAssignment(const std::string& variable, std::shared_ptr<BaseExpression> value, std::map<std::string, Assignment>& mapping) {
+ //std::cout << "Adding int assignment for " << variable << std::endl;
this->state->assignedLocalIntegerVariables_.add(variable, variable);
mapping[variable] = Assignment(variable, value);
}
void PrismParser::PrismGrammar::addBoolAssignment(const std::string& variable, std::shared_ptr<BaseExpression> value, std::map<std::string, Assignment>& mapping) {
+ //std::cout << "Adding bool assignment for " << variable << std::endl;
this->state->assignedLocalBooleanVariables_.add(variable, variable);
mapping[variable] = Assignment(variable, value);
}
@@ -81,6 +83,21 @@ namespace parser {
return res;
}
+ void PrismParser::PrismGrammar::createIntegerVariable(const std::string name, std::shared_ptr<BaseExpression> lower, std::shared_ptr<BaseExpression> upper, std::shared_ptr<BaseExpression> init, std::vector<IntegerVariable>& vars, std::map<std::string, uint_fast64_t>& varids) {
+ //std::cout << "Creating int " << name << " = " << init << std::endl;
+ uint_fast64_t id = this->state->addIntegerVariable(name, lower, upper, init);
+ vars.emplace_back(id, name, lower, upper, init);
+ varids[name] = id;
+ this->state->localIntegerVariables_.add(name, name);
+ }
+ void PrismParser::PrismGrammar::createBooleanVariable(const std::string name, std::shared_ptr<BaseExpression> init, std::vector<BooleanVariable>& vars, std::map<std::string, uint_fast64_t>& varids) {
+ //std::cout << "Creating bool " << name << std::endl;
+ uint_fast64_t id = this->state->addBooleanVariable(name, init);
+ vars.emplace_back(id, name, init);
+ varids[name] = id;
+ this->state->localBooleanVariables_.add(name, name);
+ }
+
StateReward createStateReward(std::shared_ptr<BaseExpression> guard, std::shared_ptr<BaseExpression> reward) {
return StateReward(guard, reward);
}
@@ -140,7 +157,8 @@ PrismParser::PrismGrammar::PrismGrammar() : PrismParser::PrismGrammar::base_type
assignmentDefinition.name("assignment");
assignmentDefinitionList = assignmentDefinition(qi::_r1, qi::_r2) % "&";
assignmentDefinitionList.name("assignment list");
- updateDefinition = (prism::ConstDoubleExpressionGrammar::instance(this->state) > qi::lit(":")[phoenix::clear(phoenix::ref(this->state->assignedLocalBooleanVariables_)), phoenix::clear(phoenix::ref(this->state->assignedLocalIntegerVariables_))] > assignmentDefinitionList(qi::_a, qi::_b))[qi::_val = phoenix::bind(&createUpdate, qi::_1, qi::_a, qi::_b)];
+ updateDefinition = (
+ prism::ConstDoubleExpressionGrammar::instance(this->state) > qi::lit(":")[phoenix::clear(phoenix::ref(this->state->assignedLocalBooleanVariables_)), phoenix::clear(phoenix::ref(this->state->assignedLocalIntegerVariables_))] > assignmentDefinitionList(qi::_a, qi::_b))[qi::_val = phoenix::bind(&createUpdate, qi::_1, qi::_a, qi::_b)];
updateDefinition.name("update");
updateListDefinition = +updateDefinition % "+";
updateListDefinition.name("update list");
@@ -154,22 +172,13 @@ PrismParser::PrismGrammar::PrismGrammar() : PrismParser::PrismGrammar::base_type
// This block defines all entities that are needed for parsing variable definitions.
booleanVariableDefinition = (prism::FreeIdentifierGrammar::instance(this->state) >> qi::lit(":") >> qi::lit("bool") > -(qi::lit("init") > prism::ConstBooleanExpressionGrammar::instance(this->state)[qi::_b = phoenix::construct<std::shared_ptr<BaseExpression>>(qi::_1)]) > qi::lit(";"))
[
- //qi::_a = phoenix::bind(&VariableState<Iterator,Skipper>::addBooleanVariable, *this->state.get(), qi::_1),
- qi::_a = phoenix::bind(&storm::parser::prism::VariableState::addBooleanVariable, *this->state, qi::_1, qi::_b),
- phoenix::push_back(qi::_r1, phoenix::construct<BooleanVariable>(qi::_a, phoenix::val(qi::_1), qi::_b)),
- phoenix::insert(qi::_r2, phoenix::construct<std::pair<std::string, uint_fast64_t>>(qi::_1, qi::_a)),
- phoenix::bind(this->state->localBooleanVariables_.add, qi::_1, qi::_1)
+ phoenix::bind(&PrismParser::PrismGrammar::createBooleanVariable, this, qi::_1, qi::_b, qi::_r1, qi::_r2)
];
booleanVariableDefinition.name("boolean variable declaration");
- integerLiteralExpression = qi::int_[qi::_val = phoenix::construct<std::shared_ptr<BaseExpression>>(phoenix::new_<IntegerLiteral>(qi::_1))];
- integerLiteralExpression.name("integer literal");
- integerVariableDefinition = (prism::FreeIdentifierGrammar::instance(this->state) >> qi::lit(":") >> qi::lit("[") > integerLiteralExpression > qi::lit("..") > integerLiteralExpression > qi::lit("]") > -(qi::lit("init") > prism::ConstIntegerExpressionGrammar::instance(this->state)[qi::_b = phoenix::construct<std::shared_ptr<BaseExpression>>(qi::_1)]) > qi::lit(";"))
+ integerVariableDefinition = (prism::FreeIdentifierGrammar::instance(this->state) >> qi::lit(":") >> qi::lit("[") > prism::ConstIntegerExpressionGrammar::instance(this->state) > qi::lit("..") > prism::ConstIntegerExpressionGrammar::instance(this->state) > qi::lit("]") > -(qi::lit("init") > prism::ConstIntegerExpressionGrammar::instance(this->state)[qi::_b = phoenix::construct<std::shared_ptr<BaseExpression>>(qi::_1)]) > qi::lit(";"))
[
- qi::_a = phoenix::bind(&storm::parser::prism::VariableState::addIntegerVariable, *this->state, qi::_1, qi::_2, qi::_3, qi::_b),
- phoenix::push_back(qi::_r1, phoenix::construct<IntegerVariable>(qi::_a, qi::_1, qi::_2, qi::_3, qi::_b)),
- phoenix::insert(qi::_r2, phoenix::construct<std::pair<std::string, uint_fast64_t>>(qi::_1, qi::_a)),
- phoenix::bind(this->state->localIntegerVariables_.add, qi::_1, qi::_1)
+ phoenix::bind(&PrismParser::PrismGrammar::createIntegerVariable, this, qi::_1, qi::_2, qi::_3, qi::_b, qi::_r1, qi::_r2)
];
integerVariableDefinition.name("integer variable declaration");
variableDefinition = (booleanVariableDefinition(qi::_r1, qi::_r3) | integerVariableDefinition(qi::_r2, qi::_r4));
@@ -228,6 +237,11 @@ PrismParser::PrismGrammar::PrismGrammar() : PrismParser::PrismGrammar::base_type
void PrismParser::PrismGrammar::prepareForSecondRun() {
this->state->prepareForSecondRun();
+ prism::BooleanExpressionGrammar::secondRun();
+ prism::ConstBooleanExpressionGrammar::secondRun();
+ prism::ConstDoubleExpressionGrammar::secondRun();
+ prism::ConstIntegerExpressionGrammar::secondRun();
+ prism::IntegerExpressionGrammar::secondRun();
}
/*!
diff --git a/src/parser/PrismParser.h b/src/parser/PrismParser.h
index 10cdeb895..32a797adf 100644
--- a/src/parser/PrismParser.h
+++ b/src/parser/PrismParser.h
@@ -64,82 +64,83 @@ public:
private:
- std::shared_ptr<storm::parser::prism::VariableState> state;
-
- // The starting point of the grammar.
- qi::rule<
- Iterator,
- Program(),
- qi::locals<
- std::map<std::string, std::shared_ptr<BooleanConstantExpression>>,
- std::map<std::string, std::shared_ptr<IntegerConstantExpression>>,
- std::map<std::string, std::shared_ptr<DoubleConstantExpression>>,
- std::map<std::string, RewardModel>,
- std::map<std::string, std::shared_ptr<BaseExpression>>
- >,
- Skipper> start;
- qi::rule<Iterator, Program::ModelType(), Skipper> modelTypeDefinition;
- qi::rule<Iterator, qi::unused_type(std::map<std::string, std::shared_ptr<BooleanConstantExpression>>&, std::map<std::string, std::shared_ptr<IntegerConstantExpression>>&, std::map<std::string, std::shared_ptr<DoubleConstantExpression>>&), Skipper> constantDefinitionList;
- qi::rule<Iterator, std::vector<Module>(), Skipper> moduleDefinitionList;
-
- // Rules for module definition.
- qi::rule<Iterator, Module(), qi::locals<std::vector<BooleanVariable>, std::vector<IntegerVariable>, std::map<std::string, uint_fast64_t>, std::map<std::string, uint_fast64_t>>, Skipper> moduleDefinition;
- qi::rule<Iterator, Module(), qi::locals<std::map<std::string, std::string>>, Skipper> moduleRenaming;
-
- // Rules for variable definitions.
- qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> integerLiteralExpression;
- qi::rule<Iterator, qi::unused_type(std::vector<BooleanVariable>&, std::vector<IntegerVariable>&, std::map<std::string, uint_fast64_t>&, std::map<std::string, uint_fast64_t>&), Skipper> variableDefinition;
- qi::rule<Iterator, qi::unused_type(std::vector<BooleanVariable>&, std::map<std::string, uint_fast64_t>&), qi::locals<uint_fast64_t, std::shared_ptr<BaseExpression>>, Skipper> booleanVariableDefinition;
- qi::rule<Iterator, qi::unused_type(std::vector<IntegerVariable>&, std::map<std::string, uint_fast64_t>&), qi::locals<uint_fast64_t, std::shared_ptr<BaseExpression>>, Skipper> integerVariableDefinition;
-
- // Rules for command definitions.
- qi::rule<Iterator, Command(), qi::locals<std::string>, Skipper> commandDefinition;
- qi::rule<Iterator, std::vector<Update>(), Skipper> updateListDefinition;
- qi::rule<Iterator, Update(), qi::locals<std::map<std::string, Assignment>, std::map<std::string, Assignment>>, Skipper> updateDefinition;
- qi::rule<Iterator, qi::unused_type(std::map<std::string, Assignment>&, std::map<std::string, Assignment>&), Skipper> assignmentDefinitionList;
- qi::rule<Iterator, qi::unused_type(std::map<std::string, Assignment>&, std::map<std::string, Assignment>&), Skipper> assignmentDefinition;
-
- // Rules for variable/command names.
- qi::rule<Iterator, std::string(), Skipper> commandName;
- qi::rule<Iterator, std::string(), Skipper> unassignedLocalBooleanVariableName;
- qi::rule<Iterator, std::string(), Skipper> unassignedLocalIntegerVariableName;
-
- // Rules for reward definitions.
- qi::rule<Iterator, qi::unused_type(std::map<std::string, RewardModel>&), Skipper> rewardDefinitionList;
- qi::rule<Iterator, qi::unused_type(std::map<std::string, RewardModel>&), qi::locals<std::vector<StateReward>, std::vector<TransitionReward>>, Skipper> rewardDefinition;
- qi::rule<Iterator, StateReward(), Skipper> stateRewardDefinition;
- qi::rule<Iterator, TransitionReward(), qi::locals<std::string>, Skipper> transitionRewardDefinition;
-
- // Rules for label definitions.
- qi::rule<Iterator, qi::unused_type(std::map<std::string, std::shared_ptr<BaseExpression>>&), Skipper> labelDefinitionList;
- qi::rule<Iterator, qi::unused_type(std::map<std::string, std::shared_ptr<BaseExpression>>&), Skipper> labelDefinition;
-
- // Rules for constant definitions.
- qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> constantDefinition;
- qi::rule<Iterator, qi::unused_type(std::map<std::string, std::shared_ptr<BooleanConstantExpression>>&, std::map<std::string, std::shared_ptr<IntegerConstantExpression>>&, std::map<std::string, std::shared_ptr<DoubleConstantExpression>>&), Skipper> undefinedConstantDefinition;
- qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> definedConstantDefinition;
- qi::rule<Iterator, qi::unused_type(std::map<std::string, std::shared_ptr<BooleanConstantExpression>>&), qi::locals<std::shared_ptr<BooleanConstantExpression>>, Skipper> undefinedBooleanConstantDefinition;
- qi::rule<Iterator, qi::unused_type(std::map<std::string, std::shared_ptr<IntegerConstantExpression>>&), qi::locals<std::shared_ptr<IntegerConstantExpression>>, Skipper> undefinedIntegerConstantDefinition;
- qi::rule<Iterator, qi::unused_type(std::map<std::string, std::shared_ptr<DoubleConstantExpression>>&), qi::locals<std::shared_ptr<DoubleConstantExpression>>, Skipper> undefinedDoubleConstantDefinition;
- qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> definedBooleanConstantDefinition;
- qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> definedIntegerConstantDefinition;
- qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> definedDoubleConstantDefinition;
-
- // Rules for variable recognition.
- qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> booleanVariableCreatorExpression;
- qi::rule<Iterator, std::shared_ptr<BaseExpression>(), qi::locals<std::shared_ptr<BaseExpression>>, Skipper> integerVariableCreatorExpression;
-
- storm::parser::prism::keywordsStruct keywords_;
- storm::parser::prism::modelTypeStruct modelType_;
- storm::parser::prism::relationalOperatorStruct relations_;
-
- std::shared_ptr<BaseExpression> addIntegerConstant(const std::string& name, const std::shared_ptr<BaseExpression> value);
- void addLabel(const std::string& name, std::shared_ptr<BaseExpression> value, std::map<std::string, std::shared_ptr<BaseExpression>>& mapping);
- void addBoolAssignment(const std::string& variable, std::shared_ptr<BaseExpression> value, std::map<std::string, Assignment>& mapping);
- void addIntAssignment(const std::string& variable, std::shared_ptr<BaseExpression> value, std::map<std::string, Assignment>& mapping);
- Module renameModule(const std::string& name, const std::string& oldname, std::map<std::string, std::string>& mapping);
- Module createModule(const std::string name, std::vector<BooleanVariable>& bools, std::vector<IntegerVariable>& ints, std::map<std::string, uint_fast64_t>& boolids, std::map<std::string, uint_fast64_t> intids, std::vector<storm::ir::Command> commands);
-
+ std::shared_ptr<storm::parser::prism::VariableState> state;
+
+ // The starting point of the grammar.
+ qi::rule<
+ Iterator,
+ Program(),
+ qi::locals<
+ std::map<std::string, std::shared_ptr<BooleanConstantExpression>>,
+ std::map<std::string, std::shared_ptr<IntegerConstantExpression>>,
+ std::map<std::string, std::shared_ptr<DoubleConstantExpression>>,
+ std::map<std::string, RewardModel>,
+ std::map<std::string, std::shared_ptr<BaseExpression>>
+ >,
+ Skipper> start;
+ qi::rule<Iterator, Program::ModelType(), Skipper> modelTypeDefinition;
+ qi::rule<Iterator, qi::unused_type(std::map<std::string, std::shared_ptr<BooleanConstantExpression>>&, std::map<std::string, std::shared_ptr<IntegerConstantExpression>>&, std::map<std::string, std::shared_ptr<DoubleConstantExpression>>&), Skipper> constantDefinitionList;
+ qi::rule<Iterator, std::vector<Module>(), Skipper> moduleDefinitionList;
+
+ // Rules for module definition.
+ qi::rule<Iterator, Module(), qi::locals<std::vector<BooleanVariable>, std::vector<IntegerVariable>, std::map<std::string, uint_fast64_t>, std::map<std::string, uint_fast64_t>>, Skipper> moduleDefinition;
+ qi::rule<Iterator, Module(), qi::locals<std::map<std::string, std::string>>, Skipper> moduleRenaming;
+
+ // Rules for variable definitions.
+ qi::rule<Iterator, qi::unused_type(std::vector<BooleanVariable>&, std::vector<IntegerVariable>&, std::map<std::string, uint_fast64_t>&, std::map<std::string, uint_fast64_t>&), Skipper> variableDefinition;
+ qi::rule<Iterator, qi::unused_type(std::vector<BooleanVariable>&, std::map<std::string, uint_fast64_t>&), qi::locals<uint_fast64_t, std::shared_ptr<BaseExpression>>, Skipper> booleanVariableDefinition;
+ qi::rule<Iterator, qi::unused_type(std::vector<IntegerVariable>&, std::map<std::string, uint_fast64_t>&), qi::locals<uint_fast64_t, std::shared_ptr<BaseExpression>>, Skipper> integerVariableDefinition;
+
+ // Rules for command definitions.
+ qi::rule<Iterator, Command(), qi::locals<std::string>, Skipper> commandDefinition;
+ qi::rule<Iterator, std::vector<Update>(), Skipper> updateListDefinition;
+ qi::rule<Iterator, Update(), qi::locals<std::map<std::string, Assignment>, std::map<std::string, Assignment>>, Skipper> updateDefinition;
+ qi::rule<Iterator, qi::unused_type(std::map<std::string, Assignment>&, std::map<std::string, Assignment>&), Skipper> assignmentDefinitionList;
+ qi::rule<Iterator, qi::unused_type(std::map<std::string, Assignment>&, std::map<std::string, Assignment>&), Skipper> assignmentDefinition;
+
+ // Rules for variable/command names.
+ qi::rule<Iterator, std::string(), Skipper> commandName;
+ qi::rule<Iterator, std::string(), Skipper> unassignedLocalBooleanVariableName;
+ qi::rule<Iterator, std::string(), Skipper> unassignedLocalIntegerVariableName;
+
+ // Rules for reward definitions.
+ qi::rule<Iterator, qi::unused_type(std::map<std::string, RewardModel>&), Skipper> rewardDefinitionList;
+ qi::rule<Iterator, qi::unused_type(std::map<std::string, RewardModel>&), qi::locals<std::vector<StateReward>, std::vector<TransitionReward>>, Skipper> rewardDefinition;
+ qi::rule<Iterator, StateReward(), Skipper> stateRewardDefinition;
+ qi::rule<Iterator, TransitionReward(), qi::locals<std::string>, Skipper> transitionRewardDefinition;
+
+ // Rules for label definitions.
+ qi::rule<Iterator, qi::unused_type(std::map<std::string, std::shared_ptr<BaseExpression>>&), Skipper> labelDefinitionList;
+ qi::rule<Iterator, qi::unused_type(std::map<std::string, std::shared_ptr<BaseExpression>>&), Skipper> labelDefinition;
+
+ // Rules for constant definitions.
+ qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> constantDefinition;
+ qi::rule<Iterator, qi::unused_type(std::map<std::string, std::shared_ptr<BooleanConstantExpression>>&, std::map<std::string, std::shared_ptr<IntegerConstantExpression>>&, std::map<std::string, std::shared_ptr<DoubleConstantExpression>>&), Skipper> undefinedConstantDefinition;
+ qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> definedConstantDefinition;
+ qi::rule<Iterator, qi::unused_type(std::map<std::string, std::shared_ptr<BooleanConstantExpression>>&), qi::locals<std::shared_ptr<BooleanConstantExpression>>, Skipper> undefinedBooleanConstantDefinition;
+ qi::rule<Iterator, qi::unused_type(std::map<std::string, std::shared_ptr<IntegerConstantExpression>>&), qi::locals<std::shared_ptr<IntegerConstantExpression>>, Skipper> undefinedIntegerConstantDefinition;
+ qi::rule<Iterator, qi::unused_type(std::map<std::string, std::shared_ptr<DoubleConstantExpression>>&), qi::locals<std::shared_ptr<DoubleConstantExpression>>, Skipper> undefinedDoubleConstantDefinition;
+ qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> definedBooleanConstantDefinition;
+ qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> definedIntegerConstantDefinition;
+ qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> definedDoubleConstantDefinition;
+
+ // Rules for variable recognition.
+ qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> booleanVariableCreatorExpression;
+ qi::rule<Iterator, std::shared_ptr<BaseExpression>(), qi::locals<std::shared_ptr<BaseExpression>>, Skipper> integerVariableCreatorExpression;
+
+ storm::parser::prism::keywordsStruct keywords_;
+ storm::parser::prism::modelTypeStruct modelType_;
+ storm::parser::prism::relationalOperatorStruct relations_;
+
+ std::shared_ptr<BaseExpression> addIntegerConstant(const std::string& name, const std::shared_ptr<BaseExpression> value);
+ void addLabel(const std::string& name, std::shared_ptr<BaseExpression> value, std::map<std::string, std::shared_ptr<BaseExpression>>& mapping);
+ void addBoolAssignment(const std::string& variable, std::shared_ptr<BaseExpression> value, std::map<std::string, Assignment>& mapping);
+ void addIntAssignment(const std::string& variable, std::shared_ptr<BaseExpression> value, std::map<std::string, Assignment>& mapping);
+ Module renameModule(const std::string& name, const std::string& oldname, std::map<std::string, std::string>& mapping);
+ Module createModule(const std::string name, std::vector<BooleanVariable>& bools, std::vector<IntegerVariable>& ints, std::map<std::string, uint_fast64_t>& boolids, std::map<std::string, uint_fast64_t> intids, std::vector<storm::ir::Command> commands);
+
+ void createIntegerVariable(const std::string name, std::shared_ptr<BaseExpression> lower, std::shared_ptr<BaseExpression> upper, std::shared_ptr<BaseExpression> init, std::vector<IntegerVariable>& vars, std::map<std::string, uint_fast64_t>& varids);
+ void createBooleanVariable(const std::string name, std::shared_ptr<BaseExpression> init, std::vector<BooleanVariable>& vars, std::map<std::string, uint_fast64_t>& varids);
};
private:
diff --git a/src/parser/PrismParser/BaseGrammar.h b/src/parser/PrismParser/BaseGrammar.h
index bcc5f3d44..0846eb12c 100644
--- a/src/parser/PrismParser/BaseGrammar.h
+++ b/src/parser/PrismParser/BaseGrammar.h
@@ -24,10 +24,18 @@ namespace prism {
static T& instance(std::shared_ptr<VariableState>& state = nullptr) {
if (BaseGrammar::instanceObject == nullptr) {
BaseGrammar::instanceObject = std::shared_ptr<T>(new T(state));
+ if (!state->firstRun) BaseGrammar::instanceObject->secondRun();
}
return *BaseGrammar::instanceObject;
}
+ static void secondRun() {
+ if (BaseGrammar::instanceObject != nullptr) {
+ BaseGrammar::instanceObject->prepareSecondRun();
+ }
+
+ }
+
std::shared_ptr<BaseExpression> createBoolLiteral(const bool value) {
return std::shared_ptr<BooleanLiteral>(new BooleanLiteral(value));
}
@@ -70,6 +78,7 @@ namespace prism {
return std::shared_ptr<UnaryBooleanFunctionExpression>(new UnaryBooleanFunctionExpression(child, UnaryBooleanFunctionExpression::NOT));
}
std::shared_ptr<BaseExpression> createAnd(std::shared_ptr<BaseExpression> left, std::shared_ptr<BaseExpression> right) {
+ //std::cerr << "Creating " << left->toString() << " & " << right->toString() << std::endl;
return std::shared_ptr<BinaryBooleanFunctionExpression>(new BinaryBooleanFunctionExpression(left, right, BinaryBooleanFunctionExpression::AND));
}
std::shared_ptr<BaseExpression> createOr(std::shared_ptr<BaseExpression> left, std::shared_ptr<BaseExpression> right) {
@@ -82,11 +91,13 @@ namespace prism {
return state->getIntegerVariable(name);
}
+ virtual void prepareSecondRun() {}
protected:
std::shared_ptr<VariableState> state;
private:
static std::shared_ptr<T> instanceObject;
+ static bool inSecondRun;
};
template <typename T>
diff --git a/src/parser/PrismParser/BooleanExpressionGrammar.cpp b/src/parser/PrismParser/BooleanExpressionGrammar.cpp
index 101db9cce..00ca2fe40 100644
--- a/src/parser/PrismParser/BooleanExpressionGrammar.cpp
+++ b/src/parser/PrismParser/BooleanExpressionGrammar.cpp
@@ -7,10 +7,10 @@ namespace storm {
namespace parser {
namespace prism {
-BooleanExpressionGrammar::BooleanExpressionGrammar(std::shared_ptr<VariableState>& state)
- : BooleanExpressionGrammar::base_type(booleanExpression), BaseGrammar(state) {
+ BooleanExpressionGrammar::BooleanExpressionGrammar(std::shared_ptr<VariableState>& state)
+ : BooleanExpressionGrammar::base_type(booleanExpression), BaseGrammar(state) {
- booleanExpression %= orExpression;
+ booleanExpression %= orExpression;
booleanExpression.name("boolean expression");
orExpression = andExpression[qi::_val = qi::_1] >> *(qi::lit("|") >> andExpression)[qi::_val = phoenix::bind(&BaseGrammar::createOr, this, qi::_val, qi::_1)];
@@ -32,6 +32,11 @@ BooleanExpressionGrammar::BooleanExpressionGrammar(std::shared_ptr<VariableState
booleanVariableExpression.name("boolean variable");
}
+ void BooleanExpressionGrammar::prepareSecondRun() {
+ booleanVariableExpression = this->state->booleanVariables_;
+ booleanVariableExpression.name("boolean variable");
+ }
+
}
}
}
\ No newline at end of file
diff --git a/src/parser/PrismParser/BooleanExpressionGrammar.h b/src/parser/PrismParser/BooleanExpressionGrammar.h
index 9d14c5ec3..9e976e64d 100644
--- a/src/parser/PrismParser/BooleanExpressionGrammar.h
+++ b/src/parser/PrismParser/BooleanExpressionGrammar.h
@@ -22,7 +22,8 @@ namespace prism {
class BooleanExpressionGrammar : public qi::grammar<Iterator, std::shared_ptr<BaseExpression>(), Skipper, Unused>, public BaseGrammar<BooleanExpressionGrammar> {
public:
BooleanExpressionGrammar(std::shared_ptr<VariableState>& state);
-
+ virtual void prepareSecondRun();
+
private:
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper, Unused> booleanExpression;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> orExpression;
diff --git a/src/parser/PrismParser/IntegerExpressionGrammar.cpp b/src/parser/PrismParser/IntegerExpressionGrammar.cpp
index 89933aeb3..e0e363030 100644
--- a/src/parser/PrismParser/IntegerExpressionGrammar.cpp
+++ b/src/parser/PrismParser/IntegerExpressionGrammar.cpp
@@ -26,6 +26,11 @@ namespace prism {
integerVariableExpression.name("integer variable");
}
+ void IntegerExpressionGrammar::prepareSecondRun() {
+ integerVariableExpression = this->state->integerVariables_;
+ integerVariableExpression.name("integer variable");
+ }
+
}
}
}
\ No newline at end of file
diff --git a/src/parser/PrismParser/IntegerExpressionGrammar.h b/src/parser/PrismParser/IntegerExpressionGrammar.h
index 5c253e437..0f44b0d01 100644
--- a/src/parser/PrismParser/IntegerExpressionGrammar.h
+++ b/src/parser/PrismParser/IntegerExpressionGrammar.h
@@ -22,6 +22,7 @@ namespace prism {
class IntegerExpressionGrammar : public qi::grammar<Iterator, std::shared_ptr<BaseExpression>(), Skipper, Unused>, public BaseGrammar<IntegerExpressionGrammar> {
public:
IntegerExpressionGrammar(std::shared_ptr<VariableState>& state);
+ virtual void prepareSecondRun();
private:
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper, Unused> integerExpression;
diff --git a/src/parser/PrismParser/VariableState.h b/src/parser/PrismParser/VariableState.h
index e6c99d9ab..e94d44056 100644
--- a/src/parser/PrismParser/VariableState.h
+++ b/src/parser/PrismParser/VariableState.h
@@ -45,13 +45,12 @@ public:
localBooleanVariables_, localIntegerVariables_, assignedLocalBooleanVariables_, assignedLocalIntegerVariables_;
uint_fast64_t addBooleanVariable(const std::string& name, const std::shared_ptr<storm::ir::expressions::BaseExpression> init) {
- //std::cerr << "adding boolean variable " << name << std::endl;
if (firstRun) {
std::shared_ptr<VariableExpression> varExpr = std::shared_ptr<VariableExpression>(new VariableExpression(storm::ir::expressions::BaseExpression::bool_, this->nextBooleanVariableIndex, name));
this->booleanVariables_.add(name, varExpr);
this->booleanVariableNames_.add(name, name);
this->nextBooleanVariableIndex++;
- return this->nextBooleanVariableIndex-1;
+ return varExpr->getVariableIndex();
} else {
std::shared_ptr<VariableExpression> res = this->booleanVariables_.at(name);
if (res != nullptr) {
@@ -70,7 +69,7 @@ public:
this->integerVariables_.add(name, varExpr);
this->integerVariableNames_.add(name, name);
this->nextIntegerVariableIndex++;
- return this->nextIntegerVariableIndex-1;
+ return varExpr->getVariableIndex();
} else {
std::shared_ptr<VariableExpression> res = this->integerVariables_.at(name);
if (res != nullptr) {
@@ -83,7 +82,6 @@ public:
}
std::shared_ptr<VariableExpression> getBooleanVariable(const std::string& name) {
- //std::cerr << "getting boolen variable " << name << std::endl;
std::shared_ptr<VariableExpression> res = this->booleanVariables_.at(name);
if (res != nullptr) {
return res;
@@ -91,7 +89,7 @@ public:
if (firstRun) {
return std::shared_ptr<VariableExpression>(new VariableExpression(BaseExpression::bool_, std::numeric_limits<uint_fast64_t>::max(), "bool", std::shared_ptr<BaseExpression>(nullptr), std::shared_ptr<BaseExpression>(nullptr)));
} else {
- std::cerr << "Variable " << name << " was not created in first run" << std::endl;
+ std::cerr << "bool Variable " << name << " was not created in first run" << std::endl;
return std::shared_ptr<VariableExpression>(nullptr);
}
}
@@ -106,7 +104,7 @@ public:
if (firstRun) {
return std::shared_ptr<VariableExpression>(new VariableExpression(BaseExpression::int_, std::numeric_limits<uint_fast64_t>::max(), "int", std::shared_ptr<BaseExpression>(nullptr), std::shared_ptr<BaseExpression>(nullptr)));
} else {
- std::cerr << "Variable " << name << " was not created in first run" << std::endl;
+ std::cerr << "int Variable " << name << " was not created in first run" << std::endl;
return std::shared_ptr<VariableExpression>(nullptr);
}
}