diff --git a/src/storm-pars/analysis/Lattice.cpp b/src/storm-pars/analysis/Lattice.cpp index 8c0e04136..404ffe47e 100644 --- a/src/storm-pars/analysis/Lattice.cpp +++ b/src/storm-pars/analysis/Lattice.cpp @@ -38,6 +38,30 @@ namespace storm { } } + Lattice::Lattice(uint_fast64_t topState, uint_fast64_t bottomState, uint_fast64_t numberOfStates) { + nodes = std::vector(numberOfStates); + + this->numberOfStates = numberOfStates; + this->addedStates = new storm::storage::BitVector(numberOfStates); + this->doneBuilding = false; + + top = new Node(); + bottom = new Node(); + + top->statesAbove = storm::storage::BitVector(numberOfStates); + bottom->statesAbove = storm::storage::BitVector(numberOfStates); + + addedStates->set(topState); + bottom->statesAbove.set(topState); + top->states.insert(topState); + nodes[topState] = top; + + addedStates->set(bottomState); + bottom->states.insert(bottomState); + nodes[bottomState] = bottom; + assert (addedStates->getNumberOfSetBits() == 2); + } + Lattice::Lattice(Lattice* lattice) { numberOfStates = lattice->getAddedStates()->size(); nodes = std::vector(numberOfStates); @@ -90,6 +114,16 @@ namespace storm { addedStates->set(state); } + void Lattice::addBetween(uint_fast64_t state, uint_fast64_t above, uint_fast64_t below) { + assert(!(*addedStates)[state]); + assert(compare(above, below) == ABOVE); + + assert (getNode(below)->states.find(below) != getNode(below)->states.end()); + assert (getNode(above)->states.find(above) != getNode(above)->states.end()); + addBetween(state, getNode(above), getNode(below)); + + } + void Lattice::addToNode(uint_fast64_t state, Node *node) { assert(!(*addedStates)[state]); node->states.insert(state); @@ -111,6 +145,10 @@ namespace storm { assert (compare(above, below) == ABOVE); } + void Lattice::addRelation(uint_fast64_t above, uint_fast64_t below) { + addRelationNodes(getNode(above), getNode(below)); + } + Lattice::NodeComparison Lattice::compare(uint_fast64_t state1, uint_fast64_t state2) { return compare(getNode(state1), getNode(state2)); } @@ -147,6 +185,11 @@ namespace storm { return UNKNOWN; } + + bool Lattice::contains(uint_fast64_t state) { + return state >= 0 && state < addedStates->size() && addedStates->get(state); + } + Lattice::Node *Lattice::getNode(uint_fast64_t stateNumber) { return nodes.at(stateNumber); } diff --git a/src/storm-pars/analysis/Lattice.h b/src/storm-pars/analysis/Lattice.h index e0aef5acd..bdd25a5f2 100644 --- a/src/storm-pars/analysis/Lattice.h +++ b/src/storm-pars/analysis/Lattice.h @@ -40,6 +40,17 @@ namespace storm { storm::storage::BitVector* initialMiddleStates, uint_fast64_t numberOfStates); + /*! + * Constructs a lattice with the given top state and bottom state. + * + * @param top The top state of the resulting lattice. + * @param bottom The bottom state of the resulting lattice. + * @param numberOfStates Max number of states in endlattice. + */ + Lattice(uint_fast64_t top, + uint_fast64_t bottom, + uint_fast64_t numberOfStates); + /*! * Constructs a copy of the given lattice. * @@ -55,6 +66,15 @@ namespace storm { */ void addBetween(uint_fast64_t state, Node *node1, Node *node2); + /*! + * Adds a node with the given state between the nodes of below and above. + * Result: below -> state -> above + * @param state The given state. + * @param above The state number of the state below which a new node (with state) is added + * @param below The state number of the state above which a new node (with state) is added + */ + void addBetween(uint_fast64_t state, uint_fast64_t above, uint_fast64_t below); + /*! * Adds state to the states of the given node. * @param state The state which is added. @@ -75,6 +95,13 @@ namespace storm { */ void addRelationNodes(storm::analysis::Lattice::Node *above, storm::analysis::Lattice::Node * below); + /*! + * Adds a new relation between two states to the lattice + * @param above The state closest to the top Node of the Lattice. + * @param below The state closest to the bottom Node of the Lattice. + */ + void addRelation(uint_fast64_t above, uint_fast64_t below); + /*! * Compares the level of the nodes of the states. * Behaviour unknown when one or more of the states doesnot occur at any Node in the Lattice. @@ -87,6 +114,13 @@ namespace storm { */ Lattice::NodeComparison compare(uint_fast64_t state1, uint_fast64_t state2); + /*! + * Check if state is already in lattice + * @param state + * @return + */ + bool contains(uint_fast64_t state); + /*! * Retrieves the pointer to a Node at which the state occurs. * diff --git a/src/storm-pars/analysis/LatticeExtender.cpp b/src/storm-pars/analysis/LatticeExtender.cpp index dc0817a8b..f8cabe47a 100644 --- a/src/storm-pars/analysis/LatticeExtender.cpp +++ b/src/storm-pars/analysis/LatticeExtender.cpp @@ -33,7 +33,33 @@ namespace storm { template LatticeExtender::LatticeExtender(std::shared_ptr> model) { this->model = model; - assumptionSeen = false; + this->matrix = model->getTransitionMatrix(); + this->assumptionSeen = false; + uint_fast64_t numberOfStates = this->model->getNumberOfStates(); + + // Build stateMap + // TODO: is dit wel nodig + for (uint_fast64_t i = 0; i < numberOfStates; ++i) { + stateMap[i] = new 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); + } + } + } + + // Check if MC contains cycles + storm::storage::StronglyConnectedComponentDecompositionOptions const options; + this->sccs = storm::storage::StronglyConnectedComponentDecomposition(matrix, options); + acyclic = true; + for (auto i = 0; acyclic && i < sccs.size(); ++i) { + acyclic &= sccs.getBlock(i).size() <= 1; + } + statesSorted = storm::utility::graph::getTopologicalSort(matrix); + } template @@ -45,6 +71,7 @@ namespace storm { uint_fast64_t numberOfStates = this->model->getNumberOfStates(); + // TODO: dit moet anders kunnen storm::modelchecker::SparsePropositionalModelChecker> propositionalChecker(*model); storm::storage::BitVector phiStates; storm::storage::BitVector psiStates; @@ -56,6 +83,7 @@ namespace storm { psiStates = propositionalChecker.check((*(formulas[0])).asProbabilityOperatorFormula().getSubformula().asEventuallyFormula().getSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector(); } + // Get the maybeStates std::pair statesWithProbability01 = storm::utility::graph::performProb01(this->model->getBackwardTransitions(), phiStates, psiStates); storm::storage::BitVector topStates = statesWithProbability01.second; @@ -75,10 +103,13 @@ namespace storm { for (auto i = 0; acyclic && i < decomposition.size(); ++i) { acyclic &= decomposition.getBlock(i).size() <= 1; } + statesSorted = storm::utility::graph::getTopologicalSort(matrix); + + // Create the Lattice + Lattice *lattice = new Lattice(&topStates, &bottomStates, &initialMiddleStates, numberOfStates); + if (acyclic) { - statesSorted = storm::utility::graph::getTopologicalSort(matrix); } else { - statesSorted = storm::utility::graph::getTopologicalSort(matrix); for (uint_fast64_t i = 0; i < numberOfStates; ++i) { stateMap[i] = new storm::storage::BitVector(numberOfStates, false); @@ -91,6 +122,7 @@ namespace storm { } } for (auto i = 0; i < decomposition.size(); ++i) { + // TODO: alleen als er nog geen van in de lattice zit auto scc = decomposition.getBlock(i); if (scc.size() > 1) { auto states = scc.getStates(); @@ -103,6 +135,7 @@ namespace storm { auto intersection = bottomStates | topStates; if (intersection[succ1] || intersection[succ2]) { initialMiddleStates.set(state); + // ipv daaraan toevoegen, hem toevoegen aan de lattice die we eerder al gecreerd hebben break; } } @@ -110,15 +143,128 @@ namespace storm { } } } - statesToHandle = &initialMiddleStates; - // Create the Lattice - Lattice *lattice = new Lattice(&topStates, &bottomStates, &initialMiddleStates, numberOfStates); + return this->extendLattice(lattice); + } + + + template + std::tuple LatticeExtender::toLattice(std::vector> formulas, std::vector minValues, std::vector maxValues) { + uint_fast64_t numberOfStates = this->model->getNumberOfStates(); + + // Compare min/max for all states + 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() + || (*(formulas[0])).asProbabilityOperatorFormula().getSubformula().isEventuallyFormula()), storm::exceptions::NotSupportedException, "Expecting until or eventually formula"); + storm::modelchecker::SparsePropositionalModelChecker> propositionalChecker(*model); + storm::storage::BitVector phiStates; + storm::storage::BitVector psiStates; + if ((*(formulas[0])).asProbabilityOperatorFormula().getSubformula().isUntilFormula()) { + phiStates = propositionalChecker.check((*(formulas[0])).asProbabilityOperatorFormula().getSubformula().asUntilFormula().getLeftSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector(); + psiStates = propositionalChecker.check((*(formulas[0])).asProbabilityOperatorFormula().getSubformula().asUntilFormula().getRightSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector(); + } else { + phiStates = storm::storage::BitVector(numberOfStates, true); + psiStates = propositionalChecker.check((*(formulas[0])).asProbabilityOperatorFormula().getSubformula().asEventuallyFormula().getSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector(); + } + + // Get the maybeStates + std::pair statesWithProbability01 = storm::utility::graph::performProb01(this->model->getBackwardTransitions(), phiStates, psiStates); + storm::storage::BitVector topStates = statesWithProbability01.second; + storm::storage::BitVector bottomStates = statesWithProbability01.first; + + STORM_LOG_THROW(topStates.begin() != topStates.end(), storm::exceptions::NotImplementedException, "Formula yields to no 1 states"); + STORM_LOG_THROW(bottomStates.begin() != bottomStates.end(), storm::exceptions::NotImplementedException, "Formula yields to no zero states"); + + uint_fast64_t bottom = bottomStates.getNextSetIndex(0); + uint_fast64_t top = topStates.getNextSetIndex(0); + Lattice* lattice = new Lattice(top, bottom, numberOfStates); + + + for (auto state : statesSorted) { + if (state != bottom && state != top) { + assert (lattice != nullptr); + auto successors = stateMap[state]; + if (successors->size() > 1) { + uint_fast64_t min = numberOfStates; + uint_fast64_t max = numberOfStates; + bool allSorted = true; + + for (auto succ = successors->getNextSetIndex(0); + succ < numberOfStates; succ = successors->getNextSetIndex(succ + 1)) { + if (min == numberOfStates) { + assert (max == numberOfStates); + min = succ; + max = succ; + } else { + if (minValues[succ] > maxValues[max]) { + max = succ; + } else if (maxValues[succ] < minValues[min]) { + min = succ; + } else { + allSorted = false; + break; + } + } + } + + if (allSorted && min != max) { + if (lattice->contains(min) && lattice->contains(max)) { + assert (lattice->compare(min,max) == Lattice::UNKNOWN || lattice->compare(min,max) == Lattice::BELOW); + if (lattice->compare(min, max) == Lattice::UNKNOWN) { + lattice->addRelation(max, min); + } + } + if (!lattice->contains(min)) { + if (lattice->contains(max)) { + lattice->addBetween(min, lattice->getNode(max), lattice->getBottom()); + } else { + lattice->add(min); + } + } + if (!lattice->contains(max)) { + // Because of construction min is in the lattice + lattice->addBetween(max, lattice->getNode(min), lattice->getTop()); + } + assert (lattice->compare(max, min) == Lattice::ABOVE); + lattice->addBetween(state, max, min); + } + } + } + } + + // Handle sccs + auto addedStates = lattice->getAddedStates(); + for (auto scc : sccs) { + if (scc.size() > 1) { + auto states = scc.getStates(); + auto candidate = -1; + for (auto const& state : states) { + if (addedStates->get(state)) { + candidate = -1; + break; + // if there is a state of the scc already present in the lattice, there is no need to add one. + } + auto successors = stateMap[state]; + if (candidate == -1 && successors->getNumberOfSetBits() == 2) { + auto succ1 = successors->getNextSetIndex(0); + auto succ2 = successors->getNextSetIndex(succ1 + 1); + if (addedStates->get(succ1) || addedStates->get(succ2)) { + candidate = state; + } + } + } + if (candidate != -1) { + lattice->add(candidate); + } + } + } return this->extendLattice(lattice); } + template void LatticeExtender::handleAssumption(Lattice* lattice, std::shared_ptr assumption) { assert (assumption != nullptr); @@ -250,15 +396,15 @@ namespace storm { if (statesSorted.size() > 0) { auto nextState = *(statesSorted.begin()); - while ((*(lattice->getAddedStates()))[nextState] && statesSorted.size() > 1) { + while (lattice->contains(nextState) && statesSorted.size() > 1) { // states.size()>1 such that there is at least one state left after erase statesSorted.erase(statesSorted.begin()); nextState = *(statesSorted.begin()); } - if (!(*(lattice->getAddedStates()))[nextState]) { + if (!lattice->contains(nextState)) { auto row = this->model->getTransitionMatrix().getRow(nextState); - auto successors = new storm::storage::BitVector(lattice->getAddedStates()->size()); + auto successors = new storm::storage::BitVector(numberOfStates); for (auto rowItr = row.begin(); rowItr != row.end(); ++rowItr) { // ignore self-loops when there are more transitions if (nextState != rowItr->getColumn()) { @@ -278,22 +424,22 @@ namespace storm { } auto added = lattice->getAddedStates()->getNumberOfSetBits(); assert (lattice->getNode(nextState) != nullptr); - assert ((*lattice->getAddedStates())[nextState]); + assert (lattice->contains(nextState)); } } else if (assumptionSeen && acyclic) { auto states = statesSorted; if (states.size() > 0) { auto nextState = *(states.begin()); - while ((*(lattice->getAddedStates()))[nextState] && states.size() > 1) { + while (lattice->contains(nextState) && states.size() > 1) { // states.size()>1 such that there is at least one state left after erase states.erase(states.begin()); nextState = *(states.begin()); } - if (!(*(lattice->getAddedStates()))[nextState]) { + if (!lattice->contains(nextState)) { auto row = this->model->getTransitionMatrix().getRow(nextState); - auto successors = new storm::storage::BitVector(lattice->getAddedStates()->size()); + auto successors = new storm::storage::BitVector(numberOfStates); for (auto rowItr = row.begin(); rowItr != row.end(); ++rowItr) { // ignore self-loops when there are more transitions if (nextState != rowItr->getColumn()) { @@ -316,25 +462,23 @@ namespace storm { } } assert (lattice->getNode(nextState) != nullptr); - assert ((*lattice->getAddedStates())[nextState]); + assert (lattice->contains(nextState)); } } else if (!acyclic) { - auto addedStates = lattice->getAddedStates(); if (assumptionSeen) { - statesToHandle = addedStates; + statesToHandle = lattice->getAddedStates(); } auto stateNumber = statesToHandle->getNextSetIndex(0); while (stateNumber != numberOfStates) { - addedStates = lattice->getAddedStates(); storm::storage::BitVector* successors = stateMap[stateNumber]; // 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); - assert ((*addedStates)[stateNumber]); + assert (lattice->contains(stateNumber)); if (successors->getNumberOfSetBits() == 1) { - if (!(*addedStates)[succ1]) { + if (!lattice->contains(succ1)) { lattice->addToNode(succ1, lattice->getNode(stateNumber)); statesToHandle->set(succ1, true); auto itr = std::find(statesSorted.begin(), statesSorted.end(), succ1); @@ -345,10 +489,10 @@ namespace storm { statesToHandle->set(stateNumber, false); stateNumber = statesToHandle->getNextSetIndex(0); } else if (successors->getNumberOfSetBits() == 2 - && (((*(addedStates))[succ1] && !(*(addedStates))[succ2]) - || (!(*(addedStates))[succ1] && (*(addedStates))[succ2]))) { + && ((lattice->contains(succ1) && !lattice->contains(succ2)) + || (!lattice->contains(succ1) && lattice->contains(succ2)))) { - if (!(*(addedStates))[succ1]) { + if (!lattice->contains(succ1)) { std::swap(succ1, succ2); } @@ -377,8 +521,8 @@ namespace storm { stateNumber = statesToHandle->getNextSetIndex(0); } - } else if (!(((*(addedStates))[succ1] && !(*(addedStates))[succ2]) - || (!(*(addedStates))[succ1] && (*(addedStates))[succ2]))) { + } else if (!((lattice->contains(succ1) && !lattice->contains(succ2)) + || (!lattice->contains(succ1) && lattice->contains(succ2)))) { stateNumber = statesToHandle->getNextSetIndex(stateNumber + 1); } else { statesToHandle->set(stateNumber, false); @@ -393,7 +537,7 @@ namespace storm { stateNumber = numberOfStates; } while (stateNumber != numberOfStates - && (*(lattice->getAddedStates()))[stateNumber]) { + && lattice->contains(stateNumber)) { statesSorted.erase(statesSorted.begin()); if (statesSorted.size() > 0) { stateNumber = *(statesSorted.begin()); @@ -407,7 +551,7 @@ namespace storm { // Check if current state has not been added yet, and all successors have, ignore selfloop in this successors->set(stateNumber, false); - if ((*successors & *addedStates) == *successors) { + if ((*successors & *(lattice->getAddedStates())) == *successors) { auto result = extendAllSuccAdded(lattice, stateNumber, successors); if (std::get<1>(result) != successors->size()) { return result; @@ -416,15 +560,14 @@ namespace storm { } } } else { - addedStates = lattice->getAddedStates(); - auto notAddedStates = addedStates->operator~(); + auto notAddedStates = lattice->getAddedStates()->operator~(); for (auto stateNumber : notAddedStates) { // Iterate over all not yet added states storm::storage::BitVector* successors = stateMap[stateNumber]; // Check if current state has not been added yet, and all successors have, ignore selfloop in this successors->set(stateNumber, false); - if ((*successors & *addedStates) == *successors) { + if ((*successors & *(lattice->getAddedStates())) == *successors) { auto result = extendAllSuccAdded(lattice, stateNumber, successors); if (std::get<1>(result) != successors->size()) { return result; diff --git a/src/storm-pars/analysis/LatticeExtender.h b/src/storm-pars/analysis/LatticeExtender.h index 4899fdf46..42b743fa5 100644 --- a/src/storm-pars/analysis/LatticeExtender.h +++ b/src/storm-pars/analysis/LatticeExtender.h @@ -5,6 +5,10 @@ #include "storm/models/sparse/Dtmc.h" #include "storm-pars/analysis/Lattice.h" #include "storm/api/storm.h" +#include "storm-pars/storage/ParameterRegion.h" +#include "storm/storage/StronglyConnectedComponentDecomposition.h" +#include "storm/storage/StronglyConnectedComponent.h" + namespace storm { @@ -23,25 +27,36 @@ namespace storm { LatticeExtender(std::shared_ptr> model); /*! - * 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); /*! - * Creates a lattice based on the given formula. + * Creates a lattice based on the given extremal values. * - * @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 toLattice(std::vector> formulas); + std::tuple toLattice(std::vector> formulas, std::vector minValues, std::vector maxValues); + + + /*! + * Extends the lattice based on the given assumption. + * + * @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 extendLattice(storm::analysis::Lattice* lattice, std::shared_ptr assumption = nullptr); + private: std::shared_ptr> model; @@ -56,6 +71,10 @@ namespace storm { storm::storage::BitVector* statesToHandle; + storm::storage::StronglyConnectedComponentDecomposition sccs; + + storm::storage::SparseMatrix matrix; + void handleAssumption(Lattice* lattice, std::shared_ptr assumption); std::tuple extendAllSuccAdded(Lattice* lattice, uint_fast64_t const & stateNumber, storm::storage::BitVector* successors); diff --git a/src/storm-pars/analysis/MonotonicityChecker.cpp b/src/storm-pars/analysis/MonotonicityChecker.cpp index f451f7df7..8565d97d3 100644 --- a/src/storm-pars/analysis/MonotonicityChecker.cpp +++ b/src/storm-pars/analysis/MonotonicityChecker.cpp @@ -175,8 +175,31 @@ namespace storm { std::map>> MonotonicityChecker::createLattice() { // Transform to Lattices storm::utility::Stopwatch latticeWatch(true); - std::tuple criticalTuple = extender->toLattice(formulas); + // Use parameter lifting modelchecker to get initial min/max values for lattice creation + storm::modelchecker::SparseDtmcParameterLiftingModelChecker, double> plaModelChecker; + std::unique_ptr checkResult; + auto env = Environment(); + + auto formula = formulas[0]; + const storm::modelchecker::CheckTask checkTask + = storm::modelchecker::CheckTask(*formula); + STORM_LOG_THROW(plaModelChecker.canHandle(model, checkTask), storm::exceptions::NotSupportedException, + "Cannot handle this formula"); + plaModelChecker.specify(env, model, checkTask); + + std::unique_ptr minCheck = plaModelChecker.check(env, region,storm::solver::OptimizationDirection::Minimize); + std::unique_ptr maxCheck = plaModelChecker.check(env, region,storm::solver::OptimizationDirection::Maximize); + auto minRes = minCheck->asExplicitQuantitativeCheckResult(); + auto maxRes = maxCheck->asExplicitQuantitativeCheckResult(); + + std::vector minValues = minRes.getValueVector(); + std::vector maxValues = maxRes.getValueVector(); + // Create initial lattice + std::tuple criticalTuple = extender->toLattice(formulas, minValues, maxValues); + + + // Continue based on not (yet) sorted states std::map>> result; auto val1 = std::get<1>(criticalTuple); @@ -515,7 +538,6 @@ namespace storm { return result; } - template std::map::type, std::pair> MonotonicityChecker::checkOnSamples(std::shared_ptr> model, uint_fast64_t numberOfSamples) { storm::utility::Stopwatch samplesWatch(true); diff --git a/src/test/storm-pars/analysis/AssumptionCheckerTest.cpp b/src/test/storm-pars/analysis/AssumptionCheckerTest.cpp index 08e7319a6..bc331296d 100644 --- a/src/test/storm-pars/analysis/AssumptionCheckerTest.cpp +++ b/src/test/storm-pars/analysis/AssumptionCheckerTest.cpp @@ -331,7 +331,7 @@ TEST(AssumptionCheckerTest, Simple4) { below.set(4); storm::storage::BitVector initialMiddle(5); auto lattice = new storm::analysis::Lattice(&above, &below, &initialMiddle, 5); - + auto assumption = std::make_shared( storm::expressions::BinaryRelationExpression(*expressionManager, expressionManager->getBooleanType(), expressionManager->getVariable("1").getExpression().getBaseExpressionPointer(), diff --git a/src/test/storm-pars/analysis/MonotonicityCheckerTest.cpp b/src/test/storm-pars/analysis/MonotonicityCheckerTest.cpp index 4dfc2e38b..3f1afd50c 100644 --- a/src/test/storm-pars/analysis/MonotonicityCheckerTest.cpp +++ b/src/test/storm-pars/analysis/MonotonicityCheckerTest.cpp @@ -110,7 +110,7 @@ TEST(MonotonicityCheckerTest, Derivative_checker) { TEST(MonotonicityCheckerTest, Brp_with_bisimulation_no_samples) { std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp16_2.pm"; - std::string formulaAsString = "P=? [F s=4 & i=N ]"; + std::string formulaAsString = "P=? [true U s=4 & i=N ]"; std::string constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5 // Program and formula @@ -159,7 +159,7 @@ std::vector> regions = TEST(MonotonicityCheckerTest, Brp_with_bisimulation_samples) { std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp16_2.pm"; - std::string formulaAsString = "P=? [F s=4 & i=N ]"; + std::string formulaAsString = "P=? [true U s=4 & i=N ]"; std::string constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5 // Program and formula