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

Create copy of lattice and assumptionslist at earlier point

tempestpy_adaptions
Jip Spel 6 years ago
parent
728dc9e8a4
commit
dc52e9b056
3 changed files with 8 additions and 14 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. 20
      src/storm-pars/analysis/AssumptionMaker.cpp
  2. 1
      src/storm-pars/analysis/AssumptionMaker.h
  3. 1
      src/storm-pars/analysis/Lattice.cpp

20
src/storm-pars/analysis/AssumptionMaker.cpp
View File

@ -13,15 +13,12 @@ namespace storm {
this->expressionManager = std::make_shared<storm::expressions::ExpressionManager>(storm::expressions::ExpressionManager());
for (uint_fast64_t i = 0; i < this->numberOfStates; ++i) {
expressionManager->declareIntegerVariable(std::to_string(i));
expressionManager->declareFreshIntegerVariable();
}
}
template<typename ValueType>
std::map<storm::analysis::Lattice*, std::set<std::shared_ptr<storm::expressions::BinaryRelationExpression>>>
AssumptionMaker<ValueType>::startMakingAssumptions(storm::analysis::Lattice* lattice, uint_fast64_t critical1, uint_fast64_t critical2) {
std::map<storm::analysis::Lattice*, std::set<std::shared_ptr<storm::expressions::BinaryRelationExpression>>> result;
std::set<std::shared_ptr<storm::expressions::BinaryRelationExpression>> emptySet;
@ -32,7 +29,9 @@ namespace storm {
storm::expressions::Variable var2 = expressionManager->getVariable(std::to_string(critical2));
std::set<std::shared_ptr<storm::expressions::BinaryRelationExpression>> assumptions;
auto myMap = createAssumptions(var1, var2, lattice, assumptions);
auto latticeCopy = new Lattice(lattice);
std::set<std::shared_ptr<storm::expressions::BinaryRelationExpression>> assumptionsCopy = std::set<std::shared_ptr<storm::expressions::BinaryRelationExpression>>(assumptions);
auto myMap = createAssumptions(var1, var2, latticeCopy, assumptionsCopy);
result.insert(myMap.begin(), myMap.end());
myMap = createAssumptions(var2, var1, lattice, assumptions);
@ -52,7 +51,9 @@ namespace storm {
storm::expressions::Variable var1 = expressionManager->getVariable(std::to_string(std::get<1>(criticalPair)));
storm::expressions::Variable var2 = expressionManager->getVariable(std::to_string(std::get<2>(criticalPair)));
auto myMap = createAssumptions(var1, var2, lattice, assumptions);
auto latticeCopy = new Lattice(lattice);
std::set<std::shared_ptr<storm::expressions::BinaryRelationExpression>> assumptionsCopy = std::set<std::shared_ptr<storm::expressions::BinaryRelationExpression>>(assumptions);
auto myMap = createAssumptions(var1, var2, latticeCopy, assumptionsCopy);
result.insert(myMap.begin(), myMap.end());
myMap = createAssumptions(var2, var1, lattice, assumptions);
result.insert(myMap.begin(), myMap.end());
@ -63,19 +64,14 @@ namespace storm {
template <typename ValueType>
std::map<storm::analysis::Lattice*, std::set<std::shared_ptr<storm::expressions::BinaryRelationExpression>>> AssumptionMaker<ValueType>::createAssumptions(storm::expressions::Variable var1, storm::expressions::Variable var2, storm::analysis::Lattice* lattice, std::set<std::shared_ptr<storm::expressions::BinaryRelationExpression>> assumptions) {
std::set<std::shared_ptr<storm::expressions::BinaryRelationExpression>> assumptions1 = std::set<std::shared_ptr<storm::expressions::BinaryRelationExpression>>(assumptions);
std::shared_ptr<storm::expressions::BinaryRelationExpression> assumption1
= std::make_shared<storm::expressions::BinaryRelationExpression>(storm::expressions::BinaryRelationExpression(*expressionManager, var1.getType(),
var1.getExpression().getBaseExpressionPointer(), var2.getExpression().getBaseExpressionPointer(),
storm::expressions::BinaryRelationExpression::RelationType::Greater));
assumptions1.insert(assumption1);
auto lattice1 = new Lattice(lattice);
return (runRecursive(lattice1, assumptions1));
assumptions.insert(assumption1);
return (runRecursive(lattice, assumptions));
}
template class AssumptionMaker<storm::RationalFunction>;
}
}
// Een map met daarin een pointer naar de lattic en een set met de geldende assumptions voor die lattice

1
src/storm-pars/analysis/AssumptionMaker.h
View File

@ -19,7 +19,6 @@ namespace storm {
std::map<storm::analysis::Lattice*, std::set<std::shared_ptr<storm::expressions::BinaryRelationExpression>>> startMakingAssumptions(storm::analysis::Lattice* lattice, uint_fast64_t critical1, uint_fast64_t critical2);
private:
std::map<storm::analysis::Lattice*, std::set<std::shared_ptr<storm::expressions::BinaryRelationExpression>>> runRecursive(storm::analysis::Lattice* lattice, std::set<std::shared_ptr<storm::expressions::BinaryRelationExpression>> assumptions);

1
src/storm-pars/analysis/Lattice.cpp
View File

@ -139,7 +139,6 @@ namespace storm {
return UNKNOWN;
}
Lattice::Node *Lattice::getNode(uint_fast64_t stateNumber) {
return nodes.at(stateNumber);
}

Write Preview
Loading…
Cancel
Save