You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
63 lines
2.8 KiB
63 lines
2.8 KiB
#ifndef STORM_MODELCHECKER_SYMBOLICQUALITATIVECHECKRESULT_H_
|
|
#define STORM_MODELCHECKER_SYMBOLICQUALITATIVECHECKRESULT_H_
|
|
|
|
#include "storm/storage/dd/DdType.h"
|
|
#include "storm/storage/dd/Bdd.h"
|
|
#include "storm/modelchecker/results/QualitativeCheckResult.h"
|
|
#include "storm/utility/OsDetection.h"
|
|
|
|
namespace storm {
|
|
namespace modelchecker {
|
|
template <storm::dd::DdType Type>
|
|
class SymbolicQualitativeCheckResult : public QualitativeCheckResult {
|
|
public:
|
|
SymbolicQualitativeCheckResult() = default;
|
|
SymbolicQualitativeCheckResult(storm::dd::Bdd<Type> const& reachableStates, storm::dd::Bdd<Type> const& truthValues);
|
|
SymbolicQualitativeCheckResult(storm::dd::Bdd<Type> const& reachableStates, storm::dd::Bdd<Type> const& states, storm::dd::Bdd<Type> const& truthValues);
|
|
|
|
SymbolicQualitativeCheckResult(SymbolicQualitativeCheckResult const& other) = default;
|
|
SymbolicQualitativeCheckResult& operator=(SymbolicQualitativeCheckResult const& other) = default;
|
|
#ifndef WINDOWS
|
|
SymbolicQualitativeCheckResult(SymbolicQualitativeCheckResult&& other) = default;
|
|
SymbolicQualitativeCheckResult& operator=(SymbolicQualitativeCheckResult&& other) = default;
|
|
#endif
|
|
|
|
virtual std::unique_ptr<CheckResult> clone() const override;
|
|
|
|
virtual bool isSymbolic() const override;
|
|
virtual bool isResultForAllStates() const override;
|
|
|
|
virtual bool isSymbolicQualitativeCheckResult() const override;
|
|
|
|
virtual QualitativeCheckResult& operator&=(QualitativeCheckResult const& other) override;
|
|
virtual QualitativeCheckResult& operator|=(QualitativeCheckResult const& other) override;
|
|
virtual void complement() override;
|
|
|
|
|
|
virtual bool existsTrue() const override;
|
|
virtual bool forallTrue() const override;
|
|
virtual uint64_t count() const override;
|
|
|
|
|
|
storm::dd::Bdd<Type> const& getTruthValuesVector() const;
|
|
storm::dd::Bdd<Type> const& getStates() const;
|
|
storm::dd::Bdd<Type> const& getReachableStates() const;
|
|
|
|
virtual std::ostream& writeToStream(std::ostream& out) const override;
|
|
|
|
virtual void filter(QualitativeCheckResult const& filter) override;
|
|
|
|
private:
|
|
// The set of all reachable states.
|
|
storm::dd::Bdd<Type> reachableStates;
|
|
|
|
// The set of states for which this check result contains values.
|
|
storm::dd::Bdd<Type> states;
|
|
|
|
// The values of the qualitative check result.
|
|
storm::dd::Bdd<Type> truthValues;
|
|
};
|
|
}
|
|
}
|
|
|
|
#endif /* STORM_MODELCHECKER_SYMBOLICQUALITATIVECHECKRESULT_H_ */
|