Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
SymbolicQualitativeResult.h
Go to the documentation of this file.
1
#pragma once
2
3
#include "
storm/storage/dd/DdType.h
"
4
5
#include "
storm-gamebased-ar/abstraction/QualitativeResult.h
"
6
#include "
storm/storage/dd/sylvan/InternalSylvanBdd.h
"
7
8
namespace
storm
{
9
namespace
dd {
10
template
<storm::dd::DdType Type>
11
class
Bdd
;
12
}
13
}
// namespace storm
14
15
namespace
storm::gbar
{
16
namespace
abstraction {
17
18
template
<storm::dd::DdType Type>
19
class
SymbolicQualitativeResult
:
public
QualitativeResult
{
20
public
:
21
virtual
~SymbolicQualitativeResult
() =
default
;
22
23
virtual
storm::dd::Bdd<Type>
const
&
getStates
()
const
= 0;
24
};
25
26
}
// namespace abstraction
27
}
// namespace storm::gbar
DdType.h
InternalSylvanBdd.h
QualitativeResult.h
storm::dd::Bdd
Definition
Bdd.h:25
storm::gbar::abstraction::QualitativeResult
Definition
QualitativeResult.h:13
storm::gbar::abstraction::SymbolicQualitativeResult
Definition
SymbolicQualitativeResult.h:19
storm::gbar::abstraction::SymbolicQualitativeResult::getStates
virtual storm::dd::Bdd< Type > const & getStates() const =0
storm::gbar::abstraction::SymbolicQualitativeResult::~SymbolicQualitativeResult
virtual ~SymbolicQualitativeResult()=default
storm::dft::modelchecker::Bdd
SFTBDDChecker::Bdd Bdd
Definition
SFTBDDChecker.cpp:14
storm::gbar
Definition
AbstractionInformation.cpp:13
storm
LabParser.cpp.
Definition
cli.cpp:18
src
storm-gamebased-ar
abstraction
SymbolicQualitativeResult.h
Generated by
1.9.8