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

Fix for SAT-based minimal counterexample generator: backward cuts are now fully correct again. Fix for PRISM grammar: missing update probabilities now default to one. 

Former-commit-id: fc139c33d0
tempestpy_adaptions
dehnert 11 years ago
parent
8244420248
commit
6a4d2183dc
3 changed files with 27 additions and 17 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. 6
      src/counterexamples/SMTMinimalCommandSetGenerator.h
  2. 2
      src/parser/prismparser/PrismGrammar.cpp
  3. 36
      src/storm.cpp

6
src/counterexamples/SMTMinimalCommandSetGenerator.h
View File

@ -356,6 +356,7 @@ namespace storm {
// FIXME: Include synchronisation cuts.
// FIXME: Fix backward cuts in the presence of synchronizing actions.
std::map<uint_fast64_t, std::set<uint_fast64_t>> precedingLabels;
std::set<uint_fast64_t> hasSynchronizingPredecessor;
// Get some data from the MDP for convenient access.
storm::storage::SparseMatrix<T> const& transitionMatrix = labeledMdp.getTransitionMatrix();
@ -377,6 +378,11 @@ namespace storm {
}
if (choiceTargetsCurrentState) {
if (choiceLabeling.at(predecessorChoice).size() > 1) {
for (auto label : choiceLabeling.at(currentChoice)) {
hasSynchronizingPredecessor.insert(label);
}
}
for (auto labelToAdd : choiceLabeling[predecessorChoice]) {
for (auto labelForWhichToAdd : choiceLabeling[currentChoice]) {
precedingLabels[labelForWhichToAdd].insert(labelToAdd);

2
src/parser/prismparser/PrismGrammar.cpp
View File

@ -179,7 +179,7 @@ namespace storm {
assignmentDefinition.name("assignment");
assignmentDefinitionList = assignmentDefinition(qi::_r1, qi::_r2) % "&";
assignmentDefinitionList.name("assignment list");
updateDefinition = (ConstDoubleExpressionGrammar::instance(this->state) > qi::lit(":")[phoenix::clear(phoenix::ref(this->state->assignedBooleanVariables_)), phoenix::clear(phoenix::ref(this->state->assignedIntegerVariables_))] > assignmentDefinitionList(qi::_a, qi::_b))[qi::_val = phoenix::bind(&PrismGrammar::createUpdate, this, qi::_1, qi::_a, qi::_b)];
updateDefinition = ((ConstDoubleExpressionGrammar::instance(this->state) | qi::attr(phoenix::construct<std::shared_ptr<BaseExpression>>(phoenix::new_<storm::ir::expressions::DoubleLiteralExpression>(1)))) > qi::lit(":")[phoenix::clear(phoenix::ref(this->state->assignedBooleanVariables_)), phoenix::clear(phoenix::ref(this->state->assignedIntegerVariables_))] > assignmentDefinitionList(qi::_a, qi::_b))[qi::_val = phoenix::bind(&PrismGrammar::createUpdate, this, qi::_1, qi::_a, qi::_b)];
updateDefinition.name("update");
updateListDefinition = +updateDefinition % "+";
updateListDefinition.name("update list");

36
src/storm.cpp
View File

@ -338,28 +338,32 @@ int main(const int argc, const char* argv[]) {
model->printModelInformationToStream(std::cout);
// Enable the following lines to test the MinimalLabelSetGenerator.
if (model->getType() == storm::models::MDP) {
std::shared_ptr<storm::models::Mdp<double>> labeledMdp = model->as<storm::models::Mdp<double>>();
storm::storage::BitVector const& finishedStates = labeledMdp->getLabeledStates("finished");
storm::storage::BitVector const& allCoinsEqual1States = labeledMdp->getLabeledStates("all_coins_equal_1");
storm::storage::BitVector targetStates = finishedStates & allCoinsEqual1States;
std::set<uint_fast64_t> labels = storm::counterexamples::MILPMinimalLabelSetGenerator<double>::getMinimalLabelSet(*labeledMdp, storm::storage::BitVector(labeledMdp->getNumberOfStates(), true), targetStates, 0.4, true, true);
std::cout << "Found solution with " << labels.size() << " commands." << std::endl;
for (uint_fast64_t label : labels) {
std::cout << label << ", ";
}
std::cout << std::endl;
}
// Enable the following lines to test the SMTMinimalCommandSetGenerator.
// if (model->getType() == storm::models::MDP) {
// std::shared_ptr<storm::models::Mdp<double>> labeledMdp = model->as<storm::models::Mdp<double>>();
// storm::storage::BitVector const& finishedStates = labeledMdp->getLabeledStates("finished");
// storm::storage::BitVector const& allCoinsEqual1States = labeledMdp->getLabeledStates("all_coins_equal_1");
// storm::storage::BitVector targetStates = finishedStates & allCoinsEqual1States;
// std::set<uint_fast64_t> labels = storm::counterexamples::SMTMinimalCommandSetGenerator<double>::getMinimalCommandSet(program, constants, *labeledMdp, storm::storage::BitVector(labeledMdp->getNumberOfStates(), true), targetStates, 0.4, true);
// std::set<uint_fast64_t> labels = storm::counterexamples::MILPMinimalLabelSetGenerator<double>::getMinimalLabelSet(*labeledMdp, storm::storage::BitVector(labeledMdp->getNumberOfStates(), true), targetStates, 0.4, true, true);
//
// std::cout << "Found solution with " << labels.size() << " commands." << std::endl;
// for (uint_fast64_t label : labels) {
// std::cout << label << ", ";
// }
// std::cout << std::endl;
// }
// Enable the following lines to test the SMTMinimalCommandSetGenerator.
if (model->getType() == storm::models::MDP) {
std::shared_ptr<storm::models::Mdp<double>> labeledMdp = model->as<storm::models::Mdp<double>>();
// storm::storage::BitVector const& finishedStates = labeledMdp->getLabeledStates("finished");
// storm::storage::BitVector const& allCoinsEqual1States = labeledMdp->getLabeledStates("all_coins_equal_1");
// storm::storage::BitVector targetStates = finishedStates & allCoinsEqual1States;
// std::set<uint_fast64_t> labels = storm::counterexamples::SMTMinimalCommandSetGenerator<double>::getMinimalCommandSet(program, constants, *labeledMdp, storm::storage::BitVector(labeledMdp->getNumberOfStates(), true), targetStates, 0.4, true);
storm::storage::BitVector const& collisionStates = labeledMdp->getLabeledStates("collision_max_backoff");
storm::storage::BitVector const& deliveredStates = labeledMdp->getLabeledStates("all_delivered");
std::set<uint_fast64_t> labels = storm::counterexamples::MILPMinimalLabelSetGenerator<double>::getMinimalLabelSet(*labeledMdp, ~collisionStates, deliveredStates, 0.5, true, true);
}
}
// Perform clean-up and terminate.

Write Preview
Loading…
Cancel
Save