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

Implementaed methods for checking until formula by providing the left and right states instead of the whole formula (same with bounded Until) in the SparseDtmcPrctlModelChecker, analouge to the SparseMdpPrctlModelChecker. 

Reverted unnecessary changes to the AbstractModel checker.
Next on the list: Adapting the subsystem generation routine to the new method of providing the subsystem to the model checker.


Former-commit-id: 6c90c064a2
main
masawei 12 years ago
parent
0cb390b186
commit
4dca7abd3f
3 changed files with 50 additions and 52 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. 10
      src/counterexamples/PathBasedSubsystemGenerator.h
  2. 40
      src/modelchecker/prctl/AbstractModelChecker.h
  3. 52
      src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h

10
src/counterexamples/PathBasedSubsystemGenerator.h
View File

@ -64,7 +64,7 @@ public:
distances[*init].second = (T) 1;
}
typename storm::storage::SparseMatrix<T>::ConstRowsIterator trans = transMat.begin(*init);
typename storm::storage::SparseMatrix<T>::ConstRowIterator trans = transMat.begin(*init);
for(; trans != transMat.end(*init); ++trans) {
//save transition only if it's no 'virtual transition of prob 0 and it doesn't go from init state to init state.
if(trans.value() != (T) 0 && !subSysStates.get(trans.column())) {
@ -111,7 +111,7 @@ public:
// Same goes for forbidden states since they may not be used on a path, except as last node.
if(!subSysStates.get(activeState.first) && allowedStates.get(activeState.first)) {
// Look at all neighbors
for(typename storm::storage::SparseMatrix<T>::ConstRowsIterator trans = transMat.begin(activeState.first); trans != transMat.end(activeState.first); ++trans) {
for(typename storm::storage::SparseMatrix<T>::ConstRowIterator trans = transMat.begin(activeState.first); trans != transMat.end(activeState.first); ++trans) {
// Only consider the transition if it's not virtual
if(trans.value() != (T) 0) {
@ -178,7 +178,7 @@ public:
continue;
}
typename storm::storage::SparseMatrix<T>::ConstRowsIterator trans = transMat.begin(*init);
typename storm::storage::SparseMatrix<T>::ConstRowIterator trans = transMat.begin(*init);
for(; trans != transMat.end(*init); ++trans) {
//save transition only if it's no 'virtual transition of prob 0 and it doesn't go from init state to init state.
if(trans.value() != (T) 0 && !subSysStates.get(trans.column())) {
@ -230,7 +230,7 @@ public:
// Same goes for forbidden states since they may not be used on a path, except as last node.
if(!subSysStates.get(activeState.first) && allowedStates.get(activeState.first)) {
// Look at all neighbors
for(typename storm::storage::SparseMatrix<T>::ConstRowsIterator trans = transMat.begin(activeState.first); trans != transMat.end(activeState.first); ++trans) {
for(typename storm::storage::SparseMatrix<T>::ConstRowIterator trans = transMat.begin(activeState.first); trans != transMat.end(activeState.first); ++trans) {
// Only consider the transition if it's not virtual
if(trans.value() != (T) 0) {
@ -508,7 +508,7 @@ public:
/*!
*
*/
static void computeCriticalSubsystem(storm::modelchecker::prctl::AbstractModelChecker<T> const& modelCheck, storm::property::prctl::AbstractStateFormula<T> const& stateFormula) {
static void computeCriticalSubsystem(storm::modelchecker::prctl::AbstractModelChecker<T>& modelCheck, storm::property::prctl::AbstractStateFormula<T> const& stateFormula) {
//-------------------------------------------------------------
// 1. Strip and handle formulas

40
src/modelchecker/prctl/AbstractModelChecker.h
View File

@ -68,14 +68,14 @@ public:
/*!
* Constructs an AbstractModelChecker with the given model.
*/
explicit AbstractModelChecker(storm::models::AbstractModel<Type> const& model, storm::storage::BitVector* subSystem = nullptr) : model(model), subSystem(subSystem) {
explicit AbstractModelChecker(storm::models::AbstractModel<Type> const& model) : model(model){
// Intentionally left empty.
}
/*!
* Copy constructs an AbstractModelChecker from the given model checker. In particular, this means that the newly
* constructed model checker will have the model of the given model checker as its associated model.
*/
explicit AbstractModelChecker(AbstractModelChecker<Type> const& modelchecker) : model(modelchecker.model), subSystem(modelchecker.subSystem) {
explicit AbstractModelChecker(AbstractModelChecker<Type> const& modelchecker) : model(modelchecker.model) {
// Intentionally left empty.
}
@ -147,7 +147,6 @@ public:
LOG4CPLUS_INFO(logger, "Model checking formula\t" << stateFormula.toString());
std::cout << "Model checking formula:\t" << stateFormula.toString() << std::endl;
storm::storage::BitVector result;
bool allSatisfied = true;
try {
result = stateFormula.check(*this);
LOG4CPLUS_INFO(logger, "Result for initial states:");
@ -155,19 +154,12 @@ public:
for (auto initialState : model.getInitialStates()) {
LOG4CPLUS_INFO(logger, "\t" << initialState << ": " << (result.get(initialState) ? "satisfied" : "not satisfied"));
std::cout << "\t" << initialState << ": " << result.get(initialState) << std::endl;
allSatisfied &= result.get(initialState);
}
} catch (std::exception& e) {
std::cout << "Error during computation: " << e.what() << "Skipping property." << std::endl;
LOG4CPLUS_ERROR(logger, "Error during computation: " << e.what() << "Skipping property.");
}
if(!allSatisfied && storm::settings::Settings::getInstance()->getOptionByLongName("prctl").getArgumentByName("subSys").getValueAsBoolean()) {
//generate critical subsystem
storm::counterexamples::PathBasedSubsystemGenerator<Type>::computeCriticalSubsystem(*this, stateFormula);
}
std::cout << std::endl << "-------------------------------------------" << std::endl;
}
@ -205,11 +197,7 @@ public:
*/
storm::storage::BitVector checkAp(storm::property::prctl::Ap<Type> const& formula) const {
if (formula.getAp() == "true") {
if(subSystem != nullptr) {
return *subSystem;
} else {
return storm::storage::BitVector(model.getNumberOfStates(), true);
}
return storm::storage::BitVector(model.getNumberOfStates(), true);
} else if (formula.getAp() == "false") {
return storm::storage::BitVector(model.getNumberOfStates());
}
@ -219,11 +207,7 @@ public:
throw storm::exceptions::InvalidPropertyException() << "Atomic proposition '" << formula.getAp() << "' is invalid.";
}
if(subSystem != nullptr) {
return *subSystem & storm::storage::BitVector(model.getLabeledStates(formula.getAp()));
} else {
return storm::storage::BitVector(model.getLabeledStates(formula.getAp()));
}
return storm::storage::BitVector(model.getLabeledStates(formula.getAp()));
}
/*!
@ -313,15 +297,6 @@ public:
return result;
}
/*!
* Sets the subsystem.
*
* @param subSystem The subsystem the model check is to be confined to.
*/
void setSubSystem(storm::storage::BitVector* subSys) {
subSystem = subSys;
}
private:
/*!
@ -331,13 +306,6 @@ private:
* model checker object is unsafe after the object has been destroyed.
*/
storm::models::AbstractModel<Type> const& model;
/*!
* A pointer to the subsystem of the Model to which the check of the model is to be confined.
*
* @note that this is a nullptr iff the check is not to be confined.
*/
storm::storage::BitVector* subSystem;
};
} // namespace prctl

52
src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h
View File

@ -74,6 +74,7 @@ public:
return formula.check(*this, false);
}
/*!
* Checks the given formula that is a bounded-until formula.
*
@ -86,14 +87,29 @@ public:
* checker. If the qualitative flag is set, exact probabilities might not be computed.
*/
virtual std::vector<Type> checkBoundedUntil(storm::property::prctl::BoundedUntil<Type> const& formula, bool qualitative) const {
// First, we need to compute the states that satisfy the sub-formulas of the bounded until-formula.
storm::storage::BitVector leftStates = formula.getLeft().check(*this);
storm::storage::BitVector rightStates = formula.getRight().check(*this);
return this->checkBoundedUntil(formula.getLeft().check(*this), formula.getRight().check(*this), formula.getBound(), qualitative);
}
/*!
* Computes the probability to satisfy phi until psi inside a given bound for each state in the model.
*
* @param phiStates A bit vector indicating which states satisfy phi.
* @param psiStates A bit vector indicating which states satisfy psi.
* @param qualitative A flag indicating whether the formula only needs to be evaluated qualitatively, i.e. if the
* results are only compared against the bounds 0 and 1. If set to true, this will most likely results that are only
* qualitatively correct, i.e. do not represent the correct value, but only the correct relation with respect to the
* bounds 0 and 1.
* @returns The probabilities for the given formula to hold on every state of the model associated with this model
* checker. If the qualitative flag is set, exact probabilities might not be computed.
*/
virtual std::vector<Type> checkBoundedUntil(storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, uint_fast64_t stepBound, bool qualitative) const {
std::vector<Type> result(this->getModel().getNumberOfStates());
// If we identify the states that have probability 0 of reaching the target states, we can exclude them in the
// further analysis.
storm::storage::BitVector statesWithProbabilityGreater0 = storm::utility::graph::performProbGreater0(this->getModel(), leftStates, rightStates, true, formula.getBound());
storm::storage::BitVector statesWithProbabilityGreater0 = storm::utility::graph::performProbGreater0(this->getModel(), phiStates, psiStates, true, stepBound);
LOG4CPLUS_INFO(logger, "Found " << statesWithProbabilityGreater0.getNumberOfSetBits() << " 'maybe' states.");
// Check if we already know the result (i.e. probability 0) for all initial states and
@ -111,7 +127,7 @@ public:
storm::storage::SparseMatrix<Type> submatrix = this->getModel().getTransitionMatrix().getSubmatrix(statesWithProbabilityGreater0);
// Compute the new set of target states in the reduced system.
storm::storage::BitVector rightStatesInReducedSystem = statesWithProbabilityGreater0 % rightStates;
storm::storage::BitVector rightStatesInReducedSystem = statesWithProbabilityGreater0 % psiStates;
// Make all rows absorbing that satisfy the second sub-formula.
submatrix.makeRowsAbsorbing(rightStatesInReducedSystem);
@ -122,7 +138,7 @@ public:
// Perform the matrix vector multiplication as often as required by the formula bound.
if (linearEquationSolver != nullptr) {
this->linearEquationSolver->performMatrixVectorMultiplication(submatrix, subresult, nullptr, formula.getBound());
this->linearEquationSolver->performMatrixVectorMultiplication(submatrix, subresult, nullptr, stepBound);
} else {
throw storm::exceptions::InvalidStateException() << "No valid linear equation solver available.";
}
@ -219,6 +235,7 @@ public:
return result;
}
/*!
* Check the given formula that is an until formula.
*
@ -231,13 +248,26 @@ public:
* checker. If the qualitative flag is set, exact probabilities might not be computed.
*/
virtual std::vector<Type> checkUntil(storm::property::prctl::Until<Type> const& formula, bool qualitative) const {
// First, we need to compute the states that satisfy the sub-formulas of the until-formula.
storm::storage::BitVector leftStates = formula.getLeft().check(*this);
storm::storage::BitVector rightStates = formula.getRight().check(*this);
return this->checkUntil(formula.getLeft().check(*this), formula.getRight().check(*this), qualitative);
}
/*!
* Computes the probability to satisfy phi until psi for each state in the model.
*
* @param phiStates A bit vector indicating which states satisfy phi.
* @param psiStates A bit vector indicating which states satisfy psi.
* @param qualitative A flag indicating whether the formula only needs to be evaluated qualitatively, i.e. if the
* results are only compared against the bounds 0 and 1. If set to true, this will most likely results that are only
* qualitatively correct, i.e. do not represent the correct value, but only the correct relation with respect to the
* bounds 0 and 1.
* @returns The probabilities for the given formula to hold on every state of the model associated with this model
* checker. If the qualitative flag is set, exact probabilities might not be computed.
*/
virtual std::vector<Type> checkUntil(storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative) const {
// Then, we need to identify the states which have to be taken out of the matrix, i.e.
// We need to identify the states which have to be taken out of the matrix, i.e.
// all states that have probability 0 and 1 of satisfying the until-formula.
std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 = storm::utility::graph::performProb01(this->getModel(), leftStates, rightStates);
std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 = storm::utility::graph::performProb01(this->getModel(), phiStates, psiStates);
storm::storage::BitVector statesWithProbability0 = std::move(statesWithProbability01.first);
storm::storage::BitVector statesWithProbability1 = std::move(statesWithProbability01.second);

Write Preview
Loading…
Cancel
Save