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

Merge branch 'future' into python_api 

Former-commit-id: fc48889e60
main
sjunges 10 years ago
parent
0730d8bcd3 64e7cd63f5
commit
ef256993b9
2 changed files with 0 additions and 120 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. 61
      src/modelchecker/reachability/MenuGameMdpModelChecker.cpp
  2. 59
      src/modelchecker/reachability/MenuGameMdpModelChecker.h

61
src/modelchecker/reachability/MenuGameMdpModelChecker.cpp
View File

@ -1,61 +0,0 @@
#include "src/modelchecker/reachability/MenuGameMdpModelChecker.h"
#include "src/utility/macros.h"
#include "src/exceptions/NotSupportedException.h"
#include "src/modelchecker/results/CheckResult.h"
namespace storm {
namespace modelchecker {
MenuGameMdpModelChecker::MenuGameMdpModelChecker(storm::prism::Program const& program, std::unique_ptr<storm::utility::solver::SmtSolverFactory>&& smtSolverFactory) : originalProgram(program), smtSolverFactory(std::move(smtSolverFactory)) {
STORM_LOG_THROW(program.getModelType() == storm::prism::Program::ModelType::MDP, storm::exceptions::NotSupportedException, "Currently only MDPs are supported by the game-based model checker.");
// Start by preparing the program. That is, we flatten the modules if there is more than one.
if (originalProgram.getNumberOfModules() > 1) {
preprocessedProgram = originalProgram.flattenModules(smtSolverFactory);
} else {
preprocessedProgram = originalProgram;
}
}
bool MenuGameMdpModelChecker::canHandle(storm::logic::Formula const& formula) const {
if (formula.isProbabilityOperatorFormula()) {
storm::logic::ProbabilityOperatorFormula const& probabilityOperatorFormula = formula.asProbabilityOperatorFormula();
return this->canHandle(probabilityOperatorFormula.getSubformula());
} else if (formula.isUntilFormula() || formula.isEventuallyFormula()) {
if (formula.isUntilFormula()) {
storm::logic::UntilFormula const& untilFormula = formula.asUntilFormula();
if (untilFormula.getLeftSubformula().isPropositionalFormula() && untilFormula.getRightSubformula().isPropositionalFormula()) {
return true;
}
} else if (formula.isEventuallyFormula()) {
storm::logic::EventuallyFormula const& eventuallyFormula = formula.asEventuallyFormula();
if (eventuallyFormula.getSubformula().isPropositionalFormula()) {
return true;
}
}
}
return false;
}
std::unique_ptr<CheckResult> MenuGameMdpModelChecker::checkProbabilityOperatorFormula(storm::logic::ProbabilityOperatorFormula const& stateFormula) {
// Depending on whether or not there is a bound, we do something slightly different here.
return nullptr;
}
std::unique_ptr<CheckResult> computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative, boost::optional<OptimizationDirection> const& optimalityType) {
// TODO
return nullptr;
}
std::unique_ptr<CheckResult> computeEventuallyProbabilities(storm::logic::EventuallyFormula const& pathFormula, bool qualitative, boost::optional<OptimizationDirection> const& optimalityType) {
// TODO
return nullptr;
}
}
}

59
src/modelchecker/reachability/MenuGameMdpModelChecker.h
View File

@ -1,59 +0,0 @@
#ifndef STORM_MODELCHECKER_MENUGAMEMDPMODELCHECKER_H_
#define STORM_MODELCHECKER_MENUGAMEMDPMODELCHECKER_H_
#include "src/modelchecker/AbstractModelChecker.h"
#include "src/storage/prism/Program.h"
#include "src/utility/solver.h"
namespace storm {
namespace modelchecker {
class MenuGameMdpModelChecker : public AbstractModelChecker {
public:
/*!
* Constructs a model checker whose underlying model is implicitly given by the provided program. All
* verification calls will be answererd with respect to this model.
*
* @param program The program that implicitly specifies the model to check.
* @param smtSolverFactory A factory used to create SMT solver when necessary.
*/
explicit MenuGameMdpModelChecker(storm::prism::Program const& program, std::unique_ptr<storm::utility::solver::SmtSolverFactory>&& smtSolverFactory);
virtual bool canHandle(storm::logic::Formula const& formula) const override;
virtual std::unique_ptr<CheckResult> checkProbabilityOperatorFormula(storm::logic::ProbabilityOperatorFormula const& stateFormula) override;
virtual std::unique_ptr<CheckResult> computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative = false, boost::optional<OptimizationDirection> const& optimalityType = boost::optional<OptimizationDirection>()) override;
virtual std::unique_ptr<CheckResult> computeEventuallyProbabilities(storm::logic::EventuallyFormula const& pathFormula, bool qualitative = false, boost::optional<OptimizationDirection> const& optimalityType = boost::optional<OptimizationDirection>()) override;
private:
/*!
* Performs game-based abstraction refinement on the model until either the precision is met or the provided
* proof goal was successfully proven.
*
* @param filterPredicate A predicate that needs to hold until the target predicate holds.
* @param targetPredicate A predicate characterizing the target states.
* @param precision The precision to use. This governs what difference between lower and upper bounds is
* acceptable.
* @param proofGoal A proof goal that says the probability must only be established to be above/below a given
* threshold. If the proof goal is met before the precision is achieved, the refinement procedure will abort
* and return the current result.
* @return A pair of values, that are under- and over-approximations of the actual probability, respectively.
*/
std::pair<double, double> performGameBasedRefinement(storm::expressions::Expression const& filterPredicate, storm::expressions::Expression const& targetPredicate, double precision, boost::optional<std::pair<double, storm::logic::ComparisonType>> const& proofGoal);
// The original program that was used to create this model checker.
storm::prism::Program originalProgram;
// The preprocessed program that contains only one module and otherwhise corresponds to the semantics of the
// original program.
storm::prism::Program preprocessedProgram;
// A factory that is used for creating SMT solvers when needed.
std::unique_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory;
};
}
}
#endif /* STORM_MODELCHECKER_MENUGAMEMDPMODELCHECKER_H_ */
Write Preview
Loading…
Cancel
Save