From 43eebf8e056c3d4eb1e53ef29a8ac235fc37d761 Mon Sep 17 00:00:00 2001
From: Jip Spel <jip.spel@cs.rwth-aachen.de>
Date: Fri, 31 Aug 2018 12:35:14 +0200
Subject: [PATCH] Return tuple and add assumptions
---
src/storm-pars-cli/storm-pars.cpp | 22 ++++++++++++++++-----
src/storm-pars/analysis/Lattice.h | 3 ---
src/storm-pars/analysis/LatticeExtender.cpp | 17 +++++++---------
src/storm-pars/analysis/LatticeExtender.h | 6 +++---
4 files changed, 27 insertions(+), 21 deletions(-)
diff --git a/src/storm-pars-cli/storm-pars.cpp b/src/storm-pars-cli/storm-pars.cpp
index b14285761..06f5a18c9 100644
--- a/src/storm-pars-cli/storm-pars.cpp
+++ b/src/storm-pars-cli/storm-pars.cpp
@@ -612,15 +612,27 @@ namespace storm {
// Transform to Lattice
storm::utility::Stopwatch latticeWatch(true);
storm::analysis::LatticeExtender<storm::models::sparse::Model<ValueType>> extender = storm::analysis::LatticeExtender<storm::models::sparse::Model<ValueType>>(sparseModel);
- storm::analysis::Lattice* lattice = extender.toLattice(formulas);
+ std::tuple<storm::analysis::Lattice*, uint_fast64_t, uint_fast64_t> criticalPair = extender.toLattice(formulas);
// Declare variables for all states
std::shared_ptr<storm::expressions::ExpressionManager> expressionManager(new storm::expressions::ExpressionManager());
- for (uint_fast64_t i = 0; i < sparseModel.get()->getNumberOfStates(); ++i) {
+ for (uint_fast64_t i = 0; i < sparseModel->getNumberOfStates(); ++i) {
expressionManager->declareFreshIntegerVariable();
}
-// std::set<storm::expressions::BinaryRelationExpression*> assumptions;
-// extender.extendLattice(lattice, expressionManager, assumptions);
+
+ // Make assumptions
+ std::set<storm::expressions::BinaryRelationExpression*> assumptions;
+ while (std::get<1>(criticalPair) != sparseModel->getNumberOfStates()) {
+ storm::expressions::Variable var1 = expressionManager->getVariable("_x" + std::to_string(std::get<1>(criticalPair)));
+ storm::expressions::Variable var2 = expressionManager->getVariable("_x" + std::to_string(std::get<2>(criticalPair)));
+ auto assumption = new storm::expressions::BinaryRelationExpression(*expressionManager, var1.getType(),
+ var1.getExpression().getBaseExpressionPointer(), var2.getExpression().getBaseExpressionPointer(),
+ storm::expressions::BinaryRelationExpression::RelationType::Greater);
+ assumptions.insert(assumption);
+ criticalPair = extender.extendLattice(std::get<0>(criticalPair), expressionManager, assumptions);
+ }
+ auto lattice = std::get<0>(criticalPair);
+
latticeWatch.stop();
STORM_PRINT(std::endl << "Time for lattice creation: " << latticeWatch << "." << std::endl << std::endl);
@@ -631,7 +643,7 @@ namespace storm {
myfile.close();
// Monotonicity?
- auto matrix = sparseModel.get()->getTransitionMatrix();
+ auto matrix = sparseModel->getTransitionMatrix();
storm::utility::Stopwatch monotonicityWatch(true);
std::map<carl::Variable, std::pair<bool, bool>> varsMonotone = analyseMonotonicity<ValueType>(lattice, matrix);
monotonicityWatch.stop();
diff --git a/src/storm-pars/analysis/Lattice.h b/src/storm-pars/analysis/Lattice.h
index 57fc43e13..dcfa8c552 100644
--- a/src/storm-pars/analysis/Lattice.h
+++ b/src/storm-pars/analysis/Lattice.h
@@ -11,9 +11,6 @@
#include "storm/storage/BitVector.h"
-
-
-
namespace storm {
namespace analysis {
class Lattice {
diff --git a/src/storm-pars/analysis/LatticeExtender.cpp b/src/storm-pars/analysis/LatticeExtender.cpp
index 921e66d42..fdb4471a8 100644
--- a/src/storm-pars/analysis/LatticeExtender.cpp
+++ b/src/storm-pars/analysis/LatticeExtender.cpp
@@ -30,7 +30,7 @@ namespace storm {
}
template <typename SparseModelType>
- storm::analysis::Lattice* LatticeExtender<SparseModelType>::toLattice(std::vector<std::shared_ptr<storm::logic::Formula const>> formulas) {
+ std::tuple<storm::analysis::Lattice*, uint_fast64_t, uint_fast64_t> LatticeExtender<SparseModelType>::toLattice(std::vector<std::shared_ptr<storm::logic::Formula const>> formulas) {
STORM_LOG_THROW((++formulas.begin()) == formulas.end(), storm::exceptions::NotSupportedException, "Only one formula allowed for monotonicity analysis");
STORM_LOG_THROW((*(formulas[0])).isProbabilityOperatorFormula()
&& ((*(formulas[0])).asProbabilityOperatorFormula().getSubformula().isUntilFormula()
@@ -77,14 +77,15 @@ namespace storm {
}
template <typename SparseModelType>
- storm::analysis::Lattice* LatticeExtender<SparseModelType>::extendLattice(storm::analysis::Lattice* lattice) {
+ std::tuple<storm::analysis::Lattice*, uint_fast64_t, uint_fast64_t> LatticeExtender<SparseModelType>::extendLattice(storm::analysis::Lattice* lattice) {
std::shared_ptr<storm::expressions::ExpressionManager> expressionManager(new storm::expressions::ExpressionManager());
std::set<storm::expressions::BinaryRelationExpression*> assumptions;
return this->extendLattice(lattice, expressionManager, assumptions);
}
template <typename SparseModelType>
- storm::analysis::Lattice* LatticeExtender<SparseModelType>::extendLattice(storm::analysis::Lattice* lattice, std::shared_ptr<storm::expressions::ExpressionManager> expressionManager, std::set<storm::expressions::BinaryRelationExpression*> assumptions) {
+ std::tuple<storm::analysis::Lattice*, uint_fast64_t, uint_fast64_t> LatticeExtender<SparseModelType>::extendLattice(storm::analysis::Lattice* lattice, std::shared_ptr<storm::expressions::ExpressionManager> expressionManager, std::set<storm::expressions::BinaryRelationExpression*> assumptions) {
+ auto numberOfStates = this->model->getNumberOfStates();
// First handle assumptions
for (auto itr = assumptions.begin(); itr != assumptions.end(); ++itr) {
storm::expressions::BinaryRelationExpression expr = *(*itr);
@@ -114,8 +115,6 @@ namespace storm {
// Create a copy of the states already present in the lattice.
storm::storage::BitVector seenStates = (lattice->getAddedStates());
-
- auto numberOfStates = this->model->getNumberOfStates();
storm::storage::BitVector oldStates(numberOfStates);
while (oldStates != seenStates) {
@@ -155,17 +154,15 @@ namespace storm {
// the successors are at the same level
lattice->addToNode(stateNumber, lattice->getNode(successor1));
} else {
- // TODO: create critical pair
+ return std::make_tuple(lattice, successor1, successor2);
}
seenStates.set(stateNumber);
}
}
}
- // TODO allow returning critical pair
- return lattice;
+ return std::make_tuple(lattice, numberOfStates, numberOfStates);
}
template class LatticeExtender<storm::models::sparse::Model<storm::RationalFunction>>;
-// template class LatticeExtender<storm::models::sparse::Mdp<storm::RationalFunction>>;
}
-}
\ No newline at end of file
+}
diff --git a/src/storm-pars/analysis/LatticeExtender.h b/src/storm-pars/analysis/LatticeExtender.h
index 37c39dc2a..9c854b4f5 100644
--- a/src/storm-pars/analysis/LatticeExtender.h
+++ b/src/storm-pars/analysis/LatticeExtender.h
@@ -23,16 +23,16 @@ namespace storm {
public:
LatticeExtender(std::shared_ptr<SparseModelType> model);
- storm::analysis::Lattice* toLattice(std::vector<std::shared_ptr<storm::logic::Formula const>> formulas);
+ std::tuple<storm::analysis::Lattice*, uint_fast64_t, uint_fast64_t> toLattice(std::vector<std::shared_ptr<storm::logic::Formula const>> formulas);
- storm::analysis::Lattice* extendLattice(storm::analysis::Lattice* lattice, std::shared_ptr<storm::expressions::ExpressionManager> expressionManager, std::set<storm::expressions::BinaryRelationExpression*> assumptions);
+ std::tuple<storm::analysis::Lattice*, uint_fast64_t, uint_fast64_t> extendLattice(storm::analysis::Lattice* lattice, std::shared_ptr<storm::expressions::ExpressionManager> expressionManager, std::set<storm::expressions::BinaryRelationExpression*> assumptions);
private:
std::shared_ptr<SparseModelType> model;
std::map<uint_fast64_t, storm::storage::BitVector> stateMap;
- storm::analysis::Lattice* extendLattice(storm::analysis::Lattice* lattice);
+ std::tuple<storm::analysis::Lattice*, uint_fast64_t, uint_fast64_t> extendLattice(storm::analysis::Lattice* lattice);
};
}