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

Fixed a lot of tests, improved some things here and there. 

Former-commit-id: baec0a4963
tempestpy_adaptions
dehnert 10 years ago
parent
d0917f033c
commit
b60c5ffdc0
23 changed files with 406 additions and 357 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. 17
      src/builder/ExplicitPrismModelBuilder.cpp
  2. 87
      src/counterexamples/MILPMinimalLabelSetGenerator.h
  3. 85
      src/counterexamples/SMTMinimalCommandSetGenerator.h
  4. 12
      src/logic/BinaryBooleanStateFormula.cpp
  5. 5
      src/logic/BinaryBooleanStateFormula.h
  6. 8
      src/logic/UnaryBooleanStateFormula.cpp
  7. 4
      src/logic/UnaryBooleanStateFormula.h
  8. 23
      src/modelchecker/AbstractModelChecker.cpp
  9. 5
      src/modelchecker/CheckResult.h
  10. 22
      src/modelchecker/ExplicitQualitativeCheckResult.cpp
  11. 4
      src/modelchecker/ExplicitQualitativeCheckResult.h
  12. 18
      src/modelchecker/ExplicitQuantitativeCheckResult.cpp
  13. 2
      src/modelchecker/ExplicitQuantitativeCheckResult.h
  14. 4
      src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp
  15. 1
      src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp
  16. 1
      src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp
  17. 72
      src/settings/modules/GeneralSettings.cpp
  18. 88
      src/settings/modules/GeneralSettings.h
  19. 10
      src/storage/prism/Program.cpp
  20. 7
      src/storage/prism/Program.h
  21. 43
      src/utility/cli.h
  22. 80
      test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp
  23. 165
      test/performance/modelchecker/SparseMdpPrctlModelCheckerTest.cpp

17
src/builder/ExplicitPrismModelBuilder.cpp
View File

@ -61,7 +61,22 @@ namespace storm {
std::map<storm::expressions::Variable, storm::expressions::Expression> constantDefinitions = storm::utility::prism::parseConstantDefinitionString(program, constantDefinitionString);
storm::prism::Program preparedProgram = program.defineUndefinedConstants(constantDefinitions);
STORM_LOG_THROW(!preparedProgram.hasUndefinedConstants(), storm::exceptions::InvalidArgumentException, "Program still contains undefined constants.");
if (preparedProgram.hasUndefinedConstants()) {
std::vector<std::reference_wrapper<storm::prism::Constant const>> undefinedConstants = preparedProgram.getUndefinedConstants();
std::stringstream stream;
bool printComma = false;
for (auto const& constant : undefinedConstants) {
if (printComma) {
stream << ", ";
} else {
printComma = true;
}
stream << constant.get().getName() << " (" << constant.get().getType() << ")";
}
stream << ".";
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Program still contains these undefined constants: " + stream.str());
}
// Now that we have defined all the constants in the program, we need to substitute their appearances in
// all expressions in the program so we can then evaluate them without having to store the values of the

87
src/counterexamples/MILPMinimalLabelSetGenerator.h
View File

@ -1,19 +1,16 @@
/*
* MILPMinimalLabelSetGenerator.h
*
* Created on: 15.09.2013
* Author: Christian Dehnert
*/
#ifndef STORM_COUNTEREXAMPLES_MILPMINIMALLABELSETGENERATOR_MDP_H_
#define STORM_COUNTEREXAMPLES_MILPMINIMALLABELSETGENERATOR_MDP_H_
#include <chrono>
#include "src/models/Mdp.h"
#include "src/logic/Formulas.h"
#include "src/storage/prism/Program.h"
#include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h"
#include "src/modelchecker/ExplicitQualitativeCheckResult.h"
#include "src/modelchecker/ExplicitQuantitativeCheckResult.h"
#include "src/exceptions/NotImplementedException.h"
#include "src/exceptions/InvalidPropertyException.h"
#include "src/exceptions/InvalidArgumentException.h"
#include "src/exceptions/InvalidStateException.h"
@ -922,7 +919,7 @@ namespace storm {
public:
static boost::container::flat_set<uint_fast64_t> getMinimalLabelSet(storm::models::Mdp<T> const& labeledMdp, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, double probabilityThreshold, bool strictBound, bool checkThresholdFeasible = false, bool includeSchedulerCuts = false) {
static boost::container::flat_set<uint_fast64_t> getMinimalLabelSet(storm::logic::Formula const& pathFormula, storm::models::Mdp<T> const& labeledMdp, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, double probabilityThreshold, bool strictBound, bool checkThresholdFeasible = false, bool includeSchedulerCuts = false) {
// (0) Check whether the MDP is indeed labeled.
if (!labeledMdp.hasChoiceLabeling()) {
throw storm::exceptions::InvalidArgumentException() << "Minimal label set generation is impossible for unlabeled model.";
@ -931,14 +928,13 @@ namespace storm {
// (1) Check whether its possible to exceed the threshold if checkThresholdFeasible is set.
double maximalReachabilityProbability = 0;
if (checkThresholdFeasible) {
storm::modelchecker::prctl::SparseMdpPrctlModelChecker<T> modelchecker(labeledMdp);
std::vector<T> result = modelchecker.checkUntil(false, phiStates, psiStates, false).first;
storm::modelchecker::SparseMdpPrctlModelChecker<T> modelchecker(labeledMdp);
std::unique_ptr<storm::modelchecker::CheckResult> result = modelchecker.check(pathFormula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> const& quantitativeResult = result->asExplicitQuantitativeCheckResult<double>();
for (auto state : labeledMdp.getInitialStates()) {
maximalReachabilityProbability = std::max(maximalReachabilityProbability, result[state]);
}
if ((strictBound && maximalReachabilityProbability < probabilityThreshold) || (!strictBound && maximalReachabilityProbability <= probabilityThreshold)) {
throw storm::exceptions::InvalidArgumentException() << "Given probability threshold " << probabilityThreshold << " can not be " << (strictBound ? "achieved" : "exceeded") << " in model with maximal reachability probability of " << maximalReachabilityProbability << ".";
maximalReachabilityProbability = std::max(maximalReachabilityProbability, quantitativeResult[state]);
}
STORM_LOG_THROW((strictBound && maximalReachabilityProbability >= probabilityThreshold) || (!strictBound && maximalReachabilityProbability > probabilityThreshold), storm::exceptions::InvalidArgumentException, "Given probability threshold " << probabilityThreshold << " can not be " << (strictBound ? "achieved" : "exceeded") << " in model with maximal reachability probability of " << maximalReachabilityProbability << ".");
std::cout << std::endl << "Maximal reachability in model is " << maximalReachabilityProbability << "." << std::endl << std::endl;
}
@ -978,49 +974,48 @@ namespace storm {
* @param formulaPtr A pointer to a safety formula. The outermost operator must be a probabilistic bound operator with a strict upper bound. The nested
* formula can be either an unbounded until formula or an eventually formula.
*/
static void computeCounterexample(storm::prism::Program const& program, storm::models::Mdp<T> const& labeledMdp, std::shared_ptr<storm::properties::prctl::AbstractPrctlFormula<double>> const& formula) {
std::cout << std::endl << "Generating minimal label counterexample for formula " << formula->toString() << std::endl;
// First, we need to check whether the current formula is an Until-Formula.
std::shared_ptr<storm::properties::prctl::ProbabilisticBoundOperator<double>> probBoundFormula = std::dynamic_pointer_cast<storm::properties::prctl::ProbabilisticBoundOperator<double>>(formula);
if (probBoundFormula.get() == nullptr) {
LOG4CPLUS_ERROR(logger, "Illegal formula " << probBoundFormula->toString() << " for counterexample generation.");
throw storm::exceptions::InvalidPropertyException() << "Illegal formula " << probBoundFormula->toString() << " for counterexample generation.";
}
static void computeCounterexample(storm::prism::Program const& program, storm::models::Mdp<T> const& labeledMdp, std::shared_ptr<storm::logic::Formula> const& formula) {
std::cout << std::endl << "Generating minimal label counterexample for formula " << *formula << std::endl;
// Check whether we were given an upper bound, because counterexample generation is limited to this case.
if (probBoundFormula->getComparisonOperator() != storm::properties::ComparisonType::LESS && probBoundFormula->getComparisonOperator() != storm::properties::ComparisonType::LESS_EQUAL) {
LOG4CPLUS_ERROR(logger, "Illegal comparison operator in formula " << probBoundFormula->toString() << ". Only upper bounds are supported for counterexample generation.");
throw storm::exceptions::InvalidPropertyException() << "Illegal comparison operator in formula " << probBoundFormula->toString() << ". Only upper bounds are supported for counterexample generation.";
}
bool strictBound = probBoundFormula->getComparisonOperator() == storm::properties::ComparisonType::LESS;
STORM_LOG_THROW(formula->isProbabilityOperatorFormula(), storm::exceptions::InvalidPropertyException, "Counterexample generation does not support this kind of formula. Expecting a probability operator as the outermost formula element.");
storm::logic::ProbabilityOperatorFormula const& probabilityOperator = formula->asProbabilityOperatorFormula();
STORM_LOG_THROW(probabilityOperator.hasBound(), storm::exceptions::InvalidPropertyException, "Counterexample generation only supports bounded formulas.");
storm::logic::ComparisonType comparisonType = probabilityOperator.getComparisonType();
STORM_LOG_THROW(comparisonType == storm::logic::ComparisonType::Less || comparisonType == storm::logic::ComparisonType::LessEqual, storm::exceptions::InvalidPropertyException, "Counterexample generation only supports formulas with an upper probability bound.");
STORM_LOG_THROW(probabilityOperator.getSubformula().isUntilFormula() || probabilityOperator.getSubformula().isEventuallyFormula(), storm::exceptions::InvalidPropertyException, "Path formula is required to be of the form 'phi U psi' for counterexample generation.");
bool strictBound = comparisonType == storm::logic::ComparisonType::Less;
double bound = probabilityOperator.getBound();
// Now derive the probability threshold we need to exceed as well as the phi and psi states. Simultaneously, check whether the formula is of a valid shape.
double bound = probBoundFormula->getBound();
std::shared_ptr<storm::properties::prctl::AbstractPathFormula<double>> pathFormula = probBoundFormula->getChild();
storm::storage::BitVector phiStates;
storm::storage::BitVector psiStates;
storm::modelchecker::prctl::SparseMdpPrctlModelChecker<T> modelchecker(labeledMdp);
storm::modelchecker::SparseMdpPrctlModelChecker<T> modelchecker(labeledMdp);
std::shared_ptr<storm::properties::prctl::Until<double>> untilFormula = std::dynamic_pointer_cast<storm::properties::prctl::Until<double>>(pathFormula);
if(untilFormula.get() != nullptr) {
phiStates = untilFormula->getLeft()->check(modelchecker);
psiStates = untilFormula->getRight()->check(modelchecker);
if (probabilityOperator.getSubformula().isUntilFormula()) {
storm::logic::UntilFormula const& untilFormula = probabilityOperator.getSubformula().asUntilFormula();
} if (std::dynamic_pointer_cast<storm::properties::prctl::Eventually<double>>(pathFormula).get() != nullptr) {
// If the nested formula was not an until formula, it remains to check whether it's an eventually formula.
std::shared_ptr<storm::properties::prctl::Eventually<double>> eventuallyFormula = std::dynamic_pointer_cast<storm::properties::prctl::Eventually<double>>(pathFormula);
std::unique_ptr<storm::modelchecker::CheckResult> leftResult = modelchecker.check(untilFormula.getLeftSubformula());
std::unique_ptr<storm::modelchecker::CheckResult> rightResult = modelchecker.check(untilFormula.getRightSubformula());
phiStates = storm::storage::BitVector(labeledMdp.getNumberOfStates(), true);
psiStates = eventuallyFormula->getChild()->check(modelchecker);
storm::modelchecker::ExplicitQualitativeCheckResult const& leftQualitativeResult = leftResult->asExplicitQualitativeCheckResult();
storm::modelchecker::ExplicitQualitativeCheckResult const& rightQualitativeResult = rightResult->asExplicitQualitativeCheckResult();
} else {
// If the nested formula is neither an until nor a finally formula, we throw an exception.
throw storm::exceptions::InvalidPropertyException() << "Formula nested inside probability bound operator must be an until or eventually formula for counterexample generation.";
phiStates = leftQualitativeResult.getTruthValues();
psiStates = rightQualitativeResult.getTruthValues();
} else if (probabilityOperator.getSubformula().isEventuallyFormula()) {
storm::logic::EventuallyFormula const& eventuallyFormula = probabilityOperator.getSubformula().asEventuallyFormula();
std::unique_ptr<storm::modelchecker::CheckResult> subResult = modelchecker.check(eventuallyFormula.getSubformula());
storm::modelchecker::ExplicitQualitativeCheckResult const& subQualitativeResult = subResult->asExplicitQualitativeCheckResult();
phiStates = storm::storage::BitVector(labeledMdp.getNumberOfStates(), true);
psiStates = subQualitativeResult.getTruthValues();
}
// Delegate the actual computation work to the function of equal name.
auto startTime = std::chrono::high_resolution_clock::now();
boost::container::flat_set<uint_fast64_t> usedLabelSet = getMinimalLabelSet(labeledMdp, phiStates, psiStates, bound, strictBound, true, storm::settings::counterexampleGeneratorSettings().isUseSchedulerCutsSet());
boost::container::flat_set<uint_fast64_t> usedLabelSet = getMinimalLabelSet(probabilityOperator.getSubformula(), labeledMdp, phiStates, psiStates, bound, strictBound, true, storm::settings::counterexampleGeneratorSettings().isUseSchedulerCutsSet());
auto endTime = std::chrono::high_resolution_clock::now();
std::cout << std::endl << "Computed minimal label set of size " << usedLabelSet.size() << " in " << std::chrono::duration_cast<std::chrono::milliseconds>(endTime - startTime).count() << "ms." << std::endl;
@ -1028,8 +1023,6 @@ namespace storm {
storm::prism::Program restrictedProgram = program.restrictCommands(usedLabelSet);
std::cout << restrictedProgram << std::endl;
std::cout << std::endl << "-------------------------------------------" << std::endl;
// FIXME: Return the DTMC that results from applying the max scheduler in the MDP restricted to the computed label set.
}
};

85
src/counterexamples/SMTMinimalCommandSetGenerator.h
View File

@ -9,6 +9,7 @@
#include "src/storage/prism/Program.h"
#include "src/storage/expressions/Expression.h"
#include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h"
#include "src/modelchecker/ExplicitQuantitativeCheckResult.h"
#include "src/solver/GmmxxNondeterministicLinearEquationSolver.h"
#include "src/utility/counterexamples.h"
@ -1594,7 +1595,7 @@ namespace storm {
* @param checkThresholdFeasible If set, it is verified that the model can actually achieve/exceed the given probability value. If this check
* is made and fails, an exception is thrown.
*/
static boost::container::flat_set<uint_fast64_t> getMinimalCommandSet(storm::prism::Program program, std::string const& constantDefinitionString, storm::models::Mdp<T> const& labeledMdp, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, double probabilityThreshold, bool strictBound, bool checkThresholdFeasible = false, bool includeReachabilityEncoding = false) {
static boost::container::flat_set<uint_fast64_t> getMinimalCommandSet(storm::logic::Formula const& pathFormula, storm::prism::Program program, std::string const& constantDefinitionString, storm::models::Mdp<T> const& labeledMdp, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, double probabilityThreshold, bool strictBound, bool checkThresholdFeasible = false, bool includeReachabilityEncoding = false) {
#ifdef STORM_HAVE_Z3
// Set up all clocks used for time measurement.
auto totalClock = std::chrono::high_resolution_clock::now();
@ -1625,15 +1626,14 @@ namespace storm {
// (1) Check whether its possible to exceed the threshold if checkThresholdFeasible is set.
double maximalReachabilityProbability = 0;
if (checkThresholdFeasible) {
storm::modelchecker::prctl::SparseMdpPrctlModelChecker<T> modelchecker(labeledMdp);
std::vector<T> result = modelchecker.checkUntil(false, phiStates, psiStates, false).first;
storm::modelchecker::SparseMdpPrctlModelChecker<T> modelchecker(labeledMdp);
std::unique_ptr<storm::modelchecker::CheckResult> result = modelchecker.check(pathFormula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> const& quantitativeResult = result->asExplicitQuantitativeCheckResult<double>();
for (auto state : labeledMdp.getInitialStates()) {
maximalReachabilityProbability = std::max(maximalReachabilityProbability, result[state]);
maximalReachabilityProbability = std::max(maximalReachabilityProbability, quantitativeResult[state]);
}
if ((strictBound && maximalReachabilityProbability < probabilityThreshold) || (!strictBound && maximalReachabilityProbability <= probabilityThreshold)) {
throw storm::exceptions::InvalidArgumentException() << "Given probability threshold " << probabilityThreshold << " can not be " << (strictBound ? "achieved" : "exceeded") << " in model with maximal reachability probability of " << maximalReachabilityProbability << ".";
}
std::cout << std::endl << "Maximal reachability in model determined is " << maximalReachabilityProbability << "." << std::endl;
STORM_LOG_THROW((strictBound && maximalReachabilityProbability >= probabilityThreshold) || (!strictBound && maximalReachabilityProbability > probabilityThreshold), storm::exceptions::InvalidArgumentException, "Given probability threshold " << probabilityThreshold << " can not be " << (strictBound ? "achieved" : "exceeded") << " in model with maximal reachability probability of " << maximalReachabilityProbability << ".");
std::cout << std::endl << "Maximal reachability in model is " << maximalReachabilityProbability << "." << std::endl << std::endl;
}
// (2) Identify all states and commands that are relevant, because only these need to be considered later.
@ -1752,50 +1752,49 @@ namespace storm {
#endif
}
static void computeCounterexample(storm::prism::Program program, std::string const& constantDefinitionString, storm::models::Mdp<T> const& labeledMdp, std::shared_ptr<storm::properties::prctl::AbstractPrctlFormula<double>> const& formula) {
static void computeCounterexample(storm::prism::Program program, std::string const& constantDefinitionString, storm::models::Mdp<T> const& labeledMdp, std::shared_ptr<storm::logic::Formula> const& formula) {
#ifdef STORM_HAVE_Z3
std::cout << std::endl << "Generating minimal label counterexample for formula " << formula->toString() << std::endl;
// First, we need to check whether the current formula is an Until-Formula.
std::shared_ptr<storm::properties::prctl::ProbabilisticBoundOperator<double>> probBoundFormula = std::dynamic_pointer_cast<storm::properties::prctl::ProbabilisticBoundOperator<double>>(formula);
if (probBoundFormula.get() == nullptr) {
LOG4CPLUS_ERROR(logger, "Illegal formula " << probBoundFormula->toString() << " for counterexample generation.");
throw storm::exceptions::InvalidPropertyException() << "Illegal formula " << probBoundFormula->toString() << " for counterexample generation.";
}
std::cout << std::endl << "Generating minimal label counterexample for formula " << *formula << std::endl;
// Check whether we were given an upper bound, because counterexample generation is limited to this case.
if (probBoundFormula->getComparisonOperator() != storm::properties::ComparisonType::LESS && probBoundFormula->getComparisonOperator() != storm::properties::ComparisonType::LESS_EQUAL) {
LOG4CPLUS_ERROR(logger, "Illegal comparison operator in formula " << probBoundFormula->toString() << ". Only upper bounds are supported for counterexample generation.");
throw storm::exceptions::InvalidPropertyException() << "Illegal comparison operator in formula " << probBoundFormula->toString() << ". Only upper bounds are supported for counterexample generation.";
}
bool strictBound = probBoundFormula->getComparisonOperator() == storm::properties::ComparisonType::LESS;
STORM_LOG_THROW(formula->isProbabilityOperatorFormula(), storm::exceptions::InvalidPropertyException, "Counterexample generation does not support this kind of formula. Expecting a probability operator as the outermost formula element.");
storm::logic::ProbabilityOperatorFormula const& probabilityOperator = formula->asProbabilityOperatorFormula();
STORM_LOG_THROW(probabilityOperator.hasBound(), storm::exceptions::InvalidPropertyException, "Counterexample generation only supports bounded formulas.");
storm::logic::ComparisonType comparisonType = probabilityOperator.getComparisonType();
STORM_LOG_THROW(comparisonType == storm::logic::ComparisonType::Less || comparisonType == storm::logic::ComparisonType::LessEqual, storm::exceptions::InvalidPropertyException, "Counterexample generation only supports formulas with an upper probability bound.");
STORM_LOG_THROW(probabilityOperator.getSubformula().isUntilFormula() || probabilityOperator.getSubformula().isEventuallyFormula(), storm::exceptions::InvalidPropertyException, "Path formula is required to be of the form 'phi U psi' for counterexample generation.");
bool strictBound = comparisonType == storm::logic::ComparisonType::Less;
double bound = probabilityOperator.getBound();
// Now derive the probability threshold we need to exceed as well as the phi and psi states. Simultaneously, check whether the formula is of a valid shape.
double bound = probBoundFormula->getBound();
std::shared_ptr<storm::properties::prctl::AbstractPathFormula<double>> pathFormula = probBoundFormula->getChild();
storm::storage::BitVector phiStates;
storm::storage::BitVector psiStates;
storm::modelchecker::prctl::SparseMdpPrctlModelChecker<T> modelchecker(labeledMdp);
std::shared_ptr<storm::properties::prctl::Until<double>> untilFormula = std::dynamic_pointer_cast<storm::properties::prctl::Until<double>>(pathFormula);
if(untilFormula.get() != nullptr) {
phiStates = untilFormula->getLeft()->check(modelchecker);
psiStates = untilFormula->getRight()->check(modelchecker);
} if (std::dynamic_pointer_cast<storm::properties::prctl::Eventually<double>>(pathFormula).get() != nullptr) {
// If the nested formula was not an until formula, it remains to check whether it's an eventually formula.
std::shared_ptr<storm::properties::prctl::Eventually<double>> eventuallyFormula = std::dynamic_pointer_cast<storm::properties::prctl::Eventually<double>>(pathFormula);
phiStates = storm::storage::BitVector(labeledMdp.getNumberOfStates(), true);
psiStates = eventuallyFormula->getChild()->check(modelchecker);
} else {
// If the nested formula is neither an until nor a finally formula, we throw an exception.
throw storm::exceptions::InvalidPropertyException() << "Formula nested inside probability bound operator must be an until or eventually formula for counterexample generation.";
storm::modelchecker::SparseMdpPrctlModelChecker<T> modelchecker(labeledMdp);
if (probabilityOperator.getSubformula().isUntilFormula()) {
storm::logic::UntilFormula const& untilFormula = probabilityOperator.getSubformula().asUntilFormula();
std::unique_ptr<storm::modelchecker::CheckResult> leftResult = modelchecker.check(untilFormula.getLeftSubformula());
std::unique_ptr<storm::modelchecker::CheckResult> rightResult = modelchecker.check(untilFormula.getRightSubformula());
storm::modelchecker::ExplicitQualitativeCheckResult const& leftQualitativeResult = leftResult.asExplicitQualitativeCheckResult();
storm::modelchecker::ExplicitQualitativeCheckResult const& rightQualitativeResult = rightResult.asExplicitQualitativeCheckResult();
phiStates = leftQualitativeResult.getTruthValues();
psiStates = rightQualitativeResult.getTruthValues();
} else if (probabilityOperator.getSubformula().isEventuallyFormula()) {
storm::logic::EventuallyFormula const& eventuallyFormula = probabilityOperator.getSubformula().asEventuallyFormula();
std::unique_ptr<storm::modelchecker::CheckResult> subResult = modelchecker.check(untilFormula.getSubformula());
storm::modelchecker::ExplicitQualitativeCheckResult const& subQualitativeResult = subResult.asExplicitQualitativeCheckResult();
phiStates = storm::storage::BitVector(labeledMdp.getNumberOfStates(), true);
psiStates = subResult.getTruthValues();
}
// Delegate the actual computation work to the function of equal name.
auto startTime = std::chrono::high_resolution_clock::now();
auto labelSet = getMinimalCommandSet(program, constantDefinitionString, labeledMdp, phiStates, psiStates, bound, strictBound, true, storm::settings::counterexampleGeneratorSettings().isEncodeReachabilitySet());
auto labelSet = getMinimalCommandSet(probabilityOperator.getSubformula(), program, constantDefinitionString, labeledMdp, phiStates, psiStates, bound, strictBound, true, storm::settings::counterexampleGeneratorSettings().isEncodeReachabilitySet());
auto endTime = std::chrono::high_resolution_clock::now();
std::cout << std::endl << "Computed minimal label set of size " << labelSet.size() << " in " << std::chrono::duration_cast<std::chrono::milliseconds>(endTime - startTime).count() << "ms." << std::endl;

12
src/logic/BinaryBooleanStateFormula.cpp
View File

@ -14,6 +14,18 @@ namespace storm {
return this->getLeftSubformula().isPropositionalFormula() && this->getRightSubformula().isPropositionalFormula();
}
BinaryBooleanStateFormula::OperatorType BinaryBooleanStateFormula::getOperator() const {
return operatorType;
}
bool BinaryBooleanStateFormula::isAnd() const {
return this->getOperator() == OperatorType::And;
}
bool BinaryBooleanStateFormula::isOr() const {
return this->getOperator() == OperatorType::Or;
}
std::ostream& BinaryBooleanStateFormula::writeToStream(std::ostream& out) const {
out << "(";
this->getLeftSubformula().writeToStream(out);

5
src/logic/BinaryBooleanStateFormula.h
View File

@ -19,6 +19,11 @@ namespace storm {
virtual bool isPropositionalFormula() const override;
OperatorType getOperator() const;
virtual bool isAnd() const;
virtual bool isOr() const;
virtual std::ostream& writeToStream(std::ostream& out) const override;
private:

8
src/logic/UnaryBooleanStateFormula.cpp
View File

@ -10,6 +10,14 @@ namespace storm {
return true;
}
UnaryBooleanStateFormula::OperatorType UnaryBooleanStateFormula::getOperator() const {
return operatorType;
}
bool UnaryBooleanStateFormula::isNot() const {
return this->getOperator() == OperatorType::Not;
}
std::ostream& UnaryBooleanStateFormula::writeToStream(std::ostream& out) const {
switch (operatorType) {
case OperatorType::Not: out << "!("; break;

4
src/logic/UnaryBooleanStateFormula.h
View File

@ -17,6 +17,10 @@ namespace storm {
virtual bool isUnaryBooleanStateFormula() const override;
OperatorType getOperator() const;
virtual bool isNot() const;
virtual std::ostream& writeToStream(std::ostream& out) const override;
private:

23
src/modelchecker/AbstractModelChecker.cpp
View File

@ -15,7 +15,7 @@ namespace storm {
} else if (formula.isRewardPathFormula()) {
return this->computeRewards(formula.asRewardPathFormula());
}
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula is invalid.");
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << formula << "' is invalid.");
}
std::unique_ptr<CheckResult> AbstractModelChecker::computeProbabilities(storm::logic::PathFormula const& pathFormula, bool qualitative, boost::optional<storm::logic::OptimalityType> const& optimalityType) {
@ -30,7 +30,7 @@ namespace storm {
} else if (pathFormula.isUntilFormula()) {
return this->computeUntilProbabilities(pathFormula.asUntilFormula(), qualitative, optimalityType);
}
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula is invalid.");
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << pathFormula << "' is invalid.");
}
std::unique_ptr<CheckResult> AbstractModelChecker::computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative, boost::optional<storm::logic::OptimalityType> const& optimalityType) {
@ -66,7 +66,7 @@ namespace storm {
} else if (rewardPathFormula.isReachabilityRewardFormula()) {
return this->computeReachabilityRewards(rewardPathFormula.asReachabilityRewardFormula(), qualitative, optimalityType);
}
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula is invalid.");
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << rewardPathFormula << "' is invalid.");
}
std::unique_ptr<CheckResult> AbstractModelChecker::computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, bool qualitative, boost::optional<storm::logic::OptimalityType> const& optimalityType) {
@ -84,6 +84,8 @@ namespace storm {
std::unique_ptr<CheckResult> AbstractModelChecker::checkStateFormula(storm::logic::StateFormula const& stateFormula) {
if (stateFormula.isBinaryBooleanStateFormula()) {
return this->checkBinaryBooleanStateFormula(stateFormula.asBinaryBooleanStateFormula());
} else if (stateFormula.isUnaryBooleanStateFormula()) {
return this->checkUnaryBooleanStateFormula(stateFormula.asUnaryBooleanStateFormula());
} else if (stateFormula.isBooleanLiteralFormula()) {
return this->checkBooleanLiteralFormula(stateFormula.asBooleanLiteralFormula());
} else if (stateFormula.isProbabilityOperatorFormula()) {
@ -116,7 +118,14 @@ namespace storm {
std::unique_ptr<CheckResult> leftResult = this->check(stateFormula.getLeftSubformula().asStateFormula());
std::unique_ptr<CheckResult> rightResult = this->check(stateFormula.getRightSubformula().asStateFormula());
*leftResult &= *rightResult;
if (stateFormula.isAnd()) {
*leftResult &= *rightResult;
} else if (stateFormula.isOr()) {
*leftResult |= *rightResult;
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << stateFormula << "' is invalid.");
}
return leftResult;
}
@ -172,7 +181,11 @@ namespace storm {
std::unique_ptr<CheckResult> AbstractModelChecker::checkUnaryBooleanStateFormula(storm::logic::UnaryBooleanStateFormula const& stateFormula) {
std::unique_ptr<CheckResult> subResult = this->check(stateFormula.getSubformula());
subResult->complement();
if (stateFormula.isNot()) {
subResult->complement();
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << stateFormula << "' is invalid.");
}
return subResult;
}
}

5
src/modelchecker/CheckResult.h
View File

@ -4,6 +4,7 @@
#include <iostream>
#include <memory>
#include "src/storage/BitVector.h"
#include "src/logic/ComparisonType.h"
namespace storm {
@ -23,8 +24,6 @@ namespace storm {
virtual std::unique_ptr<CheckResult> compareAgainstBound(storm::logic::ComparisonType comparisonType, double bound) const;
friend std::ostream& operator<<(std::ostream& out, CheckResult& checkResult);
virtual bool isExplicit() const;
virtual bool isQuantitative() const;
virtual bool isQualitative() const;
@ -42,8 +41,8 @@ namespace storm {
template<typename ValueType>
ExplicitQuantitativeCheckResult<ValueType> const& asExplicitQuantitativeCheckResult() const;
protected:
virtual std::ostream& writeToStream(std::ostream& out) const = 0;
virtual std::ostream& writeToStream(std::ostream& out, storm::storage::BitVector const& filter) const = 0;
};
std::ostream& operator<<(std::ostream& out, CheckResult& checkResult);

22
src/modelchecker/ExplicitQualitativeCheckResult.cpp
View File

@ -47,5 +47,27 @@ namespace storm {
out << truthValues;
return out;
}
std::ostream& ExplicitQualitativeCheckResult::writeToStream(std::ostream& out, storm::storage::BitVector const& filter) const {
std::ios::fmtflags oldflags(std::cout.flags());
out << "[";
storm::storage::BitVector::const_iterator it = filter.begin();
storm::storage::BitVector::const_iterator itPlusOne = filter.begin();
++itPlusOne;
storm::storage::BitVector::const_iterator ite = filter.end();
out << std::boolalpha;
for (; it != ite; ++itPlusOne, ++it) {
out << truthValues[*it];
if (itPlusOne != ite) {
out << ", ";
}
}
out << "]";
std::cout.flags(oldflags);
return out;
}
}
}

4
src/modelchecker/ExplicitQualitativeCheckResult.h
View File

@ -47,9 +47,9 @@ namespace storm {
storm::storage::BitVector const& getTruthValues() const;
protected:
virtual std::ostream& writeToStream(std::ostream& out) const override;
virtual std::ostream& writeToStream(std::ostream& out, storm::storage::BitVector const& filter) const override;
private:
// The values of the quantitative check result.
storm::storage::BitVector truthValues;

18
src/modelchecker/ExplicitQuantitativeCheckResult.cpp
View File

@ -12,6 +12,24 @@ namespace storm {
return values;
}
template<typename ValueType>
std::ostream& ExplicitQuantitativeCheckResult<ValueType>::writeToStream(std::ostream& out, storm::storage::BitVector const& filter) const {
out << "[";
storm::storage::BitVector::const_iterator it = filter.begin();
storm::storage::BitVector::const_iterator itPlusOne = filter.begin();
++itPlusOne;
storm::storage::BitVector::const_iterator ite = filter.end();
for (; it != ite; ++itPlusOne, ++it) {
out << values[*it];
if (itPlusOne != ite) {
out << ", ";
}
}
out << "]";
return out;
}
template<typename ValueType>
std::ostream& ExplicitQuantitativeCheckResult<ValueType>::writeToStream(std::ostream& out) const {
out << "[";

2
src/modelchecker/ExplicitQuantitativeCheckResult.h
View File

@ -47,8 +47,8 @@ namespace storm {
std::vector<ValueType> const& getValues() const;
protected:
virtual std::ostream& writeToStream(std::ostream& out) const override;
virtual std::ostream& writeToStream(std::ostream& out, storm::storage::BitVector const& filter) const override;
private:
// The values of the quantitative check result.

4
src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp
View File

@ -13,6 +13,7 @@
#include "src/solver/LpSolver.h"
#include "src/exceptions/InvalidPropertyException.h"
#include "src/exceptions/NotImplementedException.h"
namespace storm {
@ -210,7 +211,7 @@ namespace storm {
template<typename ValueType>
std::vector<ValueType> SparseMarkovAutomatonCslModelChecker<ValueType>::computeReachabilityRewardsHelper(bool minimize, storm::storage::BitVector const& targetStates, bool qualitative) const {
// FIXME
}
template<typename ValueType>
@ -232,6 +233,7 @@ namespace storm {
template<typename ValueType>
std::unique_ptr<CheckResult> SparseMarkovAutomatonCslModelChecker<ValueType>::checkAtomicLabelFormula(storm::logic::AtomicLabelFormula const& stateFormula) {
STORM_LOG_THROW(model.hasAtomicProposition(stateFormula.getLabel()), storm::exceptions::InvalidPropertyException, "The property refers to unknown label '" << stateFormula.getLabel() << "'.");
return std::unique_ptr<CheckResult>(new ExplicitQualitativeCheckResult(model.getLabeledStates(stateFormula.getLabel())));
}

1
src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp
View File

@ -308,6 +308,7 @@ namespace storm {
template<typename ValueType>
std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<ValueType>::checkAtomicLabelFormula(storm::logic::AtomicLabelFormula const& stateFormula) {
STORM_LOG_THROW(model.hasAtomicProposition(stateFormula.getLabel()), storm::exceptions::InvalidPropertyException, "The property refers to unknown label '" << stateFormula.getLabel() << "'.");
return std::unique_ptr<CheckResult>(new ExplicitQualitativeCheckResult(model.getLabeledStates(stateFormula.getLabel())));
}

1
src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp
View File

@ -319,6 +319,7 @@ namespace storm {
template<typename ValueType>
std::unique_ptr<CheckResult> SparseMdpPrctlModelChecker<ValueType>::checkAtomicLabelFormula(storm::logic::AtomicLabelFormula const& stateFormula) {
STORM_LOG_THROW(model.hasAtomicProposition(stateFormula.getLabel()), storm::exceptions::InvalidPropertyException, "The property refers to unknown label '" << stateFormula.getLabel() << "'.");
return std::unique_ptr<CheckResult>(new ExplicitQualitativeCheckResult(model.getLabeledStates(stateFormula.getLabel())));
}

72
src/settings/modules/GeneralSettings.cpp
View File

@ -23,12 +23,8 @@ namespace storm {
const std::string GeneralSettings::explicitOptionShortName = "e";
const std::string GeneralSettings::symbolicOptionName = "symbolic";
const std::string GeneralSettings::symbolicOptionShortName = "s";
const std::string GeneralSettings::pctlOptionName = "pctl";
const std::string GeneralSettings::pctlFileOptionName = "pctlfile";
const std::string GeneralSettings::cslOptionName = "csl";
const std::string GeneralSettings::cslFileOptionName = "cslfile";
const std::string GeneralSettings::ltlOptionName = "ltl";
const std::string GeneralSettings::ltlFileOptionName = "ltlfile";
const std::string GeneralSettings::propertyOptionName = "prop";
const std::string GeneralSettings::propertyFileOptionName = "propfile";
const std::string GeneralSettings::transitionRewardsOptionName = "transrew";
const std::string GeneralSettings::stateRewardsOptionName = "staterew";
const std::string GeneralSettings::counterexampleOptionName = "counterexample";
@ -63,18 +59,10 @@ namespace storm {
this->addOption(storm::settings::OptionBuilder(moduleName, symbolicOptionName, false, "Parses the model given in a symbolic representation.").setShortName(symbolicOptionShortName)
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file from which to read the symbolic model.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build())
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("rewardmodel", "The name of the reward model to use.").setDefaultValueString("").setIsOptional(true).build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, pctlOptionName, false, "Specifies a PCTL formula that is to be checked on the model.")
this->addOption(storm::settings::OptionBuilder(moduleName, propertyOptionName, false, "Specifies a PCTL formula that is to be checked on the model.")
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("formula", "The formula to check.").build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, pctlFileOptionName, false, "Specifies the PCTL formulas that are to be checked on the model.")
this->addOption(storm::settings::OptionBuilder(moduleName, propertyFileOptionName, false, "Specifies the PCTL formulas that are to be checked on the model.")
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The file from which to read the PCTL formulas.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, cslOptionName, false, "Specifies a CSL formula that is to be checked on the model.")
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("formula", "The formula to check.").build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, cslFileOptionName, false, "Specifies the CSL formulas that are to be checked on the model.")
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The file from which to read the CSL formulas.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, ltlOptionName, false, "Specifies an LTL formula that is to be checked on the model.")
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("formula", "The formula to check.").build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, ltlFileOptionName, false, "Specifies the LTL formulas that are to be checked on the model.")
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The file from which to read the LTL formulas.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, counterexampleOptionName, false, "Generates a counterexample for the given PRCTL formulas if not satisfied by the model")
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file to which the counterexample is to be written.").setDefaultValueString("-").setIsOptional(true).build()).setShortName(counterexampleOptionShortName).build());
this->addOption(storm::settings::OptionBuilder(moduleName, bisimulationOptionName, false, "Sets whether to perform bisimulation minimization.").setShortName(bisimulationOptionShortName).build());
@ -163,52 +151,20 @@ namespace storm {
return this->getOption(symbolicOptionName).getArgumentByName("rewardmodel").getValueAsString();
}
bool GeneralSettings::isPctlPropertySet() const {
return this->getOption(pctlOptionName).getHasOptionBeenSet();
}
std::string GeneralSettings::getPctlProperty() const {
return this->getOption(pctlOptionName).getArgumentByName("formula").getValueAsString();
}
bool GeneralSettings::isPctlFileSet() const {
return this->getOption(pctlFileOptionName).getHasOptionBeenSet();
}
std::string GeneralSettings::getPctlPropertiesFilename() const {
return this->getOption(pctlFileOptionName).getArgumentByName("filename").getValueAsString();
}
bool GeneralSettings::isCslPropertySet() const {
return this->getOption(cslOptionName).getHasOptionBeenSet();
}
std::string GeneralSettings::getCslProperty() const {
return this->getOption(cslOptionName).getArgumentByName("formula").getValueAsString();
}
bool GeneralSettings::isCslFileSet() const {
return this->getOption(cslFileOptionName).getHasOptionBeenSet();
}
std::string GeneralSettings::getCslPropertiesFilename() const {
return this->getOption(cslOptionName).getArgumentByName("filename").getValueAsString();
}
bool GeneralSettings::isLtlPropertySet() const {
return this->getOption(ltlOptionName).getHasOptionBeenSet();
bool GeneralSettings::isPropertySet() const {
return this->getOption(propertyOptionName).getHasOptionBeenSet();
}
std::string GeneralSettings::getLtlProperty() const {
return this->getOption(ltlOptionName).getArgumentByName("formula").getValueAsString();
std::string GeneralSettings::getProperty() const {
return this->getOption(propertyOptionName).getArgumentByName("formula").getValueAsString();
}
bool GeneralSettings::isLtlFileSet() const {
return this->getOption(ltlFileOptionName).getHasOptionBeenSet();
bool GeneralSettings::isPropertyFileSet() const {
return this->getOption(propertyFileOptionName).getHasOptionBeenSet();
}
std::string GeneralSettings::getLtlPropertiesFilename() const {
return this->getOption(ltlOptionName).getArgumentByName("filename").getValueAsString();
std::string GeneralSettings::getPropertiesFilename() const {
return this->getOption(propertyFileOptionName).getArgumentByName("filename").getValueAsString();
}
bool GeneralSettings::isTransitionRewardsSet() const {
@ -288,8 +244,8 @@ namespace storm {
STORM_LOG_THROW(!isSymbolicSet() || !isExplicitSet(), storm::exceptions::InvalidSettingsException, "The model may be either given in an explicit or a symbolic format, but not both.");
// Make sure that one "source" for properties is given.
uint_fast64_t propertySources = 0 + (isPctlPropertySet() ? 1 : 0) + (isPctlFileSet() ? 1 : 0) + (isCslPropertySet() ? + 1 : 0) + (isCslFileSet() ? 1 : 0) + (isLtlPropertySet() ? 1 : 0) + (isLtlFileSet() ? 1 : 0);
STORM_LOG_THROW(propertySources <= 1, storm::exceptions::InvalidSettingsException, "Please specify exactly one source of properties.");
uint_fast64_t propertySources = 0 + (isPropertySet() ? 1 : 0) + (isPropertyFileSet() ? 1 : 0);
STORM_LOG_THROW(propertySources <= 1, storm::exceptions::InvalidSettingsException, "Please specify either a file that contains the properties or a property on the command line, but not both.");
return true;
}

88
src/settings/modules/GeneralSettings.h
View File

@ -142,88 +142,32 @@ namespace storm {
std::string getSymbolicRewardModelName() const;
/*!
* Retrieves whether the pctl option was set.
* Retrieves whether the property option was set.
*
* @return True if the pctl option was set.
* @return True if the property option was set.
*/
bool isPctlPropertySet() const;
bool isPropertySet() const;
/*!
* Retrieves the property specified with the pctl option.
* Retrieves the property specified with the property option.
*
* @return The property specified with the pctl option.
* @return The property specified with the property option.
*/
std::string getPctlProperty() const;
std::string getProperty() const;
/*!
* Retrieves whether the pctl-file option was set.
* Retrieves whether a property file was set.
*
* @return True iff the pctl-file option was set.
* @return True iff a property was set.
*/
bool isPctlFileSet() const;
bool isPropertyFileSet() const;
/*!
* Retrieves the name of the file that contains the PCTL properties to be checked on the model.
* Retrieves the name of the file that contains the properties to be checked on the model.
*
* @return The name of the file that contains the PCTL properties to be checked on the model.
* @return The name of the file that contains the properties to be checked on the model.
*/
std::string getPctlPropertiesFilename() const;
/*!
* Retrieves whether the csl option was set.
*
* @return True if the csl option was set.
*/
bool isCslPropertySet() const;
/*!
* Retrieves the property specified with the csl option.
*
* @return The property specified with the csl option.
*/
std::string getCslProperty() const;
/*!
* Retrieves whether the csl-file option was set.
*
* @return True iff the csl-file option was set.
*/
bool isCslFileSet() const;
/*!
* Retrieves the name of the file that contains the CSL properties to be checked on the model.
*
* @return The name of the file that contains the CSL properties to be checked on the model.
*/
std::string getCslPropertiesFilename() const;
/*!
* Retrieves whether the ltl option was set.
*
* @return True if the ltl option was set.
*/
bool isLtlPropertySet() const;
/*!
* Retrieves the property specified with the ltl option.
*
* @return The property specified with the ltl option.
*/
std::string getLtlProperty() const;
/*!
* Retrieves whether the ltl-file option was set.
*
* @return True iff the ltl-file option was set.
*/
bool isLtlFileSet() const;
/*!
* Retrieves the name of the file that contains the LTL properties to be checked on the model.
*
* @return The name of the file that contains the LTL properties to be checked on the model.
*/
std::string getLtlPropertiesFilename() const;
std::string getPropertiesFilename() const;
/*!
* Retrieves whether the transition reward option was set.
@ -363,12 +307,8 @@ namespace storm {
static const std::string explicitOptionShortName;
static const std::string symbolicOptionName;
static const std::string symbolicOptionShortName;
static const std::string pctlOptionName;
static const std::string pctlFileOptionName;
static const std::string cslOptionName;
static const std::string cslFileOptionName;
static const std::string ltlOptionName;
static const std::string ltlFileOptionName;
static const std::string propertyOptionName;
static const std::string propertyFileOptionName;
static const std::string transitionRewardsOptionName;
static const std::string stateRewardsOptionName;
static const std::string counterexampleOptionName;

10
src/storage/prism/Program.cpp
View File

@ -53,6 +53,16 @@ namespace storm {
return false;
}
std::vector<std::reference_wrapper<storm::prism::Constant const>> Program::getUndefinedConstants() const {
std::vector<std::reference_wrapper<storm::prism::Constant const>> result;
for (auto const& constant : this->getConstants()) {
if (!constant.isDefined()) {
result.push_back(constant);
}
}
return result;
}
bool Program::hasConstant(std::string const& constantName) const {
return this->constantToIndexMap.find(constantName) != this->constantToIndexMap.end();
}

7
src/storage/prism/Program.h
View File

@ -72,6 +72,13 @@ namespace storm {
*/
bool hasUndefinedConstants() const;
/*!
* Retrieves the undefined constants in the program.
*
* @return The undefined constants in the program.
*/
std::vector<std::reference_wrapper<storm::prism::Constant const>> getUndefinedConstants() const;
/*!
* Retrieves whether the given constant exists in the program.
*

43
src/utility/cli.h
View File

@ -40,7 +40,10 @@ log4cplus::Logger logger;
// Headers related to parsing.
#include "src/parser/AutoParser.h"
#include "src/parser/PrismParser.h"
#include "src/parser/PrctlParser.h"
#include "src/parser/FormulaParser.h"
// Formula headers.
#include "src/logic/Formulas.h"
// Model headers.
#include "src/models/AbstractModel.h"
@ -61,6 +64,7 @@ log4cplus::Logger logger;
#include "src/counterexamples/SMTMinimalCommandSetGenerator.h"
// Headers related to exception handling.
#include "src/exceptions/InvalidArgumentException.h"
#include "src/exceptions/InvalidSettingsException.h"
#include "src/exceptions/InvalidTypeException.h"
@ -290,7 +294,7 @@ namespace storm {
return result;
}
void generateCounterexample(std::shared_ptr<storm::models::AbstractModel<double>> model, std::shared_ptr<storm::properties::prctl::AbstractPrctlFormula<double>> const& formula) {
void generateCounterexample(std::shared_ptr<storm::models::AbstractModel<double>> model, std::shared_ptr<storm::logic::Formula> const& formula) {
if (storm::settings::counterexampleGeneratorSettings().isMinimalCommandSetGenerationSet()) {
STORM_LOG_THROW(model->getType() == storm::models::MDP, storm::exceptions::InvalidTypeException, "Minimal command set generation is only available for MDPs.");
STORM_LOG_THROW(storm::settings::generalSettings().isSymbolicSet(), storm::exceptions::InvalidSettingsException, "Minimal command set generation is only available for symbolic models.");
@ -324,21 +328,32 @@ namespace storm {
// If we were requested to generate a counterexample, we now do so.
if (settings.isCounterexampleSet()) {
STORM_LOG_THROW(settings.isPctlPropertySet(), storm::exceptions::InvalidSettingsException, "Unable to generate counterexample without a property.");
std::shared_ptr<storm::properties::prctl::PrctlFilter<double>> filterFormula = storm::parser::PrctlParser::parsePrctlFormula(settings.getPctlProperty());
generateCounterexample(model, filterFormula->getChild());
} else if (settings.isPctlPropertySet()) {
std::shared_ptr<storm::properties::prctl::PrctlFilter<double>> filterFormula = storm::parser::PrctlParser::parsePrctlFormula(storm::settings::generalSettings().getPctlProperty());
STORM_LOG_THROW(settings.isPropertySet(), storm::exceptions::InvalidSettingsException, "Unable to generate counterexample without a property.");
storm::parser::FormulaParser formulaParser;
std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseFromString(settings.getProperty());
generateCounterexample(model, formula);
} else if (settings.isPropertySet()) {
storm::parser::FormulaParser formulaParser;
std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseFromString(storm::settings::generalSettings().getProperty());
std::cout << "Model checking property: " << *formula << " ...";
std::unique_ptr<storm::modelchecker::CheckResult> result;
if (model->getType() == storm::models::DTMC) {
std::shared_ptr<storm::models::Dtmc<double>> dtmc = model->as<storm::models::Dtmc<double>>();
modelchecker::prctl::SparseDtmcPrctlModelChecker<double> modelchecker(*dtmc);
filterFormula->check(modelchecker);
}
if (model->getType() == storm::models::MDP) {
storm::modelchecker::SparseDtmcPrctlModelChecker<double> modelchecker(*dtmc);
result = modelchecker.check(*formula);
} else if (model->getType() == storm::models::MDP) {
std::shared_ptr<storm::models::Mdp<double>> mdp = model->as<storm::models::Mdp<double>>();
modelchecker::prctl::SparseMdpPrctlModelChecker<double> modelchecker(*mdp);
filterFormula->check(modelchecker);
storm::modelchecker::SparseMdpPrctlModelChecker<double> modelchecker(*mdp);
result = modelchecker.check(*formula);
}
if (result) {
std::cout << " done." << std::endl;
std::cout << "Result (initial states): ";
result->writeToStream(std::cout, model->getInitialStates());
std::cout << std::endl << std::endl;
} else {
std::cout << " skipped, because the modelling formalism is currently unsupported." << std::endl;
}
}
}

80
test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp
View File

@ -3,6 +3,7 @@
#include "src/settings/SettingsManager.h"
#include "src/settings/SettingMemento.h"
#include "src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h"
#include "src/modelchecker/ExplicitQuantitativeCheckResult.h"
#include "src/solver/GmmxxLinearEquationSolver.h"
#include "src/parser/AutoParser.h"
@ -16,34 +17,31 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, Crowds) {
ASSERT_EQ(2036647ull, dtmc->getNumberOfStates());
ASSERT_EQ(7362293ull, dtmc->getNumberOfTransitions());
storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double> mc(*dtmc, std::unique_ptr<storm::solver::LinearEquationSolver<double>>(new storm::solver::GmmxxLinearEquationSolver<double>()));
storm::modelchecker::SparseDtmcPrctlModelChecker<double> checker(*dtmc, std::unique_ptr<storm::solver::LinearEquationSolver<double>>(new storm::solver::GmmxxLinearEquationSolver<double>()));
auto apFormula = std::make_shared<storm::properties::prctl::Ap<double>>("observe0Greater1");
auto eventuallyFormula = std::make_shared<storm::properties::prctl::Eventually<double>>(apFormula);
auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("observe0Greater1");
auto eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula);
LOG4CPLUS_WARN(logger, "Model Checking P=? [F observe0Greater1] on crowds/crowds20_5...");
std::vector<double> result = eventuallyFormula->check(mc, false);
LOG4CPLUS_WARN(logger, "Done.");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*eventuallyFormula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
ASSERT_LT(std::abs(result[0] - 0.2296800237), storm::settings::gmmxxEquationSolverSettings().getPrecision());
EXPECT_NEAR(0.2296800237, quantitativeResult1[0], storm::settings::gmmxxEquationSolverSettings().getPrecision());
apFormula = std::make_shared<storm::properties::prctl::Ap<double>>("observeIGreater1");
eventuallyFormula = std::make_shared<storm::properties::prctl::Eventually<double>>(apFormula);
labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("observeIGreater1");
eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula);
LOG4CPLUS_WARN(logger, "Model Checking P=? [F observeIGreater1] on crowds/crowds20_5...");
result = eventuallyFormula->check(mc, false);
LOG4CPLUS_WARN(logger, "Done.");
result = checker.check(*eventuallyFormula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
ASSERT_LT(std::abs(result[0] - 0.05073232193), storm::settings::gmmxxEquationSolverSettings().getPrecision());
EXPECT_NEAR(0.05073232193, quantitativeResult2[0], storm::settings::gmmxxEquationSolverSettings().getPrecision());
apFormula = std::make_shared<storm::properties::prctl::Ap<double>>("observeOnlyTrueSender");
eventuallyFormula = std::make_shared<storm::properties::prctl::Eventually<double>>(apFormula);
labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("observeOnlyTrueSender");
eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula);
LOG4CPLUS_WARN(logger, "Model Checking P=? [F observeOnlyTrueSender] on crowds/crowds20_5...");
result = eventuallyFormula->check(mc, false);
LOG4CPLUS_WARN(logger, "Done.");
ASSERT_LT(std::abs(result[0] - 0.22742171078), storm::settings::gmmxxEquationSolverSettings().getPrecision());
result = checker.check(*eventuallyFormula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.22742171078, quantitativeResult3[0], storm::settings::gmmxxEquationSolverSettings().getPrecision());
}
@ -57,32 +55,30 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, SynchronousLeader) {
ASSERT_EQ(1312334ull, dtmc->getNumberOfStates());
ASSERT_EQ(1574477ull, dtmc->getNumberOfTransitions());
storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double> mc(*dtmc, std::unique_ptr<storm::solver::LinearEquationSolver<double>>(new storm::solver::GmmxxLinearEquationSolver<double>()));
auto apFormula = std::make_shared<storm::properties::prctl::Ap<double>>("elected");
auto eventuallyFormula = std::make_shared<storm::properties::prctl::Eventually<double>>(apFormula);
LOG4CPLUS_WARN(logger, "Model Checking P=? [F elected] on synchronous_leader/leader6_8...");
std::vector<double> result = eventuallyFormula->check(mc, false);
LOG4CPLUS_WARN(logger, "Done.");
storm::modelchecker::SparseDtmcPrctlModelChecker<double> checker(*dtmc, std::unique_ptr<storm::solver::LinearEquationSolver<double>>(new storm::solver::GmmxxLinearEquationSolver<double>()));
ASSERT_LT(std::abs(result[0] - 1.0), storm::settings::gmmxxEquationSolverSettings().getPrecision());
auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("elected");
auto eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula);
apFormula = std::make_shared<storm::properties::prctl::Ap<double>>("elected");
auto boundedUntilFormula = std::make_shared<storm::properties::prctl::BoundedUntil<double>>(std::make_shared<storm::properties::prctl::Ap<double>>("true"), apFormula, 20);
LOG4CPLUS_WARN(logger, "Model Checking P=? [F<=20 elected] on synchronous_leader/leader6_8...");
result = boundedUntilFormula->check(mc, false);
LOG4CPLUS_WARN(logger, "Done.");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*eventuallyFormula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(1.0, quantitativeResult1[0], storm::settings::gmmxxEquationSolverSettings().getPrecision());
ASSERT_LT(std::abs(result[0] - 0.9993949793), storm::settings::gmmxxEquationSolverSettings().getPrecision());
labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("elected");
auto trueFormula = std::make_shared<storm::logic::BooleanLiteralFormula>(true);
auto boundedUntilFormula = std::make_shared<storm::logic::BoundedUntilFormula>(trueFormula, labelFormula, 20);
apFormula = std::make_shared<storm::properties::prctl::Ap<double>>("elected");
auto reachabilityRewardFormula = std::make_shared<storm::properties::prctl::ReachabilityReward<double>>(apFormula);
result = checker.check(*boundedUntilFormula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.9993949793, quantitativeResult2[0], storm::settings::gmmxxEquationSolverSettings().getPrecision());
LOG4CPLUS_WARN(logger, "Model Checking R=? [F elected] on synchronous_leader/leader6_8...");
result = reachabilityRewardFormula->check(mc, false);
LOG4CPLUS_WARN(logger, "Done.");
labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("elected");
auto reachabilityRewardFormula = std::make_shared<storm::logic::ReachabilityRewardFormula>(labelFormula);
ASSERT_LT(std::abs(result[0] - 1.025106273), storm::settings::gmmxxEquationSolverSettings().getPrecision());
result = checker.check(*reachabilityRewardFormula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(1.025106273, quantitativeResult3[0], storm::settings::gmmxxEquationSolverSettings().getPrecision());
}

165
test/performance/modelchecker/SparseMdpPrctlModelCheckerTest.cpp
View File

@ -3,6 +3,7 @@
#include "src/settings/SettingsManager.h"
#include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h"
#include "src/modelchecker/ExplicitQuantitativeCheckResult.h"
#include "src/solver/NativeNondeterministicLinearEquationSolver.h"
#include "src/parser/AutoParser.h"
@ -16,46 +17,59 @@ TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) {
ASSERT_EQ(2095783ull, mdp->getNumberOfStates());
ASSERT_EQ(7714385ull, mdp->getNumberOfTransitions());
storm::modelchecker::prctl::SparseMdpPrctlModelChecker<double> mc(*mdp, std::shared_ptr<storm::solver::NativeNondeterministicLinearEquationSolver<double>>(new storm::solver::NativeNondeterministicLinearEquationSolver<double>()));
storm::modelchecker::SparseMdpPrctlModelChecker<double> checker(*mdp, std::shared_ptr<storm::solver::NativeNondeterministicLinearEquationSolver<double>>(new storm::solver::NativeNondeterministicLinearEquationSolver<double>()));
auto apFormula = std::make_shared<storm::properties::prctl::Ap<double>>("elected");
auto eventuallyFormula = std::make_shared<storm::properties::prctl::Eventually<double>>(apFormula);
std::vector<double> result = mc.checkOptimizingOperator(*eventuallyFormula, true);
ASSERT_LT(std::abs(result[0] - 1.0), storm::settings::nativeEquationSolverSettings().getPrecision());
result = mc.checkOptimizingOperator(*eventuallyFormula, false);
ASSERT_LT(std::abs(result[0] - 1.0), storm::settings::nativeEquationSolverSettings().getPrecision());
auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("elected");
auto eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula);
auto minProbabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Minimize, eventuallyFormula);
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*minProbabilityOperatorFormula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(1.0, quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision());
apFormula = std::make_shared<storm::properties::prctl::Ap<double>>("elected");
auto boundedEventuallyFormula = std::make_shared<storm::properties::prctl::BoundedEventually<double>>(apFormula, 25);
auto maxProbabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Maximize, eventuallyFormula);
result = checker.check(*maxProbabilityOperatorFormula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
result = mc.checkOptimizingOperator(*boundedEventuallyFormula, true);
EXPECT_NEAR(1.0, quantitativeResult2[0], storm::settings::nativeEquationSolverSettings().getPrecision());
ASSERT_LT(std::abs(result[0] - 0.0), storm::settings::nativeEquationSolverSettings().getPrecision());
labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("elected");
auto trueFormula = std::make_shared<storm::logic::BooleanLiteralFormula>(true);
auto boundedUntilFormula = std::make_shared<storm::logic::BoundedUntilFormula>(trueFormula, labelFormula, 25);
minProbabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Minimize, boundedUntilFormula);
result = mc.checkOptimizingOperator(*boundedEventuallyFormula, false);
result = checker.check(*minProbabilityOperatorFormula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.0, quantitativeResult3[0], storm::settings::nativeEquationSolverSettings().getPrecision());
ASSERT_LT(std::abs(result[0] - 0.0), storm::settings::nativeEquationSolverSettings().getPrecision());
maxProbabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Maximize, boundedUntilFormula);
result = checker.check(*maxProbabilityOperatorFormula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult4 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.0, quantitativeResult4[0], storm::settings::nativeEquationSolverSettings().getPrecision());
apFormula = std::make_shared<storm::properties::prctl::Ap<double>>("elected");
auto reachabilityRewardFormula = std::make_shared<storm::properties::prctl::ReachabilityReward<double>>(apFormula);
labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("elected");
auto reachabilityRewardFormula = std::make_shared<storm::logic::ReachabilityRewardFormula>(labelFormula);
auto minRewardOperatorFormula = std::make_shared<storm::logic::RewardOperatorFormula>(storm::logic::OptimalityType::Minimize, reachabilityRewardFormula);
result = mc.checkOptimizingOperator(*reachabilityRewardFormula, true);
result = checker.check(*minRewardOperatorFormula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult5 = result->asExplicitQuantitativeCheckResult<double>();
ASSERT_LT(std::abs(result[0] - 6.172433512), storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(6.172433512, quantitativeResult5[0], storm::settings::nativeEquationSolverSettings().getPrecision());
result = mc.checkOptimizingOperator(*reachabilityRewardFormula, false);
auto maxRewardOperatorFormula = std::make_shared<storm::logic::RewardOperatorFormula>(storm::logic::OptimalityType::Maximize, reachabilityRewardFormula);
result = checker.check(*maxRewardOperatorFormula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult6 = result->asExplicitQuantitativeCheckResult<double>();
ASSERT_LT(std::abs(result[0] - 6.1724344), storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(6.1724344, quantitativeResult6[0], storm::settings::nativeEquationSolverSettings().getPrecision());
}
TEST(SparseMdpPrctlModelCheckerTest, Consensus) {
// Increase the maximal number of iterations, because the solver does not converge otherwise.
// This is done in the main cpp unit
std::shared_ptr<storm::models::AbstractModel<double>> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.tra", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.lab", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.steps.state.rew", "");
ASSERT_EQ(abstractModel->getType(), storm::models::MDP);
@ -65,62 +79,81 @@ TEST(SparseMdpPrctlModelCheckerTest, Consensus) {
ASSERT_EQ(63616ull, mdp->getNumberOfStates());
ASSERT_EQ(213472ull, mdp->getNumberOfTransitions());
storm::modelchecker::prctl::SparseMdpPrctlModelChecker<double> mc(*mdp, std::shared_ptr<storm::solver::NativeNondeterministicLinearEquationSolver<double>>(new storm::solver::NativeNondeterministicLinearEquationSolver<double>()));
auto apFormula = std::make_shared<storm::properties::prctl::Ap<double>>("finished");
auto eventuallyFormula = std::make_shared<storm::properties::prctl::Eventually<double>>(apFormula);
std::vector<double> result = mc.checkOptimizingOperator(*eventuallyFormula, true);
storm::modelchecker::SparseMdpPrctlModelChecker<double> checker(*mdp, std::shared_ptr<storm::solver::NativeNondeterministicLinearEquationSolver<double>>(new storm::solver::NativeNondeterministicLinearEquationSolver<double>()));
ASSERT_LT(std::abs(result[31168] - 1.0), storm::settings::nativeEquationSolverSettings().getPrecision());
auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("finished");
auto eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula);
auto minProbabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Minimize, eventuallyFormula);
apFormula = std::make_shared<storm::properties::prctl::Ap<double>>("finished");
auto apFormula2 = std::make_shared<storm::properties::prctl::Ap<double>>("all_coins_equal_0");
auto andFormula = std::make_shared<storm::properties::prctl::And<double>>(apFormula, apFormula2);
eventuallyFormula = std::make_shared<storm::properties::prctl::Eventually<double>>(andFormula);
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*minProbabilityOperatorFormula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
result = mc.checkOptimizingOperator(*eventuallyFormula, true);
EXPECT_NEAR(1.0, quantitativeResult1[31168], storm::settings::nativeEquationSolverSettings().getPrecision());
ASSERT_LT(std::abs(result[31168] - 0.4374282832), storm::settings::nativeEquationSolverSettings().getPrecision());
labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("finished");
auto labelFormula2 = std::make_shared<storm::logic::AtomicLabelFormula>("all_coins_equal_0");
auto andFormula = std::make_shared<storm::logic::BinaryBooleanStateFormula>(storm::logic::BinaryBooleanStateFormula::OperatorType::And, labelFormula, labelFormula2);
eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(andFormula);
minProbabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Minimize, eventuallyFormula);
apFormula = std::make_shared<storm::properties::prctl::Ap<double>>("finished");
apFormula2 = std::make_shared<storm::properties::prctl::Ap<double>>("all_coins_equal_1");
andFormula = std::make_shared<storm::properties::prctl::And<double>>(apFormula, apFormula2);
eventuallyFormula = std::make_shared<storm::properties::prctl::Eventually<double>>(andFormula);
result = checker.check(*minProbabilityOperatorFormula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
result = mc.checkOptimizingOperator(*eventuallyFormula, false);
EXPECT_NEAR(0.4374282832, quantitativeResult2[31168], storm::settings::nativeEquationSolverSettings().getPrecision());
ASSERT_LT(std::abs(result[31168] - 0.5293286369), storm::settings::nativeEquationSolverSettings().getPrecision());
apFormula = std::make_shared<storm::properties::prctl::Ap<double>>("finished");
apFormula2 = std::make_shared<storm::properties::prctl::Ap<double>>("agree");
auto notFormula = std::make_shared<storm::properties::prctl::Not<double>>(apFormula2);
andFormula = std::make_shared<storm::properties::prctl::And<double>>(apFormula, notFormula);
eventuallyFormula = std::make_shared<storm::properties::prctl::Eventually<double>>(andFormula);
labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("finished");
labelFormula2 = std::make_shared<storm::logic::AtomicLabelFormula>("all_coins_equal_1");
andFormula = std::make_shared<storm::logic::BinaryBooleanStateFormula>(storm::logic::BinaryBooleanStateFormula::OperatorType::And, labelFormula, labelFormula2);
eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(andFormula);
auto maxProbabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Maximize, eventuallyFormula);
result = mc.checkOptimizingOperator(*eventuallyFormula, false);
result = checker.check(*maxProbabilityOperatorFormula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>();
ASSERT_LT(std::abs(result[31168] - 0.10414097), storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(0.5293286369, quantitativeResult3[31168], storm::settings::nativeEquationSolverSettings().getPrecision());
labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("finished");
labelFormula2 = std::make_shared<storm::logic::AtomicLabelFormula>("agree");
auto notFormula = std::make_shared<storm::logic::UnaryBooleanStateFormula>(storm::logic::UnaryBooleanStateFormula::OperatorType::Not, labelFormula2);
andFormula = std::make_shared<storm::logic::BinaryBooleanStateFormula>(storm::logic::BinaryBooleanStateFormula::OperatorType::And, labelFormula, notFormula);
eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(andFormula);
maxProbabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Maximize, eventuallyFormula);
apFormula = std::make_shared<storm::properties::prctl::Ap<double>>("finished");
auto boundedEventuallyFormula = std::make_shared<storm::properties::prctl::BoundedEventually<double>>(apFormula, 50ull);
result = checker.check(*maxProbabilityOperatorFormula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult4 = result->asExplicitQuantitativeCheckResult<double>();
result = mc.checkOptimizingOperator(*boundedEventuallyFormula, true);
EXPECT_NEAR(0.10414097, quantitativeResult4[31168], storm::settings::nativeEquationSolverSettings().getPrecision());
labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("finished");
auto trueFormula = std::make_shared<storm::logic::BooleanLiteralFormula>(true);
auto boundedUntilFormula = std::make_shared<storm::logic::BoundedUntilFormula>(trueFormula, labelFormula, 50);
minProbabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Minimize, boundedUntilFormula);
result = checker.check(*minProbabilityOperatorFormula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult5 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.0, quantitativeResult5[31168], storm::settings::nativeEquationSolverSettings().getPrecision());
maxProbabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Maximize, boundedUntilFormula);
ASSERT_LT(std::abs(result[31168] - 0.0), storm::settings::nativeEquationSolverSettings().getPrecision());
result = checker.check(*maxProbabilityOperatorFormula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult6 = result->asExplicitQuantitativeCheckResult<double>();
result = mc.checkOptimizingOperator(*boundedEventuallyFormula, false);
EXPECT_NEAR(0.0, quantitativeResult6[31168], storm::settings::nativeEquationSolverSettings().getPrecision());
ASSERT_LT(std::abs(result[31168] - 0.0), storm::settings::nativeEquationSolverSettings().getPrecision());
labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("finished");
auto reachabilityRewardFormula = std::make_shared<storm::logic::ReachabilityRewardFormula>(labelFormula);
auto minRewardOperatorFormula = std::make_shared<storm::logic::RewardOperatorFormula>(storm::logic::OptimalityType::Minimize, reachabilityRewardFormula);
apFormula = std::make_shared<storm::properties::prctl::Ap<double>>("finished");
auto reachabilityRewardFormula = std::make_shared<storm::properties::prctl::ReachabilityReward<double>>(apFormula);
result = checker.check(*minRewardOperatorFormula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult7 = result->asExplicitQuantitativeCheckResult<double>();
result = mc.checkOptimizingOperator(*reachabilityRewardFormula, true);
ASSERT_LT(std::abs(result[31168] - 1725.593313), storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(1725.593313, quantitativeResult7[31168], storm::settings::nativeEquationSolverSettings().getPrecision());
result = mc.checkOptimizingOperator(*reachabilityRewardFormula, false);
auto maxRewardOperatorFormula = std::make_shared<storm::logic::RewardOperatorFormula>(storm::logic::OptimalityType::Maximize, reachabilityRewardFormula);
result = checker.check(*maxRewardOperatorFormula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult8 = result->asExplicitQuantitativeCheckResult<double>();
ASSERT_LT(std::abs(result[31168] - 2183.142422), storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(2183.142422, quantitativeResult8[31168], storm::settings::nativeEquationSolverSettings().getPrecision());
}
Write Preview
Loading…
Cancel
Save