From 8d95e71c3e20f052f3819bfc9acdffdb3d884592 Mon Sep 17 00:00:00 2001 From: Jip Spel Date: Tue, 29 Jan 2019 10:33:50 +0100 Subject: [PATCH] Change output, Fix some small bugs --- src/storm-pars-cli/storm-pars.cpp | 13 +- src/storm-pars/analysis/AssumptionChecker.cpp | 18 +- src/storm-pars/analysis/AssumptionMaker.cpp | 11 +- src/storm-pars/analysis/Lattice.cpp | 57 ++++-- src/storm-pars/analysis/Lattice.h | 7 + src/storm-pars/analysis/LatticeExtender.cpp | 177 +++++++++++------- src/storm-pars/analysis/LatticeExtender.h | 18 +- .../analysis/MonotonicityChecker.cpp | 159 ++++++++++------ .../analysis/AssumptionCheckerTest.cpp | 22 ++- .../analysis/AssumptionMakerTest.cpp | 14 +- src/test/storm-pars/analysis/LatticeTest.cpp | 34 ++++ 11 files changed, 368 insertions(+), 162 deletions(-) diff --git a/src/storm-pars-cli/storm-pars.cpp b/src/storm-pars-cli/storm-pars.cpp index 03a43e395..572562302 100644 --- a/src/storm-pars-cli/storm-pars.cpp +++ b/src/storm-pars-cli/storm-pars.cpp @@ -514,6 +514,11 @@ namespace storm { std::cout << "Hello, Jip1" << std::endl; // Simplify the model storm::utility::Stopwatch simplifyingWatch(true); + std::ofstream outfile; + outfile.open("results.txt", std::ios_base::app); + outfile << ioSettings.getPrismInputFilename() << ", "; + + if (model->isOfType(storm::models::ModelType::Dtmc)) { auto consideredModel = (model->as>()); auto simplifier = storm::transformer::SparseParametricDtmcSimplifier>(*consideredModel); @@ -543,6 +548,9 @@ namespace storm { simplifyingWatch.stop(); STORM_PRINT(std::endl << "Time for model simplification: " << simplifyingWatch << "." << std::endl << std::endl); model->printModelInformationToStream(std::cout); + outfile << simplifyingWatch << ", "; + outfile.close(); + std::cout << "Bye, Jip1" << std::endl; } @@ -562,8 +570,6 @@ namespace storm { // Monotonicity std::ofstream outfile; outfile.open("results.txt", std::ios_base::app); - outfile << std::endl << ioSettings.getPrismInputFilename() << "; "; - outfile.close(); storm::utility::Stopwatch monotonicityWatch(true); auto monotonicityChecker = storm::analysis::MonotonicityChecker(model, formulas, parSettings.isValidateAssumptionsSet()); monotonicityChecker.checkMonotonicity(); @@ -571,7 +577,10 @@ namespace storm { STORM_PRINT(std::endl << "Total time for monotonicity checking: " << monotonicityWatch << "." << std::endl << std::endl); + outfile << monotonicityWatch << std::endl; + outfile.close(); std::cout << "Bye, Jip2" << std::endl; + return; } diff --git a/src/storm-pars/analysis/AssumptionChecker.cpp b/src/storm-pars/analysis/AssumptionChecker.cpp index b454cf451..e27cd2610 100644 --- a/src/storm-pars/analysis/AssumptionChecker.cpp +++ b/src/storm-pars/analysis/AssumptionChecker.cpp @@ -34,7 +34,8 @@ namespace storm { auto valuation = storm::utility::parametric::Valuation(); for (auto itr = variables.begin(); itr != variables.end(); ++itr) { // TODO: Type - auto val = std::pair((*itr), storm::utility::convertNumber(boost::lexical_cast((i+1)/(double (numberOfSamples + 1))))); + // Creates samples between 0 and 1, 1/(#samples+2), 2/(#samples+2), ..., (#samples+1)/(#samples+2) + auto val = std::pair((*itr), storm::utility::convertNumber(boost::lexical_cast((i+1)/(double (numberOfSamples + 2))))); valuation.insert(val); } storm::models::sparse::Dtmc sampleModel = instantiator.instantiate(valuation); @@ -127,10 +128,12 @@ namespace storm { assumption->gatherVariables(vars); STORM_LOG_THROW(assumption->getRelationType() == - storm::expressions::BinaryRelationExpression::RelationType::GreaterOrEqual, + storm::expressions::BinaryRelationExpression::RelationType::Greater ||assumption->getRelationType() == + storm::expressions::BinaryRelationExpression::RelationType::Equal, storm::exceptions::NotSupportedException, "Only Greater Or Equal assumptions supported"); + // TODO: implement validation of equal/greater equations auto row1 = matrix.getRow(std::stoi(assumption->getFirstOperand()->asVariableExpression().getVariableName())); auto row2 = matrix.getRow(std::stoi(assumption->getSecondOperand()->asVariableExpression().getVariableName())); @@ -239,7 +242,9 @@ namespace storm { result = false; } } - return result && prob.evaluate(substitutions) >= 0; +// return result && prob.evaluate(substitutions) >= 0; +//TODO check for > and = + return false; } template @@ -296,7 +301,9 @@ namespace storm { s.add(exprBounds); smtResult = s.check(); - return smtResult == storm::solver::SmtSolver::CheckResult::Sat; +// return smtResult == storm::solver::SmtSolver::CheckResult::Sat; +//TODO check for > and = + return false; } template @@ -387,8 +394,9 @@ namespace storm { assert(s.check() == storm::solver::SmtSolver::CheckResult::Sat); s.add(exprToCheck); auto smtRes = s.check(); + //TODO check for > and = result = result && smtRes == storm::solver::SmtSolver::CheckResult::Sat; - return result; + return false; } template diff --git a/src/storm-pars/analysis/AssumptionMaker.cpp b/src/storm-pars/analysis/AssumptionMaker.cpp index ceb05ea72..0a5ab376e 100644 --- a/src/storm-pars/analysis/AssumptionMaker.cpp +++ b/src/storm-pars/analysis/AssumptionMaker.cpp @@ -27,17 +27,24 @@ namespace storm { std::shared_ptr assumption1 = std::make_shared(storm::expressions::BinaryRelationExpression(*expressionManager, expressionManager->getBooleanType(), var1.getExpression().getBaseExpressionPointer(), var2.getExpression().getBaseExpressionPointer(), - storm::expressions::BinaryRelationExpression::RelationType::GreaterOrEqual)); + storm::expressions::BinaryRelationExpression::RelationType::Greater)); bool result1 = (validate && assumptionChecker->validateAssumption(assumption1, lattice) && assumptionChecker->valid(assumption1)); result[assumption1] = result1; std::shared_ptr assumption2 = std::make_shared(storm::expressions::BinaryRelationExpression(*expressionManager, expressionManager->getBooleanType(), var2.getExpression().getBaseExpressionPointer(), var1.getExpression().getBaseExpressionPointer(), - storm::expressions::BinaryRelationExpression::RelationType::GreaterOrEqual)); + storm::expressions::BinaryRelationExpression::RelationType::Greater)); bool result2 = (validate && assumptionChecker->validateAssumption(assumption2, lattice) && assumptionChecker->valid(assumption2)); result[assumption2] = result2; + std::shared_ptr assumption3 + = std::make_shared(storm::expressions::BinaryRelationExpression(*expressionManager, expressionManager->getBooleanType(), + var2.getExpression().getBaseExpressionPointer(), var1.getExpression().getBaseExpressionPointer(), + storm::expressions::BinaryRelationExpression::RelationType::Equal)); + bool result3 = (validate && assumptionChecker->validateAssumption(assumption3, lattice) && assumptionChecker->valid(assumption3)); + result[assumption3] = result3; + return result; } diff --git a/src/storm-pars/analysis/Lattice.cpp b/src/storm-pars/analysis/Lattice.cpp index 9a1bacbc4..07bc5b01f 100644 --- a/src/storm-pars/analysis/Lattice.cpp +++ b/src/storm-pars/analysis/Lattice.cpp @@ -112,11 +112,11 @@ namespace storm { } addedStates.set(state); + } void Lattice::addToNode(uint_fast64_t state, Node *node) { assert(!addedStates[state]); - node->states.set(state); nodes.at(state) = node; addedStates.set(state); @@ -131,12 +131,13 @@ namespace storm { } void Lattice::add(uint_fast64_t state) { + assert(!addedStates[state]); addBetween(state, top, bottom); } void Lattice::addRelationNodes(Lattice::Node *above, Lattice::Node * below) { assert (compare(above, below) == UNKNOWN); - + assert ((above->statesAbove & below->statesBelow).getNumberOfSetBits() == 0); setStatesBelow(above, below->states | below->statesBelow, true); setStatesAbove(below, above->states | above->statesAbove, true); @@ -147,6 +148,7 @@ namespace storm { for (auto i = above->statesAbove.getNextSetIndex(0); i < above->statesAbove.size(); i = above->statesAbove.getNextSetIndex(i + 1)) { setStatesBelow(getNode(i), below->states | below->statesBelow, true); } + } int Lattice::compare(uint_fast64_t state1, uint_fast64_t state2) { @@ -314,16 +316,17 @@ namespace storm { } bool Lattice::above(Node *node1, Node *node2) { - return node1->statesBelow.get(node2->states.getNextSetIndex(0)); + return node1->statesBelow[node2->states.getNextSetIndex(0)]; } void Lattice::setStatesAbove(Lattice::Node *node, uint_fast64_t state, bool alreadyInitialized) { - assert (!node->states.get(state)); + assert (!node->states[state]); if (!alreadyInitialized) { node->statesAbove = storm::storage::BitVector(numberOfStates); } + assert (!node->statesBelow[state]); node->statesAbove.set(state); } @@ -333,32 +336,60 @@ namespace storm { if (!alreadyInitialized) { node->statesBelow = storm::storage::BitVector(numberOfStates); } - + assert (!node->statesAbove[state]); node->statesBelow.set(state); } void Lattice::setStatesAbove(Lattice::Node *node, storm::storage::BitVector states, bool alreadyInitialized) { assert((states.getNumberOfSetBits() - (node->states & states).getNumberOfSetBits()) != 0); + // the states to add to the above state of the current node shouldnt occur in either statesbelow or states of ndoe - auto complement = storm::storage::BitVector(node->states); - complement.complement(); + assert ((node->states & states).getNumberOfSetBits() ==0); if (alreadyInitialized) { - node->statesAbove |= (states & complement); + assert ((node->statesBelow & states).getNumberOfSetBits() == 0); + + node->statesAbove |= (states); } else { - node->statesAbove = (storm::storage::BitVector(states) & complement); + node->statesAbove = (storm::storage::BitVector(states)); } } void Lattice::setStatesBelow(Lattice::Node *node, storm::storage::BitVector states, bool alreadyInitialized) { assert((states.getNumberOfSetBits() - (node->states & states).getNumberOfSetBits()) != 0); - auto complement = storm::storage::BitVector(node->states); - complement.complement(); + assert ((node->states & states).getNumberOfSetBits() ==0); if (alreadyInitialized) { - node->statesBelow |= (states & complement); + assert ((node->statesAbove & states).getNumberOfSetBits() == 0); + node->statesBelow |= (states); } else { - node->statesBelow = (storm::storage::BitVector(states) & complement); + node->statesBelow = (storm::storage::BitVector(states)); } } + + void Lattice::mergeNodes(storm::analysis::Lattice::Node *node1, storm::analysis::Lattice::Node *node2) { + // Merges node2 into node 1 + // everything above n2 also above n1 + node1->statesAbove |= node2->statesAbove; + // everything below node 2 also below node 1 + node1->statesBelow |= node2->statesBelow; + + // add states of node 2 to node 1 + node1->states|= node2->states; + for(auto i = node2->states.getNextSetIndex(0); i < node2->states.size(); i = node2->states.getNextSetIndex(i+1)) { + nodes.at(i) = node1; + } + + // TODO hier gaat het op magische wijze nog fout + // Add all states of combined node to states Above of all states Below of node1 + for (auto i = node1->statesBelow.getNextSetIndex(0); i < node1->statesBelow.size(); i= node1->statesBelow.getNextSetIndex(i+1)) { + getNode(i)->statesAbove |= node1->states | node1->statesAbove; + } + + // Add all states of combined node to states Below of all states Above of node1 + for (auto i = node1->statesAbove.getNextSetIndex(0); i < node1->statesAbove.size(); i= node1->statesAbove.getNextSetIndex(i+1)) { + getNode(i)->statesBelow |= node1->states | node1->statesBelow; + } + + } } } diff --git a/src/storm-pars/analysis/Lattice.h b/src/storm-pars/analysis/Lattice.h index 4bf9a68ee..057ff9f30 100644 --- a/src/storm-pars/analysis/Lattice.h +++ b/src/storm-pars/analysis/Lattice.h @@ -165,6 +165,13 @@ namespace storm { */ void toDotFile(std::ostream &out); + /*! + * Merges node2 into node1 + * @param node1 + * @param node2 + */ + void mergeNodes(Node* node1, Node* node2); + /*! * Constants for comparison of nodes/states */ diff --git a/src/storm-pars/analysis/LatticeExtender.cpp b/src/storm-pars/analysis/LatticeExtender.cpp index dc80e3106..4917da795 100644 --- a/src/storm-pars/analysis/LatticeExtender.cpp +++ b/src/storm-pars/analysis/LatticeExtender.cpp @@ -4,6 +4,7 @@ #include "LatticeExtender.h" #include "storm/utility/macros.h" +#include "storm/utility/graph.h" #include "storm/storage/SparseMatrix.h" #include "storm/utility/graph.h" #include @@ -35,7 +36,7 @@ namespace storm { template std::tuple LatticeExtender::toLattice(std::vector> formulas) { - storm::utility::Stopwatch latticeWatch(true); +// storm::utility::Stopwatch latticeWatch(true); STORM_LOG_THROW((++formulas.begin()) == formulas.end(), storm::exceptions::NotSupportedException, "Only one formula allowed for monotonicity analysis"); STORM_LOG_THROW((*(formulas[0])).isProbabilityOperatorFormula() @@ -66,36 +67,43 @@ namespace storm { // Transform to Lattice auto matrix = this->model->getTransitionMatrix(); - for (uint_fast64_t i = 0; i < numberOfStates; ++i) { - stateMap[i] = storm::storage::BitVector(numberOfStates, false); - - auto row = matrix.getRow(i); - for (auto rowItr = row.begin(); rowItr != row.end(); ++rowItr) { - // ignore self-loops when there are more transitions - if (i != rowItr->getColumn() || row.getNumberOfEntries() == 1) { - stateMap[i].set(rowItr->getColumn(), true); - } - } - } - auto initialMiddleStates = storm::storage::BitVector(numberOfStates); // Check if MC contains cycles auto decomposition = storm::storage::StronglyConnectedComponentDecomposition(model->getTransitionMatrix(), false, false); - for (auto i = 0; i < decomposition.size(); ++i) { - auto scc = decomposition.getBlock(i); - if (scc.size() > 1) { - auto states = scc.getStates(); - // check if the state has already one successor in bottom of top, in that case pick it - bool found = false; - for (auto stateItr = states.begin(); !found && stateItr < states.end(); ++stateItr) { - auto successors = stateMap[*stateItr]; - if (successors.getNumberOfSetBits() == 2) { - auto succ1 = successors.getNextSetIndex(0); - auto succ2 = successors.getNextSetIndex(succ1 + 1); - auto intersection = bottomStates | topStates; - if (intersection[succ1] || intersection[succ2]) { - initialMiddleStates.set(*stateItr); - found = true; + acyclic = true; + for (auto i = 0; acyclic && i < decomposition.size(); ++i) { + acyclic &= decomposition.getBlock(i).size() <= 1; + } + if (acyclic) { + states = storm::utility::graph::getTopologicalSort(matrix); + } else { + for (uint_fast64_t i = 0; i < numberOfStates; ++i) { + stateMap[i] = storm::storage::BitVector(numberOfStates, false); + + auto row = matrix.getRow(i); + for (auto rowItr = row.begin(); rowItr != row.end(); ++rowItr) { + // ignore self-loops when there are more transitions + if (i != rowItr->getColumn() || row.getNumberOfEntries() == 1) { + stateMap[i].set(rowItr->getColumn(), true); + } + } + } + for (auto i = 0; i < decomposition.size(); ++i) { + auto scc = decomposition.getBlock(i); + if (scc.size() > 1) { + auto states = scc.getStates(); + // check if the state has already one successor in bottom of top, in that case pick it + bool found = false; + for (auto stateItr = states.begin(); !found && stateItr < states.end(); ++stateItr) { + auto successors = stateMap[*stateItr]; + if (successors.getNumberOfSetBits() == 2) { + auto succ1 = successors.getNextSetIndex(0); + auto succ2 = successors.getNextSetIndex(succ1 + 1); + auto intersection = bottomStates | topStates; + if (intersection[succ1] || intersection[succ2]) { + initialMiddleStates.set(*stateItr); + found = true; + } } } } @@ -105,8 +113,8 @@ namespace storm { // Create the Lattice Lattice *lattice = new Lattice(topStates, bottomStates, initialMiddleStates, numberOfStates); - latticeWatch.stop(); - STORM_PRINT(std::endl << "Time for initialization of lattice: " << latticeWatch << "." << std::endl << std::endl); +// latticeWatch.stop(); +// STORM_PRINT(std::endl << "Time for initialization of lattice: " << latticeWatch << "." << std::endl << std::endl); return this->extendLattice(lattice); } @@ -115,7 +123,7 @@ namespace storm { assert (assumption != nullptr); storm::expressions::BinaryRelationExpression expr = *assumption; - assert (expr.getRelationType() == storm::expressions::BinaryRelationExpression::RelationType::GreaterOrEqual + assert (expr.getRelationType() == storm::expressions::BinaryRelationExpression::RelationType::Greater || expr.getRelationType() == storm::expressions::BinaryRelationExpression::RelationType::Equal); if (expr.getRelationType() == storm::expressions::BinaryRelationExpression::RelationType::Equal) { @@ -131,8 +139,7 @@ namespace storm { Lattice::Node *n2 = lattice->getNode(val2); if (n1 != nullptr && n2 != nullptr) { - // TODO: mergeNode method - assert(false); + lattice->mergeNodes(n1,n2); } else if (n1 != nullptr) { lattice->addToNode(val2, n1); } else if (n2 != nullptr) { @@ -219,6 +226,8 @@ namespace storm { return std::make_tuple(lattice, numberOfStates, numberOfStates); } + + template std::tuple LatticeExtender::extendLattice(Lattice* lattice, std::shared_ptr assumption) { auto numberOfStates = this->model->getNumberOfStates(); @@ -230,57 +239,93 @@ namespace storm { auto oldNumberSet = numberOfStates; while (oldNumberSet != lattice->getAddedStates().getNumberOfSetBits()) { oldNumberSet = lattice->getAddedStates().getNumberOfSetBits(); - // TODO: kan dit niet efficienter - for (auto stateItr = stateMap.begin(); stateItr != stateMap.end(); ++stateItr) { - // Iterate over all states - auto stateNumber = stateItr->first; - storm::storage::BitVector successors = stateItr->second; - - auto seenStates = (lattice->getAddedStates()); - - // Check if current state has not been added yet, and all successors have - bool check = !seenStates[stateNumber]; - for (auto succIndex = successors.getNextSetIndex(0); check && succIndex != successors.size(); succIndex = successors.getNextSetIndex(++succIndex)) { - // if the stateNumber equals succIndex we have a self-loop, ignoring selfloop as seenStates[stateNumber] = false - if (succIndex != stateNumber) { - check &= seenStates[succIndex]; - } + + if (acyclic && states.size() > 0) { + auto nextState = *(states.begin()); + while (lattice->getAddedStates().get(nextState) && states.size() > 0) { + states.erase(states.begin()); + + nextState = *(states.begin()); } - if (check) { - auto result = extendAllSuccAdded(lattice, stateNumber, successors); + if (! lattice->getAddedStates().get(nextState)) { + auto row = this->model->getTransitionMatrix().getRow(nextState); + auto successors = storm::storage::BitVector(lattice->getAddedStates().size()); + for (auto rowItr = row.begin(); rowItr != row.end(); ++rowItr) { + // ignore self-loops when there are more transitions + if (nextState != rowItr->getColumn()) { + successors.set(rowItr->getColumn()); + } + } + auto seenStates = (lattice->getAddedStates()); + assert ((seenStates & successors) == successors); + + auto result = extendAllSuccAdded(lattice, nextState, successors); if (std::get<1>(result) != successors.size()) { return result; + } else { + states.erase(states.begin()); } } + assert (lattice->getNode(nextState) != nullptr); + + } else if (!acyclic) { + // TODO: kan dit niet efficienter + auto addedStates = lattice->getAddedStates(); + for (auto stateNumber = addedStates.getNextUnsetIndex(0); stateNumber < addedStates.size(); stateNumber = addedStates.getNextUnsetIndex(stateNumber+1)) { + // Iterate over all states +// auto stateNumber = i; + storm::storage::BitVector successors = stateMap[stateNumber]; + + auto seenStates = (lattice->getAddedStates()); + + assert(!acyclic); + // Check if current state has not been added yet, and all successors have + bool check = !seenStates[stateNumber]; + for (auto succIndex = successors.getNextSetIndex(0); + check && succIndex != successors.size(); succIndex = successors.getNextSetIndex( + ++succIndex)) { + // if the stateNumber equals succIndex we have a self-loop, ignoring selfloop as seenStates[stateNumber] = false + if (succIndex != stateNumber) { + check &= seenStates[succIndex]; + } + } - // Checking for states which are already added to the lattice, and only have one successor left which haven't been added yet - auto succ1 = successors.getNextSetIndex(0); - auto succ2 = successors.getNextSetIndex(succ1 + 1); + if (check) { + auto result = extendAllSuccAdded(lattice, stateNumber, successors); + if (std::get<1>(result) != successors.size()) { + return result; + } + } + + // Checking for states which are already added to the lattice, and only have one successor left which haven't been added yet + auto succ1 = successors.getNextSetIndex(0); + auto succ2 = successors.getNextSetIndex(succ1 + 1); - if (seenStates[stateNumber] && successors.getNumberOfSetBits() == 2 + if (seenStates[stateNumber] && successors.getNumberOfSetBits() == 2 && (seenStates[succ1] || seenStates[succ2]) && (!seenStates[succ1] || !seenStates[succ2])) { - if (!seenStates[succ1]) { - std::swap(succ1, succ2); - } + if (!seenStates[succ1]) { + std::swap(succ1, succ2); + std::swap(succ1, succ2); + } - auto compare = lattice->compare(stateNumber, succ1); - if (compare == Lattice::ABOVE) { - lattice->addBetween(succ2, lattice->getTop(), lattice->getNode(stateNumber)); - } else if (compare == Lattice::BELOW) { - lattice->addBetween(succ2, lattice->getNode(stateNumber), lattice->getBottom()); - } else { - // TODO: implement? - assert(false); + auto compare = lattice->compare(stateNumber, succ1); + if (compare == Lattice::ABOVE) { + lattice->addBetween(succ2, lattice->getTop(), lattice->getNode(stateNumber)); + } else if (compare == Lattice::BELOW) { + lattice->addBetween(succ2, lattice->getNode(stateNumber), lattice->getBottom()); + } else { + // TODO: implement? + assert(false); + } } } } } return std::make_tuple(lattice, numberOfStates, numberOfStates); } - template class LatticeExtender; } } diff --git a/src/storm-pars/analysis/LatticeExtender.h b/src/storm-pars/analysis/LatticeExtender.h index e4cd8b0c4..7ff23ba05 100644 --- a/src/storm-pars/analysis/LatticeExtender.h +++ b/src/storm-pars/analysis/LatticeExtender.h @@ -29,31 +29,35 @@ namespace storm { LatticeExtender(std::shared_ptr> model); /*! - * Creates a lattice based on the given formula. + * Extends the lattice based on the given assumption. * - * @param formulas The formulas based on which the lattice is created, only the first is used. + * @param lattice The lattice. + * @param assumption The assumption on states. * @return A triple with a pointer to the lattice and two states of which the current place in the lattice * is unknown but needed. When the states have as number the number of states, no states are * unplaced but needed. */ - std::tuple toLattice(std::vector> formulas); + std::tuple extendLattice(storm::analysis::Lattice* lattice, std::shared_ptr assumption = nullptr); /*! - * Extends the lattice based on the given assumption. + * Creates a lattice based on the given formula. * - * @param lattice The lattice. - * @param assumption The assumption on states. + * @param formulas The formulas based on which the lattice is created, only the first is used. * @return A triple with a pointer to the lattice and two states of which the current place in the lattice * is unknown but needed. When the states have as number the number of states, no states are * unplaced but needed. */ - std::tuple extendLattice(storm::analysis::Lattice* lattice, std::shared_ptr assumption = nullptr); + std::tuple toLattice(std::vector> formulas); private: std::shared_ptr> model; std::map stateMap; + std::vector states; + + bool acyclic; + void handleAssumption(Lattice* lattice, std::shared_ptr assumption); std::tuple extendAllSuccAdded(Lattice* lattice, uint_fast64_t stateNumber, storm::storage::BitVector successors); diff --git a/src/storm-pars/analysis/MonotonicityChecker.cpp b/src/storm-pars/analysis/MonotonicityChecker.cpp index 91d9b6929..9c2a90b1f 100644 --- a/src/storm-pars/analysis/MonotonicityChecker.cpp +++ b/src/storm-pars/analysis/MonotonicityChecker.cpp @@ -27,8 +27,6 @@ #include "storm/storage/expressions/RationalFunctionToExpression.h" - - namespace storm { namespace analysis { template @@ -41,7 +39,7 @@ namespace storm { if (model != nullptr) { std::shared_ptr> sparseModel = model->as>(); this->extender = new storm::analysis::LatticeExtender(sparseModel); - outfile << model->getNumberOfStates() << "; " << model->getNumberOfTransitions() << "; "; + outfile << model->getNumberOfStates() << ", " << model->getNumberOfTransitions() << ", "; } outfile.close(); totalWatch = storm::utility::Stopwatch(true); @@ -49,9 +47,11 @@ namespace storm { template std::map>> MonotonicityChecker::checkMonotonicity() { - totalWatch = storm::utility::Stopwatch(true); // TODO: check on samples or not? + totalWatch = storm::utility::Stopwatch(true); + auto latticeWatch = storm::utility::Stopwatch(true); auto map = createLattice(); + // STORM_PRINT(std::endl << "Time for creating lattice: " << latticeWatch << "." << std::endl << std::endl); std::shared_ptr> sparseModel = model->as>(); auto matrix = sparseModel->getTransitionMatrix(); return checkMonotonicity(map, matrix); @@ -101,10 +101,21 @@ namespace storm { bool assumptionsHold = true; for (auto itr = assumptions.begin(); assumptionsHold && itr != assumptions.end(); ++itr) { auto assumption = *itr; - assert (assumption->getRelationType() == storm::expressions::BinaryRelationExpression::RelationType::GreaterOrEqual); - auto state1 = std::stoi(assumption->getFirstOperand()->asVariableExpression().getVariableName()); - auto state2 = std::stoi(assumption->getSecondOperand()->asVariableExpression().getVariableName()); - assumptionsHold &= valuesLower[state1] >= valuesUpper[state2]; + if (assumption->getRelationType() == storm::expressions::BinaryRelationExpression::RelationType::Greater) { + auto state1 = std::stoi( + assumption->getFirstOperand()->asVariableExpression().getVariableName()); + auto state2 = std::stoi( + assumption->getSecondOperand()->asVariableExpression().getVariableName()); + assumptionsHold &= valuesLower[state1] >= valuesUpper[state2]; + } else if (assumption->getRelationType() == storm::expressions::BinaryRelationExpression::RelationType::Equal) { + auto state1 = std::stoi( + assumption->getFirstOperand()->asVariableExpression().getVariableName()); + auto state2 = std::stoi( + assumption->getSecondOperand()->asVariableExpression().getVariableName()); + assumptionsHold &= valuesLower[state1] == valuesUpper[state2]; + } else { + assert(false); + } } if (!assumptionsHold) { std::vector> newRegions; @@ -126,55 +137,67 @@ namespace storm { template std::map>> MonotonicityChecker::checkMonotonicity(std::map>> map, storm::storage::SparseMatrix matrix) { - storm::utility::Stopwatch finalCheckWatch(true); + storm::utility::Stopwatch monotonicityCheckWatch(true); std::map>> result; + outfile.open(filename, std::ios_base::app); if (map.size() == 0) { - outfile.open(filename, std::ios_base::app); - outfile << " | No assumptions, ? | ;"; - outfile.close(); - STORM_PRINT(std::endl << "Do not know about monotonicity" << std::endl); + // Nothing is known + outfile << " No assumptions; ?"; + // STORM_PRINT(std::endl << "Do not know about monotonicity" << std::endl); } else { auto i = 0; for (auto itr = map.begin(); i < map.size() && itr != map.end(); ++itr) { auto lattice = itr->first; - outfile.open(filename, std::ios_base::app); - outfile << "|"; - outfile.close(); + if (itr != map.begin()) { + outfile << ";"; + } std::map> varsMonotone = analyseMonotonicity(i, lattice, matrix); - outfile.open(filename, std::ios_base::app); auto assumptions = itr->second; bool validSomewhere = true; if (assumptions.size() > 0) { - auto regions = checkAssumptionsOnRegion(assumptions); - if (regions.size() > 0) { - STORM_PRINT("For regions: " << std::endl); - } - bool first = true; - for (auto itr2 = regions.begin(); itr2 != regions.end(); ++itr2) { - if (first) { - STORM_PRINT(" "); - first = false; +// auto regions = checkAssumptionsOnRegion(assumptions); +// if (regions.size() > 0) { +// // STORM_PRINT("For regions: " << std::endl); +// bool first = true; +// for (auto itr2 = regions.begin(); itr2 != regions.end(); ++itr2) { +// if (first) { +// // STORM_PRINT(" "); +// first = false; +// } +// // STORM_PRINT(*itr2); +// outfile << (*itr2); +// } +// // STORM_PRINT(std::endl); +// outfile << ", "; +// } else { + // STORM_PRINT("Assumption(s): "); + bool first = true; + for (auto itr2 = assumptions.begin(); itr2 != assumptions.end(); ++itr2) { + if (!first) { + // STORM_PRINT(" ^ "); + outfile << (" ^ "); + } else { + first = false; + } + // STORM_PRINT(*(*itr2)); + outfile << (*(*itr2)); } - STORM_PRINT(*itr2); - outfile << (*itr2); - } - if (regions.size() > 0) { - STORM_PRINT(std::endl); - outfile << ", "; - } + // STORM_PRINT(std::endl); + outfile << " - "; +// } } if (validSomewhere && assumptions.size() == 0) { - outfile << "No assumptions, "; + outfile << "No assumptions - "; } if (validSomewhere && varsMonotone.size() == 0) { - STORM_PRINT("Result is constant" << std::endl); + // STORM_PRINT("Result is constant" << std::endl); outfile << "No params"; } else if (validSomewhere) { auto itr2 = varsMonotone.begin(); @@ -182,45 +205,41 @@ namespace storm { if (resultCheckOnSamples.find(itr2->first) != resultCheckOnSamples.end() && (!resultCheckOnSamples[itr2->first].first && !resultCheckOnSamples[itr2->first].second)) { - STORM_PRINT(" - Not monotone in: " << itr2->first << std::endl); + // STORM_PRINT(" - Not monotone in: " << itr2->first << std::endl); outfile << "X " << itr2->first; } else { if (itr2->second.first && itr2->second.second) { - STORM_PRINT(" - Constant in" << itr2->first << std::endl); + // STORM_PRINT(" - Constant in" << itr2->first << std::endl); outfile << "C " << itr2->first; } else if (itr2->second.first) { - STORM_PRINT(" - Monotone increasing in: " << itr2->first << std::endl); + // STORM_PRINT(" - Monotone increasing in: " << itr2->first << std::endl); outfile << "I " << itr2->first; } else if (itr2->second.second) { - STORM_PRINT(" - Monotone decreasing in: " << itr2->first << std::endl); + // STORM_PRINT(" - Monotone decreasing in: " << itr2->first << std::endl); outfile << "D " << itr2->first; } else { - STORM_PRINT( - " - Do not know if monotone incr/decreasing in: " << itr2->first << std::endl); + // STORM_PRINT(" - Do not know if monotone incr/decreasing in: " << itr2->first << std::endl); outfile << "? " << itr2->first; } } ++itr2; if (itr2 != varsMonotone.end()) { - outfile << ", "; + outfile << " "; } } result.insert( std::pair>>( lattice, varsMonotone)); } - outfile << "| "; - outfile.close(); ++i; } } + outfile << ", "; - finalCheckWatch.stop(); - STORM_PRINT(std::endl << "Time for monotonicity check on lattice: " << finalCheckWatch << "." << std::endl << std::endl); - outfile.open(filename, std::ios_base::app); - totalWatch.stop(); - outfile << totalWatch << "; "; + monotonicityCheckWatch.stop(); + outfile << monotonicityCheckWatch << ", "; + // STORM_PRINT(std::endl << "Time for monotonicity check on lattice: " << monotonicityCheckWatch << "." << std::endl << std::endl); outfile.close(); return result; } @@ -259,8 +278,10 @@ namespace storm { assert(false); } latticeWatch.stop(); - STORM_PRINT(std::endl << "Total time for lattice creation: " << latticeWatch << "." << std::endl << std::endl); - outfile << latticeWatch << "; "; + // STORM_PRINT(std::endl << "Total time for lattice creation: " << latticeWatch << "." << std::endl << std::endl); + outfile.open(filename, std::ios_base::app); + outfile << latticeWatch << ", "; + outfile.close(); return result; } @@ -273,19 +294,27 @@ namespace storm { assert (val1 == val2); result.insert(std::pair>>(lattice, assumptions)); } else { - auto assumptionPair = assumptionMaker->createAndCheckAssumption(val1, val2, lattice); - assert (assumptionPair.size() == 2); - auto itr = assumptionPair.begin(); + + // TODO: should be triple + auto assumptionTriple = assumptionMaker->createAndCheckAssumption(val1, val2, lattice); + assert (assumptionTriple.size() == 3); + auto itr = assumptionTriple.begin(); auto assumption1 = *itr; ++itr; auto assumption2 = *itr; + ++itr; + auto assumption3 = *itr; if (!assumption1.second && !assumption2.second) { + // Both assumption cannot be validated, so we need to keep them both // TODO: hier niet verder gaan als je iets gevonden hebt? auto assumptionsCopy = std::vector>(assumptions); + auto assumptionsCopy2 = std::vector>(assumptions); auto latticeCopy = new storm::analysis::Lattice(lattice); + auto latticeCopy2 = new storm::analysis::Lattice(lattice); assumptions.push_back(assumption1.first); assumptionsCopy.push_back(assumption2.first); + assumptionsCopy2.push_back(assumption2.first); auto criticalTuple = extender->extendLattice(lattice, assumption1.first); if (somewhereMonotonicity(std::get<0>(criticalTuple))) { @@ -300,7 +329,16 @@ namespace storm { assumptionsCopy); result.insert(map.begin(), map.end()); } + // TODO verbeteren +// criticalTuple = extender->extendLattice(latticeCopy2, assumption3.first); +// if (somewhereMonotonicity(std::get<0>(criticalTuple))) { +// auto map = extendLatticeWithAssumptions(std::get<0>(criticalTuple), assumptionMaker, +// std::get<1>(criticalTuple), std::get<2>(criticalTuple), +// assumptionsCopy2); +// result.insert(map.begin(), map.end()); +// } } else if (assumption1.second && assumption2.second) { + //TODO Both assumptions hold --> should not happen if we change it to < instead of <= auto assumption = assumptionMaker->createEqualAssumption(val1, val2); if (!validate) { assumptions.push_back(assumption); @@ -312,6 +350,7 @@ namespace storm { } } else if (assumption1.second) { if (!validate) { + assert(false); assumptions.push_back(assumption1.first); } // if validate is true and both hold, then they must be valid, so no need to add to assumptions @@ -339,7 +378,7 @@ namespace storm { template std::map> MonotonicityChecker::analyseMonotonicity(uint_fast64_t j, storm::analysis::Lattice* lattice, storm::storage::SparseMatrix matrix) { - storm::utility::Stopwatch analyseWatch(true); +// storm::utility::Stopwatch analyseWatch(true); std::map> varsMonotone; @@ -413,9 +452,9 @@ namespace storm { } } - analyseWatch.stop(); - STORM_PRINT(std::endl << "Time to check monotonicity based on the lattice: " << analyseWatch << "." << std::endl << std::endl); - outfile << analyseWatch << "; "; +// analyseWatch.stop(); + // STORM_PRINT(std::endl << "Time to check monotonicity based on the lattice: " << analyseWatch << "." << std::endl << std::endl); +// outfile << analyseWatch << "; "; return varsMonotone; } @@ -609,7 +648,7 @@ namespace storm { } samplesWatch.stop(); - STORM_PRINT(std::endl << "Time to check monotonicity on samples: " << samplesWatch << "." << std::endl << std::endl); + // STORM_PRINT(std::endl << "Time to check monotonicity on samples: " << samplesWatch << "." << std::endl << std::endl); resultCheckOnSamples = result; return result; } @@ -680,7 +719,7 @@ namespace storm { } samplesWatch.stop(); - STORM_PRINT(std::endl << "Time to check monotonicity on samples: " << samplesWatch << "." << std::endl << std::endl); + // STORM_PRINT(std::endl << "Time to check monotonicity on samples: " << samplesWatch << "." << std::endl << std::endl); resultCheckOnSamples = result; return result; } diff --git a/src/test/storm-pars/analysis/AssumptionCheckerTest.cpp b/src/test/storm-pars/analysis/AssumptionCheckerTest.cpp index 3880a525f..b8ac1981e 100644 --- a/src/test/storm-pars/analysis/AssumptionCheckerTest.cpp +++ b/src/test/storm-pars/analysis/AssumptionCheckerTest.cpp @@ -62,6 +62,20 @@ TEST(AssumptionCheckerTest, Brp_no_bisimulation) { storm::expressions::BinaryRelationExpression::RelationType::GreaterOrEqual)); EXPECT_TRUE(checker.checkOnSamples(assumption)); + assumption = std::make_shared( + storm::expressions::BinaryRelationExpression(*expressionManager, expressionManager->getBooleanType(), + expressionManager->getVariable("7").getExpression().getBaseExpressionPointer(), + expressionManager->getVariable("5").getExpression().getBaseExpressionPointer(), + storm::expressions::BinaryRelationExpression::RelationType::Greater)); + EXPECT_TRUE(checker.checkOnSamples(assumption)); + + assumption = std::make_shared( + storm::expressions::BinaryRelationExpression(*expressionManager, expressionManager->getBooleanType(), + expressionManager->getVariable("7").getExpression().getBaseExpressionPointer(), + expressionManager->getVariable("5").getExpression().getBaseExpressionPointer(), + storm::expressions::BinaryRelationExpression::RelationType::Equal)); + EXPECT_FALSE(checker.checkOnSamples(assumption)); + storm::storage::BitVector above(8); above.set(0); storm::storage::BitVector below(8); @@ -79,17 +93,17 @@ TEST(AssumptionCheckerTest, Brp_no_bisimulation) { storm::expressions::BinaryRelationExpression(*expressionManager, expressionManager->getBooleanType(), expressionManager->getVariable("6").getExpression().getBaseExpressionPointer(), expressionManager->getVariable("8").getExpression().getBaseExpressionPointer(), - storm::expressions::BinaryRelationExpression::RelationType::GreaterOrEqual)); + storm::expressions::BinaryRelationExpression::RelationType::Greater)); above = storm::storage::BitVector(13); above.set(12); below = storm::storage::BitVector(13); below.set(9); initialMiddle = storm::storage::BitVector(13); dummyLattice = new storm::analysis::Lattice(above, below, initialMiddle, 13); - EXPECT_TRUE(checker.checkOnSamples(assumption)); - EXPECT_TRUE(checker.validateAssumption(assumption, dummyLattice)); + EXPECT_FALSE(checker.checkOnSamples(assumption)); + EXPECT_FALSE(checker.validateAssumption(assumption, dummyLattice)); EXPECT_TRUE(checker.validated(assumption)); - EXPECT_TRUE(checker.valid(assumption)); + EXPECT_FALSE(checker.valid(assumption)); } diff --git a/src/test/storm-pars/analysis/AssumptionMakerTest.cpp b/src/test/storm-pars/analysis/AssumptionMakerTest.cpp index f233d2563..af6f0213d 100644 --- a/src/test/storm-pars/analysis/AssumptionMakerTest.cpp +++ b/src/test/storm-pars/analysis/AssumptionMakerTest.cpp @@ -61,14 +61,14 @@ TEST(AssumptionMakerTest, Brp_without_bisimulation) { auto var1 = itr->first->getManager().getVariable("183"); auto var2 = itr->first->getManager().getVariable("186"); - EXPECT_EQ(2, result.size()); + EXPECT_EQ(3, result.size()); EXPECT_EQ(false, itr->second); EXPECT_EQ(true, itr->first->getFirstOperand()->isVariable()); EXPECT_EQ(true, itr->first->getSecondOperand()->isVariable()); EXPECT_EQ(var1, itr->first->getFirstOperand()->asVariableExpression().getVariable()); EXPECT_EQ(var2, itr->first->getSecondOperand()->asVariableExpression().getVariable()); - EXPECT_EQ(storm::expressions::BinaryRelationExpression::RelationType::GreaterOrEqual, itr->first->getRelationType()); + EXPECT_EQ(storm::expressions::BinaryRelationExpression::RelationType::Greater, itr->first->getRelationType()); ++itr; EXPECT_EQ(false, itr->second); @@ -76,6 +76,14 @@ TEST(AssumptionMakerTest, Brp_without_bisimulation) { EXPECT_EQ(true, itr->first->getSecondOperand()->isVariable()); EXPECT_EQ(var2, itr->first->getFirstOperand()->asVariableExpression().getVariable()); EXPECT_EQ(var1, itr->first->getSecondOperand()->asVariableExpression().getVariable()); - EXPECT_EQ(storm::expressions::BinaryRelationExpression::RelationType::GreaterOrEqual, itr->first->getRelationType()); + EXPECT_EQ(storm::expressions::BinaryRelationExpression::RelationType::Greater, itr->first->getRelationType()); + + ++itr; + EXPECT_EQ(false, itr->second); + EXPECT_EQ(true, itr->first->getFirstOperand()->isVariable()); + EXPECT_EQ(true, itr->first->getSecondOperand()->isVariable()); + EXPECT_EQ(var2, itr->first->getFirstOperand()->asVariableExpression().getVariable()); + EXPECT_EQ(var1, itr->first->getSecondOperand()->asVariableExpression().getVariable()); + EXPECT_EQ(storm::expressions::BinaryRelationExpression::RelationType::Equal, itr->first->getRelationType()); // TODO: createEqualsAssumption checken } diff --git a/src/test/storm-pars/analysis/LatticeTest.cpp b/src/test/storm-pars/analysis/LatticeTest.cpp index 5fba6eac4..ad65b98c7 100644 --- a/src/test/storm-pars/analysis/LatticeTest.cpp +++ b/src/test/storm-pars/analysis/LatticeTest.cpp @@ -139,3 +139,37 @@ TEST(LatticeTest, copy_lattice) { EXPECT_EQ(storm::analysis::Lattice::BELOW, latticeCopy.compare(6,5)); EXPECT_EQ(storm::analysis::Lattice::ABOVE, latticeCopy.compare(5,6)); } + +TEST(LatticeTest, merge_nodes) { + auto numberOfStates = 7; + auto above = storm::storage::BitVector(numberOfStates); + above.set(0); + auto below = storm::storage::BitVector(numberOfStates); + below.set(1); + auto initialMiddle = storm::storage::BitVector(numberOfStates); + + auto lattice = storm::analysis::Lattice(above, below, initialMiddle, numberOfStates); + lattice.add(2); + lattice.add(3); + lattice.addToNode(4, lattice.getNode(2)); + lattice.addBetween(5, lattice.getNode(0), lattice.getNode(3)); + lattice.addBetween(6, lattice.getNode(5), lattice.getNode(3)); + + lattice.mergeNodes(lattice.getNode(4), lattice.getNode(5)); + EXPECT_EQ(storm::analysis::Lattice::SAME, lattice.compare(2,4)); + EXPECT_EQ(storm::analysis::Lattice::SAME, lattice.compare(2,5)); + + EXPECT_EQ(storm::analysis::Lattice::ABOVE, lattice.compare(0,5)); + EXPECT_EQ(storm::analysis::Lattice::ABOVE, lattice.compare(0,2)); + EXPECT_EQ(storm::analysis::Lattice::ABOVE, lattice.compare(0,4)); + + EXPECT_EQ(storm::analysis::Lattice::BELOW, lattice.compare(6,2)); + EXPECT_EQ(storm::analysis::Lattice::BELOW, lattice.compare(6,4)); + EXPECT_EQ(storm::analysis::Lattice::BELOW, lattice.compare(6,5)); + EXPECT_EQ(storm::analysis::Lattice::BELOW, lattice.compare(3,2)); + EXPECT_EQ(storm::analysis::Lattice::BELOW, lattice.compare(3,4)); + EXPECT_EQ(storm::analysis::Lattice::BELOW, lattice.compare(3,5)); + EXPECT_EQ(storm::analysis::Lattice::BELOW, lattice.compare(1,2)); + EXPECT_EQ(storm::analysis::Lattice::BELOW, lattice.compare(1,4)); + EXPECT_EQ(storm::analysis::Lattice::BELOW, lattice.compare(1,5)); +}