Storm
A Modern Probabilistic Model Checker
Toggle main menu visibility
Main Page
Namespaces
Namespace List
Namespace Members
All
_
a
b
c
d
e
f
g
h
i
j
k
l
m
n
o
p
q
r
s
t
u
v
w
x
z
Functions
_
a
b
c
d
e
f
g
h
i
j
l
m
n
o
p
q
r
s
t
u
v
w
x
z
Variables
a
b
c
d
e
f
g
i
l
m
n
o
p
q
r
s
t
u
v
w
z
Typedefs
a
b
c
e
f
i
j
m
n
o
p
r
s
v
Enumerations
a
b
c
d
e
f
g
l
m
n
o
p
q
r
s
t
u
Enumerator
Classes
Class List
Class Index
Class Hierarchy
Class Members
All
_
a
b
c
d
e
f
g
h
i
j
k
l
m
n
o
p
q
r
s
t
u
v
w
x
y
z
~
Functions
a
b
c
d
e
f
g
h
i
j
k
l
m
n
o
p
q
r
s
t
u
v
w
z
~
Variables
_
a
b
c
d
e
f
g
h
i
j
k
l
m
n
o
p
q
r
s
t
u
v
w
x
y
z
Typedefs
a
b
c
d
e
f
g
i
j
l
m
n
o
p
r
s
t
v
w
Enumerations
b
c
d
e
f
i
l
m
n
o
p
q
r
s
t
v
Enumerator
Related Symbols
a
b
c
d
e
f
i
m
n
o
p
r
s
t
v
x
Files
File List
File Members
All
a
b
c
d
e
g
i
m
n
o
p
r
s
t
w
Functions
b
c
e
g
i
m
n
o
p
r
s
t
Variables
Typedefs
Macros
a
b
c
e
m
p
s
w
•
All
Classes
Namespaces
Files
Functions
Variables
Typedefs
Enumerations
Enumerator
Friends
Macros
Pages
Loading...
Searching...
No Matches
ClockVariable.cpp
Go to the documentation of this file.
1
#include "
storm/storage/prism/ClockVariable.h
"
2
#include "
storm/adapters/RationalNumberAdapter.h
"
3
#include "
storm/storage/expressions/ExpressionManager.h
"
4
#include "
storm/utility/constants.h
"
5
6
namespace
storm
{
7
namespace
prism {
8
ClockVariable::ClockVariable
(
storm::expressions::Variable
const
& variable,
bool
observable, std::string
const
& filename, uint_fast64_t lineNumber)
9
:
Variable
(variable, variable.getManager().rational(
storm
::utility::zero<
storm
::RationalNumber>()), observable, filename, lineNumber) {
10
// Nothing to do here.
11
}
8
ClockVariable::ClockVariable
(
storm::expressions::Variable
const
& variable,
bool
observable, std::string
const
& filename, uint_fast64_t lineNumber) {
…
}
12
13
void
ClockVariable::createMissingInitialValue
() {
14
if
(!this->
hasInitialValue
()) {
15
this->
setInitialValueExpression
(this->
getExpressionVariable
().getManager().rational(storm::utility::zero<storm::RationalNumber>()));
16
}
17
}
13
void
ClockVariable::createMissingInitialValue
() {
…
}
18
19
std::ostream&
operator<<
(std::ostream& stream,
ClockVariable
const
& variable) {
20
stream << variable.
getName
() <<
": clock"
<<
";"
;
21
return
stream;
22
}
19
std::ostream&
operator<<
(std::ostream& stream,
ClockVariable
const
& variable) {
…
};
23
24
}
// namespace prism
25
}
// namespace storm
ClockVariable.h
ExpressionManager.h
RationalNumberAdapter.h
storm::expressions::Variable
Definition
Variable.h:18
storm::prism::ClockVariable
Definition
ClockVariable.h:9
storm::prism::ClockVariable::ClockVariable
ClockVariable()=default
storm::prism::ClockVariable::createMissingInitialValue
virtual void createMissingInitialValue() override
Sets a missing initial value (note that for clock variables, this is always zero)
Definition
ClockVariable.cpp:13
storm::prism::Variable
Definition
Variable.h:13
storm::prism::Variable::getExpressionVariable
storm::expressions::Variable const & getExpressionVariable() const
Retrieves the expression variable associated with this variable.
Definition
Variable.cpp:40
storm::prism::Variable::setInitialValueExpression
void setInitialValueExpression(storm::expressions::Expression const &initialValueExpression)
Sets the expression defining the initial value of the variable.
Definition
Variable.cpp:36
storm::prism::Variable::getName
std::string const & getName() const
Retrieves the name of the variable.
Definition
Variable.cpp:24
storm::prism::Variable::hasInitialValue
bool hasInitialValue() const
Retrieves whether the variable has an initial value.
Definition
Variable.cpp:28
constants.h
storm::prism::operator<<
std::ostream & operator<<(std::ostream &stream, Assignment const &assignment)
Definition
Assignment.cpp:39
storm
LabParser.cpp.
Definition
cli.cpp:18
src
storm
storage
prism
ClockVariable.cpp
Generated by
1.9.8