diff --git a/src/counterexamples/MILPMinimalLabelSetGenerator.h b/src/counterexamples/MILPMinimalLabelSetGenerator.h index 7e57fff60..33e632cc0 100644 --- a/src/counterexamples/MILPMinimalLabelSetGenerator.h +++ b/src/counterexamples/MILPMinimalLabelSetGenerator.h @@ -1000,35 +1000,35 @@ 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::ir::Program const& program, storm::models::Mdp const& labeledMdp, std::shared_ptr> const & formulaPtr) { + static void computeCounterexample(storm::ir::Program const& program, storm::models::Mdp const& labeledMdp, std::shared_ptr> const & formulaPtr) { std::cout << std::endl << "Generating minimal label counterexample for formula " << formulaPtr->toString() << std::endl; // First, we need to check whether the current formula is an Until-Formula. - std::shared_ptr> probBoundFormula = std::dynamic_pointer_cast>(formulaPtr); + std::shared_ptr> probBoundFormula = std::dynamic_pointer_cast>(formulaPtr); 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."; } - if (probBoundFormula->getComparisonOperator() != storm::property::ComparisonType::LESS && probBoundFormula->getComparisonOperator() != storm::property::ComparisonType::LESS_EQUAL) { + 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::property::ComparisonType::LESS); + bool strictBound = !(probBoundFormula->getComparisonOperator() == storm::properties::ComparisonType::LESS); // 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> pathFormula = probBoundFormula->getChild(); + std::shared_ptr> pathFormula = probBoundFormula->getChild(); storm::storage::BitVector phiStates; storm::storage::BitVector psiStates; storm::modelchecker::prctl::SparseMdpPrctlModelChecker modelchecker(labeledMdp); - std::shared_ptr> untilFormula = std::dynamic_pointer_cast>(pathFormula); + std::shared_ptr> untilFormula = std::dynamic_pointer_cast>(pathFormula); if(untilFormula.get() != nullptr) { phiStates = untilFormula->getLeft()->check(modelchecker); psiStates = untilFormula->getRight()->check(modelchecker); - } if (std::dynamic_pointer_cast>(pathFormula).get() != nullptr) { + } if (std::dynamic_pointer_cast>(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> eventuallyFormula = std::dynamic_pointer_cast>(pathFormula); + std::shared_ptr> eventuallyFormula = std::dynamic_pointer_cast>(pathFormula); phiStates = storm::storage::BitVector(labeledMdp.getNumberOfStates(), true); psiStates = eventuallyFormula->getChild()->check(modelchecker); diff --git a/src/counterexamples/PathBasedSubsystemGenerator.h b/src/counterexamples/PathBasedSubsystemGenerator.h index 2713643bf..c4e7a6558 100644 --- a/src/counterexamples/PathBasedSubsystemGenerator.h +++ b/src/counterexamples/PathBasedSubsystemGenerator.h @@ -375,7 +375,7 @@ public: /*! * */ - static storm::models::Dtmc computeCriticalSubsystem(storm::models::Dtmc const & model, std::shared_ptr> const & stateFormula) { + static storm::models::Dtmc computeCriticalSubsystem(storm::models::Dtmc const & model, std::shared_ptr> const & stateFormula) { //------------------------------------------------------------- // 1. Strip and handle formulas @@ -395,14 +395,14 @@ public: // Strip bound operator - std::shared_ptr> boundOperator = std::dynamic_pointer_cast>(stateFormula); + std::shared_ptr> boundOperator = std::dynamic_pointer_cast>(stateFormula); if(boundOperator == nullptr){ LOG4CPLUS_ERROR(logger, "No path bound operator at formula root."); return model.getSubDtmc(subSys); } T bound = boundOperator->getBound(); - std::shared_ptr> pathFormula = boundOperator->getChild(); + std::shared_ptr> pathFormula = boundOperator->getChild(); // get "init" labeled states storm::storage::BitVector initStates = model.getLabeledStates("init"); @@ -423,9 +423,9 @@ public: storm::storage::BitVector allowedStates; storm::storage::BitVector targetStates; - std::shared_ptr> eventually = std::dynamic_pointer_cast>(pathFormula); - std::shared_ptr> globally = std::dynamic_pointer_cast>(pathFormula); - std::shared_ptr> until = std::dynamic_pointer_cast>(pathFormula); + std::shared_ptr> eventually = std::dynamic_pointer_cast>(pathFormula); + std::shared_ptr> globally = std::dynamic_pointer_cast>(pathFormula); + std::shared_ptr> until = std::dynamic_pointer_cast>(pathFormula); if(eventually.get() != nullptr) { targetStates = eventually->getChild()->check(modelCheck); allowedStates = storm::storage::BitVector(targetStates.size(), true); diff --git a/src/counterexamples/SMTMinimalCommandSetGenerator.h b/src/counterexamples/SMTMinimalCommandSetGenerator.h index dee532960..3d2c5be49 100644 --- a/src/counterexamples/SMTMinimalCommandSetGenerator.h +++ b/src/counterexamples/SMTMinimalCommandSetGenerator.h @@ -1773,37 +1773,37 @@ namespace storm { #endif } - static void computeCounterexample(storm::ir::Program program, std::string const& constantDefinitionString, storm::models::Mdp const& labeledMdp, std::shared_ptr> const & formulaPtr) { + static void computeCounterexample(storm::ir::Program program, std::string const& constantDefinitionString, storm::models::Mdp const& labeledMdp, std::shared_ptr> const & formulaPtr) { #ifdef STORM_HAVE_Z3 std::cout << std::endl << "Generating minimal label counterexample for formula " << formulaPtr->toString() << std::endl; // First, we need to check whether the current formula is an Until-Formula. - std::shared_ptr> probBoundFormula = std::dynamic_pointer_cast>(formulaPtr); + std::shared_ptr> probBoundFormula = std::dynamic_pointer_cast>(formulaPtr); 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."; } // Check whether we were given an upper bound, because counterexample generation is limited to this case. - if (probBoundFormula->getComparisonOperator() != storm::property::ComparisonType::LESS && probBoundFormula->getComparisonOperator() != storm::property::ComparisonType::LESS_EQUAL) { + 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::property::ComparisonType::LESS); + bool strictBound = !(probBoundFormula->getComparisonOperator() == storm::properties::ComparisonType::LESS); // 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> pathFormula = probBoundFormula->getPathFormula(); + std::shared_ptr> pathFormula = probBoundFormula->getPathFormula(); storm::storage::BitVector phiStates; storm::storage::BitVector psiStates; storm::modelchecker::prctl::SparseMdpPrctlModelChecker modelchecker(labeledMdp); - std::shared_ptr> untilFormula = std::dynamic_pointer_cast>(pathFormula); + std::shared_ptr> untilFormula = std::dynamic_pointer_cast>(pathFormula); if(untilFormula.get() != nullptr) { phiStates = untilFormula->getLeft()->check(modelchecker); psiStates = untilFormula->getRight()->check(modelchecker); - } if (std::dynamic_pointer_cast>(pathFormula).get() != nullptr) { + } if (std::dynamic_pointer_cast>(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> eventuallyFormula = std::dynamic_pointer_cast>(pathFormula); + std::shared_ptr> eventuallyFormula = std::dynamic_pointer_cast>(pathFormula); phiStates = storm::storage::BitVector(labeledMdp.getNumberOfStates(), true); psiStates = eventuallyFormula->getChild()->check(modelchecker); diff --git a/src/modelchecker/csl/AbstractModelChecker.h b/src/modelchecker/csl/AbstractModelChecker.h index 3a9ff9285..e2c68e740 100644 --- a/src/modelchecker/csl/AbstractModelChecker.h +++ b/src/modelchecker/csl/AbstractModelChecker.h @@ -10,7 +10,7 @@ #include #include "src/exceptions/InvalidPropertyException.h" -#include "src/formula/Csl.h" +#include "src/properties/Csl.h" #include "src/storage/BitVector.h" #include "src/models/AbstractModel.h" @@ -37,17 +37,17 @@ template class AbstractModelChecker : // A list of interfaces the model checker supports. Typically, for each of the interfaces, a check method needs to // be implemented that performs the corresponding check. - public virtual storm::property::csl::IApModelChecker, - public virtual storm::property::csl::IAndModelChecker, - public virtual storm::property::csl::IOrModelChecker, - public virtual storm::property::csl::INotModelChecker, - public virtual storm::property::csl::IUntilModelChecker, - public virtual storm::property::csl::IEventuallyModelChecker, - public virtual storm::property::csl::IGloballyModelChecker, - public virtual storm::property::csl::INextModelChecker, - public virtual storm::property::csl::ITimeBoundedUntilModelChecker, - public virtual storm::property::csl::ITimeBoundedEventuallyModelChecker, - public virtual storm::property::csl::IProbabilisticBoundOperatorModelChecker { + public virtual storm::properties::csl::IApModelChecker, + public virtual storm::properties::csl::IAndModelChecker, + public virtual storm::properties::csl::IOrModelChecker, + public virtual storm::properties::csl::INotModelChecker, + public virtual storm::properties::csl::IUntilModelChecker, + public virtual storm::properties::csl::IEventuallyModelChecker, + public virtual storm::properties::csl::IGloballyModelChecker, + public virtual storm::properties::csl::INextModelChecker, + public virtual storm::properties::csl::ITimeBoundedUntilModelChecker, + public virtual storm::properties::csl::ITimeBoundedEventuallyModelChecker, + public virtual storm::properties::csl::IProbabilisticBoundOperatorModelChecker { public: /*! @@ -112,7 +112,7 @@ public: * @param formula The formula to be checked. * @returns The set of states satisfying the formula represented by a bit vector. */ - storm::storage::BitVector checkAp(storm::property::csl::Ap const& formula) const { + storm::storage::BitVector checkAp(storm::properties::csl::Ap const& formula) const { if (formula.getAp() == "true") { return storm::storage::BitVector(model.getNumberOfStates(), true); } else if (formula.getAp() == "false") { @@ -133,7 +133,7 @@ public: * @param formula The formula to be checked. * @returns The set of states satisfying the formula represented by a bit vector. */ - storm::storage::BitVector checkAnd(storm::property::csl::And const& formula) const { + storm::storage::BitVector checkAnd(storm::properties::csl::And const& formula) const { storm::storage::BitVector result = formula.getLeft()->check(*this); storm::storage::BitVector right = formula.getRight()->check(*this); result &= right; @@ -146,7 +146,7 @@ public: * @param formula The formula to check. * @returns The set of states satisfying the formula represented by a bit vector. */ - storm::storage::BitVector checkOr(storm::property::csl::Or const& formula) const { + storm::storage::BitVector checkOr(storm::properties::csl::Or const& formula) const { storm::storage::BitVector result = formula.getLeft()->check(*this); storm::storage::BitVector right = formula.getRight()->check(*this); result |= right; @@ -159,7 +159,7 @@ public: * @param formula The formula to check. * @returns The set of states satisfying the formula represented by a bit vector. */ - storm::storage::BitVector checkNot(const storm::property::csl::Not& formula) const { + storm::storage::BitVector checkNot(const storm::properties::csl::Not& formula) const { storm::storage::BitVector result = formula.getChild()->check(*this); result.complement(); return result; @@ -172,7 +172,7 @@ public: * @param formula The formula to check. * @returns The set of states satisfying the formula represented by a bit vector. */ - virtual storm::storage::BitVector checkProbabilisticBoundOperator(storm::property::csl::ProbabilisticBoundOperator const& formula) const { + virtual storm::storage::BitVector checkProbabilisticBoundOperator(storm::properties::csl::ProbabilisticBoundOperator const& formula) const { // First, we need to compute the probability for satisfying the path formula for each state. std::vector quantitativeResult = formula.getChild()->check(*this, false); @@ -197,7 +197,7 @@ public: * @param minimumOperator True iff minimum probabilities/rewards are to be computed. * @returns The probabilities to satisfy the formula or the rewards accumulated by it, represented by a vector. */ - virtual std::vector checkMinMaxOperator(storm::property::csl::AbstractPathFormula const & formula, bool minimumOperator) const { + virtual std::vector checkMinMaxOperator(storm::properties::csl::AbstractPathFormula const & formula, bool minimumOperator) const { minimumOperatorStack.push(minimumOperator); std::vector result = formula.check(*this, false); minimumOperatorStack.pop(); @@ -211,7 +211,7 @@ public: * @param minimumOperator True iff minimum probabilities/rewards are to be computed. * @returns The set of states satisfying the formula represented by a bit vector. */ - virtual storm::storage::BitVector checkMinMaxOperator(storm::property::csl::AbstractStateFormula const & formula, bool minimumOperator) const { + virtual storm::storage::BitVector checkMinMaxOperator(storm::properties::csl::AbstractStateFormula const & formula, bool minimumOperator) const { minimumOperatorStack.push(minimumOperator); storm::storage::BitVector result = formula.check(*this); minimumOperatorStack.pop(); diff --git a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h index 71213f1b8..b3f1dfe40 100644 --- a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h +++ b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h @@ -54,10 +54,10 @@ public: * @param formula The formula to check. * @returns The set of states satisfying the formula represented by a bit vector. */ - virtual storm::storage::BitVector checkProbabilisticBoundOperator(storm::property::csl::ProbabilisticBoundOperator const& formula) const override{ + virtual storm::storage::BitVector checkProbabilisticBoundOperator(storm::properties::csl::ProbabilisticBoundOperator const& formula) const override{ // For P< and P<= the MA satisfies the formula iff the probability maximizing scheduler is used. // For P> and P>= " iff the probability minimizing " . - if(formula.getComparisonOperator() == storm::property::LESS || formula.getComparisonOperator() == storm::property::LESS_EQUAL) { + if(formula.getComparisonOperator() == storm::properties::LESS || formula.getComparisonOperator() == storm::properties::LESS_EQUAL) { this->minimumOperatorStack.push(false); } else { @@ -84,7 +84,7 @@ public: return result; } - std::vector checkUntil(storm::property::csl::Until const& formula, bool qualitative) const { + std::vector checkUntil(storm::properties::csl::Until const& formula, bool qualitative) const { // Test whether it is specified if the minimum or maximum probabilities are to be computed. if(this->minimumOperatorStack.empty()) { LOG4CPLUS_ERROR(logger, "Formula does not specify neither min nor max optimality, which is not meaningful over nondeterministic models."); @@ -100,11 +100,11 @@ public: return storm::modelchecker::prctl::SparseMdpPrctlModelChecker::computeUnboundedUntilProbabilities(min, this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getInitialStates(), leftStates, rightStates, nondeterministicLinearEquationSolver, qualitative); } - std::vector checkTimeBoundedUntil(storm::property::csl::TimeBoundedUntil const& formula, bool qualitative) const { + std::vector checkTimeBoundedUntil(storm::properties::csl::TimeBoundedUntil const& formula, bool qualitative) const { throw storm::exceptions::NotImplementedException() << "Model checking Until formulas on Markov automata is not yet implemented."; } - std::vector checkTimeBoundedEventually(storm::property::csl::TimeBoundedEventually const& formula, bool qualitative) const { + std::vector checkTimeBoundedEventually(storm::properties::csl::TimeBoundedEventually const& formula, bool qualitative) const { // Test whether it is specified if the minimum or maximum probabilities are to be computed. if(this->minimumOperatorStack.empty()) { LOG4CPLUS_ERROR(logger, "Formula does not specify neither min nor max optimality, which is not meaningful over nondeterministic models."); @@ -115,11 +115,11 @@ public: return this->checkTimeBoundedEventually(this->minimumOperatorStack.top(), goalStates, formula.getLowerBound(), formula.getUpperBound()); } - std::vector checkGlobally(storm::property::csl::Globally const& formula, bool qualitative) const { + std::vector checkGlobally(storm::properties::csl::Globally const& formula, bool qualitative) const { throw storm::exceptions::NotImplementedException() << "Model checking Globally formulas on Markov automata is not yet implemented."; } - std::vector checkEventually(storm::property::csl::Eventually const& formula, bool qualitative) const { + std::vector checkEventually(storm::properties::csl::Eventually const& formula, bool qualitative) const { // Test whether it is specified if the minimum or maximum probabilities are to be computed. if(this->minimumOperatorStack.empty()) { LOG4CPLUS_ERROR(logger, "Formula does not specify neither min nor max optimality, which is not meaningful over nondeterministic models."); @@ -130,7 +130,7 @@ public: return computeUnboundedUntilProbabilities(this->minimumOperatorStack.top(), storm::storage::BitVector(this->getModel().getNumberOfStates(), true), subFormulaStates, qualitative).first; } - std::vector checkNext(storm::property::csl::Next const& formula, bool qualitative) const { + std::vector checkNext(storm::properties::csl::Next const& formula, bool qualitative) const { throw storm::exceptions::NotImplementedException() << "Model checking Next formulas on Markov automata is not yet implemented."; } diff --git a/src/modelchecker/ltl/AbstractModelChecker.h b/src/modelchecker/ltl/AbstractModelChecker.h index 03284fed6..ce18dfb48 100644 --- a/src/modelchecker/ltl/AbstractModelChecker.h +++ b/src/modelchecker/ltl/AbstractModelChecker.h @@ -9,7 +9,7 @@ #define STORM_MODELCHECKER_LTL_ABSTRACTMODELCHECKER_H_ #include "src/exceptions/InvalidPropertyException.h" -#include "src/formula/Ltl.h" +#include "src/properties/Ltl.h" #include "src/storage/BitVector.h" #include "src/models/AbstractModel.h" @@ -36,16 +36,16 @@ template class AbstractModelChecker : // A list of interfaces the model checker supports. Typically, for each of the interfaces, a check method needs to // be implemented that performs the corresponding check. - public virtual storm::property::ltl::IApModelChecker, - public virtual storm::property::ltl::IAndModelChecker, - public virtual storm::property::ltl::IOrModelChecker, - public virtual storm::property::ltl::INotModelChecker, - public virtual storm::property::ltl::IUntilModelChecker, - public virtual storm::property::ltl::IEventuallyModelChecker, - public virtual storm::property::ltl::IGloballyModelChecker, - public virtual storm::property::ltl::INextModelChecker, - public virtual storm::property::ltl::IBoundedUntilModelChecker, - public virtual storm::property::ltl::IBoundedEventuallyModelChecker { + public virtual storm::properties::ltl::IApModelChecker, + public virtual storm::properties::ltl::IAndModelChecker, + public virtual storm::properties::ltl::IOrModelChecker, + public virtual storm::properties::ltl::INotModelChecker, + public virtual storm::properties::ltl::IUntilModelChecker, + public virtual storm::properties::ltl::IEventuallyModelChecker, + public virtual storm::properties::ltl::IGloballyModelChecker, + public virtual storm::properties::ltl::INextModelChecker, + public virtual storm::properties::ltl::IBoundedUntilModelChecker, + public virtual storm::properties::ltl::IBoundedEventuallyModelChecker { public: /*! @@ -110,7 +110,7 @@ public: * @param formula The formula to be checked. * @returns The set of states satisfying the formula represented by a bit vector. */ - virtual std::vector checkAp(storm::property::ltl::Ap const& formula) const = 0; + virtual std::vector checkAp(storm::properties::ltl::Ap const& formula) const = 0; /*! * Checks the given formula that is a logical "and" of two formulae. @@ -118,7 +118,7 @@ public: * @param formula The formula to be checked. * @returns The set of states satisfying the formula represented by a bit vector. */ - virtual std::vector checkAnd(storm::property::ltl::And const& formula) const = 0; + virtual std::vector checkAnd(storm::properties::ltl::And const& formula) const = 0; /*! * Checks the given formula that is a logical "or" of two formulae. @@ -126,7 +126,7 @@ public: * @param formula The formula to check. * @returns The set of states satisfying the formula represented by a bit vector. */ - virtual std::vector checkOr(storm::property::ltl::Or const& formula) const = 0; + virtual std::vector checkOr(storm::properties::ltl::Or const& formula) const = 0; /*! * Checks the given formula that is a logical "not" of a sub-formula. @@ -134,7 +134,7 @@ public: * @param formula The formula to check. * @returns The set of states satisfying the formula represented by a bit vector. */ - virtual std::vector checkNot(const storm::property::ltl::Not& formula) const = 0; + virtual std::vector checkNot(const storm::properties::ltl::Not& formula) const = 0; private: diff --git a/src/modelchecker/prctl/AbstractModelChecker.h b/src/modelchecker/prctl/AbstractModelChecker.h index f33cd8952..930c002db 100644 --- a/src/modelchecker/prctl/AbstractModelChecker.h +++ b/src/modelchecker/prctl/AbstractModelChecker.h @@ -19,7 +19,7 @@ namespace prctl { #include #include "src/exceptions/InvalidPropertyException.h" -#include "src/formula/Prctl.h" +#include "src/properties/Prctl.h" #include "src/storage/BitVector.h" #include "src/models/AbstractModel.h" #include "src/settings/Settings.h" @@ -47,21 +47,21 @@ template class AbstractModelChecker : // A list of interfaces the model checker supports. Typically, for each of the interfaces, a check method needs to // be implemented that performs the corresponding check. - public virtual storm::property::prctl::IApModelChecker, - public virtual storm::property::prctl::IAndModelChecker, - public virtual storm::property::prctl::IOrModelChecker, - public virtual storm::property::prctl::INotModelChecker, - public virtual storm::property::prctl::IUntilModelChecker, - public virtual storm::property::prctl::IEventuallyModelChecker, - public virtual storm::property::prctl::IGloballyModelChecker, - public virtual storm::property::prctl::INextModelChecker, - public virtual storm::property::prctl::IBoundedUntilModelChecker, - public virtual storm::property::prctl::IBoundedEventuallyModelChecker, - public virtual storm::property::prctl::IProbabilisticBoundOperatorModelChecker, - public virtual storm::property::prctl::IRewardBoundOperatorModelChecker, - public virtual storm::property::prctl::IReachabilityRewardModelChecker, - public virtual storm::property::prctl::ICumulativeRewardModelChecker, - public virtual storm::property::prctl::IInstantaneousRewardModelChecker { + public virtual storm::properties::prctl::IApModelChecker, + public virtual storm::properties::prctl::IAndModelChecker, + public virtual storm::properties::prctl::IOrModelChecker, + public virtual storm::properties::prctl::INotModelChecker, + public virtual storm::properties::prctl::IUntilModelChecker, + public virtual storm::properties::prctl::IEventuallyModelChecker, + public virtual storm::properties::prctl::IGloballyModelChecker, + public virtual storm::properties::prctl::INextModelChecker, + public virtual storm::properties::prctl::IBoundedUntilModelChecker, + public virtual storm::properties::prctl::IBoundedEventuallyModelChecker, + public virtual storm::properties::prctl::IProbabilisticBoundOperatorModelChecker, + public virtual storm::properties::prctl::IRewardBoundOperatorModelChecker, + public virtual storm::properties::prctl::IReachabilityRewardModelChecker, + public virtual storm::properties::prctl::ICumulativeRewardModelChecker, + public virtual storm::properties::prctl::IInstantaneousRewardModelChecker { public: /*! @@ -127,7 +127,7 @@ public: * @param formula The formula to be checked. * @return The set of states satisfying the formula represented by a bit vector. */ - storm::storage::BitVector checkAp(storm::property::prctl::Ap const& formula) const { + storm::storage::BitVector checkAp(storm::properties::prctl::Ap const& formula) const { if (formula.getAp() == "true") { return storm::storage::BitVector(model.getNumberOfStates(), true); } else if (formula.getAp() == "false") { @@ -148,7 +148,7 @@ public: * @param formula The formula to be checked. * @return The set of states satisfying the formula represented by a bit vector. */ - storm::storage::BitVector checkAnd(storm::property::prctl::And const& formula) const { + storm::storage::BitVector checkAnd(storm::properties::prctl::And const& formula) const { storm::storage::BitVector result = formula.getLeft()->check(*this); storm::storage::BitVector right = formula.getRight()->check(*this); result &= right; @@ -161,7 +161,7 @@ public: * @param formula The formula to check. * @return The set of states satisfying the formula represented by a bit vector. */ - storm::storage::BitVector checkOr(storm::property::prctl::Or const& formula) const { + storm::storage::BitVector checkOr(storm::properties::prctl::Or const& formula) const { storm::storage::BitVector result = formula.getLeft()->check(*this); storm::storage::BitVector right = formula.getRight()->check(*this); result |= right; @@ -174,7 +174,7 @@ public: * @param formula The formula to check. * @return The set of states satisfying the formula represented by a bit vector. */ - storm::storage::BitVector checkNot(const storm::property::prctl::Not& formula) const { + storm::storage::BitVector checkNot(const storm::properties::prctl::Not& formula) const { storm::storage::BitVector result = formula.getChild()->check(*this); result.complement(); return result; @@ -187,7 +187,7 @@ public: * @param formula The formula to check. * @return The set of states satisfying the formula represented by a bit vector. */ - virtual storm::storage::BitVector checkProbabilisticBoundOperator(storm::property::prctl::ProbabilisticBoundOperator const& formula) const { + virtual storm::storage::BitVector checkProbabilisticBoundOperator(storm::properties::prctl::ProbabilisticBoundOperator const& formula) const { // First, we need to compute the probability for satisfying the path formula for each state. std::vector quantitativeResult = formula.getChild()->check(*this, false); @@ -211,7 +211,7 @@ public: * @param formula The formula to check. * @return The set of states satisfying the formula represented by a bit vector. */ - virtual storm::storage::BitVector checkRewardBoundOperator(const storm::property::prctl::RewardBoundOperator& formula) const { + virtual storm::storage::BitVector checkRewardBoundOperator(const storm::properties::prctl::RewardBoundOperator& formula) const { // First, we need to compute the probability for satisfying the path formula for each state. std::vector quantitativeResult = formula.getChild()->check(*this, false); @@ -236,7 +236,7 @@ public: * @param optOperator True iff minimum probabilities are to be computed. * @returns The probabilities to satisfy the formula, represented by a vector. */ - virtual std::vector checkOptimizingOperator(storm::property::prctl::AbstractPathFormula const & formula, bool optOperator) const { + virtual std::vector checkOptimizingOperator(storm::properties::prctl::AbstractPathFormula const & formula, bool optOperator) const { minimumOperatorStack.push(optOperator); std::vector result = formula.check(*this, false); minimumOperatorStack.pop(); @@ -250,7 +250,7 @@ public: * @param optOperator True iff minimum rewards are to be computed. * @returns The the rewards accumulated by the formula, represented by a vector. */ - virtual std::vector checkOptimizingOperator(storm::property::prctl::AbstractRewardPathFormula const & formula, bool optOperator) const { + virtual std::vector checkOptimizingOperator(storm::properties::prctl::AbstractRewardPathFormula const & formula, bool optOperator) const { minimumOperatorStack.push(optOperator); std::vector result = formula.check(*this, false); minimumOperatorStack.pop(); @@ -264,7 +264,7 @@ public: * @param optOperator True iff minimum probabilities/rewards are to be computed. * @returns The set of states satisfying the formula represented by a bit vector. */ - virtual storm::storage::BitVector checkOptimizingOperator(storm::property::prctl::AbstractStateFormula const & formula, bool optOperator) const { + virtual storm::storage::BitVector checkOptimizingOperator(storm::properties::prctl::AbstractStateFormula const & formula, bool optOperator) const { minimumOperatorStack.push(optOperator); storm::storage::BitVector result = formula.check(*this); minimumOperatorStack.pop(); diff --git a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h index 74557fbea..e10fd77e4 100644 --- a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h +++ b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h @@ -71,7 +71,7 @@ public: * @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 checkBoundedUntil(storm::property::prctl::BoundedUntil const& formula, bool qualitative) const { + virtual std::vector checkBoundedUntil(storm::properties::prctl::BoundedUntil const& formula, bool qualitative) const { return this->checkBoundedUntil(formula.getLeft()->check(*this), formula.getRight()->check(*this), formula.getBound(), qualitative); } @@ -145,7 +145,7 @@ public: * @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 checkNext(storm::property::prctl::Next const& formula, bool qualitative) const { + virtual std::vector checkNext(storm::properties::prctl::Next const& formula, bool qualitative) const { // First, we need to compute the states that satisfy the child formula of the next-formula. storm::storage::BitVector nextStates = formula.getChild()->check(*this); @@ -174,7 +174,7 @@ public: * @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 checkBoundedEventually(storm::property::prctl::BoundedEventually const& formula, bool qualitative) const { + virtual std::vector checkBoundedEventually(storm::properties::prctl::BoundedEventually const& formula, bool qualitative) const { return this->checkBoundedUntil(storm::storage::BitVector(this->getModel().getNumberOfStates(), true), formula.getChild()->check(*this), formula.getBound(), qualitative); } @@ -189,9 +189,9 @@ public: * @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 checkEventually(storm::property::prctl::Eventually const& formula, bool qualitative) const { + virtual std::vector checkEventually(storm::properties::prctl::Eventually const& formula, bool qualitative) const { // Create equivalent temporary until formula and check it. - storm::property::prctl::Until temporaryUntilFormula(std::shared_ptr>(new storm::property::prctl::Ap("true")), formula.getChild()); + storm::properties::prctl::Until temporaryUntilFormula(std::shared_ptr>(new storm::properties::prctl::Ap("true")), formula.getChild()); return this->checkUntil(temporaryUntilFormula, qualitative); } @@ -206,9 +206,9 @@ public: * @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 checkGlobally(storm::property::prctl::Globally const& formula, bool qualitative) const { + virtual std::vector checkGlobally(storm::properties::prctl::Globally const& formula, bool qualitative) const { // Create "equivalent" (equivalent up to negation) temporary eventually formula and check it. - storm::property::prctl::Eventually temporaryEventuallyFormula(std::shared_ptr>(new storm::property::prctl::Not(formula.getChild()))); + storm::properties::prctl::Eventually temporaryEventuallyFormula(std::shared_ptr>(new storm::properties::prctl::Not(formula.getChild()))); std::vector result = this->checkEventually(temporaryEventuallyFormula, qualitative); // Now subtract the resulting vector from the constant one vector to obtain final result. @@ -228,7 +228,7 @@ public: * @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 checkUntil(storm::property::prctl::Until const& formula, bool qualitative) const { + virtual std::vector checkUntil(storm::properties::prctl::Until const& formula, bool qualitative) const { return this->checkUntil(formula.getLeft()->check(*this), formula.getRight()->check(*this), qualitative); } @@ -319,7 +319,7 @@ public: * @returns The reward values for the given formula for every state of the model associated with this model * checker. If the qualitative flag is set, exact values might not be computed. */ - virtual std::vector checkInstantaneousReward(storm::property::prctl::InstantaneousReward const& formula, bool qualitative) const { + virtual std::vector checkInstantaneousReward(storm::properties::prctl::InstantaneousReward const& formula, bool qualitative) const { // Only compute the result if the model has a state-based reward model. if (!this->getModel().hasStateRewards()) { LOG4CPLUS_ERROR(logger, "Missing (state-based) reward model for formula."); @@ -350,7 +350,7 @@ public: * @returns The reward values for the given formula for every state of the model associated with this model * checker. If the qualitative flag is set, exact values might not be computed. */ - virtual std::vector checkCumulativeReward(storm::property::prctl::CumulativeReward const& formula, bool qualitative) const { + virtual std::vector checkCumulativeReward(storm::properties::prctl::CumulativeReward const& formula, bool qualitative) const { // Only compute the result if the model has at least one reward model. if (!this->getModel().hasStateRewards() && !this->getModel().hasTransitionRewards()) { LOG4CPLUS_ERROR(logger, "Missing reward model for formula."); @@ -397,7 +397,7 @@ public: * @returns The reward values for the given formula for every state of the model associated with this model * checker. If the qualitative flag is set, exact values might not be computed. */ - virtual std::vector checkReachabilityReward(storm::property::prctl::ReachabilityReward const& formula, bool qualitative) const { + virtual std::vector checkReachabilityReward(storm::properties::prctl::ReachabilityReward const& formula, bool qualitative) const { // Only compute the result if the model has at least one reward model. if (!this->getModel().hasStateRewards() && !this->getModel().hasTransitionRewards()) { LOG4CPLUS_ERROR(logger, "Missing reward model for formula. Skipping formula"); @@ -491,7 +491,7 @@ public: * @param optOperator True iff minimum probabilities/rewards are to be computed. * @returns The probabilities to satisfy the formula or the rewards accumulated by it, represented by a vector. */ - virtual std::vector checkOptimizingOperator(storm::property::prctl::AbstractPathFormula const & formula, bool optOperator) const override { + virtual std::vector checkOptimizingOperator(storm::properties::prctl::AbstractPathFormula const & formula, bool optOperator) const override { LOG4CPLUS_WARN(logger, "Formula contains min/max operator, which is not meaningful over deterministic models."); @@ -509,7 +509,7 @@ public: * @param optOperator True iff minimum probabilities/rewards are to be computed. * @returns The set of states satisfying the formula represented by a bit vector. */ - virtual storm::storage::BitVector checkOptimizingOperator(storm::property::prctl::AbstractStateFormula const & formula, bool optOperator) const override { + virtual storm::storage::BitVector checkOptimizingOperator(storm::properties::prctl::AbstractStateFormula const & formula, bool optOperator) const override { LOG4CPLUS_WARN(logger, "Formula contains min/max operator, which is not meaningful over deterministic models."); diff --git a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h index 239a0a37f..4c193c4ed 100644 --- a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h +++ b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h @@ -75,11 +75,11 @@ namespace storm { * @param formula The formula to check. * @return The set of states satisfying the formula represented by a bit vector. */ - virtual storm::storage::BitVector checkProbabilisticBoundOperator(storm::property::prctl::ProbabilisticBoundOperator const& formula) const override { + virtual storm::storage::BitVector checkProbabilisticBoundOperator(storm::properties::prctl::ProbabilisticBoundOperator const& formula) const override { // For P< and P<= the MDP satisfies the formula iff the probability maximizing scheduler is used. // For P> and P>= " iff the probability minimizing " . - if(formula.getComparisonOperator() == storm::property::LESS || formula.getComparisonOperator() == storm::property::LESS_EQUAL) { + if(formula.getComparisonOperator() == storm::properties::LESS || formula.getComparisonOperator() == storm::properties::LESS_EQUAL) { this->minimumOperatorStack.push(false); } else { @@ -112,11 +112,11 @@ namespace storm { * @param formula The formula to check. * @return The set of states satisfying the formula represented by a bit vector. */ - virtual storm::storage::BitVector checkRewardBoundOperator(const storm::property::prctl::RewardBoundOperator& formula) const override { + virtual storm::storage::BitVector checkRewardBoundOperator(const storm::properties::prctl::RewardBoundOperator& formula) const override { // For R< and R<= the MDP satisfies the formula iff the reward maximizing scheduler is used. // For R> and R>= " iff the reward minimizing " . - if(formula.getComparisonOperator() == storm::property::LESS || formula.getComparisonOperator() == storm::property::LESS_EQUAL) { + if(formula.getComparisonOperator() == storm::properties::LESS || formula.getComparisonOperator() == storm::properties::LESS_EQUAL) { this->minimumOperatorStack.push(false); } else { @@ -218,7 +218,7 @@ namespace storm { * @return 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 checkBoundedUntil(storm::property::prctl::BoundedUntil const& formula, bool qualitative) const { + virtual std::vector checkBoundedUntil(storm::properties::prctl::BoundedUntil const& formula, bool qualitative) const { return checkBoundedUntil(formula.getLeft()->check(*this), formula.getRight()->check(*this), formula.getBound(), qualitative); } @@ -260,7 +260,7 @@ namespace storm { * @return 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 checkNext(const storm::property::prctl::Next& formula, bool qualitative) const { + virtual std::vector checkNext(const storm::properties::prctl::Next& formula, bool qualitative) const { return checkNext(formula.getChild()->check(*this), qualitative); } @@ -275,9 +275,9 @@ namespace storm { * @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 checkBoundedEventually(const storm::property::prctl::BoundedEventually& formula, bool qualitative) const { + virtual std::vector checkBoundedEventually(const storm::properties::prctl::BoundedEventually& formula, bool qualitative) const { // Create equivalent temporary bounded until formula and check it. - storm::property::prctl::BoundedUntil temporaryBoundedUntilFormula(std::shared_ptr>(new storm::property::prctl::Ap("true")), formula.getChild(), formula.getBound()); + storm::properties::prctl::BoundedUntil temporaryBoundedUntilFormula(std::shared_ptr>(new storm::properties::prctl::Ap("true")), formula.getChild(), formula.getBound()); return this->checkBoundedUntil(temporaryBoundedUntilFormula, qualitative); } @@ -292,9 +292,9 @@ namespace storm { * @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 checkEventually(const storm::property::prctl::Eventually& formula, bool qualitative) const { + virtual std::vector checkEventually(const storm::properties::prctl::Eventually& formula, bool qualitative) const { // Create equivalent temporary until formula and check it. - storm::property::prctl::Until temporaryUntilFormula(std::shared_ptr>(new storm::property::prctl::Ap("true")), formula.getChild()); + storm::properties::prctl::Until temporaryUntilFormula(std::shared_ptr>(new storm::properties::prctl::Ap("true")), formula.getChild()); return this->checkUntil(temporaryUntilFormula, qualitative); } @@ -309,9 +309,9 @@ namespace storm { * @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 checkGlobally(const storm::property::prctl::Globally& formula, bool qualitative) const { + virtual std::vector checkGlobally(const storm::properties::prctl::Globally& formula, bool qualitative) const { // Create "equivalent" temporary eventually formula and check it. - storm::property::prctl::Eventually temporaryEventuallyFormula(std::shared_ptr>(new storm::property::prctl::Not(formula.getChild()))); + storm::properties::prctl::Eventually temporaryEventuallyFormula(std::shared_ptr>(new storm::properties::prctl::Not(formula.getChild()))); std::vector result = this->checkEventually(temporaryEventuallyFormula, qualitative); // Now subtract the resulting vector from the constant one vector to obtain final result. @@ -333,7 +333,7 @@ namespace storm { * @return 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 checkUntil(const storm::property::prctl::Until& formula, bool qualitative) const { + virtual std::vector checkUntil(const storm::properties::prctl::Until& formula, bool qualitative) const { // First test if it is specified if the minimum or maximum probabilities are to be computed. if(this->minimumOperatorStack.empty()) { LOG4CPLUS_ERROR(logger, "Formula does not specify neither min nor max optimality, which is not meaningful over nondeterministic models."); @@ -438,7 +438,7 @@ namespace storm { * @return The reward values for the given formula for every state of the model associated with this model * checker. If the qualitative flag is set, exact values might not be computed. */ - virtual std::vector checkInstantaneousReward(const storm::property::prctl::InstantaneousReward& formula, bool qualitative) const { + virtual std::vector checkInstantaneousReward(const storm::properties::prctl::InstantaneousReward& formula, bool qualitative) const { // Only compute the result if the model has a state-based reward model. if (!this->getModel().hasStateRewards()) { LOG4CPLUS_ERROR(logger, "Missing (state-based) reward model for formula."); @@ -470,7 +470,7 @@ namespace storm { * @return The reward values for the given formula for every state of the model associated with this model * checker. If the qualitative flag is set, exact values might not be computed. */ - virtual std::vector checkCumulativeReward(const storm::property::prctl::CumulativeReward& formula, bool qualitative) const { + virtual std::vector checkCumulativeReward(const storm::properties::prctl::CumulativeReward& formula, bool qualitative) const { // Only compute the result if the model has at least one reward model. if (!this->getModel().hasStateRewards() && !this->getModel().hasTransitionRewards()) { LOG4CPLUS_ERROR(logger, "Missing reward model for formula."); @@ -518,7 +518,7 @@ namespace storm { * @return The reward values for the given formula for every state of the model associated with this model * checker. If the qualitative flag is set, exact values might not be computed. */ - virtual std::vector checkReachabilityReward(const storm::property::prctl::ReachabilityReward& formula, bool qualitative) const { + virtual std::vector checkReachabilityReward(const storm::properties::prctl::ReachabilityReward& formula, bool qualitative) const { // First test whether it is specified if the minimum or maximum probabilities are to be computed. if(this->minimumOperatorStack.empty()) { LOG4CPLUS_ERROR(logger, "Formula does not specify neither min nor max optimality, which is not meaningful over nondeterministic models."); diff --git a/src/parser/CslParser.cpp b/src/parser/CslParser.cpp index 1f2f66361..1739ebecd 100644 --- a/src/parser/CslParser.cpp +++ b/src/parser/CslParser.cpp @@ -10,12 +10,12 @@ #include "src/utility/constants.h" // The action class headers. -#include "src/formula/actions/AbstractAction.h" -#include "src/formula/actions/BoundAction.h" -#include "src/formula/actions/InvertAction.h" -#include "src/formula/actions/FormulaAction.h" -#include "src/formula/actions/RangeAction.h" -#include "src/formula/actions/SortAction.h" +#include "src/properties/actions/AbstractAction.h" +#include "src/properties/actions/BoundAction.h" +#include "src/properties/actions/InvertAction.h" +#include "src/properties/actions/FormulaAction.h" +#include "src/properties/actions/RangeAction.h" +#include "src/properties/actions/SortAction.h" // If the parser fails due to ill-formed data, this exception is thrown. #include "src/exceptions/WrongFormatException.h" @@ -41,7 +41,7 @@ typedef std::string::const_iterator BaseIteratorType; typedef boost::spirit::classic::position_iterator2 PositionIteratorType; namespace qi = boost::spirit::qi; namespace phoenix = boost::phoenix; -namespace csl = storm::property::csl; +namespace csl = storm::properties::csl; namespace storm { namespace parser { @@ -52,13 +52,13 @@ struct CslParser::CslGrammar : qi::grammar> *(qi::alnum | qi::char_('_'))]; comparisonType = ( - (qi::lit(">="))[qi::_val = storm::property::GREATER_EQUAL] | - (qi::lit(">"))[qi::_val = storm::property::GREATER] | - (qi::lit("<="))[qi::_val = storm::property::LESS_EQUAL] | - (qi::lit("<"))[qi::_val = storm::property::LESS]); + (qi::lit(">="))[qi::_val = storm::properties::GREATER_EQUAL] | + (qi::lit(">"))[qi::_val = storm::properties::GREATER] | + (qi::lit("<="))[qi::_val = storm::properties::LESS_EQUAL] | + (qi::lit("<"))[qi::_val = storm::properties::LESS]); sortingCategory = ( - (qi::lit("index"))[qi::_val = storm::property::action::SortAction::INDEX] | - (qi::lit("value"))[qi::_val = storm::property::action::SortAction::VALUE] + (qi::lit("index"))[qi::_val = storm::properties::action::SortAction::INDEX] | + (qi::lit("value"))[qi::_val = storm::properties::action::SortAction::VALUE] ); //Comment: Empty line or line starting with "//" comment = (qi::lit("//") >> *(qi::char_))[qi::_val = nullptr]; @@ -136,43 +136,43 @@ struct CslParser::CslGrammar : qi::grammar> qi::lit("min") >> qi::lit("=") > qi::lit("?") >> pathFormula)[qi::_val = - MAKE(csl::CslFilter, qi::_1, storm::property::MINIMIZE)] | + MAKE(csl::CslFilter, qi::_1, storm::properties::MINIMIZE)] | (qi::lit("P") >> qi::lit("max") >> qi::lit("=") > qi::lit("?") >> pathFormula)[qi::_val = - MAKE(csl::CslFilter, qi::_1, storm::property::MAXIMIZE)] | + MAKE(csl::CslFilter, qi::_1, storm::properties::MAXIMIZE)] | (qi::lit("P") >> qi::lit("=") > qi::lit("?") >> pathFormula)[qi::_val = MAKE(csl::CslFilter, qi::_1)]; probabilisticNoBoundOperator.name("probabilistic no bound operator"); steadyStateNoBoundOperator = (qi::lit("S") >> qi::lit("=") > qi::lit("?") >> stateFormula )[qi::_val = - MAKE(csl::CslFilter, qi::_1, storm::property::UNDEFINED, true)]; + MAKE(csl::CslFilter, qi::_1, storm::properties::UNDEFINED, true)]; steadyStateNoBoundOperator.name("steady state no bound operator"); // This block defines rules for parsing filter actions. boundAction = (qi::lit("bound") > qi::lit("(") >> comparisonType >> qi::lit(",") >> qi::double_ >> qi::lit(")"))[qi::_val = - MAKE(storm::property::action::BoundAction ,qi::_1, qi::_2)]; + MAKE(storm::properties::action::BoundAction ,qi::_1, qi::_2)]; boundAction.name("bound action"); - invertAction = qi::lit("invert")[qi::_val = MAKE(storm::property::action::InvertAction, )]; + invertAction = qi::lit("invert")[qi::_val = MAKE(storm::properties::action::InvertAction, )]; invertAction.name("invert action"); formulaAction = (qi::lit("formula") > qi::lit("(") >> stateFormula >> qi::lit(")"))[qi::_val = - MAKE(storm::property::action::FormulaAction, qi::_1)]; + MAKE(storm::properties::action::FormulaAction, qi::_1)]; formulaAction.name("formula action"); rangeAction = ( (qi::lit("range") >> qi::lit("(") >> qi::uint_ >> qi::lit(",") > qi::uint_ >> qi::lit(")"))[qi::_val = - MAKE(storm::property::action::RangeAction, qi::_1, qi::_2)] | + MAKE(storm::properties::action::RangeAction, qi::_1, qi::_2)] | (qi::lit("range") >> qi::lit("(") >> qi::uint_ >> qi::lit(")"))[qi::_val = - MAKE(storm::property::action::RangeAction, qi::_1, qi::_1 + 1)] + MAKE(storm::properties::action::RangeAction, qi::_1, qi::_1 + 1)] ); rangeAction.name("range action"); sortAction = ( (qi::lit("sort") >> qi::lit("(") >> sortingCategory >> qi::lit(")"))[qi::_val = - MAKE(storm::property::action::SortAction, qi::_1)] | + MAKE(storm::properties::action::SortAction, qi::_1)] | (qi::lit("sort") >> qi::lit("(") >> sortingCategory >> qi::lit(", ") >> (qi::lit("ascending") | qi::lit("asc")) > qi::lit(")"))[qi::_val = - MAKE(storm::property::action::SortAction, qi::_1, true)] | + MAKE(storm::properties::action::SortAction, qi::_1, true)] | (qi::lit("sort") >> qi::lit("(") >> sortingCategory >> qi::lit(", ") >> (qi::lit("descending") | qi::lit("desc")) > qi::lit(")"))[qi::_val = - MAKE(storm::property::action::SortAction, qi::_1, false)] + MAKE(storm::properties::action::SortAction, qi::_1, false)] ); sortAction.name("sort action"); @@ -182,9 +182,9 @@ struct CslParser::CslGrammar : qi::grammar> qi::lit("[") >> +abstractAction >> qi::lit("]") >> qi::lit("(") >> formula >> qi::lit(")"))[qi::_val = MAKE(csl::CslFilter, qi::_2, qi::_1)] | (qi::lit("filter") >> qi::lit("[") >> qi::lit("max") > +abstractAction >> qi::lit("]") >> qi::lit("(") >> formula >> qi::lit(")"))[qi::_val = - MAKE(csl::CslFilter, qi::_2, qi::_1, storm::property::MAXIMIZE)] | + MAKE(csl::CslFilter, qi::_2, qi::_1, storm::properties::MAXIMIZE)] | (qi::lit("filter") >> qi::lit("[") >> qi::lit("min") > +abstractAction >> qi::lit("]") >> qi::lit("(") >> formula >> qi::lit(")"))[qi::_val = - MAKE(csl::CslFilter, qi::_2, qi::_1, storm::property::MINIMIZE)] | + MAKE(csl::CslFilter, qi::_2, qi::_1, storm::properties::MINIMIZE)] | (noBoundOperator)[qi::_val = qi::_1] | (formula)[qi::_val = @@ -204,12 +204,12 @@ struct CslParser::CslGrammar : qi::grammar>(), Skipper> probabilisticNoBoundOperator; qi::rule>(), Skipper> steadyStateNoBoundOperator; - qi::rule>(), Skipper> abstractAction; - qi::rule>(), Skipper> boundAction; - qi::rule>(), Skipper> invertAction; - qi::rule>(), Skipper> formulaAction; - qi::rule>(), Skipper> rangeAction; - qi::rule>(), Skipper> sortAction; + qi::rule>(), Skipper> abstractAction; + qi::rule>(), Skipper> boundAction; + qi::rule>(), Skipper> invertAction; + qi::rule>(), Skipper> formulaAction; + qi::rule>(), Skipper> rangeAction; + qi::rule>(), Skipper> sortAction; qi::rule>(), Skipper> formula; qi::rule>(), Skipper> comment; @@ -229,17 +229,17 @@ struct CslParser::CslGrammar : qi::grammar>(), Skipper> eventually; qi::rule>(), Skipper> next; qi::rule>(), Skipper> globally; - qi::rule>(), qi::locals< std::shared_ptr>>, Skipper> timeBoundedUntil; - qi::rule>(), qi::locals< std::shared_ptr>>, Skipper> until; + qi::rule>(), qi::locals< std::shared_ptr>>, Skipper> timeBoundedUntil; + qi::rule>(), qi::locals< std::shared_ptr>>, Skipper> until; qi::rule freeIdentifierName; - qi::rule comparisonType; - qi::rule::SortingCategory(), Skipper> sortingCategory; + qi::rule comparisonType; + qi::rule::SortingCategory(), Skipper> sortingCategory; }; -std::shared_ptr> CslParser::parseCslFormula(std::string formulaString) { +std::shared_ptr> CslParser::parseCslFormula(std::string formulaString) { // Prepare iterators to input. BaseIteratorType stringIteratorBegin = formulaString.begin(); BaseIteratorType stringIteratorEnd = formulaString.end(); @@ -248,7 +248,7 @@ std::shared_ptr> CslParser::parseCslForm // Prepare resulting intermediate representation of input. - std::shared_ptr> result_pointer(nullptr); + std::shared_ptr> result_pointer(nullptr); CslGrammar grammar; diff --git a/src/parser/CslParser.h b/src/parser/CslParser.h index ccb5b90c3..78b42c844 100644 --- a/src/parser/CslParser.h +++ b/src/parser/CslParser.h @@ -8,8 +8,8 @@ #ifndef STORM_PARSER_CSLPARSER_H_ #define STORM_PARSER_CSLPARSER_H_ -#include "src/formula/Csl.h" -#include "src/formula/csl/CslFilter.h" +#include "src/properties/Csl.h" +#include "src/properties/csl/CslFilter.h" #include namespace storm { @@ -25,7 +25,7 @@ public: /*! * Reads a CSL formula from its string representation and parses it into a formula tree, consisting of - * classes in the namespace storm::property. + * classes in the namespace storm::properties. * * If the string could not be parsed successfully, it will throw a wrongFormatException. * @@ -33,7 +33,7 @@ public: * @throw wrongFormatException If the input could not be parsed successfully. * @return A CslFilter maintaining the parsed formula. */ - static std::shared_ptr> parseCslFormula(std::string formulaString); + static std::shared_ptr> parseCslFormula(std::string formulaString); private: diff --git a/src/parser/LtlFileParser.cpp b/src/parser/LtlFileParser.cpp index e056a99ee..c7b056183 100644 --- a/src/parser/LtlFileParser.cpp +++ b/src/parser/LtlFileParser.cpp @@ -15,7 +15,7 @@ namespace storm { namespace parser { -std::list>> LtlFileParser::parseLtlFile(std::string filename) { +std::list>> LtlFileParser::parseLtlFile(std::string filename) { // Open file std::ifstream inputFileStream(filename, std::ios::in); @@ -24,7 +24,7 @@ std::list>> LtlFileParse throw storm::exceptions::FileIoException() << message << filename; } - std::list>> result; + std::list>> result; while(!inputFileStream.eof()) { std::string line; diff --git a/src/parser/LtlFileParser.h b/src/parser/LtlFileParser.h index f21210b7d..4caa67d8f 100644 --- a/src/parser/LtlFileParser.h +++ b/src/parser/LtlFileParser.h @@ -8,8 +8,8 @@ #ifndef LTLFILEPARSER_H_ #define LTLFILEPARSER_H_ -#include "formula/Ltl.h" -#include "src/formula/ltl/LtlFilter.h" +#include "properties/Ltl.h" +#include "src/properties/ltl/LtlFilter.h" #include @@ -25,7 +25,7 @@ public: * @param filename Name and path to the file in which the formula strings can be found. * @return The list of parsed formulas. */ - static std::list>> parseLtlFile(std::string filename); + static std::list>> parseLtlFile(std::string filename); }; } //namespace parser diff --git a/src/parser/LtlParser.cpp b/src/parser/LtlParser.cpp index bb87ab79c..df4d28c9e 100644 --- a/src/parser/LtlParser.cpp +++ b/src/parser/LtlParser.cpp @@ -11,11 +11,11 @@ #include "src/utility/constants.h" // The action class headers. -#include "src/formula/actions/AbstractAction.h" -#include "src/formula/actions/BoundAction.h" -#include "src/formula/actions/InvertAction.h" -#include "src/formula/actions/RangeAction.h" -#include "src/formula/actions/SortAction.h" +#include "src/properties/actions/AbstractAction.h" +#include "src/properties/actions/BoundAction.h" +#include "src/properties/actions/InvertAction.h" +#include "src/properties/actions/RangeAction.h" +#include "src/properties/actions/SortAction.h" // If the parser fails due to ill-formed data, this exception is thrown. #include "src/exceptions/WrongFormatException.h" @@ -41,7 +41,7 @@ typedef std::string::const_iterator BaseIteratorType; typedef boost::spirit::classic::position_iterator2 PositionIteratorType; namespace qi = boost::spirit::qi; namespace phoenix = boost::phoenix; -namespace ltl = storm::property::ltl; +namespace ltl = storm::properties::ltl; namespace storm { @@ -49,18 +49,18 @@ namespace storm { namespace parser { template -struct LtlParser::LtlGrammar : qi::grammar>(), Skipper > { +struct LtlParser::LtlGrammar : qi::grammar>(), Skipper > { LtlGrammar() : LtlGrammar::base_type(start) { //This block contains helper rules that may be used several times freeIdentifierName = qi::lexeme[qi::alpha >> *(qi::alnum | qi::char_('_'))]; comparisonType = ( - (qi::lit(">="))[qi::_val = storm::property::GREATER_EQUAL] | - (qi::lit(">"))[qi::_val = storm::property::GREATER] | - (qi::lit("<="))[qi::_val = storm::property::LESS_EQUAL] | - (qi::lit("<"))[qi::_val = storm::property::LESS]); + (qi::lit(">="))[qi::_val = storm::properties::GREATER_EQUAL] | + (qi::lit(">"))[qi::_val = storm::properties::GREATER] | + (qi::lit("<="))[qi::_val = storm::properties::LESS_EQUAL] | + (qi::lit("<"))[qi::_val = storm::properties::LESS]); sortingCategory = ( - (qi::lit("index"))[qi::_val = storm::property::action::SortAction::INDEX] | - (qi::lit("value"))[qi::_val = storm::property::action::SortAction::VALUE] + (qi::lit("index"))[qi::_val = storm::properties::action::SortAction::INDEX] | + (qi::lit("value"))[qi::_val = storm::properties::action::SortAction::VALUE] ); // Comment: Empty line or line starting with "//" comment = (qi::lit("//") >> *(qi::char_))[qi::_val = nullptr]; @@ -110,27 +110,27 @@ struct LtlParser::LtlGrammar : qi::grammar qi::lit("(") >> comparisonType >> qi::lit(",") >> qi::double_ >> qi::lit(")"))[qi::_val = - MAKE(storm::property::action::BoundAction ,qi::_1, qi::_2)]; + MAKE(storm::properties::action::BoundAction ,qi::_1, qi::_2)]; boundAction.name("bound action"); - invertAction = qi::lit("invert")[qi::_val = MAKE(storm::property::action::InvertAction, )]; + invertAction = qi::lit("invert")[qi::_val = MAKE(storm::properties::action::InvertAction, )]; invertAction.name("invert action"); rangeAction = ( (qi::lit("range") >> qi::lit("(") >> qi::uint_ >> qi::lit(",") > qi::uint_ >> qi::lit(")"))[qi::_val = - MAKE(storm::property::action::RangeAction, qi::_1, qi::_2)] | + MAKE(storm::properties::action::RangeAction, qi::_1, qi::_2)] | (qi::lit("range") >> qi::lit("(") >> qi::uint_ >> qi::lit(")"))[qi::_val = - MAKE(storm::property::action::RangeAction, qi::_1, qi::_1 + 1)] + MAKE(storm::properties::action::RangeAction, qi::_1, qi::_1 + 1)] ); rangeAction.name("range action"); sortAction = ( (qi::lit("sort") >> qi::lit("(") >> sortingCategory >> qi::lit(")"))[qi::_val = - MAKE(storm::property::action::SortAction, qi::_1)] | + MAKE(storm::properties::action::SortAction, qi::_1)] | (qi::lit("sort") >> qi::lit("(") >> sortingCategory >> qi::lit(", ") >> (qi::lit("ascending") | qi::lit("asc")) > qi::lit(")"))[qi::_val = - MAKE(storm::property::action::SortAction, qi::_1, true)] | + MAKE(storm::properties::action::SortAction, qi::_1, true)] | (qi::lit("sort") >> qi::lit("(") >> sortingCategory >> qi::lit(", ") >> (qi::lit("descending") | qi::lit("desc")) > qi::lit(")"))[qi::_val = - MAKE(storm::property::action::SortAction, qi::_1, false)] + MAKE(storm::properties::action::SortAction, qi::_1, false)] ); sortAction.name("sort action"); @@ -140,9 +140,9 @@ struct LtlParser::LtlGrammar : qi::grammar> qi::lit("[") >> +abstractAction >> qi::lit("]") > qi::lit("(") >> formula >> qi::lit(")"))[qi::_val = MAKE(ltl::LtlFilter, qi::_2, qi::_1)] | (qi::lit("filter") >> qi::lit("[") >> qi::lit("max") > +abstractAction >> qi::lit("]") >> qi::lit("(") >> formula >> qi::lit(")"))[qi::_val = - MAKE(ltl::LtlFilter, qi::_2, qi::_1, storm::property::MAXIMIZE)] | + MAKE(ltl::LtlFilter, qi::_2, qi::_1, storm::properties::MAXIMIZE)] | (qi::lit("filter") >> qi::lit("[") >> qi::lit("min") > +abstractAction >> qi::lit("]") >> qi::lit("(") >> formula >> qi::lit(")"))[qi::_val = - MAKE(ltl::LtlFilter, qi::_2, qi::_1, storm::property::MINIMIZE)] | + MAKE(ltl::LtlFilter, qi::_2, qi::_1, storm::properties::MINIMIZE)] | (formula)[qi::_val = MAKE(ltl::LtlFilter, qi::_1)]; filter.name("LTL formula filter"); @@ -151,39 +151,39 @@ struct LtlParser::LtlGrammar : qi::grammar>(), Skipper> start; - qi::rule>(), Skipper> filter; - - qi::rule>(), Skipper> abstractAction; - qi::rule>(), Skipper> boundAction; - qi::rule>(), Skipper> invertAction; - qi::rule>(), Skipper> rangeAction; - qi::rule>(), Skipper> sortAction; - - qi::rule>(), Skipper> comment; - qi::rule>(), Skipper> formula; - qi::rule>(), Skipper> atomicLtlFormula; - - qi::rule>(), Skipper> andFormula; - qi::rule>(), Skipper> untilFormula; - qi::rule>(), Skipper> atomicProposition; - qi::rule>(), Skipper> orFormula; - qi::rule>(), Skipper> notFormula; - - qi::rule>(), Skipper> pathFormula; - qi::rule>(), Skipper> boundedEventually; - qi::rule>(), Skipper> eventually; - qi::rule>(), Skipper> globally; - qi::rule>(), Skipper> next; - qi::rule>(), qi::locals< std::shared_ptr>>, Skipper> boundedUntil; - qi::rule>(), qi::locals< std::shared_ptr>>, Skipper> until; + qi::rule>(), Skipper> start; + qi::rule>(), Skipper> filter; + + qi::rule>(), Skipper> abstractAction; + qi::rule>(), Skipper> boundAction; + qi::rule>(), Skipper> invertAction; + qi::rule>(), Skipper> rangeAction; + qi::rule>(), Skipper> sortAction; + + qi::rule>(), Skipper> comment; + qi::rule>(), Skipper> formula; + qi::rule>(), Skipper> atomicLtlFormula; + + qi::rule>(), Skipper> andFormula; + qi::rule>(), Skipper> untilFormula; + qi::rule>(), Skipper> atomicProposition; + qi::rule>(), Skipper> orFormula; + qi::rule>(), Skipper> notFormula; + + qi::rule>(), Skipper> pathFormula; + qi::rule>(), Skipper> boundedEventually; + qi::rule>(), Skipper> eventually; + qi::rule>(), Skipper> globally; + qi::rule>(), Skipper> next; + qi::rule>(), qi::locals< std::shared_ptr>>, Skipper> boundedUntil; + qi::rule>(), qi::locals< std::shared_ptr>>, Skipper> until; qi::rule freeIdentifierName; - qi::rule comparisonType; - qi::rule::SortingCategory(), Skipper> sortingCategory; + qi::rule comparisonType; + qi::rule::SortingCategory(), Skipper> sortingCategory; }; -std::shared_ptr> LtlParser::parseLtlFormula(std::string formulaString) { +std::shared_ptr> LtlParser::parseLtlFormula(std::string formulaString) { // Prepare iterators to input. BaseIteratorType stringIteratorBegin = formulaString.begin(); BaseIteratorType stringIteratorEnd = formulaString.end(); @@ -192,7 +192,7 @@ std::shared_ptr> LtlParser::parseLtlForm // Prepare resulting intermediate representation of input. - std::shared_ptr> result_pointer(nullptr); + std::shared_ptr> result_pointer(nullptr); LtlGrammar grammar; diff --git a/src/parser/LtlParser.h b/src/parser/LtlParser.h index ebbad77c0..dac3a63ec 100644 --- a/src/parser/LtlParser.h +++ b/src/parser/LtlParser.h @@ -8,8 +8,8 @@ #ifndef STORM_PARSER_LTLPARSER_H_ #define STORM_PARSER_LTLPARSER_H_ -#include "src/formula/Ltl.h" -#include "src/formula/ltl/LtlFilter.h" +#include "src/properties/Ltl.h" +#include "src/properties/ltl/LtlFilter.h" namespace storm { namespace parser { @@ -24,7 +24,7 @@ public: /*! * Reads a LTL formula from its string representation and parses it into a formula tree, consisting of - * classes in the namespace storm::property. + * classes in the namespace storm::properties. * * If the string could not be parsed successfully, it will throw a wrongFormatException. * @@ -32,7 +32,7 @@ public: * @throw wrongFormatException If the input could not be parsed successfully. * @return A LtlFilter maintaining the parsed formula. */ - static std::shared_ptr> parseLtlFormula(std::string formulaString); + static std::shared_ptr> parseLtlFormula(std::string formulaString); private: diff --git a/src/parser/PrctlFileParser.cpp b/src/parser/PrctlFileParser.cpp index 323d5984b..64abd2b15 100644 --- a/src/parser/PrctlFileParser.cpp +++ b/src/parser/PrctlFileParser.cpp @@ -14,7 +14,7 @@ namespace storm { namespace parser { -std::list>> PrctlFileParser::parsePrctlFile(std::string filename) { +std::list>> PrctlFileParser::parsePrctlFile(std::string filename) { // Open file std::ifstream inputFileStream; inputFileStream.open(filename, std::ios::in); @@ -24,12 +24,12 @@ std::list>> PrctlFil throw storm::exceptions::FileIoException() << message << filename; } - std::list>> result; + std::list>> result; std::string line; //The while loop reads the input file line by line while (std::getline(inputFileStream, line)) { - std::shared_ptr> formula = PrctlParser::parsePrctlFormula(line); + std::shared_ptr> formula = PrctlParser::parsePrctlFormula(line); if (formula != nullptr) { //lines containing comments will be skipped. LOG4CPLUS_INFO(logger, "Parsed formula \"" + line + "\" into \"" + formula->toString() + "\""); diff --git a/src/parser/PrctlFileParser.h b/src/parser/PrctlFileParser.h index 615e219c1..dbf458fbf 100644 --- a/src/parser/PrctlFileParser.h +++ b/src/parser/PrctlFileParser.h @@ -8,8 +8,8 @@ #ifndef STORM_PARSER_PRCTLFILEPARSER_H_ #define STORM_PARSER_PRCTLFILEPARSER_H_ -#include "formula/Prctl.h" -#include "src/formula/prctl/PrctlFilter.h" +#include "properties/Prctl.h" +#include "src/properties/prctl/PrctlFilter.h" #include @@ -25,7 +25,7 @@ public: * @param filename Name and path to the file in which the formula strings can be found. * @return The list of parsed formulas */ - static std::list>> parsePrctlFile(std::string filename); + static std::list>> parsePrctlFile(std::string filename); }; diff --git a/src/parser/PrctlParser.cpp b/src/parser/PrctlParser.cpp index bd9590980..41a9ab701 100644 --- a/src/parser/PrctlParser.cpp +++ b/src/parser/PrctlParser.cpp @@ -3,12 +3,12 @@ #include "src/utility/constants.h" // The action class headers. -#include "src/formula/actions/AbstractAction.h" -#include "src/formula/actions/BoundAction.h" -#include "src/formula/actions/InvertAction.h" -#include "src/formula/actions/FormulaAction.h" -#include "src/formula/actions/RangeAction.h" -#include "src/formula/actions/SortAction.h" +#include "src/properties/actions/AbstractAction.h" +#include "src/properties/actions/BoundAction.h" +#include "src/properties/actions/InvertAction.h" +#include "src/properties/actions/FormulaAction.h" +#include "src/properties/actions/RangeAction.h" +#include "src/properties/actions/SortAction.h" // If the parser fails due to ill-formed data, this exception is thrown. #include "src/exceptions/WrongFormatException.h" @@ -35,7 +35,7 @@ typedef std::string::const_iterator BaseIteratorType; typedef boost::spirit::classic::position_iterator2 PositionIteratorType; namespace qi = boost::spirit::qi; namespace phoenix = boost::phoenix; -namespace prctl = storm::property::prctl; +namespace prctl = storm::properties::prctl; namespace storm { @@ -43,18 +43,18 @@ namespace storm { namespace parser { template -struct PrctlParser::PrctlGrammar : qi::grammar>(), Skipper > { +struct PrctlParser::PrctlGrammar : qi::grammar>(), Skipper > { PrctlGrammar() : PrctlGrammar::base_type(start) { // This block contains helper rules that may be used several times freeIdentifierName = qi::lexeme[qi::alpha >> *(qi::alnum | qi::char_('_'))]; comparisonType = ( - (qi::lit(">="))[qi::_val = storm::property::GREATER_EQUAL] | - (qi::lit(">"))[qi::_val = storm::property::GREATER] | - (qi::lit("<="))[qi::_val = storm::property::LESS_EQUAL] | - (qi::lit("<"))[qi::_val = storm::property::LESS]); + (qi::lit(">="))[qi::_val = storm::properties::GREATER_EQUAL] | + (qi::lit(">"))[qi::_val = storm::properties::GREATER] | + (qi::lit("<="))[qi::_val = storm::properties::LESS_EQUAL] | + (qi::lit("<"))[qi::_val = storm::properties::LESS]); sortingCategory = ( - (qi::lit("index"))[qi::_val = storm::property::action::SortAction::INDEX] | - (qi::lit("value"))[qi::_val = storm::property::action::SortAction::VALUE] + (qi::lit("index"))[qi::_val = storm::properties::action::SortAction::INDEX] | + (qi::lit("value"))[qi::_val = storm::properties::action::SortAction::VALUE] ); // Comment: Empty line or line starting with "//" comment = (qi::lit("//") >> *(qi::char_))[qi::_val = nullptr]; @@ -133,9 +133,9 @@ struct PrctlParser::PrctlGrammar : qi::grammar> qi::lit("min") >> qi::lit("=") > qi::lit("?") >> pathFormula )[qi::_val = - MAKE(prctl::PrctlFilter, qi::_1, storm::property::MINIMIZE)] | + MAKE(prctl::PrctlFilter, qi::_1, storm::properties::MINIMIZE)] | (qi::lit("P") >> qi::lit("max") >> qi::lit("=") > qi::lit("?") >> pathFormula )[qi::_val = - MAKE(prctl::PrctlFilter, qi::_1, storm::property::MAXIMIZE)] | + MAKE(prctl::PrctlFilter, qi::_1, storm::properties::MAXIMIZE)] | (qi::lit("P") >> qi::lit("=") > qi::lit("?") >> pathFormula )[qi::_val = MAKE(prctl::PrctlFilter, qi::_1)] ); @@ -143,9 +143,9 @@ struct PrctlParser::PrctlGrammar : qi::grammar> qi::lit("min") >> qi::lit("=") > qi::lit("?") >> rewardPathFormula )[qi::_val = - MAKE(prctl::PrctlFilter, qi::_1, storm::property::MINIMIZE)] | + MAKE(prctl::PrctlFilter, qi::_1, storm::properties::MINIMIZE)] | (qi::lit("R") >> qi::lit("max") >> qi::lit("=") > qi::lit("?") >> rewardPathFormula )[qi::_val = - MAKE(prctl::PrctlFilter, qi::_1, storm::property::MAXIMIZE)] | + MAKE(prctl::PrctlFilter, qi::_1, storm::properties::MAXIMIZE)] | (qi::lit("R") >> qi::lit("=") > qi::lit("?") >> rewardPathFormula )[qi::_val = MAKE(prctl::PrctlFilter, qi::_1)] @@ -155,31 +155,31 @@ struct PrctlParser::PrctlGrammar : qi::grammar qi::lit("(") >> comparisonType >> qi::lit(",") >> qi::double_ >> qi::lit(")"))[qi::_val = - MAKE(storm::property::action::BoundAction ,qi::_1, qi::_2)]; + MAKE(storm::properties::action::BoundAction ,qi::_1, qi::_2)]; boundAction.name("bound action"); - invertAction = qi::lit("invert")[qi::_val = MAKE(storm::property::action::InvertAction, )]; + invertAction = qi::lit("invert")[qi::_val = MAKE(storm::properties::action::InvertAction, )]; invertAction.name("invert action"); formulaAction = (qi::lit("formula") > qi::lit("(") >> stateFormula >> qi::lit(")"))[qi::_val = - MAKE(storm::property::action::FormulaAction, qi::_1)]; + MAKE(storm::properties::action::FormulaAction, qi::_1)]; formulaAction.name("formula action"); rangeAction = ( (qi::lit("range") >> qi::lit("(") >> qi::uint_ >> qi::lit(",") > qi::uint_ >> qi::lit(")"))[qi::_val = - MAKE(storm::property::action::RangeAction, qi::_1, qi::_2)] | + MAKE(storm::properties::action::RangeAction, qi::_1, qi::_2)] | (qi::lit("range") >> qi::lit("(") >> qi::uint_ >> qi::lit(")"))[qi::_val = - MAKE(storm::property::action::RangeAction, qi::_1, qi::_1 + 1)] + MAKE(storm::properties::action::RangeAction, qi::_1, qi::_1 + 1)] ); rangeAction.name("range action"); sortAction = ( (qi::lit("sort") >> qi::lit("(") >> sortingCategory >> qi::lit(")"))[qi::_val = - MAKE(storm::property::action::SortAction, qi::_1)] | + MAKE(storm::properties::action::SortAction, qi::_1)] | (qi::lit("sort") >> qi::lit("(") >> sortingCategory >> qi::lit(", ") >> (qi::lit("ascending") | qi::lit("asc")) > qi::lit(")"))[qi::_val = - MAKE(storm::property::action::SortAction, qi::_1, true)] | + MAKE(storm::properties::action::SortAction, qi::_1, true)] | (qi::lit("sort") >> qi::lit("(") >> sortingCategory >> qi::lit(", ") >> (qi::lit("descending") | qi::lit("desc")) > qi::lit(")"))[qi::_val = - MAKE(storm::property::action::SortAction, qi::_1, false)] + MAKE(storm::properties::action::SortAction, qi::_1, false)] ); sortAction.name("sort action"); @@ -189,9 +189,9 @@ struct PrctlParser::PrctlGrammar : qi::grammar> qi::lit("[") >> +abstractAction >> qi::lit("]") > qi::lit("(") >> formula >> qi::lit(")"))[qi::_val = MAKE(prctl::PrctlFilter, qi::_2, qi::_1)] | (qi::lit("filter") >> qi::lit("[") >> qi::lit("max") > +abstractAction >> qi::lit("]") >> qi::lit("(") >> formula >> qi::lit(")"))[qi::_val = - MAKE(prctl::PrctlFilter, qi::_2, qi::_1, storm::property::MAXIMIZE)] | + MAKE(prctl::PrctlFilter, qi::_2, qi::_1, storm::properties::MAXIMIZE)] | (qi::lit("filter") >> qi::lit("[") >> qi::lit("min") > +abstractAction >> qi::lit("]") >> qi::lit("(") >> formula >> qi::lit(")"))[qi::_val = - MAKE(prctl::PrctlFilter, qi::_2, qi::_1, storm::property::MINIMIZE)] | + MAKE(prctl::PrctlFilter, qi::_2, qi::_1, storm::properties::MINIMIZE)] | (noBoundOperator)[qi::_val = qi::_1] | (formula)[qi::_val = @@ -203,54 +203,54 @@ struct PrctlParser::PrctlGrammar : qi::grammar>(), Skipper> start; - qi::rule>(), Skipper> filter; + qi::rule>(), Skipper> start; + qi::rule>(), Skipper> filter; - qi::rule>(), Skipper> noBoundOperator; - qi::rule>(), Skipper> probabilisticNoBoundOperator; - qi::rule>(), Skipper> rewardNoBoundOperator; + qi::rule>(), Skipper> noBoundOperator; + qi::rule>(), Skipper> probabilisticNoBoundOperator; + qi::rule>(), Skipper> rewardNoBoundOperator; - qi::rule>(), Skipper> abstractAction; - qi::rule>(), Skipper> boundAction; - qi::rule>(), Skipper> invertAction; - qi::rule>(), Skipper> formulaAction; - qi::rule>(), Skipper> rangeAction; - qi::rule>(), Skipper> sortAction; + qi::rule>(), Skipper> abstractAction; + qi::rule>(), Skipper> boundAction; + qi::rule>(), Skipper> invertAction; + qi::rule>(), Skipper> formulaAction; + qi::rule>(), Skipper> rangeAction; + qi::rule>(), Skipper> sortAction; - qi::rule>(), Skipper> formula; - qi::rule>(), Skipper> comment; + qi::rule>(), Skipper> formula; + qi::rule>(), Skipper> comment; - qi::rule>(), Skipper> stateFormula; - qi::rule>(), Skipper> atomicStateFormula; + qi::rule>(), Skipper> stateFormula; + qi::rule>(), Skipper> atomicStateFormula; - qi::rule>(), Skipper> andFormula; - qi::rule>(), Skipper> atomicProposition; - qi::rule>(), Skipper> orFormula; - qi::rule>(), Skipper> notFormula; - qi::rule>(), Skipper> probabilisticBoundOperator; - qi::rule>(), Skipper> rewardBoundOperator; + qi::rule>(), Skipper> andFormula; + qi::rule>(), Skipper> atomicProposition; + qi::rule>(), Skipper> orFormula; + qi::rule>(), Skipper> notFormula; + qi::rule>(), Skipper> probabilisticBoundOperator; + qi::rule>(), Skipper> rewardBoundOperator; - qi::rule>(), Skipper> pathFormula; - qi::rule>(), Skipper> boundedEventually; - qi::rule>(), Skipper> eventually; - qi::rule>(), Skipper> next; - qi::rule>(), Skipper> globally; - qi::rule>(), qi::locals< std::shared_ptr>>, Skipper> boundedUntil; - qi::rule>(), qi::locals< std::shared_ptr>>, Skipper> until; + qi::rule>(), Skipper> pathFormula; + qi::rule>(), Skipper> boundedEventually; + qi::rule>(), Skipper> eventually; + qi::rule>(), Skipper> next; + qi::rule>(), Skipper> globally; + qi::rule>(), qi::locals< std::shared_ptr>>, Skipper> boundedUntil; + qi::rule>(), qi::locals< std::shared_ptr>>, Skipper> until; - qi::rule>(), Skipper> rewardPathFormula; - qi::rule>(), Skipper> cumulativeReward; - qi::rule>(), Skipper> reachabilityReward; - qi::rule>(), Skipper> instantaneousReward; - qi::rule>(), Skipper> steadyStateReward; + qi::rule>(), Skipper> rewardPathFormula; + qi::rule>(), Skipper> cumulativeReward; + qi::rule>(), Skipper> reachabilityReward; + qi::rule>(), Skipper> instantaneousReward; + qi::rule>(), Skipper> steadyStateReward; qi::rule freeIdentifierName; - qi::rule comparisonType; - qi::rule::SortingCategory(), Skipper> sortingCategory; + qi::rule comparisonType; + qi::rule::SortingCategory(), Skipper> sortingCategory; }; -std::shared_ptr> PrctlParser::parsePrctlFormula(std::string formulaString) { +std::shared_ptr> PrctlParser::parsePrctlFormula(std::string formulaString) { // Prepare iterators to input. BaseIteratorType stringIteratorBegin = formulaString.begin(); BaseIteratorType stringIteratorEnd = formulaString.end(); @@ -259,7 +259,7 @@ std::shared_ptr> PrctlParser::parseP // Prepare resulting intermediate representation of input. - std::shared_ptr> result_pointer(nullptr); + std::shared_ptr> result_pointer(nullptr); PrctlGrammar grammar; diff --git a/src/parser/PrctlParser.h b/src/parser/PrctlParser.h index 75e13c117..c1fc798bb 100644 --- a/src/parser/PrctlParser.h +++ b/src/parser/PrctlParser.h @@ -1,8 +1,8 @@ #ifndef STORM_PARSER_PRCTLPARSER_H_ #define STORM_PARSER_PRCTLPARSER_H_ -#include "src/formula/Prctl.h" -#include "src/formula/prctl/PrctlFilter.h" +#include "src/properties/Prctl.h" +#include "src/properties/prctl/PrctlFilter.h" namespace storm { namespace parser { @@ -17,7 +17,7 @@ public: /*! * Reads a Prctl formula from its string representation and parses it into a formula tree, consisting of - * classes in the namespace storm::property. + * classes in the namespace storm::properties. * * If the string could not be parsed successfully, it will throw a wrongFormatException. * @@ -25,7 +25,7 @@ public: * @throw wrongFormatException If the input could not be parsed successfully * @return A PrctlFilter maintaining the parsed formula. If the line just contained a comment a nullptr will be returned instead. */ - static std::shared_ptr> parsePrctlFormula(std::string formulaString); + static std::shared_ptr> parsePrctlFormula(std::string formulaString); private: diff --git a/src/formula/AbstractFilter.h b/src/properties/AbstractFilter.h similarity index 97% rename from src/formula/AbstractFilter.h rename to src/properties/AbstractFilter.h index 3824817fe..5c8899a09 100644 --- a/src/formula/AbstractFilter.h +++ b/src/properties/AbstractFilter.h @@ -10,11 +10,11 @@ #include #include -#include "src/formula/AbstractFormula.h" -#include "src/formula/actions/AbstractAction.h" +#include "src/properties/AbstractFormula.h" +#include "src/properties/actions/AbstractAction.h" namespace storm { -namespace property { +namespace properties { /*! * This enum contains value indicating which kind of scheduler is to be used @@ -215,7 +215,7 @@ protected: OptimizingOperator opt; }; -} //namespace property +} //namespace properties } //namespace storm diff --git a/src/formula/AbstractFormula.h b/src/properties/AbstractFormula.h similarity index 92% rename from src/formula/AbstractFormula.h rename to src/properties/AbstractFormula.h index 9b009f208..9c55dc370 100644 --- a/src/formula/AbstractFormula.h +++ b/src/properties/AbstractFormula.h @@ -12,21 +12,19 @@ #include namespace storm { -namespace property { +namespace properties { template class AbstractFormula; -} //namespace property +} //namespace properties } //namespace storm namespace storm { -namespace property { - -// do properties +namespace properties { /*! * This is the abstract base class for every formula class in every logic. * * There are currently three implemented logics Ltl, Csl and Pctl. - * The implementation of these logics can be found in the namespaces storm::property:: + * The implementation of these logics can be found in the namespaces storm::properties:: * where is one of ltl, pctl and csl. * * @note While formula classes do have copy constructors using a copy constructor @@ -66,7 +64,7 @@ public: } }; -} // namespace property +} // namespace properties } // namespace storm #endif /* STORM_FORMULA_ABSTRACTFORMULA_H_ */ diff --git a/src/formula/ComparisonType.h b/src/properties/ComparisonType.h similarity index 95% rename from src/formula/ComparisonType.h rename to src/properties/ComparisonType.h index bb6ea82ee..c0eb598bc 100644 --- a/src/formula/ComparisonType.h +++ b/src/properties/ComparisonType.h @@ -9,7 +9,7 @@ #define STORM_FORMULA_COMPARISONTYPE_H_ namespace storm { -namespace property { +namespace properties { /*! * An enum representing the greater- and less-than operators in both diff --git a/src/formula/Csl.h b/src/properties/Csl.h similarity index 100% rename from src/formula/Csl.h rename to src/properties/Csl.h diff --git a/src/formula/Ltl.h b/src/properties/Ltl.h similarity index 100% rename from src/formula/Ltl.h rename to src/properties/Ltl.h diff --git a/src/formula/Prctl.h b/src/properties/Prctl.h similarity index 100% rename from src/formula/Prctl.h rename to src/properties/Prctl.h diff --git a/src/formula/actions/AbstractAction.h b/src/properties/actions/AbstractAction.h similarity index 99% rename from src/formula/actions/AbstractAction.h rename to src/properties/actions/AbstractAction.h index 0912751fd..b0f17bb28 100644 --- a/src/formula/actions/AbstractAction.h +++ b/src/properties/actions/AbstractAction.h @@ -16,7 +16,7 @@ #include "src/modelchecker/ltl/AbstractModelChecker.h" namespace storm { -namespace property { +namespace properties { namespace action { /*! @@ -141,7 +141,7 @@ public: }; } //namespace action -} //namespace property +} //namespace properties } //namespace storm diff --git a/src/formula/actions/BoundAction.h b/src/properties/actions/BoundAction.h similarity index 90% rename from src/formula/actions/BoundAction.h rename to src/properties/actions/BoundAction.h index 1603c3308..7dadc4c37 100644 --- a/src/formula/actions/BoundAction.h +++ b/src/properties/actions/BoundAction.h @@ -8,12 +8,12 @@ #ifndef STORM_FORMULA_ACTION_BOUNDACTION_H_ #define STORM_FORMULA_ACTION_BOUNDACTION_H_ -#include "src/formula/actions/AbstractAction.h" -#include "src/formula/ComparisonType.h" +#include "src/properties/actions/AbstractAction.h" +#include "src/properties/ComparisonType.h" #include "src/exceptions/InvalidArgumentException.h" namespace storm { -namespace property { +namespace properties { namespace action { /*! @@ -34,7 +34,7 @@ public: * Constructs an empty BoundAction. * The bound is set to >= 0. Thus, all states will be selected by the action. */ - BoundAction() : comparisonOperator(storm::property::GREATER_EQUAL), bound(0) { + BoundAction() : comparisonOperator(storm::properties::GREATER_EQUAL), bound(0) { //Intentionally left empty. } @@ -44,7 +44,7 @@ public: * @param comparisonOperator The operator used to make the comparison between the bound and the modelchecking values for each state. * @param bound The bound to compare the modelchecking values against. */ - BoundAction(storm::property::ComparisonType comparisonOperator, T bound) : comparisonOperator(comparisonOperator), bound(bound) { + BoundAction(storm::properties::ComparisonType comparisonOperator, T bound) : comparisonOperator(comparisonOperator), bound(bound) { //Intentionally left empty. } @@ -148,16 +148,16 @@ private: for(uint_fast64_t i = 0; i < result.pathResult.size(); i++) { if(result.selection[i]) { switch(comparisonOperator) { - case storm::property::GREATER_EQUAL: + case storm::properties::GREATER_EQUAL: out.set(i, result.pathResult[i] >= bound); break; - case storm::property::GREATER: + case storm::properties::GREATER: out.set(i, result.pathResult[i] > bound); break; - case storm::property::LESS_EQUAL: + case storm::properties::LESS_EQUAL: out.set(i, result.pathResult[i] <= bound); break; - case storm::property::LESS: + case storm::properties::LESS: out.set(i, result.pathResult[i] < bound); break; default: @@ -173,16 +173,16 @@ private: for(uint_fast64_t i = 0; i < result.stateMap.size(); i++) { if(result.selection[i]) { switch(comparisonOperator) { - case storm::property::GREATER_EQUAL: + case storm::properties::GREATER_EQUAL: out.set(i, result.stateResult[i] >= bound); break; - case storm::property::GREATER: + case storm::properties::GREATER: out.set(i, result.stateResult[i] > bound); break; - case storm::property::LESS_EQUAL: + case storm::properties::LESS_EQUAL: out.set(i, result.stateResult[i] <= bound); break; - case storm::property::LESS: + case storm::properties::LESS: out.set(i, result.stateResult[i] < bound); break; default: @@ -198,7 +198,7 @@ private: } // The operator used to make the comparison between the bound and the modelchecking values for each state at time of evaluation. - storm::property::ComparisonType comparisonOperator; + storm::properties::ComparisonType comparisonOperator; // The bound to compare the modelchecking values against during evaluation. T bound; diff --git a/src/formula/actions/FormulaAction.h b/src/properties/actions/FormulaAction.h similarity index 84% rename from src/formula/actions/FormulaAction.h rename to src/properties/actions/FormulaAction.h index 5028253fe..744c76038 100644 --- a/src/formula/actions/FormulaAction.h +++ b/src/properties/actions/FormulaAction.h @@ -8,15 +8,15 @@ #ifndef STORM_FORMULA_ACTION_FORMULAACTION_H_ #define STORM_FORMULA_ACTION_FORMULAACTION_H_ -#include "src/formula/actions/AbstractAction.h" -#include "src/formula/prctl/AbstractStateFormula.h" -#include "src/formula/csl/AbstractStateFormula.h" +#include "src/properties/actions/AbstractAction.h" +#include "src/properties/prctl/AbstractStateFormula.h" +#include "src/properties/csl/AbstractStateFormula.h" #include namespace storm { -namespace property { +namespace properties { namespace action { /*! @@ -48,7 +48,7 @@ public: * * @param prctlFormula The Prctl state formula used to filter the selection during evaluation. */ - FormulaAction(std::shared_ptr> const & prctlFormula) : prctlFormula(prctlFormula), cslFormula(nullptr) { + FormulaAction(std::shared_ptr> const & prctlFormula) : prctlFormula(prctlFormula), cslFormula(nullptr) { //Intentionally left empty. } @@ -57,7 +57,7 @@ public: * * @param cslFormula The Csl state formula used to filter the selection during evaluation. */ - FormulaAction(std::shared_ptr> const & cslFormula) : prctlFormula(nullptr), cslFormula(cslFormula) { + FormulaAction(std::shared_ptr> const & cslFormula) : prctlFormula(nullptr), cslFormula(cslFormula) { //Intentionally left empty. } @@ -126,15 +126,15 @@ public: private: // The Prctl state formula used during evaluation. - std::shared_ptr> prctlFormula; + std::shared_ptr> prctlFormula; // The Csl state formula used during evaluation. - std::shared_ptr> cslFormula; + std::shared_ptr> cslFormula; }; } //namespace action -} //namespace property +} //namespace properties } //namespace storm #endif /* STORM_FORMULA_ACTION_FORMULAACTION_H_ */ diff --git a/src/formula/actions/InvertAction.h b/src/properties/actions/InvertAction.h similarity index 97% rename from src/formula/actions/InvertAction.h rename to src/properties/actions/InvertAction.h index 7084d52e2..69c7baa23 100644 --- a/src/formula/actions/InvertAction.h +++ b/src/properties/actions/InvertAction.h @@ -8,10 +8,10 @@ #ifndef STORM_FORMULA_ACTION_INVERTACTION_H_ #define STORM_FORMULA_ACTION_INVERTACTION_H_ -#include "src/formula/actions/AbstractAction.h" +#include "src/properties/actions/AbstractAction.h" namespace storm { -namespace property { +namespace properties { namespace action { /*! @@ -103,7 +103,7 @@ private: }; } //namespace action -} //namespace property +} //namespace properties } //namespace storm diff --git a/src/formula/actions/RangeAction.h b/src/properties/actions/RangeAction.h similarity index 98% rename from src/formula/actions/RangeAction.h rename to src/properties/actions/RangeAction.h index 8136715b2..5647deca4 100644 --- a/src/formula/actions/RangeAction.h +++ b/src/properties/actions/RangeAction.h @@ -8,10 +8,10 @@ #ifndef STORM_FORMULA_ACTION_RANGEACTION_H_ #define STORM_FORMULA_ACTION_RANGEACTION_H_ -#include "src/formula/actions/AbstractAction.h" +#include "src/properties/actions/AbstractAction.h" namespace storm { -namespace property { +namespace properties { namespace action { /*! @@ -149,7 +149,7 @@ private: }; } //namespace action -} //namespace property +} //namespace properties } //namespace storm #endif /* STORM_FORMULA_ACTION_RANGEACTION_H_ */ diff --git a/src/formula/actions/SortAction.h b/src/properties/actions/SortAction.h similarity index 98% rename from src/formula/actions/SortAction.h rename to src/properties/actions/SortAction.h index 289426f6f..7498eb7bf 100644 --- a/src/formula/actions/SortAction.h +++ b/src/properties/actions/SortAction.h @@ -8,11 +8,11 @@ #ifndef STORM_FORMULA_ACTION_SORTACTION_H_ #define STORM_FORMULA_ACTION_SORTACTION_H_ -#include "src/formula/actions/AbstractAction.h" +#include "src/properties/actions/AbstractAction.h" #include namespace storm { -namespace property { +namespace properties { namespace action { /*! @@ -225,7 +225,7 @@ private: }; } //namespace action -} //namespace property +} //namespace properties } //namespace storm #endif /* STORM_FORMULA_ACTION_SORTACTION_H_ */ diff --git a/src/formula/csl/AbstractCslFormula.h b/src/properties/csl/AbstractCslFormula.h similarity index 73% rename from src/formula/csl/AbstractCslFormula.h rename to src/properties/csl/AbstractCslFormula.h index 360b5d411..4f8694340 100644 --- a/src/formula/csl/AbstractCslFormula.h +++ b/src/properties/csl/AbstractCslFormula.h @@ -8,10 +8,10 @@ #ifndef STORM_FORMULA_CSL_ABSTRACTCSLFORMULA_H_ #define STORM_FORMULA_CSL_ABSTRACTCSLFORMULA_H_ -#include "src/formula/AbstractFormula.h" +#include "src/properties/AbstractFormula.h" namespace storm { -namespace property { +namespace properties { namespace csl { // Forward declarations. @@ -25,7 +25,7 @@ template class Until; } namespace storm { -namespace property { +namespace properties { namespace csl { /*! @@ -37,7 +37,7 @@ namespace csl { * the original and the copy. */ template -class AbstractCslFormula : public virtual storm::property::AbstractFormula{ +class AbstractCslFormula : public virtual storm::properties::AbstractFormula{ public: /*! @@ -59,23 +59,23 @@ public: bool isProbEventuallyAP() const { // Test if a probabilistic bound operator is at the root. - if(dynamic_cast const *>(this) == nullptr) { + if(dynamic_cast const *>(this) == nullptr) { return false; } - auto probFormula = dynamic_cast const *>(this); + auto probFormula = dynamic_cast const *>(this); // Check if the direct subformula of the probabilistic bound operator is an eventually or until formula. - if(std::dynamic_pointer_cast>(probFormula->getChild()).get() != nullptr) { + if(std::dynamic_pointer_cast>(probFormula->getChild()).get() != nullptr) { // Get the subformula and check if its subformulas are propositional. - auto eventuallyFormula = std::dynamic_pointer_cast>(probFormula->getChild()); + auto eventuallyFormula = std::dynamic_pointer_cast>(probFormula->getChild()); return eventuallyFormula->getChild()->isPropositional(); } - else if(std::dynamic_pointer_cast>(probFormula->getChild()).get() != nullptr) { + else if(std::dynamic_pointer_cast>(probFormula->getChild()).get() != nullptr) { // Get the subformula and check if its subformulas are propositional. - auto untilFormula = std::dynamic_pointer_cast>(probFormula->getChild()); + auto untilFormula = std::dynamic_pointer_cast>(probFormula->getChild()); return untilFormula->getLeft()->isPropositional() && untilFormula->getRight()->isPropositional(); } @@ -84,6 +84,6 @@ public: }; } /* namespace csl */ -} /* namespace property */ +} /* namespace properties */ } /* namespace storm */ #endif /* STORM_FORMULA_CSL_ABSTRACTCSLFORMULA_H_ */ diff --git a/src/formula/csl/AbstractPathFormula.h b/src/properties/csl/AbstractPathFormula.h similarity index 90% rename from src/formula/csl/AbstractPathFormula.h rename to src/properties/csl/AbstractPathFormula.h index a8d415616..e7aa31e08 100644 --- a/src/formula/csl/AbstractPathFormula.h +++ b/src/properties/csl/AbstractPathFormula.h @@ -8,7 +8,7 @@ #ifndef STORM_FORMULA_CSL_ABSTRACTPATHFORMULA_H_ #define STORM_FORMULA_CSL_ABSTRACTPATHFORMULA_H_ -#include "src/formula/csl/AbstractCslFormula.h" +#include "src/properties/csl/AbstractCslFormula.h" #include "src/modelchecker/csl/ForwardDeclarations.h" #include @@ -16,7 +16,7 @@ #include namespace storm { -namespace property { +namespace properties { namespace csl { /*! @@ -26,7 +26,7 @@ namespace csl { * The result of a modelchecking process on such a formula is a vector representing the satisfaction probabilities for each state of the model. */ template -class AbstractPathFormula : public virtual storm::property::csl::AbstractCslFormula { +class AbstractPathFormula : public virtual storm::properties::csl::AbstractCslFormula { public: @@ -63,7 +63,7 @@ public: }; } //namespace csl -} //namespace property +} //namespace properties } //namespace storm #endif /* STORM_FORMULA_CSL_ABSTRACTPATHFORMULA_H_ */ diff --git a/src/formula/csl/AbstractStateFormula.h b/src/properties/csl/AbstractStateFormula.h similarity index 89% rename from src/formula/csl/AbstractStateFormula.h rename to src/properties/csl/AbstractStateFormula.h index dec96eb45..9c48a1007 100644 --- a/src/formula/csl/AbstractStateFormula.h +++ b/src/properties/csl/AbstractStateFormula.h @@ -8,19 +8,19 @@ #ifndef STORM_FORMULA_CSL_ABSTRACTSTATEFORMULA_H_ #define STORM_FORMULA_CSL_ABSTRACTSTATEFORMULA_H_ -#include "src/formula/csl/AbstractCslFormula.h" +#include "src/properties/csl/AbstractCslFormula.h" #include "src/storage/BitVector.h" #include "src/modelchecker/csl/ForwardDeclarations.h" namespace storm { -namespace property { +namespace properties { namespace csl { /*! * Abstract base class for Csl state formulas. */ template -class AbstractStateFormula : public storm::property::csl::AbstractCslFormula { +class AbstractStateFormula : public storm::properties::csl::AbstractCslFormula { public: @@ -57,7 +57,7 @@ public: }; } //namespace csl -} //namespace property +} //namespace properties } //namespace storm diff --git a/src/formula/csl/And.h b/src/properties/csl/And.h similarity index 98% rename from src/formula/csl/And.h rename to src/properties/csl/And.h index a5ebaffb2..f9aaa1a85 100644 --- a/src/formula/csl/And.h +++ b/src/properties/csl/And.h @@ -8,12 +8,12 @@ #ifndef STORM_FORMULA_CSL_AND_H_ #define STORM_FORMULA_CSL_AND_H_ -#include "src/formula/csl/AbstractStateFormula.h" +#include "src/properties/csl/AbstractStateFormula.h" #include "src/modelchecker/csl/ForwardDeclarations.h" #include namespace storm { -namespace property { +namespace properties { namespace csl { // Forward declaration for the interface class. @@ -209,7 +209,7 @@ private: } //namespace csl -} //namespace property +} //namespace properties } //namespace storm diff --git a/src/formula/csl/Ap.h b/src/properties/csl/Ap.h similarity index 97% rename from src/formula/csl/Ap.h rename to src/properties/csl/Ap.h index 8ab7600fe..9dc5f2392 100644 --- a/src/formula/csl/Ap.h +++ b/src/properties/csl/Ap.h @@ -8,11 +8,11 @@ #ifndef STORM_FORMULA_CSL_AP_H_ #define STORM_FORMULA_CSL_AP_H_ -#include "src/formula/csl/AbstractStateFormula.h" +#include "src/properties/csl/AbstractStateFormula.h" #include "src/modelchecker/csl/ForwardDeclarations.h" namespace storm { -namespace property { +namespace properties { namespace csl { // Forward declaration for the interface class. @@ -134,7 +134,7 @@ private: } //namespace abstract -} //namespace property +} //namespace properties } //namespace storm diff --git a/src/formula/csl/CslFilter.h b/src/properties/csl/CslFilter.h similarity index 97% rename from src/formula/csl/CslFilter.h rename to src/properties/csl/CslFilter.h index 4d92829e5..560a65faf 100644 --- a/src/formula/csl/CslFilter.h +++ b/src/properties/csl/CslFilter.h @@ -8,16 +8,16 @@ #ifndef STORM_FORMULA_PRCTL_CSLFILTER_H_ #define STORM_FORMULA_PRCTL_CSLFILTER_H_ -#include "src/formula/AbstractFilter.h" -#include "src/formula/csl/AbstractCslFormula.h" -#include "src/formula/csl/AbstractPathFormula.h" -#include "src/formula/csl/AbstractStateFormula.h" +#include "src/properties/AbstractFilter.h" +#include "src/properties/csl/AbstractCslFormula.h" +#include "src/properties/csl/AbstractPathFormula.h" +#include "src/properties/csl/AbstractStateFormula.h" #include "src/modelchecker/csl/AbstractModelChecker.h" -#include "src/formula/actions/AbstractAction.h" +#include "src/properties/actions/AbstractAction.h" namespace storm { -namespace property { +namespace properties { namespace csl { /*! @@ -27,10 +27,10 @@ namespace csl { * Additionally it maintains a list of filter actions that are used to further manipulate the modelchecking results and prepare them for output. */ template -class CslFilter : public storm::property::AbstractFilter { +class CslFilter : public storm::properties::AbstractFilter { // Convenience typedef to make the code more readable. - typedef typename storm::property::action::AbstractAction::Result Result; + typedef typename storm::properties::action::AbstractAction::Result Result; public: @@ -408,7 +408,7 @@ private: }; } //namespace csl -} //namespace property +} //namespace properties } //namespace storm #endif /* STORM_FORMULA_CSL_CSLFILTER_H_ */ diff --git a/src/formula/csl/Eventually.h b/src/properties/csl/Eventually.h similarity index 96% rename from src/formula/csl/Eventually.h rename to src/properties/csl/Eventually.h index 6c27dfa75..b156280aa 100644 --- a/src/formula/csl/Eventually.h +++ b/src/properties/csl/Eventually.h @@ -8,12 +8,12 @@ #ifndef STORM_FORMULA_CSL_EVENTUALLY_H_ #define STORM_FORMULA_CSL_EVENTUALLY_H_ -#include "src/formula/csl/AbstractPathFormula.h" -#include "src/formula/csl/AbstractStateFormula.h" +#include "src/properties/csl/AbstractPathFormula.h" +#include "src/properties/csl/AbstractStateFormula.h" #include "src/modelchecker/csl/ForwardDeclarations.h" namespace storm { -namespace property { +namespace properties { namespace csl { // Forward declaration for the interface class. @@ -164,7 +164,7 @@ private: }; } //namespace csl -} //namespace property +} //namespace properties } //namespace storm #endif /* STORM_FORMULA_CSL_EVENTUALLY_H_ */ diff --git a/src/formula/csl/Globally.h b/src/properties/csl/Globally.h similarity index 96% rename from src/formula/csl/Globally.h rename to src/properties/csl/Globally.h index 421d9e354..52f25ba24 100644 --- a/src/formula/csl/Globally.h +++ b/src/properties/csl/Globally.h @@ -8,12 +8,12 @@ #ifndef STORM_FORMULA_CSL_GLOBALLY_H_ #define STORM_FORMULA_CSL_GLOBALLY_H_ -#include "src/formula/csl/AbstractPathFormula.h" -#include "src/formula/csl/AbstractStateFormula.h" +#include "src/properties/csl/AbstractPathFormula.h" +#include "src/properties/csl/AbstractStateFormula.h" #include "src/modelchecker/csl/ForwardDeclarations.h" namespace storm { -namespace property { +namespace properties { namespace csl { // Forward declaration for the interface class. @@ -163,7 +163,7 @@ private: }; } //namespace csl -} //namespace property +} //namespace properties } //namespace storm #endif /* STORM_FORMULA_CSL_GLOBALLY_H_ */ diff --git a/src/formula/csl/Next.h b/src/properties/csl/Next.h similarity index 96% rename from src/formula/csl/Next.h rename to src/properties/csl/Next.h index 478247de6..462a5eae4 100644 --- a/src/formula/csl/Next.h +++ b/src/properties/csl/Next.h @@ -8,11 +8,11 @@ #ifndef STORM_FORMULA_CSL_NEXT_H_ #define STORM_FORMULA_CSL_NEXT_H_ -#include "src/formula/csl/AbstractPathFormula.h" -#include "src/formula/csl/AbstractStateFormula.h" +#include "src/properties/csl/AbstractPathFormula.h" +#include "src/properties/csl/AbstractStateFormula.h" namespace storm { -namespace property { +namespace properties { namespace csl { // Forward declaration for the interface class. @@ -162,7 +162,7 @@ private: }; } //namespace csl -} //namespace property +} //namespace properties } //namespace storm #endif /* STORM_FORMULA_CSL_NEXT_H_ */ diff --git a/src/formula/csl/Not.h b/src/properties/csl/Not.h similarity index 97% rename from src/formula/csl/Not.h rename to src/properties/csl/Not.h index 5e382893d..de2f4acfb 100644 --- a/src/formula/csl/Not.h +++ b/src/properties/csl/Not.h @@ -8,11 +8,11 @@ #ifndef STORM_FORMULA_CSL_NOT_H_ #define STORM_FORMULA_CSL_NOT_H_ -#include "src/formula/csl/AbstractStateFormula.h" +#include "src/properties/csl/AbstractStateFormula.h" #include "src/modelchecker/csl/ForwardDeclarations.h" namespace storm { -namespace property { +namespace properties { namespace csl { // Forward declaration for the interface class. @@ -166,7 +166,7 @@ private: }; } //namespace csl -} //namespace property +} //namespace properties } //namespace storm #endif /* STORM_FORMULA_CSL_NOT_H_ */ diff --git a/src/formula/csl/Or.h b/src/properties/csl/Or.h similarity index 98% rename from src/formula/csl/Or.h rename to src/properties/csl/Or.h index d1c1a795c..f70144634 100644 --- a/src/formula/csl/Or.h +++ b/src/properties/csl/Or.h @@ -8,10 +8,10 @@ #ifndef STORM_FORMULA_CSL_OR_H_ #define STORM_FORMULA_CSL_OR_H_ -#include "src/formula/csl/AbstractStateFormula.h" +#include "src/properties/csl/AbstractStateFormula.h" namespace storm { -namespace property { +namespace properties { namespace csl { // Forward declaration for the interface class. @@ -206,7 +206,7 @@ private: }; } //namespace csl -} //namespace property +} //namespace properties } //namespace storm #endif /* STORM_FORMULA_CSL_OR_H_ */ diff --git a/src/formula/csl/ProbabilisticBoundOperator.h b/src/properties/csl/ProbabilisticBoundOperator.h similarity index 91% rename from src/formula/csl/ProbabilisticBoundOperator.h rename to src/properties/csl/ProbabilisticBoundOperator.h index a9adc4d6b..d8005d2fe 100644 --- a/src/formula/csl/ProbabilisticBoundOperator.h +++ b/src/properties/csl/ProbabilisticBoundOperator.h @@ -8,13 +8,13 @@ #ifndef STORM_FORMULA_CSL_PROBABILISTICBOUNDOPERATOR_H_ #define STORM_FORMULA_CSL_PROBABILISTICBOUNDOPERATOR_H_ -#include "src/formula/csl/AbstractStateFormula.h" -#include "src/formula/csl/AbstractPathFormula.h" -#include "src/formula/ComparisonType.h" +#include "src/properties/csl/AbstractStateFormula.h" +#include "src/properties/csl/AbstractPathFormula.h" +#include "src/properties/ComparisonType.h" #include "utility/constants.h" namespace storm { -namespace property { +namespace properties { namespace csl { // Forward declaration for the interface class. @@ -82,7 +82,7 @@ public: * @param bound The bound for the probability. * @param child The child formula subtree. */ - ProbabilisticBoundOperator(storm::property::ComparisonType comparisonOperator, T bound, std::shared_ptr> const & child) + ProbabilisticBoundOperator(storm::properties::ComparisonType comparisonOperator, T bound, std::shared_ptr> const & child) : comparisonOperator(comparisonOperator), bound(bound), child(child) { // Intentionally left empty. } @@ -175,7 +175,7 @@ public: * * @returns An enum value representing the comparison relation. */ - storm::property::ComparisonType const getComparisonOperator() const { + storm::properties::ComparisonType const getComparisonOperator() const { return comparisonOperator; } @@ -184,7 +184,7 @@ public: * * @param comparisonOperator An enum value representing the new comparison relation. */ - void setComparisonOperator(storm::property::ComparisonType comparisonOperator) { + void setComparisonOperator(storm::properties::ComparisonType comparisonOperator) { this->comparisonOperator = comparisonOperator; } @@ -225,7 +225,7 @@ public: private: // The operator used to indicate the kind of bound that is to be met. - storm::property::ComparisonType comparisonOperator; + storm::properties::ComparisonType comparisonOperator; // The probability bound. T bound; @@ -235,7 +235,7 @@ private: }; } //namespace csl -} //namespace property +} //namespace properties } //namespace storm #endif /* STORM_FORMULA_CSL_PROBABILISTICBOUNDOPERATOR_H_ */ diff --git a/src/formula/csl/SteadyStateBoundOperator.h b/src/properties/csl/SteadyStateBoundOperator.h similarity index 96% rename from src/formula/csl/SteadyStateBoundOperator.h rename to src/properties/csl/SteadyStateBoundOperator.h index 4ca8a2cba..141f070b7 100644 --- a/src/formula/csl/SteadyStateBoundOperator.h +++ b/src/properties/csl/SteadyStateBoundOperator.h @@ -9,10 +9,10 @@ #define STORM_FORMULA_CSL_STEADYSTATEOPERATOR_H_ #include "AbstractStateFormula.h" -#include "src/formula/ComparisonType.h" +#include "src/properties/ComparisonType.h" namespace storm { -namespace property { +namespace properties { namespace csl { // Forward declaration for the interface class. @@ -78,7 +78,7 @@ public: * @param bound The bound for the probability. * @param child The child formula subtree. */ - SteadyStateBoundOperator(storm::property::ComparisonType comparisonOperator, T bound, std::shared_ptr> const & child) + SteadyStateBoundOperator(storm::properties::ComparisonType comparisonOperator, T bound, std::shared_ptr> const & child) : comparisonOperator(comparisonOperator), bound(bound), child(child) { // Intentionally left empty } @@ -228,7 +228,7 @@ private: }; } //namespace csl -} //namespace property +} //namespace properties } //namespace storm #endif /* STORM_FORMULA_CSL_STEADYSTATEOPERATOR_H_ */ diff --git a/src/formula/csl/TimeBoundedEventually.h b/src/properties/csl/TimeBoundedEventually.h similarity index 94% rename from src/formula/csl/TimeBoundedEventually.h rename to src/properties/csl/TimeBoundedEventually.h index 785a1677a..3d537a34a 100644 --- a/src/formula/csl/TimeBoundedEventually.h +++ b/src/properties/csl/TimeBoundedEventually.h @@ -8,11 +8,11 @@ #ifndef STORM_FORMULA_CSL_TIMEBOUNDEDEVENTUALLY_H_ #define STORM_FORMULA_CSL_TIMEBOUNDEDEVENTUALLY_H_ -#include "src/formula/csl/AbstractPathFormula.h" -#include "src/formula/csl/AbstractStateFormula.h" +#include "src/properties/csl/AbstractPathFormula.h" +#include "src/properties/csl/AbstractStateFormula.h" namespace storm { -namespace property { +namespace properties { namespace csl { // Forward declaration for the interface class. @@ -68,7 +68,7 @@ public: * Creates a TimeBoundedEventually node without a subnode. * The resulting object will not represent a complete formula! */ - TimeBoundedEventually() : lowerBound(0), upperBound(0), child(nullptr) { + TimeBoundedEventually() : child(nullptr), lowerBound(0), upperBound(0) { // Intentionally left empty. } @@ -98,7 +98,8 @@ public: * @returns A new TimeBoundedEventually object that is a deep copy of the called object. */ virtual std::shared_ptr> clone() const override { - std::shared_ptr> result(new TimeBoundedEventually(lowerBound, upperBound)); + auto result = std::make_shared>(); + result->setInterval(lowerBound, upperBound); if (this->isChildSet()) { result->setChild(child->clone()); } @@ -212,7 +213,7 @@ private: }; } /* namespace csl */ -} /* namespace property */ +} /* namespace properties */ } /* namespace storm */ #endif /* STORM_FORMULA_CSL_TIMEBOUNDEDEVENTUALLY_H_ */ diff --git a/src/formula/csl/TimeBoundedUntil.h b/src/properties/csl/TimeBoundedUntil.h similarity index 94% rename from src/formula/csl/TimeBoundedUntil.h rename to src/properties/csl/TimeBoundedUntil.h index 5e27edd37..c224f93df 100644 --- a/src/formula/csl/TimeBoundedUntil.h +++ b/src/properties/csl/TimeBoundedUntil.h @@ -8,11 +8,11 @@ #ifndef STORM_FORMULA_CSL_TIMEBOUNDEDUNTIL_H_ #define STORM_FORMULA_CSL_TIMEBOUNDEDUNTIL_H_ -#include "src/formula/csl/AbstractPathFormula.h" -#include "src/formula/csl/AbstractStateFormula.h" +#include "src/properties/csl/AbstractPathFormula.h" +#include "src/properties/csl/AbstractStateFormula.h" namespace storm { -namespace property { +namespace properties { namespace csl { // Forward declaration for the interface class. @@ -70,8 +70,8 @@ public: * Creates a TimeBoundedUntil node without a subnode. * The resulting object will not represent a complete formula! */ - TimeBoundedUntil() : lowerBound(0), upperBound(0), left(nullptr), right(nullptr) { - setInterval(lowerBound, upperBound); + TimeBoundedUntil() : left(nullptr), right(nullptr), lowerBound(0), upperBound(0) { + // Intentionally left empty. } /*! @@ -100,7 +100,8 @@ public: * @returns A new TimeBoundedUntil object that is a deep copy of the called object. */ virtual std::shared_ptr> clone() const override { - std::shared_ptr> result(new TimeBoundedUntil(lowerBound, upperBound)); + auto result = std::make_shared>(); + result->setInterval(lowerBound, upperBound); if (this->isLeftSet()) { result->setLeft(left->clone()); } @@ -249,7 +250,7 @@ private: }; } /* namespace csl */ -} /* namespace property */ +} /* namespace properties */ } /* namespace storm */ #endif /* STORM_FORMULA_CSL_TIMEBOUNDEDUNTIL_H_ */ diff --git a/src/formula/csl/Until.h b/src/properties/csl/Until.h similarity index 97% rename from src/formula/csl/Until.h rename to src/properties/csl/Until.h index 8db1fa7d6..b709a1d82 100644 --- a/src/formula/csl/Until.h +++ b/src/properties/csl/Until.h @@ -8,11 +8,11 @@ #ifndef STORM_FORMULA_CSL_UNTIL_H_ #define STORM_FORMULA_CSL_UNTIL_H_ -#include "src/formula/csl/AbstractPathFormula.h" -#include "src/formula/csl/AbstractStateFormula.h" +#include "src/properties/csl/AbstractPathFormula.h" +#include "src/properties/csl/AbstractStateFormula.h" namespace storm { -namespace property { +namespace properties { namespace csl { // Forward declaration for the interface class. @@ -199,7 +199,7 @@ private: }; } //namespace csl -} //namespace property +} //namespace properties } //namespace storm #endif /* STORM_FORMULA_CSL_UNTIL_H_ */ diff --git a/src/formula/ltl/AbstractLtlFormula.h b/src/properties/ltl/AbstractLtlFormula.h similarity index 90% rename from src/formula/ltl/AbstractLtlFormula.h rename to src/properties/ltl/AbstractLtlFormula.h index 3605779be..c4ff5ad5a 100644 --- a/src/formula/ltl/AbstractLtlFormula.h +++ b/src/properties/ltl/AbstractLtlFormula.h @@ -10,10 +10,10 @@ #include #include "src/modelchecker/ltl/ForwardDeclarations.h" -#include "src/formula/AbstractFormula.h" +#include "src/properties/AbstractFormula.h" namespace storm { -namespace property { +namespace properties { namespace ltl { /*! @@ -25,7 +25,7 @@ namespace ltl { * the original and the copy. */ template -class AbstractLtlFormula : public virtual storm::property::AbstractFormula { +class AbstractLtlFormula : public virtual storm::properties::AbstractFormula { public: /*! @@ -59,6 +59,6 @@ public: }; } /* namespace ltl */ -} /* namespace property */ +} /* namespace properties */ } /* namespace storm */ #endif /* STORM_LTL_ABSTRACTLTLFORMULA_H_ */ diff --git a/src/formula/ltl/And.h b/src/properties/ltl/And.h similarity index 99% rename from src/formula/ltl/And.h rename to src/properties/ltl/And.h index 67656ef9b..51c88651b 100644 --- a/src/formula/ltl/And.h +++ b/src/properties/ltl/And.h @@ -13,7 +13,7 @@ #include namespace storm { -namespace property { +namespace properties { namespace ltl { // Forward declaration for the interface class. @@ -209,7 +209,7 @@ private: } //namespace ltl -} //namespace property +} //namespace properties } //namespace storm diff --git a/src/formula/ltl/Ap.h b/src/properties/ltl/Ap.h similarity index 96% rename from src/formula/ltl/Ap.h rename to src/properties/ltl/Ap.h index 544d84ed5..ed5356720 100644 --- a/src/formula/ltl/Ap.h +++ b/src/properties/ltl/Ap.h @@ -11,7 +11,7 @@ #include "AbstractLtlFormula.h" namespace storm { -namespace property { +namespace properties { namespace ltl { // Forward declaration for the interface class. @@ -51,7 +51,7 @@ class IApModelChecker { * @see AbstractLtlFormula */ template -class Ap: public storm::property::ltl::AbstractLtlFormula { +class Ap: public storm::properties::ltl::AbstractLtlFormula { public: @@ -131,6 +131,6 @@ private: }; } /* namespace ltl */ -} /* namespace property */ +} /* namespace properties */ } /* namespace storm */ #endif /* STORM_FORMULA_LTL_AP_H_ */ diff --git a/src/formula/ltl/BoundedEventually.h b/src/properties/ltl/BoundedEventually.h similarity index 99% rename from src/formula/ltl/BoundedEventually.h rename to src/properties/ltl/BoundedEventually.h index 57027cea3..120dec759 100644 --- a/src/formula/ltl/BoundedEventually.h +++ b/src/properties/ltl/BoundedEventually.h @@ -14,7 +14,7 @@ #include "src/modelchecker/ltl/ForwardDeclarations.h" namespace storm { -namespace property { +namespace properties { namespace ltl { // Forward declaration for the interface class. @@ -190,7 +190,7 @@ private: }; } //namespace ltl -} //namespace property +} //namespace properties } //namespace storm #endif /* STORM_FORMULA_LTL_BOUNDEDUNTIL_H_ */ diff --git a/src/formula/ltl/BoundedUntil.h b/src/properties/ltl/BoundedUntil.h similarity index 98% rename from src/formula/ltl/BoundedUntil.h rename to src/properties/ltl/BoundedUntil.h index 748e3ae0e..01e7dd14b 100644 --- a/src/formula/ltl/BoundedUntil.h +++ b/src/properties/ltl/BoundedUntil.h @@ -8,13 +8,13 @@ #ifndef STORM_FORMULA_LTL_BOUNDEDUNTIL_H_ #define STORM_FORMULA_LTL_BOUNDEDUNTIL_H_ -#include "src/formula/ltl/AbstractLtlFormula.h" +#include "src/properties/ltl/AbstractLtlFormula.h" #include #include #include "src/modelchecker/ltl/ForwardDeclarations.h" namespace storm { -namespace property { +namespace properties { namespace ltl { // Forward declaration for the interface class. @@ -223,7 +223,7 @@ private: }; } //namespace ltl -} //namespace property +} //namespace properties } //namespace storm #endif /* STORM_FORMULA_LTL_BOUNDEDUNTIL_H_ */ diff --git a/src/formula/ltl/Eventually.h b/src/properties/ltl/Eventually.h similarity index 97% rename from src/formula/ltl/Eventually.h rename to src/properties/ltl/Eventually.h index 9af8ad9b2..6c2ac2940 100644 --- a/src/formula/ltl/Eventually.h +++ b/src/properties/ltl/Eventually.h @@ -8,11 +8,11 @@ #ifndef STORM_FORMULA_LTL_EVENTUALLY_H_ #define STORM_FORMULA_LTL_EVENTUALLY_H_ -#include "src/formula/ltl/AbstractLtlFormula.h" +#include "src/properties/ltl/AbstractLtlFormula.h" #include "src/modelchecker/ltl/ForwardDeclarations.h" namespace storm { -namespace property { +namespace properties { namespace ltl { // Forward declaration for the interface class. @@ -159,7 +159,7 @@ private: }; } //namespace ltl -} //namespace property +} //namespace properties } //namespace storm #endif /* STORM_FORMULA_LTL_EVENTUALLY_H_ */ diff --git a/src/formula/ltl/Globally.h b/src/properties/ltl/Globally.h similarity index 98% rename from src/formula/ltl/Globally.h rename to src/properties/ltl/Globally.h index 0e0af887a..443ac20bb 100644 --- a/src/formula/ltl/Globally.h +++ b/src/properties/ltl/Globally.h @@ -12,7 +12,7 @@ #include "src/modelchecker/ltl/ForwardDeclarations.h" namespace storm { -namespace property { +namespace properties { namespace ltl { // Forward declaration for the interface class. @@ -159,7 +159,7 @@ private: }; } //namespace ltl -} //namespace property +} //namespace properties } //namespace storm #endif /* STORM_FORMULA_LTL_GLOBALLY_H_ */ diff --git a/src/formula/ltl/LtlFilter.h b/src/properties/ltl/LtlFilter.h similarity index 96% rename from src/formula/ltl/LtlFilter.h rename to src/properties/ltl/LtlFilter.h index 4b7704b10..5e4760fa2 100644 --- a/src/formula/ltl/LtlFilter.h +++ b/src/properties/ltl/LtlFilter.h @@ -8,14 +8,14 @@ #ifndef STORM_FORMULA_LTL_LTLFILTER_H_ #define STORM_FORMULA_LTL_LTLFILTER_H_ -#include "src/formula/AbstractFilter.h" +#include "src/properties/AbstractFilter.h" #include "src/modelchecker/ltl/AbstractModelChecker.h" -#include "src/formula/ltl/AbstractLtlFormula.h" -#include "src/formula/actions/AbstractAction.h" +#include "src/properties/ltl/AbstractLtlFormula.h" +#include "src/properties/actions/AbstractAction.h" #include "src/exceptions/NotImplementedException.h" namespace storm { -namespace property { +namespace properties { namespace ltl { /*! @@ -25,10 +25,10 @@ namespace ltl { * Additionally it maintains a list of filter actions that are used to further manipulate the modelchecking results and prepare them for output. */ template -class LtlFilter : public storm::property::AbstractFilter { +class LtlFilter : public storm::properties::AbstractFilter { // Convenience typedef to make the code more readable. - typedef typename storm::property::action::AbstractAction::Result Result; + typedef typename storm::properties::action::AbstractAction::Result Result; public: @@ -275,7 +275,7 @@ private: } //namespace ltl -} //namespace property +} //namespace properties } //namespace storm #endif /* STORM_FORMULA_LTL_LTLFILTER_H_ */ diff --git a/src/formula/ltl/Next.h b/src/properties/ltl/Next.h similarity index 98% rename from src/formula/ltl/Next.h rename to src/properties/ltl/Next.h index 0eb64a2ed..40ad52b0c 100644 --- a/src/formula/ltl/Next.h +++ b/src/properties/ltl/Next.h @@ -11,7 +11,7 @@ #include "AbstractLtlFormula.h" namespace storm { -namespace property { +namespace properties { namespace ltl { // Forward declaration for the interface class. @@ -158,7 +158,7 @@ private: }; } //namespace ltl -} //namespace property +} //namespace properties } //namespace storm #endif /* STORM_FORMULA_LTL_NEXT_H_ */ diff --git a/src/formula/ltl/Not.h b/src/properties/ltl/Not.h similarity index 98% rename from src/formula/ltl/Not.h rename to src/properties/ltl/Not.h index cd1edd251..e0accc91f 100644 --- a/src/formula/ltl/Not.h +++ b/src/properties/ltl/Not.h @@ -11,7 +11,7 @@ #include "AbstractLtlFormula.h" namespace storm { -namespace property { +namespace properties { namespace ltl { // Forward declaration for the interface class. @@ -165,7 +165,7 @@ private: }; } //namespace ltl -} //namespace property +} //namespace properties } //namespace storm #endif /* STORM_FORMULA_LTL_NOT_H_ */ diff --git a/src/formula/ltl/Or.h b/src/properties/ltl/Or.h similarity index 97% rename from src/formula/ltl/Or.h rename to src/properties/ltl/Or.h index a7c73a1f1..5a2f20ab6 100644 --- a/src/formula/ltl/Or.h +++ b/src/properties/ltl/Or.h @@ -11,7 +11,7 @@ #include "AbstractLtlFormula.h" namespace storm { -namespace property { +namespace properties { namespace ltl { // Forward declaration for the interface class. @@ -57,7 +57,7 @@ class IOrModelChecker { * @see AbstractLtlFormula */ template -class Or: public storm::property::ltl::AbstractLtlFormula { +class Or: public storm::properties::ltl::AbstractLtlFormula { public: @@ -205,6 +205,6 @@ private: }; } /* namespace ltl */ -} /* namespace property */ +} /* namespace properties */ } /* namespace storm */ #endif /* OR_H_ */ diff --git a/src/formula/ltl/Until.h b/src/properties/ltl/Until.h similarity index 99% rename from src/formula/ltl/Until.h rename to src/properties/ltl/Until.h index 56301c0f4..2d415aeac 100644 --- a/src/formula/ltl/Until.h +++ b/src/properties/ltl/Until.h @@ -11,7 +11,7 @@ #include "AbstractLtlFormula.h" namespace storm { -namespace property { +namespace properties { namespace ltl { // Forward declaration for the interface class. @@ -194,7 +194,7 @@ private: }; } //namespace ltl -} //namespace property +} //namespace properties } //namespace storm #endif /* STORM_FORMULA_LTL_UNTIL_H_ */ diff --git a/src/formula/prctl/AbstractPathFormula.h b/src/properties/prctl/AbstractPathFormula.h similarity index 90% rename from src/formula/prctl/AbstractPathFormula.h rename to src/properties/prctl/AbstractPathFormula.h index 1caf60297..98ba51f19 100644 --- a/src/formula/prctl/AbstractPathFormula.h +++ b/src/properties/prctl/AbstractPathFormula.h @@ -8,7 +8,7 @@ #ifndef STORM_FORMULA_PRCTL_ABSTRACTPATHFORMULA_H_ #define STORM_FORMULA_PRCTL_ABSTRACTPATHFORMULA_H_ -#include "src/formula/prctl/AbstractPrctlFormula.h" +#include "src/properties/prctl/AbstractPrctlFormula.h" #include "src/modelchecker/prctl/ForwardDeclarations.h" #include @@ -16,7 +16,7 @@ #include namespace storm { -namespace property { +namespace properties { namespace prctl { /*! @@ -26,7 +26,7 @@ namespace prctl { * The result of a modelchecking process on such a formula is a vector representing the satisfaction probabilities for each state of the model. */ template -class AbstractPathFormula : public virtual storm::property::prctl::AbstractPrctlFormula { +class AbstractPathFormula : public virtual storm::properties::prctl::AbstractPrctlFormula { public: @@ -63,7 +63,7 @@ public: }; } //namespace prctl -} //namespace property +} //namespace properties } //namespace storm #endif /* STORM_FORMULA_PRCTL_ABSTRACTPATHFORMULA_H_ */ diff --git a/src/formula/prctl/AbstractPrctlFormula.h b/src/properties/prctl/AbstractPrctlFormula.h similarity index 73% rename from src/formula/prctl/AbstractPrctlFormula.h rename to src/properties/prctl/AbstractPrctlFormula.h index e7b165afa..cefe91e4b 100644 --- a/src/formula/prctl/AbstractPrctlFormula.h +++ b/src/properties/prctl/AbstractPrctlFormula.h @@ -8,10 +8,10 @@ #ifndef STORM_FORMULA_PRCTL_ABSTRACTPRCTLFORMULA_H_ #define STORM_FORMULA_PRCTL_ABSTRACTPRCTLFORMULA_H_ -#include "src/formula/AbstractFormula.h" +#include "src/properties/AbstractFormula.h" namespace storm { -namespace property { +namespace properties { namespace prctl { // Forward declarations. @@ -25,7 +25,7 @@ template class Until; } namespace storm { -namespace property { +namespace properties { namespace prctl { /*! @@ -37,7 +37,7 @@ namespace prctl { * the original and the copy. */ template -class AbstractPrctlFormula : public virtual storm::property::AbstractFormula { +class AbstractPrctlFormula : public virtual storm::properties::AbstractFormula { public: /*! @@ -59,23 +59,23 @@ public: bool isProbEventuallyAP() const { // Test if a probabilistic bound operator is at the root. - if(dynamic_cast const *>(this) == nullptr) { + if(dynamic_cast const *>(this) == nullptr) { return false; } - auto probFormula = dynamic_cast const *>(this); + auto probFormula = dynamic_cast const *>(this); // Check if the direct subformula of the probabilistic bound operator is an eventually or until formula. - if(std::dynamic_pointer_cast>(probFormula->getChild()).get() != nullptr) { + if(std::dynamic_pointer_cast>(probFormula->getChild()).get() != nullptr) { // Get the subformula and check if its subformulas are propositional. - auto eventuallyFormula = std::dynamic_pointer_cast>(probFormula->getChild()); + auto eventuallyFormula = std::dynamic_pointer_cast>(probFormula->getChild()); return eventuallyFormula->getChild()->isPropositional(); } - else if(std::dynamic_pointer_cast>(probFormula->getChild()).get() != nullptr) { + else if(std::dynamic_pointer_cast>(probFormula->getChild()).get() != nullptr) { // Get the subformula and check if its subformulas are propositional. - auto untilFormula = std::dynamic_pointer_cast>(probFormula->getChild()); + auto untilFormula = std::dynamic_pointer_cast>(probFormula->getChild()); return untilFormula->getLeft()->isPropositional() && untilFormula->getRight()->isPropositional(); } @@ -84,6 +84,6 @@ public: }; } /* namespace prctl */ -} /* namespace property */ +} /* namespace properties */ } /* namespace storm */ #endif /* ABSTRACTPRCTLFORMULA_H_ */ diff --git a/src/formula/prctl/AbstractRewardPathFormula.h b/src/properties/prctl/AbstractRewardPathFormula.h similarity index 90% rename from src/formula/prctl/AbstractRewardPathFormula.h rename to src/properties/prctl/AbstractRewardPathFormula.h index 09d0dcbf2..e19523679 100644 --- a/src/formula/prctl/AbstractRewardPathFormula.h +++ b/src/properties/prctl/AbstractRewardPathFormula.h @@ -8,10 +8,10 @@ #ifndef STORM_FORMULA_PRCTL_ABSTRACTREWARDPATHFORMULA_H_ #define STORM_FORMULA_PRCTL_ABSTRACTREWARDPATHFORMULA_H_ -#include "src/formula/prctl/AbstractPrctlFormula.h" +#include "src/properties/prctl/AbstractPrctlFormula.h" namespace storm { -namespace property { +namespace properties { namespace prctl { /*! @@ -25,7 +25,7 @@ namespace prctl { * @see AbstractPrctlFormula */ template -class AbstractRewardPathFormula : public virtual storm::property::prctl::AbstractPrctlFormula { +class AbstractRewardPathFormula : public virtual storm::properties::prctl::AbstractPrctlFormula { public: @@ -62,7 +62,7 @@ public: }; } //namespace prctl -} //namespace property +} //namespace properties } //namespace storm diff --git a/src/formula/prctl/AbstractStateFormula.h b/src/properties/prctl/AbstractStateFormula.h similarity index 88% rename from src/formula/prctl/AbstractStateFormula.h rename to src/properties/prctl/AbstractStateFormula.h index 2da8c093b..2e088d88e 100644 --- a/src/formula/prctl/AbstractStateFormula.h +++ b/src/properties/prctl/AbstractStateFormula.h @@ -8,19 +8,19 @@ #ifndef STORM_FORMULA_PRCTL_ABSTRACTSTATEFORMULA_H_ #define STORM_FORMULA_PRCTL_ABSTRACTSTATEFORMULA_H_ -#include "src/formula/prctl/AbstractPrctlFormula.h" +#include "src/properties/prctl/AbstractPrctlFormula.h" #include "src/storage/BitVector.h" #include "src/modelchecker/prctl/ForwardDeclarations.h" namespace storm { -namespace property { +namespace properties { namespace prctl { /*! * Abstract base class for Prctl state formulas. */ template -class AbstractStateFormula : public storm::property::prctl::AbstractPrctlFormula { +class AbstractStateFormula : public storm::properties::prctl::AbstractPrctlFormula { public: @@ -57,7 +57,7 @@ public: }; } //namespace prctl -} //namespace property +} //namespace properties } //namespace storm diff --git a/src/formula/prctl/And.h b/src/properties/prctl/And.h similarity index 98% rename from src/formula/prctl/And.h rename to src/properties/prctl/And.h index c312f30c5..adbff8c92 100644 --- a/src/formula/prctl/And.h +++ b/src/properties/prctl/And.h @@ -8,12 +8,12 @@ #ifndef STORM_FORMULA_PRCTL_AND_H_ #define STORM_FORMULA_PRCTL_AND_H_ -#include "src/formula/prctl/AbstractStateFormula.h" +#include "src/properties/prctl/AbstractStateFormula.h" #include "src/modelchecker/prctl/ForwardDeclarations.h" #include namespace storm { -namespace property { +namespace properties { namespace prctl { // Forward declaration for the interface class. @@ -210,7 +210,7 @@ private: } //namespace prctl -} //namespace property +} //namespace properties } //namespace storm diff --git a/src/formula/prctl/Ap.h b/src/properties/prctl/Ap.h similarity index 96% rename from src/formula/prctl/Ap.h rename to src/properties/prctl/Ap.h index 15bd442ca..fb9fe1361 100644 --- a/src/formula/prctl/Ap.h +++ b/src/properties/prctl/Ap.h @@ -8,11 +8,11 @@ #ifndef STORM_FORMULA_PRCTL_AP_H_ #define STORM_FORMULA_PRCTL_AP_H_ -#include "src/formula/prctl/AbstractStateFormula.h" +#include "src/properties/prctl/AbstractStateFormula.h" #include "src/modelchecker/prctl/ForwardDeclarations.h" namespace storm { -namespace property { +namespace properties { namespace prctl { // Forward declaration for the interface class. @@ -134,7 +134,7 @@ private: } //namespace abstract -} //namespace property +} //namespace properties } //namespace storm diff --git a/src/formula/prctl/BoundedEventually.h b/src/properties/prctl/BoundedEventually.h similarity index 97% rename from src/formula/prctl/BoundedEventually.h rename to src/properties/prctl/BoundedEventually.h index 920a6a073..980717cfa 100644 --- a/src/formula/prctl/BoundedEventually.h +++ b/src/properties/prctl/BoundedEventually.h @@ -8,14 +8,14 @@ #ifndef STORM_FORMULA_PRCTL_BOUNDEDEVENTUALLY_H_ #define STORM_FORMULA_PRCTL_BOUNDEDEVENTUALLY_H_ -#include "src/formula/prctl/AbstractPathFormula.h" -#include "src/formula/prctl/AbstractStateFormula.h" +#include "src/properties/prctl/AbstractPathFormula.h" +#include "src/properties/prctl/AbstractStateFormula.h" #include #include #include "src/modelchecker/prctl/ForwardDeclarations.h" namespace storm { -namespace property { +namespace properties { namespace prctl{ // Forward declaration for the interface class. @@ -191,7 +191,7 @@ private: }; } //namespace prctl -} //namespace property +} //namespace properties } //namespace storm #endif /* STORM_FORMULA_PRCTL_BOUNDEDUNTIL_H_ */ diff --git a/src/formula/prctl/BoundedNaryUntil.h b/src/properties/prctl/BoundedNaryUntil.h similarity index 97% rename from src/formula/prctl/BoundedNaryUntil.h rename to src/properties/prctl/BoundedNaryUntil.h index c6e4092e9..526c236ad 100644 --- a/src/formula/prctl/BoundedNaryUntil.h +++ b/src/properties/prctl/BoundedNaryUntil.h @@ -8,8 +8,8 @@ #ifndef STORM_FORMULA_PRCTL_BOUNDEDNARYUNTIL_H_ #define STORM_FORMULA_PRCTL_BOUNDEDNARYUNTIL_H_ -#include "src/formula/prctl/AbstractPathFormula.h" -#include "src/formula/prctl/AbstractStateFormula.h" +#include "src/properties/prctl/AbstractPathFormula.h" +#include "src/properties/prctl/AbstractStateFormula.h" #include #include #include @@ -18,7 +18,7 @@ #include "src/modelchecker/prctl/ForwardDeclarations.h" namespace storm { -namespace property { +namespace properties { namespace prctl { // Forward declaration for the interface class. @@ -226,7 +226,7 @@ private: }; } //namespace prctl -} //namespace property +} //namespace properties } //namespace storm #endif /* STORM_FORMULA_PRCTL_BOUNDEDNARYUNTIL_H_ */ diff --git a/src/formula/prctl/BoundedUntil.h b/src/properties/prctl/BoundedUntil.h similarity index 97% rename from src/formula/prctl/BoundedUntil.h rename to src/properties/prctl/BoundedUntil.h index ec0b59f51..b52fffe55 100644 --- a/src/formula/prctl/BoundedUntil.h +++ b/src/properties/prctl/BoundedUntil.h @@ -8,14 +8,14 @@ #ifndef STORM_FORMULA_PRCTL_BOUNDEDUNTIL_H_ #define STORM_FORMULA_PRCTL_BOUNDEDUNTIL_H_ -#include "src/formula/prctl/AbstractPathFormula.h" -#include "src/formula/prctl/AbstractStateFormula.h" +#include "src/properties/prctl/AbstractPathFormula.h" +#include "src/properties/prctl/AbstractStateFormula.h" #include #include #include "src/modelchecker/prctl/ForwardDeclarations.h" namespace storm { -namespace property { +namespace properties { namespace prctl { // Forward declaration for the interface class. @@ -227,7 +227,7 @@ private: }; } //namespace prctl -} //namespace property +} //namespace properties } //namespace storm #endif /* STORM_FORMULA_PRCTL_BOUNDEDUNTIL_H_ */ diff --git a/src/formula/prctl/CumulativeReward.h b/src/properties/prctl/CumulativeReward.h similarity index 98% rename from src/formula/prctl/CumulativeReward.h rename to src/properties/prctl/CumulativeReward.h index fd51db72c..9b27aefd6 100644 --- a/src/formula/prctl/CumulativeReward.h +++ b/src/properties/prctl/CumulativeReward.h @@ -12,7 +12,7 @@ #include namespace storm { -namespace property { +namespace properties { namespace prctl { // Forward declaration for the interface class. @@ -142,7 +142,7 @@ private: }; } //namespace prctl -} //namespace property +} //namespace properties } //namespace storm #endif /* STORM_FORMULA_PRCTL_INSTANTANEOUSREWARD_H_ */ diff --git a/src/formula/prctl/Eventually.h b/src/properties/prctl/Eventually.h similarity index 96% rename from src/formula/prctl/Eventually.h rename to src/properties/prctl/Eventually.h index 6d22e1dd4..01ed2150b 100644 --- a/src/formula/prctl/Eventually.h +++ b/src/properties/prctl/Eventually.h @@ -8,12 +8,12 @@ #ifndef STORM_FORMULA_PRCTL_EVENTUALLY_H_ #define STORM_FORMULA_PRCTL_EVENTUALLY_H_ -#include "src/formula/prctl/AbstractPathFormula.h" -#include "src/formula/prctl/AbstractStateFormula.h" +#include "src/properties/prctl/AbstractPathFormula.h" +#include "src/properties/prctl/AbstractStateFormula.h" #include "src/modelchecker/prctl/ForwardDeclarations.h" namespace storm { -namespace property { +namespace properties { namespace prctl { // Forward declaration for the interface class. @@ -163,7 +163,7 @@ private: }; } //namespace prctl -} //namespace property +} //namespace properties } //namespace storm #endif /* STORM_FORMULA_PRCTL_EVENTUALLY_H_ */ diff --git a/src/formula/prctl/Globally.h b/src/properties/prctl/Globally.h similarity index 96% rename from src/formula/prctl/Globally.h rename to src/properties/prctl/Globally.h index 12f29f19d..2a1f85dec 100644 --- a/src/formula/prctl/Globally.h +++ b/src/properties/prctl/Globally.h @@ -8,12 +8,12 @@ #ifndef STORM_FORMULA_PRCTL_GLOBALLY_H_ #define STORM_FORMULA_PRCTL_GLOBALLY_H_ -#include "src/formula/prctl/AbstractPathFormula.h" -#include "src/formula/prctl/AbstractStateFormula.h" +#include "src/properties/prctl/AbstractPathFormula.h" +#include "src/properties/prctl/AbstractStateFormula.h" #include "src/modelchecker/prctl/ForwardDeclarations.h" namespace storm { -namespace property { +namespace properties { namespace prctl { // Forward declaration for the interface class. @@ -163,7 +163,7 @@ private: }; } //namespace prctl -} //namespace property +} //namespace properties } //namespace storm #endif /* STORM_FORMULA_PRCTL_GLOBALLY_H_ */ diff --git a/src/formula/prctl/InstantaneousReward.h b/src/properties/prctl/InstantaneousReward.h similarity index 98% rename from src/formula/prctl/InstantaneousReward.h rename to src/properties/prctl/InstantaneousReward.h index c8f61b120..d2f6d21a6 100644 --- a/src/formula/prctl/InstantaneousReward.h +++ b/src/properties/prctl/InstantaneousReward.h @@ -13,7 +13,7 @@ #include namespace storm { -namespace property { +namespace properties { namespace prctl { // Forward declaration for the interface class. @@ -143,7 +143,7 @@ private: }; } //namespace prctl -} //namespace property +} //namespace properties } //namespace storm #endif /* STORM_FORMULA_PRCTL_INSTANTANEOUSREWARD_H_ */ diff --git a/src/formula/prctl/Next.h b/src/properties/prctl/Next.h similarity index 96% rename from src/formula/prctl/Next.h rename to src/properties/prctl/Next.h index a83ff1690..642754ec1 100644 --- a/src/formula/prctl/Next.h +++ b/src/properties/prctl/Next.h @@ -8,11 +8,11 @@ #ifndef STORM_FORMULA_PRCTL_NEXT_H_ #define STORM_FORMULA_PRCTL_NEXT_H_ -#include "src/formula/prctl/AbstractPathFormula.h" -#include "src/formula/prctl/AbstractStateFormula.h" +#include "src/properties/prctl/AbstractPathFormula.h" +#include "src/properties/prctl/AbstractStateFormula.h" namespace storm { -namespace property { +namespace properties { namespace prctl { // Forward declaration for the interface class. @@ -162,7 +162,7 @@ private: }; } //namespace prctl -} //namespace property +} //namespace properties } //namespace storm #endif /* STORM_FORMULA_PRCTL_NEXT_H_ */ diff --git a/src/formula/prctl/Not.h b/src/properties/prctl/Not.h similarity index 98% rename from src/formula/prctl/Not.h rename to src/properties/prctl/Not.h index 83af85e53..db3e2ce7d 100644 --- a/src/formula/prctl/Not.h +++ b/src/properties/prctl/Not.h @@ -12,7 +12,7 @@ #include "src/modelchecker/prctl/ForwardDeclarations.h" namespace storm { -namespace property { +namespace properties { namespace prctl { // Forward declaration for the interface class. @@ -167,7 +167,7 @@ private: }; } //namespace prctl -} //namespace property +} //namespace properties } //namespace storm #endif /* STORM_FORMULA_PRCTL_NOT_H_ */ diff --git a/src/formula/prctl/Or.h b/src/properties/prctl/Or.h similarity index 98% rename from src/formula/prctl/Or.h rename to src/properties/prctl/Or.h index 3044ce3e7..3a897ec6f 100644 --- a/src/formula/prctl/Or.h +++ b/src/properties/prctl/Or.h @@ -8,10 +8,10 @@ #ifndef STORM_FORMULA_PRCTL_OR_H_ #define STORM_FORMULA_PRCTL_OR_H_ -#include "src/formula/prctl/AbstractStateFormula.h" +#include "src/properties/prctl/AbstractStateFormula.h" namespace storm { -namespace property { +namespace properties { namespace prctl { // Forward declaration for the interface class. @@ -207,7 +207,7 @@ private: }; } //namespace prctl -} //namespace property +} //namespace properties } //namespace storm #endif /* STORM_FORMULA_PRCTL_OR_H_ */ diff --git a/src/formula/prctl/PrctlFilter.h b/src/properties/prctl/PrctlFilter.h similarity index 95% rename from src/formula/prctl/PrctlFilter.h rename to src/properties/prctl/PrctlFilter.h index 02ffa5c5a..1e742a515 100644 --- a/src/formula/prctl/PrctlFilter.h +++ b/src/properties/prctl/PrctlFilter.h @@ -8,18 +8,18 @@ #ifndef STORM_FORMULA_PRCTL_PRCTLFILTER_H_ #define STORM_FORMULA_PRCTL_PRCTLFILTER_H_ -#include "src/formula/AbstractFilter.h" -#include "src/formula/prctl/AbstractPrctlFormula.h" -#include "src/formula/prctl/AbstractPathFormula.h" -#include "src/formula/prctl/AbstractStateFormula.h" +#include "src/properties/AbstractFilter.h" +#include "src/properties/prctl/AbstractPrctlFormula.h" +#include "src/properties/prctl/AbstractPathFormula.h" +#include "src/properties/prctl/AbstractStateFormula.h" #include "src/modelchecker/prctl/AbstractModelChecker.h" -#include "src/formula/actions/AbstractAction.h" +#include "src/properties/actions/AbstractAction.h" #include #include namespace storm { -namespace property { +namespace properties { namespace prctl { /*! @@ -29,10 +29,10 @@ namespace prctl { * Additionally it maintains a list of filter actions that are used to further manipulate the modelchecking results and prepare them for output. */ template -class PrctlFilter : public storm::property::AbstractFilter { +class PrctlFilter : public storm::properties::AbstractFilter { // Convenience typedef to make the code more readable. - typedef typename storm::property::action::AbstractAction::Result Result; + typedef typename storm::properties::action::AbstractAction::Result Result; public: @@ -271,7 +271,7 @@ private: if(this->opt != UNDEFINED) { // If it is specified that min/max probabilities/rewards should be computed, call the appropriate method of the model checker. - result.stateResult = modelchecker.checkOptimizingOperator(*formula, this->opt == storm::property::MINIMIZE ? true : false); + result.stateResult = modelchecker.checkOptimizingOperator(*formula, this->opt == storm::properties::MINIMIZE ? true : false); } else { result.stateResult = formula->check(modelchecker); } @@ -295,7 +295,7 @@ private: if(this->opt != UNDEFINED) { // If it is specified that min/max probabilities/rewards should be computed, call the appropriate method of the model checker. - result.pathResult = modelchecker.checkOptimizingOperator(*formula, this->opt == storm::property::MINIMIZE ? true : false); + result.pathResult = modelchecker.checkOptimizingOperator(*formula, this->opt == storm::properties::MINIMIZE ? true : false); } else { result.pathResult = formula->check(modelchecker, false); } @@ -319,7 +319,7 @@ private: if(this->opt != UNDEFINED) { // If it is specified that min/max probabilities/rewards should be computed, call the appropriate method of the model checker. - result.pathResult = modelchecker.checkOptimizingOperator(*formula, this->opt == storm::property::MINIMIZE ? true : false); + result.pathResult = modelchecker.checkOptimizingOperator(*formula, this->opt == storm::properties::MINIMIZE ? true : false); } else { result.pathResult = formula->check(modelchecker, false); } @@ -428,7 +428,7 @@ private: }; } //namespace prctl -} //namespace property +} //namespace properties } //namespace storm diff --git a/src/formula/prctl/ProbabilisticBoundOperator.h b/src/properties/prctl/ProbabilisticBoundOperator.h similarity index 93% rename from src/formula/prctl/ProbabilisticBoundOperator.h rename to src/properties/prctl/ProbabilisticBoundOperator.h index abaf1e1db..c7b4e075a 100644 --- a/src/formula/prctl/ProbabilisticBoundOperator.h +++ b/src/properties/prctl/ProbabilisticBoundOperator.h @@ -11,10 +11,10 @@ #include "AbstractStateFormula.h" #include "AbstractPathFormula.h" #include "utility/constants.h" -#include "src/formula/ComparisonType.h" +#include "src/properties/ComparisonType.h" namespace storm { -namespace property { +namespace properties { namespace prctl { // Forward declaration for the interface class. @@ -83,7 +83,7 @@ public: * @param bound The bound for the probability. * @param child The child formula subtree. */ - ProbabilisticBoundOperator(storm::property::ComparisonType comparisonOperator, T bound, std::shared_ptr> const & child) + ProbabilisticBoundOperator(storm::properties::ComparisonType comparisonOperator, T bound, std::shared_ptr> const & child) : comparisonOperator(comparisonOperator), bound(bound), child(child) { // Intentionally left empty. } @@ -176,7 +176,7 @@ public: * * @returns An enum value representing the comparison relation. */ - storm::property::ComparisonType const getComparisonOperator() const { + storm::properties::ComparisonType const getComparisonOperator() const { return comparisonOperator; } @@ -185,7 +185,7 @@ public: * * @param comparisonOperator An enum value representing the new comparison relation. */ - void setComparisonOperator(storm::property::ComparisonType comparisonOperator) { + void setComparisonOperator(storm::properties::ComparisonType comparisonOperator) { this->comparisonOperator = comparisonOperator; } @@ -226,7 +226,7 @@ public: private: // The operator used to indicate the kind of bound that is to be met. - storm::property::ComparisonType comparisonOperator; + storm::properties::ComparisonType comparisonOperator; // The probability bound. T bound; @@ -236,7 +236,7 @@ private: }; } //namespace prctl -} //namespace property +} //namespace properties } //namespace storm #endif /* STORM_FORMULA_PRCTL_PROBABILISTICBOUNDOPERATOR_H_ */ diff --git a/src/formula/prctl/ReachabilityReward.h b/src/properties/prctl/ReachabilityReward.h similarity index 99% rename from src/formula/prctl/ReachabilityReward.h rename to src/properties/prctl/ReachabilityReward.h index 2187b6250..3b20fe7f5 100644 --- a/src/formula/prctl/ReachabilityReward.h +++ b/src/properties/prctl/ReachabilityReward.h @@ -12,7 +12,7 @@ #include "AbstractStateFormula.h" namespace storm { -namespace property { +namespace properties { namespace prctl { // Forward declaration for the interface class. @@ -164,7 +164,7 @@ private: }; } //namespace prctl -} //namespace property +} //namespace properties } //namespace storm #endif /* STORM_FORMULA_PRCTL_REACHABILITYREWARD_H_ */ diff --git a/src/formula/prctl/RewardBoundOperator.h b/src/properties/prctl/RewardBoundOperator.h similarity index 93% rename from src/formula/prctl/RewardBoundOperator.h rename to src/properties/prctl/RewardBoundOperator.h index a7a4089a9..30322f2be 100644 --- a/src/formula/prctl/RewardBoundOperator.h +++ b/src/properties/prctl/RewardBoundOperator.h @@ -11,10 +11,10 @@ #include "AbstractRewardPathFormula.h" #include "AbstractStateFormula.h" #include "utility/constants.h" -#include "src/formula/ComparisonType.h" +#include "src/properties/ComparisonType.h" namespace storm { -namespace property { +namespace properties { namespace prctl { // Forward declaration for the interface class. @@ -84,7 +84,7 @@ public: * @param bound The bound for the rewards. * @param child The child formula subtree. */ - RewardBoundOperator(storm::property::ComparisonType comparisonOperator, T bound, std::shared_ptr> const & child) + RewardBoundOperator(storm::properties::ComparisonType comparisonOperator, T bound, std::shared_ptr> const & child) : comparisonOperator(comparisonOperator), bound(bound), child(child) { // Intentionally left empty } @@ -177,7 +177,7 @@ public: * * @returns An enum value representing the comparison relation. */ - storm::property::ComparisonType const getComparisonOperator() const { + storm::properties::ComparisonType const getComparisonOperator() const { return comparisonOperator; } @@ -186,7 +186,7 @@ public: * * @param comparisonOperator An enum value representing the new comparison relation. */ - void setComparisonOperator(storm::property::ComparisonType comparisonOperator) { + void setComparisonOperator(storm::properties::ComparisonType comparisonOperator) { this->comparisonOperator = comparisonOperator; } @@ -227,7 +227,7 @@ public: private: // The operator used to indicate the kind of bound that is to be met. - storm::property::ComparisonType comparisonOperator; + storm::properties::ComparisonType comparisonOperator; // The reward bound. T bound; @@ -237,7 +237,7 @@ private: }; } //namespace prctl -} //namespace property +} //namespace properties } //namespace storm #endif /* STORM_FORMULA_PRCTL_REWARDBOUNDOPERATOR_H_ */ diff --git a/src/formula/prctl/SteadyStateReward.h b/src/properties/prctl/SteadyStateReward.h similarity index 98% rename from src/formula/prctl/SteadyStateReward.h rename to src/properties/prctl/SteadyStateReward.h index c075abba9..0143c91a1 100644 --- a/src/formula/prctl/SteadyStateReward.h +++ b/src/properties/prctl/SteadyStateReward.h @@ -12,7 +12,7 @@ #include namespace storm { -namespace property { +namespace properties { namespace prctl { // Forward declaration for the interface class. @@ -109,6 +109,6 @@ public: }; } //namespace prctl -} //namespace property +} //namespace properties } //namespace storm #endif /* STORM_FORMULA_PRCTL_STEADYSTATEREWARD_H_ */ diff --git a/src/formula/prctl/Until.h b/src/properties/prctl/Until.h similarity index 99% rename from src/formula/prctl/Until.h rename to src/properties/prctl/Until.h index 27eb89167..f9e19955b 100644 --- a/src/formula/prctl/Until.h +++ b/src/properties/prctl/Until.h @@ -12,7 +12,7 @@ #include "AbstractStateFormula.h" namespace storm { -namespace property { +namespace properties { namespace prctl { // Forward declaration for the interface class. @@ -199,7 +199,7 @@ private: }; } //namespace prctl -} //namespace property +} //namespace properties } //namespace storm #endif /* STORM_FORMULA_PRCTL_UNTIL_H_ */ diff --git a/src/storm.cpp b/src/storm.cpp index 2896bd4b9..e3786c35f 100644 --- a/src/storm.cpp +++ b/src/storm.cpp @@ -40,7 +40,7 @@ #include "src/parser/MarkovAutomatonParser.h" #include "src/parser/PrctlParser.h" #include "src/utility/ErrorHandling.h" -#include "src/formula/Prctl.h" +#include "src/properties/Prctl.h" #include "src/utility/vector.h" #include "src/settings/Settings.h" @@ -285,7 +285,7 @@ void checkPrctlFormulae(storm::modelchecker::prctl::AbstractModelChecker if (s->isSet("prctl")) { std::string const chosenPrctlFile = s->getOptionByLongName("prctl").getArgument(0).getValueAsString(); LOG4CPLUS_INFO(logger, "Parsing prctl file: " << chosenPrctlFile << "."); - std::list>> formulaList = storm::parser::PrctlFileParser::parsePrctlFile(chosenPrctlFile); + std::list>> formulaList = storm::parser::PrctlFileParser::parsePrctlFile(chosenPrctlFile); for (auto formula : formulaList) { formula->check(modelchecker); @@ -338,7 +338,7 @@ void checkPrctlFormulae(storm::modelchecker::prctl::AbstractModelChecker std::string const chosenPrctlFile = s->getOptionByLongName("prctl").getArgument(0).getValueAsString(); LOG4CPLUS_INFO(logger, "Parsing prctl file: " << chosenPrctlFile << "."); - std::list>> formulaList = storm::parser::PrctlFileParser::parsePrctlFile(chosenPrctlFile); + std::list>> formulaList = storm::parser::PrctlFileParser::parsePrctlFile(chosenPrctlFile); // Test for each formula if a counterexample can be generated for it. if(formulaList.size() == 0) { @@ -368,12 +368,12 @@ void checkPrctlFormulae(storm::modelchecker::prctl::AbstractModelChecker for (auto formula : formulaList) { // First check if it is a formula type for which a counterexample can be generated. - if (std::dynamic_pointer_cast>(formula->getChild()).get() == nullptr) { + if (std::dynamic_pointer_cast>(formula->getChild()).get() == nullptr) { LOG4CPLUS_ERROR(logger, "Unexpected kind of formula. Expected a state formula."); continue; } - std::shared_ptr> stateForm = std::static_pointer_cast>(formula->getChild()); + std::shared_ptr> stateForm = std::static_pointer_cast>(formula->getChild()); // Do some output std::cout << "Generating counterexample for formula " << fIndex << ":" << std::endl; @@ -548,7 +548,7 @@ int main(const int argc, const char* argv[]) { // Now parse the property file and receive the list of parsed formulas. std::string const& propertyFile = s->getOptionByLongName("mincmd").getArgumentByName("propertyFile").getValueAsString(); - std::list>> formulaList = storm::parser::PrctlFileParser::parsePrctlFile(propertyFile); + std::list>> formulaList = storm::parser::PrctlFileParser::parsePrctlFile(propertyFile); // Now generate the counterexamples for each formula. for (auto formulaPtr : formulaList) { diff --git a/test/functional/modelchecker/ActionTest.cpp b/test/functional/modelchecker/ActionTest.cpp index 647d8464f..83113a614 100644 --- a/test/functional/modelchecker/ActionTest.cpp +++ b/test/functional/modelchecker/ActionTest.cpp @@ -8,11 +8,11 @@ #include "gtest/gtest.h" #include "storm-config.h" -#include "src/formula/actions/BoundAction.h" -#include "src/formula/actions/FormulaAction.h" -#include "src/formula/actions/InvertAction.h" -#include "src/formula/actions/RangeAction.h" -#include "src/formula/actions/SortAction.h" +#include "src/properties/actions/BoundAction.h" +#include "src/properties/actions/FormulaAction.h" +#include "src/properties/actions/InvertAction.h" +#include "src/properties/actions/RangeAction.h" +#include "src/properties/actions/SortAction.h" #include "src/parser/MarkovAutomatonParser.h" #include "src/parser/DeterministicModelParser.h" @@ -21,7 +21,7 @@ #include "src/solver/GmmxxLinearEquationSolver.h" #include "src/exceptions/InvalidArgumentException.h" -typedef typename storm::property::action::AbstractAction::Result Result; +typedef typename storm::properties::action::AbstractAction::Result Result; TEST(ActionTest, BoundActionFunctionality) { @@ -31,7 +31,7 @@ TEST(ActionTest, BoundActionFunctionality) { // Build the filter input. // Basically the modelchecking result of "F a" on the used DTMC. - std::vector pathResult = mc.checkEventually(storm::property::prctl::Eventually(std::make_shared>("a")), false); + std::vector pathResult = mc.checkEventually(storm::properties::prctl::Eventually(std::make_shared>("a")), false); std::vector stateMap(pathResult.size()); for(uint_fast64_t i = 0; i < pathResult.size(); i++) { stateMap[i] = i; @@ -40,7 +40,7 @@ TEST(ActionTest, BoundActionFunctionality) { // Test the action. // First test that the boundAction build by the empty constructor does not change the selection. - storm::property::action::BoundAction action; + storm::properties::action::BoundAction action; Result result = action.evaluate(input, mc); for(auto value : result.selection) { @@ -48,7 +48,7 @@ TEST(ActionTest, BoundActionFunctionality) { } // Test that using a strict bound can give different results than using a non-strict bound. - action = storm::property::action::BoundAction(storm::property::GREATER, 0); + action = storm::properties::action::BoundAction(storm::properties::GREATER, 0); result = action.evaluate(input, mc); for(uint_fast64_t i = 0; i < result.selection.size()-2; i++) { @@ -58,7 +58,7 @@ TEST(ActionTest, BoundActionFunctionality) { ASSERT_FALSE(result.selection[7]); // Test whether the filter actually uses the selection given by the input. - action = storm::property::action::BoundAction(storm::property::LESS, 0.5); + action = storm::properties::action::BoundAction(storm::properties::LESS, 0.5); result = action.evaluate(result, mc); ASSERT_FALSE(result.selection[0]); @@ -71,7 +71,7 @@ TEST(ActionTest, BoundActionFunctionality) { stateMap[i] = pathResult.size() - i - 1; } - action = storm::property::action::BoundAction(storm::property::GREATER, 0); + action = storm::properties::action::BoundAction(storm::properties::GREATER, 0); result = action.evaluate(input, mc); for(uint_fast64_t i = 0; i < result.selection.size()-2; i++) { @@ -82,8 +82,8 @@ TEST(ActionTest, BoundActionFunctionality) { // Test the functionality for state formulas instead. input.pathResult = std::vector(); - input.stateResult = mc.checkAp(storm::property::prctl::Ap("a")); - action = storm::property::action::BoundAction(storm::property::GREATER, 0.5); + input.stateResult = mc.checkAp(storm::properties::prctl::Ap("a")); + action = storm::properties::action::BoundAction(storm::properties::GREATER, 0.5); result = action.evaluate(input, mc); for(uint_fast64_t i = 0; i < result.selection.size(); i++) { @@ -116,8 +116,8 @@ TEST(ActionTest, BoundActionSafety) { // Build the filter input. // Basically the modelchecking result of "F a" on the used DTMC. - std::vector pathResult = mc.checkEventually(storm::property::prctl::Eventually(std::make_shared>("a")), false); - storm::storage::BitVector stateResult = mc.checkAp(storm::property::prctl::Ap("a")); + std::vector pathResult = mc.checkEventually(storm::properties::prctl::Eventually(std::make_shared>("a")), false); + storm::storage::BitVector stateResult = mc.checkAp(storm::properties::prctl::Ap("a")); std::vector stateMap(pathResult.size()); for(uint_fast64_t i = 0; i < pathResult.size(); i++) { stateMap[i] = i; @@ -125,30 +125,30 @@ TEST(ActionTest, BoundActionSafety) { Result input(storm::storage::BitVector(pathResult.size(), true), stateMap, pathResult, storm::storage::BitVector()); // First, test unusual bounds. - storm::property::action::BoundAction action(storm::property::LESS, -2044); + storm::properties::action::BoundAction action(storm::properties::LESS, -2044); Result result; ASSERT_NO_THROW(result = action.evaluate(input, mc)); ASSERT_EQ(0, result.selection.getNumberOfSetBits()); - action = storm::property::action::BoundAction(storm::property::GREATER_EQUAL, 5879); + action = storm::properties::action::BoundAction(storm::properties::GREATER_EQUAL, 5879); ASSERT_NO_THROW(result = action.evaluate(input, mc)); ASSERT_EQ(0, result.selection.getNumberOfSetBits()); - action = storm::property::action::BoundAction(storm::property::LESS_EQUAL, 5879); + action = storm::properties::action::BoundAction(storm::properties::LESS_EQUAL, 5879); ASSERT_NO_THROW(result = action.evaluate(input, mc)); ASSERT_EQ(result.selection.size(), result.selection.getNumberOfSetBits()); // Now, check the behavior under a undefined comparison type. - action = storm::property::action::BoundAction(static_cast(10), 5879); + action = storm::properties::action::BoundAction(static_cast(10), 5879); ASSERT_THROW(action.toString(), storm::exceptions::InvalidArgumentException); ASSERT_THROW(action.evaluate(input, mc), storm::exceptions::InvalidArgumentException); // Test for a result input with both results filled. // It should put out a warning and use the pathResult. - action = storm::property::action::BoundAction(storm::property::GREATER_EQUAL, 0.5); + action = storm::properties::action::BoundAction(storm::properties::GREATER_EQUAL, 0.5); input.stateResult = stateResult; // To capture the warning, redirect cout and test the written buffer content. @@ -177,8 +177,8 @@ TEST(ActionTest, FormulaActionFunctionality) { // Build the filter input. // Basically the modelchecking result of "F a" on the used DTMC. - std::vector pathResult = mc.checkEventually(storm::property::prctl::Eventually(std::make_shared>("a")), false); - storm::storage::BitVector stateResult = mc.checkAp(storm::property::prctl::Ap("c")); + std::vector pathResult = mc.checkEventually(storm::properties::prctl::Eventually(std::make_shared>("a")), false); + storm::storage::BitVector stateResult = mc.checkAp(storm::properties::prctl::Ap("c")); std::vector stateMap(pathResult.size()); for(uint_fast64_t i = 0; i < pathResult.size(); i++) { stateMap[i] = i; @@ -188,7 +188,7 @@ TEST(ActionTest, FormulaActionFunctionality) { // Test the action. // First test that the empty action does no change to the input. - storm::property::action::FormulaAction action; + storm::properties::action::FormulaAction action; input.selection.set(0,false); ASSERT_NO_THROW(result = action.evaluate(input, mc)); for(uint_fast64_t i = 0; i < pathResult.size(); i++) { @@ -204,7 +204,7 @@ TEST(ActionTest, FormulaActionFunctionality) { input.selection.set(0,true); // Now test the general functionality. - action = storm::property::action::FormulaAction(std::make_shared>(storm::property::LESS, 0.5, std::make_shared>(std::make_shared>("b")))); + action = storm::properties::action::FormulaAction(std::make_shared>(storm::properties::LESS, 0.5, std::make_shared>(std::make_shared>("b")))); ASSERT_NO_THROW(result = action.evaluate(input, mc)); ASSERT_TRUE(result.selection[0]); ASSERT_TRUE(result.selection[1]); @@ -249,7 +249,7 @@ TEST(ActionTest, FormulaActionSafety){ // Build the filter input. // Basically the modelchecking result of "F a" on the used DTMC. - std::vector pathResult = mc.checkEventually(storm::property::prctl::Eventually(std::make_shared>("a")), false); + std::vector pathResult = mc.checkEventually(storm::properties::prctl::Eventually(std::make_shared>("a")), false); std::vector stateMap(pathResult.size()); for(uint_fast64_t i = 0; i < pathResult.size(); i++) { stateMap[i] = i; @@ -258,7 +258,7 @@ TEST(ActionTest, FormulaActionSafety){ Result result; // Check that constructing the action using a nullptr and using an empty constructor leads to the same behavior. - storm::property::action::FormulaAction action(std::shared_ptr>(nullptr)); + storm::properties::action::FormulaAction action(std::shared_ptr>(nullptr)); input.selection.set(0,false); ASSERT_NO_THROW(result = action.evaluate(input, mc)); for(uint_fast64_t i = 0; i < pathResult.size(); i++) { @@ -282,8 +282,8 @@ TEST(ActionTest, InvertActionFunctionality){ // Build the filter input. // Basically the modelchecking result of "F a" on the used DTMC. - std::vector pathResult = mc.checkEventually(storm::property::prctl::Eventually(std::make_shared>("a")), false); - storm::storage::BitVector stateResult = mc.checkAp(storm::property::prctl::Ap("c")); + std::vector pathResult = mc.checkEventually(storm::properties::prctl::Eventually(std::make_shared>("a")), false); + storm::storage::BitVector stateResult = mc.checkAp(storm::properties::prctl::Ap("c")); std::vector stateMap(pathResult.size()); for(uint_fast64_t i = 0; i < pathResult.size(); i++) { stateMap[i] = pathResult.size()-i-1; @@ -292,7 +292,7 @@ TEST(ActionTest, InvertActionFunctionality){ Result result; // Check whether the selection becomes inverted while the rest stays the same. - storm::property::action::InvertAction action; + storm::properties::action::InvertAction action; input.selection.set(0,false); ASSERT_NO_THROW(result = action.evaluate(input, mc)); for(uint_fast64_t i = 0; i < pathResult.size(); i++) { @@ -316,8 +316,8 @@ TEST(ActionTest, RangeActionFunctionality){ // Build the filter input. // Basically the modelchecking result of "F a" on the used DTMC. - std::vector pathResult = mc.checkEventually(storm::property::prctl::Eventually(std::make_shared>("a")), false); - storm::storage::BitVector stateResult = mc.checkAp(storm::property::prctl::Ap("c")); + std::vector pathResult = mc.checkEventually(storm::properties::prctl::Eventually(std::make_shared>("a")), false); + storm::storage::BitVector stateResult = mc.checkAp(storm::properties::prctl::Ap("c")); std::vector stateMap(pathResult.size()); for(uint_fast64_t i = 0; i < pathResult.size(); i++) { stateMap[i] = i; @@ -327,7 +327,7 @@ TEST(ActionTest, RangeActionFunctionality){ // Test if the action selects the first 3 states in relation to the order given by the stateMap. // First in index order. - storm::property::action::RangeAction action(0,2); + storm::properties::action::RangeAction action(0,2); ASSERT_NO_THROW(result = action.evaluate(input, mc)); for(uint_fast64_t i = 0; i < result.selection.size(); i++) { ASSERT_EQ(input.stateMap[i], result.stateMap[i]); @@ -384,7 +384,7 @@ TEST(ActionTest, RangeActionFunctionality){ // Test that specifying and interval of (i,i) selects only state i. for(uint_fast64_t i = 0; i < input.selection.size(); i++) { - action = storm::property::action::RangeAction(i,i); + action = storm::properties::action::RangeAction(i,i); ASSERT_NO_THROW(result = action.evaluate(input, mc)); ASSERT_EQ(1, result.selection.getNumberOfSetBits()); ASSERT_TRUE(result.selection[result.stateMap[i]]); @@ -398,8 +398,8 @@ TEST(ActionTest, RangeActionSafety){ // Build the filter input. // Basically the modelchecking result of "F a" on the used DTMC. - std::vector pathResult = mc.checkEventually(storm::property::prctl::Eventually(std::make_shared>("a")), false); - storm::storage::BitVector stateResult = mc.checkAp(storm::property::prctl::Ap("c")); + std::vector pathResult = mc.checkEventually(storm::properties::prctl::Eventually(std::make_shared>("a")), false); + storm::storage::BitVector stateResult = mc.checkAp(storm::properties::prctl::Ap("c")); std::vector stateMap(pathResult.size()); for(uint_fast64_t i = 0; i < pathResult.size(); i++) { stateMap[i] = i; @@ -414,21 +414,21 @@ TEST(ActionTest, RangeActionSafety){ std::streambuf * sbuf = std::cout.rdbuf(); std::cout.rdbuf(buffer.rdbuf()); - storm::property::action::RangeAction action(0,42); + storm::properties::action::RangeAction action(0,42); ASSERT_NO_THROW(result = action.evaluate(input, mc)); ASSERT_TRUE(result.selection.full()); ASSERT_FALSE(buffer.str().empty()); buffer.str(""); - action = storm::property::action::RangeAction(42,98); + action = storm::properties::action::RangeAction(42,98); ASSERT_NO_THROW(result = action.evaluate(input, mc)); ASSERT_TRUE(result.selection.empty()); ASSERT_FALSE(buffer.str().empty()); std::cout.rdbuf(sbuf); - ASSERT_THROW(storm::property::action::RangeAction(3,1), storm::exceptions::IllegalArgumentValueException); + ASSERT_THROW(storm::properties::action::RangeAction(3,1), storm::exceptions::IllegalArgumentValueException); } TEST(ActionTest, SortActionFunctionality){ @@ -438,8 +438,8 @@ TEST(ActionTest, SortActionFunctionality){ // Build the filter input. // Basically the modelchecking result of "F a" on the used DTMC. - std::vector pathResult = mc.checkEventually(storm::property::prctl::Eventually(std::make_shared>("a")), false); - storm::storage::BitVector stateResult = mc.checkAp(storm::property::prctl::Ap("c")); + std::vector pathResult = mc.checkEventually(storm::properties::prctl::Eventually(std::make_shared>("a")), false); + storm::storage::BitVector stateResult = mc.checkAp(storm::properties::prctl::Ap("c")); std::vector stateMap(pathResult.size()); for(uint_fast64_t i = 0; i < pathResult.size(); i++) { stateMap[i] = pathResult.size()-i-1; @@ -448,7 +448,7 @@ TEST(ActionTest, SortActionFunctionality){ Result result; // Test that sorting preserves everything except the state map. - storm::property::action::SortAction action; + storm::properties::action::SortAction action; ASSERT_NO_THROW(action.toString()); input.selection.set(0,false); ASSERT_NO_THROW(result = action.evaluate(input, mc)); @@ -468,14 +468,14 @@ TEST(ActionTest, SortActionFunctionality){ // 1) index, ascending -> see above // 2) index descending input.selection.set(3,false); - action = storm::property::action::SortAction(storm::property::action::SortAction::INDEX, false); + action = storm::properties::action::SortAction(storm::properties::action::SortAction::INDEX, false); ASSERT_NO_THROW(result = action.evaluate(input, mc)); for(uint_fast64_t i = 0; i < pathResult.size(); i++) { ASSERT_EQ(pathResult.size()-i-1, result.stateMap[i]); } // 3) value, ascending - action = storm::property::action::SortAction(storm::property::action::SortAction::VALUE); + action = storm::properties::action::SortAction(storm::properties::action::SortAction::VALUE); ASSERT_NO_THROW(result = action.evaluate(input, mc)); ASSERT_EQ(6, result.stateMap[0]); ASSERT_EQ(7, result.stateMap[1]); @@ -487,7 +487,7 @@ TEST(ActionTest, SortActionFunctionality){ ASSERT_EQ(5, result.stateMap[7]); // 3) value, decending - action = storm::property::action::SortAction(storm::property::action::SortAction::VALUE, false); + action = storm::properties::action::SortAction(storm::properties::action::SortAction::VALUE, false); ASSERT_NO_THROW(result = action.evaluate(input, mc)); ASSERT_EQ(5, result.stateMap[0]); ASSERT_EQ(2, result.stateMap[1]); @@ -502,7 +502,7 @@ TEST(ActionTest, SortActionFunctionality){ input.pathResult = std::vector(); input.stateResult = stateResult; - action = storm::property::action::SortAction(storm::property::action::SortAction::VALUE); + action = storm::properties::action::SortAction(storm::properties::action::SortAction::VALUE); ASSERT_NO_THROW(result = action.evaluate(input, mc)); ASSERT_EQ(5, result.stateMap[0]); ASSERT_EQ(6, result.stateMap[1]); @@ -513,7 +513,7 @@ TEST(ActionTest, SortActionFunctionality){ ASSERT_EQ(3, result.stateMap[6]); ASSERT_EQ(4, result.stateMap[7]); - action = storm::property::action::SortAction(storm::property::action::SortAction::VALUE, false); + action = storm::properties::action::SortAction(storm::properties::action::SortAction::VALUE, false); ASSERT_NO_THROW(result = action.evaluate(input, mc)); ASSERT_EQ(0, result.stateMap[0]); ASSERT_EQ(1, result.stateMap[1]); @@ -528,9 +528,9 @@ TEST(ActionTest, SortActionFunctionality){ input.stateResult = storm::storage::BitVector(); input.pathResult = pathResult; - action = storm::property::action::SortAction(storm::property::action::SortAction::INDEX); + action = storm::properties::action::SortAction(storm::properties::action::SortAction::INDEX); ASSERT_NO_THROW(input = action.evaluate(input, mc)); - action = storm::property::action::SortAction(storm::property::action::SortAction::VALUE); + action = storm::properties::action::SortAction(storm::properties::action::SortAction::VALUE); ASSERT_NO_THROW(result = action.evaluate(input, mc)); ASSERT_EQ(6, result.stateMap[0]); ASSERT_EQ(7, result.stateMap[1]); @@ -551,8 +551,8 @@ TEST(ActionTest, SortActionSafety){ // Build the filter input. // Basically the modelchecking result of "F a" on the used DTMC. - std::vector pathResult = mc.checkEventually(storm::property::prctl::Eventually(std::make_shared>("a")), false); - storm::storage::BitVector stateResult = mc.checkAp(storm::property::prctl::Ap("c")); + std::vector pathResult = mc.checkEventually(storm::properties::prctl::Eventually(std::make_shared>("a")), false); + storm::storage::BitVector stateResult = mc.checkAp(storm::properties::prctl::Ap("c")); std::vector stateMap(pathResult.size()); for(uint_fast64_t i = 0; i < pathResult.size(); i++) { stateMap[i] = pathResult.size()-i-1; @@ -560,7 +560,7 @@ TEST(ActionTest, SortActionSafety){ Result input(storm::storage::BitVector(pathResult.size(), true), stateMap, pathResult, stateResult); Result result; - storm::property::action::SortAction action(storm::property::action::SortAction::VALUE); + storm::properties::action::SortAction action(storm::properties::action::SortAction::VALUE); ASSERT_NO_THROW(result = action.evaluate(input, mc)); ASSERT_EQ(6, result.stateMap[0]); ASSERT_EQ(7, result.stateMap[1]); diff --git a/test/functional/modelchecker/EigenDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/EigenDtmcPrctlModelCheckerTest.cpp index 0d36a1d77..8cb8d131d 100644 --- a/test/functional/modelchecker/EigenDtmcPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/EigenDtmcPrctlModelCheckerTest.cpp @@ -21,9 +21,9 @@ TEST(EigenDtmcPrctlModelCheckerTest, Die) { storm::modelChecker::EigenDtmcPrctlModelChecker mc(*dtmc); - storm::property::Ap* apFormula = new storm::property::Ap("one"); - storm::property::Eventually* eventuallyFormula = new storm::property::Eventually(apFormula); - storm::property::ProbabilisticNoBoundOperator* probFormula = new storm::property::ProbabilisticNoBoundOperator(eventuallyFormula); + storm::properties::Ap* apFormula = new storm::properties::Ap("one"); + storm::properties::Eventually* eventuallyFormula = new storm::properties::Eventually(apFormula); + storm::properties::ProbabilisticNoBoundOperator* probFormula = new storm::properties::ProbabilisticNoBoundOperator(eventuallyFormula); std::vector* result = probFormula->check(mc); @@ -32,9 +32,9 @@ TEST(EigenDtmcPrctlModelCheckerTest, Die) { delete probFormula; delete result; - apFormula = new storm::property::Ap("two"); - eventuallyFormula = new storm::property::Eventually(apFormula); - probFormula = new storm::property::ProbabilisticNoBoundOperator(eventuallyFormula); + apFormula = new storm::properties::Ap("two"); + eventuallyFormula = new storm::properties::Eventually(apFormula); + probFormula = new storm::properties::ProbabilisticNoBoundOperator(eventuallyFormula); result = probFormula->check(mc); @@ -43,9 +43,9 @@ TEST(EigenDtmcPrctlModelCheckerTest, Die) { delete probFormula; delete result; - apFormula = new storm::property::Ap("three"); - eventuallyFormula = new storm::property::Eventually(apFormula); - probFormula = new storm::property::ProbabilisticNoBoundOperator(eventuallyFormula); + apFormula = new storm::properties::Ap("three"); + eventuallyFormula = new storm::properties::Eventually(apFormula); + probFormula = new storm::properties::ProbabilisticNoBoundOperator(eventuallyFormula); result = probFormula->check(mc); @@ -54,9 +54,9 @@ TEST(EigenDtmcPrctlModelCheckerTest, Die) { delete probFormula; delete result; - storm::property::Ap* done = new storm::property::Ap("done"); - storm::property::ReachabilityReward* reachabilityRewardFormula = new storm::property::ReachabilityReward(done); - storm::property::RewardNoBoundOperator* rewardFormula = new storm::property::RewardNoBoundOperator(reachabilityRewardFormula); + storm::properties::Ap* done = new storm::properties::Ap("done"); + storm::properties::ReachabilityReward* reachabilityRewardFormula = new storm::properties::ReachabilityReward(done); + storm::properties::RewardNoBoundOperator* rewardFormula = new storm::properties::RewardNoBoundOperator(reachabilityRewardFormula); result = rewardFormula->check(mc); @@ -82,9 +82,9 @@ TEST(EigenDtmcPrctlModelCheckerTest, Crowds) { storm::modelChecker::EigenDtmcPrctlModelChecker mc(*dtmc); - storm::property::Ap* apFormula = new storm::property::Ap("observe0Greater1"); - storm::property::Eventually* eventuallyFormula = new storm::property::Eventually(apFormula); - storm::property::ProbabilisticNoBoundOperator* probFormula = new storm::property::ProbabilisticNoBoundOperator(eventuallyFormula); + storm::properties::Ap* apFormula = new storm::properties::Ap("observe0Greater1"); + storm::properties::Eventually* eventuallyFormula = new storm::properties::Eventually(apFormula); + storm::properties::ProbabilisticNoBoundOperator* probFormula = new storm::properties::ProbabilisticNoBoundOperator(eventuallyFormula); std::vector* result = probFormula->check(mc); @@ -93,9 +93,9 @@ TEST(EigenDtmcPrctlModelCheckerTest, Crowds) { delete probFormula; delete result; - apFormula = new storm::property::Ap("observeIGreater1"); - eventuallyFormula = new storm::property::Eventually(apFormula); - probFormula = new storm::property::ProbabilisticNoBoundOperator(eventuallyFormula); + apFormula = new storm::properties::Ap("observeIGreater1"); + eventuallyFormula = new storm::properties::Eventually(apFormula); + probFormula = new storm::properties::ProbabilisticNoBoundOperator(eventuallyFormula); result = probFormula->check(mc); @@ -104,9 +104,9 @@ TEST(EigenDtmcPrctlModelCheckerTest, Crowds) { delete probFormula; delete result; - apFormula = new storm::property::Ap("observeOnlyTrueSender"); - eventuallyFormula = new storm::property::Eventually(apFormula); - probFormula = new storm::property::ProbabilisticNoBoundOperator(eventuallyFormula); + apFormula = new storm::properties::Ap("observeOnlyTrueSender"); + eventuallyFormula = new storm::properties::Eventually(apFormula); + probFormula = new storm::properties::ProbabilisticNoBoundOperator(eventuallyFormula); result = probFormula->check(mc); @@ -131,9 +131,9 @@ TEST(EigenDtmcPrctlModelCheckerTest, SynchronousLeader) { storm::modelChecker::EigenDtmcPrctlModelChecker mc(*dtmc); - storm::property::Ap* apFormula = new storm::property::Ap("elected"); - storm::property::Eventually* eventuallyFormula = new storm::property::Eventually(apFormula); - storm::property::ProbabilisticNoBoundOperator* probFormula = new storm::property::ProbabilisticNoBoundOperator(eventuallyFormula); + storm::properties::Ap* apFormula = new storm::properties::Ap("elected"); + storm::properties::Eventually* eventuallyFormula = new storm::properties::Eventually(apFormula); + storm::properties::ProbabilisticNoBoundOperator* probFormula = new storm::properties::ProbabilisticNoBoundOperator(eventuallyFormula); std::vector* result = probFormula->check(mc); @@ -142,9 +142,9 @@ TEST(EigenDtmcPrctlModelCheckerTest, SynchronousLeader) { delete probFormula; delete result; - apFormula = new storm::property::Ap("elected"); - storm::property::BoundedUntil* boundedUntilFormula = new storm::property::BoundedUntil(new storm::property::Ap("true"), apFormula, 20); - probFormula = new storm::property::ProbabilisticNoBoundOperator(boundedUntilFormula); + apFormula = new storm::properties::Ap("elected"); + storm::properties::BoundedUntil* boundedUntilFormula = new storm::properties::BoundedUntil(new storm::properties::Ap("true"), apFormula, 20); + probFormula = new storm::properties::ProbabilisticNoBoundOperator(boundedUntilFormula); result = probFormula->check(mc); @@ -153,9 +153,9 @@ TEST(EigenDtmcPrctlModelCheckerTest, SynchronousLeader) { delete probFormula; delete result; - apFormula = new storm::property::Ap("elected"); - storm::property::ReachabilityReward* reachabilityRewardFormula = new storm::property::ReachabilityReward(apFormula); - storm::property::RewardNoBoundOperator* rewardFormula = new storm::property::RewardNoBoundOperator(reachabilityRewardFormula); + apFormula = new storm::properties::Ap("elected"); + storm::properties::ReachabilityReward* reachabilityRewardFormula = new storm::properties::ReachabilityReward(apFormula); + storm::properties::RewardNoBoundOperator* rewardFormula = new storm::properties::RewardNoBoundOperator(reachabilityRewardFormula); result = rewardFormula->check(mc); diff --git a/test/functional/modelchecker/FilterTest.cpp b/test/functional/modelchecker/FilterTest.cpp index ffbd11978..f85382bbb 100644 --- a/test/functional/modelchecker/FilterTest.cpp +++ b/test/functional/modelchecker/FilterTest.cpp @@ -13,17 +13,17 @@ #include "src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h" #include "src/solver/GmmxxLinearEquationSolver.h" #include "src/solver/GmmxxNondeterministicLinearEquationSolver.h" -#include "src/formula/prctl/PrctlFilter.h" -#include "src/formula/csl/CslFilter.h" -#include "src/formula/ltl/LtlFilter.h" +#include "src/properties/prctl/PrctlFilter.h" +#include "src/properties/csl/CslFilter.h" +#include "src/properties/ltl/LtlFilter.h" #include "src/parser/PrctlParser.h" #include "src/parser/CslParser.h" #include "src/parser/MarkovAutomatonParser.h" -#include "src/formula/actions/InvertAction.h" +#include "src/properties/actions/InvertAction.h" #include -typedef typename storm::property::action::AbstractAction::Result Result; +typedef typename storm::properties::action::AbstractAction::Result Result; TEST(PrctlFilterTest, generalFunctionality) { // Test filter queries of increasing complexity. @@ -34,7 +34,7 @@ TEST(PrctlFilterTest, generalFunctionality) { // Find the best valued state to finally reach a 'b' state. std::string input = "filter[sort(value, descending); range(0,0)](F b)"; - std::shared_ptr> formula(nullptr); + std::shared_ptr> formula(nullptr); ASSERT_NO_THROW( formula = storm::parser::PrctlParser::parsePrctlFormula(input) ); @@ -151,26 +151,26 @@ TEST(PrctlFilterTest, Safety) { storm::modelchecker::prctl::SparseDtmcPrctlModelChecker mc(model, new storm::solver::GmmxxLinearEquationSolver()); // Make a stub formula as child. - auto apFormula = std::make_shared>("a"); + auto apFormula = std::make_shared>("a"); // Test the filter for nullptr action handling. - auto formula = std::make_shared>(apFormula, nullptr); + auto formula = std::make_shared>(apFormula, nullptr); ASSERT_EQ(0, formula->getActionCount()); ASSERT_NO_THROW(formula->evaluate(mc)); // Repeat with vector containing only one action but three nullptr. - std::vector>> actions(4, nullptr); - actions[1] = std::make_shared>(); + std::vector>> actions(4, nullptr); + actions[1] = std::make_shared>(); - formula = std::make_shared>(apFormula, actions); + formula = std::make_shared>(apFormula, actions); ASSERT_EQ(1, formula->getActionCount()); ASSERT_NO_THROW(formula->evaluate(mc)); // Test the filter for nullptr child formula handling. // It sholud not write anything to the standard out and return an empty result. - formula = std::make_shared>(); + formula = std::make_shared>(); Result result; // To capture the output, redirect cout and test the written buffer content. @@ -200,7 +200,7 @@ TEST(CslFilterTest, generalFunctionality) { // Find the best valued state to finally reach a 'r1' state. std::string input = "filter[max; sort(value, descending); range(0,0)](F r1)"; - std::shared_ptr> formula(nullptr); + std::shared_ptr> formula(nullptr); ASSERT_NO_THROW( formula = storm::parser::CslParser::parseCslFormula(input) ); @@ -317,26 +317,26 @@ TEST(CslFilterTest, Safety) { storm::modelchecker::csl::SparseMarkovAutomatonCslModelChecker mc(model, std::make_shared>()); // Make a stub formula as child. - auto apFormula = std::make_shared>("r1"); + auto apFormula = std::make_shared>("r1"); // Test the filter for nullptr action handling. - auto formula = std::make_shared>(apFormula, nullptr, storm::property::MAXIMIZE); + auto formula = std::make_shared>(apFormula, nullptr, storm::properties::MAXIMIZE); ASSERT_NO_THROW(formula->evaluate(mc)); ASSERT_EQ(0, formula->getActionCount()); // Repeat with vector containing only one action but three nullptr. - std::vector>> actions(4, nullptr); - actions[1] = std::make_shared>(); + std::vector>> actions(4, nullptr); + actions[1] = std::make_shared>(); - formula = std::make_shared>(apFormula, actions, storm::property::MAXIMIZE); + formula = std::make_shared>(apFormula, actions, storm::properties::MAXIMIZE); ASSERT_EQ(1, formula->getActionCount()); ASSERT_NO_THROW(formula->evaluate(mc)); // Test the filter for nullptr child formula handling. // It sholud not write anything to the standard out and return an empty result. - formula = std::make_shared>(); + formula = std::make_shared>(); Result result; // To capture the output, redirect cout and test the written buffer content. diff --git a/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp index 15d0a7814..183072ce2 100644 --- a/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp @@ -22,29 +22,29 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, Die) { storm::modelchecker::prctl::SparseDtmcPrctlModelChecker mc(*dtmc, new storm::solver::GmmxxLinearEquationSolver()); - auto apFormula = std::make_shared>("one"); - auto eventuallyFormula = std::make_shared>(apFormula); + auto apFormula = std::make_shared>("one"); + auto eventuallyFormula = std::make_shared>(apFormula); std::vector result = eventuallyFormula->check(mc, false); ASSERT_LT(std::abs(result[0] - ((double)1.0/6.0)), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); - apFormula = std::make_shared>("two"); - eventuallyFormula = std::make_shared>(apFormula); + apFormula = std::make_shared>("two"); + eventuallyFormula = std::make_shared>(apFormula); result = eventuallyFormula->check(mc, false); ASSERT_LT(std::abs(result[0] - ((double)1.0/6.0)), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); - apFormula = std::make_shared>("three"); - eventuallyFormula = std::make_shared>(apFormula); + apFormula = std::make_shared>("three"); + eventuallyFormula = std::make_shared>(apFormula); result = eventuallyFormula->check(mc, false); ASSERT_LT(std::abs(result[0] - ((double)1.0/6.0)), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); - auto done = std::make_shared>("done"); - auto reachabilityRewardFormula = std::make_shared>(done); + auto done = std::make_shared>("done"); + auto reachabilityRewardFormula = std::make_shared>(done); result = reachabilityRewardFormula->check(mc, false); @@ -66,22 +66,22 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, Crowds) { storm::modelchecker::prctl::SparseDtmcPrctlModelChecker mc(*dtmc, new storm::solver::GmmxxLinearEquationSolver()); - auto apFormula = std::make_shared>("observe0Greater1"); - auto eventuallyFormula = std::make_shared>(apFormula); + auto apFormula = std::make_shared>("observe0Greater1"); + auto eventuallyFormula = std::make_shared>(apFormula); std::vector result = eventuallyFormula->check(mc, false); ASSERT_LT(std::abs(result[0] - 0.3328800375801578281), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); - apFormula = std::make_shared>("observeIGreater1"); - eventuallyFormula = std::make_shared>(apFormula); + apFormula = std::make_shared>("observeIGreater1"); + eventuallyFormula = std::make_shared>(apFormula); result = eventuallyFormula->check(mc, false); ASSERT_LT(std::abs(result[0] - 0.1522194965), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); - apFormula = std::make_shared>("observeOnlyTrueSender"); - eventuallyFormula = std::make_shared>(apFormula); + apFormula = std::make_shared>("observeOnlyTrueSender"); + eventuallyFormula = std::make_shared>(apFormula); result = eventuallyFormula->check(mc, false); @@ -102,22 +102,22 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, SynchronousLeader) { storm::modelchecker::prctl::SparseDtmcPrctlModelChecker mc(*dtmc, new storm::solver::GmmxxLinearEquationSolver()); - auto apFormula = std::make_shared>("elected"); - auto eventuallyFormula = std::make_shared>(apFormula); + auto apFormula = std::make_shared>("elected"); + auto eventuallyFormula = std::make_shared>(apFormula); std::vector result = eventuallyFormula->check(mc, false); ASSERT_LT(std::abs(result[0] - 1.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); - apFormula = std::make_shared>("elected"); - auto boundedUntilFormula = std::make_shared>(std::make_shared>("true"), apFormula, 20); + apFormula = std::make_shared>("elected"); + auto boundedUntilFormula = std::make_shared>(std::make_shared>("true"), apFormula, 20); result = boundedUntilFormula->check(mc, false); ASSERT_LT(std::abs(result[0] - 0.9999965911265462636), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); - apFormula = std::make_shared>("elected"); - auto reachabilityRewardFormula = std::make_shared>(apFormula); + apFormula = std::make_shared>("elected"); + auto reachabilityRewardFormula = std::make_shared>(apFormula); result = reachabilityRewardFormula->check(mc, false); diff --git a/test/functional/modelchecker/SparseMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/SparseMdpPrctlModelCheckerTest.cpp index bc423ad02..0cb31fcec 100644 --- a/test/functional/modelchecker/SparseMdpPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/SparseMdpPrctlModelCheckerTest.cpp @@ -19,8 +19,8 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) { storm::modelchecker::prctl::SparseMdpPrctlModelChecker mc(*mdp, std::shared_ptr>(new storm::solver::NativeNondeterministicLinearEquationSolver())); - auto apFormula = std::make_shared>("two"); - auto eventuallyFormula = std::make_shared>(apFormula); + auto apFormula = std::make_shared>("two"); + auto eventuallyFormula = std::make_shared>(apFormula); std::vector result = mc.checkOptimizingOperator(*eventuallyFormula, true); @@ -30,8 +30,8 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) { ASSERT_LT(std::abs(result[0] - 0.0277777612209320068), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); - apFormula = std::make_shared>("three"); - eventuallyFormula = std::make_shared>(apFormula); + apFormula = std::make_shared>("three"); + eventuallyFormula = std::make_shared>(apFormula); result = mc.checkOptimizingOperator(*eventuallyFormula, true); @@ -41,8 +41,8 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) { ASSERT_LT(std::abs(result[0] - 0.0555555224418640136), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); - apFormula = std::make_shared>("four"); - eventuallyFormula = std::make_shared>(apFormula); + apFormula = std::make_shared>("four"); + eventuallyFormula = std::make_shared>(apFormula); result = mc.checkOptimizingOperator(*eventuallyFormula, true); @@ -52,8 +52,8 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) { ASSERT_LT(std::abs(result[0] - 0.083333283662796020508), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); - apFormula = std::make_shared>("done"); - auto reachabilityRewardFormula = std::make_shared>(apFormula); + apFormula = std::make_shared>("done"); + auto reachabilityRewardFormula = std::make_shared>(apFormula); result = mc.checkOptimizingOperator(*reachabilityRewardFormula, true); @@ -71,8 +71,8 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) { storm::modelchecker::prctl::SparseMdpPrctlModelChecker stateRewardModelChecker(*stateRewardMdp, std::shared_ptr>(new storm::solver::NativeNondeterministicLinearEquationSolver())); - apFormula = std::make_shared>("done"); - reachabilityRewardFormula = std::make_shared>(apFormula); + apFormula = std::make_shared>("done"); + reachabilityRewardFormula = std::make_shared>(apFormula); result = stateRewardModelChecker.checkOptimizingOperator(*reachabilityRewardFormula, true); @@ -90,8 +90,8 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) { storm::modelchecker::prctl::SparseMdpPrctlModelChecker stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp, std::shared_ptr>(new storm::solver::NativeNondeterministicLinearEquationSolver())); - apFormula = std::make_shared>("done"); - reachabilityRewardFormula = std::make_shared>(apFormula); + apFormula = std::make_shared>("done"); + reachabilityRewardFormula = std::make_shared>(apFormula); result = stateAndTransitionRewardModelChecker.checkOptimizingOperator(*reachabilityRewardFormula, true); @@ -115,8 +115,8 @@ TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) { storm::modelchecker::prctl::SparseMdpPrctlModelChecker mc(*mdp, std::shared_ptr>(new storm::solver::NativeNondeterministicLinearEquationSolver())); - auto apFormula = std::make_shared>("elected"); - auto eventuallyFormula = std::make_shared>(apFormula); + auto apFormula = std::make_shared>("elected"); + auto eventuallyFormula = std::make_shared>(apFormula); std::vector result = mc.checkOptimizingOperator(*eventuallyFormula, true); @@ -126,8 +126,8 @@ TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) { ASSERT_LT(std::abs(result[0] - 1), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); - apFormula = std::make_shared>("elected"); - auto boundedEventuallyFormula = std::make_shared>(apFormula, 25); + apFormula = std::make_shared>("elected"); + auto boundedEventuallyFormula = std::make_shared>(apFormula, 25); result = mc.checkOptimizingOperator(*boundedEventuallyFormula, true); @@ -137,8 +137,8 @@ TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) { ASSERT_LT(std::abs(result[0] - 0.0625), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); - apFormula = std::make_shared>("elected"); - auto reachabilityRewardFormula = std::make_shared>(apFormula); + apFormula = std::make_shared>("elected"); + auto reachabilityRewardFormula = std::make_shared>(apFormula); result = mc.checkOptimizingOperator(*reachabilityRewardFormula, true); diff --git a/test/functional/parser/CslParserTest.cpp b/test/functional/parser/CslParserTest.cpp index ecff80e4d..42b805ac4 100644 --- a/test/functional/parser/CslParserTest.cpp +++ b/test/functional/parser/CslParserTest.cpp @@ -9,13 +9,13 @@ #include "storm-config.h" #include "src/parser/CslParser.h" #include "src/exceptions/WrongFormatException.h" -#include "src/formula/actions/FormulaAction.h" -#include "src/formula/actions/InvertAction.h" -#include "src/formula/actions/SortAction.h" -#include "src/formula/actions/RangeAction.h" -#include "src/formula/actions/BoundAction.h" +#include "src/properties/actions/FormulaAction.h" +#include "src/properties/actions/InvertAction.h" +#include "src/properties/actions/SortAction.h" +#include "src/properties/actions/RangeAction.h" +#include "src/properties/actions/BoundAction.h" -namespace csl = storm::property::csl; +namespace csl = storm::properties::csl; TEST(CslParserTest, parseApOnlyTest) { std::string input = "ap"; @@ -70,7 +70,7 @@ TEST(CslParserTest, parsePathFormulaTest) { ASSERT_NE(std::dynamic_pointer_cast>(nextFormula->getChild()).get(), nullptr); auto probBoundFormula = std::dynamic_pointer_cast>(nextFormula->getChild()); ASSERT_EQ(0.9, probBoundFormula->getBound()); - ASSERT_EQ(storm::property::LESS, probBoundFormula->getComparisonOperator()); + ASSERT_EQ(storm::properties::LESS, probBoundFormula->getComparisonOperator()); ASSERT_FALSE(probBoundFormula->isPropositional()); ASSERT_TRUE(probBoundFormula->isProbEventuallyAP()); @@ -99,9 +99,9 @@ TEST(CslParserTest, parseProbabilisticFormulaTest) { // The parser did not falsely recognize the input as a comment. ASSERT_NE(formula.get(), nullptr); - auto op = std::dynamic_pointer_cast>(formula->getChild()); + auto op = std::dynamic_pointer_cast>(formula->getChild()); ASSERT_NE(op.get(), nullptr); - ASSERT_EQ(storm::property::GREATER, op->getComparisonOperator()); + ASSERT_EQ(storm::properties::GREATER, op->getComparisonOperator()); ASSERT_EQ(0.5, op->getBound()); ASSERT_FALSE(op->isPropositional()); ASSERT_TRUE(op->isProbEventuallyAP()); @@ -120,9 +120,9 @@ TEST(CslParserTest, parseSteadyStateBoundFormulaTest) { // The parser did not falsely recognize the input as a comment. ASSERT_NE(formula.get(), nullptr); - auto op = std::dynamic_pointer_cast>(formula->getChild()); + auto op = std::dynamic_pointer_cast>(formula->getChild()); ASSERT_NE(op.get(), nullptr); - ASSERT_EQ(storm::property::GREATER_EQUAL, op->getComparisonOperator()); + ASSERT_EQ(storm::properties::GREATER_EQUAL, op->getComparisonOperator()); ASSERT_EQ(15.0, op->getBound()); ASSERT_FALSE(op->isPropositional()); ASSERT_FALSE(op->isProbEventuallyAP()); @@ -193,14 +193,14 @@ TEST(CslParserTest, parseCslFilterTest) { // The parser did not falsely recognize the input as a comment. ASSERT_NE(formula, nullptr); - ASSERT_EQ(storm::property::MAXIMIZE, formula->getOptimizingOperator()); + ASSERT_EQ(storm::properties::MAXIMIZE, formula->getOptimizingOperator()); ASSERT_EQ(5, formula->getActionCount()); - ASSERT_NE(std::dynamic_pointer_cast>(formula->getAction(0)).get(), nullptr); - ASSERT_NE(std::dynamic_pointer_cast>(formula->getAction(1)).get(), nullptr); - ASSERT_NE(std::dynamic_pointer_cast>(formula->getAction(2)).get(), nullptr); - ASSERT_NE(std::dynamic_pointer_cast>(formula->getAction(3)).get(), nullptr); - ASSERT_NE(std::dynamic_pointer_cast>(formula->getAction(4)).get(), nullptr); + ASSERT_NE(std::dynamic_pointer_cast>(formula->getAction(0)).get(), nullptr); + ASSERT_NE(std::dynamic_pointer_cast>(formula->getAction(1)).get(), nullptr); + ASSERT_NE(std::dynamic_pointer_cast>(formula->getAction(2)).get(), nullptr); + ASSERT_NE(std::dynamic_pointer_cast>(formula->getAction(3)).get(), nullptr); + ASSERT_NE(std::dynamic_pointer_cast>(formula->getAction(4)).get(), nullptr); ASSERT_FALSE(formula->getChild()->isPropositional()); ASSERT_FALSE(formula->getChild()->isProbEventuallyAP()); diff --git a/test/functional/parser/LtlParserTest.cpp b/test/functional/parser/LtlParserTest.cpp index e44f84f0e..d13c48688 100644 --- a/test/functional/parser/LtlParserTest.cpp +++ b/test/functional/parser/LtlParserTest.cpp @@ -9,16 +9,16 @@ #include "storm-config.h" #include "src/parser/LtlParser.h" #include "src/exceptions/WrongFormatException.h" -#include "src/formula/actions/InvertAction.h" -#include "src/formula/actions/SortAction.h" -#include "src/formula/actions/RangeAction.h" -#include "src/formula/actions/BoundAction.h" +#include "src/properties/actions/InvertAction.h" +#include "src/properties/actions/SortAction.h" +#include "src/properties/actions/RangeAction.h" +#include "src/properties/actions/BoundAction.h" -namespace ltl = storm::property::ltl; +namespace ltl = storm::properties::ltl; TEST(LtlParserTest, parseApOnlyTest) { std::string input = "ap"; - std::shared_ptr> formula(nullptr); + std::shared_ptr> formula(nullptr); ASSERT_NO_THROW( formula = storm::parser::LtlParser::parseLtlFormula(input); ); @@ -87,7 +87,7 @@ TEST(LtlParserTest, parseBoundedEventuallyFormulaTest) { ASSERT_FALSE(formula->getChild()->isPropositional()); - std::shared_ptr> op = std::dynamic_pointer_cast>(formula->getChild()); + std::shared_ptr> op = std::dynamic_pointer_cast>(formula->getChild()); ASSERT_NE(op.get(), nullptr); ASSERT_EQ(static_cast(5), op->getBound()); @@ -106,7 +106,7 @@ TEST(LtlParserTest, parseBoundedUntilFormulaTest) { ASSERT_FALSE(formula->getChild()->isPropositional()); - std::shared_ptr> op = std::dynamic_pointer_cast>(formula->getChild()); + std::shared_ptr> op = std::dynamic_pointer_cast>(formula->getChild()); ASSERT_NE(op.get(), nullptr); ASSERT_EQ(static_cast(3), op->getBound()); @@ -126,13 +126,13 @@ TEST(LtlParserTest, parseLtlFilterTest) { ASSERT_FALSE(formula->getChild()->isPropositional()); - ASSERT_EQ(storm::property::MAXIMIZE, formula->getOptimizingOperator()); + ASSERT_EQ(storm::properties::MAXIMIZE, formula->getOptimizingOperator()); ASSERT_EQ(4, formula->getActionCount()); - ASSERT_NE(std::dynamic_pointer_cast>(formula->getAction(0)).get(), nullptr); - ASSERT_NE(std::dynamic_pointer_cast>(formula->getAction(1)).get(), nullptr); - ASSERT_NE(std::dynamic_pointer_cast>(formula->getAction(2)).get(), nullptr); - ASSERT_NE(std::dynamic_pointer_cast>(formula->getAction(3)).get(), nullptr); + ASSERT_NE(std::dynamic_pointer_cast>(formula->getAction(0)).get(), nullptr); + ASSERT_NE(std::dynamic_pointer_cast>(formula->getAction(1)).get(), nullptr); + ASSERT_NE(std::dynamic_pointer_cast>(formula->getAction(2)).get(), nullptr); + ASSERT_NE(std::dynamic_pointer_cast>(formula->getAction(3)).get(), nullptr); // The input was parsed correctly. ASSERT_EQ("filter[max; invert; bound(<, 0.500000); sort(value, ascending); range(0, 3)](X a)", formula->toString()); diff --git a/test/functional/parser/PrctlParserTest.cpp b/test/functional/parser/PrctlParserTest.cpp index 1a63495d0..22e52e7d1 100644 --- a/test/functional/parser/PrctlParserTest.cpp +++ b/test/functional/parser/PrctlParserTest.cpp @@ -10,13 +10,13 @@ #include "storm-config.h" #include "src/parser/PrctlParser.h" #include "src/exceptions/WrongFormatException.h" -#include "src/formula/actions/FormulaAction.h" -#include "src/formula/actions/InvertAction.h" -#include "src/formula/actions/SortAction.h" -#include "src/formula/actions/RangeAction.h" -#include "src/formula/actions/BoundAction.h" +#include "src/properties/actions/FormulaAction.h" +#include "src/properties/actions/InvertAction.h" +#include "src/properties/actions/SortAction.h" +#include "src/properties/actions/RangeAction.h" +#include "src/properties/actions/BoundAction.h" -namespace prctl = storm::property::prctl; +namespace prctl = storm::properties::prctl; TEST(PrctlParserTest, parseApOnlyTest) { std::string input = "ap"; @@ -71,7 +71,7 @@ TEST(PrctlParserTest, parsePathFormulaTest) { ASSERT_NE(std::dynamic_pointer_cast>(nextFormula->getChild()).get(), nullptr); auto probBoundFormula = std::dynamic_pointer_cast>(nextFormula->getChild()); ASSERT_EQ(0.9, probBoundFormula->getBound()); - ASSERT_EQ(storm::property::LESS, probBoundFormula->getComparisonOperator()); + ASSERT_EQ(storm::properties::LESS, probBoundFormula->getComparisonOperator()); ASSERT_FALSE(probBoundFormula->isPropositional()); ASSERT_TRUE(probBoundFormula->isProbEventuallyAP()); @@ -103,7 +103,7 @@ TEST(PrctlParserTest, parseProbabilisticFormulaTest) { ASSERT_NE(std::dynamic_pointer_cast>(formula->getChild()).get(), nullptr); std::shared_ptr> op = std::static_pointer_cast>(formula->getChild()); - ASSERT_EQ(storm::property::GREATER, op->getComparisonOperator()); + ASSERT_EQ(storm::properties::GREATER, op->getComparisonOperator()); ASSERT_EQ(0.5, op->getBound()); ASSERT_FALSE(op->isPropositional()); ASSERT_TRUE(op->isProbEventuallyAP()); @@ -125,7 +125,7 @@ TEST(PrctlParserTest, parseRewardFormulaTest) { ASSERT_NE(std::dynamic_pointer_cast>(formula->getChild()).get(), nullptr); std::shared_ptr> op = std::static_pointer_cast>(formula->getChild()); - ASSERT_EQ(storm::property::GREATER_EQUAL, op->getComparisonOperator()); + ASSERT_EQ(storm::properties::GREATER_EQUAL, op->getComparisonOperator()); ASSERT_EQ(15.0, op->getBound()); ASSERT_FALSE(op->isPropositional()); ASSERT_FALSE(op->isProbEventuallyAP()); @@ -195,14 +195,14 @@ TEST(PrctlParserTest, parsePrctlFilterTest) { // The parser did not falsely recognize the input as a comment. ASSERT_NE(formula.get(), nullptr); - ASSERT_EQ(storm::property::MAXIMIZE, formula->getOptimizingOperator()); + ASSERT_EQ(storm::properties::MAXIMIZE, formula->getOptimizingOperator()); ASSERT_EQ(5, formula->getActionCount()); - ASSERT_NE(std::dynamic_pointer_cast>(formula->getAction(0)).get(), nullptr); - ASSERT_NE(std::dynamic_pointer_cast>(formula->getAction(1)).get(), nullptr); - ASSERT_NE(std::dynamic_pointer_cast>(formula->getAction(2)).get(), nullptr); - ASSERT_NE(std::dynamic_pointer_cast>(formula->getAction(3)).get(), nullptr); - ASSERT_NE(std::dynamic_pointer_cast>(formula->getAction(4)).get(), nullptr); + ASSERT_NE(std::dynamic_pointer_cast>(formula->getAction(0)).get(), nullptr); + ASSERT_NE(std::dynamic_pointer_cast>(formula->getAction(1)).get(), nullptr); + ASSERT_NE(std::dynamic_pointer_cast>(formula->getAction(2)).get(), nullptr); + ASSERT_NE(std::dynamic_pointer_cast>(formula->getAction(3)).get(), nullptr); + ASSERT_NE(std::dynamic_pointer_cast>(formula->getAction(4)).get(), nullptr); ASSERT_FALSE(formula->getChild()->isPropositional()); ASSERT_FALSE(formula->getChild()->isProbEventuallyAP()); diff --git a/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp b/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp index 2d2850ac2..1b6b5e5c8 100644 --- a/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp +++ b/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp @@ -21,8 +21,8 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, Crowds) { storm::modelchecker::prctl::SparseDtmcPrctlModelChecker mc(*dtmc, new storm::solver::GmmxxLinearEquationSolver()); - auto apFormula = std::make_shared>("observe0Greater1"); - auto eventuallyFormula = std::make_shared>(apFormula); + auto apFormula = std::make_shared>("observe0Greater1"); + auto eventuallyFormula = std::make_shared>(apFormula); LOG4CPLUS_WARN(logger, "Model Checking P=? [F observe0Greater1] on crowds/crowds20_5..."); std::vector result = eventuallyFormula->check(mc, false); @@ -30,8 +30,8 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, Crowds) { ASSERT_LT(std::abs(result[0] - 0.2296800237), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); - apFormula = std::make_shared>("observeIGreater1"); - eventuallyFormula = std::make_shared>(apFormula); + apFormula = std::make_shared>("observeIGreater1"); + eventuallyFormula = std::make_shared>(apFormula); LOG4CPLUS_WARN(logger, "Model Checking P=? [F observeIGreater1] on crowds/crowds20_5..."); result = eventuallyFormula->check(mc, false); @@ -39,8 +39,8 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, Crowds) { ASSERT_LT(std::abs(result[0] - 0.05073232193), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); - apFormula = std::make_shared>("observeOnlyTrueSender"); - eventuallyFormula = std::make_shared>(apFormula); + apFormula = std::make_shared>("observeOnlyTrueSender"); + eventuallyFormula = std::make_shared>(apFormula); LOG4CPLUS_WARN(logger, "Model Checking P=? [F observeOnlyTrueSender] on crowds/crowds20_5..."); result = eventuallyFormula->check(mc, false); @@ -65,8 +65,8 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, SynchronousLeader) { storm::modelchecker::prctl::SparseDtmcPrctlModelChecker mc(*dtmc, new storm::solver::GmmxxLinearEquationSolver()); - auto apFormula = std::make_shared>("elected"); - auto eventuallyFormula = std::make_shared>(apFormula); + auto apFormula = std::make_shared>("elected"); + auto eventuallyFormula = std::make_shared>(apFormula); LOG4CPLUS_WARN(logger, "Model Checking P=? [F elected] on synchronous_leader/leader6_8..."); std::vector result = eventuallyFormula->check(mc, false); @@ -74,8 +74,8 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, SynchronousLeader) { ASSERT_LT(std::abs(result[0] - 1.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); - apFormula = std::make_shared>("elected"); - auto boundedUntilFormula = std::make_shared>(std::make_shared>("true"), apFormula, 20); + apFormula = std::make_shared>("elected"); + auto boundedUntilFormula = std::make_shared>(std::make_shared>("true"), apFormula, 20); LOG4CPLUS_WARN(logger, "Model Checking P=? [F<=20 elected] on synchronous_leader/leader6_8..."); result = boundedUntilFormula->check(mc, false); @@ -83,8 +83,8 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, SynchronousLeader) { ASSERT_LT(std::abs(result[0] - 0.9993949793), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); - apFormula = std::make_shared>("elected"); - auto reachabilityRewardFormula = std::make_shared>(apFormula); + apFormula = std::make_shared>("elected"); + auto reachabilityRewardFormula = std::make_shared>(apFormula); LOG4CPLUS_WARN(logger, "Model Checking R=? [F elected] on synchronous_leader/leader6_8..."); result = reachabilityRewardFormula->check(mc, false); diff --git a/test/performance/modelchecker/SparseMdpPrctlModelCheckerTest.cpp b/test/performance/modelchecker/SparseMdpPrctlModelCheckerTest.cpp index 3152e0b6d..0a177b588 100644 --- a/test/performance/modelchecker/SparseMdpPrctlModelCheckerTest.cpp +++ b/test/performance/modelchecker/SparseMdpPrctlModelCheckerTest.cpp @@ -19,8 +19,8 @@ TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) { storm::modelchecker::prctl::SparseMdpPrctlModelChecker mc(*mdp, std::shared_ptr>(new storm::solver::NativeNondeterministicLinearEquationSolver())); - auto apFormula = std::make_shared>("elected"); - auto eventuallyFormula = std::make_shared>(apFormula); + auto apFormula = std::make_shared>("elected"); + auto eventuallyFormula = std::make_shared>(apFormula); std::vector result = mc.checkOptimizingOperator(*eventuallyFormula, true); @@ -30,8 +30,8 @@ TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) { ASSERT_LT(std::abs(result[0] - 1.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); - apFormula = std::make_shared>("elected"); - auto boundedEventuallyFormula = std::make_shared>(apFormula, 25); + apFormula = std::make_shared>("elected"); + auto boundedEventuallyFormula = std::make_shared>(apFormula, 25); result = mc.checkOptimizingOperator(*boundedEventuallyFormula, true); @@ -41,8 +41,8 @@ TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) { ASSERT_LT(std::abs(result[0] - 0.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); - apFormula = std::make_shared>("elected"); - auto reachabilityRewardFormula = std::make_shared>(apFormula); + apFormula = std::make_shared>("elected"); + auto reachabilityRewardFormula = std::make_shared>(apFormula); result = mc.checkOptimizingOperator(*reachabilityRewardFormula, true); @@ -69,43 +69,43 @@ TEST(SparseMdpPrctlModelCheckerTest, Consensus) { storm::modelchecker::prctl::SparseMdpPrctlModelChecker mc(*mdp, std::shared_ptr>(new storm::solver::NativeNondeterministicLinearEquationSolver())); - auto apFormula = std::make_shared>("finished"); - auto eventuallyFormula = std::make_shared>(apFormula); + auto apFormula = std::make_shared>("finished"); + auto eventuallyFormula = std::make_shared>(apFormula); std::vector result = mc.checkOptimizingOperator(*eventuallyFormula, true); ASSERT_LT(std::abs(result[31168] - 1.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); - apFormula = std::make_shared>("finished"); - auto apFormula2 = std::make_shared>("all_coins_equal_0"); - auto andFormula = std::make_shared>(apFormula, apFormula2); - eventuallyFormula = std::make_shared>(andFormula); + apFormula = std::make_shared>("finished"); + auto apFormula2 = std::make_shared>("all_coins_equal_0"); + auto andFormula = std::make_shared>(apFormula, apFormula2); + eventuallyFormula = std::make_shared>(andFormula); result = mc.checkOptimizingOperator(*eventuallyFormula, true); ASSERT_LT(std::abs(result[31168] - 0.4374282832), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); - apFormula = std::make_shared>("finished"); - apFormula2 = std::make_shared>("all_coins_equal_1"); - andFormula = std::make_shared>(apFormula, apFormula2); - eventuallyFormula = std::make_shared>(andFormula); + apFormula = std::make_shared>("finished"); + apFormula2 = std::make_shared>("all_coins_equal_1"); + andFormula = std::make_shared>(apFormula, apFormula2); + eventuallyFormula = std::make_shared>(andFormula); result = mc.checkOptimizingOperator(*eventuallyFormula, false); ASSERT_LT(std::abs(result[31168] - 0.5293286369), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); - apFormula = std::make_shared>("finished"); - apFormula2 = std::make_shared>("agree"); - auto notFormula = std::make_shared>(apFormula2); - andFormula = std::make_shared>(apFormula, notFormula); - eventuallyFormula = std::make_shared>(andFormula); + apFormula = std::make_shared>("finished"); + apFormula2 = std::make_shared>("agree"); + auto notFormula = std::make_shared>(apFormula2); + andFormula = std::make_shared>(apFormula, notFormula); + eventuallyFormula = std::make_shared>(andFormula); result = mc.checkOptimizingOperator(*eventuallyFormula, false); ASSERT_LT(std::abs(result[31168] - 0.10414097), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); - apFormula = std::make_shared>("finished"); - auto boundedEventuallyFormula = std::make_shared>(apFormula, 50ull); + apFormula = std::make_shared>("finished"); + auto boundedEventuallyFormula = std::make_shared>(apFormula, 50ull); result = mc.checkOptimizingOperator(*boundedEventuallyFormula, true); @@ -115,8 +115,8 @@ TEST(SparseMdpPrctlModelCheckerTest, Consensus) { ASSERT_LT(std::abs(result[31168] - 0.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); - apFormula = std::make_shared>("finished"); - auto reachabilityRewardFormula = std::make_shared>(apFormula); + apFormula = std::make_shared>("finished"); + auto reachabilityRewardFormula = std::make_shared>(apFormula); result = mc.checkOptimizingOperator(*reachabilityRewardFormula, true);