diff --git a/resources/3rdparty/CMakeLists.txt b/resources/3rdparty/CMakeLists.txt index f5606a095..d52134a56 100644 --- a/resources/3rdparty/CMakeLists.txt +++ b/resources/3rdparty/CMakeLists.txt @@ -208,9 +208,7 @@ include(${STORM_3RDPARTY_SOURCE_DIR}/include_cudd.cmake) ############################################################# set(STORM_HAVE_CARL OFF) -set(CARL_MINYEAR 17) -set(CARL_MINMONTH 08) -set(CARL_MINPATCH 0) +set(CARL_MINVERSION "17.08") if (NOT STORM_FORCE_SHIPPED_CARL) if (NOT "${STORM_CARL_DIR_HINT}" STREQUAL "") find_package(carl QUIET PATHS ${STORM_CARL_DIR_HINT} NO_DEFAULT_PATH) @@ -228,20 +226,8 @@ if(carl_FOUND AND NOT STORM_FORCE_SHIPPED_CARL) else() message(SEND_ERROR "File ${carlLOCATION} does not exist, did you build carl?") endif() - if("${carl_MINORYEARVERSION}" STREQUAL "" OR "${carl_MINORMONTHVERSION}" STREQUAL "" OR "${carl_MAINTENANCEVERSION}" STREQUAL "") - # don't have detailed version information, probably an old version of carl - message(FATAL_ERROR "Carl at ${carlLOCATION} outdated, require ${CARL_MINYEAR}.${CARL_MINMONTH}.${CARL_MINPATCH}, have ${carl_VERSION}") - endif() - if(${carl_MINORYEARVERSION} LESS ${CARL_MINYEAR}) - message(SEND_ERROR "Carl outdated, require ${CARL_MINYEAR}.${CARL_MINMONTH}.${CARL_MINPATCH}, have ${carl_VERSION}") - elseif(${carl_MINORYEARVERSION} EQUAL ${CARL_MINYEAR}) - if(${carl_MINORMONTHVERSION} LESS ${CARL_MINMONTH}) - message(SEND_ERROR "Carl outdated, require ${CARL_MINYEAR}.${CARL_MINMONTH}.${CARL_MINPATCH}, have ${carl_VERSION}") - elseif(${carl_MINORMONTHVERSION} EQUAL ${CARL_MINMONTH}) - if(${carl_MAINTENANCEVERSION} LESS ${CARL_MINPATCH}) - message(SEND_ERROR "Carl outdated, require ${CARL_MINYEAR}.${CARL_MINMONTH}.${CARL_MINPATCH}, have ${carl_VERSION}") - endif() - endif() + if("${carl_VERSION}" VERSION_LESS "${CARL_MINVERSION}") + message(SEND_ERROR "Carl outdated, require ${CARL_MINVERSION}, have ${carl_VERSION}") endif() set(STORM_SHIPPED_CARL OFF) diff --git a/src/storm-dft/builder/DftExplorationHeuristic.h b/src/storm-dft/builder/DftExplorationHeuristic.h index f4cc3c1ce..2de704e29 100644 --- a/src/storm-dft/builder/DftExplorationHeuristic.h +++ b/src/storm-dft/builder/DftExplorationHeuristic.h @@ -22,6 +22,8 @@ namespace storm { DFTExplorationHeuristic(size_t id, DFTExplorationHeuristic const& predecessor, ValueType rate, ValueType exitRate); + virtual ~DFTExplorationHeuristic() = default; + void setBounds(ValueType lowerBound, ValueType upperBound); virtual bool updateHeuristicValues(DFTExplorationHeuristic const& predecessor, ValueType rate, ValueType exitRate) = 0; diff --git a/src/storm-pgcl/storage/pgcl/AbstractStatementVisitor.h b/src/storm-pgcl/storage/pgcl/AbstractStatementVisitor.h index 75cb54186..0c0809e94 100755 --- a/src/storm-pgcl/storage/pgcl/AbstractStatementVisitor.h +++ b/src/storm-pgcl/storage/pgcl/AbstractStatementVisitor.h @@ -13,6 +13,8 @@ namespace storm { */ class AbstractStatementVisitor { public: + virtual ~AbstractStatementVisitor() = default; + // Those functions need to be implemented for every possible // statement instantiation. virtual void visit(class AssignmentStatement const&) = 0; diff --git a/src/storm-pgcl/storage/ppg/ProgramAction.h b/src/storm-pgcl/storage/ppg/ProgramAction.h index adeb1c858..839a097c7 100644 --- a/src/storm-pgcl/storage/ppg/ProgramAction.h +++ b/src/storm-pgcl/storage/ppg/ProgramAction.h @@ -13,7 +13,9 @@ namespace storm { ProgramAction(ProgramGraph* graph, ProgramActionIdentifier id) : graph(graph), actId(id) { } - + + virtual ~ProgramAction() = default; + ProgramActionIdentifier id() const { return actId; } diff --git a/src/storm/abstraction/MenuGameAbstractor.h b/src/storm/abstraction/MenuGameAbstractor.h index 283559470..946fb0a97 100644 --- a/src/storm/abstraction/MenuGameAbstractor.h +++ b/src/storm/abstraction/MenuGameAbstractor.h @@ -24,6 +24,8 @@ namespace storm { template class MenuGameAbstractor { public: + virtual ~MenuGameAbstractor() = default; + /// Retrieves the abstraction. virtual MenuGame abstract() = 0; diff --git a/src/storm/abstraction/QualitativeResult.h b/src/storm/abstraction/QualitativeResult.h index 8d2873541..0d027b3a7 100644 --- a/src/storm/abstraction/QualitativeResult.h +++ b/src/storm/abstraction/QualitativeResult.h @@ -13,6 +13,8 @@ namespace storm { template class QualitativeResult { public: + virtual ~QualitativeResult() = default; + virtual storm::dd::Bdd const& getStates() const = 0; }; diff --git a/src/storm/abstraction/QualitativeResultMinMax.h b/src/storm/abstraction/QualitativeResultMinMax.h index e748d4023..b6aa96382 100644 --- a/src/storm/abstraction/QualitativeResultMinMax.h +++ b/src/storm/abstraction/QualitativeResultMinMax.h @@ -10,6 +10,8 @@ namespace storm { class QualitativeResultMinMax { public: + virtual ~QualitativeResultMinMax() = default; + virtual bool isSymbolic() const; template diff --git a/src/storm/abstraction/StateSet.h b/src/storm/abstraction/StateSet.h index 2a4e0642d..badeaf534 100644 --- a/src/storm/abstraction/StateSet.h +++ b/src/storm/abstraction/StateSet.h @@ -10,6 +10,8 @@ namespace storm { class StateSet { public: + virtual ~StateSet() = default; + virtual bool isSymbolic() const; template diff --git a/src/storm/counterexamples/Counterexample.h b/src/storm/counterexamples/Counterexample.h index 8cd93178d..060f1f718 100644 --- a/src/storm/counterexamples/Counterexample.h +++ b/src/storm/counterexamples/Counterexample.h @@ -7,6 +7,8 @@ namespace storm { class Counterexample { public: + virtual ~Counterexample() = default; + virtual void writeToStream(std::ostream& out) const = 0; }; diff --git a/src/storm/exceptions/BaseException.cpp b/src/storm/exceptions/BaseException.cpp index 626231487..86119f600 100644 --- a/src/storm/exceptions/BaseException.cpp +++ b/src/storm/exceptions/BaseException.cpp @@ -19,11 +19,8 @@ namespace storm { } const char* BaseException::what() const NOEXCEPT { - std::string errorString = this->stream.str(); - char* result = new char[errorString.size() + 1]; - result[errorString.size()] = '\0'; - std::copy(errorString.begin(), errorString.end(), result); - return result; + errorString = this->stream.str(); + return errorString.c_str(); } } } diff --git a/src/storm/exceptions/BaseException.h b/src/storm/exceptions/BaseException.h index f9224cfb9..a3febc290 100644 --- a/src/storm/exceptions/BaseException.h +++ b/src/storm/exceptions/BaseException.h @@ -46,6 +46,10 @@ namespace storm { protected: // This stream stores the message of this exception. std::stringstream stream; + + private: + // storage for the string backing the C string returned by what() + mutable std::string errorString; }; } // namespace exceptions diff --git a/src/storm/logic/FormulaVisitor.h b/src/storm/logic/FormulaVisitor.h index 9548096f7..f0abd0436 100644 --- a/src/storm/logic/FormulaVisitor.h +++ b/src/storm/logic/FormulaVisitor.h @@ -10,6 +10,8 @@ namespace storm { class FormulaVisitor { public: + virtual ~FormulaVisitor() = default; + virtual boost::any visit(AtomicExpressionFormula const& f, boost::any const& data) const = 0; virtual boost::any visit(AtomicLabelFormula const& f, boost::any const& data) const = 0; virtual boost::any visit(BinaryBooleanStateFormula const& f, boost::any const& data) const = 0; diff --git a/src/storm/modelchecker/hints/ModelCheckerHint.h b/src/storm/modelchecker/hints/ModelCheckerHint.h index 14dd4dcbb..5ee82aea5 100644 --- a/src/storm/modelchecker/hints/ModelCheckerHint.h +++ b/src/storm/modelchecker/hints/ModelCheckerHint.h @@ -15,7 +15,8 @@ namespace storm { class ModelCheckerHint { public: ModelCheckerHint() = default; - + virtual ~ModelCheckerHint() = default; + // Returns true iff this hint does not contain any information. virtual bool isEmpty() const; diff --git a/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessorTask.h b/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessorTask.h index f84b935b6..474eb10f8 100644 --- a/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessorTask.h +++ b/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessorTask.h @@ -24,7 +24,9 @@ namespace storm { SparseMultiObjectivePreprocessorTask(std::shared_ptr> const& objective) : objective(objective) { // intentionally left empty } - + + virtual ~SparseMultiObjectivePreprocessorTask() = default; + virtual void perform(SparseModelType& preprocessedModel) const = 0; virtual bool requiresEndComponentAnalysis() const { diff --git a/src/storm/modelchecker/prctl/helper/DsMpiUpperRewardBoundsComputer.h b/src/storm/modelchecker/prctl/helper/DsMpiUpperRewardBoundsComputer.h index 7f2bb4278..f49470dcf 100644 --- a/src/storm/modelchecker/prctl/helper/DsMpiUpperRewardBoundsComputer.h +++ b/src/storm/modelchecker/prctl/helper/DsMpiUpperRewardBoundsComputer.h @@ -27,7 +27,9 @@ namespace storm { * @param oneStepTargetProbabilities For each state the probability to go to a goal state in one step. */ DsMpiDtmcUpperRewardBoundsComputer(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& rewards, std::vector const& oneStepTargetProbabilities); - + + virtual ~DsMpiDtmcUpperRewardBoundsComputer() = default; + /*! * Computes upper bounds on the expected rewards. */ diff --git a/src/storm/models/sparse/ItemLabeling.h b/src/storm/models/sparse/ItemLabeling.h index 746320afd..04d9950d2 100644 --- a/src/storm/models/sparse/ItemLabeling.h +++ b/src/storm/models/sparse/ItemLabeling.h @@ -33,6 +33,7 @@ namespace storm { ItemLabeling(ItemLabeling const& other) = default; ItemLabeling& operator=(ItemLabeling const& other) = default; + virtual ~ItemLabeling() = default; virtual bool isStateLabeling() const; virtual bool isChoiceLabeling() const; diff --git a/src/storm/models/sparse/StateAnnotation.h b/src/storm/models/sparse/StateAnnotation.h index b42e2c9be..edaf0feda 100644 --- a/src/storm/models/sparse/StateAnnotation.h +++ b/src/storm/models/sparse/StateAnnotation.h @@ -9,6 +9,8 @@ namespace storm { class StateAnnotation { public: + virtual ~StateAnnotation() = default; + virtual std::string getStateInfo(storm::storage::sparse::state_type const& state) const = 0; }; diff --git a/src/storm/permissivesched/PermissiveSchedulerComputation.h b/src/storm/permissivesched/PermissiveSchedulerComputation.h index 372b4a15d..5aa2f400e 100644 --- a/src/storm/permissivesched/PermissiveSchedulerComputation.h +++ b/src/storm/permissivesched/PermissiveSchedulerComputation.h @@ -26,8 +26,9 @@ namespace storm { { } - - + + virtual ~PermissiveSchedulerComputation() = default; + virtual void calculatePermissiveScheduler(bool lowerBound, double boundary) = 0; void setPenalties(PermissiveSchedulerPenalties penalties) { diff --git a/src/storm/settings/ArgumentBase.h b/src/storm/settings/ArgumentBase.h index b48a46183..4a5b4f133 100644 --- a/src/storm/settings/ArgumentBase.h +++ b/src/storm/settings/ArgumentBase.h @@ -26,7 +26,9 @@ namespace storm { ArgumentBase(std::string const& name, std::string const& description) : hasBeenSet(false), name(name), description(description) { // Intentionally left empty. } - + + virtual ~ArgumentBase() = default; + /*! * Retrieves the type of the argument. * diff --git a/src/storm/settings/ArgumentValidators.h b/src/storm/settings/ArgumentValidators.h index 4b3b0b3d8..93ced6f26 100644 --- a/src/storm/settings/ArgumentValidators.h +++ b/src/storm/settings/ArgumentValidators.h @@ -12,6 +12,8 @@ namespace storm { template class ArgumentValidator { public: + virtual ~ArgumentValidator() = default; + /*! * Checks whether the argument passes the validation. */ diff --git a/src/storm/solver/GameSolver.h b/src/storm/solver/GameSolver.h index 23c3b7bc3..fd9e63667 100644 --- a/src/storm/solver/GameSolver.h +++ b/src/storm/solver/GameSolver.h @@ -137,6 +137,7 @@ namespace storm { class GameSolverFactory { public: GameSolverFactory(); + virtual ~GameSolverFactory() = default; virtual std::unique_ptr> create(Environment const& env, storm::storage::SparseMatrix const& player1Matrix, storm::storage::SparseMatrix const& player2Matrix) const; virtual std::unique_ptr> create(Environment const& env, storm::storage::SparseMatrix&& player1Matrix, storm::storage::SparseMatrix&& player2Matrix) const; diff --git a/src/storm/solver/LinearEquationSolver.h b/src/storm/solver/LinearEquationSolver.h index ae8281615..de17808c8 100644 --- a/src/storm/solver/LinearEquationSolver.h +++ b/src/storm/solver/LinearEquationSolver.h @@ -182,6 +182,8 @@ namespace storm { template class LinearEquationSolverFactory { public: + virtual ~LinearEquationSolverFactory() = default; + /*! * Creates a new linear equation solver instance with the given matrix. * diff --git a/src/storm/solver/LpSolver.h b/src/storm/solver/LpSolver.h index 7ec7cb906..08d91c463 100644 --- a/src/storm/solver/LpSolver.h +++ b/src/storm/solver/LpSolver.h @@ -36,6 +36,8 @@ namespace storm { */ LpSolver(OptimizationDirection const& optDir); + virtual ~LpSolver() = default; + /*! * Registers an upper- and lower-bounded continuous variable, i.e. a variable that may take all real values * within its bounds. diff --git a/src/storm/solver/MinMaxLinearEquationSolver.h b/src/storm/solver/MinMaxLinearEquationSolver.h index 33297aa07..c2b30eeda 100644 --- a/src/storm/solver/MinMaxLinearEquationSolver.h +++ b/src/storm/solver/MinMaxLinearEquationSolver.h @@ -210,6 +210,7 @@ namespace storm { class MinMaxLinearEquationSolverFactory { public: MinMaxLinearEquationSolverFactory(); + virtual ~MinMaxLinearEquationSolverFactory() = default; std::unique_ptr> create(Environment const& env, storm::storage::SparseMatrix const& matrix) const; std::unique_ptr> create(Environment const& env, storm::storage::SparseMatrix&& matrix) const; diff --git a/src/storm/solver/SmtSolver.h b/src/storm/solver/SmtSolver.h index 3e3a4eeb5..6d842500c 100644 --- a/src/storm/solver/SmtSolver.h +++ b/src/storm/solver/SmtSolver.h @@ -36,7 +36,8 @@ namespace storm { * @param manager The manager responsible for the variables whose value can be requested. */ ModelReference(storm::expressions::ExpressionManager const& manager); - + virtual ~ModelReference() = default; + virtual bool getBooleanValue(storm::expressions::Variable const& variable) const = 0; virtual int_fast64_t getIntegerValue(storm::expressions::Variable const& variable) const = 0; virtual double getRationalValue(storm::expressions::Variable const& variable) const = 0; diff --git a/src/storm/solver/SymbolicEquationSolver.h b/src/storm/solver/SymbolicEquationSolver.h index 73681d762..b4aa62933 100644 --- a/src/storm/solver/SymbolicEquationSolver.h +++ b/src/storm/solver/SymbolicEquationSolver.h @@ -13,6 +13,7 @@ namespace storm { public: SymbolicEquationSolver() = default; SymbolicEquationSolver(storm::dd::Bdd const& allRows); + virtual ~SymbolicEquationSolver() = default; virtual void setLowerBounds(storm::dd::Add const& lowerBounds); virtual void setLowerBound(ValueType const& lowerBound); diff --git a/src/storm/solver/SymbolicGameSolver.h b/src/storm/solver/SymbolicGameSolver.h index 095a3684a..69446f3d1 100644 --- a/src/storm/solver/SymbolicGameSolver.h +++ b/src/storm/solver/SymbolicGameSolver.h @@ -38,6 +38,8 @@ namespace storm { */ SymbolicGameSolver(storm::dd::Add const& A, storm::dd::Bdd const& allRows, storm::dd::Bdd const& illegalPlayer1Mask, storm::dd::Bdd const& illegalPlayer2Mask, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs, std::set const& player1Variables, std::set const& player2Variables); + virtual ~SymbolicGameSolver() = default; + /*! * Solves the equation system defined by the game matrix. Note that the game matrix has to be given upon * construction time of the solver object. @@ -108,6 +110,8 @@ namespace storm { template class SymbolicGameSolverFactory { public: + virtual ~SymbolicGameSolverFactory() = default; + virtual std::unique_ptr> create(storm::dd::Add const& A, storm::dd::Bdd const& allRows, storm::dd::Bdd const& illegalPlayer1Mask, storm::dd::Bdd const& illegalPlayer2Mask, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs, std::set const& player1Variables, std::set const& player2Variables) const; }; diff --git a/src/storm/solver/SymbolicLinearEquationSolver.h b/src/storm/solver/SymbolicLinearEquationSolver.h index bb4b0f986..0eb02da1a 100644 --- a/src/storm/solver/SymbolicLinearEquationSolver.h +++ b/src/storm/solver/SymbolicLinearEquationSolver.h @@ -36,7 +36,8 @@ namespace storm { class SymbolicLinearEquationSolver : public SymbolicEquationSolver { public: SymbolicLinearEquationSolver(); - + virtual ~SymbolicLinearEquationSolver() = default; + /*! * Constructs a symbolic linear equation solver with the given meta variable sets and pairs. * @@ -119,6 +120,8 @@ namespace storm { template class SymbolicLinearEquationSolverFactory { public: + virtual ~SymbolicLinearEquationSolverFactory() = default; + std::unique_ptr> create(Environment const& env, storm::dd::Bdd const& allRows, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs) const; std::unique_ptr> create(Environment const& env, storm::dd::Add const& A, storm::dd::Bdd const& allRows, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs) const; diff --git a/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp b/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp index 10cad8986..d9b7698de 100644 --- a/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp @@ -277,6 +277,7 @@ namespace storm { if (solver.getEquationProblemFormat(env) == storm::solver::LinearEquationSolverProblemFormat::EquationSystem) { schedulerA = diagonal - schedulerA; } + storm::dd::Add schedulerB = scheduler.ite(b, scheduler.getDdManager().template getAddZero()).sumAbstract(this->choiceVariables); // Set the matrix for the solver. @@ -314,9 +315,16 @@ namespace storm { storm::dd::Bdd nextScheduler; if (dir == storm::solver::OptimizationDirection::Minimize) { choiceValues += illegalMaskAdd; - nextScheduler = choiceValues.minAbstractRepresentative(this->choiceVariables); + + storm::dd::Add newStateValues = choiceValues.minAbstract(this->choiceVariables); + storm::dd::Bdd improvedStates = newStateValues.less(schedulerX); + + nextScheduler = improvedStates.ite(choiceValues.minAbstractRepresentative(this->choiceVariables), scheduler); } else { - nextScheduler = choiceValues.maxAbstractRepresentative(this->choiceVariables); + storm::dd::Add newStateValues = choiceValues.maxAbstract(this->choiceVariables); + storm::dd::Bdd improvedStates = newStateValues.greater(schedulerX); + + nextScheduler = improvedStates.ite(choiceValues.maxAbstractRepresentative(this->choiceVariables), scheduler); } // Check for convergence. diff --git a/src/storm/solver/SymbolicMinMaxLinearEquationSolver.h b/src/storm/solver/SymbolicMinMaxLinearEquationSolver.h index 70cf90536..95be76a0c 100644 --- a/src/storm/solver/SymbolicMinMaxLinearEquationSolver.h +++ b/src/storm/solver/SymbolicMinMaxLinearEquationSolver.h @@ -40,7 +40,8 @@ namespace storm { class SymbolicMinMaxLinearEquationSolver : public SymbolicEquationSolver { public: SymbolicMinMaxLinearEquationSolver(); - + virtual ~SymbolicMinMaxLinearEquationSolver() = default; + /*! * Constructs a symbolic min/max linear equation solver with the given meta variable sets and pairs. * @@ -213,6 +214,8 @@ namespace storm { template class SymbolicMinMaxLinearEquationSolverFactory { public: + virtual ~SymbolicMinMaxLinearEquationSolverFactory() = default; + virtual std::unique_ptr> create(storm::dd::Add const& A, storm::dd::Bdd const& allRows, storm::dd::Bdd const& illegalMask, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::set const& choiceVariables, std::vector> const& rowColumnMetaVariablePairs) const = 0; /*! diff --git a/src/storm/solver/TerminationCondition.h b/src/storm/solver/TerminationCondition.h index 86733ade9..a8e21697e 100644 --- a/src/storm/solver/TerminationCondition.h +++ b/src/storm/solver/TerminationCondition.h @@ -10,6 +10,8 @@ namespace storm { template class TerminationCondition { public: + virtual ~TerminationCondition() = default; + /*! * Retrieves whether the guarantee provided by the solver for the current result is sufficient to terminate. */ diff --git a/src/storm/solver/stateelimination/EliminatorBase.h b/src/storm/solver/stateelimination/EliminatorBase.h index 1d918d562..996da58e6 100644 --- a/src/storm/solver/stateelimination/EliminatorBase.h +++ b/src/storm/solver/stateelimination/EliminatorBase.h @@ -19,7 +19,8 @@ namespace storm { typedef typename FlexibleRowType::iterator FlexibleRowIterator; EliminatorBase(storm::storage::FlexibleSparseMatrix& matrix, storm::storage::FlexibleSparseMatrix& transposedMatrix); - + virtual ~EliminatorBase() = default; + void eliminate(uint64_t row, uint64_t column, bool clearRow); // Provide virtual methods that can be customized by subclasses to govern side-effect of the elimination. diff --git a/src/storm/solver/stateelimination/StatePriorityQueue.h b/src/storm/solver/stateelimination/StatePriorityQueue.h index f5cf6c445..cc133fced 100644 --- a/src/storm/solver/stateelimination/StatePriorityQueue.h +++ b/src/storm/solver/stateelimination/StatePriorityQueue.h @@ -10,6 +10,8 @@ namespace storm { class StatePriorityQueue { public: + virtual ~StatePriorityQueue() = default; + virtual bool hasNext() const = 0; virtual storm::storage::sparse::state_type pop() = 0; virtual void update(storm::storage::sparse::state_type state); diff --git a/src/storm/storage/BitVector.cpp b/src/storm/storage/BitVector.cpp index bf4b305a0..18ac1feb3 100644 --- a/src/storm/storage/BitVector.cpp +++ b/src/storm/storage/BitVector.cpp @@ -118,6 +118,7 @@ namespace storm { bitCount = other.bitCount; if (buckets && bucketCount() != other.bucketCount()) { delete[] buckets; + buckets = nullptr; } if (!buckets) { buckets = new uint64_t[other.bucketCount()]; @@ -157,6 +158,9 @@ namespace storm { // Only perform the assignment if the source and target are not identical. if (this != &other) { bitCount = other.bitCount; + if (this->buckets) { + delete[] this->buckets; + } this->buckets = other.buckets; other.buckets = nullptr; } diff --git a/src/storm/storage/bisimulation/BisimulationDecomposition.h b/src/storm/storage/bisimulation/BisimulationDecomposition.h index 6aa56345c..51383da56 100644 --- a/src/storm/storage/bisimulation/BisimulationDecomposition.h +++ b/src/storm/storage/bisimulation/BisimulationDecomposition.h @@ -180,7 +180,9 @@ namespace storm { * @param options The options to use during for the decomposition. */ BisimulationDecomposition(ModelType const& model, Options const& options); - + + virtual ~BisimulationDecomposition() = default; + /*! * Retrieves the quotient of the model under the computed bisimulation. * diff --git a/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp b/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp index 218b11ad7..12b5e39f5 100644 --- a/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp +++ b/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp @@ -255,6 +255,8 @@ namespace storm { STORM_LOG_TRACE("Partition has " << partitionBdd.existsAbstract(model.getRowVariables()).getNonZeroCount() << " states in " << this->numberOfBlocks << " blocks."); } + virtual ~InternalSparseQuotientExtractorBase() = default; + storm::storage::SparseMatrix extractTransitionMatrix(storm::dd::Add const& transitionMatrix) { return extractMatrixInternal(transitionMatrix); } diff --git a/src/storm/storage/dd/cudd/InternalCuddAdd.h b/src/storm/storage/dd/cudd/InternalCuddAdd.h index 64e1176e7..5871e20dc 100644 --- a/src/storm/storage/dd/cudd/InternalCuddAdd.h +++ b/src/storm/storage/dd/cudd/InternalCuddAdd.h @@ -67,7 +67,8 @@ namespace storm { InternalAdd& operator=(InternalAdd const& other) = default; InternalAdd(InternalAdd&& other) = default; InternalAdd& operator=(InternalAdd&& other) = default; - + virtual ~InternalAdd() = default; + /*! * Retrieves whether the two DDs represent the same function. * diff --git a/src/storm/storage/dd/sylvan/InternalSylvanAdd.h b/src/storm/storage/dd/sylvan/InternalSylvanAdd.h index c4374c2b1..79a29f187 100644 --- a/src/storm/storage/dd/sylvan/InternalSylvanAdd.h +++ b/src/storm/storage/dd/sylvan/InternalSylvanAdd.h @@ -60,7 +60,8 @@ namespace storm { InternalAdd& operator=(InternalAdd const& other) = default; InternalAdd(InternalAdd&& other) = default; InternalAdd& operator=(InternalAdd&& other) = default; - + virtual ~InternalAdd() = default; + /*! * Retrieves whether the two DDs represent the same function. * @@ -732,7 +733,7 @@ namespace storm { static MTBDD getLeaf(uint_fast64_t value); /*! - * Retrieves the sylvan representation of the given storm::RatíonalNumber. + * Retrieves the sylvan representation of the given storm::Rat�onalNumber. * * @return The sylvan node for the given value. */ diff --git a/src/storm/storage/expressions/CompiledExpression.h b/src/storm/storage/expressions/CompiledExpression.h index 786408c94..dfa0ea02b 100644 --- a/src/storm/storage/expressions/CompiledExpression.h +++ b/src/storm/storage/expressions/CompiledExpression.h @@ -7,6 +7,7 @@ namespace storm { class CompiledExpression { public: + virtual ~CompiledExpression() = default; virtual bool isExprtkCompiledExpression() const; ExprtkCompiledExpression& asExprtkCompiledExpression(); diff --git a/src/storm/storage/expressions/ExpressionEvaluatorBase.h b/src/storm/storage/expressions/ExpressionEvaluatorBase.h index 80ae61af6..8fd552d28 100644 --- a/src/storm/storage/expressions/ExpressionEvaluatorBase.h +++ b/src/storm/storage/expressions/ExpressionEvaluatorBase.h @@ -9,7 +9,8 @@ namespace storm { class ExpressionEvaluatorBase { public: ExpressionEvaluatorBase(storm::expressions::ExpressionManager const& manager); - + virtual ~ExpressionEvaluatorBase() = default; + virtual bool asBool(Expression const& expression) const = 0; virtual int_fast64_t asInt(Expression const& expression) const = 0; virtual RationalReturnType asRational(Expression const& expression) const = 0; diff --git a/src/storm/storage/expressions/ExpressionVisitor.h b/src/storm/storage/expressions/ExpressionVisitor.h index edbdc5d5a..8ef1ea90d 100644 --- a/src/storm/storage/expressions/ExpressionVisitor.h +++ b/src/storm/storage/expressions/ExpressionVisitor.h @@ -20,6 +20,8 @@ namespace storm { class ExpressionVisitor { public: + virtual ~ExpressionVisitor() = default; + virtual boost::any visit(IfThenElseExpression const& expression, boost::any const& data) = 0; virtual boost::any visit(BinaryBooleanFunctionExpression const& expression, boost::any const& data) = 0; virtual boost::any visit(BinaryNumericalFunctionExpression const& expression, boost::any const& data) = 0; diff --git a/src/storm/storage/expressions/Type.h b/src/storm/storage/expressions/Type.h index 44295b76f..b173d5d53 100644 --- a/src/storm/storage/expressions/Type.h +++ b/src/storm/storage/expressions/Type.h @@ -15,6 +15,7 @@ namespace storm { class BaseType { public: BaseType(); + virtual ~BaseType() = default; /*! * Retrieves the mask that is associated with this type. diff --git a/src/storm/storage/expressions/Variable.cpp b/src/storm/storage/expressions/Variable.cpp index 0259ab3e5..675f1caef 100644 --- a/src/storm/storage/expressions/Variable.cpp +++ b/src/storm/storage/expressions/Variable.cpp @@ -16,7 +16,7 @@ namespace storm { } bool Variable::operator==(Variable const& other) const { - return manager == other.manager && index == other.index; + return &this->getManager() == &other.getManager() && index == other.index; } bool Variable::operator!=(Variable const& other) const { @@ -48,8 +48,7 @@ namespace storm { } ExpressionManager const& Variable::getManager() const { - STORM_LOG_ASSERT(manager != nullptr, "Manager is null."); - return *manager; + return *manager.lock(); } bool Variable::hasBooleanType() const { diff --git a/src/storm/storage/expressions/Variable.h b/src/storm/storage/expressions/Variable.h index 8a51df376..3ecea02c0 100644 --- a/src/storm/storage/expressions/Variable.h +++ b/src/storm/storage/expressions/Variable.h @@ -138,7 +138,7 @@ namespace storm { private: // The manager that is responsible for this variable. - std::shared_ptr manager; + std::weak_ptr manager; // The index of the variable. uint_fast64_t index; diff --git a/src/storm/storage/jani/Composition.h b/src/storm/storage/jani/Composition.h index 773dd93cd..b1375cdce 100644 --- a/src/storm/storage/jani/Composition.h +++ b/src/storm/storage/jani/Composition.h @@ -9,6 +9,8 @@ namespace storm { class Composition { public: + virtual ~Composition() = default; + virtual boost::any accept(CompositionVisitor& visitor, boost::any const& data) const = 0; virtual void write(std::ostream& stream) const = 0; diff --git a/src/storm/storage/jani/CompositionVisitor.h b/src/storm/storage/jani/CompositionVisitor.h index c346826e2..c9086c722 100644 --- a/src/storm/storage/jani/CompositionVisitor.h +++ b/src/storm/storage/jani/CompositionVisitor.h @@ -11,6 +11,8 @@ namespace storm { class CompositionVisitor { public: + virtual ~CompositionVisitor() = default; + virtual boost::any visit(AutomatonComposition const& composition, boost::any const& data) = 0; virtual boost::any visit(ParallelComposition const& composition, boost::any const& data) = 0; }; diff --git a/src/storm/storage/prism/Composition.h b/src/storm/storage/prism/Composition.h index ac9602af6..06c61b362 100644 --- a/src/storm/storage/prism/Composition.h +++ b/src/storm/storage/prism/Composition.h @@ -10,6 +10,7 @@ namespace storm { class Composition { public: Composition() = default; + virtual ~Composition() = default; friend std::ostream& operator<<(std::ostream& stream, Composition const& composition); diff --git a/src/storm/storage/prism/CompositionVisitor.h b/src/storm/storage/prism/CompositionVisitor.h index 81f7ee40c..41fcd7f72 100644 --- a/src/storm/storage/prism/CompositionVisitor.h +++ b/src/storm/storage/prism/CompositionVisitor.h @@ -15,6 +15,8 @@ namespace storm { class CompositionVisitor { public: + virtual ~CompositionVisitor() = default; + virtual boost::any visit(ModuleComposition const& composition, boost::any const& data) = 0; virtual boost::any visit(RenamingComposition const& composition, boost::any const& data) = 0; virtual boost::any visit(HidingComposition const& composition, boost::any const& data) = 0; diff --git a/src/storm/storage/prism/Variable.h b/src/storm/storage/prism/Variable.h index 42ba9aec0..ae6c12935 100644 --- a/src/storm/storage/prism/Variable.h +++ b/src/storm/storage/prism/Variable.h @@ -17,7 +17,8 @@ namespace storm { Variable& operator=(Variable const& otherVariable)= default; Variable(Variable&& otherVariable) = default; Variable& operator=(Variable&& otherVariable) = default; - + virtual ~Variable() = default; + /*! * Retrieves the name of the variable. * diff --git a/src/storm/utility/solver.h b/src/storm/utility/solver.h index 2dd77f1d6..e75397535 100644 --- a/src/storm/utility/solver.h +++ b/src/storm/utility/solver.h @@ -59,6 +59,8 @@ namespace storm { template class LpSolverFactory { public: + virtual ~LpSolverFactory() = default; + /*! * Creates a new linear equation solver instance with the given name. * @@ -98,6 +100,8 @@ namespace storm { class SmtSolverFactory { public: + virtual ~SmtSolverFactory() = default; + /*! * Creates a new SMT solver instance. *